From f37078447757601cf24eb3ee92970f275a434d82 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Apr 2022 13:05:12 -0500 Subject: [PATCH] Move linear arithmetic solver to theory::arith::linear (#8628) This moves the current linear arithmetic solver to src/theory/arith/linear, and inside `cvc5::internal::theory::arith::linear`. Some code uses internal utilities from `arith::linear`, although this should be minimized. This is preparation for breaking dependencies with the old code. --- src/CMakeLists.txt | 96 +++++++++---------- .../passes/pseudo_boolean_processor.cpp | 12 +-- src/theory/arith/arith_ite_utils.cpp | 22 ++--- src/theory/arith/arith_rewriter.cpp | 1 - src/theory/arith/arith_rewriter.h | 1 - src/theory/arith/arith_state.cpp | 4 +- src/theory/arith/arith_state.h | 6 +- src/theory/arith/arith_utilities.h | 5 - src/theory/arith/bound_inference.cpp | 4 +- .../arith/{ => linear}/approx_simplex.cpp | 20 ++-- .../arith/{ => linear}/approx_simplex.h | 4 +- .../{ => linear}/arith_static_learner.cpp | 6 +- .../arith/{ => linear}/arith_static_learner.h | 2 +- src/theory/arith/{ => linear}/arithvar.cpp | 4 +- src/theory/arith/{ => linear}/arithvar.h | 2 +- .../arith/{ => linear}/arithvar_node_map.h | 8 +- .../{ => linear}/attempt_solution_simplex.cpp | 12 +-- .../{ => linear}/attempt_solution_simplex.h | 6 +- src/theory/arith/{ => linear}/bound_counts.h | 4 +- src/theory/arith/{ => linear}/callbacks.cpp | 6 +- src/theory/arith/{ => linear}/callbacks.h | 8 +- .../arith/{ => linear}/congruence_manager.cpp | 8 +- .../arith/{ => linear}/congruence_manager.h | 9 +- src/theory/arith/{ => linear}/constraint.cpp | 10 +- src/theory/arith/{ => linear}/constraint.h | 8 +- .../arith/{ => linear}/constraint_forward.h | 2 +- src/theory/arith/{ => linear}/cut_log.cpp | 10 +- src/theory/arith/{ => linear}/cut_log.h | 6 +- src/theory/arith/{ => linear}/dio_solver.cpp | 6 +- src/theory/arith/{ => linear}/dio_solver.h | 4 +- .../arith/{ => linear}/dual_simplex.cpp | 10 +- src/theory/arith/{ => linear}/dual_simplex.h | 4 +- src/theory/arith/{ => linear}/error_set.cpp | 6 +- src/theory/arith/{ => linear}/error_set.h | 12 +-- src/theory/arith/{ => linear}/fc_simplex.cpp | 8 +- src/theory/arith/{ => linear}/fc_simplex.h | 10 +- .../arith/{ => linear}/infer_bounds.cpp | 4 +- src/theory/arith/{ => linear}/infer_bounds.h | 2 +- .../arith/{ => linear}/linear_equality.cpp | 6 +- .../arith/{ => linear}/linear_equality.h | 12 +-- src/theory/arith/{ => linear}/matrix.cpp | 4 +- src/theory/arith/{ => linear}/matrix.h | 8 +- src/theory/arith/{ => linear}/normal_form.cpp | 4 +- src/theory/arith/{ => linear}/normal_form.h | 2 +- .../arith/{ => linear}/partial_model.cpp | 8 +- src/theory/arith/{ => linear}/partial_model.h | 11 ++- src/theory/arith/{ => linear}/simplex.cpp | 12 +-- src/theory/arith/{ => linear}/simplex.h | 6 +- .../arith/{ => linear}/simplex_update.cpp | 6 +- .../arith/{ => linear}/simplex_update.h | 6 +- src/theory/arith/{ => linear}/soi_simplex.cpp | 10 +- src/theory/arith/{ => linear}/soi_simplex.h | 8 +- src/theory/arith/{ => linear}/tableau.cpp | 4 +- src/theory/arith/{ => linear}/tableau.h | 6 +- .../arith/{ => linear}/tableau_sizes.cpp | 6 +- src/theory/arith/{ => linear}/tableau_sizes.h | 4 +- .../{ => linear}/theory_arith_private.cpp | 38 ++++---- .../arith/{ => linear}/theory_arith_private.h | 37 +++---- src/theory/arith/nl/icp/icp_solver.cpp | 4 +- src/theory/arith/proof_checker.cpp | 3 +- src/theory/arith/theory_arith.cpp | 12 +-- src/theory/arith/theory_arith.h | 7 +- .../cegqi/ceg_arith_instantiator.cpp | 4 +- 63 files changed, 291 insertions(+), 289 deletions(-) rename src/theory/arith/{ => linear}/approx_simplex.cpp (99%) rename src/theory/arith/{ => linear}/approx_simplex.h (98%) rename src/theory/arith/{ => linear}/arith_static_learner.cpp (98%) rename src/theory/arith/{ => linear}/arith_static_learner.h (98%) rename src/theory/arith/{ => linear}/arithvar.cpp (93%) rename src/theory/arith/{ => linear}/arithvar.h (98%) rename src/theory/arith/{ => linear}/arithvar_node_map.h (91%) rename src/theory/arith/{ => linear}/attempt_solution_simplex.cpp (94%) rename src/theory/arith/{ => linear}/attempt_solution_simplex.h (96%) rename src/theory/arith/{ => linear}/bound_counts.h (99%) rename src/theory/arith/{ => linear}/callbacks.cpp (97%) rename src/theory/arith/{ => linear}/callbacks.h (96%) rename src/theory/arith/{ => linear}/congruence_manager.cpp (99%) rename src/theory/arith/{ => linear}/congruence_manager.h (97%) rename src/theory/arith/{ => linear}/constraint.cpp (99%) rename src/theory/arith/{ => linear}/constraint.h (99%) rename src/theory/arith/{ => linear}/constraint_forward.h (98%) rename src/theory/arith/{ => linear}/cut_log.cpp (98%) rename src/theory/arith/{ => linear}/cut_log.h (98%) rename src/theory/arith/{ => linear}/dio_solver.cpp (99%) rename src/theory/arith/{ => linear}/dio_solver.h (99%) rename src/theory/arith/{ => linear}/dual_simplex.cpp (97%) rename src/theory/arith/{ => linear}/dual_simplex.h (98%) rename src/theory/arith/{ => linear}/error_set.cpp (99%) rename src/theory/arith/{ => linear}/error_set.h (97%) rename src/theory/arith/{ => linear}/fc_simplex.cpp (99%) rename src/theory/arith/{ => linear}/fc_simplex.h (97%) rename src/theory/arith/{ => linear}/infer_bounds.cpp (98%) rename src/theory/arith/{ => linear}/infer_bounds.h (99%) rename src/theory/arith/{ => linear}/linear_equality.cpp (99%) rename src/theory/arith/{ => linear}/linear_equality.h (98%) rename src/theory/arith/{ => linear}/matrix.cpp (93%) rename src/theory/arith/{ => linear}/matrix.h (99%) rename src/theory/arith/{ => linear}/normal_form.cpp (99%) rename src/theory/arith/{ => linear}/normal_form.h (99%) rename src/theory/arith/{ => linear}/partial_model.cpp (99%) rename src/theory/arith/{ => linear}/partial_model.h (97%) rename src/theory/arith/{ => linear}/simplex.cpp (97%) rename src/theory/arith/{ => linear}/simplex.h (98%) rename src/theory/arith/{ => linear}/simplex_update.cpp (97%) rename src/theory/arith/{ => linear}/simplex_update.h (98%) rename src/theory/arith/{ => linear}/soi_simplex.cpp (99%) rename src/theory/arith/{ => linear}/soi_simplex.h (98%) rename src/theory/arith/{ => linear}/tableau.cpp (98%) rename src/theory/arith/{ => linear}/tableau.h (97%) rename src/theory/arith/{ => linear}/tableau_sizes.cpp (89%) rename src/theory/arith/{ => linear}/tableau_sizes.h (93%) rename src/theory/arith/{ => linear}/theory_arith_private.cpp (99%) rename src/theory/arith/{ => linear}/theory_arith_private.h (97%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8cf8d516e..f414db97d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -349,8 +349,6 @@ libcvc5_add_sources( smt/witness_form.h smt_util/boolean_simplification.cpp smt_util/boolean_simplification.h - theory/arith/approx_simplex.cpp - theory/arith/approx_simplex.h theory/arith/arith_evaluator.cpp theory/arith/arith_evaluator.h theory/arith/arith_ite_utils.cpp @@ -365,48 +363,66 @@ libcvc5_add_sources( theory/arith/arith_rewriter.h theory/arith/arith_state.cpp theory/arith/arith_state.h - theory/arith/arith_static_learner.cpp - theory/arith/arith_static_learner.h theory/arith/arith_utilities.cpp theory/arith/arith_utilities.h - theory/arith/arithvar.cpp - theory/arith/arithvar.h - theory/arith/attempt_solution_simplex.cpp - theory/arith/attempt_solution_simplex.h - theory/arith/bound_counts.h theory/arith/bound_inference.cpp theory/arith/bound_inference.h theory/arith/branch_and_bound.cpp theory/arith/branch_and_bound.h - theory/arith/callbacks.cpp - theory/arith/callbacks.h - theory/arith/congruence_manager.cpp - theory/arith/congruence_manager.h - theory/arith/constraint.cpp - theory/arith/constraint.h - theory/arith/constraint_forward.h - theory/arith/cut_log.cpp - theory/arith/cut_log.h theory/arith/delta_rational.cpp theory/arith/delta_rational.h - theory/arith/dio_solver.cpp - theory/arith/dio_solver.h - theory/arith/dual_simplex.cpp - theory/arith/dual_simplex.h theory/arith/equality_solver.cpp theory/arith/equality_solver.h - theory/arith/error_set.cpp - theory/arith/error_set.h - theory/arith/fc_simplex.cpp - theory/arith/fc_simplex.h - theory/arith/infer_bounds.cpp - theory/arith/infer_bounds.h theory/arith/inference_manager.cpp theory/arith/inference_manager.h - theory/arith/linear_equality.cpp - theory/arith/linear_equality.h - theory/arith/matrix.cpp - theory/arith/matrix.h + theory/arith/linear/approx_simplex.cpp + theory/arith/linear/approx_simplex.h + theory/arith/linear/arith_static_learner.cpp + theory/arith/linear/arith_static_learner.h + theory/arith/linear/arithvar.cpp + theory/arith/linear/arithvar.h + theory/arith/linear/attempt_solution_simplex.cpp + theory/arith/linear/attempt_solution_simplex.h + theory/arith/linear/bound_counts.h + theory/arith/linear/callbacks.cpp + theory/arith/linear/callbacks.h + theory/arith/linear/congruence_manager.cpp + theory/arith/linear/congruence_manager.h + theory/arith/linear/constraint.cpp + theory/arith/linear/constraint.h + theory/arith/linear/constraint_forward.h + theory/arith/linear/cut_log.cpp + theory/arith/linear/cut_log.h + theory/arith/linear/dio_solver.cpp + theory/arith/linear/dio_solver.h + theory/arith/linear/dual_simplex.cpp + theory/arith/linear/dual_simplex.h + theory/arith/linear/error_set.cpp + theory/arith/linear/error_set.h + theory/arith/linear/fc_simplex.cpp + theory/arith/linear/fc_simplex.h + theory/arith/linear/infer_bounds.cpp + theory/arith/linear/infer_bounds.h + theory/arith/linear/linear_equality.cpp + theory/arith/linear/linear_equality.h + theory/arith/linear/matrix.cpp + theory/arith/linear/matrix.h + theory/arith/linear/normal_form.cpp + theory/arith/linear/normal_form.h + theory/arith/linear/partial_model.cpp + theory/arith/linear/partial_model.h + theory/arith/linear/simplex.cpp + theory/arith/linear/simplex.h + theory/arith/linear/simplex_update.cpp + theory/arith/linear/simplex_update.h + theory/arith/linear/soi_simplex.cpp + theory/arith/linear/soi_simplex.h + theory/arith/linear/tableau.cpp + theory/arith/linear/tableau.h + theory/arith/linear/tableau_sizes.cpp + theory/arith/linear/tableau_sizes.h + theory/arith/linear/theory_arith_private.cpp + theory/arith/linear/theory_arith_private.h theory/arith/nl/coverings_solver.cpp theory/arith/nl/coverings_solver.h theory/arith/nl/coverings/cdcac.cpp @@ -487,12 +503,8 @@ libcvc5_add_sources( theory/arith/nl/transcendental/transcendental_solver.h theory/arith/nl/transcendental/transcendental_state.cpp theory/arith/nl/transcendental/transcendental_state.h - theory/arith/normal_form.cpp - theory/arith/normal_form.h theory/arith/operator_elim.cpp theory/arith/operator_elim.h - theory/arith/partial_model.cpp - theory/arith/partial_model.h theory/arith/pp_rewrite_eq.cpp theory/arith/pp_rewrite_eq.h theory/arith/proof_checker.cpp @@ -506,20 +518,8 @@ libcvc5_add_sources( theory/arith/rewriter/rewrite_atom.h theory/arith/rewrites.cpp theory/arith/rewrites.h - theory/arith/simplex.cpp - theory/arith/simplex.h - theory/arith/simplex_update.cpp - theory/arith/simplex_update.h - theory/arith/soi_simplex.cpp - theory/arith/soi_simplex.h - theory/arith/tableau.cpp - theory/arith/tableau.h - theory/arith/tableau_sizes.cpp - theory/arith/tableau_sizes.h theory/arith/theory_arith.cpp theory/arith/theory_arith.h - theory/arith/theory_arith_private.cpp - theory/arith/theory_arith_private.h theory/arith/theory_arith_type_rules.cpp theory/arith/theory_arith_type_rules.h theory/arith/type_enumerator.h diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index e680dc4b5..a3ceddeb9 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -22,7 +22,7 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/normal_form.h" #include "theory/rewriter.h" namespace cvc5::internal { @@ -78,13 +78,13 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated) return false; } - if (!Polynomial::isMember(l)) + if (!linear::Polynomial::isMember(l)) { Trace("pbs::rewrites") << "not polynomial" << assertion << std::endl; return false; } - Polynomial p = Polynomial::parsePolynomial(l); + linear::Polynomial p = linear::Polynomial::parsePolynomial(l); clear(); if (negated) { @@ -112,9 +112,9 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated) Assert(d_off.value().isIntegral()); int adj = negated ? -1 : 1; - for (Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i) + for (linear::Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i) { - Monomial m = *i; + linear::Monomial m = *i; const Rational& coeff = m.getConstant().getValue(); if (!(coeff.isOne() || coeff.isNegativeOne())) { @@ -122,7 +122,7 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated) } Assert(coeff.sgn() != 0); - const VarList& vl = m.getVarList(); + const linear::VarList& vl = m.getVarList(); Node v = vl.getNode(); if (!isPseudoBoolean(v)) diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 6bf79b4ea..ee79b8375 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -26,7 +26,7 @@ #include "preprocessing/util/ite_utilities.h" #include "smt/env.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/normal_form.h" #include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/theory_model.h" @@ -102,7 +102,7 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ default: { TypeNode tn = n.getType(); - if (tn.isRealOrInt() && Polynomial::isMember(n)) + if (tn.isRealOrInt() && linear::Polynomial::isMember(n)) { Node newn = Node::null(); if(!d_contains.containsTermITE(n)){ @@ -110,12 +110,12 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ }else if(n.getNumChildren() > 0){ newn = applyReduceVariablesInItes(n); newn = rewrite(newn); - Assert(Polynomial::isMember(newn)); + Assert(linear::Polynomial::isMember(newn)); }else{ newn = n; } NodeManager* nm = NodeManager::currentNM(); - Polynomial p = Polynomial::parsePolynomial(newn); + linear::Polynomial p = linear::Polynomial::parsePolynomial(newn); if(p.isConstant()){ d_constants[n] = newn; d_varParts[n] = nm->mkConstRealOrInt(tn, Rational(0)); @@ -127,7 +127,7 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ d_reduceVar[n] = p.getNode(); return p.getNode(); }else{ - Monomial mc = p.getHead(); + linear::Monomial mc = p.getHead(); d_constants[n] = mc.getConstant().getNode(); d_varParts[n] = p.getTail().getNode(); d_reduceVar[n] = newn; @@ -444,12 +444,12 @@ bool ArithIteUtils::solveBinOr(TNode binor){ Node useForCmpL = selectForCmp(otherL); Node useForCmpR = selectForCmp(otherR); - Assert(Polynomial::isMember(sel)); - Assert(Polynomial::isMember(useForCmpL)); - Assert(Polynomial::isMember(useForCmpR)); - Polynomial lside = Polynomial::parsePolynomial( useForCmpL ); - Polynomial rside = Polynomial::parsePolynomial( useForCmpR ); - Polynomial diff = lside-rside; + Assert(linear::Polynomial::isMember(sel)); + Assert(linear::Polynomial::isMember(useForCmpL)); + Assert(linear::Polynomial::isMember(useForCmpR)); + linear::Polynomial lside = linear::Polynomial::parsePolynomial( useForCmpL ); + linear::Polynomial rside = linear::Polynomial::parsePolynomial( useForCmpR ); + linear::Polynomial diff = lside-rside; Trace("arith::ite") << "diff: " << diff.getNode() << endl; if(diff.isConstant()){ diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 8add0b5ec..b32d488a2 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -28,7 +28,6 @@ #include "smt/logic_exception.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/normal_form.h" #include "theory/arith/operator_elim.h" #include "theory/arith/rewriter/addition.h" #include "theory/arith/rewriter/node_utils.h" diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index e74790d26..0f2a55f84 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -13,7 +13,6 @@ * Rewriter for the theory of arithmetic. * * This rewrites to the normal form for arithmetic. - * See theory/arith/normal_form.h for more information. */ #include "cvc5_private.h" diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp index 86088cc06..315551b4e 100644 --- a/src/theory/arith/arith_state.cpp +++ b/src/theory/arith/arith_state.cpp @@ -15,7 +15,7 @@ #include "theory/arith/arith_state.h" -#include "theory/arith/theory_arith_private.h" +#include "theory/arith/linear/theory_arith_private.h" namespace cvc5::internal { namespace theory { @@ -31,7 +31,7 @@ bool ArithState::isInConflict() const return d_parent->anyConflict() || d_conflict; } -void ArithState::setParent(TheoryArithPrivate* p) { d_parent = p; } +void ArithState::setParent(linear::TheoryArithPrivate* p) { d_parent = p; } } // namespace arith } // namespace theory diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h index 3df2d68b0..2fffb8cc5 100644 --- a/src/theory/arith/arith_state.h +++ b/src/theory/arith/arith_state.h @@ -24,7 +24,9 @@ namespace cvc5::internal { namespace theory { namespace arith { +namespace linear { class TheoryArithPrivate; +} /** * The arithmetic state. @@ -44,11 +46,11 @@ class ArithState : public TheoryState /** Are we currently in conflict? */ bool isInConflict() const override; /** Set parent */ - void setParent(TheoryArithPrivate* p); + void setParent(linear::TheoryArithPrivate* p); private: /** reference to parent */ - TheoryArithPrivate* d_parent; + linear::TheoryArithPrivate* d_parent; }; } // namespace arith diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 0f85468a2..7f4398b9b 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -25,7 +25,6 @@ #include "context/cdhashset.h" #include "expr/node.h" #include "expr/subs.h" -#include "theory/arith/arithvar.h" #include "util/dense_map.h" #include "util/integer.h" #include "util/rational.h" @@ -39,10 +38,6 @@ typedef std::unordered_set NodeSet; typedef std::unordered_set TNodeSet; typedef context::CDHashSet CDNodeSet; -//Maps from Nodes -> ArithVars, and vice versa -typedef std::unordered_map NodeToArithVarMap; -typedef DenseMap ArithVarToNodeMap; - inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL, q); } diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp index 68b3a7b2a..3ec622dcf 100644 --- a/src/theory/arith/bound_inference.cpp +++ b/src/theory/arith/bound_inference.cpp @@ -16,7 +16,7 @@ #include "theory/arith/bound_inference.h" #include "smt/env.h" -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/normal_form.h" #include "theory/rewriter.h" using namespace cvc5::internal::kind; @@ -62,7 +62,7 @@ bool BoundInference::add(const Node& n, bool onlyVariables) return false; } // Parse the node as a comparison - auto comp = Comparison::parseNormalForm(tmp); + auto comp = linear::Comparison::parseNormalForm(tmp); auto dec = comp.decompose(true); if (onlyVariables && !std::get<0>(dec).isVariable()) { diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/linear/approx_simplex.cpp similarity index 99% rename from src/theory/arith/approx_simplex.cpp rename to src/theory/arith/linear/approx_simplex.cpp index 0c8f4506a..81c6183f1 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/linear/approx_simplex.cpp @@ -15,7 +15,7 @@ * [[ Add lengthier description here ]] * \todo document this file */ -#include "theory/arith/approx_simplex.h" +#include "theory/arith/linear/approx_simplex.h" #include @@ -27,20 +27,20 @@ #include "base/output.h" #include "proof/eager_proof_generator.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/constraint.h" -#include "theory/arith/cut_log.h" -#include "theory/arith/matrix.h" -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/cut_log.h" +#include "theory/arith/linear/matrix.h" +#include "theory/arith/linear/normal_form.h" #ifdef CVC5_USE_GLPK -#include "theory/arith/partial_model.h" +#include "theory/arith/linear/partial_model.h" #endif using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { struct AuxInfo { TreeLog* tl; @@ -365,7 +365,7 @@ extern "C" { namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { Kind glpk_type_to_kind(int glpk_cut_type){ switch(glpk_cut_type){ @@ -524,7 +524,7 @@ private: /* Begin GPLK/NOGLPK Glue code. */ namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { ApproximateSimplex* ApproximateSimplex::mkApproximateSimplexSolver(const ArithVariables& vars, TreeLog& l, ApproximateStatistics& s){ #ifdef CVC5_USE_GLPK return new ApproxGLPK(vars, l, s); @@ -548,7 +548,7 @@ bool ApproximateSimplex::enabled() { #ifdef CVC5_USE_GLPK namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { #ifdef CVC5_ASSERTIONS static CutInfoKlass fromGlpkClass(int klass){ diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/linear/approx_simplex.h similarity index 98% rename from src/theory/arith/approx_simplex.h rename to src/theory/arith/linear/approx_simplex.h index 0b4bc2cd3..feac8156c 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/linear/approx_simplex.h @@ -23,7 +23,7 @@ #include #include -#include "theory/arith/arithvar.h" +#include "theory/arith/linear/arithvar.h" #include "theory/arith/delta_rational.h" #include "util/dense_map.h" #include "util/rational.h" @@ -31,7 +31,7 @@ namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { enum LinResult { LinUnknown, /* Unknown error */ diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/linear/arith_static_learner.cpp similarity index 98% rename from src/theory/arith/arith_static_learner.cpp rename to src/theory/arith/linear/arith_static_learner.cpp index f45f5977a..c07359b51 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/linear/arith_static_learner.cpp @@ -22,17 +22,15 @@ #include "expr/node_algorithm.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/arith_static_learner.h" +#include "theory/arith/linear/arith_static_learner.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/normal_form.h" -#include "theory/rewriter.h" using namespace std; using namespace cvc5::internal::kind; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { ArithStaticLearner::ArithStaticLearner(context::Context* userContext) : d_minMap(userContext), d_maxMap(userContext), d_statistics() diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/linear/arith_static_learner.h similarity index 98% rename from src/theory/arith/arith_static_learner.h rename to src/theory/arith/linear/arith_static_learner.h index 1ac8d7ce5..c07681b45 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/linear/arith_static_learner.h @@ -32,7 +32,7 @@ class Context; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class ArithStaticLearner { private: diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/linear/arithvar.cpp similarity index 93% rename from src/theory/arith/arithvar.cpp rename to src/theory/arith/linear/arithvar.cpp index d83fe2b03..2cebf540b 100644 --- a/src/theory/arith/arithvar.cpp +++ b/src/theory/arith/linear/arithvar.cpp @@ -16,13 +16,13 @@ * \todo document this file */ -#include "theory/arith/arithvar.h" +#include "theory/arith/linear/arithvar.h" #include #include namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { const ArithVar ARITHVAR_SENTINEL = std::numeric_limits::max(); diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/linear/arithvar.h similarity index 98% rename from src/theory/arith/arithvar.h rename to src/theory/arith/linear/arithvar.h index 33eb19631..f7679413e 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/linear/arithvar.h @@ -29,7 +29,7 @@ namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { typedef Index ArithVar; extern const ArithVar ARITHVAR_SENTINEL; diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/linear/arithvar_node_map.h similarity index 91% rename from src/theory/arith/arithvar_node_map.h rename to src/theory/arith/linear/arithvar_node_map.h index 85a962758..067d990d4 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/linear/arithvar_node_map.h @@ -21,7 +21,7 @@ #ifndef CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H #define CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H -#include "theory/arith/arithvar.h" +#include "theory/arith/linear/arithvar.h" #include "context/context.h" #include "context/cdlist.h" #include "context/cdhashmap.h" @@ -29,7 +29,11 @@ namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { + +//Maps from Nodes -> ArithVars, and vice versa +typedef std::unordered_map NodeToArithVarMap; +typedef DenseMap ArithVarToNodeMap; class ArithVarNodeMap { private: diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/linear/attempt_solution_simplex.cpp similarity index 94% rename from src/theory/arith/attempt_solution_simplex.cpp rename to src/theory/arith/linear/attempt_solution_simplex.cpp index ed35dad74..7ded87711 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/linear/attempt_solution_simplex.cpp @@ -15,21 +15,21 @@ * [[ Add lengthier description here ]] * \todo document this file */ -#include "theory/arith/attempt_solution_simplex.h" +#include "theory/arith/linear/attempt_solution_simplex.h" #include "base/output.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/constraint.h" -#include "theory/arith/error_set.h" -#include "theory/arith/linear_equality.h" -#include "theory/arith/tableau.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/error_set.h" +#include "theory/arith/linear/linear_equality.h" +#include "theory/arith/linear/tableau.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { AttemptSolutionSDP::AttemptSolutionSDP(Env& env, LinearEqualityModule& linEq, diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/linear/attempt_solution_simplex.h similarity index 96% rename from src/theory/arith/attempt_solution_simplex.h rename to src/theory/arith/linear/attempt_solution_simplex.h index 43c6f718d..1e3682be0 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/linear/attempt_solution_simplex.h @@ -55,13 +55,13 @@ #pragma once -#include "theory/arith/approx_simplex.h" -#include "theory/arith/simplex.h" +#include "theory/arith/linear/approx_simplex.h" +#include "theory/arith/linear/simplex.h" #include "util/statistics_stats.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class AttemptSolutionSDP : public SimplexDecisionProcedure { public: diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/linear/bound_counts.h similarity index 99% rename from src/theory/arith/bound_counts.h rename to src/theory/arith/linear/bound_counts.h index bef547d75..3524e1cb2 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/linear/bound_counts.h @@ -20,12 +20,12 @@ #pragma once #include "base/check.h" -#include "theory/arith/arithvar.h" +#include "theory/arith/linear/arithvar.h" #include "util/dense_map.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class BoundCounts { private: diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/linear/callbacks.cpp similarity index 97% rename from src/theory/arith/callbacks.cpp rename to src/theory/arith/linear/callbacks.cpp index fb38ac0cd..87b022cf6 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/linear/callbacks.cpp @@ -16,15 +16,15 @@ * \todo document this file */ -#include "theory/arith/callbacks.h" +#include "theory/arith/linear/callbacks.h" #include "expr/skolem_manager.h" #include "proof/proof_node.h" -#include "theory/arith/theory_arith_private.h" +#include "theory/arith/linear/theory_arith_private.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta) : d_arith(ta) diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/linear/callbacks.h similarity index 96% rename from src/theory/arith/callbacks.h rename to src/theory/arith/linear/callbacks.h index 976cdf6b0..c93db91ca 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/linear/callbacks.h @@ -19,9 +19,9 @@ #pragma once #include "expr/node.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/bound_counts.h" -#include "theory/arith/constraint_forward.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/bound_counts.h" +#include "theory/arith/linear/constraint_forward.h" #include "theory/inference_id.h" #include "util/rational.h" @@ -30,7 +30,7 @@ namespace cvc5::internal { class ProofNode; namespace theory { -namespace arith { +namespace arith::linear { class TheoryArithPrivate; diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/linear/congruence_manager.cpp similarity index 99% rename from src/theory/arith/congruence_manager.cpp rename to src/theory/arith/linear/congruence_manager.cpp index a9a096200..da4d81aa7 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/linear/congruence_manager.cpp @@ -16,7 +16,7 @@ * \todo document this file */ -#include "theory/arith/congruence_manager.h" +#include "theory/arith/linear/congruence_manager.h" #include "base/output.h" #include "options/arith_options.h" @@ -25,8 +25,8 @@ #include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/constraint.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/partial_model.h" #include "theory/ee_setup_info.h" #include "theory/rewriter.h" #include "theory/uf/equality_engine.h" @@ -36,7 +36,7 @@ using namespace cvc5::internal::kind; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { ArithCongruenceManager::ArithCongruenceManager( Env& env, diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/linear/congruence_manager.h similarity index 97% rename from src/theory/arith/congruence_manager.h rename to src/theory/arith/linear/congruence_manager.h index 1cacb9431..c9dfb158d 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/linear/congruence_manager.h @@ -27,9 +27,10 @@ #include "proof/trust_node.h" #include "smt/env_obj.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/callbacks.h" -#include "theory/arith/constraint_forward.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/arithvar_node_map.h" +#include "theory/arith/linear/callbacks.h" +#include "theory/arith/linear/constraint_forward.h" #include "theory/uf/equality_engine_notify.h" #include "util/dense_map.h" #include "util/statistics_stats.h" @@ -52,7 +53,7 @@ class ProofEqEngine; class EqualityEngine; } -namespace arith { +namespace arith::linear { class ArithVariables; diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/linear/constraint.cpp similarity index 99% rename from src/theory/arith/constraint.cpp rename to src/theory/arith/linear/constraint.cpp index dc1f430c8..9ed758f98 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/linear/constraint.cpp @@ -15,7 +15,7 @@ * [[ Add lengthier description here ]] * \todo document this file */ -#include "theory/arith/constraint.h" +#include "theory/arith/linear/constraint.h" #include #include @@ -28,9 +28,9 @@ #include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/congruence_manager.h" -#include "theory/arith/normal_form.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/linear/congruence_manager.h" +#include "theory/arith/linear/normal_form.h" +#include "theory/arith/linear/partial_model.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" @@ -39,7 +39,7 @@ using namespace cvc5::internal::kind; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { ConstraintRule::ConstraintRule() : d_constraint(NullConstraint), diff --git a/src/theory/arith/constraint.h b/src/theory/arith/linear/constraint.h similarity index 99% rename from src/theory/arith/constraint.h rename to src/theory/arith/linear/constraint.h index f59e8ead1..745462e4b 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/linear/constraint.h @@ -88,9 +88,9 @@ #include "expr/node.h" #include "proof/trust_node.h" #include "smt/env_obj.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/callbacks.h" -#include "theory/arith/constraint_forward.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/callbacks.h" +#include "theory/arith/linear/constraint_forward.h" #include "theory/arith/delta_rational.h" #include "util/statistics_stats.h" @@ -104,7 +104,7 @@ class EagerProofGenerator; namespace theory { -namespace arith { +namespace arith::linear { class Comparison; class ArithCongruenceManager; diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/linear/constraint_forward.h similarity index 98% rename from src/theory/arith/constraint_forward.h rename to src/theory/arith/linear/constraint_forward.h index 5b700ceeb..fa7f16c3b 100644 --- a/src/theory/arith/constraint_forward.h +++ b/src/theory/arith/linear/constraint_forward.h @@ -28,7 +28,7 @@ namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class Constraint; typedef Constraint* ConstraintP; diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/linear/cut_log.cpp similarity index 98% rename from src/theory/arith/cut_log.cpp rename to src/theory/arith/linear/cut_log.cpp index 0fc239e53..9bf3cb118 100644 --- a/src/theory/arith/cut_log.cpp +++ b/src/theory/arith/linear/cut_log.cpp @@ -16,7 +16,7 @@ * \todo document this file */ -#include "theory/arith/cut_log.h" +#include "theory/arith/linear/cut_log.h" #include #include @@ -27,16 +27,16 @@ #include "base/cvc5config.h" #include "base/output.h" -#include "theory/arith/approx_simplex.h" -#include "theory/arith/constraint.h" -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/approx_simplex.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/normal_form.h" #include "util/ostream_util.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { NodeLog::const_iterator NodeLog::begin() const { return d_cuts.begin(); } NodeLog::const_iterator NodeLog::end() const { return d_cuts.end(); } diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/linear/cut_log.h similarity index 98% rename from src/theory/arith/cut_log.h rename to src/theory/arith/linear/cut_log.h index 2cf3eac4d..bfcabc32b 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/linear/cut_log.h @@ -26,13 +26,13 @@ #include #include "expr/kind.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/constraint_forward.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/constraint_forward.h" #include "util/dense_map.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { /** A low level vector of indexed doubles. */ struct PrimitiveVec { diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/linear/dio_solver.cpp similarity index 99% rename from src/theory/arith/dio_solver.cpp rename to src/theory/arith/linear/dio_solver.cpp index 8e5f636e0..b3eede0dd 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/linear/dio_solver.cpp @@ -14,7 +14,7 @@ * * A Diophantine equation solver for the theory of arithmetic. */ -#include "theory/arith/dio_solver.h" +#include "theory/arith/linear/dio_solver.h" #include @@ -23,13 +23,13 @@ #include "options/arith_options.h" #include "smt/env.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/linear/partial_model.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { inline Node makeIntegerVariable(){ NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/linear/dio_solver.h similarity index 99% rename from src/theory/arith/dio_solver.h rename to src/theory/arith/linear/dio_solver.h index 1ac2eaadb..9887a2396 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/linear/dio_solver.h @@ -27,7 +27,7 @@ #include "context/cdo.h" #include "context/cdqueue.h" #include "smt/env_obj.h" -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/normal_form.h" #include "util/rational.h" #include "util/statistics_stats.h" @@ -36,7 +36,7 @@ class Context; } namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class DioSolver : protected EnvObj { diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/linear/dual_simplex.cpp similarity index 97% rename from src/theory/arith/dual_simplex.cpp rename to src/theory/arith/linear/dual_simplex.cpp index e43119154..3ef92bc6b 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/linear/dual_simplex.cpp @@ -13,22 +13,22 @@ * This is an implementation of the Simplex Module for the Simplex for * DPLL(T) decision procedure. */ -#include "theory/arith/dual_simplex.h" +#include "theory/arith/linear/dual_simplex.h" #include "base/output.h" #include "options/arith_options.h" #include "smt/env.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/constraint.h" -#include "theory/arith/error_set.h" -#include "theory/arith/linear_equality.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/error_set.h" +#include "theory/arith/linear/linear_equality.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { DualSimplexDecisionProcedure::DualSimplexDecisionProcedure( Env& env, diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/linear/dual_simplex.h similarity index 98% rename from src/theory/arith/dual_simplex.h rename to src/theory/arith/linear/dual_simplex.h index b4df9b4c5..1bb40e871 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/linear/dual_simplex.h @@ -55,12 +55,12 @@ #pragma once -#include "theory/arith/simplex.h" +#include "theory/arith/linear/simplex.h" #include "util/statistics_stats.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class DualSimplexDecisionProcedure : public SimplexDecisionProcedure{ public: diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/linear/error_set.cpp similarity index 99% rename from src/theory/arith/error_set.cpp rename to src/theory/arith/linear/error_set.cpp index 8a904b549..025af4136 100644 --- a/src/theory/arith/error_set.cpp +++ b/src/theory/arith/linear/error_set.cpp @@ -16,16 +16,16 @@ * \todo document this file */ -#include "theory/arith/error_set.h" +#include "theory/arith/linear/error_set.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/constraint.h" +#include "theory/arith/linear/constraint.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { ErrorInformation::ErrorInformation() : d_variable(ARITHVAR_SENTINEL), diff --git a/src/theory/arith/error_set.h b/src/theory/arith/linear/error_set.h similarity index 97% rename from src/theory/arith/error_set.h rename to src/theory/arith/linear/error_set.h index ec61ee0c8..448601b6c 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/linear/error_set.h @@ -24,18 +24,18 @@ #include #include "options/arith_options.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/bound_counts.h" -#include "theory/arith/callbacks.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/bound_counts.h" +#include "theory/arith/linear/callbacks.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/tableau_sizes.h" +#include "theory/arith/linear/partial_model.h" +#include "theory/arith/linear/tableau_sizes.h" #include "util/bin_heap.h" #include "util/statistics_stats.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { /** diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/linear/fc_simplex.cpp similarity index 99% rename from src/theory/arith/fc_simplex.cpp rename to src/theory/arith/linear/fc_simplex.cpp index a4bb076d3..9e2554109 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/linear/fc_simplex.cpp @@ -13,20 +13,20 @@ * This is an implementation of the Simplex Module for the Simplex for * DPLL(T)decision procedure. */ -#include "theory/arith/fc_simplex.h" +#include "theory/arith/linear/fc_simplex.h" #include "base/output.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/constraint.h" -#include "theory/arith/error_set.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/error_set.h" #include "util/statistics_stats.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { FCSimplexDecisionProcedure::FCSimplexDecisionProcedure( Env& env, diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/linear/fc_simplex.h similarity index 97% rename from src/theory/arith/fc_simplex.h rename to src/theory/arith/linear/fc_simplex.h index c9460916f..1d07df95a 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/linear/fc_simplex.h @@ -55,16 +55,16 @@ #pragma once -#include "theory/arith/error_set.h" -#include "theory/arith/linear_equality.h" -#include "theory/arith/simplex.h" -#include "theory/arith/simplex_update.h" +#include "theory/arith/linear/error_set.h" +#include "theory/arith/linear/linear_equality.h" +#include "theory/arith/linear/simplex.h" +#include "theory/arith/linear/simplex_update.h" #include "util/dense_map.h" #include "util/statistics_stats.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class FCSimplexDecisionProcedure : public SimplexDecisionProcedure{ public: diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/linear/infer_bounds.cpp similarity index 98% rename from src/theory/arith/infer_bounds.cpp rename to src/theory/arith/linear/infer_bounds.cpp index 30ae5f934..ec2843aa2 100644 --- a/src/theory/arith/infer_bounds.cpp +++ b/src/theory/arith/linear/infer_bounds.cpp @@ -16,14 +16,14 @@ * \todo document this file */ -#include "theory/arith/infer_bounds.h" +#include "theory/arith/linear/infer_bounds.h" #include "theory/rewriter.h" using namespace cvc5::internal::kind; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { using namespace inferbounds; diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/linear/infer_bounds.h similarity index 99% rename from src/theory/arith/infer_bounds.h rename to src/theory/arith/linear/infer_bounds.h index cf9d71a77..de6b50e38 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/linear/infer_bounds.h @@ -30,7 +30,7 @@ namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { namespace inferbounds { enum Algorithms {None = 0, Lookup, RowSum, Simplex}; diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear/linear_equality.cpp similarity index 99% rename from src/theory/arith/linear_equality.cpp rename to src/theory/arith/linear/linear_equality.cpp index 337f24491..6fcabefab 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear/linear_equality.cpp @@ -12,18 +12,18 @@ * * This implements the LinearEqualityModule. */ -#include "theory/arith/linear_equality.h" +#include "theory/arith/linear/linear_equality.h" #include "base/output.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/constraint.h" +#include "theory/arith/linear/constraint.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { /* Explicitly instatiate these functions. */ diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear/linear_equality.h similarity index 98% rename from src/theory/arith/linear_equality.h rename to src/theory/arith/linear/linear_equality.h index ac6b8deae..30b137dd8 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear/linear_equality.h @@ -31,17 +31,17 @@ #pragma once #include "options/arith_options.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/constraint_forward.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/constraint_forward.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/simplex_update.h" -#include "theory/arith/tableau.h" +#include "theory/arith/linear/partial_model.h" +#include "theory/arith/linear/simplex_update.h" +#include "theory/arith/linear/tableau.h" #include "util/statistics_stats.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { struct Border{ // The constraint for the border diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/linear/matrix.cpp similarity index 93% rename from src/theory/arith/matrix.cpp rename to src/theory/arith/linear/matrix.cpp index bcd4eb880..3a8b3b9fb 100644 --- a/src/theory/arith/matrix.cpp +++ b/src/theory/arith/linear/matrix.cpp @@ -13,12 +13,12 @@ * Sparse matrix implementations for different types. */ -#include "theory/arith/matrix.h" +#include "theory/arith/linear/matrix.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { void NoEffectCCCB::update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) {} void NoEffectCCCB::multiplyRow(RowIndex ridx, int sgn){} diff --git a/src/theory/arith/matrix.h b/src/theory/arith/linear/matrix.h similarity index 99% rename from src/theory/arith/matrix.h rename to src/theory/arith/linear/matrix.h index 95ce0225f..bed8aa9df 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/linear/matrix.h @@ -24,13 +24,13 @@ #include #include "base/output.h" -#include "theory/arith/arithvar.h" +#include "theory/arith/linear/arithvar.h" #include "util/dense_map.h" #include "util/index.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { typedef Index EntryID; const EntryID ENTRYID_SENTINEL = std::numeric_limits::max(); @@ -368,8 +368,8 @@ public: typedef MatrixEntry Entry; protected: - typedef cvc5::internal::theory::arith::RowVector RowVectorT; - typedef cvc5::internal::theory::arith::ColumnVector ColumnVectorT; + typedef RowVector RowVectorT; + typedef ColumnVector ColumnVectorT; public: typedef typename RowVectorT::const_iterator RowIterator; diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/linear/normal_form.cpp similarity index 99% rename from src/theory/arith/normal_form.cpp rename to src/theory/arith/linear/normal_form.cpp index b7b10036c..81bb23833 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/linear/normal_form.cpp @@ -15,7 +15,7 @@ * [[ Add lengthier description here ]] * \todo document this file */ -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/normal_form.h" #include @@ -27,7 +27,7 @@ using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { Constant Constant::mkConstant(const Rational& rat) { return Constant(mkRationalNode(rat)); diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/linear/normal_form.h similarity index 99% rename from src/theory/arith/normal_form.h rename to src/theory/arith/linear/normal_form.h index 5e79d8a54..9656e2876 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/linear/normal_form.h @@ -31,7 +31,7 @@ namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { /***********************************************/ /***************** Normal Form *****************/ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/linear/partial_model.cpp similarity index 99% rename from src/theory/arith/partial_model.cpp rename to src/theory/arith/linear/partial_model.cpp index 65330381c..58beca87f 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/linear/partial_model.cpp @@ -17,15 +17,15 @@ */ #include "base/output.h" -#include "theory/arith/constraint.h" -#include "theory/arith/normal_form.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/normal_form.h" +#include "theory/arith/linear/partial_model.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { ArithVariables::ArithVariables(context::Context* c, DeltaComputeCallback deltaComputingFunc) diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/linear/partial_model.h similarity index 97% rename from src/theory/arith/partial_model.h rename to src/theory/arith/linear/partial_model.h index 3f027e6b8..349478b69 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/linear/partial_model.h @@ -27,10 +27,11 @@ #include "context/cdlist.h" #include "expr/node.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/bound_counts.h" -#include "theory/arith/callbacks.h" -#include "theory/arith/constraint_forward.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/arithvar_node_map.h" +#include "theory/arith/linear/bound_counts.h" +#include "theory/arith/linear/callbacks.h" +#include "theory/arith/linear/constraint_forward.h" #include "theory/arith/delta_rational.h" namespace cvc5::context { @@ -38,7 +39,7 @@ class Context; } namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { /** * (For the moment) the type hierarchy goes as: diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/linear/simplex.cpp similarity index 97% rename from src/theory/arith/simplex.cpp rename to src/theory/arith/linear/simplex.cpp index 66aba1042..6e20cccd0 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/linear/simplex.cpp @@ -14,23 +14,23 @@ * DPLL(T) decision procedure. */ -#include "theory/arith/simplex.h" +#include "theory/arith/linear/simplex.h" #include "base/output.h" #include "options/arith_options.h" #include "options/smt_options.h" #include "smt/env.h" -#include "theory/arith/constraint.h" -#include "theory/arith/error_set.h" -#include "theory/arith/linear_equality.h" -#include "theory/arith/tableau.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/error_set.h" +#include "theory/arith/linear/linear_equality.h" +#include "theory/arith/linear/tableau.h" #include "util/statistics_value.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { SimplexDecisionProcedure::SimplexDecisionProcedure( Env& env, diff --git a/src/theory/arith/simplex.h b/src/theory/arith/linear/simplex.h similarity index 98% rename from src/theory/arith/simplex.h rename to src/theory/arith/linear/simplex.h index fd50a8594..e739ac837 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/linear/simplex.h @@ -59,15 +59,15 @@ #include "options/arith_options.h" #include "smt/env_obj.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/partial_model.h" #include "util/dense_map.h" #include "util/result.h" #include "util/statistics_stats.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class ErrorSet; class LinearEqualityModule; diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/linear/simplex_update.cpp similarity index 97% rename from src/theory/arith/simplex_update.cpp rename to src/theory/arith/linear/simplex_update.cpp index 19d5fcc19..9e7a55108 100644 --- a/src/theory/arith/simplex_update.cpp +++ b/src/theory/arith/linear/simplex_update.cpp @@ -13,15 +13,15 @@ * This implements the UpdateInfo. */ -#include "theory/arith/simplex_update.h" +#include "theory/arith/linear/simplex_update.h" -#include "theory/arith/constraint.h" +#include "theory/arith/linear/constraint.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { /* * Generates a string representation of std::optional and inserts it into a diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/linear/simplex_update.h similarity index 98% rename from src/theory/arith/simplex_update.h rename to src/theory/arith/linear/simplex_update.h index 4bcadbb98..0a4c90ecc 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/linear/simplex_update.h @@ -31,13 +31,13 @@ #include -#include "theory/arith/arithvar.h" -#include "theory/arith/constraint_forward.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/constraint_forward.h" #include "theory/arith/delta_rational.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { enum WitnessImprovement { ConflictFound = 0, diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/linear/soi_simplex.cpp similarity index 99% rename from src/theory/arith/soi_simplex.cpp rename to src/theory/arith/linear/soi_simplex.cpp index ad5a71d04..0ba3e3495 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/linear/soi_simplex.cpp @@ -13,23 +13,23 @@ * This is an implementation of the Simplex Module for the Simplex for * DPLL(T) decision procedure. */ -#include "theory/arith/soi_simplex.h" +#include "theory/arith/linear/soi_simplex.h" #include #include "base/output.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" -#include "theory/arith/constraint.h" -#include "theory/arith/error_set.h" -#include "theory/arith/tableau.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/error_set.h" +#include "theory/arith/linear/tableau.h" #include "util/statistics_stats.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(Env& env, LinearEqualityModule& linEq, diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/linear/soi_simplex.h similarity index 98% rename from src/theory/arith/soi_simplex.h rename to src/theory/arith/linear/soi_simplex.h index 56483ee62..c8cfc649a 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/linear/soi_simplex.h @@ -55,15 +55,15 @@ #pragma once -#include "theory/arith/linear_equality.h" -#include "theory/arith/simplex.h" -#include "theory/arith/simplex_update.h" +#include "theory/arith/linear/linear_equality.h" +#include "theory/arith/linear/simplex.h" +#include "theory/arith/linear/simplex_update.h" #include "util/dense_map.h" #include "util/statistics_stats.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure { public: diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/linear/tableau.cpp similarity index 98% rename from src/theory/arith/tableau.cpp rename to src/theory/arith/linear/tableau.cpp index 9a96ca944..324f5df87 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/linear/tableau.cpp @@ -17,12 +17,12 @@ */ #include "base/output.h" -#include "theory/arith/tableau.h" +#include "theory/arith/linear/tableau.h" using namespace std; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { void Tableau::pivot(ArithVar oldBasic, ArithVar newBasic, CoefficientChangeCallback& cb){ diff --git a/src/theory/arith/tableau.h b/src/theory/arith/linear/tableau.h similarity index 97% rename from src/theory/arith/tableau.h rename to src/theory/arith/linear/tableau.h index 2c5fc3ccb..7bbc0d6ed 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/linear/tableau.h @@ -22,14 +22,14 @@ #include -#include "theory/arith/arithvar.h" -#include "theory/arith/matrix.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/matrix.h" #include "util/dense_map.h" #include "util/rational.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { /** * A Tableau is a Rational matrix that keeps its rows in solved form. diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/linear/tableau_sizes.cpp similarity index 89% rename from src/theory/arith/tableau_sizes.cpp rename to src/theory/arith/linear/tableau_sizes.cpp index b353812ff..a7c8f9e88 100644 --- a/src/theory/arith/tableau_sizes.cpp +++ b/src/theory/arith/linear/tableau_sizes.cpp @@ -17,12 +17,12 @@ */ #include "base/output.h" -#include "theory/arith/tableau_sizes.h" -#include "theory/arith/tableau.h" +#include "theory/arith/linear/tableau_sizes.h" +#include "theory/arith/linear/tableau.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { uint32_t TableauSizes::getRowLength(ArithVar b) const { return d_tab->basicRowLength(b); diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/linear/tableau_sizes.h similarity index 93% rename from src/theory/arith/tableau_sizes.h rename to src/theory/arith/linear/tableau_sizes.h index cf189a146..3fbd0c14f 100644 --- a/src/theory/arith/tableau_sizes.h +++ b/src/theory/arith/linear/tableau_sizes.h @@ -20,11 +20,11 @@ #pragma once -#include "theory/arith/arithvar.h" +#include "theory/arith/linear/arithvar.h" namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { class Tableau; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp similarity index 99% rename from src/theory/arith/theory_arith_private.cpp rename to src/theory/arith/linear/theory_arith_private.cpp index 58ec5ee19..04ebdeffb 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -16,7 +16,7 @@ * \todo document this file */ -#include "theory/arith/theory_arith_private.h" +#include "theory/arith/linear/theory_arith_private.h" #include #include @@ -45,22 +45,22 @@ #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" -#include "theory/arith/approx_simplex.h" +#include "theory/arith/linear/approx_simplex.h" #include "theory/arith/arith_rewriter.h" -#include "theory/arith/arith_static_learner.h" +#include "theory/arith/linear/arith_static_learner.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/congruence_manager.h" -#include "theory/arith/constraint.h" -#include "theory/arith/cut_log.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/congruence_manager.h" +#include "theory/arith/linear/constraint.h" +#include "theory/arith/linear/cut_log.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/dio_solver.h" -#include "theory/arith/linear_equality.h" -#include "theory/arith/matrix.h" +#include "theory/arith/linear/dio_solver.h" +#include "theory/arith/linear/linear_equality.h" +#include "theory/arith/linear/matrix.h" #include "theory/arith/nl/nonlinear_extension.h" -#include "theory/arith/normal_form.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/simplex.h" +#include "theory/arith/linear/normal_form.h" +#include "theory/arith/linear/partial_model.h" +#include "theory/arith/linear/simplex.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" #include "theory/quantifiers/fmf/bounded_integers.h" @@ -80,7 +80,7 @@ using namespace cvc5::internal::kind; namespace cvc5::internal { namespace theory { -namespace arith { +namespace arith::linear { static Node toSumNode(const ArithVariables& vars, const DenseMap& sum); static bool complexityBelow(const DenseMap& row, uint32_t cap); @@ -3528,9 +3528,8 @@ bool TheoryArithPrivate::splitDisequalities(){ TrustNode lemma = front->split(); ++(d_statistics.d_statDisequalitySplits); - Trace("arith::lemma") << "Now " << rewrite(lemma.getNode()) << endl; + Trace("arith::lemma") << "Now " << lemma.getNode() << endl; outputTrustedLemma(lemma, InferenceId::ARITH_SPLIT_DEQ); - // cout << "Now " << rewrite(lemma) << endl; splitSomething = true; }else if(d_partialModel.strictlyLessThanLowerBound(lhsVar, rhsValue)){ Trace("arith::eq") << "can drop as less than lb" << front << endl; @@ -4569,7 +4568,12 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ return d_rowTracking[ridx]; } -std::pair TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ +std::pair TheoryArithPrivate::entailmentCheck(TNode lit) +{ + ArithEntailmentCheckParameters params; + params.addLookupRowSumAlgorithms(); + ArithEntailmentCheckSideEffects out; + using namespace inferbounds; // l k r diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/linear/theory_arith_private.h similarity index 97% rename from src/theory/arith/theory_arith_private.h rename to src/theory/arith/linear/theory_arith_private.h index eab5669ee..d8a361315 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/linear/theory_arith_private.h @@ -29,25 +29,25 @@ #include "expr/node.h" #include "expr/node_builder.h" #include "proof/trust_node.h" -#include "theory/arith/arith_static_learner.h" +#include "theory/arith/linear/arith_static_learner.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/arithvar.h" -#include "theory/arith/attempt_solution_simplex.h" +#include "theory/arith/linear/arithvar.h" +#include "theory/arith/linear/attempt_solution_simplex.h" #include "theory/arith/branch_and_bound.h" -#include "theory/arith/congruence_manager.h" -#include "theory/arith/constraint.h" +#include "theory/arith/linear/congruence_manager.h" +#include "theory/arith/linear/constraint.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/dio_solver.h" -#include "theory/arith/dual_simplex.h" -#include "theory/arith/error_set.h" -#include "theory/arith/fc_simplex.h" -#include "theory/arith/infer_bounds.h" -#include "theory/arith/linear_equality.h" -#include "theory/arith/matrix.h" -#include "theory/arith/normal_form.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/linear/dio_solver.h" +#include "theory/arith/linear/dual_simplex.h" +#include "theory/arith/linear/error_set.h" +#include "theory/arith/linear/fc_simplex.h" +#include "theory/arith/linear/infer_bounds.h" +#include "theory/arith/linear/linear_equality.h" +#include "theory/arith/linear/matrix.h" +#include "theory/arith/linear/normal_form.h" +#include "theory/arith/linear/partial_model.h" #include "theory/arith/proof_checker.h" -#include "theory/arith/soi_simplex.h" +#include "theory/arith/linear/soi_simplex.h" #include "theory/arith/theory_arith.h" #include "theory/valuation.h" #include "util/dense_map.h" @@ -64,7 +64,7 @@ namespace theory { class TheoryModel; -namespace arith { +namespace arith::linear { class BranchCutInfo; class TreeLog; @@ -76,7 +76,7 @@ namespace inferbounds { class InferBoundAlgorithm; } class InferBoundsResult; - + /** * Implementation of QF_LRA. * Based upon: @@ -483,7 +483,7 @@ private: Node getModelValue(TNode var); - std::pair entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out); + std::pair entailmentCheck(TNode lit); //--------------------------------- standard check /** Pre-check, called before the fact queue of the theory is processed. */ @@ -875,6 +875,7 @@ private: Statistics d_statistics; }; /* class TheoryArithPrivate */ + } // namespace arith } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index 8b6e0c303..1a19216b5 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -23,7 +23,7 @@ #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/poly_conversion.h" -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/normal_form.h" #include "theory/rewriter.h" #include "util/poly_util.h" @@ -89,7 +89,7 @@ std::vector ICPSolver::constructCandidates(const Node& n) { return {}; } - auto comp = Comparison::parseNormalForm(tmp).decompose(false); + auto comp = linear::Comparison::parseNormalForm(tmp).decompose(false); Kind k = std::get<1>(comp); if (k == Kind::DISTINCT) { diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 93ffb542d..f05bd2185 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -21,8 +21,7 @@ #include "expr/skolem_manager.h" #include "theory/arith/arith_poly_norm.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/constraint.h" -#include "theory/arith/normal_form.h" +#include "theory/arith/linear/constraint.h" #include "theory/arith/operator_elim.h" using namespace cvc5::internal::kind; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index f6496166d..fe04a9c26 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -22,9 +22,8 @@ #include "theory/arith/arith_evaluator.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/equality_solver.h" -#include "theory/arith/infer_bounds.h" #include "theory/arith/nl/nonlinear_extension.h" -#include "theory/arith/theory_arith_private.h" +#include "theory/arith/linear/theory_arith_private.h" #include "theory/ext_theory.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -45,7 +44,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_ppre(d_env), d_bab(env, d_astate, d_im, d_ppre, d_pnm), d_eqSolver(nullptr), - d_internal(new TheoryArithPrivate(*this, env, d_bab)), + d_internal(new linear::TheoryArithPrivate(*this, env, d_bab)), d_nonlinearExtension(nullptr), d_opElim(d_env), d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim), @@ -363,12 +362,9 @@ Node TheoryArith::getModelValue(TNode var) { std::pair TheoryArith::entailmentCheck(TNode lit) { - ArithEntailmentCheckParameters def; - def.addLookupRowSumAlgorithms(); - ArithEntailmentCheckSideEffects ase; - std::pair res = d_internal->entailmentCheck(lit, def, ase); - return res; + return d_internal->entailmentCheck(lit); } + eq::ProofEqEngine* TheoryArith::getProofEqEngine() { return d_im.getProofEqEngine(); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 2682b4d71..c6ced5781 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -34,7 +34,10 @@ class NonlinearExtension; } class EqualitySolver; + +namespace linear { class TheoryArithPrivate; +} /** * Implementation of linear and non-linear integer and real arithmetic. @@ -42,7 +45,7 @@ class TheoryArithPrivate; * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf */ class TheoryArith : public Theory { - friend class TheoryArithPrivate; + friend class linear::TheoryArithPrivate; public: TheoryArith(Env& env, OutputChannel& out, Valuation valuation); virtual ~TheoryArith(); @@ -157,7 +160,7 @@ class TheoryArith : public Theory { /** The equality solver */ std::unique_ptr d_eqSolver; /** The (old) linear arithmetic solver */ - TheoryArithPrivate* d_internal; + linear::TheoryArithPrivate* d_internal; /** * The non-linear extension, responsible for all approaches for non-linear diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 33b5f08f2..e468ae001 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -18,9 +18,9 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/linear/partial_model.h" #include "theory/arith/theory_arith.h" -#include "theory/arith/theory_arith_private.h" +#include "theory/arith/linear/theory_arith_private.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "util/random.h" -- 2.30.2