diff options
Diffstat (limited to 'src/theory/arith')
152 files changed, 529 insertions, 546 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 8d98475ce..c911d03e9 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -36,7 +36,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -367,9 +367,9 @@ public: double sumInfeasibilities(bool mip) const override { return 0.0; } }; -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -535,14 +535,14 @@ private: int ApproxGLPK::s_verbosity = 0; -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 #endif /*#ifdef CVC4_USE_GLPK */ /* End the declaration of GLPK specific code. */ /* Begin GPLK/NOGLPK Glue code. */ -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { ApproximateSimplex* ApproximateSimplex::mkApproximateSimplexSolver(const ArithVariables& vars, TreeLog& l, ApproximateStatistics& s){ @@ -559,15 +559,14 @@ bool ApproximateSimplex::enabled() { return false; #endif } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 /* End GPLK/NOGLPK Glue code. */ - /* Begin GPLK implementation. */ #ifdef CVC4_USE_GLPK -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -3175,9 +3174,8 @@ void ApproxGLPK::tryCut(int nid, CutInfo& cut) } } - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 a9b179e31..5835c57c1 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -163,7 +163,6 @@ class ApproximateSimplex{ static Integer s_defaultMaxDenom; };/* class ApproximateSimplex */ - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index fa6fd108c..42189f86a 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -47,7 +47,7 @@ Node ArithIteUtils::applyReduceVariablesInItes(Node n){ } Node ArithIteUtils::reduceVariablesInItes(Node n){ - using namespace CVC4::kind; + using namespace CVC5::kind; if(d_reduceVar.find(n) != d_reduceVar.end()){ Node res = d_reduceVar[n]; return res.isNull() ? n : res; @@ -455,7 +455,6 @@ bool ArithIteUtils::solveBinOr(TNode binor){ return false; } - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index e1e27884d..263ddda8e 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 CVC4 { +namespace CVC5 { namespace preprocessing { namespace util { class ContainsTermITEVisitor; @@ -109,8 +109,8 @@ private: }; /* class ArithIteUtils */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 83b8b67c2..9190dac7d 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { bool ArithMSum::getMonomial(Node n, Node& c, Node& v) @@ -321,5 +321,5 @@ void ArithMSum::debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c) Trace(c) << std::endl; } -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h index f7470d4e0..f4a2bf824 100644 --- a/src/theory/arith/arith_msum.h +++ b/src/theory/arith/arith_msum.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace theory { /** Arithmetic utilities regarding monomial sums. @@ -182,7 +182,7 @@ class ArithMSum static void debugPrintMonomialSum(std::map<Node, Node>& msum, const char* c); }; -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace theory +} // 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 a075c87fe..2b120c9c7 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -80,4 +80,4 @@ bool ArithPreprocess::isReduced(TNode atom) const } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index db0fd7d5e..45ce0c597 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 CVC4 { +namespace CVC5 { namespace theory { class SkolemLemma; @@ -86,6 +86,6 @@ class ArithPreprocess } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 2de8cf66b..01e88b1a8 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 CVC4 { +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()){ - CVC4::Rational r(expr::NodeValue::MAX_CHILDREN); + CVC5::Rational r(expr::NodeValue::MAX_CHILDREN); if (exp <= r) { unsigned num = exp.getNumerator().toUnsignedInt(); @@ -899,6 +899,6 @@ RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r) return RewriteResponse(REWRITE_AGAIN_FULL, ret); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 9bf88dfe6..556a7bda7 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -71,8 +71,8 @@ class ArithRewriter : public TheoryRewriter static RewriteResponse returnRewrite(TNode t, Node ret, Rewrite r); }; /* class ArithRewriter */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 1c41ecf81..bab1d6eb9 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -35,4 +35,4 @@ bool ArithState::isInConflict() const } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h index ffb4a2abc..dfe2bc877 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -52,6 +52,6 @@ class ArithState : public TheoryState } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index b7169df1f..b0129970e 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -271,6 +271,6 @@ void ArithStaticLearner::addBound(TNode n) { } } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 799d0bcee..668527c0f 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 CVC4 { +namespace CVC5 { namespace context { class Context; } @@ -69,8 +69,8 @@ private: };/* class ArithStaticLearner */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 4f1f50b7a..16c412546 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -16,9 +16,9 @@ #include <cmath> -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -325,4 +325,4 @@ Node negateProofLiteral(TNode n) } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 40ca7b8f6..9c0edb893 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -342,8 +342,8 @@ Rational greatestIntLessThan(const Rational&); /** Negates a node in arithmetic proof normal form. */ Node negateProofLiteral(TNode n); -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__ARITH__ARITH_UTILITIES_H */ diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp index 59253e87c..a0c29cb84 100644 --- a/src/theory/arith/arithvar.cpp +++ b/src/theory/arith/arithvar.cpp @@ -19,7 +19,7 @@ #include <limits> #include <set> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -30,6 +30,6 @@ bool debugIsASet(const std::vector<ArithVar>& variables){ return asSet.size() == variables.size(); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index dd5ea70d9..a49797845 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -39,7 +39,6 @@ typedef std::vector< ArithRatPair > ArithRatPairVec; extern bool debugIsASet(const ArithVarVec& variables); - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index f01b0c7ac..dceeeb407 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -88,8 +88,8 @@ public: };/* class ArithVarNodeMap */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 e5c995971..292fccb34 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -151,6 +151,6 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol) } } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index b7266a1e2..faca0cb25 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -90,6 +90,6 @@ public: } d_statistics; };/* class AttemptSolutionSDP */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index cb9053669..949828aeb 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -229,6 +229,6 @@ public: virtual void operator()(ArithVar v, const BoundsInfo& up) = 0; }; -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp index d2adc94af..126954144 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/bound_inference.h b/src/theory/arith/bound_inference.h index dc32ff179..7041777d8 100644 --- a/src/theory/arith/bound_inference.h +++ b/src/theory/arith/bound_inference.h @@ -21,7 +21,7 @@ #include "expr/node.h" -namespace CVC4 { +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 CVC4 +} // namespace CVC5 #endif
\ No newline at end of file diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 81f48ad00..7fe8e4934 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -194,6 +194,6 @@ BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const { return boundsInfo(basic).hasBounds(); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 9f0ae1017..66004871b 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 CVC4 { +namespace CVC5 { class ProofNode; @@ -197,6 +197,6 @@ public: BoundCounts hasBounds(ArithVar basic) const; }; -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index f2210574b..f2e51be02 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -689,6 +689,6 @@ std::vector<Node> andComponents(TNode an) return a; } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 9815ad9c8..540e985f7 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 CVC4 { +namespace CVC5 { class ProofNodeManager; @@ -297,6 +297,6 @@ private: std::vector<Node> andComponents(TNode an); -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index f2de5da6c..cc1129f50 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -32,9 +32,9 @@ using namespace std; -using namespace CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -2426,6 +2426,6 @@ std::pair<int, int> Constraint::unateFarkasSigns(ConstraintCP ca, ConstraintCP c return make_pair(a_sgn, b_sgn); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 6ac03bb82..3caa5a030 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 CVC4 { +namespace CVC5 { class ProofNodeManager; @@ -1275,9 +1275,8 @@ private: }; /* ConstraintDatabase */ - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 9a42b8a97..8d36df304 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -44,8 +44,8 @@ typedef const RationalVector* RationalVectorCP; static const RationalVectorCP RationalVectorCPSentinel = NULL; static const RationalVectorP RationalVectorPSentinel = NULL; -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 426e10956..36c8d06f1 100644 --- a/src/theory/arith/cut_log.cpp +++ b/src/theory/arith/cut_log.cpp @@ -31,7 +31,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -702,6 +702,6 @@ void DenseVector::print(ostream& out, const DenseMap<Rational>& v){ out << "]"; } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 2b67026dc..961092f6e 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -288,8 +288,6 @@ public: void printBranchInfo(std::ostream& os) const; }; - - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index b7f641338..7d20a1859 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -21,7 +21,7 @@ using namespace std; -namespace CVC4 { +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 } } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index ce0a2cffd..e2b769b18 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 CVC4 { +namespace CVC5 { class DeltaRational; @@ -46,22 +46,20 @@ class DeltaRationalException : public Exception { */ class DeltaRational { private: - CVC4::Rational c; - CVC4::Rational k; + CVC5::Rational c; + CVC5::Rational k; public: DeltaRational() : c(0,1), k(0,1) {} - DeltaRational(const CVC4::Rational& base) : c(base), k(0,1) {} - DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) : - c(base), k(coeff) {} - - const CVC4::Rational& getInfinitesimalPart() const { - return k; + DeltaRational(const CVC5::Rational& base) : c(base), k(0, 1) {} + DeltaRational(const CVC5::Rational& base, const CVC5::Rational& coeff) + : c(base), k(coeff) + { } - const CVC4::Rational& getNoninfinitesimalPart() const { - return c; - } + const CVC5::Rational& getInfinitesimalPart() const { return k; } + + const CVC5::Rational& getNoninfinitesimalPart() const { return c; } int sgn() const { int s = getNoninfinitesimalPart().sgn(); @@ -99,14 +97,14 @@ public: } DeltaRational operator+(const DeltaRational& other) const{ - CVC4::Rational tmpC = c+other.c; - CVC4::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{ - CVC4::Rational tmpC = a*c; - CVC4::Rational tmpK = a*k; + CVC5::Rational tmpC = a * c; + CVC5::Rational tmpK = a * k; return DeltaRational(tmpC, tmpK); } @@ -129,7 +127,7 @@ public: DeltaRational operator-(const DeltaRational& a) const{ - CVC4::Rational negOne(CVC4::Integer(-1)); + CVC5::Rational negOne(CVC5::Integer(-1)); return *(this) + (a * negOne); } @@ -138,14 +136,14 @@ public: } DeltaRational operator/(const Rational& a) const{ - CVC4::Rational tmpC = c/a; - CVC4::Rational tmpK = k/a; + CVC5::Rational tmpC = c / a; + CVC5::Rational tmpK = k / a; return DeltaRational(tmpC, tmpK); } DeltaRational operator/(const Integer& a) const{ - CVC4::Rational tmpC = c/a; - CVC4::Rational tmpK = k/a; + CVC5::Rational tmpC = c / a; + CVC5::Rational tmpK = k / a; return DeltaRational(tmpC, tmpK); } @@ -206,7 +204,8 @@ public: return *(this); } - DeltaRational& operator*=(const CVC4::Rational& a){ + DeltaRational& operator*=(const CVC5::Rational& a) + { c *= a; k *= a; @@ -300,4 +299,4 @@ public: std::ostream& operator<<(std::ostream& os, const DeltaRational& n); -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index a232464e5..51dd69650 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -24,7 +24,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -833,6 +833,6 @@ Node DioSolver::trailIndexToEquality(TrailIndex i) const { return eq; } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index dc4711800..7892bec52 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 CVC4 { +namespace CVC5 { namespace context { class Context; } @@ -421,8 +421,8 @@ public: Statistics d_statistics; };/* class DioSolver */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 5ad2f16c0..d4e26600d 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -273,6 +273,6 @@ bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingI return false; } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index 174a91c75..3e1bc0ee7 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -111,6 +111,6 @@ private: } d_statistics; };/* class DualSimplexDecisionProcedure */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp index 9c88ccfad..142a060ec 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/error_set.cpp @@ -22,7 +22,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -477,6 +477,6 @@ void ErrorSet::pushFocusInto(ArithVarVec& vec) const{ } } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 7400a229f..cdf155c6d 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -412,6 +412,6 @@ private: Statistics d_statistics; }; -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index c85c3df2a..61280d651 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -25,7 +25,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -859,6 +859,6 @@ const Rational& FCSimplexDecisionProcedure::focusCoefficient(ArithVar nb) const } } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 45a9b79bb..73e5ae54f 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -254,6 +254,6 @@ private: } d_statistics; };/* class FCSimplexDecisionProcedure */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp index 0475e2472..25494bdee 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -264,4 +264,4 @@ std::ostream& operator<<(std::ostream& os, const Algorithms a){ } /* namespace arith */ } /* namespace theory */ -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h index 03ab8e53b..251c7cbb8 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/infer_bounds.h @@ -27,8 +27,7 @@ #include "util/maybe.h" #include "util/rational.h" - -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -161,4 +160,4 @@ private: } /* namespace arith */ } /* namespace theory */ -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index a281c825b..66b628302 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -147,4 +147,4 @@ bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem) } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index dd617f4a3..bf5ed7b10 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -117,6 +117,6 @@ class InferenceManager : public InferenceManagerBuffered } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 04bdc277e..b839ccc22 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -4,13 +4,13 @@ # src/theory/builtin/kinds. # -theory THEORY_ARITH ::CVC4::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 ::CVC4::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 \ - ::CVC4::Divisible \ - ::CVC4::DivisibleHashFunction \ + ::CVC5::Divisible \ + ::CVC5::DivisibleHashFunction \ "util/divisible.h" \ - "operator for the divisibility-by-k predicate; payload is an instance of the CVC4::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 \ - ::CVC4::Rational \ - ::CVC4::RationalHashFunction \ + ::CVC5::Rational \ + ::CVC5::RationalHashFunction \ "util/rational.h" \ - "a multiple-precision rational constant; payload is an instance of the CVC4::Rational class" + "a multiple-precision rational constant; payload is an instance of the CVC5::Rational class" enumerator REAL_TYPE \ - "::CVC4::theory::arith::RationalEnumerator" \ + "::CVC5::theory::arith::RationalEnumerator" \ "theory/arith/type_enumerator.h" enumerator INTEGER_TYPE \ - "::CVC4::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 \ - ::CVC4::IndexedRootPredicate \ - ::CVC4::IndexedRootPredicateHashFunction \ + ::CVC5::IndexedRootPredicate \ + ::CVC5::IndexedRootPredicateHashFunction \ "util/indexed_root_predicate.h" \ - "operator for the indexed root predicate; payload is an instance of the CVC4::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 ::CVC4::theory::arith::ArithOperatorTypeRule -typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule -typerule NONLINEAR_MULT ::CVC4::theory::arith::ArithOperatorTypeRule -typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule -typerule UMINUS ::CVC4::theory::arith::ArithOperatorTypeRule -typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule -typerule POW ::CVC4::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 ::CVC4::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 ::CVC4::theory::arith::IndexedRootPredicateTypeRule +typerule INDEXED_ROOT_PREDICATE ::CVC5::theory::arith::IndexedRootPredicateTypeRule -typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule CAST_TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule TO_INTEGER ::CVC4::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 ::CVC4::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 ::CVC4::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 \ - ::CVC4::IntAnd \ - "::CVC4::UnsignedHashFunction< ::CVC4::IntAnd >" \ + ::CVC5::IntAnd \ + "::CVC5::UnsignedHashFunction< ::CVC5::IntAnd >" \ "util/iand.h" \ - "operator for integer AND; payload is an instance of the CVC4::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 ::CVC4::theory::arith::IAndOpTypeRule -typerule IAND ::CVC4::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 943f3216e..28f386e2a 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -22,7 +22,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -1411,6 +1411,6 @@ void LinearEqualityModule::directlyAddToCoefficient(ArithVar row, ArithVar col, d_tableau.directlyAddToCoefficient(row, col, mult, d_trackCallback); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index df4e5f30e..4a923b677 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -756,6 +756,6 @@ public: } }; -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp index fb8c02379..dd7f28228 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -26,6 +26,6 @@ void NoEffectCCCB::update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) { void NoEffectCCCB::multiplyRow(RowIndex ridx, int sgn){} bool NoEffectCCCB::canUseRow(RowIndex ridx) const { return false; } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 09fdc2e91..553cef7d4 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -368,8 +368,8 @@ public: typedef MatrixEntry<T> Entry; protected: - typedef CVC4::theory::arith::RowVector<T> RowVectorT; - typedef CVC4::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; @@ -997,7 +997,6 @@ protected: };/* class Matrix<T> */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index c4ecfbbfa..7fd22fb76 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) { - CVC4::container_to_stream(os, v); + CVC5::container_to_stream(os, v); return os; } } // namespace std -namespace CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 15230d14c..2b607ae78 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -210,7 +210,7 @@ class CDCAC } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp index 24bad8d60..f40d528ff 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h index dad9bbd7a..3b3a3638b 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp index 028a61833..1ea172d11 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -79,6 +79,6 @@ void Constraints::sortConstraints() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index 42f8920c8..70c52e85c 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -87,7 +87,7 @@ class Constraints } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp index 5d72f5a2e..b9e17f844 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index 33267cb7a..3b8eb412f 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -25,7 +25,7 @@ #include <vector> -namespace CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp index 45c43e2aa..f1ab2d6a9 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -58,4 +58,4 @@ Node CADProofRuleChecker::checkInternal(PfRule id, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index 5ebe0c6b7..26bbcc3a9 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -53,6 +53,6 @@ class CADProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 9f0799e7c..fe3734dce 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index 4709b8e59..c1bb4be1e 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 CVC4 { +namespace CVC5 { class ProofGenerator; @@ -144,7 +144,7 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 958191fe1..63db35553 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h index 43e85b3cb..7fda3faa4 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index c72c9d48d..dc18fbdf5 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index b83398cd6..de97c48cc 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 CVC4 { +namespace CVC5 { class ProofNodeManager; @@ -110,6 +110,6 @@ class CadSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 9ec3b1fc1..41331d041 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h index d5ed7ccfd..9e6451c99 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -84,6 +84,6 @@ class ConstraintDb } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 28373223b..fc806199e 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -23,8 +23,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nl_lemma_utils.h" - -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -110,4 +109,4 @@ CDProof* ExtState::getProof() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 46ccaeb14..1d8e7ea0a 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 CVC4 { +namespace CVC5 { class CDProof; @@ -91,6 +91,6 @@ struct ExtState } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 7a0da42aa..675368843 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index 4c017d198..89c5fce30 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 CVC4 { +namespace CVC5 { class CDProof; @@ -69,6 +69,6 @@ class FactoringCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp index a0d388dca..86abed70c 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -333,4 +333,4 @@ Node MonomialDb::mkMonomialRemFactor(Node n, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h index 19f855233..98083b996 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -144,6 +144,6 @@ class MonomialDb } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 f1a2f45b9..c8194bbd0 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -520,4 +520,4 @@ void MonomialBoundsCheck::checkResBounds() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 e7ba4d861..e63dd454a 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -86,6 +86,6 @@ class MonomialBoundsCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 7f99b876d..9fc2ba10a 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -757,4 +757,4 @@ void MonomialCheck::setMonomialFactor(Node a, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index a08554476..948368542 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -194,6 +194,6 @@ class MonomialCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index ca600ad55..26db3c9e0 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -158,4 +158,4 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h index d53b674b2..7bd4b7e38 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -51,6 +51,6 @@ class ExtProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 45f4160a0..543b6a0bd 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -57,4 +57,4 @@ void SplitZeroCheck::check() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 030445737..316e304ff 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -50,6 +50,6 @@ class SplitZeroCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 64ea19f3c..bdeca7a29 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -164,4 +164,4 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 a771ae543..7d48d249b 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -67,6 +67,6 @@ class TangentPlaneCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index 214d2a51a..125fbb05a 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -129,4 +129,4 @@ bool NlExtTheoryCallback::isExtfReduced(int effort, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index a3dc74ec8..c747eef69 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 CVC4 { +namespace CVC5 { namespace theory { namespace eq { class EqualityEngine; @@ -84,6 +84,6 @@ class NlExtTheoryCallback : public ExtTheoryCallback } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 7272bb6e3..01f4c6e15 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -298,4 +298,4 @@ Node IAndSolver::bitwiseLemma(Node i) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 137d430c0..95d9632aa 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -132,6 +132,6 @@ class IAndSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 cb3a03aed..cd96021b0 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h index a84fcf978..da5f8f04f 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -169,6 +169,6 @@ class IAndUtils } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 df894ee12..87d823018 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h index 5d8c2b2d0..d4ad11fcf 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp index a076dbdb0..c0b0cb768 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h index bef6b2848..0f22b5463 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index 5b505b070..e09264a25 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -384,4 +384,4 @@ void ICPSolver::check() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index 85b2e86c6..56ec03706 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -153,6 +153,6 @@ class ICPSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index 3dc0ca815..6cdba297c 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index 1670a8f68..c453f8314 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h index ff4bbfcac..8acbfec05 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 CVC4 { +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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index d7785dbc9..f3c2d70c8 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index 6f3ef077a..71d86b08a 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -144,6 +144,6 @@ class ArgTrie } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 5467c64ce..f7edefff7 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -1342,4 +1342,4 @@ void NlModel::getModelValueRepair( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index cd52cb159..b2c435098 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 CVC4 { +namespace CVC5 { namespace context { class Context; @@ -329,6 +329,6 @@ class NlModel } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 781fb0c71..ff1962629 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -621,4 +621,4 @@ void NonlinearExtension::runStrategy(Theory::Effort effort, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index bc8f48c26..b6fb53651 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 CVC4 { +namespace CVC5 { namespace theory { namespace eq { class EqualityEngine; @@ -296,6 +296,6 @@ class NonlinearExtension } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 0dd7cc070..5738dccfc 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { -poly::Variable VariableMapper::operator()(const CVC4::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 CVC4::Node& n) return it->second; } -CVC4::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 @@ CVC4::Node VariableMapper::operator()(const poly::Variable& n) return it->second; } -CVC4::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC4::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 @@ CVC4::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC4::Node& var) return res; } -poly::UPolynomial as_poly_upolynomial_impl(const CVC4::Node& n, +poly::UPolynomial as_poly_upolynomial_impl(const CVC5::Node& n, poly::Integer& denominator, - const CVC4::Node& var) + const CVC5::Node& var) { denominator = poly::Integer(1); if (n.isVar()) @@ -140,14 +140,14 @@ poly::UPolynomial as_poly_upolynomial_impl(const CVC4::Node& n, return poly::UPolynomial(); } -poly::UPolynomial as_poly_upolynomial(const CVC4::Node& n, - const CVC4::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 CVC4::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 CVC4::Node& n, } return poly::Polynomial(); } -poly::Polynomial as_poly_polynomial(const CVC4::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 CVC4::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 -CVC4::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 @@ CVC4::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm) return cmd.d_nm->mkNode(Kind::PLUS, cmd.d_terms); } -poly::SignCondition normalize_kind(CVC4::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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 47a66d5f1..9adc9a996 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -42,23 +42,23 @@ namespace nl { struct VariableMapper { /** A mapping from CVC4 variables to poly variables. */ - std::map<CVC4::Node, poly::Variable> mVarCVCpoly; + std::map<CVC5::Node, poly::Variable> mVarCVCpoly; /** A mapping from poly variables to CVC4 variables. */ - std::map<poly::Variable, CVC4::Node> mVarpolyCVC; + std::map<poly::Variable, CVC5::Node> mVarpolyCVC; /** Retrieves the according poly variable. */ - poly::Variable operator()(const CVC4::Node& n); + poly::Variable operator()(const CVC5::Node& n); /** Retrieves the according CVC4 variable. */ - CVC4::Node operator()(const poly::Variable& n); + CVC5::Node operator()(const poly::Variable& n); }; -/** Convert a poly univariate polynomial to a CVC4::Node. */ -CVC4::Node as_cvc_upolynomial(const poly::UPolynomial& p, - const CVC4::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 CVC4::Node to a poly univariate polynomial. */ -poly::UPolynomial as_poly_upolynomial(const CVC4::Node& n, - const CVC4::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 CVC4::Node& n, * in the context of ICP) the second overload provides the denominator in the * third argument. */ -poly::Polynomial as_poly_polynomial(const CVC4::Node& n, VariableMapper& vm); -poly::Polynomial as_poly_polynomial(const CVC4::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 CVC4::Node& n, * multiplications with one or use NONLINEAR_MULT where regular MULT may be * sufficient), so it may be sensible to rewrite it afterwards. */ -CVC4::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 CVC4 +} // namespace CVC5 #endif diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp index c707dd9bc..92cebc8fc 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -38,4 +38,4 @@ NlStats::~NlStats() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index 94e1882b3..66157d0a3 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -44,6 +44,6 @@ class NlStats } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 5d6eeea9e..af23f67f9 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -173,4 +173,4 @@ StepGenerator Strategy::getStrategy() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index 3540f9ad1..9caf6322b 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -18,7 +18,7 @@ #include <iosfwd> #include <vector> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -173,6 +173,6 @@ class Strategy } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 8b6f4484d..05849a579 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index 484174d5f..8bd00c456 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -108,6 +108,6 @@ class ExponentialSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 223db8355..fe071c36a 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -402,4 +402,4 @@ Node TranscendentalProofRuleChecker::checkInternal( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h index b00c1811c..2a6837590 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -53,6 +53,6 @@ class TranscendentalProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 528e0bea2..052b6c056 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index c628559fc..c20c50f6d 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -175,6 +175,6 @@ class SineSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 ced202308..f2817344a 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index 7cb03cd7c..b13be57f0 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -118,6 +118,6 @@ class TaylorGenerator } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 f236b472a..bedfe4d3b 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index 290e74322..e22bf3e64 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -200,6 +200,6 @@ class TranscendentalSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 593354794..6ab136d39 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 CVC4 { +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 CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index cd5466e89..21a60e038 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 CVC4 { +namespace CVC5 { class CDProof; namespace theory { namespace arith { @@ -278,6 +278,6 @@ struct TranscendentalState } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 537a39a77..d1ef6486e 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -24,7 +24,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -1412,4 +1412,4 @@ bool Polynomial::isNonlinear() const { } //namespace arith } //namespace theory -} //namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index c3500e699..c4d0e2268 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -28,8 +28,7 @@ #include "theory/arith/delta_rational.h" #include "util/rational.h" - -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -1403,8 +1402,8 @@ public: };/* class Comparison */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 ee15e0f11..15e09eaa5 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -499,4 +499,4 @@ Node OperatorElim::mkWitnessTerm(Node v, } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 489974eac..fa09ad26b 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 CVC4 { +namespace CVC5 { class TConvProofGenerator; @@ -142,4 +142,4 @@ class OperatorElim : public EagerProofGenerator } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 32c61e815..6e4fa6bed 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -22,7 +22,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -684,6 +684,6 @@ void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){ d_pm->popUpperBound(p); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index af0fe37ec..b7a1a0efe 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 CVC4 { +namespace CVC5 { namespace context { class Context; } @@ -412,9 +412,8 @@ private: };/* class ArithVariables */ - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 c595791ab..09ef5bf34 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -360,4 +360,4 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, } } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h index 0745bdd61..5b9a50387 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -43,6 +43,6 @@ class ArithProofRuleChecker : public ProofRuleChecker } // namespace arith } // namespace theory -} // namespace CVC4 +} // 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 d453285d6..169e4e2db 100644 --- a/src/theory/arith/proof_macros.h +++ b/src/theory/arith/proof_macros.h @@ -20,12 +20,12 @@ #include "options/smt_options.h" -#define ARITH_PROOF(x) \ - if (CVC4::options::produceProofs()) \ - { \ - x; \ +#define ARITH_PROOF(x) \ + if (CVC5::options::produceProofs()) \ + { \ + x; \ } -#define ARITH_NULLPROOF(x) (CVC4::options::produceProofs()) ? x : NULL -#define ARITH_PROOF_ON() CVC4::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 f2eef7013..9522ef4f4 100644 --- a/src/theory/arith/rewrites.cpp +++ b/src/theory/arith/rewrites.cpp @@ -16,7 +16,7 @@ #include <iostream> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -47,4 +47,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r) } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h index 6b5e8fc9f..250eacb09 100644 --- a/src/theory/arith/rewrites.h +++ b/src/theory/arith/rewrites.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -77,6 +77,6 @@ std::ostream& operator<<(std::ostream& out, Rewrite r); } // namespace arith } // namespace theory -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__THEORY__ARITH__REWRITES_H */ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 49267034c..fe6fad4d7 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -278,6 +278,6 @@ SimplexDecisionProcedure::sgn_table::const_iterator SimplexDecisionProcedure::fi pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn)); return sgns.find(p); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 5edfc1608..a1ee18adf 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -219,6 +219,6 @@ protected: };/* class SimplexDecisionProcedure */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp index 98bf07ccf..ea868a886 100644 --- a/src/theory/arith/simplex_update.cpp +++ b/src/theory/arith/simplex_update.cpp @@ -19,7 +19,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -186,6 +186,6 @@ std::ostream& operator<<(std::ostream& out, WitnessImprovement w){ return out; } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index f8a6bf957..833e92dd4 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -352,6 +352,6 @@ private: std::ostream& operator<<(std::ostream& out, const UpdateInfo& up); -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index eef0ede43..0efc33d02 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -1022,6 +1022,6 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){ } } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index d9d11dcc5..16af7292d 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -240,6 +240,6 @@ private: } d_statistics; };/* class FCSimplexDecisionProcedure */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 1d57a40dd..c39b3aae7 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -190,6 +190,6 @@ void Tableau::printBasicRow(ArithVar basic, std::ostream& out){ printRow(basicToRowIndex(basic), out); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 9ee33d7b6..0834c7f35 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -157,8 +157,6 @@ private: };/* class Tableau */ - - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp index 4b699a019..a167cf1a8 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -31,6 +31,6 @@ uint32_t TableauSizes::getColumnLength(ArithVar x) const { return d_tab->getColLength(x); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h index 16e58bb2e..3bbb5c818 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -37,7 +37,6 @@ public: uint32_t getColumnLength(ArithVar x) const; }; /* TableauSizes */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index a179336af..12603ea7d 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -311,6 +311,6 @@ eq::ProofEqEngine* TheoryArith::getProofEqEngine() return d_im.getProofEqEngine(); } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e0fa1b2d0..e430f6da6 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { namespace nl { @@ -163,6 +163,6 @@ class TheoryArith : public Theory { };/* class TheoryArith */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index b85aeb135..1e9e8ca3f 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 CVC4::kind; +using namespace CVC5::kind; -namespace CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -5712,6 +5712,6 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg // return result; // } -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 4b2fcf8a8..e0b7cea56 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 CVC4 { +namespace CVC5 { namespace theory { class EagerProofGenerator; @@ -884,6 +884,6 @@ private: Statistics d_statistics; };/* class TheoryArithPrivate */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index fbf31e6e2..dc8885e55 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -157,8 +157,8 @@ class IndexedRootPredicateTypeRule } }; /* class IndexedRootPredicateTypeRule */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // 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 a9e35cdc3..a32073ad9 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 CVC4 { +namespace CVC5 { namespace theory { namespace arith { @@ -100,8 +100,8 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> { bool isFinished() override { return false; } };/* class IntegerEnumerator */ -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace arith +} // namespace theory +} // namespace CVC5 #endif /* CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */ |