diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/logic_request.h | 53 | ||||
| -rw-r--r-- | src/smt/options | 9 | ||||
| -rw-r--r-- | src/smt/options_handlers.h | 13 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 581 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 9 | ||||
| -rw-r--r-- | src/smt/smt_options_template.cpp | 8 |
6 files changed, 244 insertions, 429 deletions
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h new file mode 100644 index 000000000..4985b0e65 --- /dev/null +++ b/src/smt/logic_request.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file logic_request.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An object to request logic widening in the running SmtEngine + ** + ** An object to request logic widening in the running SmtEngine. This + ** class exists as a proxy between theory code and the SmtEngine, allowing + ** a theory to enable another theory in the SmtEngine after initialization + ** (thus the usual, public setLogic() cannot be used). This is mainly to + ** support features like uninterpreted divide-by-zero (to support the + ** partial function DIVISION), where during theory expansion, the theory + ** of uninterpreted functions needs to be added to the logic to support + ** partial functions. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__LOGIC_REQUEST_H +#define __CVC4__LOGIC_REQUEST_H + +#include "expr/kind.h" +#include "smt/smt_engine.h" + +namespace CVC4 { + +class LogicRequest { + /** The SmtEngine at play. */ + SmtEngine& d_smt; + +public: + LogicRequest(SmtEngine& smt) : d_smt(smt) { } + + /** Widen the logic to include the given theory. */ + void widenLogic(theory::TheoryId id) { + d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(id); + d_smt.d_logic.lock(); + } + +};/* class LogicRequest */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__LOGIC_REQUEST_H */ diff --git a/src/smt/options b/src/smt/options index b76822caf..f3429287f 100644 --- a/src/smt/options +++ b/src/smt/options @@ -5,11 +5,14 @@ module SMT "smt/options.h" SMT layer -common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h" +common-option - dump --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h" dump preprocessed assertions, etc., see --dump=help -common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h" +common-option - dump-to --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h" all dumping goes to FILE (instead of stdout) +expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo :include "theory/logic_info.h" :handler CVC4::smt::stringToLogicInfo :handler-include "smt/options_handlers.h" :default '""' + set the logic, and override all further user attempts to change it + option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h" choose simplification mode, see --simplification=help alias --no-simplification = --simplification=none @@ -40,7 +43,7 @@ option produceAssignments produce-assignments --produce-assignments bool :defaul # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive" # is a mode in which the assertion list must be kept. So it belongs here. -common-option interactive interactive-mode --interactive bool :read-write +common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write force interactive mode option doITESimp --ite-simp bool :read-write diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index c9c3d6345..49f2c7943 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -257,6 +257,19 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { #endif /* CVC4_DUMPING */ } +inline LogicInfo stringToLogicInfo(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + try { + LogicInfo logic(optarg); + if(smt != NULL) { + smt->setLogic(logic); + } + return logic; + } catch(IllegalArgumentException& e) { + throw OptionException(std::string("invalid logic specification for --force-logic: `") + + optarg + "':\n" + e.what()); + } +} + inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "batch") { return SIMPLIFICATION_MODE_BATCH; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 02542b640..328a20c28 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -43,6 +43,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/model_postprocessor.h" +#include "smt/logic_request.h" #include "theory/theory_engine.h" #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" @@ -80,8 +81,10 @@ #include "util/sort_inference.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/macros.h" -#include "theory/datatypes/options.h" #include "theory/quantifiers/first_order_reasoning.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/options.h" +#include "theory/datatypes/options.h" #include "theory/strings/theory_strings_preprocess.h" using namespace std; @@ -306,44 +309,6 @@ class SmtEnginePrivate : public NodeManagerListener { */ hash_map<Node, Node, NodeHashFunction> d_abstractValues; - /** - * Function symbol used to implement uninterpreted undefined string - * semantics. Needed to deal with partial charat/substr function. - */ - Node d_ufSubstr; - - /** - * Function symbol used to implement uninterpreted undefined string - * semantics. Needed to deal with partial str2int function. - */ - Node d_ufS2I; - - /** - * Function symbol used to implement uninterpreted division-by-zero - * semantics. Needed to deal with partial division function ("/"). - */ - Node d_divByZero; - - /** - * Maps from bit-vector width to divison-by-zero uninterpreted - * function symbols. - */ - hash_map<unsigned, Node> d_BVDivByZero; - hash_map<unsigned, Node> d_BVRemByZero; - - /** - * Function symbol used to implement uninterpreted - * int-division-by-zero semantics. Needed to deal with partial - * function "div". - */ - Node d_intDivByZero; - - /** - * Function symbol used to implement uninterpreted mod-zero - * semantics. Needed to deal with partial function "mod". - */ - Node d_modZero; - /** Number of calls of simplify assertions active. */ unsigned d_simplifyAssertionsDepth; @@ -446,9 +411,6 @@ public: d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues(), - d_divByZero(), - d_intDivByZero(), - d_modZero(), d_simplifyAssertionsDepth(0), d_iteSkolemMap(), d_iteRemover(smt.d_userContext), @@ -552,25 +514,6 @@ public: throw(TypeCheckingException, LogicException); /** - * Return the uinterpreted function symbol corresponding to division-by-zero - * for this particular bit-width - * @param k should be UREM or UDIV - * @param width - * - * @return - */ - Node getBVDivByZero(Kind k, unsigned width); - - /** - * Returns the node modeling the division-by-zero semantics of node n. - * - * @param n - * - * @return - */ - Node expandBVDivByZero(TNode n); - - /** * Expand definitions in n. */ Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache) @@ -596,11 +539,6 @@ public: } /** - * Pre-skolemize quantifiers. - */ - Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs); - - /** * Substitute away all AbstractValues in a node. */ Node substituteAbstractValues(TNode n) { @@ -736,6 +674,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : } void SmtEngine::finishInit() { + // ensure that our heuristics are properly set up + setDefaults(); + d_decisionEngine = new DecisionEngine(d_context, d_userContext); d_decisionEngine->init(); // enable appropriate strategies @@ -793,24 +734,7 @@ void SmtEngine::finalOptionsAreSet() { return; } - if(options::bitvectorEagerBitblast()) { - // Eager solver should use the internal decision strategy - options::decisionMode.set(DECISION_STRATEGY_INTERNAL); - } - - if(options::checkModels()) { - if(! options::interactive()) { - Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; - setOption("interactive-mode", SExpr("true")); - } - } - if(options::produceAssignments() && !options::produceModels()) { - Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl; - setOption("produce-models", SExpr("true")); - } - if(! d_logic.isLocked()) { - // ensure that our heuristics are properly set up setLogicInternal(); } @@ -925,15 +849,68 @@ LogicInfo SmtEngine::getLogicInfo() const { return d_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() { Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run"); - d_logic.lock(); +} + +void SmtEngine::setDefaults() { + if(options::forceLogic.wasSetByUser()) { + d_logic = options::forceLogic(); + } + + // set strings-exp + if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + if(! options::stringExp.wasSetByUser()) { + options::stringExp.set( true ); + Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl; + } + } + // for strings + if(options::stringExp()) { + if( !d_logic.isQuantified() ) { + d_logic = d_logic.getUnlockedCopy(); + d_logic.enableQuantifiers(); + d_logic.lock(); + Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; + } + if(! options::finiteModelFind.wasSetByUser()) { + options::finiteModelFind.set( true ); + Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; + } + if(! options::fmfBoundInt.wasSetByUser()) { + options::fmfBoundInt.set( true ); + Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; + } + /* + if(! options::rewriteDivk.wasSetByUser()) { + options::rewriteDivk.set( true ); + Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl; + }*/ + /* + if(! options::stringFMF.wasSetByUser()) { + options::stringFMF.set( true ); + Trace("smt") << "turning on strings-fmf, for strings-exp" << std::endl; + } + */ + } + + if(options::bitvectorEagerBitblast()) { + // Eager solver should use the internal decision strategy + options::decisionMode.set(DECISION_STRATEGY_INTERNAL); + } + + if(options::checkModels()) { + if(! options::interactive()) { + Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; + setOption("interactive-mode", SExpr("true")); + } + } + + if(options::produceAssignments() && !options::produceModels()) { + Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl; + setOption("produce-models", SExpr("true")); + } // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { @@ -966,7 +943,7 @@ void SmtEngine::setLogicInternal() throw() { options::fmfBoundInt.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } - /* + /* if(! options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl; @@ -1068,7 +1045,7 @@ void SmtEngine::setLogicInternal() throw() { if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) { // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); // bool uncSimp = false && !qf_sat && !options::incrementalSolving(); - bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::checkModels() && + bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::produceAssignments() && !options::checkModels() && (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV)); Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl; options::unconstrainedSimp.set(uncSimp); @@ -1079,6 +1056,10 @@ void SmtEngine::setLogicInternal() throw() { Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl; setOption("produce-models", SExpr("false")); } + if (options::produceAssignments()) { + Notice() << "SmtEngine: turning off produce-assignments to support unconstrainedSimp" << endl; + setOption("produce-assignments", SExpr("false")); + } if (options::checkModels()) { Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl; setOption("check-models", SExpr("false")); @@ -1188,7 +1169,7 @@ void SmtEngine::setLogicInternal() throw() { //instantiate only on last call if( options::fmfInstEngine() ){ Trace("smt") << "setting inst when mode to LAST_CALL" << endl; - options::instWhenMode.set( INST_WHEN_LAST_CALL ); + options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } if ( options::fmfBoundInt() ){ @@ -1214,7 +1195,7 @@ void SmtEngine::setLogicInternal() throw() { //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ - if( d_logic.isQuantified() || options::produceModels() || options::checkModels() ){ + if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ options::minisatUseElim.set( false ); } } @@ -1223,6 +1204,10 @@ void SmtEngine::setLogicInternal() throw() { Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl; setOption("produce-models", SExpr("false")); } + if (options::produceAssignments()) { + Notice() << "SmtEngine: turning off produce-assignments to support minisatUseElim" << endl; + setOption("produce-assignments", SExpr("false")); + } if (options::checkModels()) { Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl; setOption("check-models", SExpr("false")); @@ -1230,7 +1215,7 @@ void SmtEngine::setLogicInternal() throw() { } // For now, these array theory optimizations do not support model-building - if (options::produceModels() || options::checkModels()) { + if (options::produceModels() || options::produceAssignments() || options::checkModels()) { options::arraysOptimizeLinear.set(false); options::arraysLazyRIntro1.set(false); } @@ -1242,6 +1227,10 @@ void SmtEngine::setLogicInternal() throw() { Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl; setOption("produce-models", SExpr("false")); } + if (options::produceAssignments()) { + Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl; + setOption("produce-assignments", SExpr("false")); + } if (options::checkModels()) { Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl; setOption("check-models", SExpr("false")); @@ -1470,55 +1459,6 @@ void SmtEngine::defineFunction(Expr func, } -Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) { - NodeManager* nm = d_smt.d_nodeManager; - if (k == kind::BITVECTOR_UDIV) { - if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) { - // lazily create the function symbols - ostringstream os; - os << "BVUDivByZero_" << width; - Node divByZero = nm->mkSkolem(os.str(), - nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)), - "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME); - d_BVDivByZero[width] = divByZero; - } - return d_BVDivByZero[width]; - } - else if (k == kind::BITVECTOR_UREM) { - if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) { - ostringstream os; - os << "BVURemByZero_" << width; - Node divByZero = nm->mkSkolem(os.str(), - nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)), - "partial bvurem", NodeManager::SKOLEM_EXACT_NAME); - d_BVRemByZero[width] = divByZero; - } - return d_BVRemByZero[width]; - } - - Unreachable(); -} - - -Node SmtEnginePrivate::expandBVDivByZero(TNode n) { - // we only deal wioth the unsigned division operators as the signed ones should have been - // expanded in terms of the unsigned operators - NodeManager* nm = d_smt.d_nodeManager; - unsigned width = n.getType().getBitVectorSize(); - Node divByZero = getBVDivByZero(n.getKind(), width); - TNode num = n[0], den = n[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0)))); - Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); - Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : - kind::BITVECTOR_UREM_TOTAL, num, den); - Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); - if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_UF); - d_smt.d_logic.lock(); - } - return node; -} Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache) @@ -1527,31 +1467,36 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF stack< triple<Node, Node, bool> > worklist; stack<Node> result; worklist.push(make_triple(Node(n), Node(n), false)); + // The worklist is made of triples, each is input / original node then the output / rewritten node + // and finally a flag tracking whether the children have been explored (i.e. if this is a downward + // or upward pass). do { - n = worklist.top().first; - Node node = worklist.top().second; + n = worklist.top().first; // n is the input / original + Node node = worklist.top().second; // node is the output / result bool childrenPushed = worklist.top().third; worklist.pop(); + // Working downwards if(!childrenPushed) { Kind k = n.getKind(); + // Apart from apply, we can short circuit leaves if(k != kind::APPLY && n.getNumChildren() == 0) { - SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n); - if(i != d_smt.d_definedFunctions->end()) { - // replacement must be closed - if((*i).second.getFormals().size() > 0) { - result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula())); - continue; - } - // don't bother putting in the cache - result.push((*i).second.getFormula()); - continue; - } - // don't bother putting in the cache - result.push(n); - continue; + SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n); + if(i != d_smt.d_definedFunctions->end()) { + // replacement must be closed + if((*i).second.getFormals().size() > 0) { + result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula())); + continue; + } + // don't bother putting in the cache + result.push((*i).second.getFormula()); + continue; + } + // don't bother putting in the cache + result.push(n); + continue; } // maybe it's in the cache @@ -1563,134 +1508,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF } // otherwise expand it - - NodeManager* nm = d_smt.d_nodeManager; - // FIXME: this theory-specific code should be factored out of the - // SmtEngine, somehow - switch(k) { - case kind::BITVECTOR_SDIV: - case kind::BITVECTOR_SREM: - case kind::BITVECTOR_SMOD: - node = bv::TheoryBVRewriter::eliminateBVSDiv(node); - break; - - case kind::BITVECTOR_UDIV: - case kind::BITVECTOR_UREM: - node = expandBVDivByZero(node); - break; - - case kind::STRING_CHARAT: { - if(d_ufSubstr.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->stringType()), - "uf substr", - NodeManager::SKOLEM_EXACT_NAME); - } - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] ); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); - Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero); - Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], one); - Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], one); - node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); - break; - } - case kind::STRING_SUBSTR: { - if(d_ufSubstr.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->stringType()), - "uf substr", - NodeManager::SKOLEM_EXACT_NAME); - } - Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), - NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); - Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], zero); - Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], zero); - Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], n[2]); - Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], n[2]); - node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); - break; - } - case kind::DIVISION: { - // partial function: division - if(d_divByZero.isNull()) { - d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()), - "partial real division", NodeManager::SKOLEM_EXACT_NAME); - if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_UF); - d_smt.d_logic.lock(); - } - } - TNode num = n[0], den = n[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num); - Node divTotalNumDen = nm->mkNode(kind::DIVISION_TOTAL, num, den); - node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); - break; - } - - case kind::INTS_DIVISION: { - // partial function: integer div - if(d_intDivByZero.isNull()) { - d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()), - "partial integer division", NodeManager::SKOLEM_EXACT_NAME); - if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_UF); - d_smt.d_logic.lock(); - } - } - TNode num = n[0], den = n[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num); - Node intDivTotalNumDen = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den); - node = nm->mkNode(kind::ITE, den_eq_0, intDivByZeroNum, intDivTotalNumDen); - break; - } - - case kind::INTS_MODULUS: { - // partial function: mod - if(d_modZero.isNull()) { - d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()), - "partial modulus", NodeManager::SKOLEM_EXACT_NAME); - if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_UF); - d_smt.d_logic.lock(); - } - } - TNode num = n[0], den = n[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); - Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num); - Node modTotalNumDen = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den); - node = nm->mkNode(kind::ITE, den_eq_0, modZeroNum, modTotalNumDen); - break; - } - - case kind::ABS: { - Node out = nm->mkNode(kind::ITE, nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), nm->mkNode(kind::UMINUS, node[0]), node[0]); - cache[n] = out; - result.push(out); - continue; - } - - case kind::APPLY: { + if (k == kind::APPLY) { // application of a user-defined symbol TNode func = n.getOperator(); SmtEngine::DefinedFunctionMap::const_iterator i = @@ -1729,25 +1547,35 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF cache[n] = (n == expanded ? Node::null() : expanded); result.push(expanded); continue; - } - default: - // unknown kind for expansion, just iterate over the children - node = n; + } else { + theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node); + + Assert(t != NULL); + LogicRequest req(d_smt); + node = t->expandDefinition(req, n); } // there should be children here, otherwise we short-circuited a result-push/continue, above + if (node.getNumChildren() == 0) { + Debug("expand") << "Unexpectedly no children..." << node << endl; + } + // This invariant holds at the moment but it is concievable that a new theory + // might introduce a kind which can have children before definition expansion but doesn't + // afterwards. If this happens, remove this assertion. Assert(node.getNumChildren() > 0); // the partial functions can fall through, in which case we still // consider their children - worklist.push(make_triple(Node(n), node, true)); + worklist.push(make_triple(Node(n), node, true)); // Original and rewritten result for(size_t i = 0; i < node.getNumChildren(); ++i) { - worklist.push(make_triple(node[i], node[i], false)); + worklist.push(make_triple(node[i], node[i], false)); // Rewrite the children of the result only } } else { + // Working upwards + // Reconstruct the node from it's (now rewritten) children on the stack Debug("expand") << "cons : " << node << endl; //cout << "cons : " << node << endl; @@ -1766,7 +1594,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF nb << expanded; } node = nb; - cache[n] = n == node ? Node::null() : node; + cache[n] = n == node ? Node::null() : node; // Only cache once all subterms are expanded result.push(node); } } while(!worklist.empty()); @@ -1776,120 +1604,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF return result.top(); } - -struct ContainsQuantAttributeId {}; -typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute; - -// check if the given node contains a universal quantifier -static bool containsQuantifiers(Node n) { - if( n.hasAttribute(ContainsQuantAttribute()) ){ - return n.getAttribute(ContainsQuantAttribute())==1; - } else if(n.getKind() == kind::FORALL) { - return true; - } else { - bool cq = false; - for( unsigned i = 0; i < n.getNumChildren(); ++i ){ - if( containsQuantifiers(n[i]) ){ - cq = true; - break; - } - } - ContainsQuantAttribute cqa; - n.setAttribute(cqa, cq ? 1 : 0); - return cq; - } -} - -Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){ - Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; - if( n.getKind()==kind::NOT ){ - Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs ); - return nn.negate(); - }else if( n.getKind()==kind::FORALL ){ - if( polarity ){ - vector< Node > children; - children.push_back( n[0] ); - //add children to current scope - vector< Node > fvss; - fvss.insert( fvss.begin(), fvs.begin(), fvs.end() ); - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - fvss.push_back( n[0][i] ); - } - //process body - children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) ); - if( n.getNumChildren()==3 ){ - children.push_back( n[2] ); - } - //return processed quantifier - return NodeManager::currentNM()->mkNode( kind::FORALL, children ); - }else{ - //process body - Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs ); - //now, substitute skolems for the variables - vector< TypeNode > argTypes; - for( int i=0; i<(int)fvs.size(); i++ ){ - argTypes.push_back( fvs[i].getType() ); - } - //calculate the variables and substitution - vector< Node > vars; - vector< Node > subs; - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - vars.push_back( n[0][i] ); - } - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - //make the new function symbol - if( argTypes.empty() ){ - Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" ); - subs.push_back( s ); - }else{ - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() ); - Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" ); - //DOTHIS: set attribute on op, marking that it should not be selected as trigger - vector< Node > funcArgs; - funcArgs.push_back( op ); - funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); - subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) ); - } - } - //apply substitution - nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - return nn; - } - }else{ - //check if it contains a quantifier as a subterm - //if so, we will write this node - if( containsQuantifiers( n ) ){ - if( n.getType().isBoolean() ){ - if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); - } - return preSkolemizeQuantifiers( nn, polarity, fvs ); - }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ - vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) ); - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - }else{ - //must pull ite's - } - } - } - return n; - } -} - void SmtEnginePrivate::removeITEs() { d_smt.finalOptionsAreSet(); @@ -3156,13 +2870,25 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-strings-pp", d_assertionsToPreprocess); } if( d_smt.d_logic.isQuantified() ){ + //remove rewrite rules + for( unsigned i=0; i < d_assertionsToPreprocess.size(); i++ ) { + if( d_assertionsToPreprocess[i].getKind() == kind::REWRITE_RULE ){ + Node prev = d_assertionsToPreprocess[i]; + Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl; + d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertionsToPreprocess[i] ) ); + Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl; + Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; + } + } + dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); if( options::preSkolemQuant() ){ //apply pre-skolemization to existential quantifiers for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { Node prev = d_assertionsToPreprocess[i]; + Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl; vector< Node > fvs; - d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) ); + d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvs ) ); if( prev!=d_assertionsToPreprocess[i] ){ Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; @@ -3174,14 +2900,14 @@ void SmtEnginePrivate::processAssertions() { //quantifiers macro expansion bool success; do{ - QuantifierMacros qm; + quantifiers::QuantifierMacros qm; success = qm.simplify( d_assertionsToPreprocess, true ); }while( success ); } Trace("fo-rsn-enable") << std::endl; if( options::foPropQuant() ){ - FirstOrderPropagation fop; + quantifiers::FirstOrderPropagation fop; fop.simplify( d_assertionsToPreprocess ); } } @@ -3677,8 +3403,15 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin // Expand, then normalize hash_map<Node, Node, NodeHashFunction> cache; n = d_private->expandDefinitions(n, cache); - n = d_private->rewriteBooleanTerms(n); - n = Rewriter::rewrite(n); + // There are two ways model values for terms are computed (for historical + // reasons). One way is that used in check-model; the other is that + // used by the Model classes. It's not clear to me exactly how these + // two are different, but they need to be unified. This ugly hack here + // is to fix bug 554 until we can revamp boolean-terms and models [MGD] + if(!n.getType().isFunction()) { + n = d_private->rewriteBooleanTerms(n); + n = Rewriter::rewrite(n); + } Trace("smt") << "--- getting value of " << n << endl; TheoryModel* m = d_theoryEngine->getModel(); @@ -3970,28 +3703,30 @@ void SmtEngine::checkModel(bool hardFailure) { Debug("boolean-terms") << "++ got " << n << endl; Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl; - if(Theory::theoryOf(n) != THEORY_REWRITERULES) { + //AJR : FIXME need to ignore quantifiers too? + if( n.getKind() != kind::REWRITE_RULE ){ // In case it's a quantifier (or contains one), look up its value before // simplifying, or the quantifier might be irreparably altered. n = m->getValue(n); - } - - // Simplify the result. - n = d_private->simplify(n); - Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; - - TheoryId thy = Theory::theoryOf(n); - if(thy == THEORY_REWRITERULES) { + } else { // Note this "skip" is done here, rather than above. This is // because (1) the quantifier could in principle simplify to false, // which should be reported, and (2) checking for the quantifier // above, before simplification, doesn't catch buried quantifiers // anyway (those not at the top-level). - Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion" + Notice() << "SmtEngine::checkModel(): -- skipping quantifiers/rewrite-rules assertion" << endl; continue; } + // Simplify the result. + n = d_private->simplify(n); + Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; + + // Replace the already-known ITEs (this is important for ground ITEs under quantifiers). + n = d_private->d_iteRemover.replace(n); + Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl; + // As a last-ditch effort, ask model to simplify it. // Presently, this is only an issue for quantifiers, which can have a value // but don't show up in our substitution map above. diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c34d3ecba..2991ab21b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -30,7 +30,6 @@ #include "util/proof.h" #include "smt/modal_exception.h" #include "smt/logic_exception.h" -#include "util/hash.h" #include "options/options.h" #include "util/result.h" #include "util/sexpr.h" @@ -59,6 +58,7 @@ class TheoryEngine; class ProofManager; class Model; +class LogicRequest; class StatisticsRegistry; namespace context { @@ -281,6 +281,12 @@ class CVC4_PUBLIC SmtEngine { void finalOptionsAreSet(); /** + * Apply heuristics settings and other defaults. Done once, at + * finishInit() time. + */ + void setDefaults(); + + /** * Create theory engine, prop engine, decision engine. Called by * finalOptionsAreSet() */ @@ -331,6 +337,7 @@ class CVC4_PUBLIC SmtEngine { friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*); friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); friend ProofManager* ::CVC4::smt::currentProofManager(); + friend class ::CVC4::LogicRequest; // to access d_modelCommands friend class ::CVC4::Model; friend class ::CVC4::theory::TheoryModel; diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp index 4edd91a8d..987d2e3c7 100644 --- a/src/smt/smt_options_template.cpp +++ b/src/smt/smt_options_template.cpp @@ -62,11 +62,15 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) throw OptionException("command-verbosity value must be a tuple (command-name, integer)"); } + if(!value.isAtom()) { + throw OptionException("bad value for :" + key); + } + string optionarg = value.getValue(); ${smt_setoption_handlers} -#line 70 "${template}" +#line 74 "${template}" throw UnrecognizedOptionException(key); } @@ -126,7 +130,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const ${smt_getoption_handlers} -#line 130 "${template}" +#line 134 "${template}" throw UnrecognizedOptionException(key); } |