diff options
Diffstat (limited to 'src/theory')
24 files changed, 290 insertions, 239 deletions
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 3dff64113..8f10d7611 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -23,8 +23,8 @@ #include "base/output.h" #include "expr/skolem_manager.h" #include "options/base_options.h" -#include "options/smt_options.h" #include "preprocessing/util/ite_utilities.h" +#include "smt/env.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" #include "theory/rewriter.h" @@ -144,14 +144,15 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ } ArithIteUtils::ArithIteUtils( + Env& env, preprocessing::util::ContainsTermITEVisitor& contains, - context::Context* uc, SubstitutionMap& subs) - : d_contains(contains), + : EnvObj(env), + d_contains(contains), d_subs(subs), d_one(1), - d_subcount(uc, 0), - d_skolems(uc), + d_subcount(userContext(), 0), + d_skolems(userContext()), d_implies(), d_orBinEqs() { @@ -273,7 +274,7 @@ void ArithIteUtils::addSubstitution(TNode f, TNode t){ } Node ArithIteUtils::applySubstitutions(TNode f){ - AlwaysAssert(!options::incrementalSolving()); + AlwaysAssert(!options().base.incrementalSolving); return d_subs.apply(f); } @@ -287,7 +288,7 @@ Node ArithIteUtils::selectForCmp(Node n) const{ } void ArithIteUtils::learnSubstitutions(const std::vector<Node>& assertions){ - AlwaysAssert(!options::incrementalSolving()); + AlwaysAssert(!options().base.incrementalSolving); for(size_t i=0, N=assertions.size(); i < N; ++i){ collectAssertions(assertions[i]); } diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index ba7a23479..6cb7a0855 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -28,6 +28,7 @@ #include "context/cdinsert_hashmap.h" #include "context/cdo.h" #include "expr/node.h" +#include "smt/env_obj.h" #include "util/integer.h" namespace cvc5 { @@ -43,7 +44,8 @@ class SubstitutionMap; namespace arith { -class ArithIteUtils { +class ArithIteUtils : protected EnvObj +{ preprocessing::util::ContainsTermITEVisitor& d_contains; SubstitutionMap& d_subs; @@ -62,7 +64,7 @@ class ArithIteUtils { Integer d_one; - context::CDO<unsigned> d_subcount; + context::CDO<uint64_t> d_subcount; typedef context::CDInsertHashMap<Node, Node> CDNodeMap; CDNodeMap d_skolems; @@ -72,8 +74,8 @@ class ArithIteUtils { std::vector<Node> d_orBinEqs; public: - ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains, - context::Context* userContext, + ArithIteUtils(Env& env, + preprocessing::util::ContainsTermITEVisitor& contains, SubstitutionMap& subs); ~ArithIteUtils(); diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 33b0e2e26..11a9cc6f2 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -31,9 +31,13 @@ namespace cvc5 { namespace theory { namespace arith { -AttemptSolutionSDP::AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) - : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc) - , d_statistics() +AttemptSolutionSDP::AttemptSolutionSDP(Env& env, + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc) + : SimplexDecisionProcedure(env, linEq, errors, conflictChannel, tvmalloc), + d_statistics() { } AttemptSolutionSDP::Statistics::Statistics() diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 8c6b28b60..2bf4948a4 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -65,19 +65,24 @@ namespace arith { class AttemptSolutionSDP : public SimplexDecisionProcedure { public: - AttemptSolutionSDP(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); + AttemptSolutionSDP(Env& env, + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc); - Result::Sat attempt(const ApproximateSimplex::Solution& sol); + Result::Sat attempt(const ApproximateSimplex::Solution& sol); - Result::Sat findModel(bool exactResult) override { Unreachable(); } + Result::Sat findModel(bool exactResult) override { Unreachable(); } - private: - bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const; +private: + bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const; - bool processSignals(){ - TimerStat &timer = d_statistics.d_queueTime; - IntStat& conflictStat = d_statistics.d_conflicts; - return standardProcessSignals(timer, conflictStat); + bool processSignals() + { + TimerStat& timer = d_statistics.d_queueTime; + IntStat& conflictStat = d_statistics.d_conflicts; + return standardProcessSignals(timer, conflictStat); } /** These fields are designed to be accessible to TheoryArith methods. */ class Statistics { diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 3a35319ed..f7d274484 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -22,6 +22,7 @@ #include "options/arith_options.h" #include "proof/proof_node.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/constraint.h" @@ -36,33 +37,33 @@ namespace theory { namespace arith { ArithCongruenceManager::ArithCongruenceManager( - context::Context* c, - context::UserContext* u, + Env& env, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, - RaiseEqualityEngineConflict raiseConflict, - ProofNodeManager* pnm) - : d_inConflict(c), + RaiseEqualityEngineConflict raiseConflict) + : EnvObj(env), + d_inConflict(context()), d_raiseConflict(raiseConflict), d_notify(*this), - d_keepAlive(c), - d_propagatations(c), - d_explanationMap(c), + d_keepAlive(context()), + d_propagatations(context()), + d_explanationMap(context()), d_constraintDatabase(cd), d_setupLiteral(setup), d_avariables(avars), d_ee(nullptr), - d_satContext(c), - d_userContext(u), - d_pnm(pnm), + d_satContext(context()), + d_userContext(userContext()), + d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() + : nullptr), // Construct d_pfGenEe with the SAT context, since its proof include // unclosed assumptions of theory literals. - d_pfGenEe( - new EagerProofGenerator(pnm, c, "ArithCongruenceManager::pfGenEe")), + d_pfGenEe(new EagerProofGenerator( + d_pnm, context(), "ArithCongruenceManager::pfGenEe")), // Construct d_pfGenEe with the USER context, since its proofs are closed. d_pfGenExplain(new EagerProofGenerator( - pnm, u, "ArithCongruenceManager::pfGenExplain")), + d_pnm, userContext(), "ArithCongruenceManager::pfGenExplain")), d_pfee(nullptr) { } @@ -71,7 +72,7 @@ ArithCongruenceManager::~ArithCongruenceManager() {} bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi) { - Assert(!options::arithEqSolver()); + Assert(!options().arith.arithEqSolver); esi.d_notify = &d_notify; esi.d_name = "arithCong::ee"; return true; @@ -79,7 +80,7 @@ bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi) void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee) { - if (options::arithEqSolver()) + if (options().arith.arithEqSolver) { // use our own copy d_allocEe.reset( diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 2c59a405f..3050f5821 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -25,6 +25,7 @@ #include "context/cdmaybe.h" #include "context/cdtrail_queue.h" #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" @@ -55,8 +56,9 @@ namespace arith { class ArithVariables; -class ArithCongruenceManager { -private: +class ArithCongruenceManager : protected EnvObj +{ + private: context::CDRaised d_inConflict; RaiseEqualityEngineConflict d_raiseConflict; @@ -227,13 +229,11 @@ private: TrustNode explainInternal(TNode internal); public: - ArithCongruenceManager(context::Context* satContext, - context::UserContext* u, + ArithCongruenceManager(Env& env, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, - RaiseEqualityEngineConflict raiseConflict, - ProofNodeManager* pnm); + RaiseEqualityEngineConflict raiseConflict); ~ArithCongruenceManager(); //--------------------------------- initialization @@ -296,7 +296,7 @@ private: Statistics(); } d_statistics; -};/* class ArithCongruenceManager */ +}; /* class ArithCongruenceManager */ std::vector<Node> andComponents(TNode an); diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 19bd2f2bf..08e9edc79 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -21,6 +21,7 @@ #include "base/output.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" +#include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/partial_model.h" @@ -38,21 +39,24 @@ inline Node makeIntegerVariable(){ "is an integer variable created by the dio solver"); } -DioSolver::DioSolver(context::Context* ctxt) - : d_lastUsedProofVariable(ctxt, 0), - d_inputConstraints(ctxt), - d_nextInputConstraintToEnqueue(ctxt, 0), - d_trail(ctxt), - d_subs(ctxt), +DioSolver::DioSolver(Env& env) + : EnvObj(env), + d_lastUsedProofVariable(context(), 0), + d_inputConstraints(context()), + d_nextInputConstraintToEnqueue(context(), 0), + d_trail(context()), + d_subs(context()), d_currentF(), - d_savedQueue(ctxt), - d_savedQueueIndex(ctxt, 0), - d_conflictIndex(ctxt), - d_maxInputCoefficientLength(ctxt, 0), - d_usedDecomposeIndex(ctxt, false), - d_lastPureSubstitution(ctxt, 0), - d_pureSubstitionIter(ctxt, 0), - d_decompositionLemmaQueue(ctxt) {} + d_savedQueue(context()), + d_savedQueueIndex(context(), 0), + d_conflictIndex(context()), + d_maxInputCoefficientLength(context(), 0), + d_usedDecomposeIndex(context(), false), + d_lastPureSubstitution(context(), 0), + d_pureSubstitionIter(context(), 0), + d_decompositionLemmaQueue(context()) +{ +} DioSolver::Statistics::Statistics() : d_conflictCalls(smtStatisticsRegistry().registerInt( @@ -812,7 +816,8 @@ void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){ } void DioSolver::addTrailElementAsLemma(TrailIndex i) { - if(options::exportDioDecompositions()){ + if (options().arith.exportDioDecompositions) + { d_decompositionLemmaQueue.push(i); } } diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 8f2411036..6be26e854 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -26,6 +26,7 @@ #include "context/cdmaybe.h" #include "context/cdo.h" #include "context/cdqueue.h" +#include "smt/env_obj.h" #include "theory/arith/normal_form.h" #include "util/rational.h" #include "util/statistics_stats.h" @@ -37,8 +38,9 @@ class Context; namespace theory { namespace arith { -class DioSolver { -private: +class DioSolver : protected EnvObj +{ + private: typedef size_t TrailIndex; typedef size_t InputConstraintIndex; typedef size_t SubIndex; @@ -176,11 +178,12 @@ private: public: /** Construct a Diophantine equation solver with the given context. */ - DioSolver(context::Context* ctxt); + DioSolver(Env& env); - /** Returns true if the substitutions use no new variables. */ - bool hasMorePureSubstitutions() const{ - return d_pureSubstitionIter < d_lastPureSubstitution; + /** Returns true if the substitutions use no new variables. */ + bool hasMorePureSubstitutions() const + { + return d_pureSubstitionIter < d_lastPureSubstitution; } Node nextPureSubstitution(); @@ -416,7 +419,7 @@ public: }; Statistics d_statistics; -};/* class DioSolver */ +}; /* class DioSolver */ } // namespace arith } // namespace theory diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 16ce2f4c0..ea7773f76 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -17,6 +17,7 @@ #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" @@ -29,10 +30,15 @@ namespace cvc5 { namespace theory { namespace arith { -DualSimplexDecisionProcedure::DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) - : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc) - , d_pivotsInRound() - , d_statistics(d_pivots) +DualSimplexDecisionProcedure::DualSimplexDecisionProcedure( + Env& env, + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc) + : SimplexDecisionProcedure(env, linEq, errors, conflictChannel, tvmalloc), + d_pivotsInRound(), + d_statistics(d_pivots) { } DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots) @@ -86,10 +92,11 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){ static const bool verbose = false; exactResult |= d_varOrderPivotLimit < 0; - uint32_t checkPeriod = options::arithSimplexCheckPeriod(); + uint32_t checkPeriod = options().arith.arithSimplexCheckPeriod; if(result == Result::SAT_UNKNOWN){ - uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ? - d_numVariables + 1 : options::arithHeuristicPivots(); + uint32_t numDifferencePivots = options().arith.arithHeuristicPivots < 0 + ? d_numVariables + 1 + : options().arith.arithHeuristicPivots; // The signed to unsigned conversion is safe. if(numDifferencePivots > 0){ @@ -187,17 +194,15 @@ bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingI --remainingIterations; - bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= options::arithPivotThreshold(); + bool useVarOrderPivot = + d_pivotsInRound.count(x_i) >= options().arith.arithPivotThreshold; if(!useVarOrderPivot){ d_pivotsInRound.add(x_i); } - - Debug("arith::update") - << "pivots in rounds: " << d_pivotsInRound.count(x_i) - << " use " << useVarOrderPivot - << " threshold " << options::arithPivotThreshold() - << endl; + Debug("arith::update") << "pivots in rounds: " << d_pivotsInRound.count(x_i) + << " use " << useVarOrderPivot << " threshold " + << options().arith.arithPivotThreshold << std::endl; LinearEqualityModule::VarPreferenceFunction pf = useVarOrderPivot ? &LinearEqualityModule::minVarOrder : &LinearEqualityModule::minBoundAndColLength; diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index e1021d2a5..930b884ac 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -64,11 +64,15 @@ namespace arith { class DualSimplexDecisionProcedure : public SimplexDecisionProcedure{ public: - DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); + DualSimplexDecisionProcedure(Env& env, + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult) override - { - return dualFindModel(exactResult); + Result::Sat findModel(bool exactResult) override + { + return dualFindModel(exactResult); } private: diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index f706babda..54d19000b 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -29,11 +29,12 @@ namespace theory { namespace arith { FCSimplexDecisionProcedure::FCSimplexDecisionProcedure( + Env& env, LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) - : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc), + : SimplexDecisionProcedure(env, linEq, errors, conflictChannel, tvmalloc), d_focusSize(0), d_focusErrorVar(ARITHVAR_SENTINEL), d_focusCoefficients(), @@ -340,7 +341,7 @@ UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, Linear } } - CompPenaltyColLength colCmp(&d_linEq); + CompPenaltyColLength colCmp(&d_linEq, options().arith.havePenalties); CandVector::iterator i = candidates.begin(); CandVector::iterator end = candidates.end(); std::make_heap(i, end, colCmp); diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 599b324ce..ddd868aca 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -68,18 +68,22 @@ namespace arith { class FCSimplexDecisionProcedure : public SimplexDecisionProcedure{ public: - FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - - Result::Sat findModel(bool exactResult) override; - - // other error variables are dropping - WitnessImprovement dualLikeImproveError(ArithVar evar); - WitnessImprovement primalImproveError(ArithVar evar); - - // dual like - // - found conflict - // - satisfied error set - Result::Sat dualLike(); + FCSimplexDecisionProcedure(Env& env, + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc); + + Result::Sat findModel(bool exactResult) override; + + // other error variables are dropping + WitnessImprovement dualLikeImproveError(ArithVar evar); + WitnessImprovement primalImproveError(ArithVar evar); + + // dual like + // - found conflict + // - satisfied error set + Result::Sat dualLike(); private: static const uint32_t PENALTY = 4; diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 9a08530ec..5f177835b 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -730,13 +730,21 @@ struct Cand { class CompPenaltyColLength { private: LinearEqualityModule* d_mod; -public: - CompPenaltyColLength(LinearEqualityModule* mod): d_mod(mod){} + const bool d_havePenalties; + + public: + CompPenaltyColLength(LinearEqualityModule* mod, bool havePenalties) + : d_mod(mod), d_havePenalties(havePenalties) + { + } bool operator()(const Cand& x, const Cand& y) const { - if(x.d_penalty == y.d_penalty || !options::havePenalties()){ + if (x.d_penalty == y.d_penalty || !d_havePenalties) + { return x.d_nb == d_mod->minBoundAndColLength(x.d_nb,y.d_nb); - }else{ + } + else + { return x.d_penalty < y.d_penalty; } } diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index b63ebf29d..649ff2080 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -181,8 +181,8 @@ class TranscendentalSolver * * Indicates that the degree of the polynomials in the Taylor approximation of * all transcendental functions is 2*d_taylor_degree. This value is set - * initially to options::nlExtTfTaylorDegree() and may be incremented - * if the option options::nlExtTfIncPrecision() is enabled. + * initially to the nlExtTfTaylorDegree option and may be incremented + * if the option nlExtTfIncPrecision is enabled. */ uint64_t d_taylor_degree; diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 7b4e920fb..90f4a2cc7 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -21,6 +21,7 @@ #include "expr/bound_var_manager.h" #include "options/arith_options.h" #include "proof/conv_proof_generator.h" +#include "smt/env.h" #include "smt/logic_exception.h" #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" @@ -57,14 +58,14 @@ struct ToIntWitnessVarAttributeId using ToIntWitnessVarAttribute = expr::Attribute<ToIntWitnessVarAttributeId, Node>; -OperatorElim::OperatorElim(ProofNodeManager* pnm, const LogicInfo& info) - : EagerProofGenerator(pnm), d_info(info) +OperatorElim::OperatorElim(Env& env) + : EnvObj(env), EagerProofGenerator(d_env.getProofNodeManager()) { } void OperatorElim::checkNonLinearLogic(Node term) { - if (d_info.isLinear()) + if (d_env.getLogicInfo().isLinear()) { Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term << std::endl; @@ -424,7 +425,7 @@ Node OperatorElim::getArithSkolem(SkolemFunId id) } Node skolem; SkolemManager* sm = nm->getSkolemManager(); - if (options::arithNoPartialFun()) + if (options().arith.arithNoPartialFun) { // partial function: division, where we treat the skolem function as // a constant @@ -445,7 +446,7 @@ Node OperatorElim::getArithSkolem(SkolemFunId id) Node OperatorElim::getArithSkolemApp(Node n, SkolemFunId id) { Node skolem = getArithSkolem(id); - if (!options::arithNoPartialFun()) + if (!options().arith.arithNoPartialFun) { skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n); } diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index 27a3d293e..e2c0ab297 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -20,6 +20,7 @@ #include "expr/node.h" #include "expr/skolem_manager.h" #include "proof/eager_proof_generator.h" +#include "smt/env_obj.h" #include "theory/logic_info.h" #include "theory/skolem_lemma.h" @@ -30,10 +31,10 @@ class TConvProofGenerator; namespace theory { namespace arith { -class OperatorElim : public EagerProofGenerator +class OperatorElim : protected EnvObj, public EagerProofGenerator { public: - OperatorElim(ProofNodeManager* pnm, const LogicInfo& info); + OperatorElim(Env& env); ~OperatorElim() {} /** Eliminate operators in this term. * @@ -59,8 +60,6 @@ class OperatorElim : public EagerProofGenerator static Node getAxiomFor(Node n); private: - /** Logic info of the owner of this class */ - const LogicInfo& d_info; /** * Function symbols used to implement: * (1) Uninterpreted division-by-zero semantics. Needed to deal with partial diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp index 0f4d97b4d..4c72eb909 100644 --- a/src/theory/arith/pp_rewrite_eq.cpp +++ b/src/theory/arith/pp_rewrite_eq.cpp @@ -16,6 +16,7 @@ #include "theory/arith/pp_rewrite_eq.h" #include "options/arith_options.h" +#include "smt/env.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" @@ -23,16 +24,16 @@ namespace cvc5 { namespace theory { namespace arith { -PreprocessRewriteEq::PreprocessRewriteEq(context::Context* c, - ProofNodeManager* pnm) - : d_ppPfGen(pnm, c, "Arith::ppRewrite"), d_pnm(pnm) +PreprocessRewriteEq::PreprocessRewriteEq(Env& env) + : EnvObj(env), + d_ppPfGen(d_env.getProofNodeManager(), context(), "Arith::ppRewrite") { } TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom) { Assert(atom.getKind() == kind::EQUAL); - if (!options::arithRewriteEq()) + if (!options().arith.arithRewriteEq) { return TrustNode::null(); } @@ -43,20 +44,18 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom) Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << std::endl; // don't need to rewrite terms since rewritten is not a non-standard op - if (proofsEnabled()) + if (d_env.isTheoryProofProducing()) { Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH); return d_ppPfGen.mkTrustedRewrite( atom, rewritten, - d_pnm->mkNode( + d_env.getProofNodeManager()->mkNode( PfRule::THEORY_INFERENCE, {}, {atom.eqNode(rewritten), t})); } return TrustNode::mkTrustRewrite(atom, rewritten, nullptr); } -bool PreprocessRewriteEq::proofsEnabled() const { return d_pnm != nullptr; } - } // namespace arith } // namespace theory } // namespace cvc5 diff --git a/src/theory/arith/pp_rewrite_eq.h b/src/theory/arith/pp_rewrite_eq.h index fc022f1d8..792477440 100644 --- a/src/theory/arith/pp_rewrite_eq.h +++ b/src/theory/arith/pp_rewrite_eq.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "proof/eager_proof_generator.h" #include "proof/proof_node_manager.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -33,10 +34,10 @@ namespace arith { * * In particular, we may rewrite (= x y) to (and (>= x y) (<= x y)). */ -class PreprocessRewriteEq +class PreprocessRewriteEq : protected EnvObj { public: - PreprocessRewriteEq(context::Context* c, ProofNodeManager* pnm); + PreprocessRewriteEq(Env& env); ~PreprocessRewriteEq() {} /** * Preprocess equality, applies ppRewrite for equalities. This method is @@ -45,12 +46,8 @@ class PreprocessRewriteEq TrustNode ppRewriteEq(TNode eq); private: - /** Are proofs enabled? */ - bool proofsEnabled() const; /** Used to prove pp-rewrites */ EagerProofGenerator d_ppPfGen; - /** Proof node manager */ - ProofNodeManager* d_pnm; }; } // namespace arith diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index ed81f9e78..d5a9b9c0a 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -19,6 +19,7 @@ #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" @@ -31,26 +32,31 @@ namespace cvc5 { namespace theory { namespace arith { - -SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) - : d_pivots(0) - , d_conflictVariables() - , d_linEq(linEq) - , d_variables(d_linEq.getVariables()) - , d_tableau(d_linEq.getTableau()) - , d_errorSet(errors) - , d_numVariables(0) - , d_conflictChannel(conflictChannel) - , d_conflictBuilder(NULL) - , d_arithVarMalloc(tvmalloc) - , d_errorSize(0) - , d_zero(0) - , d_posOne(1) - , d_negOne(-1) +SimplexDecisionProcedure::SimplexDecisionProcedure( + Env& env, + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc) + : EnvObj(env), + d_pivots(0), + d_conflictVariables(), + d_linEq(linEq), + d_variables(d_linEq.getVariables()), + d_tableau(d_linEq.getTableau()), + d_errorSet(errors), + d_numVariables(0), + d_conflictChannel(conflictChannel), + d_conflictBuilder(NULL), + d_arithVarMalloc(tvmalloc), + d_errorSize(0), + d_zero(0), + d_posOne(1), + d_negOne(-1) { - d_heuristicRule = options::arithErrorSelectionRule(); + d_heuristicRule = options().arith.arithErrorSelectionRule; d_errorSet.setSelectionRule(d_heuristicRule); - d_conflictBuilder = new FarkasConflictBuilder(options::produceProofs()); + d_conflictBuilder = new FarkasConflictBuilder(options().smt.produceProofs); } SimplexDecisionProcedure::~SimplexDecisionProcedure(){ diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 8e36c1b54..f2fa8b6a6 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -58,6 +58,7 @@ #include <unordered_map> #include "options/arith_options.h" +#include "smt/env_obj.h" #include "theory/arith/arithvar.h" #include "theory/arith/partial_model.h" #include "util/dense_map.h" @@ -72,8 +73,9 @@ class ErrorSet; class LinearEqualityModule; class Tableau; -class SimplexDecisionProcedure { -protected: +class SimplexDecisionProcedure : protected EnvObj +{ + protected: typedef std::vector< std::pair<ArithVar, int> > AVIntPairVec; /** Pivot count of the current round of pivoting. */ @@ -145,74 +147,73 @@ protected: void shrinkInfeasFunc(TimerStat& timer, ArithVar inf, const ArithVarVec& dropped); public: - SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); - virtual ~SimplexDecisionProcedure(); - - /** - * Tries to update the assignments of variables such that all of the - * assignments are consistent with their bounds. - * This is done by a simplex search through the possible bases of the tableau. - * - * If all of the variables can be made consistent with their bounds - * SAT is returned. Otherwise UNSAT is returned, and at least 1 conflict - * was reported on the conflictCallback passed to the Module. - * - * Tableau pivoting is performed so variables may switch from being basic to - * nonbasic and vice versa. - * - * Corresponds to the "check()" procedure in [Cav06]. - */ - virtual Result::Sat findModel(bool exactResult) = 0; - - void increaseMax() { d_numVariables++; } - - - uint32_t getPivots() const { return d_pivots; } - - /** Set the variable ordering pivot limit */ - void setVarOrderPivotLimit(int64_t value) { d_varOrderPivotLimit = value; } - - protected: - - /** Reports a conflict to on the output channel. */ - void reportConflict(ArithVar basic); - - /** - * Checks a basic variable, b, to see if it is in conflict. - * If a conflict is discovered a node summarizing the conflict is returned. - * Otherwise, Node::null() is returned. - */ - bool maybeGenerateConflictForBasic(ArithVar basic) const; - - /** Returns true if a tracked basic variable has a conflict on it. */ - bool checkBasicForConflict(ArithVar b) const; - - /** - * If a basic variable has a conflict on its row, - * this produces a minimized row on the conflict channel. - */ - ConstraintCP generateConflictForBasic(ArithVar basic) const; - + SimplexDecisionProcedure(Env& env, + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc); + virtual ~SimplexDecisionProcedure(); + + /** + * Tries to update the assignments of variables such that all of the + * assignments are consistent with their bounds. + * This is done by a simplex search through the possible bases of the tableau. + * + * If all of the variables can be made consistent with their bounds + * SAT is returned. Otherwise UNSAT is returned, and at least 1 conflict + * was reported on the conflictCallback passed to the Module. + * + * Tableau pivoting is performed so variables may switch from being basic to + * nonbasic and vice versa. + * + * Corresponds to the "check()" procedure in [Cav06]. + */ + virtual Result::Sat findModel(bool exactResult) = 0; + + void increaseMax() { d_numVariables++; } + + uint32_t getPivots() const { return d_pivots; } + + /** Set the variable ordering pivot limit */ + void setVarOrderPivotLimit(int64_t value) { d_varOrderPivotLimit = value; } - /** Gets a fresh variable from TheoryArith. */ - ArithVar requestVariable(){ - return d_arithVarMalloc.request(); - } - - /** Releases a requested variable from TheoryArith.*/ - void releaseVariable(ArithVar v){ - d_arithVarMalloc.release(v); - } - - /** Post condition: !d_queue.moreSignals() */ - bool standardProcessSignals(TimerStat &timer, IntStat& conflictStat); - - struct ArithVarIntPairHashFunc { - size_t operator()(const std::pair<ArithVar, int>& p) const { - size_t h1 = std::hash<ArithVar>()(p.first); - size_t h2 = std::hash<int>()(p.second); - return h1 + 3389 * h2; - } +protected: + /** Reports a conflict to on the output channel. */ + void reportConflict(ArithVar basic); + + /** + * Checks a basic variable, b, to see if it is in conflict. + * If a conflict is discovered a node summarizing the conflict is returned. + * Otherwise, Node::null() is returned. + */ + bool maybeGenerateConflictForBasic(ArithVar basic) const; + + /** Returns true if a tracked basic variable has a conflict on it. */ + bool checkBasicForConflict(ArithVar b) const; + + /** + * If a basic variable has a conflict on its row, + * this produces a minimized row on the conflict channel. + */ + ConstraintCP generateConflictForBasic(ArithVar basic) const; + + /** Gets a fresh variable from TheoryArith. */ + ArithVar requestVariable() { return d_arithVarMalloc.request(); } + + /** Releases a requested variable from TheoryArith.*/ + void releaseVariable(ArithVar v) { d_arithVarMalloc.release(v); } + + /** Post condition: !d_queue.moreSignals() */ + bool standardProcessSignals(TimerStat& timer, IntStat& conflictStat); + + struct ArithVarIntPairHashFunc + { + size_t operator()(const std::pair<ArithVar, int>& p) const + { + size_t h1 = std::hash<ArithVar>()(p.first); + size_t h2 = std::hash<int>()(p.second); + return h1 + 3389 * h2; + } }; typedef std::unordered_map< std::pair<ArithVar, int>, ArithVarVec, ArithVarIntPairHashFunc> sgn_table; @@ -227,7 +228,7 @@ public: sgn_table::const_iterator find_sgns(const sgn_table& sgns, ArithVar col, int sgn); -};/* class SimplexDecisionProcedure */ +}; /* class SimplexDecisionProcedure */ } // namespace arith } // namespace theory diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 94f6742e3..d6cdb3a13 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -31,11 +31,12 @@ namespace cvc5 { namespace theory { namespace arith { -SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, +SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(Env& env, + LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc) - : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc), + : SimplexDecisionProcedure(env, linEq, errors, conflictChannel, tvmalloc), d_soiVar(ARITHVAR_SENTINEL), d_pivotBudget(0), d_prevWitnessImprovement(AntiProductive), @@ -253,7 +254,7 @@ UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePre } } - CompPenaltyColLength colCmp(&d_linEq); + CompPenaltyColLength colCmp(&d_linEq, options().arith.havePenalties); CandVector::iterator i = candidates.begin(); CandVector::iterator end = candidates.end(); std::make_heap(i, end, colCmp); @@ -845,10 +846,13 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){ tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar); d_soiVar = ARITHVAR_SENTINEL; - if(options::soiQuickExplain()){ + if (options().arith.soiQuickExplain) + { quickExplain(); generateSOIConflict(d_qeConflict); - }else{ + } + else + { vector<ArithVarVec> subsets = greedyConflictSubsets(); Assert(d_soiVar == ARITHVAR_SENTINEL); bool anySuccess = false; diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 5bff01d99..71b0b36d8 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -67,13 +67,17 @@ namespace arith { class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure { public: - SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc); + SumOfInfeasibilitiesSPD(Env& env, + LinearEqualityModule& linEq, + ErrorSet& errors, + RaiseConflict conflictChannel, + TempVarMalloc tvmalloc); - Result::Sat findModel(bool exactResult) override; + Result::Sat findModel(bool exactResult) override; - // other error variables are dropping - WitnessImprovement dualLikeImproveError(ArithVar evar); - WitnessImprovement primalImproveError(ArithVar evar); + // other error variables are dropping + WitnessImprovement dualLikeImproveError(ArithVar evar); + WitnessImprovement primalImproveError(ArithVar evar); private: /** The current sum of infeasibilities variable. */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 5a2d1a397..76a0c363d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -41,12 +41,12 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) statisticsRegistry().registerTimer("theory::arith::ppRewriteTimer")), d_astate(env, valuation), d_im(env, *this, d_astate, d_pnm), - d_ppre(context(), d_pnm), + 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_nonlinearExtension(nullptr), - d_opElim(d_pnm, logicInfo()), + d_opElim(d_env), d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim), d_rewriter(d_opElim) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 8e6bb6ccc..7ce45c374 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -46,7 +46,6 @@ #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" #include "theory/arith/approx_simplex.h" -#include "theory/arith/arith_ite_utils.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_utilities.h" @@ -122,7 +121,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)), - d_diosolver(context()), + d_diosolver(env), d_restartsCounter(0), d_tableauSizeHasBeenModified(false), d_tableauResetDensity(1.6), @@ -130,23 +129,21 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_conflicts(context()), d_blackBoxConflict(context(), Node::null()), d_blackBoxConflictPf(context(), std::shared_ptr<ProofNode>(nullptr)), - d_congruenceManager(context(), - userContext(), + d_congruenceManager(d_env, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, - RaiseEqualityEngineConflict(*this), - d_pnm), + RaiseEqualityEngineConflict(*this)), d_cmEnabled(context(), options().arith.arithCongMan), d_dualSimplex( - d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), + env, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_fcSimplex( - d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), + env, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_soiSimplex( - d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), + env, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_attemptSolSimplex( - d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), + env, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_pass1SDP(NULL), d_otherSDP(NULL), d_lastContextIntegerAttempted(context(), -1), |