diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 49 |
1 files changed, 33 insertions, 16 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index dfd3c9fee..ca5558e87 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -751,7 +751,12 @@ class SmtEnginePrivate : public NodeManagerListener { * formula might be pushed out to the propositional layer * immediately, or it might be simplified and kept, or it might not * even be simplified. - * the 2nd and 3rd arguments added for bookkeeping for proofs + * The arguments isInput and isAssumption are used for bookkeeping for proofs. + * The argument maybeHasFv should be set to true if the assertion may have + * free variables. By construction, assertions from the smt2 parser are + * guaranteed not to have free variables. However, other cases such as + * assertions from the SyGuS parser may have free variables (say if the + * input contains an assert or define-fun-rec command). * * @param isAssumption If true, the formula is considered to be an assumption * (this is used to distinguish assertions and assumptions) @@ -759,7 +764,8 @@ class SmtEnginePrivate : public NodeManagerListener { void addFormula(TNode n, bool inUnsatCore, bool inInput = true, - bool isAssumption = false); + bool isAssumption = false, + bool maybeHasFv = false); /** Expand definitions in n. */ Node expandDefinitions(TNode n, @@ -1155,15 +1161,9 @@ void SmtEngine::setDefaults() { // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus. options::bitvectorDivByZeroConst.set( language::isInputLang_smt2_6(options::inputLanguage()) - || options::inputLanguage() == language::input::LANG_SYGUS - || options::inputLanguage() == language::input::LANG_SYGUS_V2); - } - bool is_sygus = false; - if (options::inputLanguage() == language::input::LANG_SYGUS - || options::inputLanguage() == language::input::LANG_SYGUS_V2) - { - is_sygus = true; + || language::isInputLangSygus(options::inputLanguage())); } + bool is_sygus = language::isInputLangSygus(options::inputLanguage()); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { @@ -2647,6 +2647,7 @@ void SmtEngine::defineFunctionsRec( } ExprManager* em = getExprManager(); + bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); for (unsigned i = 0, size = funcs.size(); i < size; i++) { // we assert a quantified formula @@ -2686,7 +2687,7 @@ void SmtEngine::defineFunctionsRec( { d_assertionList->push_back(e); } - d_private->addFormula(e.getNode(), false); + d_private->addFormula(e.getNode(), false, true, false, maybeHasFv); } } @@ -3579,10 +3580,8 @@ void SmtEnginePrivate::processAssertions() { getIteSkolemMap().clear(); } -void SmtEnginePrivate::addFormula(TNode n, - bool inUnsatCore, - bool inInput, - bool isAssumption) +void SmtEnginePrivate::addFormula( + TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv) { if (n == d_true) { // nothing to do @@ -3594,6 +3593,23 @@ void SmtEnginePrivate::addFormula(TNode n, << ", inInput = " << inInput << ", isAssumption = " << isAssumption << endl; + // Ensure that it does not contain free variables + if (maybeHasFv) + { + if (expr::hasFreeVar(n)) + { + std::stringstream se; + se << "Cannot process assertion with free variable."; + if (language::isInputLangSygus(options::inputLanguage())) + { + // Common misuse of SyGuS is to use top-level assert instead of + // constraint when defining the synthesis conjecture. + se << " Perhaps you meant `constraint` instead of `assert`?"; + } + throw ModalException(se.str().c_str()); + } + } + // Give it to proof manager PROOF( if( inInput ){ @@ -3901,7 +3917,8 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) if(d_assertionList != NULL) { d_assertionList->push_back(e); } - d_private->addFormula(e.getNode(), inUnsatCore); + bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); + d_private->addFormula(e.getNode(), inUnsatCore, true, false, maybeHasFv); return quickCheck().asValidityResult(); }/* SmtEngine::assertFormula() */ |