diff options
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 56 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 6 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.h | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 8 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 8 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.cpp | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 8 | ||||
-rw-r--r-- | src/theory/builtin/type_enumerator.cpp | 8 | ||||
-rw-r--r-- | src/theory/builtin/type_enumerator.h | 8 |
11 files changed, 59 insertions, 59 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index cf68e060c..48ceaf103 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -196,7 +196,7 @@ # is with your type checker: # # cardinality MY_TYPE \ -# ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \ +# ::CVC5::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \ # "theory/foo/theory_foo_type_rules.h" # # well-founded K wellfoundedness-computer ground-term-computer [header] @@ -240,13 +240,13 @@ # commands. # -theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h" +theory THEORY_BUILTIN ::CVC5::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h" typechecker "theory/builtin/theory_builtin_type_rules.h" properties stable-infinite # Rewriter responsible for all the terms of the theory -rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h" +rewriter ::CVC5::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h" sort BUILTIN_OPERATOR_TYPE \ Cardinality::INTEGERS \ @@ -259,33 +259,33 @@ parameterized SORT_TYPE SORT_TAG 0: "specifies types of user-declared 'uninterpr # enough (for now) ? cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)" well-founded SORT_TYPE \ - "::CVC4::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" + "::CVC5::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \ + "::CVC5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" constant UNINTERPRETED_CONSTANT \ - ::CVC4::UninterpretedConstant \ - ::CVC4::UninterpretedConstantHashFunction \ + ::CVC5::UninterpretedConstant \ + ::CVC5::UninterpretedConstantHashFunction \ "expr/uninterpreted_constant.h" \ - "the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::UninterpretedConstant class (used in models)" -typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule + "the kind of expressions representing uninterpreted constants; payload is an instance of the CVC5::UninterpretedConstant class (used in models)" +typerule UNINTERPRETED_CONSTANT ::CVC5::theory::builtin::UninterpretedConstantTypeRule enumerator SORT_TYPE \ - ::CVC4::theory::builtin::UninterpretedSortEnumerator \ + ::CVC5::theory::builtin::UninterpretedSortEnumerator \ "theory/builtin/type_enumerator.h" constant ABSTRACT_VALUE \ - ::CVC4::AbstractValue \ - ::CVC4::AbstractValueHashFunction \ + ::CVC5::AbstractValue \ + ::CVC5::AbstractValueHashFunction \ "util/abstract_value.h" \ - "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the CVC4::AbstractValue class (used in models)" -typerule ABSTRACT_VALUE ::CVC4::theory::builtin::AbstractValueTypeRule + "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the CVC5::AbstractValue class (used in models)" +typerule ABSTRACT_VALUE ::CVC5::theory::builtin::AbstractValueTypeRule # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. constant BUILTIN \ - ::CVC4::Kind \ - ::CVC4::kind::KindHashFunction \ + ::CVC5::Kind \ + ::CVC5::kind::KindHashFunction \ "expr/kind.h" \ "the kind of expressions representing built-in operators" @@ -301,33 +301,33 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body" constant TYPE_CONSTANT \ - ::CVC4::TypeConstant \ - ::CVC4::TypeConstantHashFunction \ + ::CVC5::TypeConstant \ + ::CVC5::TypeConstantHashFunction \ "expr/kind.h" \ "a representation for basic types" operator FUNCTION_TYPE 2: "a function type" cardinality FUNCTION_TYPE \ - "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ + "::CVC5::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" well-founded FUNCTION_TYPE \ - "::CVC4::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \ - "::CVC4::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \ + "::CVC5::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \ + "::CVC5::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" enumerator FUNCTION_TYPE \ - ::CVC4::theory::builtin::FunctionEnumerator \ + ::CVC5::theory::builtin::FunctionEnumerator \ "theory/builtin/type_enumerator.h" sort SEXPR_TYPE \ Cardinality::INTEGERS \ not-well-founded \ "the type of a symbolic expression" -typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule -typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule -typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule -typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule -typerule WITNESS ::CVC4::theory::builtin::WitnessTypeRule +typerule EQUAL ::CVC5::theory::builtin::EqualityTypeRule +typerule DISTINCT ::CVC5::theory::builtin::DistinctTypeRule +typerule SEXPR ::CVC5::theory::builtin::SExprTypeRule +typerule LAMBDA ::CVC5::theory::builtin::LambdaTypeRule +typerule WITNESS ::CVC5::theory::builtin::WitnessTypeRule # lambda expressions that are isomorphic to array constants can be considered constants -construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +construle LAMBDA ::CVC5::theory::builtin::LambdaTypeRule endtheory diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 3e0eca128..62f0f1b9a 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -20,9 +20,9 @@ #include "theory/rewriter.h" #include "theory/theory.h" -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { const char* toString(MethodId id) @@ -497,4 +497,4 @@ Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid) } // namespace builtin } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 77cb2593a..ed68f1215 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -22,7 +22,7 @@ #include "expr/proof_node.h" #include "theory/quantifiers/extended_rewrite.h" -namespace CVC4 { +namespace CVC5 { namespace theory { /** @@ -179,6 +179,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker } // namespace builtin } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */ diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 13162960c..83e9d3fed 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -24,7 +24,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace builtin { @@ -62,4 +62,4 @@ void TheoryBuiltin::finishInit() } // namespace builtin } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 94a00b7e3..449282ae6 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -23,7 +23,7 @@ #include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace builtin { @@ -53,6 +53,6 @@ class TheoryBuiltin : public Theory } // namespace builtin } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */ diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 16e454e04..16fc59a5a 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -23,7 +23,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace builtin { @@ -502,6 +502,6 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda(TNode n) return Rewriter::rewrite(anode); } -}/* CVC4::theory::builtin namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace builtin +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index bf84d543b..c419abdb3 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -22,7 +22,7 @@ #include "theory/theory_rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace builtin { @@ -117,8 +117,8 @@ class TheoryBuiltinRewriter : public TheoryRewriter static Node getArrayRepresentationForLambda(TNode n); }; /* class TheoryBuiltinRewriter */ -}/* CVC4::theory::builtin namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace builtin +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index 3abdbd48f..d5a5c9ab7 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -18,7 +18,7 @@ #include "expr/attribute.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace builtin { @@ -47,4 +47,4 @@ Node SortProperties::mkGroundTerm(TypeNode type) } // namespace builtin } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index e0c68aa0f..815483507 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -25,7 +25,7 @@ #include <sstream> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace builtin { @@ -246,8 +246,8 @@ class FunctionProperties { } };/* class FuctionProperties */ -}/* CVC4::theory::builtin namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace builtin +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */ diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp index 6f7082191..4dda11070 100644 --- a/src/theory/builtin/type_enumerator.cpp +++ b/src/theory/builtin/type_enumerator.cpp @@ -18,7 +18,7 @@ #include "theory/builtin/theory_builtin_rewriter.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace builtin { @@ -47,6 +47,6 @@ FunctionEnumerator& FunctionEnumerator::operator++() return *this; } -} /* CVC4::theory::builtin namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace builtin +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 7b4b09f84..50cd50dda 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -25,7 +25,7 @@ #include "theory/type_enumerator.h" #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { namespace theory { namespace builtin { @@ -104,8 +104,8 @@ class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator> Node d_bvl; }; /* class FunctionEnumerator */ -}/* CVC4::theory::builtin namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace builtin +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */ |