This PR removes the usage of static accesses to options from the arithmetic theory, mostly by making more classes inherit from EnvObj.
util::ContainsTermITEVisitor& contains =
*(d_iteUtilities.getContainsVisitor());
arith::ArithIteUtils aiteu(
- contains,
- userContext(),
- d_preprocContext->getTopLevelSubstitutions().get());
+ d_env, contains, d_preprocContext->getTopLevelSubstitutions().get());
bool anyItes = false;
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
#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"
}
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()
{
}
Node ArithIteUtils::applySubstitutions(TNode f){
- AlwaysAssert(!options::incrementalSolving());
+ AlwaysAssert(!options().base.incrementalSolving);
return d_subs.apply(f);
}
}
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]);
}
#include "context/cdinsert_hashmap.h"
#include "context/cdo.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "util/integer.h"
namespace cvc5 {
namespace arith {
-class ArithIteUtils {
+class ArithIteUtils : protected EnvObj
+{
preprocessing::util::ContainsTermITEVisitor& d_contains;
SubstitutionMap& d_subs;
Integer d_one;
- context::CDO<unsigned> d_subcount;
+ context::CDO<uint64_t> d_subcount;
typedef context::CDInsertHashMap<Node, Node> CDNodeMap;
CDNodeMap d_skolems;
std::vector<Node> d_orBinEqs;
public:
- ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains,
- context::Context* userContext,
+ ArithIteUtils(Env& env,
+ preprocessing::util::ContainsTermITEVisitor& contains,
SubstitutionMap& subs);
~ArithIteUtils();
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()
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 {
#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"
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)
{
}
bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi)
{
- Assert(!options::arithEqSolver());
+ Assert(!options().arith.arithEqSolver);
esi.d_notify = &d_notify;
esi.d_name = "arithCong::ee";
return true;
void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
{
- if (options::arithEqSolver())
+ if (options().arith.arithEqSolver)
{
// use our own copy
d_allocEe.reset(
#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"
class ArithVariables;
-class ArithCongruenceManager {
-private:
+class ArithCongruenceManager : protected EnvObj
+{
+ private:
context::CDRaised d_inConflict;
RaiseEqualityEngineConflict d_raiseConflict;
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
Statistics();
} d_statistics;
-};/* class ArithCongruenceManager */
+}; /* class ArithCongruenceManager */
std::vector<Node> andComponents(TNode an);
#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"
"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(
}
void DioSolver::addTrailElementAsLemma(TrailIndex i) {
- if(options::exportDioDecompositions()){
+ if (options().arith.exportDioDecompositions)
+ {
d_decompositionLemmaQueue.push(i);
}
}
#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"
namespace theory {
namespace arith {
-class DioSolver {
-private:
+class DioSolver : protected EnvObj
+{
+ private:
typedef size_t TrailIndex;
typedef size_t InputConstraintIndex;
typedef size_t SubIndex;
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();
};
Statistics d_statistics;
-};/* class DioSolver */
+}; /* class DioSolver */
} // namespace arith
} // namespace theory
#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"
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)
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){
--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;
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:
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(),
}
}
- 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);
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;
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;
}
}
*
* 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;
#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"
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;
}
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
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);
}
#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"
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.
*
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
#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"
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();
}
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
#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 {
*
* 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
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
#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"
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(){
#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"
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. */
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;
sgn_table::const_iterator find_sgns(const sgn_table& sgns, ArithVar col, int sgn);
-};/* class SimplexDecisionProcedure */
+}; /* class SimplexDecisionProcedure */
} // namespace arith
} // namespace theory
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),
}
}
- 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);
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;
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. */
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)
{
#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"
d_tableau,
d_rowTracking,
BasicVarModelUpdateCallBack(*this)),
- d_diosolver(context()),
+ d_diosolver(env),
d_restartsCounter(0),
d_tableauSizeHasBeenModified(false),
d_tableauResetDensity(1.6),
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),
projects / cvc5.git / commitdiff