From 0042f301908763cf1edb8a2d56b3f373a0055908 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 23 Oct 2014 20:58:08 -0400 Subject: [PATCH] sygus input language and benchmark --- src/main/driver_unified.cpp | 10 + src/options/options_template.cpp | 3 +- src/parser/antlr_input.cpp | 5 + src/parser/parser_builder.cpp | 3 + src/parser/smt2/Makefile.am | 2 + src/parser/smt2/Smt2.g | 454 ++++++++++++++++--- src/parser/smt2/smt2.cpp | 39 +- src/parser/smt2/smt2.h | 84 +++- src/parser/smt2/sygus_input.cpp | 70 +++ src/parser/smt2/sygus_input.h | 96 ++++ src/theory/quantifiers/options | 4 +- src/util/language.cpp | 2 + src/util/language.h | 5 + test/Makefile.am | 1 + test/regress/regress0/Makefile.am | 4 +- test/regress/regress0/parser/Makefile.am | 1 + test/regress/regress0/parser/constraint.smt2 | 5 + test/regress/regress0/sygus/Makefile | 8 + test/regress/regress0/sygus/Makefile.am | 45 ++ test/regress/regress0/sygus/max.sl | 32 ++ test/regress/regress0/sygus/max.smt2 | 52 +++ test/regress/regress0/sygus/sygus-uf.sl | 20 + test/regress/run_regression | 23 +- 23 files changed, 892 insertions(+), 76 deletions(-) create mode 100644 src/parser/smt2/sygus_input.cpp create mode 100644 src/parser/smt2/sygus_input.h create mode 100644 test/regress/regress0/parser/constraint.smt2 create mode 100644 test/regress/regress0/sygus/Makefile create mode 100644 test/regress/regress0/sygus/Makefile.am create mode 100644 test/regress/regress0/sygus/max.sl create mode 100644 test/regress/regress0/sygus/max.smt2 create mode 100644 test/regress/regress0/sygus/sygus-uf.sl diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 9035ed8b8..c011671f8 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -34,6 +34,7 @@ #include "expr/command.h" #include "util/configuration.h" #include "options/options.h" +#include "theory/quantifiers/options.h" #include "main/command_executor.h" #ifdef PORTFOLIO_BUILD @@ -198,6 +199,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { opts.set(options::inputLanguage, language::input::LANG_CVC4); + } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) + || (len >= 3 && !strcmp(".sl", filename + len - 3))) { + opts.set(options::inputLanguage, language::input::LANG_SYGUS); } } } @@ -206,6 +210,12 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage])); } + // if doing sygus, turn on CEGQI by default + if(opts[options::inputLanguage] == language::input::LANG_SYGUS && + !opts.wasSetByUser(options::ceGuidedInst)) { + opts.set(options::ceGuidedInst, true); + } + // Determine which messages to show based on smtcomp_mode and verbosity if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(CVC4::null_os); diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 62bff7ec1..a9721ad20 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -265,6 +265,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ tptp TPTP format (cnf and fof)\n\ + sygus SyGuS format\n\ \n\ Languages currently supported as arguments to the --output-lang option:\n\ auto match output language to input language\n\ @@ -274,8 +275,8 @@ Languages currently supported as arguments to the --output-lang option:\n\ smt | smtlib | smt2 |\n\ smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ - z3str SMT-LIB 2.0 with Z3-str string constraints\n\ tptp TPTP format\n\ + z3str SMT-LIB 2.0 with Z3-str string constraints\n\ ast internal format (simple syntax trees)\n\ "; diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index f8730e372..4c779c46a 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -32,6 +32,7 @@ #include "parser/cvc/cvc_input.h" #include "parser/smt1/smt1_input.h" #include "parser/smt2/smt2_input.h" +#include "parser/smt2/sygus_input.h" #include "parser/tptp/tptp_input.h" #include "util/output.h" @@ -206,6 +207,10 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre input = new Smt2Input(inputStream, lang); break; + case LANG_SYGUS: + input = new SygusInput(inputStream); + break; + case LANG_TPTP: input = new TptpInput(inputStream); break; diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 241c9c815..a2faec704 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -93,6 +93,9 @@ Parser* ParserBuilder::build() case language::input::LANG_SMTLIB_V2_5: parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); break; + case language::input::LANG_SYGUS: + parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); + break; case language::input::LANG_TPTP: parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly); break; diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am index bf42e9288..38de258cc 100644 --- a/src/parser/smt2/Makefile.am +++ b/src/parser/smt2/Makefile.am @@ -33,6 +33,8 @@ libparsersmt2_la_SOURCES = \ smt2.cpp \ smt2_input.h \ smt2_input.cpp \ + sygus_input.h \ + sygus_input.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = \ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d7f4489bf..320fead5f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -214,6 +214,18 @@ parseCommand returns [CVC4::Command* cmd = NULL] | EOF { $cmd = 0; } ; +/** + * Parses a SyGuS command + * @return the parsed SyGuS command, or NULL if we've reached the end of the input + */ +parseSygus returns [CVC4::Command* cmd = NULL] +@declarations { + std::string name; +} + : LPAREN_TOK c=sygusCommand RPAREN_TOK { $cmd = c; } + | EOF { $cmd = 0; } + ; + /** * Parse the internal portion of the command, ignoring the surrounding * parentheses. @@ -468,6 +480,302 @@ command returns [CVC4::Command* cmd = NULL] } ; +sygusCommand returns [CVC4::Command* cmd = NULL] +@declarations { + std::string name, fun; + std::vector names; + Expr expr, expr2; + Type t, range; + std::vector terms; + std::vector sorts; + std::vector > sortedVarNames; + SExpr sexpr; + CommandSequence* seq; + std::vector datatypes; + std::vector< std::vector > ops; +} + : /* 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 { seq = new CommandSequence(); } + ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] symbolicExpr[sexpr] RPAREN_TOK + { PARSER_STATE->setOption(name.c_str(), sexpr); + seq->addCommand(new SetOptionCommand(name.c_str() + 1, sexpr)); + } + )+ RPAREN_TOK + { $cmd = seq; } + | /* sort definition */ + DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_SORT] + { PARSER_STATE->checkUserSymbol(name); } + LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK + { PARSER_STATE->pushScope(true); + for(std::vector::const_iterator i = names.begin(), + iend = names.end(); + i != iend; + ++i) { + sorts.push_back(PARSER_STATE->mkSort(*i)); + } + } + sortSymbol[t,CHECK_DECLARED] + { PARSER_STATE->popScope(); + // Do NOT call mkSort, since that creates a new sort! + // This name is not its own distinct sort, it's an alias. + PARSER_STATE->defineParameterizedType(name, sorts, t); + $cmd = new DefineTypeCommand(name, sorts, t); + } + | /* declare-var */ + DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortSymbol[t,CHECK_DECLARED] + { PARSER_STATE->mkSygusVar(name, t); + $cmd = new EmptyCommand(); } + | /* declare-fun */ + (DECLARE_FUN_TOK)=> + DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { PARSER_STATE->parseError("declare-fun not yet supported in SyGuS input"); } + | /* 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 ) { + std::vector sorts; + 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); + } + | /* synth-fun */ + SYNTH_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + { seq = new CommandSequence(); + 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)); + } + Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms); + terms.clear(); + terms.push_back(bvl); + } + sortSymbol[range,CHECK_DECLARED] + LPAREN_TOK + ( LPAREN_TOK + symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->pushScope(true); } + sortSymbol[t,CHECK_DECLARED] + { sorts.push_back(t); + datatypes.push_back(Datatype(name)); + ops.push_back(std::vector()); + if(!PARSER_STATE->isUnresolvedType(name)) { + // if not unresolved, must be undeclared + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT); + } + } + // Note the official spec for NTDef is missing the ( parens ) + // but they are necessary to parse SyGuS examples + LPAREN_TOK sygusGTerm[datatypes.back(), ops.back()]+ RPAREN_TOK + RPAREN_TOK + { PARSER_STATE->popScope(); } + )+ + RPAREN_TOK + { PARSER_STATE->popScope(); + seq = new CommandSequence(); + std::vector datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); + seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); + std::map evals; + // make all the evals first, since they are mutually referential + for(size_t i = 0; i < datatypeTypes.size(); ++i) { + DatatypeType dtt = datatypeTypes[i]; + const Datatype& dt = dtt.getDatatype(); + name = "eval_" + dt.getName(); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + std::vector evalType; + evalType.push_back(dtt); + for(size_t j = 0; j < terms[0].getNumChildren(); ++j) { + evalType.push_back(terms[0][j].getType()); + } + evalType.push_back(sorts[i]); + Expr eval = PARSER_STATE->mkVar(name, EXPR_MANAGER->mkFunctionType(evalType)); + evals.insert(std::make_pair(dtt, eval)); + if(i == 0) { + PARSER_STATE->addSygusFun(fun, eval); + } + } + // now go through and settle everything + for(size_t i = 0; i < datatypeTypes.size(); ++i) { + DatatypeType dtt = datatypeTypes[i]; + const Datatype& dt = dtt.getDatatype(); + Expr eval = evals[dtt]; + for(size_t j = 0; j < dt.getNumConstructors(); ++j) { + const DatatypeConstructor& ctor = dt[j]; + std::vector bvs, extraArgs; + for(size_t k = 0; k < ctor.getNumArgs(); ++k) { + Expr bv = EXPR_MANAGER->mkBoundVar(ctor[k].getName(), SelectorType(ctor[k].getType()).getRangeType()); + bvs.push_back(bv); + extraArgs.push_back(bv); + } + bvs.insert(bvs.end(), terms[0].begin(), terms[0].end()); + Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, bvs); + std::vector patv; + patv.push_back(eval); + std::vector applyv; + applyv.push_back(ctor.getConstructor()); + applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end()); + for(size_t k = 0; k < applyv.size(); ++k) { + } + patv.push_back(MK_EXPR(kind::APPLY_CONSTRUCTOR, applyv)); + patv.insert(patv.end(), terms[0].begin(), terms[0].end()); + Expr evalApply = MK_EXPR(kind::APPLY_UF, patv); + std::vector builtApply; + for(size_t k = 0; k < extraArgs.size(); ++k) { + patv.clear(); + patv.push_back(evals[DatatypeType(extraArgs[k].getType())]); + patv.push_back(extraArgs[k]); + patv.insert(patv.end(), terms[0].begin(), terms[0].end()); + builtApply.push_back(MK_EXPR(kind::APPLY_UF, patv)); + } + for(size_t k = 0; k < builtApply.size(); ++k) { + } + Expr builtTerm = ops[i][j].getKind() == kind::BUILTIN ? MK_EXPR(ops[i][j], builtApply) : ops[i][j]; + Expr assertion = MK_EXPR(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm); + Expr pattern = MK_EXPR(kind::INST_PATTERN, evalApply); + pattern = MK_EXPR(kind::INST_PATTERN_LIST, pattern); + assertion = MK_EXPR(kind::FORALL, bvl, assertion, pattern); + seq->addCommand(new AssertCommand(assertion)); + } + } + $cmd = seq; + } + | /* constraint */ + CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { PARSER_STATE->defineSygusFuns(); } + term[expr, expr2] + { PARSER_STATE->addSygusConstraint(expr); + $cmd = new EmptyCommand(); + } + | /* check-synth */ + CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType()); + Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar)); + std::vector bodyv; + Expr body = EXPR_MANAGER->mkExpr(kind::NOT, PARSER_STATE->getSygusConstraints()); + body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body); + body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr); + Command* c = new SetUserAttributeCommand("sygus", sygusVar); + c->setMuted(true); + PARSER_STATE->preemptCommand(c); + c = new AssertCommand(body); + 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()); + } + ; + +// SyGuS grammar term +sygusGTerm[CVC4::Datatype& dt, std::vector& ops] +@declarations { + std::string name; + Kind k; + Type t; + CVC4::DatatypeConstructor* ctor = NULL; + unsigned count = 0; +} + : LPAREN_TOK + ( builtinOp[k] + { ops.push_back(EXPR_MANAGER->operatorOf(k)); + name = kind::kindToString(k); + } + | symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { // what is this sygus term trying to accomplish here, if the + // symbol isn't yet declared?! probably the following line will + // fail, but we need an operator to continue here.. + Expr bv = PARSER_STATE->getVariable(name); + ops.push_back(bv); + } + ) + { name = dt.getName() + "_" + name; + std::string testerId("is-"); + testerId.append(name); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + ctor = new CVC4::DatatypeConstructor(name, testerId); + } + ( sortSymbol[t,CHECK_NONE] + { std::stringstream cname; + cname << name << "_" << ++count; + ctor->addArg(cname.str(), t); + } )+ RPAREN_TOK + { dt.addConstructor(*ctor); + delete ctor; } + | INTEGER_LITERAL + { ops.push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)))); + name = dt.getName() + "_" + AntlrInput::tokenText($INTEGER_LITERAL); + std::string testerId("is-"); + testerId.append(name); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId); + dt.addConstructor(c); + } + | HEX_LITERAL + { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); + std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); + ops.push_back(MK_CONST( BitVector(hexString, 16) )); + } + | BINARY_LITERAL + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); + std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); + ops.push_back(MK_CONST( BitVector(binString, 2) )); + } + | symbol[name,CHECK_DECLARED,SYM_VARIABLE] + { Expr bv = PARSER_STATE->getVariable(name); + ops.push_back(bv); + name = dt.getName() + "_" + name; + std::string testerId("is-"); + testerId.append(name); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId); + dt.addConstructor(c); + } + ; + // Separate this into its own rule (can be invoked by set-info or meta-info) metaInfoInternal[CVC4::Command*& cmd] @declarations { @@ -749,7 +1057,7 @@ datatypesDefCommand[bool isCo, CVC4::Command*& cmd] std::string name; std::vector sorts; } - : { PARSER_STATE->checkThatLogicIsSet(); + : { PARSER_STATE->checkThatLogicIsSet(); /* open a scope to keep the UnresolvedTypes contained */ PARSER_STATE->pushScope(true); } LPAREN_TOK /* parametric sorts */ @@ -759,7 +1067,7 @@ datatypesDefCommand[bool isCo, CVC4::Command*& cmd] RPAREN_TOK LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); - cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } ; rewriterulesCommand[CVC4::Command*& cmd] @@ -1785,6 +2093,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] std::string name; std::vector args; std::vector numerals; + bool indexed; } : sortName[name,CHECK_NONE] { @@ -1794,65 +2103,77 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] t = PARSER_STATE->mkUnresolvedType(name); } } - | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK - { - if( name == "BitVec" ) { - if( numerals.size() != 1 ) { - PARSER_STATE->parseError("Illegal bitvector type."); - } - if(numerals.front() == 0) { - PARSER_STATE->parseError("Illegal bitvector size: 0"); - } - t = EXPR_MANAGER->mkBitVectorType(numerals.front()); - } else if ( name == "FloatingPoint" ) { - if( numerals.size() != 2 ) { - PARSER_STATE->parseError("Illegal floating-point type."); - } - if(!validExponentSize(numerals[0])) { - PARSER_STATE->parseError("Illegal floating-point exponent size"); + | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;}) + symbol[name,CHECK_NONE,SYM_SORT] + ( nonemptyNumeralList[numerals] + { // allow sygus inputs to elide the `_' + if( !indexed && !PARSER_STATE->sygus() ) { + std::stringstream ss; + ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name << " ...)"; + PARSER_STATE->parseError(ss.str()); } - if(!validSignificandSize(numerals[1])) { - PARSER_STATE->parseError("Illegal floating-point significand size"); + if( name == "BitVec" ) { + if( numerals.size() != 1 ) { + PARSER_STATE->parseError("Illegal bitvector type."); + } + if(numerals.front() == 0) { + PARSER_STATE->parseError("Illegal bitvector size: 0"); + } + t = EXPR_MANAGER->mkBitVectorType(numerals.front()); + } else if ( name == "FloatingPoint" ) { + if( numerals.size() != 2 ) { + PARSER_STATE->parseError("Illegal floating-point type."); + } + if(!validExponentSize(numerals[0])) { + PARSER_STATE->parseError("Illegal floating-point exponent size"); + } + if(!validSignificandSize(numerals[1])) { + PARSER_STATE->parseError("Illegal floating-point significand size"); + } + t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]); + } else { + std::stringstream ss; + ss << "unknown indexed sort symbol `" << name << "'"; + PARSER_STATE->parseError(ss.str()); } - t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]); - } else { - std::stringstream ss; - ss << "unknown indexed symbol `" << name << "'"; - PARSER_STATE->parseError(ss.str()); } - } - | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK - { - if(args.empty()) { - PARSER_STATE->parseError("Extra parentheses around sort name not permitted in SMT-LIB"); - } else if(name == "Array" && - PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) { - if(args.size() != 2) { - PARSER_STATE->parseError("Illegal array type."); - } - t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); - } else if(name == "Set" && - PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) { - if(args.size() != 1) { - PARSER_STATE->parseError("Illegal set type."); + | sortList[args] + { if( indexed ) { + std::stringstream ss; + ss << "Unexpected use of indexing operator `_' before `" << name << "', try leaving it out"; + PARSER_STATE->parseError(ss.str()); } - t = EXPR_MANAGER->mkSetType( args[0] ); - } else if(check == CHECK_DECLARED || - PARSER_STATE->isDeclared(name, SYM_SORT)) { - t = PARSER_STATE->getSort(name, args); - } else { - // make unresolved type if(args.empty()) { - t = PARSER_STATE->mkUnresolvedType(name); - Debug("parser-param") << "param: make unres type " << name << std::endl; + PARSER_STATE->parseError("Extra parentheses around sort name not permitted in SMT-LIB"); + } else if(name == "Array" && + PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) { + if(args.size() != 2) { + PARSER_STATE->parseError("Illegal array type."); + } + t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); + } else if(name == "Set" && + PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) { + if(args.size() != 1) { + PARSER_STATE->parseError("Illegal set type."); + } + t = EXPR_MANAGER->mkSetType( args[0] ); + } else if(check == CHECK_DECLARED || + PARSER_STATE->isDeclared(name, SYM_SORT)) { + t = PARSER_STATE->getSort(name, args); } else { - t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args); - t = SortConstructorType(t).instantiate( args ); - Debug("parser-param") << "param: make unres param type " << name << " " << args.size() << " " - << PARSER_STATE->getArity( name ) << std::endl; + // make unresolved type + if(args.empty()) { + t = PARSER_STATE->mkUnresolvedType(name); + Debug("parser-param") << "param: make unres type " << name << std::endl; + } else { + t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args); + t = SortConstructorType(t).instantiate( args ); + Debug("parser-param") << "param: make unres param type " << name << " " << args.size() << " " + << PARSER_STATE->getArity( name ) << std::endl; + } } } - } + ) RPAREN_TOK ; /** @@ -1884,10 +2205,16 @@ symbol[std::string& id, PARSER_STATE->checkDeclaration(id, check, type); } } - | 'repeat' - { id = "repeat"; - PARSER_STATE->checkDeclaration(id, check, type); - } + | ( 'repeat' { id = "repeat"; } + /* these are keywords in SyGuS but we don't want to inhibit their + * use as symbols in SMT-LIB */ + | SET_OPTIONS_TOK { id = "set-options"; } + | DECLARE_VAR_TOK { id = "declare-var"; } + | SYNTH_FUN_TOK { id = "synth-fun"; } + | CONSTRAINT_TOK { id = "constraint"; } + | CHECK_SYNTH_TOK { id = "check-synth"; } + ) + { PARSER_STATE->checkDeclaration(id, check, type); } | QUOTED_SYMBOL { id = AntlrInput::tokenText($QUOTED_SYMBOL); /* strip off the quotes */ @@ -1954,11 +2281,11 @@ constructorDef[CVC4::Datatype& type] std::string id; CVC4::DatatypeConstructor* ctor = NULL; } - : symbol[id,CHECK_UNDECLARED,SYM_SORT] + : symbol[id,CHECK_UNDECLARED,SYM_VARIABLE] { // make the tester std::string testerId("is-"); testerId.append(id); - PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); ctor = new CVC4::DatatypeConstructor(id, testerId); } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* @@ -2031,6 +2358,13 @@ DEFINE_CONST_TOK : 'define-const'; SIMPLIFY_TOK : 'simplify'; INCLUDE_TOK : 'include'; +// SyGuS commands +SYNTH_FUN_TOK : 'synth-fun'; +CHECK_SYNTH_TOK : 'check-synth'; +DECLARE_VAR_TOK : 'declare-var'; +CONSTRAINT_TOK : 'constraint'; +SET_OPTIONS_TOK : 'set-options'; + // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern'; @@ -2058,7 +2392,7 @@ NOT_TOK : 'not'; OR_TOK : 'or'; // PERCENT_TOK : '%'; PLUS_TOK : '+'; -POUND_TOK : '#'; +//POUND_TOK : '#'; SELECT_TOK : 'select'; STAR_TOK : '*'; STORE_TOK : 'store'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7740d0b94..27ba07008 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -30,7 +30,8 @@ namespace parser { Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : Parser(exprManager,input,strictMode,parseOnly), - d_logicSet(false) { + d_logicSet(false), + d_nextSygusFun(0) { d_unsatCoreNames.push(std::map()); if( !strictModeEnabled() ) { addTheory(Smt2::THEORY_CORE); @@ -116,7 +117,7 @@ void Smt2::addFloatingPointOperators() { Parser::addOperator(kind::FLOATINGPOINT_GT); Parser::addOperator(kind::FLOATINGPOINT_ISN); Parser::addOperator(kind::FLOATINGPOINT_ISSN); - Parser::addOperator(kind::FLOATINGPOINT_ISZ); + Parser::addOperator(kind::FLOATINGPOINT_ISZ); Parser::addOperator(kind::FLOATINGPOINT_ISINF); Parser::addOperator(kind::FLOATINGPOINT_ISNAN); Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); @@ -297,7 +298,23 @@ void Smt2::resetAssertions() { this->Parser::reset(); } -void Smt2::setLogic(const std::string& name) { +void Smt2::setLogic(std::string name) { + if(sygus()) { + if(name == "Arrays") { + name = "AUF"; + } else if(name == "Reals") { + name = "UFLRA"; + } else if(name == "LIA") { + name = "UFLIA"; + } else if(name == "BV") { + name = "UFBV"; + } else { + std::stringstream ss; + ss << "Unknown SyGuS background logic `" << name << "'"; + parseError(ss.str()); + } + } + d_logicSet = true; if(logicIsForced()) { d_logic = getForcedLogic(); @@ -364,15 +381,19 @@ void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { void Smt2::checkThatLogicIsSet() { if( ! logicIsSet() ) { - if( strictModeEnabled() ) { + if(strictModeEnabled()) { parseError("set-logic must appear before this point."); } else { - warning("No set-logic command was given before this point."); - warning("CVC4 will assume the non-standard ALL_SUPPORTED logic."); - warning("Consider setting a stricter logic for (likely) better performance."); - warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED)."); + if(sygus()) { + setLogic("LIA"); + } else { + warning("No set-logic command was given before this point."); + warning("CVC4 will assume the non-standard ALL_SUPPORTED logic."); + warning("Consider setting a stricter logic for (likely) better performance."); + warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED)."); - setLogic("ALL_SUPPORTED"); + setLogic("ALL_SUPPORTED"); + } Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED"); c->setMuted(true); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 82498b624..50edc3311 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -62,6 +62,9 @@ private: std::pair d_lastNamedTerm; // this is a user-context stack std::stack< std::map > d_unsatCoreNames; + std::vector d_sygusVars, d_sygusConstraints, d_sygusFunSymbols; + std::vector< std::pair > d_sygusFuns; + size_t d_nextSygusFun; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); @@ -94,7 +97,7 @@ public: * * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ - void setLogic(const std::string& name); + void setLogic(std::string name); /** * Get the logic. @@ -107,6 +110,9 @@ public: bool v2_5() const { return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5; } + bool sygus() const { + return getInput()->getLanguage() == language::input::LANG_SYGUS; + } void setLanguage(InputLanguage lang) { ((Smt2Input*) getInput())->setLanguage(lang); @@ -166,6 +172,82 @@ public: return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1)))); } + Expr mkSygusVar(const std::string& name, const Type& type) { + Expr e = mkBoundVar(name, type); + d_sygusVars.push_back(e); + return e; + } + + void addSygusFun(const std::string& fun, Expr eval) { + d_sygusFuns.push_back(std::make_pair(fun, eval)); + } + + void defineSygusFuns() { + // only define each one once + while(d_nextSygusFun < d_sygusFuns.size()) { + std::pair p = d_sygusFuns[d_nextSygusFun]; + std::string fun = p.first; + Expr eval = p.second; + FunctionType evalType = eval.getType(); + std::vector argTypes = evalType.getArgTypes(); + Type rangeType = evalType.getRangeType(); + + // first make the function type + std::vector funType; + for(size_t j = 1; j < argTypes.size(); ++j) { + funType.push_back(argTypes[j]); + } + Type funt = getExprManager()->mkFunctionType(funType, rangeType); + + // copy the bound vars + std::vector sygusVars; + std::vector types; + for(size_t i = 0; i < d_sygusVars.size(); ++i) { + std::stringstream ss; + ss << d_sygusVars[i]; + Type type = d_sygusVars[i].getType(); + sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type)); + types.push_back(type); + } + + Type t = getExprManager()->mkFunctionType(types, rangeType); + Expr lambda = mkFunction(fun, t, ExprManager::VAR_FLAG_DEFINED); + std::vector applyv; + Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]); + d_sygusFunSymbols.push_back(funbv); + applyv.push_back(eval); + applyv.push_back(funbv); + for(size_t i = 0; i < d_sygusVars.size(); ++i) { + applyv.push_back(d_sygusVars[i]); + } + Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv); + Command* cmd = new DefineFunctionCommand(fun, lambda, d_sygusVars, apply); + preemptCommand(cmd); + + ++d_nextSygusFun; + } + } + + void addSygusConstraint(Expr constraint) { + d_sygusConstraints.push_back(constraint); + } + + Expr getSygusConstraints() { + switch(d_sygusConstraints.size()) { + case 0: return getExprManager()->mkConst(bool(true)); + case 1: return d_sygusConstraints[0]; + default: return getExprManager()->mkExpr(kind::AND, d_sygusConstraints); + } + } + + const std::vector& getSygusVars() { + return d_sygusVars; + } + + const std::vector& getSygusFunSymbols() { + return d_sygusFunSymbols; + } + /** * Smt2 parser provides its own checkDeclaration, which does the * same as the base, but with some more helpful errors. diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp new file mode 100644 index 000000000..8bd02485b --- /dev/null +++ b/src/parser/smt2/sygus_input.cpp @@ -0,0 +1,70 @@ +/********************* */ +/*! \file sygus_input.cpp + ** \verbatim + ** Original author: Christopher L. Conway + ** Major contributors: Morgan Deters + ** 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 [[ Add file-specific comments here ]]. + ** + ** [[ Add file-specific comments here ]] + **/ + +#include + +#include "parser/smt2/sygus_input.h" +#include "expr/expr_manager.h" +#include "parser/input.h" +#include "parser/parser.h" +#include "parser/parser_exception.h" +#include "parser/smt2/sygus_input.h" +#include "parser/smt2/generated/Smt2Lexer.h" +#include "parser/smt2/generated/Smt2Parser.h" + +namespace CVC4 { +namespace parser { + +/* Use lookahead=2 */ +SygusInput::SygusInput(AntlrInputStream& inputStream) : + AntlrInput(inputStream, 2) { + + pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); + assert( input != NULL ); + + d_pSmt2Lexer = Smt2LexerNew(input); + if( d_pSmt2Lexer == NULL ) { + throw ParserException("Failed to create SMT2 lexer."); + } + + setAntlr3Lexer( d_pSmt2Lexer->pLexer ); + + pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); + assert( tokenStream != NULL ); + + d_pSmt2Parser = Smt2ParserNew(tokenStream); + if( d_pSmt2Parser == NULL ) { + throw ParserException("Failed to create SMT2 parser."); + } + + setAntlr3Parser(d_pSmt2Parser->pParser); +} + +SygusInput::~SygusInput() { + d_pSmt2Lexer->free(d_pSmt2Lexer); + d_pSmt2Parser->free(d_pSmt2Parser); +} + +Command* SygusInput::parseCommand() { + return d_pSmt2Parser->parseSygus(d_pSmt2Parser); +} + +Expr SygusInput::parseExpr() { + return d_pSmt2Parser->parseExpr(d_pSmt2Parser); +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h new file mode 100644 index 000000000..d5e6b8b87 --- /dev/null +++ b/src/parser/smt2/sygus_input.h @@ -0,0 +1,96 @@ +/********************* */ +/*! \file sygus_input.h + ** \verbatim + ** Original author: Christopher L. Conway + ** Major contributors: Morgan Deters + ** 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 [[ Add file-specific comments here ]]. + ** + ** [[ Add file-specific comments here ]] + **/ + +#include "cvc4parser_private.h" + +#ifndef __CVC4__PARSER__SYGUS_INPUT_H +#define __CVC4__PARSER__SYGUS_INPUT_H + +#include "parser/antlr_input.h" +#include "parser/smt2/generated/Smt2Lexer.h" +#include "parser/smt2/generated/Smt2Parser.h" + +// extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); + +namespace CVC4 { + +class Command; +class Expr; +class ExprManager; + +namespace parser { + +class Smt2; + +class SygusInput : public AntlrInput { + typedef AntlrInput super; + + /** The ANTLR3 SMT2 lexer for the input. */ + pSmt2Lexer d_pSmt2Lexer; + + /** The ANTLR3 SMT2 parser for the input. */ + pSmt2Parser d_pSmt2Parser; + + /** Which (variant of the) input language we're using */ + InputLanguage d_lang; + + /** + * Initialize the class. Called from the constructors once the input + * stream is initialized. + */ + void init(); + +public: + + /** + * Create an input. + * + * @param inputStream the input stream to use + */ + SygusInput(AntlrInputStream& inputStream); + + /** Destructor. Frees the lexer and the parser. */ + virtual ~SygusInput(); + + /** Get the language that this Input is reading. */ + InputLanguage getLanguage() const throw() { + return language::input::LANG_SYGUS; + } + +protected: + + /** + * Parse a command from the input. Returns NULL if + * there is no command there to parse. + * + * @throws ParserException if an error is encountered during parsing. + */ + Command* parseCommand(); + + /** + * Parse an expression from the input. Returns a null + * Expr if there is no expression there to parse. + * + * @throws ParserException if an error is encountered during parsing. + */ + Expr parseExpr(); + +};/* class SygusInput */ + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__SYGUS_INPUT_H */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 8c43453d7..e04e76835 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -192,8 +192,8 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0 option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false more aggressive merging for universal equality engine, introduces terms -option ceGuidedInst --cegqi bool :default false - counterexample guided quantifier instantiation +option ceGuidedInst --cegqi bool :default false :read-write + counterexample-guided quantifier instantiation option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" if and how to apply fairness for cegqi diff --git a/src/util/language.cpp b/src/util/language.cpp index ca611f729..4b213422c 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -113,6 +113,8 @@ InputLanguage toInputLanguage(std::string language) { } else if(language == "smtlib2.5" || language == "smt2.5" || language == "LANG_SMTLIB_V2_5") { return input::LANG_SMTLIB_V2_5; + } else if(language == "sygus" || language == "LANG_SYGUS") { + return input::LANG_SYGUS; } else if(language == "tptp" || language == "LANG_TPTP") { return input::LANG_TPTP; } else if(language == "z3str" || language == "z3-str" || diff --git a/src/util/language.h b/src/util/language.h index abde0b509..c865c2615 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -60,6 +60,8 @@ enum CVC4_PUBLIC Language { // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10 // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES + /** The SyGuS input language */ + LANG_SYGUS, /** LANG_MAX is > any valid InputLanguage id */ LANG_MAX @@ -89,6 +91,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_Z3STR: out << "LANG_Z3STR"; break; + case LANG_SYGUS: + out << "LANG_SYGUS"; + break; default: out << "undefined_input_language"; } diff --git a/test/Makefile.am b/test/Makefile.am index 236443eb9..dcb58b591 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -58,6 +58,7 @@ subdirs_to_check = \ regress/regress0/strings \ regress/regress0/sets \ regress/regress0/parser \ + regress/regress0/sygus \ regress/regress1 \ regress/regress1/arith \ regress/regress2 \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 68d002367..128072f24 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,5 +1,5 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser -DIST_SUBDIRS = $(SUBDIRS) #. arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser sygus +DIST_SUBDIRS = $(SUBDIRS) # don't override a BINARY imported from a personal.mk @mk_if@eq ($(BINARY),) diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am index eb27e797b..44318d492 100644 --- a/test/regress/regress0/parser/Makefile.am +++ b/test/regress/regress0/parser/Makefile.am @@ -20,6 +20,7 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ declarefun-emptyset-uf.smt2 \ + constraint.smt2 \ strings20.smt2 \ strings25.smt2 diff --git a/test/regress/regress0/parser/constraint.smt2 b/test/regress/regress0/parser/constraint.smt2 new file mode 100644 index 000000000..ffd56625e --- /dev/null +++ b/test/regress/regress0/parser/constraint.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_UF) +(set-info :status sat) +(declare-sort U 0) +(declare-fun Constraint () U) +(check-sat) diff --git a/test/regress/regress0/sygus/Makefile b/test/regress/regress0/sygus/Makefile new file mode 100644 index 000000000..cc09c6091 --- /dev/null +++ b/test/regress/regress0/sygus/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/sygus + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am new file mode 100644 index 000000000..ad1296af0 --- /dev/null +++ b/test/regress/regress0/sygus/Makefile.am @@ -0,0 +1,45 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = + +# sygus tests currently taking too long for make regress +EXTRA_DIST = $(TESTS) \ + max.sl \ + max.smt2 \ + sygus-uf.sl + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif + +# disabled tests, yet distribute +#EXTRA_DIST += \ +# setofsets-disequal.smt2 + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/sygus/max.sl b/test/regress/regress0/sygus/max.sl new file mode 100644 index 000000000..aea8e8186 --- /dev/null +++ b/test/regress/regress0/sygus/max.sl @@ -0,0 +1,32 @@ +; EXPECT: unsat +(set-logic LIA) + +(synth-fun max ((x Int) (y Int)) Int + ((Start Int (0 1 x y + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (not StartBool) + (<= Start Start))))) + +;(synth-fun min ((x Int) (y Int)) Int +; ((Start Int ((Constant Int) (Variable Int) +; (+ Start Start) +; (- Start Start) +; (ite StartBool Start Start))) +; (StartBool Bool ((and StartBool StartBool) +; (not StartBool) +; (<= Start Start))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (>= (max x y) x)) +(constraint (>= (max x y) y)) +(constraint (or (= x (max x y)) + (= y (max x y)))) +;(constraint (= (+ (max x y) (min x y)) +; (+ x y))) + +(check-synth) diff --git a/test/regress/regress0/sygus/max.smt2 b/test/regress/regress0/sygus/max.smt2 new file mode 100644 index 000000000..97c223e16 --- /dev/null +++ b/test/regress/regress0/sygus/max.smt2 @@ -0,0 +1,52 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi + +(set-logic UFDTLIA) + +(declare-datatypes () ((start (startx) + (starty) + (start1) + (start0) + (startplus (startplus1 start) (startplus2 start)) + (startminus (startminus1 start) (startminus2 start)) + (startite (startite1 startbool) (startite2 start) (startite3 start))) + (startbool (startand (startand1 startbool) (startand2 startbool)) + (startor (startor1 startbool) (startor2 startbool)) + (startnot (startnot1 startbool)) + (startleq (startleq1 start) (startleq2 start)) + (starteq (starteq1 start) (starteq2 start)) + (startgeq (startgeq1 start) (startgeq2 start)) + ))) + +(declare-fun eval (start Int Int) Int) +(declare-fun evalbool (startbool Int Int) Bool) + +(assert (forall ((x Int) (y Int)) (! (= (eval startx x y) x) :pattern ((eval startx x y))))) +(assert (forall ((x Int) (y Int)) (! (= (eval starty x y) y) :pattern ((eval starty x y))))) +(assert (forall ((x Int) (y Int)) (! (= (eval start0 x y) 0) :pattern ((eval start0 x y))))) +(assert (forall ((x Int) (y Int)) (! (= (eval start1 x y) 1) :pattern ((eval start1 x y))))) +(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (eval (startplus s1 s2) x y) (+ (eval s1 x y) (eval s2 x y))) :pattern ((eval (startplus s1 s2) x y))))) +(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (eval (startminus s1 s2) x y) (- (eval s1 x y) (eval s2 x y))) :pattern ((eval (startminus s1 s2) x y))))) +(assert (forall ((s1 startbool) (s2 start) (s3 start) (x Int) (y Int)) (! (= (eval (startite s1 s2 s3) x y) (ite (evalbool s1 x y) (eval s2 x y) (eval s3 x y))) + :pattern ((eval (startite s1 s2 s3) x y))))) + +(assert (forall ((s1 startbool) (s2 startbool) (x Int) (y Int)) (! (= (evalbool (startand s1 s2) x y) (and (evalbool s1 x y) (evalbool s2 x y))) + :pattern ((evalbool (startand s1 s2) x y))))) +(assert (forall ((s1 startbool) (s2 startbool) (x Int) (y Int)) (! (= (evalbool (startor s1 s2) x y) (or (evalbool s1 x y) (evalbool s2 x y))) + :pattern ((evalbool (startor s1 s2) x y))))) +(assert (forall ((s1 startbool) (x Int) (y Int)) (! (= (evalbool (startnot s1) x y) (not (evalbool s1 x y))) + :pattern ((evalbool (startnot s1) x y))))) +(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (startleq s1 s2) x y) (<= (eval s1 x y) (eval s2 x y))) + :pattern ((evalbool (startleq s1 s2) x y))))) +(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (starteq s1 s2) x y) (= (eval s1 x y) (eval s2 x y))) + :pattern ((evalbool (starteq s1 s2) x y))))) +(assert (forall ((s1 start) (s2 start) (x Int) (y Int)) (! (= (evalbool (startgeq s1 s2) x y) (>= (eval s1 x y) (eval s2 x y))) + :pattern ((evalbool (startgeq s1 s2) x y))))) + + +(define-fun P ((fmax start) (x Int) (y Int)) Bool (and (>= (eval fmax x y) x) (>= (eval fmax x y) y) (or (= (eval fmax x y) x) (= (eval fmax x y) y)))) + +(assert (forall ((fmax start)) (! (exists ((x Int) (y Int)) (not (P fmax x y))) :sygus))) + + +(check-sat) diff --git a/test/regress/regress0/sygus/sygus-uf.sl b/test/regress/regress0/sygus/sygus-uf.sl new file mode 100644 index 000000000..95cd8771e --- /dev/null +++ b/test/regress/regress0/sygus/sygus-uf.sl @@ -0,0 +1,20 @@ +(set-logic LIA) + +(declare-fun uf (Int) Int) + +(synth-fun f ((x Int) (y Int)) Bool + ((Start Bool (true false + (<= IntExpr IntExpr) + (= IntExpr IntExpr) + (and Start Start) + (or Start Start) + (not Start))) + (IntExpr Int (0 1 x y + (+ IntExpr IntExpr) + (- IntExpr IntExpr))))) + +(declare-var x Int) + +(constraint (f (uf x) (uf x))) + +(check-synth) diff --git a/test/regress/run_regression b/test/regress/run_regression index 062458055..7b215dc2a 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -179,8 +179,29 @@ elif expr "$benchmark" : '.*\.p$' &>/dev/null; then if grep -q '^% COMMAND-LINE: ' "$benchmark"; then command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` fi +elif expr "$benchmark" : '.*\.sy$' &>/dev/null; then + lang=sygus + if test -e "$benchmark.expect"; then + expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` + expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` + command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'` + if [ -z "$expected_exit_status" ]; then + expected_exit_status=0 + fi + elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then + expected_output=`grep '^; EXPECT: ' "$benchmark" | sed 's,^; EXPECT: ,,'` + expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'` + expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'` + command_line=`grep '^; COMMAND-LINE: ' "$benchmark" | sed 's,^; COMMAND-LINE: ,,'` + if [ -z "$expected_exit_status" ]; then + expected_exit_status=0 + fi + else + error "cannot determine expected output of \`$benchmark'" + fi else - error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p" + error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p or *.sy" fi command_line="${command_line:+$command_line }--lang=$lang" -- 2.30.2