diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 167 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 |
2 files changed, 123 insertions, 49 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9b4837d43..b3eaec1fd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -95,6 +95,7 @@ #include "theory/logic_info.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/fun_def_process.h" +#include "theory/quantifiers/global_negate.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" @@ -982,38 +983,39 @@ public: }/* namespace CVC4::smt */ -SmtEngine::SmtEngine(ExprManager* em) throw() : - d_context(new Context()), - d_userLevels(), - d_userContext(new UserContext()), - d_exprManager(em), - d_nodeManager(d_exprManager->getNodeManager()), - d_decisionEngine(NULL), - d_theoryEngine(NULL), - d_propEngine(NULL), - d_proofManager(NULL), - d_definedFunctions(NULL), - d_fmfRecFunctionsDefined(NULL), - d_assertionList(NULL), - d_assignments(NULL), - d_modelGlobalCommands(), - d_modelCommands(NULL), - d_dumpCommands(), - d_defineCommands(), - d_logic(), - d_originalOptions(), - d_pendingPops(0), - d_fullyInited(false), - d_problemExtended(false), - d_queryMade(false), - d_needPostsolve(false), - d_earlyTheoryPP(true), - d_status(), - d_replayStream(NULL), - d_private(NULL), - d_statisticsRegistry(NULL), - d_stats(NULL), - d_channels(new LemmaChannels()) +SmtEngine::SmtEngine(ExprManager* em) throw() + : d_context(new Context()), + d_userLevels(), + d_userContext(new UserContext()), + d_exprManager(em), + d_nodeManager(d_exprManager->getNodeManager()), + d_decisionEngine(NULL), + d_theoryEngine(NULL), + d_propEngine(NULL), + d_proofManager(NULL), + d_definedFunctions(NULL), + d_fmfRecFunctionsDefined(NULL), + d_assertionList(NULL), + d_assignments(NULL), + d_modelGlobalCommands(), + d_modelCommands(NULL), + d_dumpCommands(), + d_defineCommands(), + d_logic(), + d_originalOptions(), + d_pendingPops(0), + d_fullyInited(false), + d_problemExtended(false), + d_queryMade(false), + d_needPostsolve(false), + d_earlyTheoryPP(true), + d_globalNegation(false), + d_status(), + d_replayStream(NULL), + d_private(NULL), + d_statisticsRegistry(NULL), + d_stats(NULL), + d_channels(new LemmaChannels()) { SmtScope smts(this); d_originalOptions.copyValues(em->getOptions()); @@ -1434,6 +1436,17 @@ void SmtEngine::setDefaults() { Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl; setOption("repeat-simp", false); } + + if (options::globalNegate()) + { + if (options::globalNegate.wasSetByUser()) + { + throw OptionException("global-negate not supported with unsat cores"); + } + Notice() << "SmtEngine: turning off global-negate to support unsat-cores" + << endl; + setOption("global-negate", false); + } } if (options::cbqiBv()) { @@ -1743,6 +1756,7 @@ void SmtEngine::setDefaults() { options::sortInference.set( false ); options::ufssFairnessMonotone.set( false ); options::quantEpr.set( false ); + options::globalNegate.set(false); } if( d_logic.hasCardinalityConstraints() ){ //must have finite model finding on @@ -1931,7 +1945,8 @@ void SmtEngine::setDefaults() { if( !options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); } - if( d_logic.isPure(THEORY_ARITH) ){ + if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)) + { options::cbqiAll.set( false ); if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); @@ -1945,9 +1960,23 @@ void SmtEngine::setDefaults() { } }else{ // only supported in pure arithmetic or pure BV - if (!d_logic.isPure(THEORY_BV)) + options::cbqiNestedQE.set(false); + } + // prenexing + if (options::cbqiNestedQE() + || options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) + { + // only complete with prenex = disj_normal or normal + if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL) { - options::cbqiNestedQE.set(false); + options::prenexQuant.set(quantifiers::PRENEX_QUANT_DISJ_NORMAL); + } + } + else if (options::globalNegate()) + { + if (!options::prenexQuant.wasSetByUser()) + { + options::prenexQuant.set(quantifiers::PRENEX_QUANT_NONE); } } } @@ -1960,13 +1989,6 @@ void SmtEngine::setDefaults() { if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } - if( options::cbqi() && - ( options::cbqiNestedQE() || options::decisionMode()==decision::DECISION_STRATEGY_INTERNAL ) ){ - //only complete with prenex = disj_normal or normal - if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL ){ - options::prenexQuant.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL ); - } - } if( options::cbqiNestedQE() ){ options::prenexQuantUser.set( true ); if( !options::preSkolemQuant.wasSetByUser() ){ @@ -2057,26 +2079,40 @@ void SmtEngine::setDefaults() { } // Non-linear arithmetic does not support models unless nlExt is enabled - if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() && !options::nlExt() ) { + if ((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() + && !options::nlExt()) + || options::globalNegate()) + { + std::string reason = + options::globalNegate() ? "--global-negate" : "nonlinear arithmetic"; if (options::produceModels()) { if(options::produceModels.wasSetByUser()) { - throw OptionException("produce-model not supported with nonlinear arith"); + throw OptionException( + std::string("produce-model not supported with " + reason)); } - Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl; + Warning() + << "SmtEngine: turning off produce-models because unsupported for " + << reason << endl; setOption("produce-models", SExpr("false")); } if (options::produceAssignments()) { if(options::produceAssignments.wasSetByUser()) { - throw OptionException("produce-assignments not supported with nonlinear arith"); + throw OptionException( + std::string("produce-assignments not supported with " + reason)); } - Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl; + Warning() << "SmtEngine: turning off produce-assignments because " + "unsupported for " + << reason << endl; setOption("produce-assignments", SExpr("false")); } if (options::checkModels()) { if(options::checkModels.wasSetByUser()) { - throw OptionException("check-models not supported with nonlinear arith"); + throw OptionException( + std::string("check-models not supported with " + reason)); } - Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl; + Warning() + << "SmtEngine: turning off check-models because unsupported for " + << reason << endl; setOption("check-models", SExpr("false")); } } @@ -4170,6 +4206,14 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; + // global negation of the formula + if (options::globalNegate()) + { + quantifiers::GlobalNegate gn; + gn.simplify(d_assertions.ref()); + d_smt.d_globalNegation = !d_smt.d_globalNegation; + } + if( options::nlExtPurify() ){ unordered_map<Node, Node, NodeHashFunction> cache; unordered_map<Node, Node, NodeHashFunction> bcache; @@ -4660,6 +4704,9 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ // Note that a query has been made d_queryMade = true; + // reset global negation + d_globalNegation = false; + // Add the formula if(!e.isNull()) { d_problemExtended = true; @@ -4676,6 +4723,28 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ if ( ( options::solveRealAsInt() || options::solveIntAsBV() > 0 ) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) { r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); } + // flipped if we did a global negation + if (d_globalNegation) + { + Trace("smt") << "SmtEngine::process global negate " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + r = Result(Result::SAT); + } + else if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + // only if satisfaction complete + if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV)) + { + r = Result(Result::UNSAT); + } + else + { + r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); + } + } + Trace("smt") << "SmtEngine::global negate returned " << r << std::endl; + } d_needPostsolve = true; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c628a1952..6d648ccda 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -241,6 +241,11 @@ class CVC4_PUBLIC SmtEngine { */ bool d_earlyTheoryPP; + /* + * Whether we did a global negation of the formula. + */ + bool d_globalNegation; + /** * Most recent result of last checkSat/query or (set-info :status). */ |