diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-07 20:45:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-07 20:45:13 +0000 |
commit | e568f34e1f4713c678336fbef1006e585128d466 (patch) | |
tree | a20636a5d50a84d22016f278e9f3a036436125dd /src/smt | |
parent | d71827eef17c181d225f64ea59d26c34d76b9b1e (diff) |
LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.
ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 83 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 20 |
2 files changed, 76 insertions, 27 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8b3e6b742..ed28c23a3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -242,7 +242,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_assertionList(NULL), d_assignments(NULL), d_logic(), - d_logicIsSet(false), + d_fullyInited(false), d_problemExtended(false), d_queryMade(false), d_needPostsolve(false), @@ -328,6 +328,19 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : if(Options::current()->cumulativeMillisecondLimit != 0) { setTimeLimit(Options::current()->cumulativeMillisecondLimit, true); } +} + +void SmtEngine::finalOptionsAreSet() { + if(d_fullyInited) { + return; + } + + AlwaysAssert( d_propEngine->getAssertionLevel() == 0, + "The PropEngine has pushed but the SmtEngine " + "hasn't finished initializing!" ); + + d_fullyInited = true; + d_logic.lock(); d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true)); d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode()); @@ -401,15 +414,12 @@ SmtEngine::~SmtEngine() throw() { void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { NodeManagerScope nms(d_nodeManager); - if(d_logicIsSet) { - throw ModalException("logic already set"); - } - if(Dump.isOn("benchmark")) { Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString()); } - setLogicInternal(logic); + d_logic = logic; + setLogicInternal(); } void SmtEngine::setLogic(const std::string& s) throw(ModalException) { @@ -418,57 +428,63 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { setLogic(LogicInfo(s)); } -void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() { - d_logic = logic; +// This function is called when d_logic has just been changed. +// The LogicInfo isn't passed in explicitly, because that might +// tempt people in the code to use the (potentially unlocked) +// version that's passed in, leading to assert-fails in certain +// uses of the CVC4 library. +void SmtEngine::setLogicInternal() throw(AssertionException) { + Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run"); + + d_logic.lock(); // by default, symmetry breaker is on only for QF_UF if(! Options::current()->ufSymmetryBreakerSetByUser) { - bool qf_uf = logic.isPure(theory::THEORY_UF) && !logic.isQuantified(); + bool qf_uf = d_logic.isPure(theory::THEORY_UF) && !d_logic.isQuantified(); Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl; NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf; } // by default, nonclausal simplification is off for QF_SAT if(! Options::current()->simplificationModeSetByUser) { - bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified(); - Trace("smt") << "setting simplification mode to <" << logic.getLogicString() << "> " << (!qf_sat) << std::endl; + bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified(); + Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << std::endl; NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH); } // If in arrays, set the UF handler to arrays - if(logic.isPure(theory::THEORY_ARRAY) && !logic.isQuantified()) { + if(d_logic.isPure(theory::THEORY_ARRAY) && !d_logic.isQuantified()) { theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY); } else { theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF); } // Turn on ite simplification for QF_LIA and QF_AUFBV if(! Options::current()->doITESimpSetByUser) { - bool iteSimp = !logic.isQuantified() && - ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear() && !logic.isDifferenceLogic() && !logic.areRealsUsed()) || - (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV))); + bool iteSimp = !d_logic.isQuantified() && + ((d_logic.isPure(theory::THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areRealsUsed()) || + (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_UF) && d_logic.isTheoryEnabled(theory::THEORY_BV))); Trace("smt") << "setting ite simplification to " << iteSimp << std::endl; NodeManager::currentNM()->getOptions()->doITESimp = iteSimp; } // Turn on multiple-pass non-clausal simplification for QF_AUFBV if(! Options::current()->repeatSimpSetByUser) { - bool repeatSimp = !logic.isQuantified() && - (logic.isTheoryEnabled(theory::THEORY_ARRAY) && logic.isTheoryEnabled(theory::THEORY_UF) && logic.isTheoryEnabled(theory::THEORY_BV)); + bool repeatSimp = !d_logic.isQuantified() && + (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_UF) && d_logic.isTheoryEnabled(theory::THEORY_BV)); Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl; NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp; } // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) { - bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified(); + bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified(); bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving; Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp; } // Turn on arith rewrite equalities only for pure arithmetic if(! Options::current()->arithRewriteEqSetByUser) { - bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified(); + bool arithRewriteEq = d_logic.isPure(theory::THEORY_ARITH) && !d_logic.isQuantified(); Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl; NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq; } - } void SmtEngine::setInfo(const std::string& key, const SExpr& value) @@ -496,7 +512,8 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string"); } NodeManagerScope nms(d_nodeManager); - setLogicInternal(value.getValue()); + d_logic = value.getValue(); + setLogicInternal(); return; } } @@ -592,7 +609,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) } else { // The following options can only be set at the beginning; we throw // a ModalException if someone tries. - if(d_logicIsSet) { + if(d_logic.isLocked()) { throw ModalException("logic already set; cannot set options"); } @@ -761,8 +778,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHas } } - void SmtEnginePrivate::removeITEs() { + d_smt.finalOptionsAreSet(); + Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl; // Remove all of the ITE occurrences and normalize @@ -774,6 +792,7 @@ void SmtEnginePrivate::removeITEs() { } void SmtEnginePrivate::staticLearning() { + d_smt.finalOptionsAreSet(); TimerStat::CodeTimer staticLearningTimer(d_smt.d_staticLearningTime); @@ -793,6 +812,7 @@ void SmtEnginePrivate::staticLearning() { } void SmtEnginePrivate::nonClausalSimplify() { + d_smt.finalOptionsAreSet(); TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime); @@ -1072,6 +1092,8 @@ void SmtEnginePrivate::simplifyAssertions() } Result SmtEngine::check() { + Assert(d_fullyInited); + Trace("smt") << "SmtEngine::check()" << endl; // Make sure the prop layer has all of the assertions @@ -1124,11 +1146,13 @@ Result SmtEngine::check() { } Result SmtEngine::quickCheck() { + Assert(d_fullyInited); Trace("smt") << "SMT quickCheck()" << endl; return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK); } void SmtEnginePrivate::processAssertions() { + Assert(d_smt.d_fullyInited); Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl; @@ -1252,6 +1276,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); + Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl; if(d_queryMade && !Options::current()->incrementalSolving) { @@ -1313,6 +1339,8 @@ Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); + Trace("smt") << "SMT query(" << e << ")" << endl; if(d_queryMade && !Options::current()->incrementalSolving) { @@ -1366,6 +1394,7 @@ Result SmtEngine::query(const BoolExpr& e) { Result SmtEngine::assertFormula(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl; ensureBoolean(e); if(d_assertionList != NULL) { @@ -1378,6 +1407,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) { Expr SmtEngine::simplify(const Expr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); if( Options::current()->typeChecking ) { e.getType(true);// ensure expr is type-checked at this point } @@ -1435,6 +1465,7 @@ Expr SmtEngine::getValue(const Expr& e) bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); Type type = e.getType(Options::current()->typeChecking); // must be Boolean CheckArgument( type.isBoolean(), e, @@ -1463,6 +1494,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Trace("smt") << "SMT getAssignment()" << endl; NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssignmentCommand(); } @@ -1519,6 +1551,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { Trace("smt") << "SMT getProof()" << endl; NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetProofCommand(); } @@ -1566,6 +1599,7 @@ size_t SmtEngine::getStackLevel() const { void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); Trace("smt") << "SMT push()" << endl; d_private->processAssertions(); if(Dump.isOn("benchmark")) { @@ -1589,6 +1623,7 @@ void SmtEngine::push() { void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); + finalOptionsAreSet(); Trace("smt") << "SMT pop()" << endl; if(Dump.isOn("benchmark")) { Dump("benchmark") << PopCommand(); @@ -1624,6 +1659,7 @@ void SmtEngine::pop() { } void SmtEngine::internalPush() { + Assert(d_fullyInited); Trace("smt") << "SmtEngine::internalPush()" << endl; if(Options::current()->incrementalSolving) { d_private->processAssertions(); @@ -1634,6 +1670,7 @@ void SmtEngine::internalPush() { } void SmtEngine::internalPop() { + Assert(d_fullyInited); Trace("smt") << "SmtEngine::internalPop()" << endl; if(Options::current()->incrementalSolving) { d_propEngine->pop(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f07815e2e..4c0fed74c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -135,9 +135,12 @@ class CVC4_PUBLIC SmtEngine { LogicInfo d_logic; /** - * Whether the logic has been set yet. + * Whether or not this SmtEngine has been fully initialized (that is, + * the ). This post-construction initialization is automatically + * triggered by the use of the SmtEngine; e.g. when setLogic() is + * called, or the first assertion is made, etc. */ - bool d_logicIsSet; + bool d_fullyInited; /** * Whether or not we have added any assertions/declarations/definitions @@ -185,6 +188,14 @@ class CVC4_PUBLIC SmtEngine { smt::SmtEnginePrivate* d_private; /** + * This is something of an "init" procedure, but is idempotent; call + * as often as you like. Should be called whenever the final options + * and logic for the problem are set (at least, those options that are + * not permitted to change after assertions and queries are made). + */ + void finalOptionsAreSet(); + + /** * This is called by the destructor, just before destroying the * PropEngine, TheoryEngine, and DecisionEngine (in that order). It * is important because there are destruction ordering issues @@ -216,9 +227,10 @@ class CVC4_PUBLIC SmtEngine { void internalPop(); /** - * Internally handle the setting of a logic. + * Internally handle the setting of a logic. This function should always + * be called when d_logic is updated. */ - void setLogicInternal(const LogicInfo& logic) throw(); + void setLogicInternal() throw(AssertionException); friend class ::CVC4::smt::SmtEnginePrivate; |