diff options
Diffstat (limited to 'src/theory/sets')
26 files changed, 94 insertions, 94 deletions
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 84e7786e8..b67df285d 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -25,9 +25,9 @@ #include "theory/valuation.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -1114,4 +1114,4 @@ const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers( } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index 47fa18d5b..c354f3f3a 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -25,7 +25,7 @@ #include "theory/type_set.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -412,6 +412,6 @@ class CardinalityExtension } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 305059797..2523512cc 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -18,9 +18,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -177,4 +177,4 @@ void InferenceManager::split(Node n, InferenceId id, int reqPol) } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index 8e4614718..90d2ce12a 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -20,7 +20,7 @@ #include "theory/inference_manager_buffered.h" #include "theory/sets/solver_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -100,6 +100,6 @@ class InferenceManager : public InferenceManagerBuffered } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */ diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 4ef22d68c..564779f6a 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -5,10 +5,10 @@ # theory THEORY_SETS \ - ::CVC5::theory::sets::TheorySets \ + ::cvc5::theory::sets::TheorySets \ "theory/sets/theory_sets.h" typechecker "theory/sets/theory_sets_type_rules.h" -rewriter ::CVC5::theory::sets::TheorySetsRewriter \ +rewriter ::cvc5::theory::sets::TheorySetsRewriter \ "theory/sets/theory_sets_rewriter.h" properties parametric @@ -16,22 +16,22 @@ properties check presolve # constants constant EMPTYSET \ - ::CVC5::EmptySet \ - ::CVC5::EmptySetHashFunction \ + ::cvc5::EmptySet \ + ::cvc5::EmptySetHashFunction \ "expr/emptyset.h" \ - "the empty set constant; payload is an instance of the CVC5::EmptySet class" + "the empty set constant; payload is an instance of the cvc5::EmptySet class" # the type operator SET_TYPE 1 "set type, takes as parameter the type of the elements" cardinality SET_TYPE \ - "::CVC5::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \ + "::cvc5::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \ "theory/sets/theory_sets_type_rules.h" well-founded SET_TYPE \ - "::CVC5::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \ - "::CVC5::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \ + "::cvc5::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \ + "::cvc5::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \ "theory/sets/theory_sets_type_rules.h" enumerator SET_TYPE \ - "::CVC5::theory::sets::SetEnumerator" \ + "::cvc5::theory::sets::SetEnumerator" \ "theory/sets/theory_sets_type_enumerator.h" # operators @@ -42,10 +42,10 @@ operator SUBSET 2 "subset predicate; first parameter a subset of second operator MEMBER 2 "set membership predicate; first parameter a member of second" constant SINGLETON_OP \ - ::CVC5::SingletonOp \ - ::CVC5::SingletonOpHashFunction \ + ::cvc5::SingletonOp \ + ::cvc5::SingletonOpHashFunction \ "theory/sets/singleton_op.h" \ - "operator for singletons; payload is an instance of the CVC5::SingletonOp class" + "operator for singletons; payload is an instance of the cvc5::SingletonOp class" parameterized SINGLETON SINGLETON_OP 1 \ "constructs a set of a single element. First parameter is a SingletonOp. Second is a term" @@ -85,30 +85,30 @@ operator TCLOSURE 1 "set transitive closure" operator JOIN_IMAGE 2 "set join image" operator IDEN 1 "set identity" -typerule UNION ::CVC5::theory::sets::SetsBinaryOperatorTypeRule -typerule INTERSECTION ::CVC5::theory::sets::SetsBinaryOperatorTypeRule -typerule SETMINUS ::CVC5::theory::sets::SetsBinaryOperatorTypeRule -typerule SUBSET ::CVC5::theory::sets::SubsetTypeRule -typerule MEMBER ::CVC5::theory::sets::MemberTypeRule +typerule UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule +typerule INTERSECTION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule +typerule SETMINUS ::cvc5::theory::sets::SetsBinaryOperatorTypeRule +typerule SUBSET ::cvc5::theory::sets::SubsetTypeRule +typerule MEMBER ::cvc5::theory::sets::MemberTypeRule typerule SINGLETON_OP "SimpleTypeRule<RBuiltinOperator>" -typerule SINGLETON ::CVC5::theory::sets::SingletonTypeRule -typerule EMPTYSET ::CVC5::theory::sets::EmptySetTypeRule -typerule INSERT ::CVC5::theory::sets::InsertTypeRule -typerule CARD ::CVC5::theory::sets::CardTypeRule -typerule COMPLEMENT ::CVC5::theory::sets::ComplementTypeRule -typerule UNIVERSE_SET ::CVC5::theory::sets::UniverseSetTypeRule -typerule COMPREHENSION ::CVC5::theory::sets::ComprehensionTypeRule -typerule CHOOSE ::CVC5::theory::sets::ChooseTypeRule -typerule IS_SINGLETON ::CVC5::theory::sets::IsSingletonTypeRule +typerule SINGLETON ::cvc5::theory::sets::SingletonTypeRule +typerule EMPTYSET ::cvc5::theory::sets::EmptySetTypeRule +typerule INSERT ::cvc5::theory::sets::InsertTypeRule +typerule CARD ::cvc5::theory::sets::CardTypeRule +typerule COMPLEMENT ::cvc5::theory::sets::ComplementTypeRule +typerule UNIVERSE_SET ::cvc5::theory::sets::UniverseSetTypeRule +typerule COMPREHENSION ::cvc5::theory::sets::ComprehensionTypeRule +typerule CHOOSE ::cvc5::theory::sets::ChooseTypeRule +typerule IS_SINGLETON ::cvc5::theory::sets::IsSingletonTypeRule -typerule JOIN ::CVC5::theory::sets::RelBinaryOperatorTypeRule -typerule PRODUCT ::CVC5::theory::sets::RelBinaryOperatorTypeRule -typerule TRANSPOSE ::CVC5::theory::sets::RelTransposeTypeRule -typerule TCLOSURE ::CVC5::theory::sets::RelTransClosureTypeRule -typerule JOIN_IMAGE ::CVC5::theory::sets::JoinImageTypeRule -typerule IDEN ::CVC5::theory::sets::RelIdenTypeRule +typerule JOIN ::cvc5::theory::sets::RelBinaryOperatorTypeRule +typerule PRODUCT ::cvc5::theory::sets::RelBinaryOperatorTypeRule +typerule TRANSPOSE ::cvc5::theory::sets::RelTransposeTypeRule +typerule TCLOSURE ::cvc5::theory::sets::RelTransClosureTypeRule +typerule JOIN_IMAGE ::cvc5::theory::sets::JoinImageTypeRule +typerule IDEN ::cvc5::theory::sets::RelIdenTypeRule -construle UNION ::CVC5::theory::sets::SetsBinaryOperatorTypeRule -construle SINGLETON ::CVC5::theory::sets::SingletonTypeRule +construle UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule +construle SINGLETON ::cvc5::theory::sets::SingletonTypeRule endtheory diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 197f31903..c0f02da7d 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -19,7 +19,7 @@ #ifndef CVC4__THEORY__SETS__NORMAL_FORM_H #define CVC4__THEORY__SETS__NORMAL_FORM_H -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -158,6 +158,6 @@ class NormalForm { }; } } -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index eb3477f5a..545e3c08c 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -21,7 +21,7 @@ #include "expr/dtype_cons.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -98,6 +98,6 @@ public: }; } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp index 4e76d35e4..0fc411788 100644 --- a/src/theory/sets/singleton_op.cpp +++ b/src/theory/sets/singleton_op.cpp @@ -18,7 +18,7 @@ #include "expr/type_node.h" -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& out, const SingletonOp& op) { @@ -47,4 +47,4 @@ bool SingletonOp::operator==(const SingletonOp& op) const return getType() == op.getType(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h index d17f8255e..7e338e518 100644 --- a/src/theory/sets/singleton_op.h +++ b/src/theory/sets/singleton_op.h @@ -19,7 +19,7 @@ #include <memory> -namespace CVC5 { +namespace cvc5 { class TypeNode; @@ -58,6 +58,6 @@ struct SingletonOpHashFunction size_t operator()(const SingletonOp& op) const; }; /* struct SingletonOpHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SINGLETON_OP_H */ diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp index 3c0f33caf..c18e9406d 100644 --- a/src/theory/sets/skolem_cache.cpp +++ b/src/theory/sets/skolem_cache.cpp @@ -16,9 +16,9 @@ #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -61,4 +61,4 @@ bool SkolemCache::isSkolem(Node n) const } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h index 42369c7a9..17e4bda71 100644 --- a/src/theory/sets/skolem_cache.h +++ b/src/theory/sets/skolem_cache.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -78,6 +78,6 @@ class SkolemCache } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index ff604f838..31f0d4aa3 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -19,9 +19,9 @@ #include "theory/sets/theory_sets_private.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -595,4 +595,4 @@ bool SolverState::merge(TNode t1, } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 431aa019d..cbbb53d88 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -24,7 +24,7 @@ #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -268,6 +268,6 @@ class SolverState : public TheoryState } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H */ diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index 6dc18591c..a093840f7 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -17,9 +17,9 @@ #include "expr/emptyset.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -151,4 +151,4 @@ void TermRegistry::debugPrintSet(Node s, const char* c) const } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index 913473ff0..3d1035c75 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -25,7 +25,7 @@ #include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -89,6 +89,6 @@ class TermRegistry } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__SETS__TERM_REGISTRY_H */ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 1530da809..bd682ca57 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -22,9 +22,9 @@ #include "theory/theory_model.h" #include "theory/trust_substitutions.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -238,4 +238,4 @@ void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 4dc5d8a0d..16829bc6d 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -29,7 +29,7 @@ #include "theory/theory_eq_notify.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -120,6 +120,6 @@ class TheorySets : public Theory } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__SETS__THEORY_SETS_H */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 285eac473..8d005c6fe 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -29,9 +29,9 @@ #include "util/result.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -1372,4 +1372,4 @@ void TheorySetsPrivate::presolve() { d_state.reset(); } } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index a822d06e7..c2f266971 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -31,7 +31,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -236,6 +236,6 @@ class TheorySetsPrivate { } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */ diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index a160e0afd..6609e4923 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -19,9 +19,9 @@ #include "theory/sets/theory_sets.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -1333,4 +1333,4 @@ void TheorySetsRels::check(Theory::Effort level) } } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 93913d4f5..badf14bd0 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -28,7 +28,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -185,6 +185,6 @@ private: } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* SRC_THEORY_SETS_THEORY_SETS_RELS_H_ */ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 935eb548d..9007cc250 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -22,9 +22,9 @@ #include "theory/sets/normal_form.h" #include "theory/sets/rels_utils.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -542,4 +542,4 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index 739a5f885..501a58430 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -21,7 +21,7 @@ #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -79,6 +79,6 @@ private: } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */ diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp index 30e279be7..87fcd2d8f 100644 --- a/src/theory/sets/theory_sets_type_enumerator.cpp +++ b/src/theory/sets/theory_sets_type_enumerator.cpp @@ -16,7 +16,7 @@ #include "theory/sets/theory_sets_type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -130,4 +130,4 @@ bool SetEnumerator::isFinished() } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 32aca5f79..006afc964 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -26,7 +26,7 @@ #include "theory/sets/normal_form.h" #include "theory/type_enumerator.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -68,6 +68,6 @@ class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 54791ac31..ab82ba710 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -23,7 +23,7 @@ #include "theory/sets/normal_form.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace sets { @@ -390,7 +390,7 @@ struct JoinImageTypeRule { throw TypeCheckingExceptionPrivate( n, " JoinImage cardinality constraint must be a constant"); } - CVC5::Rational r(INT_MAX); + cvc5::Rational r(INT_MAX); if (n[1].getConst<Rational>() > r) { throw TypeCheckingExceptionPrivate( n, " JoinImage Exceeded INT_MAX in cardinality constraint"); @@ -444,6 +444,6 @@ struct SetsProperties { } // namespace sets } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */ |