diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 453 |
1 files changed, 219 insertions, 234 deletions
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'; |