diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:56:14 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-01 16:56:14 +0000 |
| commit | 05a53a2ac405bcd18a84024247145f161809c3b0 (patch) | |
| tree | 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/theory/arith | |
| parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) | |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/theory/arith')
152 files changed, 404 insertions, 404 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index c911d03e9..8e75f6850 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -36,7 +36,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -369,7 +369,7 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 /* Begin the declaration of GLPK specific code. */ #ifdef CVC4_USE_GLPK @@ -377,7 +377,7 @@ extern "C" { #include <glpk.h> }/* extern "C" */ -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -537,12 +537,12 @@ int ApproxGLPK::s_verbosity = 0; } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /*#ifdef CVC4_USE_GLPK */ /* End the declaration of GLPK specific code. */ /* Begin GPLK/NOGLPK Glue code. */ -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { ApproximateSimplex* ApproximateSimplex::mkApproximateSimplexSolver(const ArithVariables& vars, TreeLog& l, ApproximateStatistics& s){ @@ -561,12 +561,12 @@ bool ApproximateSimplex::enabled() { } } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 /* End GPLK/NOGLPK Glue code. */ /* Begin GPLK implementation. */ #ifdef CVC4_USE_GLPK -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -3176,6 +3176,6 @@ void ApproxGLPK::tryCut(int nid, CutInfo& cut) } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /*#ifdef CVC4_USE_GLPK */ /* End GPLK implementation. */ diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 5835c57c1..787effc94 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -28,7 +28,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -165,4 +165,4 @@ class ApproximateSimplex{ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 42189f86a..4c991dba3 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -30,7 +30,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -47,7 +47,7 @@ Node ArithIteUtils::applyReduceVariablesInItes(Node n){ } Node ArithIteUtils::reduceVariablesInItes(Node n){ - using namespace CVC5::kind; + using namespace cvc5::kind; if(d_reduceVar.find(n) != d_reduceVar.end()){ Node res = d_reduceVar[n]; return res.isNull() ? n : res; @@ -457,4 +457,4 @@ bool ArithIteUtils::solveBinOr(TNode binor){ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 263ddda8e..3e548f42d 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -28,7 +28,7 @@ #include "context/cdo.h" #include "context/cdinsert_hashmap.h" -namespace CVC5 { +namespace cvc5 { namespace preprocessing { namespace util { class ContainsTermITEVisitor; @@ -111,6 +111,6 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */ diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index 9190dac7d..a2ae138fd 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -16,9 +16,9 @@ #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { bool ArithMSum::getMonomial(Node n, Node& c, Node& v) @@ -322,4 +322,4 @@ void ArithMSum::debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c) } } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h index f4a2bf824..7854e0d3b 100644 --- a/src/theory/arith/arith_msum.h +++ b/src/theory/arith/arith_msum.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { /** Arithmetic utilities regarding monomial sums. @@ -183,6 +183,6 @@ class ArithMSum }; } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__MSUM_H */ diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 2b120c9c7..e57b6c57f 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -18,7 +18,7 @@ #include "theory/arith/inference_manager.h" #include "theory/skolem_lemma.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -80,4 +80,4 @@ bool ArithPreprocess::isReduced(TNode atom) const } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index 45ce0c597..663c09abe 100644 --- a/src/theory/arith/arith_preprocess.h +++ b/src/theory/arith/arith_preprocess.h @@ -21,7 +21,7 @@ #include "theory/arith/operator_elim.h" #include "theory/logic_info.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class SkolemLemma; @@ -86,6 +86,6 @@ class ArithPreprocess } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 01e88b1a8..87aba7b45 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -28,7 +28,7 @@ #include "theory/theory.h" #include "util/iand.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -228,7 +228,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ if(exp.sgn() == 0){ return RewriteResponse(REWRITE_DONE, mkRationalNode(Rational(1))); }else if(exp.sgn() > 0 && exp.isIntegral()){ - CVC5::Rational r(expr::NodeValue::MAX_CHILDREN); + cvc5::Rational r(expr::NodeValue::MAX_CHILDREN); if (exp <= r) { unsigned num = exp.getNumerator().toUnsignedInt(); @@ -901,4 +901,4 @@ RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r) } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 556a7bda7..803f8c8a8 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -23,7 +23,7 @@ #include "theory/arith/rewrites.h" #include "theory/theory_rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -73,6 +73,6 @@ class ArithRewriter : public TheoryRewriter } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__ARITH_REWRITER_H */ diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp index bab1d6eb9..f4be43b06 100644 --- a/src/theory/arith/arith_state.cpp +++ b/src/theory/arith/arith_state.cpp @@ -16,7 +16,7 @@ #include "theory/arith/theory_arith_private.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -35,4 +35,4 @@ bool ArithState::isInConflict() const } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h index dfe2bc877..05b09a5a2 100644 --- a/src/theory/arith/arith_state.h +++ b/src/theory/arith/arith_state.h @@ -19,7 +19,7 @@ #include "theory/theory_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -52,6 +52,6 @@ class ArithState : public TheoryState } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index b0129970e..9c764ac7a 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -27,9 +27,9 @@ #include "theory/rewriter.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -273,4 +273,4 @@ void ArithStaticLearner::addBound(TNode n) { } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 668527c0f..73810dedd 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -25,7 +25,7 @@ #include "theory/arith/delta_rational.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace context { class Context; } @@ -71,6 +71,6 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */ diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 16c412546..abffcc3d3 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -16,9 +16,9 @@ #include <cmath> -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -325,4 +325,4 @@ Node negateProofLiteral(TNode n) } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 9c0edb893..852550917 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -28,7 +28,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -344,6 +344,6 @@ Node negateProofLiteral(TNode n); } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__ARITH_UTILITIES_H */ diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp index a0c29cb84..b2db30f82 100644 --- a/src/theory/arith/arithvar.cpp +++ b/src/theory/arith/arithvar.cpp @@ -19,7 +19,7 @@ #include <limits> #include <set> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -32,4 +32,4 @@ bool debugIsASet(const std::vector<ArithVar>& variables){ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index a49797845..959db4b0d 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -26,7 +26,7 @@ #include "util/index.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -41,4 +41,4 @@ extern bool debugIsASet(const ArithVarVec& variables); } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index dceeeb407..6764e8e0b 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -27,7 +27,7 @@ #include "context/cdhashmap.h" #include "context/cdo.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -90,6 +90,6 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */ diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 292fccb34..d0f69b7a3 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -153,4 +153,4 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index faca0cb25..411bf776e 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -58,7 +58,7 @@ #include "theory/arith/approx_simplex.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -92,4 +92,4 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 949828aeb..9caa965ac 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -22,7 +22,7 @@ #include "theory/arith/arithvar.h" #include "util/dense_map.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -231,4 +231,4 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp index 126954144..a3357c1d9 100644 --- a/src/theory/arith/bound_inference.cpp +++ b/src/theory/arith/bound_inference.cpp @@ -17,7 +17,7 @@ #include "theory/arith/normal_form.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -247,4 +247,4 @@ std::map<Node, std::pair<Node,Node>> getBounds(const std::vector<Node>& assertio } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/bound_inference.h b/src/theory/arith/bound_inference.h index 7041777d8..fc5e68cff 100644 --- a/src/theory/arith/bound_inference.h +++ b/src/theory/arith/bound_inference.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -113,6 +113,6 @@ std::map<Node, std::pair<Node,Node>> getBounds(const std::vector<Node>& assertio } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif
\ No newline at end of file diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 7fe8e4934..b2c48163f 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -21,7 +21,7 @@ #include "theory/arith/proof_macros.h" #include "theory/arith/theory_arith_private.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -196,4 +196,4 @@ BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const { } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 66004871b..539b7f70d 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -24,7 +24,7 @@ #include "theory/inference_id.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { class ProofNode; @@ -199,4 +199,4 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index f2e51be02..ea597468d 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -30,7 +30,7 @@ #include "theory/uf/proof_equality_engine.h" #include "options/arith_options.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -691,4 +691,4 @@ std::vector<Node> andComponents(TNode an) } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 540e985f7..055d5ddbb 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -32,7 +32,7 @@ #include "util/dense_map.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; @@ -299,4 +299,4 @@ std::vector<Node> andComponents(TNode an); } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index cc1129f50..baa9b1ebb 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -32,9 +32,9 @@ using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -2428,4 +2428,4 @@ std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca, ConstraintCP c } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 3caa5a030..d00f16c90 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -93,7 +93,7 @@ #include "theory/trust_node.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; @@ -1277,6 +1277,6 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__CONSTRAINT_H */ diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h index 8d36df304..146ffd607 100644 --- a/src/theory/arith/constraint_forward.h +++ b/src/theory/arith/constraint_forward.h @@ -24,7 +24,7 @@ #include "cvc4_private.h" #include <vector> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -46,6 +46,6 @@ static const RationalVectorP RationalVectorPSentinel = NULL; } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */ diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp index 36c8d06f1..faf2fddbe 100644 --- a/src/theory/arith/cut_log.cpp +++ b/src/theory/arith/cut_log.cpp @@ -31,7 +31,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -704,4 +704,4 @@ void DenseVector::print(ostream& out, const DenseMap<Rational>& v){ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 961092f6e..3ab0bb6bf 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -28,7 +28,7 @@ #include "theory/arith/constraint_forward.h" #include "util/dense_map.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -290,4 +290,4 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index 7d20a1859..e93b0315e 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -21,7 +21,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& os, const DeltaRational& dq){ return os << "(" << dq.getNoninfinitesimalPart() @@ -106,4 +106,4 @@ Integer DeltaRational::euclidianDivideRemainder(const DeltaRational& y) const } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index e2b769b18..cd01f9c1a 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -26,7 +26,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { class DeltaRational; @@ -46,20 +46,20 @@ class DeltaRationalException : public Exception { */ class DeltaRational { private: - CVC5::Rational c; - CVC5::Rational k; + cvc5::Rational c; + cvc5::Rational k; public: DeltaRational() : c(0,1), k(0,1) {} - DeltaRational(const CVC5::Rational& base) : c(base), k(0, 1) {} - DeltaRational(const CVC5::Rational& base, const CVC5::Rational& coeff) + DeltaRational(const cvc5::Rational& base) : c(base), k(0, 1) {} + DeltaRational(const cvc5::Rational& base, const cvc5::Rational& coeff) : c(base), k(coeff) { } - const CVC5::Rational& getInfinitesimalPart() const { return k; } + const cvc5::Rational& getInfinitesimalPart() const { return k; } - const CVC5::Rational& getNoninfinitesimalPart() const { return c; } + const cvc5::Rational& getNoninfinitesimalPart() const { return c; } int sgn() const { int s = getNoninfinitesimalPart().sgn(); @@ -97,14 +97,14 @@ public: } DeltaRational operator+(const DeltaRational& other) const{ - CVC5::Rational tmpC = c + other.c; - CVC5::Rational tmpK = k + other.k; + cvc5::Rational tmpC = c + other.c; + cvc5::Rational tmpK = k + other.k; return DeltaRational(tmpC, tmpK); } DeltaRational operator*(const Rational& a) const{ - CVC5::Rational tmpC = a * c; - CVC5::Rational tmpK = a * k; + cvc5::Rational tmpC = a * c; + cvc5::Rational tmpK = a * k; return DeltaRational(tmpC, tmpK); } @@ -127,7 +127,7 @@ public: DeltaRational operator-(const DeltaRational& a) const{ - CVC5::Rational negOne(CVC5::Integer(-1)); + cvc5::Rational negOne(cvc5::Integer(-1)); return *(this) + (a * negOne); } @@ -136,14 +136,14 @@ public: } DeltaRational operator/(const Rational& a) const{ - CVC5::Rational tmpC = c / a; - CVC5::Rational tmpK = k / a; + cvc5::Rational tmpC = c / a; + cvc5::Rational tmpK = k / a; return DeltaRational(tmpC, tmpK); } DeltaRational operator/(const Integer& a) const{ - CVC5::Rational tmpC = c / a; - CVC5::Rational tmpK = k / a; + cvc5::Rational tmpC = c / a; + cvc5::Rational tmpK = k / a; return DeltaRational(tmpC, tmpK); } @@ -204,7 +204,7 @@ public: return *(this); } - DeltaRational& operator*=(const CVC5::Rational& a) + DeltaRational& operator*=(const cvc5::Rational& a) { c *= a; k *= a; @@ -299,4 +299,4 @@ public: std::ostream& operator<<(std::ostream& os, const DeltaRational& n); -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 51dd69650..6e069cdf6 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -24,7 +24,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -835,4 +835,4 @@ Node DioSolver::trailIndexToEquality(TrailIndex i) const { } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 7892bec52..9b3106036 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -33,7 +33,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC5 { +namespace cvc5 { namespace context { class Context; } @@ -423,6 +423,6 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__DIO_SOLVER_H */ diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index d4e26600d..52dd20779 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -275,4 +275,4 @@ bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingI } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index 3e1bc0ee7..a0a727a0a 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -57,7 +57,7 @@ #include "theory/arith/simplex.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -113,4 +113,4 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index 142a060ec..b8c20104b 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -22,7 +22,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -479,4 +479,4 @@ void ErrorSet::pushFocusInto(ArithVarVec& vec) const{ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index cdf155c6d..4788d2697 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -31,7 +31,7 @@ #include "util/bin_heap.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -414,4 +414,4 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 61280d651..9d7711361 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -25,7 +25,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -861,4 +861,4 @@ const Rational& FCSimplexDecisionProcedure::focusCoefficient(ArithVar nb) const } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 73e5ae54f..2b303ffa2 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -61,7 +61,7 @@ #include "util/dense_map.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -256,4 +256,4 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp index 25494bdee..a8b6374cc 100644 --- a/src/theory/arith/infer_bounds.cpp +++ b/src/theory/arith/infer_bounds.cpp @@ -18,7 +18,7 @@ #include "theory/arith/infer_bounds.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -264,4 +264,4 @@ std::ostream& operator<<(std::ostream& os, const Algorithms a){ } /* namespace arith */ } /* namespace theory */ -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h index 251c7cbb8..27bc611b3 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/infer_bounds.h @@ -27,7 +27,7 @@ #include "util/maybe.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -160,4 +160,4 @@ private: } /* namespace arith */ } /* namespace theory */ -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 66b628302..732111f97 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -19,7 +19,7 @@ #include "theory/arith/theory_arith.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -147,4 +147,4 @@ bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem) } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index bf5ed7b10..a5b200f8b 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -22,7 +22,7 @@ #include "theory/inference_id.h" #include "theory/inference_manager_buffered.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -117,6 +117,6 @@ class InferenceManager : public InferenceManagerBuffered } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index b839ccc22..f9f88cddf 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -4,13 +4,13 @@ # src/theory/builtin/kinds. # -theory THEORY_ARITH ::CVC5::theory::arith::TheoryArith "theory/arith/theory_arith.h" +theory THEORY_ARITH ::cvc5::theory::arith::TheoryArith "theory/arith/theory_arith.h" typechecker "theory/arith/theory_arith_type_rules.h" properties stable-infinite properties check propagate ppStaticLearn presolve notifyRestart -rewriter ::CVC5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" +rewriter ::cvc5::theory::arith::ArithRewriter "theory/arith/arith_rewriter.h" operator PLUS 2: "arithmetic addition (N-ary)" operator MULT 2: "arithmetic multiplication (N-ary)" @@ -44,10 +44,10 @@ operator ARCCOTANGENT 1 "arc cotangent" operator SQRT 1 "square root" constant DIVISIBLE_OP \ - ::CVC5::Divisible \ - ::CVC5::DivisibleHashFunction \ + ::cvc5::Divisible \ + ::cvc5::DivisibleHashFunction \ "util/divisible.h" \ - "operator for the divisibility-by-k predicate; payload is an instance of the CVC5::Divisible class" + "operator for the divisibility-by-k predicate; payload is an instance of the cvc5::Divisible class" sort REAL_TYPE \ Cardinality::REALS \ @@ -63,16 +63,16 @@ sort INTEGER_TYPE \ "integer type" constant CONST_RATIONAL \ - ::CVC5::Rational \ - ::CVC5::RationalHashFunction \ + ::cvc5::Rational \ + ::cvc5::RationalHashFunction \ "util/rational.h" \ - "a multiple-precision rational constant; payload is an instance of the CVC5::Rational class" + "a multiple-precision rational constant; payload is an instance of the cvc5::Rational class" enumerator REAL_TYPE \ - "::CVC5::theory::arith::RationalEnumerator" \ + "::cvc5::theory::arith::RationalEnumerator" \ "theory/arith/type_enumerator.h" enumerator INTEGER_TYPE \ - "::CVC5::theory::arith::IntegerEnumerator" \ + "::cvc5::theory::arith::IntegerEnumerator" \ "theory/arith/type_enumerator.h" operator LT 2 "less than, x < y" @@ -82,10 +82,10 @@ operator GEQ 2 "greater than or equal, x >= y" # represents an indexed root predicate. See util/indexed_root_predicate.h for more documentation. constant INDEXED_ROOT_PREDICATE_OP \ - ::CVC5::IndexedRootPredicate \ - ::CVC5::IndexedRootPredicateHashFunction \ + ::cvc5::IndexedRootPredicate \ + ::cvc5::IndexedRootPredicateHashFunction \ "util/indexed_root_predicate.h" \ - "operator for the indexed root predicate; payload is an instance of the CVC5::IndexedRootPredicate class" + "operator for the indexed root predicate; payload is an instance of the cvc5::IndexedRootPredicate class" parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial" operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" @@ -99,15 +99,15 @@ operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this # This way, we avoid having 2 nested TO_REAL nodess as a result of Solver::mkTerm(TO_REAL, Solver::mkReal(int val)) operator CAST_TO_REAL 1 "cast term to real same as TO_REAL, but it is used internally, whereas TO_REAL is accessible in the API" -typerule PLUS ::CVC5::theory::arith::ArithOperatorTypeRule -typerule MULT ::CVC5::theory::arith::ArithOperatorTypeRule -typerule NONLINEAR_MULT ::CVC5::theory::arith::ArithOperatorTypeRule -typerule MINUS ::CVC5::theory::arith::ArithOperatorTypeRule -typerule UMINUS ::CVC5::theory::arith::ArithOperatorTypeRule -typerule DIVISION ::CVC5::theory::arith::ArithOperatorTypeRule -typerule POW ::CVC5::theory::arith::ArithOperatorTypeRule +typerule PLUS ::cvc5::theory::arith::ArithOperatorTypeRule +typerule MULT ::cvc5::theory::arith::ArithOperatorTypeRule +typerule NONLINEAR_MULT ::cvc5::theory::arith::ArithOperatorTypeRule +typerule MINUS ::cvc5::theory::arith::ArithOperatorTypeRule +typerule UMINUS ::cvc5::theory::arith::ArithOperatorTypeRule +typerule DIVISION ::cvc5::theory::arith::ArithOperatorTypeRule +typerule POW ::cvc5::theory::arith::ArithOperatorTypeRule -typerule CONST_RATIONAL ::CVC5::theory::arith::ArithConstantTypeRule +typerule CONST_RATIONAL ::cvc5::theory::arith::ArithConstantTypeRule typerule LT "SimpleTypeRule<RBool, AReal, AReal>" typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>" @@ -115,11 +115,11 @@ typerule GT "SimpleTypeRule<RBool, AReal, AReal>" typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>" typerule INDEXED_ROOT_PREDICATE_OP "SimpleTypeRule<RBuiltinOperator>" -typerule INDEXED_ROOT_PREDICATE ::CVC5::theory::arith::IndexedRootPredicateTypeRule +typerule INDEXED_ROOT_PREDICATE ::cvc5::theory::arith::IndexedRootPredicateTypeRule -typerule TO_REAL ::CVC5::theory::arith::ArithOperatorTypeRule -typerule CAST_TO_REAL ::CVC5::theory::arith::ArithOperatorTypeRule -typerule TO_INTEGER ::CVC5::theory::arith::ArithOperatorTypeRule +typerule TO_REAL ::cvc5::theory::arith::ArithOperatorTypeRule +typerule CAST_TO_REAL ::cvc5::theory::arith::ArithOperatorTypeRule +typerule TO_INTEGER ::cvc5::theory::arith::ArithOperatorTypeRule typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>" typerule ABS "SimpleTypeRule<RInteger, AInteger>" @@ -128,7 +128,7 @@ typerule INTS_MODULUS "SimpleTypeRule<RInteger, AInteger, AInteger>" typerule DIVISIBLE "SimpleTypeRule<RBool, AInteger>" typerule DIVISIBLE_OP "SimpleTypeRule<RBuiltinOperator>" -typerule DIVISION_TOTAL ::CVC5::theory::arith::ArithOperatorTypeRule +typerule DIVISION_TOTAL ::cvc5::theory::arith::ArithOperatorTypeRule typerule INTS_DIVISION_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>" typerule INTS_MODULUS_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>" @@ -150,20 +150,20 @@ typerule SQRT "SimpleTypeRule<RReal, AReal>" nullaryoperator PI "pi" -typerule PI ::CVC5::theory::arith::RealNullaryOperatorTypeRule +typerule PI ::cvc5::theory::arith::RealNullaryOperatorTypeRule # Integer AND, which is parameterized by a (positive) bitwidth k. # ((_ iand k) i1 i2) is equivalent to: # (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2))) # for all integers i1, i2. constant IAND_OP \ - ::CVC5::IntAnd \ - "::CVC5::UnsignedHashFunction< ::CVC5::IntAnd >" \ + ::cvc5::IntAnd \ + "::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >" \ "util/iand.h" \ - "operator for integer AND; payload is an instance of the CVC5::IntAnd class" + "operator for integer AND; payload is an instance of the cvc5::IntAnd class" parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms" -typerule IAND_OP ::CVC5::theory::arith::IAndOpTypeRule -typerule IAND ::CVC5::theory::arith::IAndTypeRule +typerule IAND_OP ::cvc5::theory::arith::IAndOpTypeRule +typerule IAND ::cvc5::theory::arith::IAndTypeRule endtheory diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 28f386e2a..95c833707 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -22,7 +22,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -1413,4 +1413,4 @@ void LinearEqualityModule::directlyAddToCoefficient(ArithVar row, ArithVar col, } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 4a923b677..4f50853c9 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -40,7 +40,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -758,4 +758,4 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp index dd7f28228..f2ecc8e4c 100644 --- a/src/theory/arith/matrix.cpp +++ b/src/theory/arith/matrix.cpp @@ -18,7 +18,7 @@ #include "theory/arith/matrix.h" using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -28,4 +28,4 @@ bool NoEffectCCCB::canUseRow(RowIndex ridx) const { return false; } } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 553cef7d4..855f56d1f 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -28,7 +28,7 @@ #include "util/dense_map.h" #include "util/index.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -368,8 +368,8 @@ public: typedef MatrixEntry<T> Entry; protected: - typedef CVC5::theory::arith::RowVector<T> RowVectorT; - typedef CVC5::theory::arith::ColumnVector<T> ColumnVectorT; + typedef cvc5::theory::arith::RowVector<T> RowVectorT; + typedef cvc5::theory::arith::ColumnVector<T> ColumnVectorT; public: typedef typename RowVectorT::const_iterator RowIterator; @@ -999,4 +999,4 @@ protected: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 7fd22fb76..c9f3ce3da 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -29,12 +29,12 @@ namespace std { template <typename T> std::ostream& operator<<(std::ostream& os, const std::vector<T>& v) { - CVC5::container_to_stream(os, v); + cvc5::container_to_stream(os, v); return os; } } // namespace std -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -545,6 +545,6 @@ void CDCAC::pruneRedundantIntervals(std::vector<CACInterval>& intervals) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 2b607ae78..338f54da2 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -31,7 +31,7 @@ #include "theory/arith/nl/cad/proof_generator.h" #include "theory/arith/nl/cad/variable_ordering.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -210,7 +210,7 @@ class CDCAC } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp index f40d528ff..999e491f6 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.cpp +++ b/src/theory/arith/nl/cad/cdcac_utils.cpp @@ -20,7 +20,7 @@ #include "theory/arith/nl/cad/projections.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -370,6 +370,6 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h index 3b3a3638b..607a2226f 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.h +++ b/src/theory/arith/nl/cad/cdcac_utils.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "theory/arith/nl/cad/projections.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -105,7 +105,7 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp index 1ea172d11..75d1cb723 100644 --- a/src/theory/arith/nl/cad/constraints.cpp +++ b/src/theory/arith/nl/cad/constraints.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/poly_conversion.h" #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -79,6 +79,6 @@ void Constraints::sortConstraints() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index 70c52e85c..e9e59c40b 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -28,7 +28,7 @@ #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -87,7 +87,7 @@ class Constraints } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp index b9e17f844..1bac0c160 100644 --- a/src/theory/arith/nl/cad/projections.cpp +++ b/src/theory/arith/nl/cad/projections.cpp @@ -20,7 +20,7 @@ #include "base/check.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -106,6 +106,6 @@ PolyVector projection_mccallum(const std::vector<Polynomial>& polys) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index 3b8eb412f..94bdfc3ef 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -25,7 +25,7 @@ #include <vector> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -76,7 +76,7 @@ PolyVector projectionMcCallum(const std::vector<poly::Polynomial>& polys); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp index f1ab2d6a9..3cd8fe98e 100644 --- a/src/theory/arith/nl/cad/proof_checker.cpp +++ b/src/theory/arith/nl/cad/proof_checker.cpp @@ -17,9 +17,9 @@ #include "expr/sequence.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -58,4 +58,4 @@ Node CADProofRuleChecker::checkInternal(PfRule id, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index 26bbcc3a9..9100762b7 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "expr/proof_checker.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -53,6 +53,6 @@ class CADProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index fe3734dce..73e19aa28 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -19,7 +19,7 @@ #include "theory/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -230,6 +230,6 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index c1bb4be1e..76a72f9c5 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -28,7 +28,7 @@ #include "theory/arith/nl/cad/cdcac_utils.h" #include "theory/lazy_tree_proof_generator.h" -namespace CVC5 { +namespace cvc5 { class ProofGenerator; @@ -144,7 +144,7 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif #endif diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp index 63db35553..7ebbc90dd 100644 --- a/src/theory/arith/nl/cad/variable_ordering.cpp +++ b/src/theory/arith/nl/cad/variable_ordering.cpp @@ -20,7 +20,7 @@ #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -132,6 +132,6 @@ std::vector<poly::Variable> VariableOrdering::operator()( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h index 7fda3faa4..0ab585197 100644 --- a/src/theory/arith/nl/cad/variable_ordering.h +++ b/src/theory/arith/nl/cad/variable_ordering.h @@ -26,7 +26,7 @@ #include "theory/arith/nl/cad/constraints.h" #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -65,7 +65,7 @@ std::vector<poly_utils::VariableInformation> collectInformation( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index dc18fbdf5..1cf9cbc54 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -20,7 +20,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -212,4 +212,4 @@ bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index de97c48cc..620679735 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -22,7 +22,7 @@ #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/cad/proof_checker.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; @@ -110,6 +110,6 @@ class CadSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__CAD_SOLVER_H */ diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp index 41331d041..688bab86d 100644 --- a/src/theory/arith/nl/ext/constraint.cpp +++ b/src/theory/arith/nl/ext/constraint.cpp @@ -18,9 +18,9 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/nl/ext/monomial.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -123,4 +123,4 @@ bool ConstraintDb::isMaximal(Node atom, Node x) const } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h index 9e6451c99..a96949a1e 100644 --- a/src/theory/arith/nl/ext/constraint.h +++ b/src/theory/arith/nl/ext/constraint.h @@ -21,7 +21,7 @@ #include "expr/kind.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -84,6 +84,6 @@ class ConstraintDb } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL_SOLVER_H */ diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index fc806199e..e20224207 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nl_lemma_utils.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -109,4 +109,4 @@ CDProof* ExtState::getProof() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 1d8e7ea0a..2d20e1557 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -21,7 +21,7 @@ #include "expr/proof_set.h" #include "theory/arith/nl/ext/monomial.h" -namespace CVC5 { +namespace cvc5 { class CDProof; @@ -91,6 +91,6 @@ struct ExtState } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 675368843..09e1d4f10 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -207,4 +207,4 @@ Node FactoringCheck::getFactorSkolem(Node n, CDProof* proof) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index 89c5fce30..08154cb98 100644 --- a/src/theory/arith/nl/ext/factoring_check.h +++ b/src/theory/arith/nl/ext/factoring_check.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class CDProof; @@ -69,6 +69,6 @@ class FactoringCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp index 86abed70c..784c07691 100644 --- a/src/theory/arith/nl/ext/monomial.cpp +++ b/src/theory/arith/nl/ext/monomial.cpp @@ -18,9 +18,9 @@ #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -333,4 +333,4 @@ Node MonomialDb::mkMonomialRemFactor(Node n, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h index 98083b996..6646e4a73 100644 --- a/src/theory/arith/nl/ext/monomial.h +++ b/src/theory/arith/nl/ext/monomial.h @@ -20,7 +20,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -144,6 +144,6 @@ class MonomialDb } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL_MONOMIAL_H */ diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index c8194bbd0..344218148 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -24,7 +24,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -520,4 +520,4 @@ void MonomialBoundsCheck::checkResBounds() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h index e63dd454a..a19c61e64 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.h +++ b/src/theory/arith/nl/ext/monomial_bounds_check.h @@ -18,7 +18,7 @@ #include "expr/node.h" #include "theory/arith/nl/ext/constraint.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -86,6 +86,6 @@ class MonomialBoundsCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 9fc2ba10a..a30d4aff9 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -22,7 +22,7 @@ #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/ext/ext_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -757,4 +757,4 @@ void MonomialCheck::setMonomialFactor(Node a, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index 948368542..f242182b4 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -19,7 +19,7 @@ #include "theory/arith/nl/ext/monomial.h" #include "theory/theory_inference.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -194,6 +194,6 @@ class MonomialCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index 26db3c9e0..b6c4572f5 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -18,9 +18,9 @@ #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -158,4 +158,4 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h index 7bd4b7e38..90518fc08 100644 --- a/src/theory/arith/nl/ext/proof_checker.h +++ b/src/theory/arith/nl/ext/proof_checker.h @@ -21,7 +21,7 @@ #include "expr/proof_checker.h" #include "expr/proof_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -51,6 +51,6 @@ class ExtProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 543b6a0bd..7392d45f4 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -22,7 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -57,4 +57,4 @@ void SplitZeroCheck::check() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index 316e304ff..04148bd19 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -18,7 +18,7 @@ #include "expr/node.h" #include "context/cdhashset.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -50,6 +50,6 @@ class SplitZeroCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index bdeca7a29..711bc9816 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -22,7 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -164,4 +164,4 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h index 7d48d249b..b5159e721 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.h +++ b/src/theory/arith/nl/ext/tangent_plane_check.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -67,6 +67,6 @@ class TangentPlaneCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index 125fbb05a..72848ac89 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -17,9 +17,9 @@ #include "theory/arith/arith_utilities.h" #include "theory/uf/equality_engine.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -129,4 +129,4 @@ bool NlExtTheoryCallback::isExtfReduced(int effort, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index c747eef69..0e0e1411b 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -18,7 +18,7 @@ #include "expr/node.h" #include "theory/ext_theory.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace eq { class EqualityEngine; @@ -84,6 +84,6 @@ class NlExtTheoryCallback : public ExtTheoryCallback } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */ diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 01f4c6e15..0e339857b 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -25,9 +25,9 @@ #include "theory/rewriter.h" #include "util/iand.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -298,4 +298,4 @@ Node IAndSolver::bitwiseLemma(Node i) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 95d9632aa..2b7f90e9b 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/arith/nl/iand_utils.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -132,6 +132,6 @@ class IAndSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__IAND_SOLVER_H */ diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index cd96021b0..e08068b7e 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -21,7 +21,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -276,4 +276,4 @@ Node IAndUtils::twoToKMinusOne(unsigned k) const } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h index da5f8f04f..60c3cbe13 100644 --- a/src/theory/arith/nl/iand_utils.h +++ b/src/theory/arith/nl/iand_utils.h @@ -20,7 +20,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -169,6 +169,6 @@ class IAndUtils } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */ diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp index 87d823018..31b7b085b 100644 --- a/src/theory/arith/nl/icp/candidate.cpp +++ b/src/theory/arith/nl/icp/candidate.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/icp/intersection.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -115,6 +115,6 @@ std::ostream& operator<<(std::ostream& os, const Candidate& c) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h index d4ad11fcf..4bcbf3e85 100644 --- a/src/theory/arith/nl/icp/candidate.h +++ b/src/theory/arith/nl/icp/candidate.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "theory/arith/nl/icp/intersection.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -78,7 +78,7 @@ std::ostream& operator<<(std::ostream& os, const Candidate& c); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp index c0b0cb768..acf499a21 100644 --- a/src/theory/arith/nl/icp/contraction_origins.cpp +++ b/src/theory/arith/nl/icp/contraction_origins.cpp @@ -14,7 +14,7 @@ #include "theory/arith/nl/icp/contraction_origins.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -117,4 +117,4 @@ inline std::ostream& operator<<(std::ostream& os, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h index 0f22b5463..dfddbce78 100644 --- a/src/theory/arith/nl/icp/contraction_origins.h +++ b/src/theory/arith/nl/icp/contraction_origins.h @@ -20,7 +20,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -99,6 +99,6 @@ std::ostream& operator<<(std::ostream& os, const ContractionOriginManager& com); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index e09264a25..2f6cdf220 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -26,7 +26,7 @@ #include "theory/rewriter.h" #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -384,4 +384,4 @@ void ICPSolver::check() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index 56ec03706..11fd9ac1b 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -28,7 +28,7 @@ #include "theory/arith/nl/icp/intersection.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -153,6 +153,6 @@ class ICPSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index 6cdba297c..e0e93e1dd 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -24,7 +24,7 @@ #include "base/output.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -221,6 +221,6 @@ PropagationResult intersect_interval_with(poly::Interval& cur, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index c453f8314..dd4afadfc 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -25,7 +25,7 @@ namespace poly { class Interval; } -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -77,7 +77,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h index 8acbfec05..981355e4a 100644 --- a/src/theory/arith/nl/icp/interval.h +++ b/src/theory/arith/nl/icp/interval.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -58,7 +58,7 @@ inline std::ostream& operator<<(std::ostream& os, const Interval& i) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index f3c2d70c8..9740e1b46 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -17,7 +17,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nonlinear_extension.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -78,4 +78,4 @@ Node ArgTrie::add(Node d, const std::vector<Node>& args) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index 71d86b08a..32fe763b4 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "theory/theory_inference.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -144,6 +144,6 @@ class ArgTrie } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H */ diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index f7edefff7..882cd12a4 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -24,9 +24,9 @@ #include "theory/theory_model.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -1342,4 +1342,4 @@ void NlModel::getModelValueRepair( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index b2c435098..9da8738b6 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -22,7 +22,7 @@ #include "expr/kind.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace context { class Context; @@ -329,6 +329,6 @@ class NlModel } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 3c46e1652..03563006b 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -27,9 +27,9 @@ #include "theory/rewriter.h" #include "theory/theory_model.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -622,4 +622,4 @@ void NonlinearExtension::runStrategy(Theory::Effort effort, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index b6fb53651..722741d7d 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -41,7 +41,7 @@ #include "theory/theory.h" #include "util/result.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace eq { class EqualityEngine; @@ -296,6 +296,6 @@ class NonlinearExtension } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */ diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 5738dccfc..c7b549655 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -23,12 +23,12 @@ #include "theory/arith/bound_inference.h" #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { -poly::Variable VariableMapper::operator()(const CVC5::Node& n) +poly::Variable VariableMapper::operator()(const cvc5::Node& n) { auto it = mVarCVCpoly.find(n); if (it == mVarCVCpoly.end()) @@ -54,7 +54,7 @@ poly::Variable VariableMapper::operator()(const CVC5::Node& n) return it->second; } -CVC5::Node VariableMapper::operator()(const poly::Variable& n) +cvc5::Node VariableMapper::operator()(const poly::Variable& n) { auto it = mVarpolyCVC.find(n); Assert(it != mVarpolyCVC.end()) @@ -62,7 +62,7 @@ CVC5::Node VariableMapper::operator()(const poly::Variable& n) return it->second; } -CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC5::Node& var) +cvc5::Node as_cvc_upolynomial(const poly::UPolynomial& p, const cvc5::Node& var) { Trace("poly::conversion") << "Converting " << p << " over " << var << std::endl; @@ -87,9 +87,9 @@ CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC5::Node& var) return res; } -poly::UPolynomial as_poly_upolynomial_impl(const CVC5::Node& n, +poly::UPolynomial as_poly_upolynomial_impl(const cvc5::Node& n, poly::Integer& denominator, - const CVC5::Node& var) + const cvc5::Node& var) { denominator = poly::Integer(1); if (n.isVar()) @@ -140,14 +140,14 @@ poly::UPolynomial as_poly_upolynomial_impl(const CVC5::Node& n, return poly::UPolynomial(); } -poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n, - const CVC5::Node& var) +poly::UPolynomial as_poly_upolynomial(const cvc5::Node& n, + const cvc5::Node& var) { poly::Integer denom; return as_poly_upolynomial_impl(n, denom, var); } -poly::Polynomial as_poly_polynomial_impl(const CVC5::Node& n, +poly::Polynomial as_poly_polynomial_impl(const cvc5::Node& n, poly::Integer& denominator, VariableMapper& vm) { @@ -195,12 +195,12 @@ poly::Polynomial as_poly_polynomial_impl(const CVC5::Node& n, } return poly::Polynomial(); } -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, VariableMapper& vm) +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm) { poly::Integer denom; return as_poly_polynomial_impl(n, denom, vm); } -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm, poly::Rational& denominator) { @@ -257,7 +257,7 @@ void collect_monomials(const lp_polynomial_context_t* ctx, } } // namespace -CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm) +cvc5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm) { CollectMonomialData cmd(vm); // Do the actual conversion @@ -274,7 +274,7 @@ CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm) return cmd.d_nm->mkNode(Kind::PLUS, cmd.d_terms); } -poly::SignCondition normalize_kind(CVC5::Kind kind, +poly::SignCondition normalize_kind(cvc5::Kind kind, bool negated, poly::Polynomial& lhs) { @@ -803,6 +803,6 @@ poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 9adc9a996..9aef0db18 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -30,7 +30,7 @@ #include "expr/node.h" #include "util/real_algebraic_number.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -42,23 +42,23 @@ namespace nl { struct VariableMapper { /** A mapping from CVC4 variables to poly variables. */ - std::map<CVC5::Node, poly::Variable> mVarCVCpoly; + std::map<cvc5::Node, poly::Variable> mVarCVCpoly; /** A mapping from poly variables to CVC4 variables. */ - std::map<poly::Variable, CVC5::Node> mVarpolyCVC; + std::map<poly::Variable, cvc5::Node> mVarpolyCVC; /** Retrieves the according poly variable. */ - poly::Variable operator()(const CVC5::Node& n); + poly::Variable operator()(const cvc5::Node& n); /** Retrieves the according CVC4 variable. */ - CVC5::Node operator()(const poly::Variable& n); + cvc5::Node operator()(const poly::Variable& n); }; -/** Convert a poly univariate polynomial to a CVC5::Node. */ -CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p, - const CVC5::Node& var); +/** Convert a poly univariate polynomial to a cvc5::Node. */ +cvc5::Node as_cvc_upolynomial(const poly::UPolynomial& p, + const cvc5::Node& var); -/** Convert a CVC5::Node to a poly univariate polynomial. */ -poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n, - const CVC5::Node& var); +/** Convert a cvc5::Node to a poly univariate polynomial. */ +poly::UPolynomial as_poly_upolynomial(const cvc5::Node& n, + const cvc5::Node& var); /** * Constructs a polynomial from the given node. @@ -73,8 +73,8 @@ poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n, * in the context of ICP) the second overload provides the denominator in the * third argument. */ -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, VariableMapper& vm); -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm); +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm, poly::Rational& denominator); @@ -87,7 +87,7 @@ poly::Polynomial as_poly_polynomial(const CVC5::Node& n, * multiplications with one or use NONLINEAR_MULT where regular MULT may be * sufficient), so it may be sensible to rewrite it afterwards. */ -CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm); +cvc5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm); /** * Constructs a constraints (a polynomial and a sign condition) from the given @@ -164,7 +164,7 @@ poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp index 92cebc8fc..33a73ddd7 100644 --- a/src/theory/arith/nl/stats.cpp +++ b/src/theory/arith/nl/stats.cpp @@ -16,7 +16,7 @@ #include "smt/smt_statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -38,4 +38,4 @@ NlStats::~NlStats() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index 66157d0a3..66f41375b 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -19,7 +19,7 @@ #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -44,6 +44,6 @@ class NlStats } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL__STATS_H */ diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index af23f67f9..4df53b103 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -19,7 +19,7 @@ #include "base/check.h" #include "options/arith_options.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -173,4 +173,4 @@ StepGenerator Strategy::getStrategy() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index 9caf6322b..139db7459 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -18,7 +18,7 @@ #include <iosfwd> #include <vector> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -173,6 +173,6 @@ class Strategy } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL__STRATEGY_H */ diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 05849a579..5e2358b68 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -28,7 +28,7 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -276,4 +276,4 @@ std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index 8bd00c456..c5eb45728 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -108,6 +108,6 @@ class ExponentialSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index fe071c36a..4fc85666a 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -19,9 +19,9 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -402,4 +402,4 @@ Node TranscendentalProofRuleChecker::checkInternal( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h index 2a6837590..a4c8b55cb 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.h +++ b/src/theory/arith/nl/transcendental/proof_checker.h @@ -21,7 +21,7 @@ #include "expr/proof_checker.h" #include "expr/proof_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -53,6 +53,6 @@ class TranscendentalProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 052b6c056..c8c375096 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -28,7 +28,7 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -484,4 +484,4 @@ std::pair<Node, Node> SineSolver::getSecantBounds(TNode e, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index c20c50f6d..b85d0dc48 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/arith/nl/transcendental/transcendental_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -175,6 +175,6 @@ class SineSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index f2817344a..5a9e87b7f 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -18,7 +18,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -243,4 +243,4 @@ std::pair<Node, Node> TaylorGenerator::getTfModelBounds(Node tf, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index b13be57f0..8b7f5340d 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -17,7 +17,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -118,6 +118,6 @@ class TaylorGenerator } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index bedfe4d3b..ed5ab4255 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -27,9 +27,9 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -438,4 +438,4 @@ int TranscendentalSolver::regionToConcavity(Kind k, int region) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index e22bf3e64..c3d098e03 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -22,7 +22,7 @@ #include "theory/arith/nl/transcendental/sine_solver.h" #include "theory/arith/nl/transcendental/transcendental_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -200,6 +200,6 @@ class TranscendentalSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 6ab136d39..e662c017e 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -21,7 +21,7 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -437,4 +437,4 @@ void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 21a60e038..a55071ef1 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -21,7 +21,7 @@ #include "theory/arith/nl/transcendental/proof_checker.h" #include "theory/arith/nl/transcendental/taylor_generator.h" -namespace CVC5 { +namespace cvc5 { class CDProof; namespace theory { namespace arith { @@ -278,6 +278,6 @@ struct TranscendentalState } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */ diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index d1ef6486e..b872b4309 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -24,7 +24,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -1412,4 +1412,4 @@ bool Polynomial::isNonlinear() const { } //namespace arith } //namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index c4d0e2268..7b9002d82 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -28,7 +28,7 @@ #include "theory/arith/delta_rational.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -1404,6 +1404,6 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NORMAL_FORM_H */ diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 15e09eaa5..600724f33 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -26,9 +26,9 @@ #include "theory/rewriter.h" #include "theory/theory.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -499,4 +499,4 @@ Node OperatorElim::mkWitnessTerm(Node v, } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index fa09ad26b..1b2f7190e 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -21,7 +21,7 @@ #include "theory/logic_info.h" #include "theory/skolem_lemma.h" -namespace CVC5 { +namespace cvc5 { class TConvProofGenerator; @@ -142,4 +142,4 @@ class OperatorElim : public EagerProofGenerator } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 6e4fa6bed..fe3408a43 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -22,7 +22,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -686,4 +686,4 @@ void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index b7a1a0efe..30a684e47 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -32,7 +32,7 @@ #include "theory/arith/constraint_forward.h" #include "theory/arith/delta_rational.h" -namespace CVC5 { +namespace cvc5 { namespace context { class Context; } @@ -414,6 +414,6 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */ diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 09ef5bf34..23f141535 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -23,7 +23,7 @@ #include "theory/arith/normal_form.h" #include "theory/arith/operator_elim.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -360,4 +360,4 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, } } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h index 5b9a50387..ca4fdfb6d 100644 --- a/src/theory/arith/proof_checker.h +++ b/src/theory/arith/proof_checker.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "expr/proof_checker.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -43,6 +43,6 @@ class ArithProofRuleChecker : public ProofRuleChecker } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__PROOF_CHECKER_H */ diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h index 169e4e2db..a02738fd3 100644 --- a/src/theory/arith/proof_macros.h +++ b/src/theory/arith/proof_macros.h @@ -21,11 +21,11 @@ #include "options/smt_options.h" #define ARITH_PROOF(x) \ - if (CVC5::options::produceProofs()) \ + if (cvc5::options::produceProofs()) \ { \ x; \ } -#define ARITH_NULLPROOF(x) (CVC5::options::produceProofs()) ? x : NULL -#define ARITH_PROOF_ON() CVC5::options::produceProofs() +#define ARITH_NULLPROOF(x) (cvc5::options::produceProofs()) ? x : NULL +#define ARITH_PROOF_ON() cvc5::options::produceProofs() #endif // CVC4__THEORY__ARITH__PROOF_MACROS_H diff --git a/src/theory/arith/rewrites.cpp b/src/theory/arith/rewrites.cpp index 9522ef4f4..d095b4a20 100644 --- a/src/theory/arith/rewrites.cpp +++ b/src/theory/arith/rewrites.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -47,4 +47,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r) } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h index 250eacb09..e7a44f27e 100644 --- a/src/theory/arith/rewrites.h +++ b/src/theory/arith/rewrites.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -77,6 +77,6 @@ std::ostream& operator<<(std::ostream& out, Rewrite r); } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__REWRITES_H */ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index fe6fad4d7..f599cdf40 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -280,4 +280,4 @@ SimplexDecisionProcedure::sgn_table::const_iterator SimplexDecisionProcedure::fi } } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index a1ee18adf..d826f0ba3 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -64,7 +64,7 @@ #include "util/statistics_registry.h" #include "util/stats_timer.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -221,4 +221,4 @@ protected: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp index ea868a886..81723f7c2 100644 --- a/src/theory/arith/simplex_update.cpp +++ b/src/theory/arith/simplex_update.cpp @@ -19,7 +19,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -188,4 +188,4 @@ std::ostream& operator<<(std::ostream& out, WitnessImprovement w){ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index 833e92dd4..8310d3783 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -33,7 +33,7 @@ #include "theory/arith/constraint_forward.h" #include "util/maybe.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -354,4 +354,4 @@ std::ostream& operator<<(std::ostream& out, const UpdateInfo& up); } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 0efc33d02..d7cfd28c1 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -1024,4 +1024,4 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 16af7292d..605d23767 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -60,7 +60,7 @@ #include "util/dense_map.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -242,4 +242,4 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index c39b3aae7..2d389b0f5 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -19,7 +19,7 @@ #include "theory/arith/tableau.h" using namespace std; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -192,4 +192,4 @@ void Tableau::printBasicRow(ArithVar basic, std::ostream& out){ } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 0834c7f35..6c597aa66 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -26,7 +26,7 @@ #include "util/dense_map.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -159,4 +159,4 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp index a167cf1a8..b0f2ab9a8 100644 --- a/src/theory/arith/tableau_sizes.cpp +++ b/src/theory/arith/tableau_sizes.cpp @@ -19,7 +19,7 @@ #include "theory/arith/tableau_sizes.h" #include "theory/arith/tableau.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -33,4 +33,4 @@ uint32_t TableauSizes::getColumnLength(ArithVar x) const { } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h index 3bbb5c818..969620db1 100644 --- a/src/theory/arith/tableau_sizes.h +++ b/src/theory/arith/tableau_sizes.h @@ -21,7 +21,7 @@ #include "theory/arith/arithvar.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -39,4 +39,4 @@ public: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 12603ea7d..577aa0e6c 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -29,9 +29,9 @@ #include "theory/theory_model.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -313,4 +313,4 @@ eq::ProofEqEngine* TheoryArith::getProofEqEngine() } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e430f6da6..40abe21e0 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -24,7 +24,7 @@ #include "theory/arith/inference_manager.h" #include "theory/theory.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -165,4 +165,4 @@ class TheoryArith : public Theory { } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 1e9e8ca3f..b11bff768 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -74,9 +74,9 @@ #include "util/statistics_registry.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -5714,4 +5714,4 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index e0b7cea56..929f40b56 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -54,7 +54,7 @@ #include "util/result.h" #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { class EagerProofGenerator; @@ -886,4 +886,4 @@ private: } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index dc8885e55..e192270ff 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -19,7 +19,7 @@ #ifndef CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H #define CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -159,6 +159,6 @@ class IndexedRootPredicateTypeRule } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */ diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index a32073ad9..9b3f4535b 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -25,7 +25,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -102,6 +102,6 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> { } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */ |