From 1aaf70f23d8f2061e5c05ca98d12deea06494a25 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 18 Sep 2015 00:04:26 +0200 Subject: [PATCH] Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quantified formulas with non-constant polarity. --- src/parser/smt2/Smt2.g | 116 +++---------------- src/theory/quantifiers/alpha_equivalence.cpp | 6 +- src/theory/quantifiers/fun_def_process.cpp | 5 + test/regress/regress0/sygus/Makefile.am | 5 +- 4 files changed, 27 insertions(+), 105 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3dda54a18..4e5c27e3d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -247,7 +247,11 @@ command returns [CVC4::Command* cmd = NULL] PARSER_STATE->parseError("Only one set-logic is allowed."); } PARSER_STATE->setLogic(name); - $cmd = new SetBenchmarkLogicCommand(name); } + if( PARSER_STATE->sygus() ){ + $cmd = new SetBenchmarkLogicCommand("ALL_SUPPORTED"); + }else{ + $cmd = new SetBenchmarkLogicCommand(name); + } } | /* set-info */ SET_INFO_TOK metaInfoInternal[cmd] | /* get-info */ @@ -362,6 +366,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetAssignmentCommand(); } | /* assertion */ ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support assert command."); } } { PARSER_STATE->clearLastNamedTerm(); } term[expr, expr2] { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; @@ -372,6 +377,7 @@ command returns [CVC4::Command* cmd = NULL] } | /* check-sat */ CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support check-sat command."); } } ( term[expr, expr2] { if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Extended commands (such as check-sat with an argument) are not permitted while operating in strict compliance mode."); @@ -505,45 +511,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr; int startIndex = -1; } - : /* set the logic */ - SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] - { PARSER_STATE->setLogic(name); - $cmd = new SetBenchmarkLogicCommand("ALL_SUPPORTED"); } - | /* set-options */ - SET_OPTIONS_TOK LPAREN_TOK - ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_QUOTED_LITERAL RPAREN_TOK - { //TODO? - //PARSER_STATE->setOption(name.c_str(), sexpr); - //seq->addCommand(new SetOptionCommand(name.c_str() + 1, sexpr)); - } - )+ RPAREN_TOK - { $cmd = new EmptyCommand(); } - | /* sort definition */ - DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_SORT] - { PARSER_STATE->checkUserSymbol(name); } - ( LPAREN_TOK SYGUS_ENUM_TOK LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK RPAREN_TOK { - Debug("parser-sygus") << "Defining enum datatype " << name << " with " << names.size() << " constructors." << std::endl; - //make datatype - datatypes.push_back(Datatype(name)); - for( unsigned i=0; icheckDeclaration(cname, CHECK_UNDECLARED, SYM_VARIABLE); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(cname, testerId); - datatypes[0].addConstructor(c); - } - std::vector datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); - $cmd = new DatatypeDeclarationCommand(datatypeTypes); - } - | sortSymbol[t,CHECK_DECLARED] { - PARSER_STATE->defineParameterizedType(name, sorts, t); - $cmd = new DefineTypeCommand(name, sorts, t); - } - ) - | /* declare-var */ + : /* declare-var */ DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } @@ -557,57 +525,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] sortSymbol[t,CHECK_DECLARED] { PARSER_STATE->mkSygusVar(name, t, true); $cmd = new EmptyCommand(); } - | /* declare-fun */ - DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - { PARSER_STATE->checkUserSymbol(name); } - LPAREN_TOK sortList[sorts] RPAREN_TOK - sortSymbol[t,CHECK_DECLARED] - { Debug("parser") << "declare fun: '" << name << "'" << std::endl; - if( sorts.size() > 0 ) { - if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseError(std::string("Functions (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString()); - } - t = EXPR_MANAGER->mkFunctionType(sorts, t); - } - Expr func = PARSER_STATE->mkVar(name, t); - $cmd = new DeclareFunctionCommand(name, func, t); } - | /* function definition */ - DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - { PARSER_STATE->checkUserSymbol(name); } - LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - sortSymbol[t,CHECK_DECLARED] - { /* add variables to parser state before parsing term */ - Debug("parser") << "define fun: '" << name << "'" << std::endl; - if( sortedVarNames.size() > 0 ) { - sorts.reserve(sortedVarNames.size()); - for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; - ++i) { - sorts.push_back((*i).second); - } - t = EXPR_MANAGER->mkFunctionType(sorts, t); - } - PARSER_STATE->pushScope(true); - for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; - ++i) { - terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); - } - } - term[expr, expr2] - { PARSER_STATE->popScope(); - // declare the name down here (while parsing term, signature - // must not be extended with the name itself; no recursion - // permitted) - Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); - $cmd = new DefineFunctionCommand(name, func, terms, expr); - } - | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] - | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] + | /* synth-fun */ ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] @@ -838,14 +756,14 @@ sygusCommand returns [CVC4::Command* cmd = NULL] PARSER_STATE->preemptCommand(c); $cmd = new CheckSatCommand(); } - - /* error handling */ - | (~(CHECK_SYNTH_TOK))=> token=. - { std::string id = AntlrInput::tokenText($token); - std::stringstream ss; - ss << "Not a recognized SyGuS command: `" << id << "'"; - PARSER_STATE->parseError(ss.str()); - } + | c = command { $cmd = c; } + // /* error handling */ + // | (~(CHECK_SYNTH_TOK))=> token=. + // { std::string id = AntlrInput::tokenText($token); + // std::stringstream ss; + // ss << "Not a recognized SyGuS command: `" << id << "'"; + // PARSER_STATE->parseError(ss.str()); + // } ; // SyGuS grammar term diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 84bf2ec14..b72f15a01 100755 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -55,9 +55,9 @@ bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE return true; }else{ //lemma ( q <=> d_quant ) - Trace("alpha-eq") << "Alpha equivalent : " << std::endl; - Trace("alpha-eq") << " " << q << std::endl; - Trace("alpha-eq") << " " << aen->d_quant << std::endl; + Trace("quant-ae") << "Alpha equivalent : " << std::endl; + Trace("quant-ae") << " " << q << std::endl; + Trace("quant-ae") << " " << aen->d_quant << std::endl; qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) ); return false; } diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 632e19a18..7d5e33fdb 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -119,6 +119,11 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl; if( n.getKind()==FORALL ){ Node c = simplifyFormula( n[1], pol, hasPol, constraints, hd, is_fun_def ); + //append prenex to constraints + for( unsigned i=0; imkNode( FORALL, n[0], constraints[i] ); + constraints[i] = Rewriter::rewrite( constraints[i] ); + } if( c!=n[1] ){ return NodeManager::currentNM()->mkNode( FORALL, n[0], c ); }else{ diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 0c78fd7bf..16ad2e4d8 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -39,7 +39,6 @@ TESTS = commutative.sy \ dup-op.sy \ nflat-fwd.sy \ nflat-fwd-3.sy \ - enum-test.sy \ no-syntax-test-bool.sy \ inv-example.sy \ uminus_one.sy \ @@ -49,8 +48,8 @@ TESTS = commutative.sy \ # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ max.smt2 \ - sygus-uf.sl - + sygus-uf.sl \ + enum-test.sy #if CVC4_BUILD_PROFILE_COMPETITION #else -- 2.30.2