diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
commit | f62d9456b41bf17df1d339e46776c9213cb3705a (patch) | |
tree | 01d3448b3c9fe89ead56c72b18f8516292092e13 /src/parser | |
parent | 7943953741c67d8246f983e193d26812d959b4cd (diff) |
Squashed merge of SygusComp 2015 branch.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.h | 27 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 453 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 358 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 71 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 2 |
5 files changed, 579 insertions, 332 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 53241709d..9c2c7f7be 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -42,6 +42,33 @@ class FunctionType; class Type; class ResourceManager; +//for sygus gterm two-pass parsing +class CVC4_PUBLIC SygusGTerm { +public: + enum{ + gterm_op, + gterm_let, + gterm_constant, + gterm_variable, + gterm_input_variable, + gterm_local_variable, + gterm_nested_sort, + gterm_unresolved, + gterm_ignore, + }; + Type d_type; + Expr d_expr; + std::vector< Expr > d_let_vars; + unsigned d_gterm_type; + std::string d_name; + std::vector< SygusGTerm > d_children; + + unsigned getNumChildren() { return d_children.size(); } + void addChild(){ + d_children.push_back( SygusGTerm() ); + } +}; + namespace parser { class Input; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 0edd8bc46..1564e6f3e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -492,6 +492,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector<std::pair<std::string, Type> > sortedVarNames; SExpr sexpr; CommandSequence* seq; + std::vector< std::vector< CVC4::SygusGTerm > > sgts; std::vector< CVC4::Datatype > datatypes; std::vector< std::vector<Expr> > ops; std::vector< std::vector< std::string > > cnames; @@ -499,7 +500,6 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector< bool > allow_const; std::vector< std::vector< std::string > > unresolved_gterm_sym; bool read_syntax = false; - int sygus_dt_index = 0; Type sygus_ret; std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr; @@ -522,22 +522,27 @@ sygusCommand returns [CVC4::Command* cmd = NULL] 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<std::string>::const_iterator i = names.begin(), - iend = names.end(); - i != iend; - ++i) { - sorts.push_back(PARSER_STATE->mkSort(*i)); + ( 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; i<names.size(); i++ ){ + std::string cname = name + "__Enum__" + names[i]; + std::string testerId("is-"); + testerId.append(cname); + PARSER_STATE->checkDeclaration(cname, CHECK_UNDECLARED, SYM_VARIABLE); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(cname, testerId); + datatypes[0].addConstructor(c); + } + std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); + $cmd = new DatatypeDeclarationCommand(datatypeTypes); } - } - 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); - } + | sortSymbol[t,CHECK_DECLARED] { + 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] @@ -545,6 +550,13 @@ sygusCommand returns [CVC4::Command* cmd = NULL] sortSymbol[t,CHECK_DECLARED] { PARSER_STATE->mkSygusVar(name, t); $cmd = new EmptyCommand(); } + | /* declare-primed-var */ + DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + 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] @@ -595,7 +607,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] $cmd = new DefineFunctionCommand(name, func, terms, expr); } | /* synth-fun */ - SYNTH_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } + ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK { seq = new CommandSequence(); @@ -615,7 +627,11 @@ sygusCommand returns [CVC4::Command* cmd = NULL] terms.clear(); terms.push_back(bvl); } - sortSymbol[range,CHECK_DECLARED] + ( sortSymbol[range,CHECK_DECLARED] )? { + if( range.isNull() ){ + PARSER_STATE->parseError("Must supply return type for synth-fun."); + } + } ( LPAREN_TOK ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] @@ -626,25 +642,28 @@ sygusCommand returns [CVC4::Command* cmd = NULL] startIndex = datatypes.size(); } std::string dname = ss.str(); + sgts.push_back( std::vector< CVC4::SygusGTerm >() ); + sgts.back().push_back( CVC4::SygusGTerm() ); PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym); Type unres_t; if(!PARSER_STATE->isUnresolvedType(dname)) { // if not unresolved, must be undeclared + Debug("parser-sygus") << "Make unresolved type : " << dname << std::endl; PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); unres_t = PARSER_STATE->mkUnresolvedType(dname); }else{ + Debug("parser-sygus") << "Get sort : " << dname << std::endl; unres_t = PARSER_STATE->getSort(dname); } sygus_to_builtin[unres_t] = t; - sygus_dt_index = datatypes.size()-1; Debug("parser-sygus") << "--- Read sygus grammar " << name << " under function " << fun << "..." << std::endl; Debug("parser-sygus") << " type to resolve " << unres_t << std::endl; Debug("parser-sygus") << " builtin type " << t << std::endl; } // Note the official spec for NTDef is missing the ( parens ) // but they are necessary to parse SyGuS examples - LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, allow_const, unresolved_gterm_sym, - sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sygus_ret, -1]+ RPAREN_TOK + LPAREN_TOK ( sygusGTerm[ sgts.back().back(), fun] { sgts.back().push_back( CVC4::SygusGTerm() ); } )+ + RPAREN_TOK { sgts.back().pop_back(); } RPAREN_TOK )+ RPAREN_TOK { read_syntax = true; } @@ -652,10 +671,22 @@ sygusCommand returns [CVC4::Command* cmd = NULL] { if( !read_syntax ){ //create the default grammar - PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars ); + Debug("parser-sygus") << "Make default grammar..." << std::endl; + PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars, startIndex ); + //set start index + Debug("parser-sygus") << "Set start index " << startIndex << "..." << std::endl; + PARSER_STATE->setSygusStartIndex( fun, startIndex, datatypes, sorts, ops ); }else{ + Debug("parser-sygus") << "--- Process " << sgts.size() << " sygus gterms..." << std::endl; + for( unsigned i=0; i<sgts.size(); i++ ){ + for( unsigned j=0; j<sgts[i].size(); j++ ){ + Type sub_ret; + PARSER_STATE->processSygusGTerm( sgts[i][j], i, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, + sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); + } + } //swap index if necessary - Debug("parser-sygus") << "Making sygus datatypes..." << std::endl; + Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl; for( unsigned i=0; i<datatypes.size(); i++ ){ Debug("parser-sygus") << "..." << datatypes[i].getName() << " has builtin sort " << sorts[i] << std::endl; } @@ -667,25 +698,11 @@ sygusCommand returns [CVC4::Command* cmd = NULL] datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false ); PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin ); } - //only care about datatypes/sorts/ops past here - if( startIndex>0 ){ - // PARSER_STATE->swapSygusStart( startIndex, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - CVC4::Datatype tmp_dt = datatypes[0]; - Type tmp_sort = sorts[0]; - std::vector< Expr > tmp_ops; - tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); - datatypes[0] = datatypes[startIndex]; - sorts[0] = sorts[startIndex]; - ops[0].clear(); - ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() ); - datatypes[startIndex] = tmp_dt; - sorts[startIndex] = tmp_sort; - ops[startIndex].clear(); - ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() ); - } + PARSER_STATE->setSygusStartIndex( fun, startIndex, datatypes, sorts, ops ); } + //only care about datatypes/sorts/ops past here PARSER_STATE->popScope(); - Debug("parser-sygus") << "Make " << datatypes.size() << " mutual datatypes..." << std::endl; + Debug("parser-sygus") << "--- Make " << datatypes.size() << " mutual datatypes..." << std::endl; for( unsigned i=0; i<datatypes.size(); i++ ){ Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() << std::endl; } @@ -730,8 +747,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL] $cmd = seq; } | /* constraint */ - CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; + CONSTRAINT_TOK { + PARSER_STATE->checkThatLogicIsSet(); + Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; PARSER_STATE->defineSygusFuns(); Debug("parser-sygus") << "Sygus : read constraint..." << std::endl; } @@ -740,6 +758,62 @@ sygusCommand returns [CVC4::Command* cmd = NULL] PARSER_STATE->addSygusConstraint(expr); $cmd = new EmptyCommand(); } + | INV_CONSTRAINT_TOK { + PARSER_STATE->checkThatLogicIsSet(); + Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; + PARSER_STATE->defineSygusFuns(); + Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl; + } + ( symbol[name,CHECK_NONE,SYM_VARIABLE] { + if( !terms.empty() ){ + if( !PARSER_STATE->isDefinedFunction(name) ){ + std::stringstream ss; + ss << "Function " << name << " in inv-constraint is not defined."; + PARSER_STATE->parseError(ss.str()); + } + } + terms.push_back( PARSER_STATE->getVariable(name) ); + } + )+ { + if( terms.size()!=4 ){ + PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 arguments."); + } + //get primed variables + std::vector< Expr > primed[2]; + std::vector< Expr > all; + for( unsigned i=0; i<2; i++ ){ + PARSER_STATE->getSygusPrimedVars( primed[i], i==1 ); + all.insert( all.end(), primed[i].begin(), primed[i].end() ); + } + //make relevant terms + for( unsigned i=0; i<4; i++ ){ + Debug("parser-sygus") << "Make inv-constraint term #" << i << "..." << std::endl; + Expr op = terms[i]; + std::vector< Expr > children; + children.push_back( op ); + if( i==2 ){ + children.insert( children.end(), all.begin(), all.end() ); + }else{ + children.insert( children.end(), primed[0].begin(), primed[0].end() ); + } + terms[i] = EXPR_MANAGER->mkExpr(kind::APPLY,children); + if( i==0 ){ + std::vector< Expr > children2; + children2.push_back( op ); + children2.insert( children2.end(), primed[1].begin(), primed[1].end() ); + terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY,children2) ); + } + } + //make constraints + std::vector< Expr > conj; + conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1], terms[0] ) ); + conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, EXPR_MANAGER->mkExpr(kind::AND, terms[0], terms[2] ), terms[4] ) ); + conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3] ) ); + Expr ic = EXPR_MANAGER->mkExpr( kind::AND, conj ); + Debug("parser-sygus") << "...read invariant constraint " << ic << std::endl; + PARSER_STATE->addSygusConstraint(ic); + $cmd = new EmptyCommand(); + } | /* check-synth */ CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); } { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType()); @@ -775,102 +849,63 @@ sygusCommand returns [CVC4::Command* cmd = NULL] // fun is the name of the synth-fun this grammar term is for. // This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1) // This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. -sygusGTerm[int index, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::string& fun, - std::vector< std::vector<CVC4::Expr> >& ops, - std::vector< std::vector<std::string> >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool > allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::vector<CVC4::Expr>& sygus_vars, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, - CVC4::Type& ret, int gtermType] +sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] @declarations { - std::string name; + std::string name, name2; + bool readEnum = false; Kind k; Type t; CVC4::DatatypeConstructor* ctor = NULL; - unsigned count = 0; std::string sname; - // 0 builtin operator, 1 defined operator, 2 any constant, 3 any variable, 4 ignore, 5 let, -1 none - int sub_gtermType = -1; - Type sub_ret; - int sub_dt_index = -1; - std::string sub_dname; - Type null_type; - Expr null_expr; std::vector< Expr > let_vars; - int let_start_index = -1; - //int let_end_index = -1; - int let_end_arg_index = -1; - Expr let_func; + bool readingLet = false; } : LPAREN_TOK - ( builtinOp[k] - { Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; + //read operator + ( builtinOp[k]{ + Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; //since we enforce satisfaction completeness, immediately convert to total version if( k==CVC4::kind::BITVECTOR_UDIV ){ k = CVC4::kind::BITVECTOR_UDIV_TOTAL; } - name = kind::kindToString(k); - sub_gtermType = 0; - ops[index].push_back(EXPR_MANAGER->operatorOf(k)); - cnames[index].push_back( name ); + sgt.d_name = kind::kindToString(k); + sgt.d_gterm_type = SygusGTerm::gterm_op; + sgt.d_expr = EXPR_MANAGER->operatorOf(k); } | LET_TOK LPAREN_TOK { - name = std::string("let"); - sub_gtermType = 5; - ops[index].push_back( null_expr ); - cnames[index].push_back( name ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + sgt.d_name = std::string("let"); + sgt.d_gterm_type = SygusGTerm::gterm_let; PARSER_STATE->pushScope(true); - let_start_index = datatypes.size(); + readingLet = true; } ( LPAREN_TOK symbol[sname,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] { Expr v = PARSER_STATE->mkBoundVar(sname,t); - let_vars.push_back( v ); - std::stringstream ss; - ss << datatypes[index].getName() << "_" << ops[index].size() << "_lv_" << let_vars.size(); - sub_dname = ss.str(); - PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - sub_dt_index = datatypes.size()-1; - sub_ret = null_type; + sgt.d_let_vars.push_back( v ); + sgt.addChild(); } - sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,allow_const,unresolved_gterm_sym, - sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_ret,sub_gtermType] { - Debug("parser-sygus") << "Process argument #" << let_vars.size() << "..." << std::endl; - Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, - sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); - cargs[index].back().push_back(tt); - } - RPAREN_TOK )+ RPAREN_TOK { - //let_end_index = datatypes.size(); - let_end_arg_index = cargs[index].back().size(); - } + sygusGTerm[sgt.d_children.back(), fun] + RPAREN_TOK )+ RPAREN_TOK | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] - { sub_gtermType = 2; allow_const[index] = true;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; } + { sgt.d_gterm_type = SygusGTerm::gterm_constant; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; } | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sub_gtermType = 3; Debug("parser-sygus") << "Sygus grammar variable." << std::endl; } + { sgt.d_gterm_type = SygusGTerm::gterm_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar variable." << std::endl; } | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sub_gtermType = 4; Debug("parser-sygus") << "Sygus grammar local variable...ignore." << std::endl; } + { sgt.d_gterm_type = SygusGTerm::gterm_local_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar local variable...ignore." << std::endl; } | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sub_gtermType = 3; Debug("parser-sygus") << "Sygus grammar (input) variable." << std::endl; } - | symbol[name,CHECK_NONE,SYM_VARIABLE] - { + { sgt.d_gterm_type = SygusGTerm::gterm_input_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar (input) variable." << std::endl; } + | symbol[name,CHECK_NONE,SYM_VARIABLE] { bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); if(isBuiltinOperator) { + Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; k = PARSER_STATE->getOperatorKind(name); if( k==CVC4::kind::BITVECTOR_UDIV ){ k = CVC4::kind::BITVECTOR_UDIV_TOTAL; } - name = kind::kindToString(k); - ops[index].push_back(EXPR_MANAGER->operatorOf(k)); - cnames[index].push_back( name ); - sub_gtermType = 0; + sgt.d_name = kind::kindToString(k); + sgt.d_gterm_type = SygusGTerm::gterm_op; + sgt.d_expr = EXPR_MANAGER->operatorOf(k); }else{ // what is this sygus term trying to accomplish here, if the // symbol isn't yet declared?! probably the following line will @@ -880,148 +915,81 @@ sygusGTerm[int index, if( !PARSER_STATE->isDefinedFunction(name) ){ PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); } - ops[index].push_back( PARSER_STATE->getVariable(name) ); - cnames[index].push_back( name ); - sub_gtermType = 1; + sgt.d_name = name; + sgt.d_gterm_type = SygusGTerm::gterm_op; + sgt.d_expr = PARSER_STATE->getVariable(name) ; } } ) - { Debug("parser-sygus") << "Read arguments under " << name << ", gtermType = " << sub_gtermType << std::endl; - if( sub_gtermType!=5 ){ - cargs[index].push_back( std::vector< CVC4::Type >() ); - if( !ops[index].empty() ){ - Debug("parser-sygus") << "Operator " << ops[index].back() << std::endl; - } - } - //add datatype definition for argument - count++; - std::stringstream ss; - ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count; - sub_dname = ss.str(); - PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - sub_dt_index = datatypes.size()-1; - sub_ret = null_type; - } - ( sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,allow_const,unresolved_gterm_sym, - sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_ret,sub_gtermType] - { Debug("parser-sygus") << "Process argument #" << count << "..." << std::endl; - Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, - sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); - cargs[index].back().push_back(tt); - //add next datatype definition for argument - count++; - std::stringstream ss; - ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << count; - sub_dname = ss.str(); - PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - sub_dt_index = datatypes.size()-1; - sub_ret = null_type; - } )* RPAREN_TOK - { - //pop argument datatype definition - PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - //process constant/variable case - if( sub_gtermType==2 || sub_gtermType==3 || sub_gtermType==4 ){ - if( !cargs[index].back().empty() ){ - PARSER_STATE->parseError(std::string("Must provide single sort for constant/variable Sygus constructor.")); - } - cargs[index].pop_back(); - Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << ", gterm type=" << sub_gtermType << std::endl; - if( sub_gtermType==2 ){ - std::vector< Expr > consts; - PARSER_STATE->mkSygusConstantsForType( t, consts ); - Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl; - for( unsigned i=0; i<consts.size(); i++ ){ - std::stringstream ss; - ss << consts[i]; - Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; - ops[index].push_back( consts[i] ); - cnames[index].push_back( ss.str() ); - cargs[index].push_back( std::vector< CVC4::Type >() ); - } - }else if( sub_gtermType==3 ){ - Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl; - for( unsigned i=0; i<sygus_vars.size(); i++ ){ - if( sygus_vars[i].getType()==t ){ - std::stringstream ss; - ss << sygus_vars[i]; - Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; - ops[index].push_back( sygus_vars[i] ); - cnames[index].push_back( ss.str() ); - cargs[index].push_back( std::vector< CVC4::Type >() ); - } - } - }else if( sub_gtermType==4 ){ - //local variable, TODO? - } - }else if( sub_gtermType==5 ){ - if( (cargs[index].back().size()-let_end_arg_index)!=1 ){ - PARSER_STATE->parseError(std::string("Must provide single body for let Sygus constructor.")); - } - PARSER_STATE->processSygusLetConstructor( let_vars, index, let_start_index, datatypes, sorts, ops, cnames, cargs, - sygus_vars, sygus_to_builtin, sygus_to_builtin_expr ); - PARSER_STATE->popScope(); - //remove datatypes defining body - //while( (int)datatypes.size()>let_end_index ){ - // Debug("parser-sygus") << "Removing let body datatype " << datatypes[datatypes.size()-1].getName() << std::endl; - // PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - //} - //Debug("parser-sygus") << "Done let body datatypes" << std::endl; - }else{ - if( cargs[index].back().empty() ){ - PARSER_STATE->parseError(std::string("Must provide argument for Sygus constructor.")); - } - } + //read arguments + { Debug("parser-sygus") << "Read arguments under " << sgt.d_name << std::endl; + sgt.addChild(); + } + ( sygusGTerm[sgt.d_children.back(), fun] + { Debug("parser-sygus") << "Finished read argument #" << sgt.d_children.size() << "..." << std::endl; + sgt.addChild(); + } )* + RPAREN_TOK { + //pop last child index + sgt.d_children.pop_back(); + if( readingLet ){ + PARSER_STATE->popScope(); } + } | INTEGER_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl; - ops[index].push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL)))); - cnames[index].push_back( AntlrInput::tokenText($INTEGER_LITERAL) ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + sgt.d_expr = MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL))); + sgt.d_name = AntlrInput::tokenText($INTEGER_LITERAL); + sgt.d_gterm_type = SygusGTerm::gterm_op; } | HEX_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal " << AntlrInput::tokenText($HEX_LITERAL) << std::endl; assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - ops[index].push_back(MK_CONST( BitVector(hexString, 16) )); - cnames[index].push_back( AntlrInput::tokenText($HEX_LITERAL) ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + sgt.d_expr = MK_CONST( BitVector(hexString, 16) ); + sgt.d_name = AntlrInput::tokenText($HEX_LITERAL); + sgt.d_gterm_type = SygusGTerm::gterm_op; } | BINARY_LITERAL { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal " << AntlrInput::tokenText($BINARY_LITERAL) << std::endl; assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); - ops[index].push_back(MK_CONST( BitVector(binString, 2) )); - cnames[index].push_back( AntlrInput::tokenText($BINARY_LITERAL) ); - cargs[index].push_back( std::vector< CVC4::Type >() ); - } - | symbol[name,CHECK_NONE,SYM_VARIABLE] - { if( name[0] == '-' ){ //hack for unary minus - Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl; - ops[index].push_back(MK_CONST(Rational(name))); - cnames[index].push_back( name ); - cargs[index].push_back( std::vector< CVC4::Type >() ); - }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){ - Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl; - Expr bv = PARSER_STATE->getVariable(name); - ops[index].push_back(bv); - cnames[index].push_back( name ); - cargs[index].push_back( std::vector< CVC4::Type >() ); + sgt.d_expr = MK_CONST( BitVector(binString, 2) ); + sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL); + sgt.d_gterm_type = SygusGTerm::gterm_op; + } + | symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )? + { if( readEnum ){ + name = name + "__Enum__" + name2; + Debug("parser-sygus") << "Sygus grammar " << fun << " : Enum constant " << name << std::endl; + Expr c = PARSER_STATE->getVariable(name); + sgt.d_expr = MK_EXPR(kind::APPLY_CONSTRUCTOR,c); + sgt.d_name = name; + sgt.d_gterm_type = SygusGTerm::gterm_op; }else{ - //prepend function name to base sorts when reading an operator - std::stringstream ss; - ss << fun << "_" << name; - name = ss.str(); - if( PARSER_STATE->isDeclared(name, SYM_SORT) ){ - Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl; - ret = PARSER_STATE->getSort(name); + if( name[0] == '-' ){ //hack for unary minus + Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl; + sgt.d_expr = MK_CONST(Rational(name)); + sgt.d_name = name; + sgt.d_gterm_type = SygusGTerm::gterm_op; + }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){ + Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl; + sgt.d_expr = PARSER_STATE->getVariable(name); + sgt.d_name = name; + sgt.d_gterm_type = SygusGTerm::gterm_op; }else{ - if( gtermType==-1 ){ - Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl; - unresolved_gterm_sym[index].push_back(name); + //prepend function name to base sorts when reading an operator + std::stringstream ss; + ss << fun << "_" << name; + name = ss.str(); + if( PARSER_STATE->isDeclared(name, SYM_SORT) ){ + Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl; + sgt.d_type = PARSER_STATE->getSort(name); + sgt.d_gterm_type = SygusGTerm::gterm_nested_sort; }else{ - Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved " << name << std::endl; - ret = PARSER_STATE->mkUnresolvedType(name); + Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl; + sgt.d_gterm_type = SygusGTerm::gterm_unresolved; + sgt.d_name = name; } } } @@ -1612,7 +1580,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind = kind::NULL_EXPR; Expr op; - std::string name; + std::string name, name2; std::vector<Expr> args; std::vector< std::pair<std::string, Type> > sortedVarNames; Expr f, f2, f3, f4; @@ -1624,6 +1592,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Type type; std::string s; bool isBuiltinOperator = false; + bool readLetSort = false; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -1824,10 +1793,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(true); } - ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] (term[expr, f2] | sortSymbol[type,CHECK_DECLARED] { readLetSort = true; } term[expr, f2] ) RPAREN_TOK // this is a parallel let, so we have to save up all the contributions // of the let and define them only later on - { if(names.count(name) == 1) { + { if( readLetSort!=PARSER_STATE->sygus() ){ + PARSER_STATE->parseError("Bad syntax for let term."); + }else if(names.count(name) == 1) { std::stringstream ss; ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones"; PARSER_STATE->warning(ss.str()); @@ -1844,7 +1815,13 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] term[expr, f2] RPAREN_TOK { PARSER_STATE->popScope(); } - + | symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { + std::string cname = name + "__Enum__" + name2; + Debug("parser-sygus") << "Check for enum const " << cname << std::endl; + expr = PARSER_STATE->getVariable(cname); + //expr.getType().isConstructor() && ConstructorType(expr.getType()).getArity()==0; + expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr); + } /* a variable */ | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { if( PARSER_STATE->sygus() && name[0]=='-' && @@ -2502,8 +2479,11 @@ symbol[std::string& id, * use as symbols in SMT-LIB */ | SET_OPTIONS_TOK { id = "set-options"; } | DECLARE_VAR_TOK { id = "declare-var"; } + | DECLARE_PRIMED_VAR_TOK { id = "declare-primed-var"; } | SYNTH_FUN_TOK { id = "synth-fun"; } + | SYNTH_INV_TOK { id = "synth-inv"; } | CONSTRAINT_TOK { id = "constraint"; } + | INV_CONSTRAINT_TOK { id = "inv-constraint"; } | CHECK_SYNTH_TOK { id = "check-synth"; } ) { PARSER_STATE->checkDeclaration(id, check, type); } @@ -2653,10 +2633,15 @@ INCLUDE_TOK : 'include'; // SyGuS commands SYNTH_FUN_TOK : 'synth-fun'; +SYNTH_INV_TOK : 'synth-inv'; CHECK_SYNTH_TOK : 'check-synth'; DECLARE_VAR_TOK : 'declare-var'; +DECLARE_PRIMED_VAR_TOK : 'declare-primed-var'; CONSTRAINT_TOK : 'constraint'; +INV_CONSTRAINT_TOK : 'inv-constraint'; SET_OPTIONS_TOK : 'set-options'; +SYGUS_ENUM_TOK : { PARSER_STATE->sygus() }? 'Enum'; +SYGUS_ENUM_CONS_TOK : { PARSER_STATE->sygus() }? '::'; SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant'; SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable'; SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'InputVariable'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3420a3e7f..b8c4793d4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -81,6 +81,8 @@ void Smt2::addBitvectorOperators() { addOperator(kind::BITVECTOR_SLE, "bvsle"); addOperator(kind::BITVECTOR_SGT, "bvsgt"); addOperator(kind::BITVECTOR_SGE, "bvsge"); + addOperator(kind::BITVECTOR_REDOR, "bvredor"); + addOperator(kind::BITVECTOR_REDAND, "bvredand"); Parser::addOperator(kind::BITVECTOR_BITOF); Parser::addOperator(kind::BITVECTOR_EXTRACT); @@ -347,9 +349,6 @@ void Smt2::setLogic(std::string name) { ss << "Unknown SyGuS background logic `" << name << "'"; parseError(ss.str()); } - //TODO : add additional non-standard define-funs here - - } d_logicSet = true; @@ -499,27 +498,120 @@ void Smt2::includeFile(const std::string& filename) { } } -void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, - std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars ) { +Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) { + Expr e = mkBoundVar(name, type); + d_sygusVars.push_back(e); + d_sygusVarPrimed[e] = false; + if( isPrimed ){ + std::stringstream ss; + ss << name << "'"; + Expr ep = mkBoundVar(ss.str(), type); + d_sygusVars.push_back(ep); + d_sygusVarPrimed[ep] = true; + } + return e; +} +void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, + std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) { + startIndex = -1; Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl; std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; + std::vector< Type > types; + for( unsigned i=0; i<sygus_vars.size(); i++ ){ + Type t = sygus_vars[i].getType(); + if( !t.isBoolean() && std::find( types.begin(), types.end(), t )==types.end() ){ + types.push_back( t ); + } + } + + //name of boolean sort std::stringstream ssb; ssb << fun << "_Bool"; std::string dbname = ssb.str(); + Type unres_bt = mkUnresolvedType(ssb.str()); + + std::vector< Type > unres_types; + for( unsigned i=0; i<types.size(); i++ ){ + std::stringstream ss; + ss << fun << "_" << types[i]; + std::string dname = ss.str(); + datatypes.push_back(Datatype(dname)); + ops.push_back(std::vector<Expr>()); + std::vector<std::string> cnames; + std::vector<std::vector<CVC4::Type> > cargs; + std::vector<std::string> unresolved_gterm_sym; + //make unresolved type + Type unres_t = mkUnresolvedType(dname); + unres_types.push_back(unres_t); + //add variables + for( unsigned j=0; j<sygus_vars.size(); j++ ){ + if( sygus_vars[j].getType()==types[i] ){ + std::stringstream ss; + ss << sygus_vars[j]; + Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; + ops.back().push_back( sygus_vars[j] ); + cnames.push_back( ss.str() ); + cargs.push_back( std::vector< CVC4::Type >() ); + } + } + //add constants + std::vector< Expr > consts; + mkSygusConstantsForType( types[i], consts ); + for( unsigned j=0; j<consts.size(); j++ ){ + std::stringstream ss; + ss << consts[j]; + Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; + ops.back().push_back( consts[j] ); + cnames.push_back( ss.str() ); + cargs.push_back( std::vector< CVC4::Type >() ); + } + //ITE + CVC4::Kind k = kind::ITE; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back( kind::kindToString(k) ); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(unres_bt); + cargs.back().push_back(unres_t); + cargs.back().push_back(unres_t); + + if( types[i].isInteger() ){ + for( unsigned j=0; j<2; j++ ){ + CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(unres_t); + cargs.back().push_back(unres_t); + } + }else{ + std::stringstream sserr; + sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl; + warning(sserr.str()); + } + Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; + datatypes.back().setSygus( types[i], bvl, true, true ); + mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); + sorts.push_back( types[i] ); + //set start index if applicable + if( types[i]==range ){ + startIndex = i; + } + } - std::stringstream ss; - ss << fun << "_" << range; - std::string dname = ss.str(); - datatypes.push_back(Datatype(dname)); + //make Boolean type + Type btype = getExprManager()->booleanType(); + datatypes.push_back(Datatype(dbname)); ops.push_back(std::vector<Expr>()); std::vector<std::string> cnames; std::vector<std::vector<CVC4::Type> > cargs; std::vector<std::string> unresolved_gterm_sym; - //variables + //add variables for( unsigned i=0; i<sygus_vars.size(); i++ ){ - if( sygus_vars[i].getType()==range ){ + if( sygus_vars[i].getType().isBoolean() ){ std::stringstream ss; ss << sygus_vars[i]; Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; @@ -528,79 +620,60 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin cargs.push_back( std::vector< CVC4::Type >() ); } } - //constants - std::vector< Expr > consts; - mkSygusConstantsForType( range, consts ); - for( unsigned i=0; i<consts.size(); i++ ){ - std::stringstream ss; - ss << consts[i]; - Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; - ops.back().push_back( consts[i] ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - } - //ITE - CVC4::Kind k = kind::ITE; - Debug("parser-sygus") << "...add for " << k << std::endl; - ops.back().push_back(getExprManager()->operatorOf(k)); - cnames.push_back( kind::kindToString(k) ); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(mkUnresolvedType(ssb.str())); - cargs.back().push_back(mkUnresolvedType(ss.str())); - cargs.back().push_back(mkUnresolvedType(ss.str())); - - if( range.isInteger() ){ - for( unsigned i=0; i<2; i++ ){ - CVC4::Kind k = i==0 ? kind::PLUS : kind::MINUS; - Debug("parser-sygus") << "...add for " << k << std::endl; - ops.back().push_back(getExprManager()->operatorOf(k)); - cnames.push_back(kind::kindToString(k)); + //add constants if no variables and no connected types + if( ops.back().empty() && types.empty() ){ + std::vector< Expr > consts; + mkSygusConstantsForType( btype, consts ); + for( unsigned j=0; j<consts.size(); j++ ){ + std::stringstream ss; + ss << consts[j]; + Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; + ops.back().push_back( consts[j] ); + cnames.push_back( ss.str() ); cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(mkUnresolvedType(ss.str())); - cargs.back().push_back(mkUnresolvedType(ss.str())); } - }else{ - std::stringstream sserr; - sserr << "Don't know default Sygus grammar for type " << range << std::endl; - parseError(sserr.str()); } - Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; - datatypes.back().setSygus( range, bvl, true, true ); - mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); - sorts.push_back( range ); - - //Boolean type - datatypes.push_back(Datatype(dbname)); - ops.push_back(std::vector<Expr>()); - cnames.clear(); - cargs.clear(); - for( unsigned i=0; i<4; i++ ){ - CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : ( i==2 ? kind::OR : kind::EQUAL ) ); + //add operators + for( unsigned i=0; i<3; i++ ){ + CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR ); Debug("parser-sygus") << "...add for " << k << std::endl; ops.back().push_back(getExprManager()->operatorOf(k)); cnames.push_back(kind::kindToString(k)); cargs.push_back( std::vector< CVC4::Type >() ); if( k==kind::NOT ){ - cargs.back().push_back(mkUnresolvedType(ssb.str())); + cargs.back().push_back(unres_bt); }else if( k==kind::AND || k==kind::OR ){ - cargs.back().push_back(mkUnresolvedType(ssb.str())); - cargs.back().push_back(mkUnresolvedType(ssb.str())); - }else if( k==kind::EQUAL ){ - cargs.back().push_back(mkUnresolvedType(ss.str())); - cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(unres_bt); + cargs.back().push_back(unres_bt); } } - if( range.isInteger() ){ - CVC4::Kind k = kind::LEQ; + //add predicates for types + for( unsigned i=0; i<types.size(); i++ ){ + //add equality per type + CVC4::Kind k = kind::EQUAL; Debug("parser-sygus") << "...add for " << k << std::endl; ops.back().push_back(getExprManager()->operatorOf(k)); - cnames.push_back(kind::kindToString(k)); + std::stringstream ss; + ss << kind::kindToString(k) << "_" << types[i]; + cnames.push_back(ss.str()); cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(mkUnresolvedType(ss.str())); - cargs.back().push_back(mkUnresolvedType(ss.str())); + cargs.back().push_back(unres_types[i]); + cargs.back().push_back(unres_types[i]); + //type specific predicates + if( types[i].isInteger() ){ + CVC4::Kind k = kind::LEQ; + Debug("parser-sygus") << "...add for " << k << std::endl; + ops.back().push_back(getExprManager()->operatorOf(k)); + cnames.push_back(kind::kindToString(k)); + cargs.push_back( std::vector< CVC4::Type >() ); + cargs.back().push_back(unres_types[i]); + cargs.back().push_back(unres_types[i]); + } + } + if( range==btype ){ + startIndex = sorts.size(); } Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; - Type btype = getExprManager()->booleanType(); datatypes.back().setSygus( btype, bvl, true, true ); mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); sorts.push_back( btype ); @@ -618,10 +691,109 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& o ops.push_back( getExprManager()->mkConst(bval0) ); BitVector bval1(sz, (unsigned int)1); ops.push_back( getExprManager()->mkConst(bval1) ); + }else if( type.isBoolean() ){ + ops.push_back(getExprManager()->mkConst(true)); + ops.push_back(getExprManager()->mkConst(false)); } //TODO : others? } +// This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1) +// This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. +void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, + std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Type>& sorts, + std::vector< std::vector<CVC4::Expr> >& ops, + std::vector< std::vector<std::string> >& cnames, + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym, + std::vector<CVC4::Expr>& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, + CVC4::Type& ret, bool isNested ){ + if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){ + Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl; + //convert to UMINUS if one child of - + if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){ + sgt.d_expr = getExprManager()->operatorOf(kind::UMINUS); + } + ops[index].push_back( sgt.d_expr ); + cnames[index].push_back( sgt.d_name ); + cargs[index].push_back( std::vector< CVC4::Type >() ); + for( unsigned i=0; i<sgt.d_children.size(); i++ ){ + std::stringstream ss; + ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i; + std::string sub_dname = ss.str(); + //add datatype for child + Type null_type; + pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); + int sub_dt_index = datatypes.size()-1; + //process child + Type sub_ret; + processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, + sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true ); + //process the nested gterm (either pop the last datatype, or flatten the argument) + Type tt = processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, + sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); + cargs[index].back().push_back(tt); + } + //if let, must create operator + if( sgt.d_gterm_type==SygusGTerm::gterm_let ){ + processSygusLetConstructor( sgt.d_let_vars, index, datatypes, sorts, ops, cnames, cargs, + sygus_vars, sygus_to_builtin, sygus_to_builtin_expr ); + } + }else if( sgt.d_gterm_type==SygusGTerm::gterm_constant ){ + if( sgt.getNumChildren()!=0 ){ + parseError("Bad syntax for Sygus Constant."); + } + std::vector< Expr > consts; + mkSygusConstantsForType( sgt.d_type, consts ); + Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl; + for( unsigned i=0; i<consts.size(); i++ ){ + std::stringstream ss; + ss << consts[i]; + Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; + ops[index].push_back( consts[i] ); + cnames[index].push_back( ss.str() ); + cargs[index].push_back( std::vector< CVC4::Type >() ); + } + allow_const[index] = true; + }else if( sgt.d_gterm_type==SygusGTerm::gterm_variable || sgt.d_gterm_type==SygusGTerm::gterm_input_variable ){ + if( sgt.getNumChildren()!=0 ){ + parseError("Bad syntax for Sygus Variable."); + } + Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl; + for( unsigned i=0; i<sygus_vars.size(); i++ ){ + if( sygus_vars[i].getType()==sgt.d_type ){ + std::stringstream ss; + ss << sygus_vars[i]; + Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; + ops[index].push_back( sygus_vars[i] ); + cnames[index].push_back( ss.str() ); + cargs[index].push_back( std::vector< CVC4::Type >() ); + } + } + }else if( sgt.d_gterm_type==SygusGTerm::gterm_nested_sort ){ + ret = sgt.d_type; + }else if( sgt.d_gterm_type==SygusGTerm::gterm_unresolved ){ + if( isNested ){ + if( isUnresolvedType(sgt.d_name) ){ + ret = getSort(sgt.d_name); + }else{ + //nested, unresolved symbol...fail + std::stringstream ss; + ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl; + parseError(ss.str()); + } + }else{ + //will resolve when adding constructors + unresolved_gterm_sym[index].push_back(sgt.d_name); + } + }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){ + + } +} + bool Smt2::pushSygusDatatypeDef( Type t, std::string& dname, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, @@ -694,6 +866,15 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){ std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] ); if( it==sygus_to_builtin_expr.end() ){ + if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){ + std::stringstream ss; + ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl; + ss << "Builtin types are currently : " << std::endl; + for( std::map< CVC4::Type, CVC4::Type >::iterator itb = sygus_to_builtin.begin(); itb != sygus_to_builtin.end(); ++itb ){ + ss << " " << itb->first << " -> " << itb->second << std::endl; + } + parseError(ss.str()); + } Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl; std::stringstream ss; @@ -726,7 +907,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st } void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, - int index, int start_index, + int index, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, @@ -760,6 +941,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, Debug("parser-sygus") << " let var " << i << " : " << let_vars[i] << " " << let_vars[i].getType() << std::endl; let_define_args.push_back( let_vars[i] ); } + /* Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl; for( unsigned i=start_index; i<datatypes.size(); i++ ){ Debug("parser-sygus") << " datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl; @@ -772,6 +954,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, } } } + */ //last argument is the return, pop cargs[index][dindex].pop_back(); collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args ); @@ -819,6 +1002,29 @@ void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusAr } } +void Smt2::setSygusStartIndex( std::string& fun, int startIndex, + std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Type>& sorts, + std::vector< std::vector<CVC4::Expr> >& ops ) { + if( startIndex>0 ){ + CVC4::Datatype tmp_dt = datatypes[0]; + Type tmp_sort = sorts[0]; + std::vector< Expr > tmp_ops; + tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); + datatypes[0] = datatypes[startIndex]; + sorts[0] = sorts[startIndex]; + ops[0].clear(); + ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() ); + datatypes[startIndex] = tmp_dt; + sorts[startIndex] = tmp_sort; + ops[startIndex].clear(); + ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() ); + }else if( startIndex<0 ){ + std::stringstream ss; + ss << "warning: no symbol named Start for synth-fun " << fun << std::endl; + warning(ss.str()); + } +} void Smt2::defineSygusFuns() { // only define each one once @@ -877,6 +1083,7 @@ void Smt2::defineSygusFuns() { } Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv); Debug("parser-sygus") << "...made apply " << apply << std::endl; + Debug("parser-sygus") << "--> Define " << fun << " as " << lambda << " " << apply << std::endl; Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply); preemptCommand(cmd); @@ -1159,6 +1366,19 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec return assertion; } +const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) { + for( unsigned i=0; i<d_sygusVars.size(); i++ ){ + Expr v = d_sygusVars[i]; + std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v ); + if( it!=d_sygusVarPrimed.end() ){ + if( it->second==isPrimed ){ + vars.push_back( v ); + } + }else{ + //should never happen + } + } +} }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 275c8a83a..c88f7cd8f 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -35,7 +35,7 @@ namespace CVC4 { class SExpr; namespace parser { - + class Smt2 : public Parser { friend class ParserBuilder; @@ -64,6 +64,7 @@ private: std::stack< std::map<Expr, std::string> > d_unsatCoreNames; std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols; std::vector< std::pair<std::string, Expr> > d_sygusFuns; + std::map< Expr, bool > d_sygusVarPrimed; size_t d_nextSygusFun; protected: @@ -172,17 +173,25 @@ 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; - } + Expr mkSygusVar(const std::string& name, const Type& type, bool isPrimed = false); void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, - std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars ); + std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ); void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ); + void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, + std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Type>& sorts, + std::vector< std::vector<CVC4::Expr> >& ops, + std::vector< std::vector<std::string> >& cnames, + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym, + std::vector<CVC4::Expr>& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, + CVC4::Type& ret, bool isNested = false ); + static bool pushSygusDatatypeDef( Type t, std::string& dname, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, @@ -199,28 +208,11 @@ public: std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym ); - - Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector<CVC4::Expr> >& ops, - std::vector< std::vector<std::string> >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool >& allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, - std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); - - void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, - int index, int start_index, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector<CVC4::Expr> >& ops, - std::vector< std::vector<std::string> >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector<CVC4::Expr>& sygus_vars, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, - std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ); + void setSygusStartIndex( std::string& fun, int startIndex, + std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Type>& sorts, + std::vector< std::vector<CVC4::Expr> >& ops ); void addSygusFun(const std::string& fun, Expr eval) { d_sygusFuns.push_back(std::make_pair(fun, eval)); @@ -238,6 +230,8 @@ public: Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, Expr eval, const Datatype& dt, size_t i, size_t j ); + + void addSygusConstraint(Expr constraint) { d_sygusConstraints.push_back(constraint); @@ -254,6 +248,7 @@ public: const std::vector<Expr>& getSygusVars() { return d_sygusVars; } + const void getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ); const std::vector<Expr>& getSygusFunSymbols() { return d_sygusFunSymbols; @@ -322,6 +317,26 @@ private: void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ); + Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Type>& sorts, + std::vector< std::vector<CVC4::Expr> >& ops, + std::vector< std::vector<std::string> >& cnames, + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector< bool >& allow_const, + std::vector< std::vector< std::string > >& unresolved_gterm_sym, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, + std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ); + + void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, int index, + std::vector< CVC4::Datatype >& datatypes, + std::vector< CVC4::Type>& sorts, + std::vector< std::vector<CVC4::Expr> >& ops, + std::vector< std::vector<std::string> >& cnames, + std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, + std::vector<CVC4::Expr>& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, + std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ); + void addArithmeticOperators(); void addBitvectorOperators(); diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index c6a94f07a..a1baa98cb 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -26,7 +26,7 @@ // extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); namespace CVC4 { - + class Command; class Expr; class ExprManager; |