diff options
Diffstat (limited to 'src/theory')
35 files changed, 502 insertions, 390 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 33860d2d9..89d7619cf 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -308,16 +308,17 @@ Rational ApproximateSimplex::estimateWithCFE(const Rational& r, const Integer& K } } -Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d, const Integer& D) +std::optional<Rational> ApproximateSimplex::estimateWithCFE(double d, + const Integer& D) { - if (Maybe<Rational> from_double = Rational::fromDouble(d)) + if (std::optional<Rational> from_double = Rational::fromDouble(d)) { - return estimateWithCFE(from_double.value(), D); + return estimateWithCFE(*from_double, D); } - return Maybe<Rational>(); + return std::optional<Rational>(); } -Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d) +std::optional<Rational> ApproximateSimplex::estimateWithCFE(double d) { return estimateWithCFE(d, s_defaultMaxDenom); } @@ -1106,9 +1107,9 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const } DeltaRational proposal; - if (Maybe<Rational> maybe_new = estimateWithCFE(newAssign)) + if (std::optional maybe_new = estimateWithCFE(newAssign)) { - proposal = maybe_new.value(); + proposal = *maybe_new; } else { @@ -2055,13 +2056,13 @@ bool ApproxGLPK::attemptBranchCut(int nid, const BranchCutInfo& br_cut){ d_pad.d_cut.lhs.set(x, Rational(1)); Rational& rhs = d_pad.d_cut.rhs; - Maybe<Rational> br_cut_rhs = Rational::fromDouble(br_cut.getRhs()); + std::optional<Rational> br_cut_rhs = Rational::fromDouble(br_cut.getRhs()); if (!br_cut_rhs) { return true; } - rhs = estimateWithCFE(br_cut_rhs.value(), Integer(1)); + rhs = estimateWithCFE(*br_cut_rhs, Integer(1)); d_pad.d_failure = !rhs.isIntegral(); if(d_pad.d_failure) { return true; } @@ -2112,13 +2113,13 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){ DenseMap<Rational>& alpha = d_pad.d_alpha.lhs; Rational& b = d_pad.d_alpha.rhs; - Maybe<Rational> delta = estimateWithCFE(mir.delta); + std::optional<Rational> delta = estimateWithCFE(mir.delta); if (!delta) { return true; } - d_pad.d_failure = (delta.value().sgn() <= 0); + d_pad.d_failure = (delta->sgn() <= 0); if(d_pad.d_failure){ return true; } Debug("approx::mir") << "applyCMIRRule() " << delta << " " << mir.delta << endl; @@ -2128,7 +2129,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){ for(; iter != iend; ++iter){ ArithVar v = *iter; const Rational& curr = alpha[v]; - Rational next = curr / delta.value(); + Rational next = curr / *delta; if(compRanges.isKey(v)){ b -= curr * compRanges[v]; alpha.set(v, - next); @@ -2136,7 +2137,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){ alpha.set(v, next); } } - b = b / delta.value(); + b = b / *delta; Rational roundB = (b + Rational(1,2)).floor(); d_pad.d_failure = (b - roundB).abs() < Rational(1,90); @@ -2554,7 +2555,7 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){ double coeff = row_sum.coeffs[i]; ArithVar x = _getArithVar(nid, M, aux_ind); if(x == ARITHVAR_SENTINEL){ return true; } - Maybe<Rational> c = estimateWithCFE(coeff); + std::optional<Rational> c = estimateWithCFE(coeff); if (!c) { return true; @@ -2562,11 +2563,11 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){ if (lhs.isKey(x)) { - lhs.get(x) -= c.value(); + lhs.get(x) -= *c; } else { - lhs.set(x, -c.value()); + lhs.set(x, -(*c)); } } @@ -2586,13 +2587,13 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){ double coeff = row_sum.coeffs[i]; ArithVar x = _getArithVar(nid, M, aux_ind); Assert(x != ARITHVAR_SENTINEL); - Maybe<Rational> c = estimateWithCFE(coeff); + std::optional<Rational> c = estimateWithCFE(coeff); if (!c) { return true; } Assert(!lhs.isKey(x)); - lhs.set(x, c.value()); + lhs.set(x, *c); } if(Debug.isOn("approx::mir")){ @@ -3023,12 +3024,12 @@ bool ApproxGLPK::guessCoefficientsConstructTableRow(int nid, int M, const Primit } Debug("guessCoefficientsConstructTableRow") << "match " << ind << "," << var << "("<<d_vars.asNode(var)<<")"<<endl; - Maybe<Rational> cfe = estimateWithCFE(coeff, D); + std::optional<Rational> cfe = estimateWithCFE(coeff, D); if (!cfe) { return true; } - tab.set(var, cfe.value()); + tab.set(var, *cfe); Debug("guessCoefficientsConstructTableRow") << var << " cfe " << cfe << endl; } if(!guessIsConstructable(tab)){ diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index aeced6f10..c0d6990a4 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -19,12 +19,13 @@ #include "cvc5_private.h" #pragma once + +#include <optional> #include <vector> #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "util/dense_map.h" -#include "util/maybe.h" #include "util/rational.h" #include "util/statistics_stats.h" @@ -126,8 +127,8 @@ class ApproximateSimplex{ * cuts off the estimate once the value is approximately zero. * This is designed for removing rounding artifacts. */ - static Maybe<Rational> estimateWithCFE(double d); - static Maybe<Rational> estimateWithCFE(double d, const Integer& D); + static std::optional<Rational> estimateWithCFE(double d); + static std::optional<Rational> estimateWithCFE(double d, const Integer& D); /** * Converts a rational to a continued fraction expansion representation diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp index 07f24f0f0..4cbb8211d 100644 --- a/src/theory/arith/infer_bounds.cpp +++ b/src/theory/arith/infer_bounds.cpp @@ -35,20 +35,21 @@ InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a) Assert(a != Simplex); } -InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds) - : d_alg(Simplex) +InferBoundAlgorithm::InferBoundAlgorithm( + const std::optional<int>& simplexRounds) + : d_alg(Simplex) {} Algorithms InferBoundAlgorithm::getAlgorithm() const{ return d_alg; } -const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{ +const std::optional<int>& InferBoundAlgorithm::getSimplexRounds() const +{ Assert(getAlgorithm() == Simplex); return d_simplexRounds; } - InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){ return InferBoundAlgorithm(Lookup); } @@ -57,7 +58,9 @@ InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){ return InferBoundAlgorithm(RowSum); } -InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){ +InferBoundAlgorithm InferBoundAlgorithm::mkSimplex( + const std::optional<int>& rounds) +{ return InferBoundAlgorithm(rounds); } diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h index 8a65c7c66..22b0b5d54 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/infer_bounds.h @@ -20,12 +20,12 @@ #pragma once +#include <optional> #include <ostream> #include "expr/node.h" #include "theory/arith/delta_rational.h" #include "util/integer.h" -#include "util/maybe.h" #include "util/rational.h" namespace cvc5 { @@ -39,19 +39,19 @@ namespace inferbounds { class InferBoundAlgorithm { private: Algorithms d_alg; - Maybe<int> d_simplexRounds; + std::optional<int> d_simplexRounds; InferBoundAlgorithm(Algorithms a); - InferBoundAlgorithm(const Maybe<int>& simplexRounds); + InferBoundAlgorithm(const std::optional<int>& simplexRounds); -public: + public: InferBoundAlgorithm(); Algorithms getAlgorithm() const; - const Maybe<int>& getSimplexRounds() const; + const std::optional<int>& getSimplexRounds() const; static InferBoundAlgorithm mkLookup(); static InferBoundAlgorithm mkRowSum(); - static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds); + static InferBoundAlgorithm mkSimplex(const std::optional<int>& rounds); }; std::ostream& operator<<(std::ostream& os, const Algorithms a); diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 82cc02815..47dd208c1 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -1054,14 +1054,12 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr Assert(nbSgn != 0); if(nbSgn > 0){ - if (d_upperBoundDifference.nothing() - || nbDiff <= d_upperBoundDifference.value()) + if (!d_upperBoundDifference || nbDiff <= *d_upperBoundDifference) { return false; } }else{ - if (d_lowerBoundDifference.nothing() - || nbDiff >= d_lowerBoundDifference.value()) + if (!d_lowerBoundDifference || nbDiff >= *d_lowerBoundDifference) { return false; } @@ -1132,8 +1130,8 @@ UpdateInfo LinearEqualityModule::mkConflictUpdate(const Tableau::Entry& entry, b UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational& focusCoeff, UpdatePreferenceFunction pref){ Assert(d_increasing.empty()); Assert(d_decreasing.empty()); - Assert(d_lowerBoundDifference.nothing()); - Assert(d_upperBoundDifference.nothing()); + Assert(!d_lowerBoundDifference); + Assert(!d_upperBoundDifference); int focusCoeffSgn = focusCoeff.sgn(); @@ -1146,14 +1144,14 @@ UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational& if(d_variables.hasUpperBound(nb)){ ConstraintP ub = d_variables.getUpperBoundConstraint(nb); d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb); - Border border(ub, d_upperBoundDifference.value(), false, NULL, true); + Border border(ub, *d_upperBoundDifference, false, NULL, true); Debug("handleBorders") << "push back increasing " << border << endl; d_increasing.push_back(border); } if(d_variables.hasLowerBound(nb)){ ConstraintP lb = d_variables.getLowerBoundConstraint(nb); d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb); - Border border(lb, d_lowerBoundDifference.value(), false, NULL, false); + Border border(lb, *d_lowerBoundDifference, false, NULL, false); Debug("handleBorders") << "push back decreasing " << border << endl; d_decreasing.push_back(border); } @@ -1189,8 +1187,8 @@ void LinearEqualityModule::clearSpeculative(){ // clear everything away d_increasing.clear(); d_decreasing.clear(); - d_lowerBoundDifference.clear(); - d_upperBoundDifference.clear(); + d_lowerBoundDifference.reset(); + d_upperBoundDifference.reset(); } void LinearEqualityModule::handleBorders(UpdateInfo& selected, ArithVar nb, const Rational& focusCoeff, BorderHeap& heap, int minimumFixes, UpdatePreferenceFunction pref){ diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 276c8e63e..7195a6583 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -37,7 +37,6 @@ #include "theory/arith/partial_model.h" #include "theory/arith/simplex_update.h" #include "theory/arith/tableau.h" -#include "util/maybe.h" #include "util/statistics_stats.h" namespace cvc5 { @@ -216,8 +215,8 @@ private: BorderHeap d_increasing; BorderHeap d_decreasing; - Maybe<DeltaRational> d_upperBoundDifference; - Maybe<DeltaRational> d_lowerBoundDifference; + std::optional<DeltaRational> d_upperBoundDifference; + std::optional<DeltaRational> d_lowerBoundDifference; Rational d_one; Rational d_negOne; diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 7db6c266f..b196f9990 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -30,20 +30,18 @@ namespace theory { namespace arith { namespace nl { -ExtState::ExtState(InferenceManager& im, - NlModel& model, - ProofNodeManager* pnm, - context::UserContext* c) - : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c) +ExtState::ExtState(InferenceManager& im, NlModel& model, Env& env) + : d_im(im), d_model(model), d_env(env) { d_false = NodeManager::currentNM()->mkConst(false); d_true = NodeManager::currentNM()->mkConst(true); d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - if (d_pnm != nullptr) + if (d_env.isTheoryProofProducing()) { - d_proof.reset(new CDProofSet<CDProof>(d_pnm, d_ctx, "nl-ext")); + d_proof.reset(new CDProofSet<CDProof>( + d_env.getProofNodeManager(), d_env.getUserContext(), "nl-ext")); } } @@ -105,7 +103,7 @@ bool ExtState::isProofEnabled() const { return d_proof.get() != nullptr; } CDProof* ExtState::getProof() { Assert(isProofEnabled()); - return d_proof->allocateProof(d_ctx); + return d_proof->allocateProof(d_env.getUserContext()); } } // namespace nl diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 7c2cc1b9b..ac00f6f87 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -20,6 +20,7 @@ #include "expr/node.h" #include "proof/proof_set.h" +#include "smt/env.h" #include "theory/arith/nl/ext/monomial.h" namespace cvc5 { @@ -37,10 +38,7 @@ class NlModel; struct ExtState { - ExtState(InferenceManager& im, - NlModel& model, - ProofNodeManager* pnm, - context::UserContext* c); + ExtState(InferenceManager& im, NlModel& model, Env& env); void init(const std::vector<Node>& xts); @@ -63,13 +61,8 @@ struct ExtState InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; - /** - * Pointer to the current proof node manager. nullptr, if proofs are - * disabled. - */ - ProofNodeManager* d_pnm; - /** The user context. */ - context::UserContext* d_ctx; + /** Reference to the environment */ + Env& d_env; /** * A CDProofSet that hands out CDProof objects for lemmas. */ diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 0deb2c99d..31bc4c662 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -207,7 +207,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts, } // compute if bound is not satisfied, and store what is required // for a possible refinement - if (options::nlExtTangentPlanes()) + if (d_data->d_env.getOptions().arith.nlExtTangentPlanes) { if (is_false_lit) { diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 6d9faa356..dcd6398b5 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -29,7 +29,7 @@ namespace arith { namespace nl { SplitZeroCheck::SplitZeroCheck(ExtState* data) - : d_data(data), d_zero_split(d_data->d_ctx) + : d_data(data), d_zero_split(d_data->d_env.getUserContext()) { } diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 785127db5..df531fca7 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -37,27 +37,29 @@ namespace arith { namespace nl { NonlinearExtension::NonlinearExtension(TheoryArith& containing, - ArithState& state, - eq::EqualityEngine* ee, - ProofNodeManager* pnm) + ArithState& state) : d_containing(containing), + d_astate(state), d_im(containing.getInferenceManager()), d_needsLastCall(false), d_checkCounter(0), - d_extTheoryCb(ee), + d_extTheoryCb(state.getEqualityEngine()), d_extTheory(d_extTheoryCb, containing.getSatContext(), containing.getUserContext(), d_im), d_model(containing.getSatContext()), - d_trSlv(d_im, d_model, pnm, containing.getUserContext()), - d_extState(d_im, d_model, pnm, containing.getUserContext()), + d_trSlv(d_im, d_model, d_astate.getEnv()), + d_extState(d_im, d_model, d_astate.getEnv()), d_factoringSlv(&d_extState), d_monomialBoundsSlv(&d_extState), d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), - d_cadSlv(d_im, d_model, state.getUserContext(), pnm), + d_cadSlv(d_im, + d_model, + state.getUserContext(), + d_astate.getEnv().getProofNodeManager()), d_icpSlv(d_im), d_iandSlv(d_im, state, d_model), d_pow2Slv(d_im, state, d_model) @@ -73,9 +75,9 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; - if (pc != nullptr) + if (d_astate.getEnv().isTheoryProofProducing()) { + ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker(); d_proofChecker.registerTo(pc); } } @@ -94,6 +96,11 @@ void NonlinearExtension::processSideEffect(const NlLemma& se) d_trSlv.processSideEffect(se); } +const Options& NonlinearExtension::options() const +{ + return d_containing.options(); +} + void NonlinearExtension::computeRelevantAssertions( const std::vector<Node>& assertions, std::vector<Node>& keep) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index aae19df6e..6cbbfcdac 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -84,10 +84,7 @@ class NonlinearExtension typedef context::CDHashSet<Node> NodeSet; public: - NonlinearExtension(TheoryArith& containing, - ArithState& state, - eq::EqualityEngine* ee, - ProofNodeManager* pnm); + NonlinearExtension(TheoryArith& containing, ArithState& state); ~NonlinearExtension(); /** * Does non-context dependent setup for a node connected to a theory. @@ -145,6 +142,9 @@ class NonlinearExtension /** Process side effect se */ void processSideEffect(const NlLemma& se); + /** Obtain options object */ + const Options& options() const; + private: /** Model-based refinement * @@ -223,6 +223,8 @@ class NonlinearExtension Node d_true; // The theory of arithmetic containing this extension. TheoryArith& d_containing; + /** A reference to the arithmetic state object */ + ArithState& d_astate; InferenceManager& d_im; /** The statistics class */ NlStats d_stats; diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index e5fa31aad..2b1ef0a2e 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -603,39 +603,39 @@ Node excluding_interval_to_lemma(const Node& variable, return nm->mkNode(Kind::OR, lb, ub); } -Maybe<Rational> get_lower_bound(const Node& n) +std::optional<Rational> get_lower_bound(const Node& n) { - if (n.getNumChildren() != 2) return Maybe<Rational>(); + if (n.getNumChildren() != 2) return std::optional<Rational>(); if (n.getKind() == Kind::LT) { - if (!n[0].isConst()) return Maybe<Rational>(); - if (!n[1].isVar()) return Maybe<Rational>(); + if (!n[0].isConst()) return std::optional<Rational>(); + if (!n[1].isVar()) return std::optional<Rational>(); return n[0].getConst<Rational>(); } else if (n.getKind() == Kind::GT) { - if (!n[0].isVar()) return Maybe<Rational>(); - if (!n[1].isConst()) return Maybe<Rational>(); + if (!n[0].isVar()) return std::optional<Rational>(); + if (!n[1].isConst()) return std::optional<Rational>(); return n[1].getConst<Rational>(); } - return Maybe<Rational>(); + return std::optional<Rational>(); } -Maybe<Rational> get_upper_bound(const Node& n) +std::optional<Rational> get_upper_bound(const Node& n) { - if (n.getNumChildren() != 2) return Maybe<Rational>(); + if (n.getNumChildren() != 2) return std::optional<Rational>(); if (n.getKind() == Kind::LT) { - if (!n[0].isVar()) return Maybe<Rational>(); - if (!n[1].isConst()) return Maybe<Rational>(); + if (!n[0].isVar()) return std::optional<Rational>(); + if (!n[1].isConst()) return std::optional<Rational>(); return n[1].getConst<Rational>(); } else if (n.getKind() == Kind::GT) { - if (!n[0].isConst()) return Maybe<Rational>(); - if (!n[1].isVar()) return Maybe<Rational>(); + if (!n[0].isConst()) return std::optional<Rational>(); + if (!n[1].isVar()) return std::optional<Rational>(); return n[0].getConst<Rational>(); } - return Maybe<Rational>(); + return std::optional<Rational>(); } /** Returns indices of appropriate parts of ran encoding. @@ -675,12 +675,12 @@ std::tuple<Node, Rational, Rational> detect_ran_encoding(const Node& n) Assert(false) << "Invalid polynomial equation."; } - Maybe<Rational> lower = get_lower_bound(n[0]); + std::optional<Rational> lower = get_lower_bound(n[0]); if (!lower) lower = get_lower_bound(n[1]); if (!lower) lower = get_lower_bound(n[2]); Assert(lower) << "Could not identify lower bound."; - Maybe<Rational> upper = get_upper_bound(n[0]); + std::optional<Rational> upper = get_upper_bound(n[0]); if (!upper) upper = get_upper_bound(n[1]); if (!upper) upper = get_upper_bound(n[2]); Assert(upper) << "Could not identify upper bound."; diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 0d5e5ad04..c7bb14b3f 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -39,11 +39,10 @@ namespace transcendental { TranscendentalSolver::TranscendentalSolver(InferenceManager& im, NlModel& m, - ProofNodeManager* pnm, - context::UserContext* c) - : d_tstate(im, m, pnm, c), d_expSlv(&d_tstate), d_sineSlv(&d_tstate) + Env& env) + : d_tstate(im, m, env), d_expSlv(&d_tstate), d_sineSlv(&d_tstate) { - d_taylor_degree = options::nlExtTfTaylorDegree(); + d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree; } TranscendentalSolver::~TranscendentalSolver() {} diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index 54bad2c1d..b63ebf29d 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -50,10 +50,7 @@ namespace transcendental { class TranscendentalSolver { public: - TranscendentalSolver(InferenceManager& im, - NlModel& m, - ProofNodeManager* pnm, - context::UserContext* c); + TranscendentalSolver(InferenceManager& im, NlModel& m, Env& env); ~TranscendentalSolver(); /** init last call @@ -187,7 +184,7 @@ class TranscendentalSolver * initially to options::nlExtTfTaylorDegree() and may be incremented * if the option options::nlExtTfIncPrecision() is enabled. */ - unsigned d_taylor_degree; + uint64_t d_taylor_degree; /** Common state for transcendental solver */ transcendental::TranscendentalState d_tstate; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index db20713f1..19a334729 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -30,20 +30,20 @@ namespace transcendental { TranscendentalState::TranscendentalState(InferenceManager& im, NlModel& model, - ProofNodeManager* pnm, - context::UserContext* c) - : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c) + Env& env) + : d_im(im), d_model(model), d_env(env) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - if (d_pnm != nullptr) + if (d_env.isTheoryProofProducing()) { - d_proof.reset(new CDProofSet<CDProof>(d_pnm, d_ctx, "nl-trans")); + d_proof.reset(new CDProofSet<CDProof>( + d_env.getProofNodeManager(), d_env.getUserContext(), "nl-trans")); d_proofChecker.reset(new TranscendentalProofRuleChecker()); - d_proofChecker->registerTo(pnm->getChecker()); + d_proofChecker->registerTo(d_env.getProofNodeManager()->getChecker()); } } @@ -55,7 +55,7 @@ bool TranscendentalState::isProofEnabled() const CDProof* TranscendentalState::getProof() { Assert(isProofEnabled()); - return d_proof->allocateProof(d_ctx); + return d_proof->allocateProof(d_env.getUserContext()); } void TranscendentalState::init(const std::vector<Node>& xts, diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 56cbec79a..65215c83c 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -18,6 +18,7 @@ #include "expr/node.h" #include "proof/proof_set.h" +#include "smt/env.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/transcendental/proof_checker.h" #include "theory/arith/nl/transcendental/taylor_generator.h" @@ -61,10 +62,7 @@ inline std::ostream& operator<<(std::ostream& os, Convexity c) { */ struct TranscendentalState { - TranscendentalState(InferenceManager& im, - NlModel& model, - ProofNodeManager* pnm, - context::UserContext* c); + TranscendentalState(InferenceManager& im, NlModel& model, Env& env); /** * Checks whether proofs are enabled. @@ -170,16 +168,11 @@ struct TranscendentalState InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; + /** Reference to the environment */ + Env& d_env; /** Utility to compute taylor approximations */ TaylorGenerator d_taylor; /** - * Pointer to the current proof node manager. nullptr, if proofs are - * disabled. - */ - ProofNodeManager* d_pnm; - /** The user context. */ - context::UserContext* d_ctx; - /** * A CDProofSet that hands out CDProof objects for lemmas. */ std::unique_ptr<CDProofSet<CDProof>> d_proof; diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp index dc01a9b42..78e58000e 100644 --- a/src/theory/arith/simplex_update.cpp +++ b/src/theory/arith/simplex_update.cpp @@ -14,6 +14,7 @@ */ #include "theory/arith/simplex_update.h" + #include "theory/arith/constraint.h" using namespace std; @@ -22,6 +23,22 @@ namespace cvc5 { namespace theory { namespace arith { +/* + * Generates a string representation of std::optional and inserts it into a + * stream. + * + * Note: We define this function here in the cvc5::theory::arith namespace, + * because it would otherwise not be found for std::optional<int>. This is due + * to the argument-dependent lookup rules. + * + * @param out The stream + * @param m The value + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, const std::optional<int>& m) +{ + return cvc5::operator<<(out, m); +} UpdateInfo::UpdateInfo(): d_nonbasic(ARITHVAR_SENTINEL), @@ -72,7 +89,7 @@ void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){ d_nonbasicDelta = delta; d_errorsChange = ec; d_focusDirection = f; - d_tableauCoefficient.clear(); + d_tableauCoefficient.reset(); updateWitness(); Assert(unbounded()); Assert(improvement(d_witness)); @@ -82,9 +99,9 @@ void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){ void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){ d_limiting = c; d_nonbasicDelta = delta; - d_errorsChange.clear(); + d_errorsChange.reset(); d_focusDirection = 1; - d_tableauCoefficient.clear(); + d_tableauCoefficient.reset(); updateWitness(); Assert(!describesPivot()); Assert(improvement(d_witness)); @@ -94,8 +111,8 @@ void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){ void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c){ d_limiting = c; d_nonbasicDelta = delta; - d_errorsChange.clear(); - d_focusDirection.clear(); + d_errorsChange.reset(); + d_focusDirection.reset(); updateWitness(); Assert(describesPivot()); Assert(debugSgnAgreement()); @@ -105,7 +122,7 @@ void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, Cons d_limiting = c; d_nonbasicDelta = delta; d_errorsChange = ec; - d_focusDirection.clear(); + d_focusDirection.reset(); d_tableauCoefficient = &r; updateWitness(); Assert(describesPivot()); @@ -117,7 +134,7 @@ void UpdateInfo::witnessedUpdate(const DeltaRational& delta, ConstraintP c, int d_nonbasicDelta = delta; d_errorsChange = ec; d_focusDirection = fd; - d_tableauCoefficient.clear(); + d_tableauCoefficient.reset(); updateWitness(); Assert(describesPivot() || improvement(d_witness)); Assert(debugSgnAgreement()); diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h index 6216f53f6..7efa51acb 100644 --- a/src/theory/arith/simplex_update.h +++ b/src/theory/arith/simplex_update.h @@ -29,10 +29,11 @@ #pragma once -#include "theory/arith/delta_rational.h" +#include <optional> + #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" -#include "util/maybe.h" +#include "theory/arith/delta_rational.h" namespace cvc5 { namespace theory { @@ -109,7 +110,7 @@ private: * This is changed via the updateProposal(...) methods. * The value needs to satisfy debugSgnAgreement() or it is in conflict. */ - Maybe<DeltaRational> d_nonbasicDelta; + std::optional<DeltaRational> d_nonbasicDelta; /** * This is true if the pivot-and-update is *known* to cause a conflict. @@ -118,16 +119,16 @@ private: bool d_foundConflict; /** This is the change in the size of the error set. */ - Maybe<int> d_errorsChange; + std::optional<int> d_errorsChange; /** This is the sgn of the change in the value of the focus set.*/ - Maybe<int> d_focusDirection; + std::optional<int> d_focusDirection; /** This is the sgn of the change in the value of the focus set.*/ - Maybe<DeltaRational> d_focusChange; + std::optional<DeltaRational> d_focusChange; /** This is the coefficient in the tableau for the entry.*/ - Maybe<const Rational*> d_tableauCoefficient; + std::optional<const Rational*> d_tableauCoefficient; /** * This is the constraint that nonbasic is basic is updating s.t. its variable is against it. @@ -329,18 +330,19 @@ private: if(d_foundConflict){ return ConflictFound; } - else if (d_errorsChange.just() && d_errorsChange.value() < 0) + else if (d_errorsChange && d_errorsChange.value() < 0) { return ErrorDropped; } - else if (d_errorsChange.nothing() || d_errorsChange.value() == 0) + else if (d_errorsChange.value_or(0) == 0) { - if(d_focusDirection.just()){ - if (d_focusDirection.value() > 0) + if (d_focusDirection) + { + if (*d_focusDirection > 0) { return FocusImproved; } - else if (d_focusDirection.value() == 0) + else if (*d_focusDirection == 0) { return Degenerate; } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 37069d8b8..aabf017a8 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -44,8 +44,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_ppre(getSatContext(), d_pnm), d_bab(d_astate, d_im, d_ppre, d_pnm), d_eqSolver(nullptr), - d_internal(new TheoryArithPrivate( - *this, getSatContext(), getUserContext(), d_bab, d_pnm)), + d_internal(new TheoryArithPrivate(*this, env, d_bab)), d_nonlinearExtension(nullptr), d_opElim(d_pnm, getLogicInfo()), d_arithPreproc(d_astate, d_im, d_pnm, d_opElim), @@ -102,8 +101,7 @@ void TheoryArith::finishInit() const LogicInfo& logicInfo = getLogicInfo(); if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) { - d_nonlinearExtension.reset( - new nl::NonlinearExtension(*this, d_astate, d_equalityEngine, d_pnm)); + d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate)); } if (d_eqSolver != nullptr) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c85376e6b..ea2887c44 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -19,6 +19,7 @@ #include "theory/arith/theory_arith_private.h" #include <map> +#include <optional> #include <queue> #include <vector> @@ -85,19 +86,19 @@ static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum) static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap); TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, - context::Context* c, - context::UserContext* u, - BranchAndBound& bab, - ProofNodeManager* pnm) + Env& env, + BranchAndBound& bab) : d_containing(containing), + d_env(env), d_foundNl(false), d_rowTracking(), d_bab(bab), - d_pnm(pnm), + d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() + : nullptr), d_checker(), - d_pfGen(new EagerProofGenerator(d_pnm, u)), - d_constraintDatabase(c, - u, + d_pfGen(new EagerProofGenerator(d_pnm, d_env.getUserContext())), + d_constraintDatabase(d_env.getContext(), + d_env.getUserContext(), d_partialModel, d_congruenceManager, RaiseConflict(*this), @@ -106,15 +107,15 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_qflraStatus(Result::SAT_UNKNOWN), d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), - d_learner(u), - d_assertionsThatDoNotMatchTheirLiterals(c), + d_learner(d_env.getUserContext()), + d_assertionsThatDoNotMatchTheirLiterals(d_env.getContext()), d_nextIntegerCheckVar(0), - d_constantIntegerVariables(c), - d_diseqQueue(c, false), + d_constantIntegerVariables(d_env.getContext()), + d_diseqQueue(d_env.getContext(), false), d_currentPropagationList(), - d_learnedBounds(c), - d_preregisteredNodes(u), - d_partialModel(c, DeltaComputeCallback(*this)), + d_learnedBounds(d_env.getContext()), + d_preregisteredNodes(d_env.getUserContext()), + d_partialModel(d_env.getContext(), DeltaComputeCallback(*this)), d_errorSet( d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)), d_tableau(), @@ -122,22 +123,23 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)), - d_diosolver(c), + d_diosolver(d_env.getContext()), d_restartsCounter(0), d_tableauSizeHasBeenModified(false), d_tableauResetDensity(1.6), d_tableauResetPeriod(10), - d_conflicts(c), - d_blackBoxConflict(c, Node::null()), - d_blackBoxConflictPf(c, std::shared_ptr<ProofNode>(nullptr)), - d_congruenceManager(c, - u, + d_conflicts(d_env.getContext()), + d_blackBoxConflict(d_env.getContext(), Node::null()), + d_blackBoxConflictPf(d_env.getContext(), + std::shared_ptr<ProofNode>(nullptr)), + d_congruenceManager(d_env.getContext(), + d_env.getUserContext(), d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseEqualityEngineConflict(*this), d_pnm), - d_cmEnabled(c, options::arithCongMan()), + d_cmEnabled(d_env.getContext(), options().arith.arithCongMan), d_dualSimplex( d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), @@ -149,22 +151,22 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_pass1SDP(NULL), d_otherSDP(NULL), - d_lastContextIntegerAttempted(c, -1), + d_lastContextIntegerAttempted(d_env.getContext(), -1), d_DELTA_ZERO(0), - d_approxCuts(c), + d_approxCuts(d_env.getContext()), d_fullCheckCounter(0), - d_cutCount(c, 0), - d_cutInContext(c), - d_likelyIntegerInfeasible(c, false), - d_guessedCoeffSet(c, false), + d_cutCount(d_env.getContext(), 0), + d_cutInContext(d_env.getContext()), + d_likelyIntegerInfeasible(d_env.getContext(), false), + d_guessedCoeffSet(d_env.getContext(), false), d_guessedCoeffs(), d_treeLog(NULL), d_replayVariables(), d_replayConstraints(), d_lhsTmp(), d_approxStats(NULL), - d_attemptSolveIntTurnedOff(u, 0), + d_attemptSolveIntTurnedOff(d_env.getUserContext(), 0), d_dioSolveResources(0), d_solveIntMaybeHelp(0u), d_solveIntAttempts(0u), @@ -508,13 +510,13 @@ bool TheoryArithPrivate::getDioCuttingResource(){ if(d_dioSolveResources > 0){ d_dioSolveResources--; if(d_dioSolveResources == 0){ - d_dioSolveResources = -options::rrTurns(); + d_dioSolveResources = -options().arith.rrTurns; } return true; }else{ d_dioSolveResources++; if(d_dioSolveResources >= 0){ - d_dioSolveResources = options::dioSolverTurns(); + d_dioSolveResources = options().arith.dioSolverTurns; } return false; } @@ -1046,7 +1048,7 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert( // Add the substitution if not recursive Assert(elim == Rewriter::rewrite(elim)); - if (right.size() > options::ppAssertMaxSubSize()) + if (right.size() > options().arith.ppAssertMaxSubSize) { Debug("simplify") << "TheoryArithPrivate::solve(): did not substitute due to the " @@ -1881,7 +1883,10 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em if(d_qflraStatus == Result::UNSAT){ return false; } if(emmmittedLemmaOrSplit){ return false; } - if(!options::useApprox()){ return false; } + if (!options().arith.useApprox) + { + return false; + } if(!ApproximateSimplex::enabled()){ return false; } if(Theory::fullEffort(effortLevel)){ @@ -1901,8 +1906,10 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em } } - - if(!options::trySolveIntStandardEffort()){ return false; } + if (!options().arith.trySolveIntStandardEffort) + { + return false; + } if (d_lastContextIntegerAttempted <= (level >> 2)) { @@ -2066,7 +2073,8 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint( if(d_partialModel.hasNode(v)){ d_lhsTmp.set(v, Rational(1)); double dval = nl.branchValue(); - Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval); + std::optional<Rational> maybe_value = + ApproximateSimplex::estimateWithCFE(dval); if (!maybe_value) { return make_pair(NullConstraint, ARITHVAR_SENTINEL); @@ -2350,7 +2358,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex if(ci->reconstructed() && ci->proven()){ const DenseMap<Rational>& row = ci->getReconstruction().lhs; - reject = !complexityBelow(row, options::replayRejectCutSize()); + reject = !complexityBelow(row, options().arith.replayRejectCutSize); } } if(conflictQueueEmpty()){ @@ -2398,8 +2406,9 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex /* check if the system is feasible under with the cuts */ if(conflictQueueEmpty()){ - Assert(options::replayEarlyCloseDepths() >= 1); - if(!nl.isBranch() || depth % options::replayEarlyCloseDepths() == 0 ){ + Assert(options().arith.replayEarlyCloseDepths >= 1); + if (!nl.isBranch() || depth % options().arith.replayEarlyCloseDepths == 0) + { TimerStat::CodeTimer codeTimer(d_statistics.d_replaySimplexTimer); //test for linear feasibility d_partialModel.stopQueueingBoundCounts(); @@ -2513,8 +2522,8 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex resolveOutPropagated(res, propagated); Debug("approx::replayLogRec") << "replayLogRec() ending" << std::endl; - - if(options::replayFailureLemma()){ + if (options().arith.replayFailureLemma) + { // must be done inside the sat context to get things // propagated at this level if(res.empty() && nid == getTreeLog().getRootId()){ @@ -2609,7 +2618,8 @@ Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx, if(d_partialModel.hasNode(v)){ Node n = d_partialModel.asNode(v); double dval = bn.branchValue(); - Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval); + std::optional<Rational> maybe_value = + ApproximateSimplex::estimateWithCFE(dval); if (!maybe_value) { return Node::null(); @@ -2656,7 +2666,8 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){ Assert(cut->proven()); const DenseMap<Rational>& row = cut->getReconstruction().lhs; - if(!complexityBelow(row, options::lemmaRejectCutSize())){ + if (!complexityBelow(row, options().arith.lemmaRejectCutSize)) + { ++(d_statistics.d_cutsRejectedDuringLemmas); continue; } @@ -2743,7 +2754,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ } // if integers are attempted, - Assert(options::useApprox()); + Assert(options().arith.useApprox); Assert(ApproximateSimplex::enabled()); int level = getSatContext()->getLevel(); @@ -2766,8 +2777,9 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ approx->setOptCoeffs(d_guessedCoeffs); } static const int32_t depthForLikelyInfeasible = 10; - int maxDepthPass1 = d_likelyIntegerInfeasible ? - depthForLikelyInfeasible : options::maxApproxDepth(); + int maxDepthPass1 = d_likelyIntegerInfeasible + ? depthForLikelyInfeasible + : options().arith.maxApproxDepth; approx->setBranchingDepth(maxDepthPass1); approx->setBranchOnVariableLimit(100); LinResult relaxRes = approx->solveRelaxation(); @@ -2830,7 +2842,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ } } if(!(anyConflict() || !d_approxCuts.empty())){ - turnOffApproxFor(options::replayNumericFailurePenalty()); + turnOffApproxFor(options().arith.replayNumericFailurePenalty); } break; case BranchesExhausted: @@ -2870,11 +2882,16 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){ if(pass1){ if(d_pass1SDP == NULL){ - if(options::useFC()){ + if (options().arith.useFC) + { d_pass1SDP = (SimplexDecisionProcedure*)(&d_fcSimplex); - }else if(options::useSOI()){ + } + else if (options().arith.useSOI) + { d_pass1SDP = (SimplexDecisionProcedure*)(&d_soiSimplex); - }else{ + } + else + { d_pass1SDP = (SimplexDecisionProcedure*)(&d_dualSimplex); } } @@ -2882,13 +2899,18 @@ SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){ return *d_pass1SDP; }else{ if(d_otherSDP == NULL){ - if(options::useFC()){ - d_otherSDP = (SimplexDecisionProcedure*)(&d_fcSimplex); - }else if(options::useSOI()){ - d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex); - }else{ - d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex); - } + if (options().arith.useFC) + { + d_otherSDP = (SimplexDecisionProcedure*)(&d_fcSimplex); + } + else if (options().arith.useSOI) + { + d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex); + } + else + { + d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex); + } } Assert(d_otherSDP != NULL); return *d_otherSDP; @@ -2909,8 +2931,8 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu } if(d_qflraStatus != Result::UNSAT){ - static const int32_t pass2Limit = 20; - int16_t oldCap = options::arithStandardCheckVarOrderPivots(); + static const int64_t pass2Limit = 20; + int64_t oldCap = options().arith.arithStandardCheckVarOrderPivots; Options::current().arith.arithStandardCheckVarOrderPivots = pass2Limit; SimplexDecisionProcedure& simplex = selectSimplex(false); d_qflraStatus = simplex.findModel(false); @@ -2961,20 +2983,19 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ d_partialModel.processBoundsQueue(utcb); d_linEq.startTrackingBoundCounts(); - bool noPivotLimit = Theory::fullEffort(effortLevel) || - !options::restrictedPivots(); + bool noPivotLimit = + Theory::fullEffort(effortLevel) || !options().arith.restrictedPivots; SimplexDecisionProcedure& simplex = selectSimplex(true); - bool useApprox = options::useApprox() && ApproximateSimplex::enabled() && getSolveIntegerResource(); + bool useApprox = options().arith.useApprox && ApproximateSimplex::enabled() + && getSolveIntegerResource(); Debug("TheoryArithPrivate::solveRealRelaxation") - << "solveRealRelaxation() approx" - << " " << options::useApprox() - << " " << ApproximateSimplex::enabled() - << " " << useApprox - << " " << safeToCallApprox() - << endl; + << "solveRealRelaxation() approx" + << " " << options().arith.useApprox << " " + << ApproximateSimplex::enabled() << " " << useApprox << " " + << safeToCallApprox() << endl; bool noPivotLimitPass1 = noPivotLimit && !useApprox; d_qflraStatus = simplex.findModel(noPivotLimitPass1); @@ -3133,7 +3154,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) if(anyConflict()){ d_qflraStatus = Result::UNSAT; - if (options::revertArithModels() && d_previousStatus == Result::SAT) + if (options().arith.revertArithModels && d_previousStatus == Result::SAT) { ++d_statistics.d_revertsOnConflicts; Debug("arith::bt") << "clearing here " @@ -3208,10 +3229,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) if(Debug.isOn("arith::consistency")){ Assert(entireStateIsConsistent("sat comit")); } - if(useSimplex && options::collectPivots()){ - if(options::useFC()){ + if (useSimplex && options().arith.collectPivots) + { + if (options().arith.useFC) + { d_statistics.d_satPivots << d_fcSimplex.getPivots(); - }else{ + } + else + { d_statistics.d_satPivots << d_dualSimplex.getPivots(); } } @@ -3226,10 +3251,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) d_partialModel.commitAssignmentChanges(); d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow); - if(useSimplex && options::collectPivots()){ - if(options::useFC()){ + if (useSimplex && options().arith.collectPivots) + { + if (options().arith.useFC) + { d_statistics.d_unknownPivots << d_fcSimplex.getPivots(); - }else{ + } + else + { d_statistics.d_unknownPivots << d_dualSimplex.getPivots(); } } @@ -3252,10 +3281,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) emmittedConflictOrSplit = true; Debug("arith::conflict") << "simplex conflict" << endl; - if(useSimplex && options::collectPivots()){ - if(options::useFC()){ + if (useSimplex && options().arith.collectPivots) + { + if (options().arith.useFC) + { d_statistics.d_unsatPivots << d_fcSimplex.getPivots(); - }else{ + } + else + { d_statistics.d_unsatPivots << d_dualSimplex.getPivots(); } } @@ -3265,8 +3298,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } d_statistics.d_avgUnknownsInARow << d_unknownsInARow; - size_t nPivots = - options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots(); + size_t nPivots = options().arith.useFC ? d_fcSimplex.getPivots() + : d_dualSimplex.getPivots(); for (std::size_t i = 0; i < nPivots; ++i) { d_containing.d_out->spendResource( @@ -3295,9 +3328,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) // This should be fine if sat or unknown if (!emmittedConflictOrSplit - && (options::arithPropagationMode() + && (options().arith.arithPropagationMode == options::ArithPropagationMode::UNATE_PROP - || options::arithPropagationMode() + || options().arith.arithPropagationMode == options::ArithPropagationMode::BOTH_PROP)) { TimerStat::CodeTimer codeTimer0(d_statistics.d_newPropTime); @@ -3380,7 +3413,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel) && !hasIntegerModel()){ Node possibleConflict = Node::null(); - if(!emmittedConflictOrSplit && options::arithDioSolver()){ + if (!emmittedConflictOrSplit && options().arith.arithDioSolver) + { possibleConflict = callDioSolver(); if(possibleConflict != Node::null()){ revertOutOfConflict(); @@ -3392,7 +3426,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } } - if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){ + if (!emmittedConflictOrSplit && d_hasDoneWorkSinceCut + && options().arith.arithDioSolver) + { if(getDioCuttingResource()){ TrustNode possibleLemma = dioCutting(); if(!possibleLemma.isNull()){ @@ -3422,7 +3458,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } } - if(options::maxCutsInContext() <= d_cutCount){ + if (options().arith.maxCutsInContext <= d_cutCount) + { if(d_diosolver.hasMoreDecompositionLemmas()){ while(d_diosolver.hasMoreDecompositionLemmas()){ Node decompositionLemma = d_diosolver.nextDecompositionLemma(); @@ -3494,7 +3531,8 @@ std::vector<ArithVar> TheoryArithPrivate::cutAllBounded() const{ vector<ArithVar> lemmas; ArithVar max = d_partialModel.getNumberOfVariables(); - if(options::doCutAllBounded() && max > 0){ + if (options().arith.doCutAllBounded && max > 0) + { for(ArithVar iter = 0; iter != max; ++iter){ //Do not include slack variables const DeltaRational& d = d_partialModel.getAssignment(iter); @@ -3642,15 +3680,18 @@ TrustNode TheoryArithPrivate::explain(TNode n) void TheoryArithPrivate::propagate(Theory::Effort e) { // This uses model values for safety. Disable for now. if (d_qflraStatus == Result::SAT - && (options::arithPropagationMode() + && (options().arith.arithPropagationMode == options::ArithPropagationMode::BOUND_INFERENCE_PROP - || options::arithPropagationMode() + || options().arith.arithPropagationMode == options::ArithPropagationMode::BOTH_PROP) && hasAnyUpdates()) { - if(options::newProp()){ + if (options().arith.newProp) + { propagateCandidatesNew(); - }else{ + } + else + { propagateCandidates(); } } @@ -4019,8 +4060,10 @@ void TheoryArithPrivate::presolve(){ } vector<TrustNode> lemmas; - if(!options::incrementalSolving()) { - switch(options::arithUnateLemmaMode()){ + if (!options().base.incrementalSolving) + { + switch (options().arith.arithUnateLemmaMode) + { case options::ArithUnateLemmaMode::NO: break; case options::ArithUnateLemmaMode::INEQUALITY: d_constraintDatabase.outputUnateInequalityLemmas(lemmas); @@ -4032,7 +4075,7 @@ void TheoryArithPrivate::presolve(){ d_constraintDatabase.outputUnateInequalityLemmas(lemmas); d_constraintDatabase.outputUnateEqualityLemmas(lemmas); break; - default: Unhandled() << options::arithUnateLemmaMode(); + default: Unhandled() << options().arith.arithUnateLemmaMode; } } @@ -4180,10 +4223,14 @@ void TheoryArithPrivate::propagateCandidates(){ DenseSet::const_iterator end = d_updatedBounds.end(); for(; i != end; ++i){ ArithVar var = *i; - if(d_tableau.isBasic(var) && - d_tableau.basicRowLength(var) <= options::arithPropagateMaxLength()){ + if (d_tableau.isBasic(var) + && d_tableau.basicRowLength(var) + <= options().arith.arithPropagateMaxLength) + { d_candidateBasics.softAdd(var); - }else{ + } + else + { Tableau::ColIterator basicIter = d_tableau.colIterator(var); for(; !basicIter.atEnd(); ++basicIter){ const Tableau::Entry& entry = *basicIter; @@ -4191,7 +4238,9 @@ void TheoryArithPrivate::propagateCandidates(){ ArithVar rowVar = d_tableau.rowIndexToBasic(ridx); Assert(entry.getColVar() == var); Assert(d_tableau.isBasic(rowVar)); - if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){ + if (d_tableau.getRowLength(ridx) + <= options().arith.arithPropagateMaxLength) + { d_candidateBasics.softAdd(rowVar); } } @@ -4425,7 +4474,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C // * coeffs[0] is for implied // * coeffs[i+1] is for explain[i] d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs); - if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){ + if (d_tableau.getRowLength(ridx) <= options().arith.arithPropAsLemmaLength) + { if (Debug.isOn("arith::prop::pf")) { for (const auto & constraint : explain) { Assert(constraint->hasProof()); @@ -4490,7 +4540,9 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C { outputLemma(clause, InferenceId::ARITH_ROW_IMPL); } - }else{ + } + else + { Assert(!implied->negationHasProof()); implied->impliedByFarkas(explain, coeffs, false); implied->tryToPropagate(); @@ -4518,9 +4570,9 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){ Debug("arith::prop") << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl; - if (rowLength >= options::arithPropagateMaxLength() + if (rowLength >= options().arith.arithPropagateMaxLength && Random::getRandom().pickWithProb( - 1.0 - double(options::arithPropagateMaxLength()) / rowLength)) + 1.0 - double(options().arith.arithPropagateMaxLength) / rowLength)) { return false; } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 4afe121b9..0cdc031e1 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -88,6 +88,9 @@ private: static const uint32_t RESET_START = 2; TheoryArith& d_containing; + Env& d_env; + + const Options& options() const { return d_env.getOptions(); } /** * Whether we encountered non-linear arithmetic at any time during solving. @@ -423,11 +426,7 @@ private: DeltaRational getDeltaValue(TNode term) const /* throw(DeltaRationalException, ModelException) */; public: - TheoryArithPrivate(TheoryArith& containing, - context::Context* c, - context::UserContext* u, - BranchAndBound& bab, - ProofNodeManager* pnm); + TheoryArithPrivate(TheoryArith& containing, Env& env, BranchAndBound& bab); ~TheoryArithPrivate(); //--------------------------------- initialization diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index 0d56dd6db..9d25dd760 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -175,63 +175,5 @@ bool ModelManager::collectModelBooleanVariables() return true; } -void ModelManager::collectAssertedTerms(TheoryId tid, - std::set<Node>& termSet, - bool includeShared) const -{ - Theory* t = d_te.theoryOf(tid); - // Collect all terms appearing in assertions - context::CDList<Assertion>::const_iterator assert_it = t->facts_begin(), - assert_it_end = t->facts_end(); - for (; assert_it != assert_it_end; ++assert_it) - { - collectTerms(tid, *assert_it, termSet); - } - - if (includeShared) - { - // Add terms that are shared terms - context::CDList<TNode>::const_iterator shared_it = t->shared_terms_begin(), - shared_it_end = - t->shared_terms_end(); - for (; shared_it != shared_it_end; ++shared_it) - { - collectTerms(tid, *shared_it, termSet); - } - } -} - -void ModelManager::collectTerms(TheoryId tid, - TNode n, - std::set<Node>& termSet) const -{ - const std::set<Kind>& irrKinds = d_model->getIrrelevantKinds(); - std::vector<TNode> visit; - TNode cur; - visit.push_back(n); - do - { - cur = visit.back(); - visit.pop_back(); - if (termSet.find(cur) != termSet.end()) - { - // already visited - continue; - } - Kind k = cur.getKind(); - // only add to term set if a relevant kind - if (irrKinds.find(k) == irrKinds.end()) - { - termSet.insert(cur); - } - // traverse owned terms, don't go under quantifiers - if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == tid) - && !cur.isClosure()) - { - visit.insert(visit.end(), cur.begin(), cur.end()); - } - } while (!visit.empty()); -} - } // namespace theory } // namespace cvc5 diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h index ff8459fcb..fd8ca6e11 100644 --- a/src/theory/model_manager.h +++ b/src/theory/model_manager.h @@ -108,22 +108,7 @@ class ModelManager * @return true if we are in conflict. */ bool collectModelBooleanVariables(); - /** - * Collect asserted terms for theory with the given identifier, add to - * termSet. - * - * @param tid The theory whose assertions we are collecting - * @param termSet The set to add terms to - * @param includeShared Whether to include the shared terms of the theory - */ - void collectAssertedTerms(TheoryId tid, - std::set<Node>& termSet, - bool includeShared = true) const; - /** - * Helper function for collectAssertedTerms, adds all subterms - * belonging to theory tid to termSet. - */ - void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const; + /** Reference to the theory engine */ TheoryEngine& d_te; /** Reference to the environment */ diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp index 4124407be..91e4cb6d4 100644 --- a/src/theory/model_manager_distributed.cpp +++ b/src/theory/model_manager_distributed.cpp @@ -81,11 +81,19 @@ bool ModelManagerDistributed::prepareModel() continue; } Theory* t = d_te.theoryOf(theoryId); + if (theoryId == TheoryId::THEORY_BOOL + || theoryId == TheoryId::THEORY_BUILTIN) + { + Trace("model-builder") + << " Skipping theory " << theoryId + << " as it does not contribute to the model anyway" << std::endl; + continue; + } Trace("model-builder") << " CollectModelInfo on theory: " << theoryId << std::endl; // collect the asserted terms std::set<Node> termSet; - collectAssertedTerms(theoryId, termSet); + t->collectAssertedTerms(termSet); // also get relevant terms t->computeRelevantTerms(termSet); if (!t->collectModelInfo(d_model.get(), termSet)) diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index ab237fc6c..8901ec314 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -111,7 +111,10 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f, int e) { options::UserPatMode upMode = getInstUserPatMode(); - if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST) + // we don't auto-generate triggers if the mode is trust or strict + if (hasUserPatterns(f) + && (upMode == options::UserPatMode::TRUST + || upMode == options::UserPatMode::STRICT)) { return InstStrategyStatus::STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index d490dce83..99949e223 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -200,11 +200,15 @@ bool InstantiationEngine::checkCompleteFor( Node q ) { void InstantiationEngine::checkOwnership(Node q) { - if( options::strictTriggers() && q.getNumChildren()==3 ){ + if (options::userPatternsQuant() == options::UserPatMode::STRICT + && q.getNumChildren() == 3) + { //if strict triggers, take ownership of this quantified formula bool hasPat = false; - for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ - if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){ + for (const Node& qc : q[2]) + { + if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN) + { hasPat = true; break; } diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 1abbd1989..33ed6f536 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -30,8 +30,7 @@ namespace quantifiers { bool QAttributes::isStandard() const { - return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull() - && !d_isInternal; + return !d_sygus && !d_quant_elim && !isFunDef() && !d_isInternal; } QuantAttributes::QuantAttributes() {} diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index b3fdd09da..910dbab5b 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -162,8 +162,7 @@ struct QAttributes * perform destructive updates (variable elimination, miniscoping, etc). * * A quantified formula is not standard if it is sygus, one for which - * we are performing quantifier elimination, is a function definition, or - * has a name. + * we are performing quantifier elimination, or is a function definition. */ bool isStandard() const; }; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 48106b858..02af92887 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -701,9 +701,65 @@ bool QuantifiersRewriter::isVarElim(Node v, Node s) return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType()); } -Node QuantifiersRewriter::getVarElimLitBv(Node lit, - const std::vector<Node>& args, - Node& var) +Node QuantifiersRewriter::getVarElimEq(Node lit, + const std::vector<Node>& args, + Node& var) +{ + Assert(lit.getKind() == EQUAL); + Node slv; + TypeNode tt = lit[0].getType(); + if (tt.isReal()) + { + slv = getVarElimEqReal(lit, args, var); + } + else if (tt.isBitVector()) + { + slv = getVarElimEqBv(lit, args, var); + } + else if (tt.isStringLike()) + { + slv = getVarElimEqString(lit, args, var); + } + return slv; +} + +Node QuantifiersRewriter::getVarElimEqReal(Node lit, + const std::vector<Node>& args, + Node& var) +{ + // for arithmetic, solve the equality + std::map<Node, Node> msum; + if (!ArithMSum::getMonomialSumLit(lit, msum)) + { + return Node::null(); + } + std::vector<Node>::const_iterator ita; + for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); + ++itm) + { + if (itm->first.isNull()) + { + continue; + } + ita = std::find(args.begin(), args.end(), itm->first); + if (ita != args.end()) + { + Node veq_c; + Node val; + int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL); + if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val)) + { + var = itm->first; + return val; + } + } + } + return Node::null(); +} + +Node QuantifiersRewriter::getVarElimEqBv(Node lit, + const std::vector<Node>& args, + Node& var) { if (Trace.isOn("quant-velim-bv")) { @@ -752,9 +808,9 @@ Node QuantifiersRewriter::getVarElimLitBv(Node lit, return Node::null(); } -Node QuantifiersRewriter::getVarElimLitString(Node lit, - const std::vector<Node>& args, - Node& var) +Node QuantifiersRewriter::getVarElimEqString(Node lit, + const std::vector<Node>& args, + Node& var) { Assert(lit.getKind() == EQUAL); NodeManager* nm = NodeManager::currentNM(); @@ -900,48 +956,10 @@ bool QuantifiersRewriter::getVarElimLit(Node lit, return true; } } - if (lit.getKind() == EQUAL && lit[0].getType().isReal() && pol) - { - // for arithmetic, solve the equality - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSumLit(lit, msum)) - { - for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ - if( !itm->first.isNull() ){ - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first ); - if( ita!=args.end() ){ - Assert(pol); - Node veq_c; - Node val; - int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL); - if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val)) - { - Trace("var-elim-quant") - << "Variable eliminate based on solved equality : " - << itm->first << " -> " << val << std::endl; - vars.push_back(itm->first); - subs.push_back(val); - args.erase(ita); - return true; - } - } - } - } - } - } if (lit.getKind() == EQUAL && pol) { Node var; - Node slv; - TypeNode tt = lit[0].getType(); - if (tt.isBitVector()) - { - slv = getVarElimLitBv(lit, args, var); - } - else if (tt.isStringLike()) - { - slv = getVarElimLitString(lit, args, var); - } + Node slv = getVarElimEq(lit, args, var); if (!slv.isNull()) { Assert(!var.isNull()); @@ -1797,7 +1815,7 @@ bool QuantifiersRewriter::doOperation(Node q, { bool is_strict_trigger = qa.d_hasPattern - && options::userPatternsQuant() == options::UserPatMode::TRUST; + && options::userPatternsQuant() == options::UserPatMode::STRICT; bool is_std = qa.isStandard() && !is_strict_trigger; if (computeOption == COMPUTE_ELIM_SYMBOLS) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index ae7f75f34..f0c3b0414 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -80,22 +80,34 @@ class QuantifiersRewriter : public TheoryRewriter std::vector<Node>& args, std::vector<Node>& vars, std::vector<Node>& subs); + /** + * Get variable eliminate for an equality based on theory-specific reasoning. + */ + static Node getVarElimEq(Node lit, const std::vector<Node>& args, Node& var); + /** variable eliminate for real equalities + * + * If this returns a non-null value ret, then var is updated to a member of + * args, lit is equivalent to ( var = ret ). + */ + static Node getVarElimEqReal(Node lit, + const std::vector<Node>& args, + Node& var); /** variable eliminate for bit-vector equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimLitBv(Node lit, - const std::vector<Node>& args, - Node& var); + static Node getVarElimEqBv(Node lit, + const std::vector<Node>& args, + Node& var); /** variable eliminate for string equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimLitString(Node lit, - const std::vector<Node>& args, - Node& var); + static Node getVarElimEqString(Node lit, + const std::vector<Node>& args, + Node& var); /** get variable elimination * * If n asserted with polarity pol entails a literal lit that corresponds diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index b774d456a..5ca1979b3 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -387,6 +387,60 @@ void Theory::computeRelevantTerms(std::set<Node>& termSet) // by default, there are no additional relevant terms } +void Theory::collectAssertedTerms(std::set<Node>& termSet, + bool includeShared) const +{ + // Collect all terms appearing in assertions + context::CDList<Assertion>::const_iterator assert_it = facts_begin(), + assert_it_end = facts_end(); + for (; assert_it != assert_it_end; ++assert_it) + { + collectTerms(*assert_it, termSet); + } + + if (includeShared) + { + // Add terms that are shared terms + context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), + shared_it_end = shared_terms_end(); + for (; shared_it != shared_it_end; ++shared_it) + { + collectTerms(*shared_it, termSet); + } + } +} + +void Theory::collectTerms(TNode n, std::set<Node>& termSet) const +{ + const std::set<Kind>& irrKinds = + d_theoryState->getModel()->getIrrelevantKinds(); + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (termSet.find(cur) != termSet.end()) + { + // already visited + continue; + } + Kind k = cur.getKind(); + // only add to term set if a relevant kind + if (irrKinds.find(k) == irrKinds.end()) + { + termSet.insert(cur); + } + // traverse owned terms, don't go under quantifiers + if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == d_id) + && !cur.isClosure()) + { + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } while (!visit.empty()); +} + bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { return true; @@ -620,7 +674,7 @@ bool Theory::usesCentralEqualityEngine(TheoryId id) } return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS - || id == THEORY_SEP || id == THEORY_ARRAYS; + || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV; } bool Theory::expUsingCentralEqualityEngine(TheoryId id) diff --git a/src/theory/theory.h b/src/theory/theory.h index a857931a8..bde00b908 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -450,6 +450,11 @@ class Theory { Env& getEnv() const { return d_env; } /** + * Shorthand to access the options object. + */ + const Options& options() const { return getEnv().getOptions(); } + + /** * Get the SAT context associated to this Theory. */ context::Context* getSatContext() const { return d_env.getContext(); } @@ -639,6 +644,19 @@ class Theory { */ virtual void computeRelevantTerms(std::set<Node>& termSet); /** + * Collect asserted terms for this theory and add them to termSet. + * + * @param termSet The set to add terms to + * @param includeShared Whether to include the shared terms of the theory + */ + void collectAssertedTerms(std::set<Node>& termSet, + bool includeShared = true) const; + /** + * Helper function for collectAssertedTerms, adds all subterms + * belonging to this theory to termSet. + */ + void collectTerms(TNode n, std::set<Node>& termSet) const; + /** * Collect model values, after equality information is added to the model. * The argument termSet is the set of relevant terms returned by * computeRelevantTerms. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 21c22586b..12d3fccfe 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -303,7 +303,16 @@ void TheoryEngine::preRegister(TNode preprocessed) { // the atom should not have free variables Debug("theory") << "TheoryEngine::preRegister: " << preprocessed << std::endl; - Assert(!expr::hasFreeVar(preprocessed)); + if (Configuration::isAssertionBuild()) + { + std::unordered_set<Node> fvs; + expr::getFreeVariables(preprocessed, fvs); + if (!fvs.empty()) + { + Unhandled() << "Preregistered term with free variable: " + << preprocessed << ", fv=" << *fvs.begin(); + } + } // should not have witness Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed)); diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 58a66ef46..cc58347bf 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -47,6 +47,8 @@ class TheoryState context::UserContext* getUserContext() const; /** Get the environment */ Env& getEnv() const { return d_env; } + /** Get the options */ + const Options& options() const { return getEnv().getOptions(); } //-------------------------------------- equality information /** Is t registered as a term in the equality engine of this class? */ virtual bool hasTerm(TNode a) const; |