summaryrefslogtreecommitdiff
path: root/src/theory/booleans
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/booleans')
-rw-r--r--src/theory/booleans/circuit_propagator.cpp4
-rw-r--r--src/theory/booleans/circuit_propagator.h4
-rw-r--r--src/theory/booleans/kinds22
-rw-r--r--src/theory/booleans/proof_checker.cpp4
-rw-r--r--src/theory/booleans/proof_checker.h4
-rw-r--r--src/theory/booleans/proof_circuit_propagator.cpp4
-rw-r--r--src/theory/booleans/proof_circuit_propagator.h4
-rw-r--r--src/theory/booleans/theory_bool.cpp8
-rw-r--r--src/theory/booleans/theory_bool.h8
-rw-r--r--src/theory/booleans/theory_bool_rewriter.cpp8
-rw-r--r--src/theory/booleans/theory_bool_rewriter.h8
-rw-r--r--src/theory/booleans/theory_bool_type_rules.h8
-rw-r--r--src/theory/booleans/type_enumerator.h8
13 files changed, 47 insertions, 47 deletions
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index b50ec34c7..897c86e93 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -31,7 +31,7 @@
using namespace std;
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -814,4 +814,4 @@ void CircuitPropagator::addProof(TNode f, std::shared_ptr<ProofNode> pf)
} // namespace booleans
} // namespace theory
-} // namespace CVC4
+} // namespace CVC5
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index ba8c5782d..6caccef08 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -31,7 +31,7 @@
#include "expr/node.h"
#include "theory/trust_node.h"
-namespace CVC4 {
+namespace CVC5 {
class ProofGenerator;
class ProofNode;
@@ -274,6 +274,6 @@ class CircuitPropagator
} // namespace booleans
} // namespace theory
-} // namespace CVC4
+} // namespace CVC5
#endif /* CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 9d7b3fbd6..d8009ad12 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -4,12 +4,12 @@
# src/theory/builtin/kinds.
#
-theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h"
+theory THEORY_BOOL ::CVC5::theory::booleans::TheoryBool "theory/booleans/theory_bool.h"
typechecker "theory/booleans/theory_bool_type_rules.h"
properties finite
-rewriter ::CVC4::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
+rewriter ::CVC5::theory::booleans::TheoryBoolRewriter "theory/booleans/theory_bool_rewriter.h"
sort BOOLEAN_TYPE \
2 \
@@ -20,12 +20,12 @@ sort BOOLEAN_TYPE \
constant CONST_BOOLEAN \
bool \
- ::CVC4::BoolHashFunction \
+ ::CVC5::BoolHashFunction \
"util/bool.h" \
"truth and falsity; payload is a (C++) bool"
enumerator BOOLEAN_TYPE \
- "::CVC4::theory::booleans::BooleanEnumerator" \
+ "::CVC5::theory::booleans::BooleanEnumerator" \
"theory/booleans/type_enumerator.h"
operator NOT 1 "logical not"
@@ -35,13 +35,13 @@ operator OR 2: "logical or (N-ary)"
operator XOR 2 "exclusive or (exactly two parameters)"
operator ITE 3 "if-then-else, used for both Boolean and term ITE constructs; first parameter is (Boolean-sorted) condition, second is 'then', third is 'else' and these two parameters must have same base sort"
-typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule
+typerule CONST_BOOLEAN ::CVC5::theory::boolean::BooleanTypeRule
-typerule NOT ::CVC4::theory::boolean::BooleanTypeRule
-typerule AND ::CVC4::theory::boolean::BooleanTypeRule
-typerule IMPLIES ::CVC4::theory::boolean::BooleanTypeRule
-typerule OR ::CVC4::theory::boolean::BooleanTypeRule
-typerule XOR ::CVC4::theory::boolean::BooleanTypeRule
-typerule ITE ::CVC4::theory::boolean::IteTypeRule
+typerule NOT ::CVC5::theory::boolean::BooleanTypeRule
+typerule AND ::CVC5::theory::boolean::BooleanTypeRule
+typerule IMPLIES ::CVC5::theory::boolean::BooleanTypeRule
+typerule OR ::CVC5::theory::boolean::BooleanTypeRule
+typerule XOR ::CVC5::theory::boolean::BooleanTypeRule
+typerule ITE ::CVC5::theory::boolean::IteTypeRule
endtheory
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 6244ff3f4..a51f238a2 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -16,7 +16,7 @@
#include "expr/skolem_manager.h"
#include "theory/rewriter.h"
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -948,4 +948,4 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
} // namespace booleans
} // namespace theory
-} // namespace CVC4
+} // namespace CVC5
diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h
index 1d807fd90..93c3baf1e 100644
--- a/src/theory/booleans/proof_checker.h
+++ b/src/theory/booleans/proof_checker.h
@@ -20,7 +20,7 @@
#include "expr/node.h"
#include "expr/proof_checker.h"
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -43,6 +43,6 @@ class BoolProofRuleChecker : public ProofRuleChecker
} // namespace booleans
} // namespace theory
-} // namespace CVC4
+} // namespace CVC5
#endif /* CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H */
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index aaff82933..b84cf5488 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -21,7 +21,7 @@
#include "expr/proof_node.h"
#include "expr/proof_node_manager.h"
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -587,4 +587,4 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::xorEval(bool x,
} // namespace booleans
} // namespace theory
-} // namespace CVC4
+} // namespace CVC5
diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h
index fa472b602..671c6e964 100644
--- a/src/theory/booleans/proof_circuit_propagator.h
+++ b/src/theory/booleans/proof_circuit_propagator.h
@@ -24,7 +24,7 @@
#include "expr/node.h"
#include "expr/proof_rule.h"
-namespace CVC4 {
+namespace CVC5 {
class ProofNode;
class ProofNodeManager;
@@ -212,6 +212,6 @@ class ProofCircuitPropagatorForward : public ProofCircuitPropagator
} // namespace booleans
} // namespace theory
-} // namespace CVC4
+} // namespace CVC5
#endif
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index bdd428245..2df179e27 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -31,7 +31,7 @@
using namespace std;
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -80,6 +80,6 @@ Theory::PPAssertStatus TheoryBool::ppAssert(
return Theory::ppAssert(tin, outSubstitutions);
}
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace booleans
+} // namespace theory
+} // namespace CVC5
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 12c9fa72f..cbd9ec381 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -24,7 +24,7 @@
#include "theory/booleans/theory_bool_rewriter.h"
#include "theory/theory.h"
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -51,8 +51,8 @@ class TheoryBool : public Theory {
BoolProofRuleChecker d_bProofChecker;
};/* class TheoryBool */
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace booleans
+} // namespace theory
+} // namespace CVC5
#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_H */
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 4c15b2d8f..3cc19a520 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -21,7 +21,7 @@
#include "expr/node_value.h"
#include "theory/booleans/theory_bool_rewriter.h"
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -429,6 +429,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
return RewriteResponse(REWRITE_DONE, n);
}
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace booleans
+} // namespace theory
+} // namespace CVC5
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index 7af1abc0c..4caf5c681 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -22,7 +22,7 @@
#include "theory/theory_rewriter.h"
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -34,8 +34,8 @@ class TheoryBoolRewriter : public TheoryRewriter
}; /* class TheoryBoolRewriter */
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace booleans
+} // namespace theory
+} // namespace CVC5
#endif /* CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H */
diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index afb5ef92e..2f59a032e 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -19,7 +19,7 @@
#ifndef CVC4__THEORY_BOOL_TYPE_RULES_H
#define CVC4__THEORY_BOOL_TYPE_RULES_H
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace boolean {
@@ -70,8 +70,8 @@ public:
}
};/* class IteTypeRule */
-}/* CVC4::theory::boolean namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace boolean
+} // namespace theory
+} // namespace CVC5
#endif /* CVC4__THEORY_BOOL_TYPE_RULES_H */
diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index b2aeecae0..9b6619961 100644
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -23,7 +23,7 @@
#include "expr/type_node.h"
#include "expr/kind.h"
-namespace CVC4 {
+namespace CVC5 {
namespace theory {
namespace booleans {
@@ -63,8 +63,8 @@ class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> {
bool isFinished() override { return d_value == DONE; }
};/* class BooleanEnumerator */
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+} // namespace booleans
+} // namespace theory
+} // namespace CVC5
#endif /* CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback