diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/theory/booleans | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/theory/booleans')
-rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 4 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 4 | ||||
-rw-r--r-- | src/theory/booleans/kinds | 22 | ||||
-rw-r--r-- | src/theory/booleans/proof_checker.cpp | 4 | ||||
-rw-r--r-- | src/theory/booleans/proof_checker.h | 4 | ||||
-rw-r--r-- | src/theory/booleans/proof_circuit_propagator.cpp | 4 | ||||
-rw-r--r-- | src/theory/booleans/proof_circuit_propagator.h | 4 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.cpp | 8 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 8 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 8 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.h | 8 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_type_rules.h | 8 | ||||
-rw-r--r-- | src/theory/booleans/type_enumerator.h | 8 |
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 */ |