diff options
35 files changed, 1288 insertions, 452 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 16ac45de2..b0d97754d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -335,6 +335,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/fun_def_process.h \ theory/quantifiers/fun_def_process.cpp \ + theory/quantifiers/fun_def_engine.h \ + theory/quantifiers/fun_def_engine.cpp \ theory/quantifiers/options_handlers.h \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ 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; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5cc044272..822818c43 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -46,7 +46,7 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw(); static void printFpParameterizedOp(std::ostream& out, TNode n) throw(); static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw(); - + void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw() { if(dag != 0) { @@ -160,17 +160,22 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; case kind::FLOATINGPOINT_TYPE: out << "(_ FloatingPoint " - << n.getConst<FloatingPointSize>().exponent() << " " - << n.getConst<FloatingPointSize>().significand() - << ")"; + << n.getConst<FloatingPointSize>().exponent() << " " + << n.getConst<FloatingPointSize>().significand() + << ")"; break; case kind::CONST_BITVECTOR: { const BitVector& bv = n.getConst<BitVector>(); const Integer& x = bv.getValue(); unsigned n = bv.getSize(); - out << "(_ "; - out << "bv" << x <<" " << n; - out << ")"; + if(d_variant == sygus_variant ){ + out << "#b" << bv.toString(); + }else{ + out << "(_ "; + out << "bv" << x <<" " << n; + out << ")"; + } + // //out << "#b"; // while(n-- > 0) { @@ -189,7 +194,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case roundTowardNegative : out << "roundTowardNegative"; break; case roundTowardZero : out << "roundTowardZero"; break; default : - Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>()); + Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>()); } break; case kind::CONST_BOOLEAN: @@ -205,7 +210,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; case kind::CONST_RATIONAL: { const Rational& r = n.getConst<Rational>(); - toStreamRational(out, r, false); + if(d_variant == sygus_variant ){ + if(r < 0) { + out << "-" << -r; + }else{ + toStreamRational(out, r, false); + } + }else{ + toStreamRational(out, r, false); + } // Rational r = n.getConst<Rational>(); // if(r < 0) { // if(r.isIntegral()) { @@ -467,6 +480,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_SGT: out << "bvsgt "; break; case kind::BITVECTOR_SGE: out << "bvsge "; break; case kind::BITVECTOR_TO_NAT: out << "bv2nat "; break; + case kind::BITVECTOR_REDOR: out << "bvredor "; break; + case kind::BITVECTOR_REDAND: out << "bvredand "; break; case kind::BITVECTOR_EXTRACT: case kind::BITVECTOR_REPEAT: @@ -540,13 +555,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // Special case, in model output integer constants that should be // Real-sorted are wrapped in a type ascription. Handle that here. - // Note: This is Tim making a guess about Morgan's Code. - Assert(n[0].getKind() == kind::CONST_RATIONAL); - toStreamRational(out, n[0].getConst<Rational>(), true); + // Note: This is Tim making a guess about Morgan's Code. + Assert(n[0].getKind() == kind::CONST_RATIONAL); + toStreamRational(out, n[0].getConst<Rational>(), true); //toStream(out, n[0], -1, false); //out << ".0"; - + return; } out << "(as "; @@ -555,8 +570,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, return; } break; - case kind::APPLY_TESTER: case kind::APPLY_CONSTRUCTOR: + case kind::APPLY_TESTER: case kind::APPLY_SELECTOR: case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: @@ -625,7 +640,18 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if( n.getMetaKind() == kind::metakind::PARAMETERIZED && stillNeedToPrintParams ) { if(toDepth != 0) { - toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); + if( d_variant==sygus_variant && n.getKind()==kind::APPLY_CONSTRUCTOR ){ + std::stringstream ss; + toStream(ss, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); + std::string tmp = ss.str(); + size_t pos = 0; + if((pos = tmp.find("__Enum__", pos)) != std::string::npos){ + tmp.replace(pos, 8, "::"); + } + out << tmp; + }else{ + toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); + } } else { out << "(...)"; } @@ -719,6 +745,7 @@ static string smtKindString(Kind k) throw() { case kind::BITVECTOR_PLUS: return "bvadd"; case kind::BITVECTOR_SUB: return "bvsub"; case kind::BITVECTOR_NEG: return "bvneg"; + case kind::BITVECTOR_UDIV_TOTAL: case kind::BITVECTOR_UDIV: return "bvudiv"; case kind::BITVECTOR_UREM: return "bvurem"; case kind::BITVECTOR_SDIV: return "bvsdiv"; @@ -735,6 +762,8 @@ static string smtKindString(Kind k) throw() { case kind::BITVECTOR_SLE: return "bvsle"; case kind::BITVECTOR_SGT: return "bvsgt"; case kind::BITVECTOR_SGE: return "bvsge"; + case kind::BITVECTOR_REDOR: return "bvredor"; + case kind::BITVECTOR_REDAND: return "bvredand"; case kind::BITVECTOR_EXTRACT: return "extract"; case kind::BITVECTOR_REPEAT: return "repeat"; @@ -775,7 +804,7 @@ static string smtKindString(Kind k) throw() { case kind::FLOATINGPOINT_ISN: return "fp.isNormal"; case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal"; - case kind::FLOATINGPOINT_ISZ: return "fp.isZero"; + case kind::FLOATINGPOINT_ISZ: return "fp.isZero"; case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite"; case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN"; case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative"; @@ -1045,7 +1074,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) } } } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) { - const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c; + const DeclareFunctionCommand* dfc = (const DeclareFunctionCommand*)c; Node n = Node::fromExpr( dfc->getFunction() ); if(dfc->getPrintInModelSetByUser()) { if(!dfc->getPrintInModel()) { @@ -1071,9 +1100,9 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) out << "(define-fun " << n << " () " << n.getType() << " "; if(val.getType().isInteger() && n.getType().isReal() && !n.getType().isInteger()) { - //toStreamReal(out, val, true); - toStreamRational(out, val.getConst<Rational>(), true); - //out << val << ".0"; + //toStreamReal(out, val, true); + toStreamRational(out, val.getConst<Rational>(), true); + //out << val << ".0"; } else { out << val; } @@ -1228,16 +1257,16 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() static void toStreamRational(std::ostream& out, const Rational& r, bool decimal) throw() { bool neg = r.sgn() < 0; - + // TODO: // We are currently printing (- (/ 5 3)) // instead of (/ (- 5) 3) which is what is in the SMT-LIB value in the theory definition. // Before switching, I'll keep to what was there and send an email. // Tim: Apologies for the ifs on one line but in this case they are cleaner. - + if (neg) { out << "(- "; } - + if(r.isIntegral()) { if (neg) { out << (-r); diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index b4ecc1d3d..3cbc45cd1 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -70,6 +70,9 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vect operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)" operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)" +operator BITVECTOR_REDOR 1 "bit-vector redor" +operator BITVECTOR_REDAND 1 "bit-vector redand" + operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)" operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" @@ -171,6 +174,10 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule +typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule + + typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 3cc1c323c..768923ee6 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -49,6 +49,8 @@ enum RewriteRuleId { UgeEliminate, SgeEliminate, SgtEliminate, + RedorEliminate, + RedandEliminate, SubEliminate, SltEliminate, SleEliminate, @@ -188,6 +190,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case SgtEliminate: out << "SgtEliminate"; return out; case UgeEliminate: out << "UgeEliminate"; return out; case SgeEliminate: out << "SgeEliminate"; return out; + case RedorEliminate: out << "RedorEliminate"; return out; + case RedandEliminate: out << "RedandEliminate"; return out; case RepeatEliminate: out << "RepeatEliminate"; return out; case RotateLeftEliminate: out << "RotateLeftEliminate"; return out; case RotateRightEliminate:out << "RotateRightEliminate";return out; @@ -522,6 +526,8 @@ struct AllRewriteRules { RewriteRule<UltPlusOne> rule119; RewriteRule<ConcatToMult> rule120; RewriteRule<IsPowerOfTwo> rule121; + RewriteRule<RedorEliminate> rule122; + RewriteRule<RedandEliminate> rule123; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 0442c47d9..cd173a6dd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -479,6 +479,33 @@ Node RewriteRule<SignExtendEliminate>::apply(TNode node) { return utils::mkConcat(extension, node[0]); } +template<> +bool RewriteRule<RedorEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_REDOR); +} + +template<> +Node RewriteRule<RedorEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned size = utils::getSize(node[0]); + Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) ); + return result.negate(); +} + +template<> +bool RewriteRule<RedandEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_REDAND); +} + +template<> +Node RewriteRule<RedandEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned size = utils::getSize(node[0]); + Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) ); + return result; +} } } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 86f2c6760..f2adea411 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -553,6 +553,22 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite) return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteRedor(TNode node, bool prerewrite){ + Node resultNode = LinearRewriteStrategy + < RewriteRule<RedorEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){ + Node resultNode = LinearRewriteStrategy + < RewriteRule<RedandEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<BVToNatEliminate> @@ -651,6 +667,8 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend; d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight; d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft; + d_rewriteTable [ kind::BITVECTOR_REDOR ] = RewriteRedor; + d_rewriteTable [ kind::BITVECTOR_REDAND ] = RewriteRedand; d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat; d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 42bccb534..3f0fa8194 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -77,6 +77,8 @@ class TheoryBVRewriter { static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false); static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false); static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 81a2d9a27..fbb285fe0 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -112,6 +112,20 @@ public: } };/* class BitVectorPredicateTypeRule */ +class BitVectorUnaryPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TypeNode type = n[0].getType(check); + if (!type.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + } + return nodeManager->booleanType(); + } +};/* class BitVectorUnaryPredicateTypeRule */ + class BitVectorEagerAtomTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 6ebc9db92..a8b6887e5 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -385,6 +385,8 @@ inline bool isBVPredicate(TNode node) { node.getKind() == kind::BITVECTOR_SGE || node.getKind() == kind::BITVECTOR_ULE || node.getKind() == kind::BITVECTOR_SLE || + node.getKind() == kind::BITVECTOR_REDOR || + node.getKind() == kind::BITVECTOR_REDAND || ( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL || node[0].getKind() == kind::BITVECTOR_ULT || node[0].getKind() == kind::BITVECTOR_SLT || @@ -393,7 +395,9 @@ inline bool isBVPredicate(TNode node) { node[0].getKind() == kind::BITVECTOR_SGT || node[0].getKind() == kind::BITVECTOR_SGE || node[0].getKind() == kind::BITVECTOR_ULE || - node[0].getKind() == kind::BITVECTOR_SLE))) + node[0].getKind() == kind::BITVECTOR_SLE || + node[0].getKind() == kind::BITVECTOR_REDOR || + node[0].getKind() == kind::BITVECTOR_REDAND))) { return true; } diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index a8121b67d..3ab29f334 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -650,12 +650,22 @@ void SygusSymBreak::addTester( Node tst ) { std::map< Node, ProgSearch * >::iterator it = d_prog_search.find( a ); ProgSearch * ps; if( it==d_prog_search.end() ){ - ps = new ProgSearch( this, a, d_context ); + //check if sygus type + TypeNode tn = a.getType(); + Assert( DatatypesRewriter::isTypeDatatype( tn ) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isSygus() ){ + ps = new ProgSearch( this, a, d_context ); + }else{ + ps = NULL; + } d_prog_search[a] = ps; }else{ ps = it->second; } - ps->addTester( tst ); + if( ps ){ + ps->addTester( tst ); + } } } @@ -781,7 +791,7 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count, std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) { Assert( depth>=curr_depth ); - Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl; + Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << " " << prog.getType() << std::endl; NodeMap::const_iterator it = d_testers.find( prog ); if( it!=d_testers.end() ){ Node tst = (*it).second; @@ -823,7 +833,7 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node int tsize = d_tds->getSygusTermSize( prog ); if( itnp==d_normalized_to_orig[at].end() ){ d_normalized_to_orig[at][progr] = prog; - if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){ + if( progr.getKind()==SKOLEM && d_tds->getSygusTypeForVar( progr )==at ){ Trace("sygus-nf") << "* Sygus sym break : " << prog << " rewrites to variable " << progr << " of same type as self" << std::endl; d_redundant[at][prog] = true; red = true; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 5f3498f49..045407bf0 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -70,7 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ - if( d_guard.isNull() ){ + if( isAssigned() && d_guard.isNull() ){ d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); //specify guard behavior d_guard = qe->getValuation().ensureLiteral( d_guard ); @@ -137,6 +137,10 @@ bool CegConjecture::isSingleInvocation() { return d_ceg_si->isSingleInvocation(); } +bool CegConjecture::needsCheck() { + return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() ); +} + CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ d_conj = new CegConjecture( qe->getSatContext() ); d_last_inst_si = false; @@ -155,7 +159,7 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("cegqi-engine-debug") << std::endl; Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl; - if( d_conj->d_active && !d_conj->d_infeasible ){ + if( d_conj->needsCheck() ){ checkCegConjecture( d_conj ); } Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; @@ -213,29 +217,32 @@ void CegInstantiation::assertNode( Node n ) { } Node CegInstantiation::getNextDecisionRequest() { - d_conj->initializeGuard( d_quantEngine ); - bool value; - if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { - //if( d_conj->d_guard_split.isNull() ){ - // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); - // d_quantEngine->getOutputChannel().lemma( lem ); - //} - Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; - return d_conj->d_guard; - } //enforce fairness - if( d_conj->isAssigned() && d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ - Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); - if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { - if( !value ){ - d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); - lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); - Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + if( d_conj->isAssigned() ){ + d_conj->initializeGuard( d_quantEngine ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { + //if( d_conj->d_guard_split.isNull() ){ + // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); + // d_quantEngine->getOutputChannel().lemma( lem ); + //} + Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; + return d_conj->d_guard; + } + + if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ + Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { + if( !value ){ + d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); + lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + return lit; + } + }else{ + Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; return lit; } - }else{ - Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; - return lit; } } @@ -484,7 +491,8 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le } void CegInstantiation::printSynthSolution( std::ostream& out ) { - if( d_conj ){ + if( d_conj->isAssigned() ){ + Trace("cegqi-debug") << "Printing synth solution..." << std::endl; //if( !(Trace.isOn("cegqi-stats")) ){ // out << "Solution:" << std::endl; //} @@ -530,6 +538,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { out << ")" << std::endl; } } + }else{ + Assert( false ); } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 74e9b0aba..5f393626c 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -83,6 +83,8 @@ public: //for fairness CegqiFairMode getCegqiFairMode(); /** is single invocation */ bool isSingleInvocation(); + /** needs check */ + bool needsCheck(); }; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 0a434e4ca..b7bbf8a93 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -742,29 +742,38 @@ CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( d_sol = NULL; d_c_inst_match_trie = NULL; d_cinst = NULL; + d_has_ites = true; } Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { if( !d_single_inv.isNull() ) { - Assert( d_single_inv.getKind()==FORALL ); d_single_inv_var.clear(); d_single_inv_sk.clear(); - for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){ - std::stringstream ss; - ss << "k_" << d_single_inv[0][i]; - Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); - d_single_inv_var.push_back( d_single_inv[0][i] ); - d_single_inv_sk.push_back( k ); - d_single_inv_sk_index[k] = i; + Node inst; + if( d_single_inv.getKind()==FORALL ){ + for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){ + std::stringstream ss; + ss << "k_" << d_single_inv[0][i]; + Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); + d_single_inv_var.push_back( d_single_inv[0][i] ); + d_single_inv_sk.push_back( k ); + d_single_inv_sk_index[k] = i; + } + inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + }else{ + inst = d_single_inv; } - Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); inst = TermDb::simpleNegate( inst ); Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; //initialize the instantiator for this - CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); - d_cinst = new CegInstantiator( d_qe, cosi ); - d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + if( !d_single_inv_sk.empty() ){ + CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); + d_cinst = new CegInstantiator( d_qe, cosi ); + d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + }else{ + d_cinst = NULL; + } return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); }else{ @@ -790,6 +799,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { std::map< Node, std::map< Node, bool > > contains; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ progs.push_back( q[0][i] ); + //check whether all types have ITE + TypeNode tn = q[0][i].getType(); + d_qe->getTermDatabaseSygus()->registerSygusType( tn ); + if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ + if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ + d_has_ites = false; + } + } } //collect information about conjunctions bool singleInvocation = false; @@ -881,8 +898,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { //construct the single invocation version of the property Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl; //std::vector< Node > si_conj; - Assert( !pbvs.empty() ); - Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); + Node pbvl; + if( !pbvs.empty() ){ + pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); + } for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ //should hold since we prevent miniscoping Assert( d_single_inv.isNull() ); @@ -978,9 +997,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { if( singleInvocation ){ Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + if( pbvl.isNull() ){ + d_single_inv = bd; + }else{ + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + } Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; - if( options::eMatching.wasSetByUser() ){ + /* + if( options::eMatching() && options::eMatching.wasSetByUser() ){ Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); std::vector< Node > patTerms; std::vector< Node > exclude; @@ -992,6 +1016,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { } } } + */ } } } @@ -999,9 +1024,68 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { if( !singleInvocation ){ Trace("cegqi-si") << "Property is not single invocation." << std::endl; if( options::cegqiSingleInvAbort() ){ - Message() << "Property is not single invocation." << std::endl; + Notice() << "Property is not single invocation." << std::endl; exit( 0 ); } + }else{ + if( options::cegqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){ + Trace("cegqi-si-presolve") << "Check " << d_single_inv << std::endl; + //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing + std::vector< Node > vars; + std::map< Node, std::vector< Node > > teq; + for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){ + vars.push_back( d_single_inv[0][i] ); + teq[d_single_inv[0][i]].clear(); + } + collectPresolveEqTerms( d_single_inv[1], teq ); + std::vector< Node > terms; + std::vector< Node > conj; + getPresolveEqConjuncts( vars, terms, teq, d_single_inv, conj ); + + if( !conj.empty() ){ + Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); + lem = NodeManager::currentNM()->mkNode( OR, g, lem ); + d_qe->getOutputChannel().lemma( lem, false, true ); + } + } + } +} + +void CegConjectureSingleInv::collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) { + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] ); + if( it!=teq.end() ){ + Node nn = n[ i==0 ? 1 : 0 ]; + if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){ + it->second.push_back( nn ); + Trace("cegqi-si-presolve") << " - " << n[i] << " = " << nn << std::endl; + } + } + } + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectPresolveEqTerms( n[i], teq ); + } +} + +void CegConjectureSingleInv::getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, + std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) { + if( conj.size()<1000 ){ + if( terms.size()==f[0].getNumChildren() ){ + Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + conj.push_back( c ); + }else{ + unsigned i = terms.size(); + Node v = f[0][i]; + terms.push_back( Node::null() ); + for( unsigned j=0; j<teq[v].size(); j++ ){ + terms[i] = teq[v][j]; + getPresolveEqConjuncts( vars, terms, teq, f, conj ); + } + terms.pop_back(); + } } } @@ -1171,8 +1255,7 @@ bool CegConjectureSingleInv::addLemma( Node n ) { } void CegConjectureSingleInv::check( std::vector< Node >& lems ) { - if( !d_single_inv.isNull() ) { - Assert( d_cinst!=NULL ); + if( !d_single_inv.isNull() && d_cinst!=NULL ) { d_curr_lemmas.clear(); //check if there are delta lemmas d_cinst->getDeltaLemmas( lems ); @@ -1186,20 +1269,61 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) { } } -Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) { +Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ) { Assert( index<d_inst.size() ); Assert( i<d_inst[index].size() ); + unsigned uindex = indices[index]; if( index==d_inst.size()-1 ){ - return d_inst[index][i]; + return d_inst[uindex][i]; }else{ - Node cond = d_lemmas_produced[index]; + Node cond = d_lemmas_produced[uindex]; cond = TermDb::simpleNegate( cond ); - Node ite1 = d_inst[index][i]; - Node ite2 = constructSolution( i, index+1 ); + Node ite1 = d_inst[uindex][i]; + Node ite2 = constructSolution( indices, i, index+1 ); return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 ); } } +//TODO: use term size? +struct sortSiInstanceIndices { + CegConjectureSingleInv* d_ccsi; + int d_i; + bool operator() (unsigned i, unsigned j) { + if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){ + return true; + }else{ + return false; + } + } +}; + +/* +Node removeBooleanIte( Node n ){ + if( n.getKind()==ITE && n.getType().isBoolean() ){ + Node n1 = removeBooleanIte( n[1] ); + Node n2 = removeBooleanIte( n[2] ); + return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ), + NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) ); + }else{ + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nn = removeBooleanIte( n[i] ); + children.push_back( nn ); + childChanged = childChanged || nn!=n[i]; + } + if( childChanged ){ + if( n.hasOperator() ){ + children.insert( children.begin(), n.getOperator() ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } + } +} +*/ + Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){ Assert( d_sol!=NULL ); Assert( !d_lemmas_produced.empty() ); @@ -1225,7 +1349,21 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& d_sol->d_varList.push_back( varList[i-1] ); } //construct the solution - Node s = constructSolution( sol_index, 0 ); + Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl; + Assert( d_lemmas_produced.size()==d_inst.size() ); + std::vector< unsigned > indices; + for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){ + Assert( sol_index<d_inst[i].size() ); + indices.push_back( i ); + } + //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions) + // TODO : to minimize solution size, put the largest term last + sortSiInstanceIndices ssii; + ssii.d_ccsi = this; + ssii.d_i = sol_index; + std::sort( indices.begin(), indices.end(), ssii ); + Trace("csi-sol") << "Construct solution" << std::endl; + Node s = constructSolution( indices, sol_index, 0 ); s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() ); d_orig_solution = s; @@ -1242,6 +1380,10 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& if( reconstructed==1 ){ Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl; } + }else{ + ////remove boolean ITE (not allowed for sygus comp 2015) + //d_solution = removeBooleanIte( d_solution ); + //Trace("csi-sol") << "Solution (after remove boolean ITE) : " << d_solution << std::endl; } @@ -1278,4 +1420,13 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& } } +bool CegConjectureSingleInv::needsCheck() { + if( options::cegqiSingleInvMultiInstAbort() ){ + if( !hasITEs() ){ + return d_inst.empty(); + } + } + return true; +} + }
\ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index eb33c479e..f8e3879ac 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -111,8 +111,11 @@ private: bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ); bool doVariableElimination( Node v, std::vector< Node >& conjuncts ); bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status ); + //presolve + void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ); + void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); //constructing solution - Node constructSolution( unsigned i, unsigned index ); + Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ); private: //map from programs to variables in single invocation property std::map< Node, Node > d_single_inv_map; @@ -127,8 +130,6 @@ private: //list of skolems for each program std::vector< Node > d_single_inv_var; //lemmas produced - std::vector< Node > d_lemmas_produced; - std::vector< std::vector< Node > > d_inst; inst::InstMatchTrie d_inst_match_trie; inst::CDInstMatchTrie * d_c_inst_match_trie; // solution @@ -136,6 +137,11 @@ private: Node d_orig_solution; Node d_solution; Node d_sygus_solution; + bool d_has_ites; +public: + //lemmas produced + std::vector< Node > d_lemmas_produced; + std::vector< std::vector< Node > > d_inst; private: std::vector< Node > d_curr_lemmas; //add instantiation @@ -159,8 +165,12 @@ public: void check( std::vector< Node >& lems ); //get solution Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ); + // has ites + bool hasITEs() { return d_has_ites; } // is single invocation bool isSingleInvocation() { return !d_single_inv.isNull(); } + //needs check + bool needsCheck(); }; } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 0429abac9..413fd9ba2 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -86,8 +86,11 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) { Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl; t = pullITEs( t ); rem = pullITEs( rem ); + Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl; + Node prev = s; s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem ); - //Trace("csi-debug-sol") << "Now : " << s << std::endl; + Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl; + Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl; success = true; } }while( success ); @@ -99,11 +102,13 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) { bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) { Assert( n_ite.getKind()==ITE ); std::vector< Node > curr_conj; + std::vector< Node > orig_conj; bool isAnd; if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){ isAnd = n_ite[0].getKind()==AND; for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){ Node cond = n_ite[0][i]; + orig_conj.push_back( cond ); if( n_ite[0].getKind()==OR ){ cond = TermDb::simpleNegate( cond ); } @@ -112,12 +117,15 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve }else{ Node neg = n_ite[0].negate(); if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){ + //if negation of condition exists, use it isAnd = false; curr_conj.push_back( neg ); }else{ + //otherwise, use condition isAnd = true; curr_conj.push_back( n_ite[0] ); } + orig_conj.push_back( n_ite[0] ); } // take intersection with current conditions std::vector< Node > new_conj; @@ -162,13 +170,14 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve //make remainder : strip out conditions in conj Assert( !conj.empty() ); std::vector< Node > cond_c; + Assert( orig_conj.size()==curr_conj.size() ); for( unsigned i=0; i<curr_conj.size(); i++ ){ if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){ - cond_c.push_back( curr_conj[i] ); + cond_c.push_back( orig_conj[i] ); } } if( cond_c.empty() ){ - rem = isAnd ? tval : rem; + rem = tval; }else{ Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c ); rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval ); @@ -437,7 +446,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] ); } if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){ - Trace("csi-sol") << "Flatten based on " << ret[0] << "." << std::endl; + Trace("csi-simp-debug") << "Flatten based on " << ret[0] << "." << std::endl; ret = flattenITEs( ret, false ); } } @@ -510,7 +519,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st } if( !new_vars.empty() ){ if( !inc.empty() ){ - Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc ); + Node ret = inc.size()==1 ? inc[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc ); Trace("csi-simp") << "Base return is : " << ret << std::endl; // apply substitution ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() ); @@ -848,12 +857,10 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in } }while( !new_t.isNull() ); } + //get decompositions for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ Kind k = d_qe->getTermDatabaseSygus()->getArgKind( stn, i ); - if( k==AND || k==OR ){ - equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, min_t ) ); - equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, NodeManager::currentNM()->mkConst( k==AND ) ) ); - } + getEquivalentTerms( k, min_t, equiv ); } //assign ids to terms Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl; @@ -1046,4 +1053,62 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) { } } +void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) { + if( k==AND || k==OR ){ + equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) ); + equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) ); + } + //multiplication for integers + //TODO for bitvectors + Kind mk = ( k==PLUS || k==MINUS ) ? MULT : UNDEFINED_KIND; + if( mk!=UNDEFINED_KIND ){ + if( n.getKind()==mk && n[0].isConst() && n[0].getType().isInteger() ){ + bool success = true; + for( unsigned i=0; i<2; i++ ){ + Node eq; + if( k==PLUS || k==MINUS ){ + Node oth = NodeManager::currentNM()->mkConst( Rational(i==0 ? 1000 : -1000) ); + eq = i==0 ? NodeManager::currentNM()->mkNode( LEQ, n[0], oth ) : NodeManager::currentNM()->mkNode( GEQ, n[0], oth ); + } + if( !eq.isNull() ){ + eq = Rewriter::rewrite( eq ); + if( eq!=d_qe->getTermDatabase()->d_true ){ + success = false; + break; + } + } + } + if( success ){ + Node var = n[1]; + Node rem; + if( k==PLUS || k==MINUS ){ + int rem_coeff = (int)n[0].getConst<Rational>().getNumerator().getSignedInt(); + if( rem_coeff>0 && k==PLUS ){ + rem_coeff--; + }else if( rem_coeff<0 && k==MINUS ){ + rem_coeff++; + }else{ + success = false; + } + if( success ){ + rem = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(rem_coeff) ), var ); + rem = Rewriter::rewrite( rem ); + } + } + if( !rem.isNull() ){ + equiv.push_back( NodeManager::currentNM()->mkNode( k, rem, var ) ); + } + } + } + } + //negative constants + if( k==MINUS ){ + if( n.isConst() && n.getType().isInteger() && n.getConst<Rational>().getNumerator().strictlyNegative() ){ + Node nn = NodeManager::currentNM()->mkNode( UMINUS, n ); + nn = Rewriter::rewrite( nn ); + equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) ); + } + } +} + } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h index 6a4b6f90f..1d84986b4 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h @@ -78,6 +78,8 @@ private: bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status ); bool getPathToRoot( int id ); void setReconstructed( int id, Node n ); + //get equivalent terms to n with top symbol k + void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ); public: Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed ); public: diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp new file mode 100644 index 000000000..56214f540 --- /dev/null +++ b/src/theory/quantifiers/fun_def_engine.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file fun_def_process.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** 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 + ** + ** This class implements specialized techniques for (recursively) defined functions + **/ + +#include <vector> + +#include "theory/quantifiers/fun_def_engine.h" +#include "theory/rewriter.h" +#include "theory/quantifiers/term_database.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) { + +} + +/* whether this module needs to check this round */ +bool FunDefEngine::needsCheck( Theory::Effort e ) { + return e>=Theory::EFFORT_LAST_CALL; +} + +/* reset at a round */ +void FunDefEngine::reset_round( Theory::Effort e ){ + //TODO +} + +/* Call during quantifier engine's check */ +void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) { + //TODO +} + +/* Called for new quantifiers */ +void FunDefEngine::registerQuantifier( Node q ) { + //TODO +} + +/** called for everything that gets asserted */ +void FunDefEngine::assertNode( Node n ) { + //TODO +} diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h new file mode 100644 index 000000000..be73d51a9 --- /dev/null +++ b/src/theory/quantifiers/fun_def_engine.h @@ -0,0 +1,59 @@ +/********************* */ +/*! \file fun_def_engine.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** 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 Specialized techniques for (recursively) defined functions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H +#define __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +//module for handling (recursively) defined functions +class FunDefEngine : public QuantifiersModule { +private: + +public: + FunDefEngine( QuantifiersEngine * qe, context::Context* c ); + ~FunDefEngine(){} + + /* whether this module needs to check this round */ + bool needsCheck( Theory::Effort e ); + /* reset at a round */ + void reset_round( Theory::Effort e ); + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ); + /** called for everything that gets asserted */ + void assertNode( Node n ); + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "FunDefEngine"; } +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 391abe9eb..ab0526471 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -220,8 +220,12 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true include constants when reconstruct solutions for single invocation conjectures in original grammar +option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true + preregister ground instantiations when single invocation option cegqiSingleInvAbort --cegqi-si-abort bool :default false - abort if our synthesis conjecture is not single invocation + abort if synthesis conjecture is not single invocation +option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false + abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form @@ -259,5 +263,10 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false option quantAlphaEquiv --quant-alpha-equiv bool :default true infer alpha equivalence between quantified formulas + +### recursive function options + +#option funDefs --fun-defs bool :default false +# enable specialized techniques for recursive function definitions endmodule diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0198e014f..6a95e243d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -905,7 +905,21 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ std::vector< Node > activeArgs; - computeArgVec2( args, activeArgs, body, ipl ); + //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables + if( options::ceGuidedInst() && !ipl.isNull() ){ + for( unsigned i=0; i<ipl.getNumChildren(); i++ ){ + Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl; + if( ipl[i].getKind()==INST_ATTRIBUTE ){ + Node avar = ipl[i][0]; + if( avar.getAttribute(SygusAttribute()) ){ + activeArgs.insert( activeArgs.end(), args.begin(), args.end() ); + } + } + } + } + if( activeArgs.empty() ){ + computeArgVec2( args, activeArgs, body, ipl ); + } if( activeArgs.empty() ){ return body; }else{ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cc8ae4db0..fa0e211b3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -23,6 +23,7 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/fun_def_engine.h" //for sygus #include "theory/bv/theory_bv_utils.h" @@ -1431,6 +1432,7 @@ void TermDb::computeAttributes( Node q ) { exit( 0 ); } d_fun_defs[f] = true; + d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() ); } if( avar.getAttribute(SygusAttribute()) ){ //not necessarily nested existential @@ -1578,7 +1580,7 @@ TNode TermDbSygus::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count } } -TypeNode TermDbSygus::getSygusType( Node v ) { +TypeNode TermDbSygus::getSygusTypeForVar( Node v ) { Assert( d_fv_stype.find( v )!=d_fv_stype.end() ); return d_fv_stype[v]; } @@ -1740,7 +1742,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int Node n = NodeManager::currentNM()->mkNode( APPLY, children ); //must expand definitions Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) ); - Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl; + Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl; return ne; */ } @@ -2093,10 +2095,10 @@ void TermDbSygus::registerSygusType( TypeNode tn ){ d_register[tn] = TypeNode::null(); }else{ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl; + Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl; d_register[tn] = TypeNode::fromType( dt.getSygusType() ); if( d_register[tn].isNull() ){ - Trace("sygus-util") << "...not sygus." << std::endl; + Trace("sygus-db") << "...not sygus." << std::endl; }else{ //for constant reconstruction Kind ck = getComparisonKind( TypeNode::fromType( dt.getSygusType() ) ); @@ -2107,14 +2109,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ){ Expr sop = dt[i].getSygusOp(); Assert( !sop.isNull() ); Node n = Node::fromExpr( sop ); - Trace("sygus-util") << " Operator #" << i << " : " << sop; + Trace("sygus-db") << " Operator #" << i << " : " << sop; if( sop.getKind() == kind::BUILTIN ){ Kind sk = NodeManager::operatorToKind( n ); - Trace("sygus-util") << ", kind = " << sk; + Trace("sygus-db") << ", kind = " << sk; d_kinds[tn][sk] = i; d_arg_kind[tn][i] = sk; }else if( sop.isConst() ){ - Trace("sygus-util") << ", constant"; + Trace("sygus-db") << ", constant"; d_consts[tn][n] = i; d_arg_const[tn][i] = n; d_const_list[tn].push_back( n ); @@ -2127,7 +2129,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ){ } d_ops[tn][n] = i; d_arg_ops[tn][i] = n; - Trace("sygus-util") << std::endl; + Trace("sygus-db") << std::endl; } //sort the constant list if( !d_const_list[tn].empty() ){ @@ -2137,12 +2139,12 @@ void TermDbSygus::registerSygusType( TypeNode tn ){ sc.d_tds = this; std::sort( d_const_list[tn].begin(), d_const_list[tn].end(), sc ); } - Trace("sygus-util") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << " "; + Trace("sygus-db") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << " "; for( unsigned i=0; i<d_const_list[tn].size(); i++ ){ - Trace("sygus-util") << d_const_list[tn][i] << " "; + Trace("sygus-db") << d_const_list[tn][i] << " "; } - Trace("sygus-util") << std::endl; - Trace("sygus-util") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl; + Trace("sygus-db") << std::endl; + Trace("sygus-db") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl; } //register connected types for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ @@ -2159,6 +2161,11 @@ bool TermDbSygus::isRegistered( TypeNode tn ) { return d_register.find( tn )!=d_register.end(); } +TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) { + Assert( isRegistered( tn ) ); + return d_register[tn]; +} + int TermDbSygus::getKindArg( TypeNode tn, Kind k ) { Assert( isRegistered( tn ) ); std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn ); @@ -2348,6 +2355,7 @@ bool TermDbSygus::doCompare( Node a, Node b, Kind k ) { return com==d_true; } + void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){ size_t pos = 0; while((pos = str.find(oldStr, pos)) != std::string::npos){ @@ -2367,7 +2375,20 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > if( n.getNumChildren()>0 ){ out << "("; } - out << dt[cIndex].getSygusOp(); + Node op = dt[cIndex].getSygusOp(); + if( op.getType().isBitVector() && op.isConst() ){ + //print in the style it was given + Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl; + std::stringstream ss; + ss << dt[cIndex].getName(); + std::string str = ss.str(); + std::size_t found = str.find_last_of("_"); + Assert( found!=std::string::npos ); + std::string name = std::string( str.begin() + found +1, str.end() ); + out << name; + }else{ + out << op; + } if( n.getNumChildren()>0 ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ out << " "; @@ -2376,9 +2397,10 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > out << ")"; } }else{ + std::stringstream let_out; //print as let term if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ - out << "(let ("; + let_out << "(let ("; } std::vector< Node > subs_lvs; std::vector< Node > new_lvs; @@ -2392,22 +2414,25 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > //map free variables to proper terms if( i<dt[cIndex].getNumSygusLetInputArgs() ){ //it should be printed as a let argument - out << "("; - out << lv << " " << lv.getType() << " "; - printSygusTerm( out, n[i], lvs ); - out << ")"; + let_out << "("; + let_out << lv << " " << lv.getType() << " "; + printSygusTerm( let_out, n[i], lvs ); + let_out << ")"; } } if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ - out << ") "; + let_out << ") "; } //print the body Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() ); let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() ); new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() ); - std::stringstream body_out; - printSygusTerm( body_out, let_body, new_lvs ); - std::string body = body_out.str(); + printSygusTerm( let_out, let_body, new_lvs ); + if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ + let_out << ")"; + } + //do variable substitutions since ASSUMING : let_vars are interpreted literally and do not represent a class of variables + std::string lbody = let_out.str(); for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){ std::stringstream old_str; old_str << new_lvs[i]; @@ -2417,12 +2442,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > }else{ new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) ); } - doStrReplace( body, old_str.str().c_str(), new_str.str().c_str() ); - } - out << body; - if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ - out << ")"; + doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() ); } + out << lbody; } return; } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e61552713..1ffe0e29e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -433,7 +433,7 @@ public: bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 ); private: //information for sygus types - std::map< TypeNode, TypeNode > d_register; //stores sygus type + std::map< TypeNode, TypeNode > d_register; //stores sygus -> builtin type std::map< TypeNode, std::map< int, Kind > > d_arg_kind; std::map< TypeNode, std::map< Kind, int > > d_kinds; std::map< TypeNode, std::map< int, Node > > d_arg_const; @@ -455,6 +455,7 @@ private: public: TermDbSygus(); bool isRegistered( TypeNode tn ); + TypeNode sygusToBuiltinType( TypeNode tn ); int getKindArg( TypeNode tn, Kind k ); int getConstArg( TypeNode tn, Node n ); int getOpArg( TypeNode tn, Node n ); @@ -485,7 +486,7 @@ public: Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status ); /** get value */ Node getTypeMaxValue( TypeNode tn ); - TypeNode getSygusType( Node v ); + TypeNode getSygusTypeForVar( Node v ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); Node sygusToBuiltin( Node n, TypeNode tn ); Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 9f8f0d6cf..ccbbd5bd5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -37,6 +37,7 @@ #include "theory/uf/theory_uf.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/fun_def_engine.h" using namespace std; using namespace CVC4; @@ -169,6 +170,12 @@ d_lemmas_produced_c(u){ }else{ d_alpha_equiv = NULL; } + //if( options::funDefs() ){ + // d_fun_def_engine = new quantifiers::FunDefEngine( this, c ); + // d_modules.push_back( d_fun_def_engine ); + //}else{ + d_fun_def_engine = NULL; + //} if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; @@ -208,6 +215,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_sg_gen; delete d_ceg_inst; delete d_lte_part_inst; + delete d_fun_def_engine; for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) { delete (*i).second; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 3040a35c7..54f63bfe0 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -93,6 +93,7 @@ namespace quantifiers { class CegInstantiation; class LtePartialInst; class AlphaEquivalence; + class FunDefEngine; }/* CVC4::theory::quantifiers */ namespace inst { @@ -142,6 +143,8 @@ private: quantifiers::CegInstantiation * d_ceg_inst; /** lte partial instantiation */ quantifiers::LtePartialInst * d_lte_part_inst; + /** function definitions engine */ + quantifiers::FunDefEngine * d_fun_def_engine; public: //effort levels enum { QEFFORT_CONFLICT, @@ -228,6 +231,8 @@ public: //modules quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } /** local theory ext partial inst */ quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } + /** function definition engine */ + quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; } private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index dbef0494a..9d7155f78 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -38,7 +38,12 @@ TESTS = commutative.sy \ let-simp.sy \ tl-type.sy \ dup-op.sy \ - nflat-fwd.sy + nflat-fwd.sy \ + nflat-fwd-3.sy \ + enum-test.sy \ + no-syntax-test-bool.sy \ + inv-example.sy \ + uminus_one.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy new file mode 100644 index 000000000..52a72c07d --- /dev/null +++ b/test/regress/regress0/sygus/enum-test.sy @@ -0,0 +1,8 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(define-sort D (Enum (a b))) +(define-fun f ((x D)) Int (ite (= x D::a) 3 7)) +(synth-fun g () D ((Start D (D::a D::b)))) +(constraint (= (f g) 7)) +(check-synth)
\ No newline at end of file diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy new file mode 100644 index 000000000..dda8e0ed5 --- /dev/null +++ b/test/regress/regress0/sygus/inv-example.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-inv inv-f ((x Int) (y Int) (b Bool))) +(declare-primed-var x Int) +(declare-primed-var y Int) +(declare-primed-var b Bool) +(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3)))) +(define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12))))) +(define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x)) +(inv-constraint inv-f pre-f trans-f post-f) +(check-synth)
\ No newline at end of file diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy new file mode 100644 index 000000000..bd7c79e3e --- /dev/null +++ b/test/regress/regress0/sygus/nflat-fwd-3.sy @@ -0,0 +1,11 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si +(set-logic LIA) +(synth-fun f ((x Int)) Int + ((Start Int ((+ (+ Con Con) Con) x)) + (Con Int (0 1)))) + +(declare-var x Int) +(constraint (= (f x) 2)) +(check-synth) + diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy new file mode 100644 index 000000000..cc3855ad1 --- /dev/null +++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy @@ -0,0 +1,15 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si + +(set-logic LIA) + +(synth-fun f ((x Int) (y Int)) Bool) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (f x y) (>= (+ x y) 500))) + + +(check-synth) + diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy new file mode 100644 index 000000000..b020c0bee --- /dev/null +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -0,0 +1,7 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi +(set-logic LIA) +(synth-fun f ((x Int)) Int ((Start Int ((- 1))))) +(declare-var x Int) +(constraint (= (f x) (- 1))) +(check-synth)
\ No newline at end of file |