From 043de624d75615ae0f5b163e2effb44cac0885a3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 29 Nov 2019 09:31:54 -0600 Subject: [PATCH] Check free variables in assertions when using SyGuS (#3504) --- src/options/language.cpp | 10 ++++++++ src/options/language.h | 4 ++++ src/parser/smt2/Smt2.g | 11 --------- src/smt/smt_engine.cpp | 49 +++++++++++++++++++++++++++------------- 4 files changed, 47 insertions(+), 27 deletions(-) diff --git a/src/options/language.cpp b/src/options/language.cpp index 0f2c513b6..8c6f8421f 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -68,6 +68,16 @@ bool isOutputLang_smt2_6(OutputLanguage lang, bool exact) && lang <= output::LANG_SMTLIB_V2_END); } +bool isInputLangSygus(InputLanguage lang) +{ + return lang == input::LANG_SYGUS || lang == input::LANG_SYGUS_V2; +} + +bool isOutputLangSygus(OutputLanguage lang) +{ + return lang == output::LANG_SYGUS || lang == output::LANG_SYGUS_V2; +} + InputLanguage toInputLanguage(OutputLanguage language) { switch(language) { case output::LANG_SMTLIB_V2_0: diff --git a/src/options/language.h b/src/options/language.h index b7eb16f91..3a9ebf9d5 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -220,6 +220,10 @@ bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC; bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_PUBLIC; bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_PUBLIC; +/** Is the language a variant of the SyGuS input language? */ +bool isInputLangSygus(InputLanguage lang) CVC4_PUBLIC; +bool isOutputLangSygus(OutputLanguage lang) CVC4_PUBLIC; + InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC; OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC; InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a5033278d..9110b9660 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -392,17 +392,6 @@ command [std::unique_ptr* cmd] csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } - // if sygus, check whether it has a free variable - // this is because, due to the sygus format, one can write assertions - // that have free function variables in them - if (PARSER_STATE->sygus()) - { - if (expr.hasFreeVariable()) - { - PARSER_STATE->parseError("Assertion has free variable. Perhaps you " - "meant constraint instead of assert?"); - } - } } | /* check-sat */ CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } 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() */ -- 2.30.2