diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-07-27 20:19:35 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-07-27 20:19:35 -0500 |
commit | 8f4a7df9bd9cb59826e9769802d1345877a392ef (patch) | |
tree | e0797f3a9a4160c6199ecfd5deb7727e562a5e91 /src | |
parent | 9f10a95e26e9e790a19a6f9e68a658ec2ab6d304 (diff) | |
parent | c0079b3110a81f2ff993b7f86782266380dd102e (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src')
58 files changed, 2631 insertions, 1138 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 60f3bc7c2..b0d97754d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -311,8 +311,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/full_model_check.cpp \ theory/quantifiers/bounded_integers.h \ theory/quantifiers/bounded_integers.cpp \ - theory/quantifiers/first_order_reasoning.h \ - theory/quantifiers/first_order_reasoning.cpp \ + theory/quantifiers/alpha_equivalence.h \ + theory/quantifiers/alpha_equivalence.cpp \ theory/quantifiers/rewrite_engine.h \ theory/quantifiers/rewrite_engine.cpp \ theory/quantifiers/relevant_domain.h \ @@ -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/main/driver_unified.cpp b/src/main/driver_unified.cpp index 653eaca8f..b9e951f7b 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -213,9 +213,13 @@ int runCvc4(int argc, char* argv[], Options& opts) { } // if doing sygus, turn on CEGQI by default - if(opts[options::inputLanguage] == language::input::LANG_SYGUS && - !opts.wasSetByUser(options::ceGuidedInst)) { - opts.set(options::ceGuidedInst, true); + if(opts[options::inputLanguage] == language::input::LANG_SYGUS ){ + if( !opts.wasSetByUser(options::ceGuidedInst)) { + opts.set(options::ceGuidedInst, true); + } + if( !opts.wasSetByUser(options::dumpSynth)) { + opts.set(options::dumpSynth, true); + } } // Determine which messages to show based on smtcomp_mode and verbosity @@ -572,7 +576,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // make sure out and err streams are flushed too *opts[options::out] << flush; *opts[options::err] << flush; - + #ifdef CVC4_DEBUG if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) { _exit(returnValue); 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..9ee6d24b4 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::stringstream ss; - ss << fun << "_" << range; - std::string dname = ss.str(); - datatypes.push_back(Datatype(dname)); + 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; + } + } + + //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,132 @@ 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; + Kind oldKind; + Kind newKind = kind::UNDEFINED_KIND; + //convert to UMINUS if one child of MINUS + if( sgt.d_children.size()==1 && sgt.d_expr==getExprManager()->operatorOf(kind::MINUS) ){ + oldKind = kind::MINUS; + newKind = kind::UMINUS; + } + //convert to IFF if boolean EQUAL + if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){ + Type ctn = sgt.d_children[0].d_type; + std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn ); + if( it != sygus_to_builtin.end() && it->second.isBoolean() ){ + oldKind = kind::EQUAL; + newKind = kind::IFF; + } + } + if( newKind!=kind::UNDEFINED_KIND ){ + Expr newExpr = getExprManager()->operatorOf(newKind); + Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl; + sgt.d_expr = newExpr; + std::string oldName = kind::kindToString(oldKind); + std::string newName = kind::kindToString(newKind); + size_t pos = 0; + if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){ + sgt.d_name.replace(pos, oldName.length(), newName); + } + } + 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, @@ -656,7 +851,7 @@ bool Smt2::popSygusDatatypeDef( std::vector< CVC4::Datatype >& datatypes, unresolved_gterm_sym.pop_back(); return true; } - + Type Smt2::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, @@ -664,7 +859,7 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st 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::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) { Type t = sub_ret; Debug("parser-sygus") << "Argument is "; @@ -694,6 +889,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,13 +930,13 @@ 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, std::vector< std::vector<std::string> >& cnames, std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector<CVC4::Expr>& sygus_vars, + 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 ) { std::vector< CVC4::Expr > let_define_args; @@ -760,6 +964,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; @@ -771,29 +976,30 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars, Debug("parser-sygus") << " cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl; } } - } + } + */ //last argument is the return, pop cargs[index][dindex].pop_back(); - collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args ); - + collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args ); + Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl; std::vector<CVC4::Type> fsorts; for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){ Debug("parser-sygus") << " " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl; fsorts.push_back(let_define_args[i].getType()); } - + Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType()); std::stringstream ss; ss << datatypes[index].getName() << "_let"; Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) ); - + ops[index].pop_back(); ops[index].push_back( let_func ); cnames[index].pop_back(); cnames[index].push_back(ss.str()); - + //mark function as let constructor d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_define_args.begin(), let_define_args.end() ); d_sygus_let_func_to_body[let_func] = let_body; @@ -814,11 +1020,34 @@ void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusAr } }else{ for( unsigned i=0; i<e.getNumChildren(); i++ ){ - collectSygusLetArgs( e[i], sygusArgs, builtinArgs ); - } + collectSygusLetArgs( e[i], sygusArgs, builtinArgs ); + } } } +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 +1106,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); @@ -886,7 +1116,7 @@ void Smt2::defineSygusFuns() { void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, - std::vector<std::string>& unresolved_gterm_sym, + std::vector<std::string>& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) { Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; @@ -942,7 +1172,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, Debug("parser-sygus") << ": replace " << ops[i] << " " << ops[i].getKind() << " " << sk << std::endl; let_body = getExprManager()->mkExpr( sk, children ); Debug("parser-sygus") << ": new body of function is " << let_body << std::endl; - + Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType()); Debug("parser-sygus") << ": function type is " << ft << std::endl; std::stringstream ss; @@ -999,7 +1229,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, } } } - + } void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, @@ -1159,6 +1389,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 79cb18d92..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()) { @@ -288,10 +301,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(n.getKind() == kind::SORT_TYPE) { string name; + if(n.getNumChildren() != 0) { + out << '('; + } if(n.getAttribute(expr::VarNameAttr(), name)) { out << maybeQuoteSymbol(name); - return; } + if(n.getNumChildren() != 0) { + for(unsigned i = 0; i < n.getNumChildren(); ++i) { + out << ' '; + toStream(out, n[i], toDepth, types); + } + out << ')'; + } + return; } bool stillNeedToPrintParams = true; @@ -457,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: @@ -530,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 "; @@ -545,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: @@ -615,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 << "(...)"; } @@ -709,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"; @@ -725,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"; @@ -765,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"; @@ -1035,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()) { @@ -1061,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; } @@ -1218,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/smt/options b/src/smt/options index 077acc6e9..7c725e508 100644 --- a/src/smt/options +++ b/src/smt/options @@ -37,7 +37,7 @@ option dumpProofs --dump-proofs bool :default false :link --proof output proofs after every UNSAT/VALID response option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response -option dumpSynth --dump-synth bool :default false +option dumpSynth --dump-synth bool :read-write :default false output solution for synthesis conjectures after every UNSAT/VALID response option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1ab4ee62a..fa145813c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -82,10 +82,8 @@ #include "prop/options.h" #include "theory/arrays/options.h" #include "util/sort_inference.h" -#include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/fun_def_process.h" -#include "theory/quantifiers/first_order_reasoning.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/options.h" #include "theory/datatypes/options.h" @@ -773,7 +771,7 @@ void SmtEngine::finishInit() { // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString()); LogicInfo everything; everything.lock(); - Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, \"all-supported\" logic (below), as some internals might require the use of a logic more general than the input.") + Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.") << SetBenchmarkLogicCommand(everything.getLogicString()); } @@ -1426,6 +1424,12 @@ void SmtEngine::setDefaults() { } //cbqi options + // enable if pure arithmetic quantifiers + if( d_logic.isQuantified() && d_logic.isPure(THEORY_ARITH) ){ + if( !options::cbqi.wasSetByUser() && !options::cbqi2.wasSetByUser() ){ + options::cbqi2.set( true ); + } + } if( options::recurseCbqi() || options::cbqi2() ){ options::cbqi.set( true ); } @@ -1461,6 +1465,13 @@ void SmtEngine::setDefaults() { if( !options::dtForceAssignment.wasSetByUser() ){ options::dtForceAssignment.set( true ); } + //try to remove ITEs from quantified formulas + if( !options::iteDtTesterSplitQuant.wasSetByUser() ){ + options::iteDtTesterSplitQuant.set( true ); + } + if( !options::iteLiftQuant.wasSetByUser() ){ + options::iteLiftQuant.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL ); + } } if( options::intWfInduction() ){ if( !options::purifyTriggers.wasSetByUser() ){ @@ -1490,8 +1501,8 @@ void SmtEngine::setDefaults() { if( !options::preSkolemQuantNested.wasSetByUser() ){ options::preSkolemQuantNested.set( false ); } - } - + } + //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ @@ -3268,7 +3279,7 @@ void SmtEnginePrivate::processAssertions() { } } dumpAssertions("post-skolem-quant", d_assertions); - if( options::macrosQuant() ){ + if( options::macrosQuant() && !options::incrementalSolving() ){ //quantifiers macro expansion bool success; do{ @@ -3276,16 +3287,12 @@ void SmtEnginePrivate::processAssertions() { success = qm.simplify( d_assertions.ref(), true ); }while( success ); } + + //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF if( options::fmfFunWellDefined() ){ quantifiers::FunDefFmf fdf; fdf.simplify( d_assertions.ref() ); } - - Trace("fo-rsn-enable") << std::endl; - if( options::foPropQuant() ){ - quantifiers::FirstOrderPropagation fop; - fop.simplify( d_assertions.ref() ); - } } if( options::sortInference() ){ 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 d08c92dd9..3ab29f334 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -88,7 +88,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > Kind k = d_tds->getArgKind( tnnp, csIndex ); //size comparison for arguments (if necessary) Node sz_leq; - if( tn1==tnn && d_tds->isComm( k ) ){ + if( tn1==tnn && quantifiers::TermDb::isComm( k ) ){ sz_leq = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkNode( DT_SIZE, n ), NodeManager::currentNM()->mkNode( DT_SIZE, arg1 ) ); } std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i ); @@ -327,7 +327,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() ); Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() ); - bool isPComm = d_tds->isComm( parentKind ); + bool isPComm = quantifiers::TermDb::isComm( parentKind ); std::map< int, bool > larg_consider; for( unsigned i=0; i<dto.getNumConstructors(); i++ ){ if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){ @@ -411,7 +411,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt int pc = d_tds->getKindArg( tnp, parent ); if( k==parent ){ //check for associativity - if( d_tds->isAssoc( k ) ){ + if( quantifiers::TermDb::isAssoc( k ) ){ //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position int firstArg = getFirstArgOccurrence( pdt[pc], dt ); Assert( firstArg!=-1 ); @@ -511,8 +511,8 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt } } if( parent==MINUS || parent==BITVECTOR_SUB ){ - - + + } return true; } @@ -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; @@ -820,10 +830,10 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node Node progr = d_tds->getNormalized( at, prog ); Node rep_prog; std::map< Node, Node >::iterator itnp = d_normalized_to_orig[at].find( progr ); - int tsize = d_tds->getTermSize( prog ); + 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/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp new file mode 100755 index 000000000..e4dcccdff --- /dev/null +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -0,0 +1,105 @@ +/********************* */ +/*! \file alpha_equivalence.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-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Alpha equivalence checking + ** + **/ + +#include "theory/quantifiers/alpha_equivalence.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; + +struct sortTypeOrder { + TermDb* d_tdb; + bool operator() (TypeNode i, TypeNode j) { + return d_tdb->getIdForType( i )<d_tdb->getIdForType( j ); + } +}; + +bool AlphaEquivalenceNode::registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { + if( tt.size()==arg_index.size()+1 ){ + Node t = tt.back(); + Node op = t.hasOperator() ? t.getOperator() : t; + arg_index.push_back( 0 ); + Trace("aeq-debug") << op << " "; + return d_children[op][t.getNumChildren()].registerNode( qe, q, tt, arg_index ); + }else if( tt.empty() ){ + //we are finished + Trace("aeq-debug") << std::endl; + if( d_quant.isNull() ){ + d_quant = q; + return true; + }else{ + //lemma ( q <=> d_quant ) + Trace("alpha-eq") << "Alpha equivalent : " << std::endl; + Trace("alpha-eq") << " " << q << std::endl; + Trace("alpha-eq") << " " << d_quant << std::endl; + qe->getOutputChannel().lemma( q.iffNode( d_quant ) ); + return false; + } + }else{ + Node t = tt.back(); + int i = arg_index.back(); + if( i==(int)t.getNumChildren() ){ + tt.pop_back(); + arg_index.pop_back(); + }else{ + tt.push_back( t[i] ); + arg_index[arg_index.size()-1]++; + } + return registerNode( qe, q, tt, arg_index ); + } +} + +bool AlphaEquivalenceTypeNode::registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ + if( index==(int)typs.size() ){ + std::vector< Node > tt; + std::vector< int > arg_index; + tt.push_back( t ); + Trace("aeq-debug") << " : "; + return d_data.registerNode( qe, q, tt, arg_index ); + }else{ + TypeNode curr = typs[index]; + Assert( typ_count.find( curr )!=typ_count.end() ); + Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] "; + return d_children[curr][typ_count[curr]].registerNode( qe, q, t, typs, typ_count, index+1 ); + } +} + +bool AlphaEquivalence::registerQuantifier( Node q ) { + Assert( q.getKind()==FORALL ); + Trace("aeq") << "Alpha equivalence : register " << q << std::endl; + //construct canonical quantified formula + Node t = d_qe->getTermDatabase()->getCanonicalTerm( q[1], true ); + Trace("aeq") << " canonical form: " << t << std::endl; + //compute variable type counts + std::map< TypeNode, int > typ_count; + std::vector< TypeNode > typs; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + typ_count[tn]++; + if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){ + typs.push_back( tn ); + } + } + sortTypeOrder sto; + sto.d_tdb = d_qe->getTermDatabase(); + std::sort( typs.begin(), typs.end(), sto ); + Trace("aeq-debug") << " "; + bool ret = d_ae_typ_trie.registerNode( d_qe, q, t, typs, typ_count ); + Trace("aeq") << " ...result : " << ret << std::endl; + return ret; +} diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h new file mode 100755 index 000000000..fa2109ccc --- /dev/null +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file alpha_equivalence.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-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Alpha equivalence checking + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__ALPHA_EQUIVALENCE_H +#define __CVC4__ALPHA_EQUIVALENCE_H + + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class AlphaEquivalenceNode { +public: + std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children; + Node d_quant; + bool registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ); +}; + +class AlphaEquivalenceTypeNode { +public: + std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children; + AlphaEquivalenceNode d_data; + bool registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 ); +}; + +class AlphaEquivalence { +private: + QuantifiersEngine* d_qe; + //per # of variables per type + AlphaEquivalenceTypeNode d_ae_typ_trie; +public: + AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){} + ~AlphaEquivalence(){} + + bool registerQuantifier( Node q ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 5f3498f49..e10ba0fef 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -37,14 +37,25 @@ CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_in void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { Assert( d_quant.isNull() ); Assert( q.getKind()==FORALL ); + d_assert_quant = q; + //register with single invocation if applicable + if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){ + d_ceg_si->initialize( qe, q ); + if( q!=d_ceg_si->d_quant ){ + //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant ); + //may have rewritten quantified formula (for invariant synthesis) + q = d_ceg_si->d_quant; + } + } d_quant = q; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) ); } + Trace("cegqi") << "Base quantified fm is : " << q << std::endl; //construct base instantiation d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) ); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - if( qe->getTermDatabase()->isQAttrSygus( q ) ){ + if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj ); Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; //store the inner variables for each disjunct @@ -59,10 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } } d_syntax_guided = true; - if( options::cegqiSingleInv() ){ - d_ceg_si->initialize( qe, q ); - } - }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){ + }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ d_syntax_guided = false; }else{ Assert( false ); @@ -70,7 +78,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 +145,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 +167,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; @@ -207,35 +219,38 @@ void CegInstantiation::assertNode( Node n ) { //d_guard_assertions[lit] = pol; d_conj->d_infeasible = !pol; } - if( lit==d_conj->d_quant ){ + if( lit==d_conj->d_assert_quant ){ d_conj->d_active = true; } } 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; } } @@ -244,6 +259,7 @@ Node CegInstantiation::getNextDecisionRequest() { void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Node q = conj->d_quant; + Node aq = conj->d_assert_quant; Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl; Trace("cegqi-engine-debug") << " * Candidate program/output symbol : "; for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ @@ -256,7 +272,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( conj->d_ce_sk.empty() ){ Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; - if( getTermDatabase()->isQAttrSygus( q ) ){ + if( conj->d_syntax_guided ){ if( conj->d_ceg_si ){ std::vector< Node > lems; conj->d_ceg_si->check( lems ); @@ -296,7 +312,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { conj->d_ce_sk.push_back( std::vector< Node >() ); } std::vector< Node > ic; - ic.push_back( q.negate() ); + ic.push_back( aq.negate() ); std::vector< Node > d; collectDisjuncts( inst, d ); Assert( d.size()==conj->d_base_disj.size() ); @@ -327,7 +343,8 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-engine") << " ...find counterexample." << std::endl; } - }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ + }else{ + Assert( aq==q ); std::vector< Node > model_terms; if( getModelValues( conj, conj->d_candidates, model_terms ) ){ d_quantEngine->addInstantiation( q, model_terms, false ); @@ -484,16 +501,18 @@ 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; //} for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){ + Node prog = d_conj->d_quant[0][i]; std::stringstream ss; - ss << d_conj->d_quant[0][i]; + ss << prog; std::string f(ss.str()); f.erase(f.begin()); - TypeNode tn = d_conj->d_quant[0][i].getType(); + TypeNode tn = prog.getType(); Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); @@ -506,7 +525,34 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { }else{ if( !d_conj->d_candidate_inst[i].empty() ){ sol = d_conj->d_candidate_inst[i].back(); - status = 1; + //check if this was based on a template, if so, we must do reconstruction + if( d_conj->d_assert_quant!=d_conj->d_quant ){ + Trace("cegqi-inv") << "Sygus version of solution is : " << sol << ", type : " << sol.getType() << std::endl; + sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() ); + Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl; + std::vector< Node > subs; + Expr svl = dt.getSygusVarList(); + for( unsigned j=0; j<svl.getNumChildren(); j++ ){ + subs.push_back( Node::fromExpr( svl[j] ) ); + } + if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + Node pre = d_conj->d_ceg_si->d_trans_pre[prog]; + pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(), + subs.begin(), subs.end() ); + sol = NodeManager::currentNM()->mkNode( OR, sol, pre ); + }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){ + Node post = d_conj->d_ceg_si->d_trans_post[prog]; + post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(), + subs.begin(), subs.end() ); + sol = NodeManager::currentNM()->mkNode( AND, sol, post ); + } + Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; + sol = Rewriter::rewrite( sol ); + Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; + sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status ); + }else{ + status = 1; + } } } if( !(Trace.isOn("cegqi-stats")) ){ @@ -530,6 +576,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..af3a19d62 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -35,7 +35,9 @@ public: context::CDO< bool > d_active; /** is conjecture infeasible */ context::CDO< bool > d_infeasible; - /** quantified formula */ + /** quantified formula asserted */ + Node d_assert_quant; + /** quantified formula (after processing) */ Node d_quant; /** guard */ Node d_guard; @@ -83,6 +85,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 22ffcd278..ef2e3005e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -538,6 +538,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< d_qe->getOutputChannel().lemma( delta_lem ); } subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); + d_used_delta = true; } } //check if we have already added this instantiation @@ -706,7 +707,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { */ } -void CegInstantiator::check() { +bool CegInstantiator::check() { for( unsigned r=0; r<2; r++ ){ std::vector< Node > subs; @@ -716,10 +717,11 @@ void CegInstantiator::check() { std::vector< int > subs_typ; //try to add an instantiation if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){ - return; + return true; } } Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + return false; } @@ -740,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{ @@ -788,9 +799,18 @@ 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; + bool invExtractPrePost = false; if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){ singleInvocation = true; //try to phrase as single invocation property @@ -807,7 +827,6 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ if( it2->second.size()>1 ){ singleInvocation = false; - break; }else if( it2->second.size()==1 ){ Node prog = it2->first; Node inv = it2->second[0]; @@ -821,15 +840,26 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { single_invoke_args[prog][k-1].push_back( arg ); } } + if( inv.getType().isBoolean() ){ + //conjunct defines pre and/or post conditions + if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ + invExtractPrePost = true; + } + } } } } } } - if( singleInvocation ){ + if( singleInvocation || invExtractPrePost ){ + //no value in extracting pre/post if we are single invocation + if( singleInvocation ){ + invExtractPrePost = false; + } Trace("cegqi-si") << "Property is single invocation with : " << std::endl; std::vector< Node > pbvs; std::vector< Node > new_vars; + std::map< Node, std::vector< Node > > prog_vars; std::map< Node, std::vector< Node > > new_assumptions; for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){ Assert( !it->second.empty() ); @@ -849,12 +879,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Assert( !single_invoke_args[prog][k-1].empty() ); if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){ invc.push_back( single_invoke_args[prog][k-1][0] ); + prog_vars[prog].push_back( single_invoke_args[prog][k-1][0] ); }else{ //introduce fresh variable, assign all Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" ); new_vars.push_back( v ); invc.push_back( v ); d_single_inv_arg_sk.push_back( v ); + prog_vars[prog].push_back( v ); for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){ Node arg = single_invoke_args[prog][k-1][i]; @@ -878,13 +910,16 @@ 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() ); std::vector< Node > conjuncts; + std::vector< Node > conjuncts_si_progs; + std::vector< Node > conjuncts_si_invokes; for( unsigned i=0; i<it->second.size(); i++ ){ Node c = it->second[i]; std::vector< Node > disj; @@ -896,17 +931,32 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { if( itp!=prog_invoke.end() ){ std::vector< Node > terms; std::vector< Node > subs; + std::vector< Node > progs; for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ - if( !it2->second.empty() ){ + if( it2->second.size()==1 ){ Node prog = it2->first; Node inv = it2->second[0]; Assert( it2->second.size()==1 ); terms.push_back( inv ); subs.push_back( d_single_inv_map[prog] ); + progs.push_back( prog ); Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl; } } - cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + if( singleInvocation ){ + cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + }else{ + cr = c; + if( invExtractPrePost ){ + if( terms.size()==1 ){ + conjuncts_si_progs.push_back( progs[0] ); + conjuncts_si_invokes.push_back( terms[0] ); + }else if( terms.size()>1 ){ + //abort when mixing multiple invariants? TODO + invExtractPrePost = false; + } + } + } }else{ cr = c; } @@ -920,6 +970,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ); curr = TermDb::simpleNegate( curr ); Trace("cegqi-si") << " " << curr; + if( invExtractPrePost && conjuncts.size()==conjuncts_si_progs.size() ){ + conjuncts_si_progs.push_back( Node::null() ); + conjuncts_si_invokes.push_back( Node::null() ); + } conjuncts.push_back( curr ); if( !it->first.isNull() ){ Trace("cegqi-si-debug") << " under " << it->first; @@ -927,68 +981,162 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Trace("cegqi-si") << std::endl; } Assert( !conjuncts.empty() ); - //make the skolems for the existential - if( !it->first.isNull() ){ - std::vector< Node > vars; - std::vector< Node > sks; - for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ - std::stringstream ss; - ss << "a_" << it->first[j]; - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); - vars.push_back( it->first[j] ); - sks.push_back( v ); + //CASE 1 : rewrite based on a template for invariants + if( invExtractPrePost ){ + //for invariant synthesis + std::map< Node, bool > has_inv; + std::map< Node, std::vector< Node > > inv_pre_post[2]; + for( unsigned c=0; c<conjuncts.size(); c++ ){ + Node inv = conjuncts_si_invokes[c]; + Node prog = conjuncts_si_progs[c]; + Trace("cegqi-si-inv-debug") << "Conjunct #" << c << ": " << conjuncts[c] << std::endl; + if( !prog.isNull() ){ + Trace("cegqi-si-inv-debug") << "...has program " << prog << " invoked once: " << inv << std::endl; + std::vector< Node > curr_disj; + //find the polarity of the invocation : this determines pre vs. post + int pol = extractInvariantPolarity( conjuncts[c], inv, curr_disj, true ); + Trace("cegqi-si-inv-debug") << "...polarity is " << pol << std::endl; + if( ( pol==1 && !curr_disj.empty() ) || pol==0 ){ + //conjunct is part of pre/post condition : will add to template of invariant + Node nc = curr_disj.empty() ? NodeManager::currentNM()->mkConst( true ) : + ( curr_disj.size()==1 ? curr_disj[0] : NodeManager::currentNM()->mkNode( AND, curr_disj ) ); + nc = pol==0 ? nc : TermDb::simpleNegate( nc ); + Trace("cegqi-si-inv-debug") << " -> " << nc << " is " << ( pol==0 ? "pre" : "post" ) << "condition of invariant " << prog << "." << std::endl; + inv_pre_post[pol][prog].push_back( nc ); + has_inv[prog] = true; + } + } } - //substitute conjunctions - for( unsigned i=0; i<conjuncts.size(); i++ ){ - conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + Trace("cegqi-si-inv") << "Constructing invariant templates..." << std::endl; + //now, contruct the template for the invariant(s) + std::map< Node, Node > prog_templ; + for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){ + Node prog = iti->first; + Trace("cegqi-si-inv") << "...for " << prog << "..." << std::endl; + Trace("cegqi-si-inv") << " args : "; + for( unsigned j=0; j<prog_vars[prog].size(); j++ ){ + Node v = NodeManager::currentNM()->mkBoundVar( prog_vars[prog][j].getType() ); + d_prog_templ_vars[prog].push_back( v ); + Trace("cegqi-si-inv") << v << " "; + } + Trace("cegqi-si-inv") << std::endl; + Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) : + ( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) ); + d_trans_pre[prog] = pre.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) : + ( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) ); + d_trans_post[prog] = post.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Trace("cegqi-si-inv") << " precondition : " << d_trans_pre[prog] << std::endl; + Trace("cegqi-si-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + Node invariant = d_single_inv_app_map[prog]; + invariant = invariant.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Trace("cegqi-si-inv") << " invariant : " << invariant << std::endl; + //construct template + Node templ; + if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + //templ = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); + templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ); + }else{ + Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ); + //templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); + templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ); + } + Trace("cegqi-si-inv") << " template : " << templ << std::endl; + prog_templ[prog] = templ; } - d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); - //substitute single invocation applications - for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ - Node n = itam->second; - d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); + Trace("cegqi-si-inv") << " body : " << bd << std::endl; + bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars ); + Trace("cegqi-si-inv-debug") << " templ-subs body : " << bd << std::endl; + //make inner existential + std::vector< Node > new_var_bv; + for( unsigned j=0; j<new_vars.size(); j++ ){ + new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( new_vars[j].getType() ) ); } - } - //ensure that this is a ground property - for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ - Node n = itam->second; - //check if all variables are arguments of this - std::vector< Node > n_args; - for( unsigned i=1; i<n.getNumChildren(); i++ ){ - n_args.push_back( n[i] ); + bd = bd.substitute( new_vars.begin(), new_vars.end(), new_var_bv.begin(), new_var_bv.end() ); + for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){ + new_var_bv.push_back( q[1][0][0][j] ); } - for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){ - if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ - Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl; - //try to do variable elimination on d_single_inv_arg_sk[i] - if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){ - Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl; - d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 ); - i--; - }else{ - singleInvocation = false; - //exit( 57 ); + if( !new_var_bv.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv ); + bd = NodeManager::currentNM()->mkNode( FORALL, bvl, TermDb::simpleNegate( bd ) ).negate(); + } + //make outer universal + bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd ); + bd = Rewriter::rewrite( bd ); + Trace("cegqi-si-inv") << " rtempl-subs body : " << bd << std::endl; + d_quant = bd; + //CASE 2 : rewrite based on single invocation + }else{ + //make the skolems for the existential + if( !it->first.isNull() ){ + std::vector< Node > vars; + std::vector< Node > sks; + for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ + std::stringstream ss; + ss << "a_" << it->first[j]; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); + vars.push_back( it->first[j] ); + sks.push_back( v ); + } + //substitute conjunctions + for( unsigned i=0; i<conjuncts.size(); i++ ){ + conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + } + d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); + //substitute single invocation applications + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + } + } + //ensure that this is a ground property + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + //check if all variables are arguments of this + std::vector< Node > n_args; + for( unsigned i=1; i<n.getNumChildren(); i++ ){ + n_args.push_back( n[i] ); + } + for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){ + if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ + Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl; + //try to do variable elimination on d_single_inv_arg_sk[i] + if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){ + Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl; + d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 ); + i--; + }else{ + singleInvocation = false; + //exit( 57 ); + } + break; } - break; } } - } - if( singleInvocation ){ - Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); - Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; - if( options::eMatching.wasSetByUser() ){ - Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); - std::vector< Node > patTerms; - std::vector< Node > exclude; - inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude ); - if( !patTerms.empty() ){ - Trace("cegqi-si-em") << "Triggers : " << std::endl; - for( unsigned i=0; i<patTerms.size(); i++ ){ - Trace("cegqi-si-em") << " " << patTerms[i] << std::endl; + if( singleInvocation ){ + Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); + 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() && options::eMatching.wasSetByUser() ){ + Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); + std::vector< Node > patTerms; + std::vector< Node > exclude; + inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude ); + if( !patTerms.empty() ){ + Trace("cegqi-si-em") << "Triggers : " << std::endl; + for( unsigned i=0; i<patTerms.size(); i++ ){ + Trace("cegqi-si-em") << " " << patTerms[i] << std::endl; + } } } + */ } } } @@ -997,9 +1145,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(); + } } } @@ -1060,9 +1267,66 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, return false; } +int CegConjectureSingleInv::extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ) { + if( n.getKind()==NOT ){ + return extractInvariantPolarity( n[0], inv, curr_disj, !pol ); + }else if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){ + int curr_pol = -1; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + int eipc = extractInvariantPolarity( n[i], inv, curr_disj, pol ); + if( eipc!=-1 ){ + if( curr_pol==-1 ){ + curr_pol = eipc; + }else{ + return -1; + } + }else{ + curr_disj.push_back( pol ? n[i] : TermDb::simpleNegate( n[i] ) ); + } + } + return curr_pol; + }else if( n==inv ){ + return pol ? 1 : 0; + }else{ + return -1; + } +} + +Node CegConjectureSingleInv::substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ) { + if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){ + std::map< Node, Node >::iterator it = prog_templ.find( n[0] ); + if( it!=prog_templ.end() ){ + std::vector< Node > children; + for( unsigned i=1; i<n.getNumChildren(); i++ ){ + children.push_back( n[i] ); + } + std::map< Node, std::vector< Node > >::iterator itv = prog_templ_vars.find( n[0] ); + Assert( itv!=prog_templ_vars.end() ); + Assert( children.size()==itv->second.size() ); + Node newc = it->second.substitute( itv->second.begin(), itv->second.end(), children.begin(), children.end() ); + return newc; + } + } + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nn = substituteInvariantTemplates( n[i], prog_templ, prog_templ_vars ); + children.push_back( nn ); + childChanged = childChanged || ( nn!=n[i] ); + } + if( childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } +} + bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children, - std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, - std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { + std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, + std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){ @@ -1169,8 +1433,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 ); @@ -1184,20 +1447,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() ); @@ -1223,7 +1527,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; @@ -1231,7 +1549,12 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl; s = d_sol->simplifySolution( s, stn ); Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; + return reconstructToSyntax( s, stn, reconstructed ); +} + +Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ) { d_solution = s; + const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); //reconstruct the solution into sygus if necessary reconstructed = 0; @@ -1240,6 +1563,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; } @@ -1276,4 +1603,14 @@ 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 54f762720..f0d00b61c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -71,8 +71,9 @@ public: std::vector< Node > d_vars; //delta Node d_n_delta; + bool d_used_delta; //check : add instantiations based on valuation of d_vars - void check(); + bool check(); // get delta lemmas : on-demand force minimality of d_n_delta void getDeltaLemmas( std::vector< Node >& lems ); }; @@ -110,8 +111,14 @@ 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 ); + //for recognizing templates for invariant synthesis + int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ); + Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ); + //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; @@ -126,8 +133,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 @@ -135,6 +140,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 @@ -149,6 +159,10 @@ public: Node d_quant; // single invocation version of quant Node d_single_inv; + // transition relation version per program + std::map< Node, Node > d_trans_pre; + std::map< Node, Node > d_trans_post; + std::map< Node, std::vector< Node > > d_prog_templ_vars; public: //get the single invocation lemma Node getSingleInvLemma( Node guard ); @@ -158,8 +172,14 @@ public: void check( std::vector< Node >& lems ); //get solution Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ); + //reconstruct to syntax + Node reconstructToSyntax( Node s, 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 845e20795..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 ); @@ -309,7 +318,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ } Node sol0 = Rewriter::rewrite( sol ); Trace("csi-sol") << "now : " << sol0 << std::endl; - + Node curr_sol = sol0; Node prev_sol; do{ @@ -359,7 +368,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ curr_sol = sol4; } }while( curr_sol!=prev_sol ); - + return curr_sol; } @@ -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() ); @@ -726,7 +735,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in if( karg!=-1 ){ //collect the children of min_t std::vector< Node > tchildren; - if( min_t.getNumChildren()>dt[karg].getNumArgs() && d_qe->getTermDatabaseSygus()->isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ + if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermDb::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ tchildren.push_back( min_t[0] ); std::vector< Node > rem_children; for( unsigned i=1; i<min_t.getNumChildren(); i++ ){ @@ -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/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 4167c3ad9..da3c0cce0 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -281,61 +281,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { } Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { - Assert( !tn.isNull() ); - while( d_free_var[tn].size()<=i ){ - std::stringstream oss; - oss << tn; - std::string typ_name = oss.str(); - while( typ_name[0]=='(' ){ - typ_name.erase( typ_name.begin() ); - } - std::stringstream os; - os << typ_name[0] << i; - Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn ); - d_free_var_num[x] = d_free_var[tn].size(); - d_free_var[tn].push_back( x ); - } - return d_free_var[tn][i]; -} - - - -Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) { - if( n.getKind()==BOUND_VARIABLE ){ - std::map< TNode, TNode >::iterator it = subs.find( n ); - if( it==subs.end() ){ - TypeNode tn = n.getType(); - //allocate variable - unsigned vn = var_count[tn]; - var_count[tn]++; - subs[n] = getFreeVar( tn, vn ); - return subs[n]; - }else{ - return it->second; - } - }else{ - std::vector< Node > children; - if( n.getKind()!=EQUAL ){ - if( n.hasOperator() ){ - TNode op = n.getOperator(); - if( !d_tge.isRelevantFunc( op ) ){ - return Node::null(); - } - children.push_back( op ); - }else{ - return Node::null(); - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node cn = getCanonicalTerm( n[i], var_count, subs ); - if( cn.isNull() ){ - return Node::null(); - }else{ - children.push_back( cn ); - } - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } + return d_quantEngine->getTermDatabase()->getCanonicalFreeVar( tn, i ); } bool ConjectureGenerator::isHandledTerm( TNode n ){ @@ -555,11 +501,14 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { TNode nr = q[1][r==0 ? 1 : 0]; Node eq = nl.eqNode( nr ); if( r==1 || std::find( d_conjectures.begin(), d_conjectures.end(), q )==d_conjectures.end() ){ - //must make it canonical - std::map< TypeNode, unsigned > var_count; - std::map< TNode, TNode > subs; - Trace("sg-proc-debug") << "get canonical " << eq << std::endl; - eq = getCanonicalTerm( eq, var_count, subs ); + //check if it contains only relevant functions + if( d_tge.isRelevantTerm( eq ) ){ + //make it canonical + Trace("sg-proc-debug") << "get canonical " << eq << std::endl; + eq = d_quantEngine->getTermDatabase()->getCanonicalTerm( eq ); + }else{ + eq = Node::null(); + } } if( !eq.isNull() ){ if( r==0 ){ @@ -697,7 +646,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { typ_to_subs_index[it->first] = sum; sum += it->second; for( unsigned i=0; i<it->second; i++ ){ - gsubs_vars.push_back( getFreeVar( it->first, i ) ); + gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) ); } } } @@ -993,7 +942,7 @@ unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< }else{ //check for max/min TypeNode tn = pat.getType(); - unsigned vn = d_free_var_num[pat]; + unsigned vn = pat.getAttribute(InstVarNumAttribute()); std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn ); if( it!=mnvn.end() ){ if( vn<it->second ){ @@ -1768,15 +1717,18 @@ void TermGenEnv::collectSignatureInformation() { for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){ if( !getTermDatabase()->d_op_map[it->first].empty() ){ Node nn = getTermDatabase()->d_op_map[it->first][0]; + Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl; if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){ bool do_enum = true; //check if we have enumerated ground terms if( nn.getKind()==APPLY_UF ){ + Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl; if( !d_cg->hasEnumeratedUf( nn ) ){ do_enum = false; } } if( do_enum ){ + Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl; d_funcs.push_back( it->first ); for( unsigned i=0; i<nn.getNumChildren(); i++ ){ d_func_args[it->first].push_back( nn[i].getType() ); @@ -1789,6 +1741,7 @@ void TermGenEnv::collectSignatureInformation() { getTermDatabase()->computeUfEqcTerms( it->first ); } } + Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl; } } //shuffle functions @@ -2012,6 +1965,28 @@ bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){ bool TermGenEnv::isRelevantFunc( Node f ) { return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end(); } + +bool TermGenEnv::isRelevantTerm( Node t ) { + if( t.getKind()!=BOUND_VARIABLE ){ + if( t.getKind()!=EQUAL ){ + if( t.hasOperator() ){ + TNode op = t.getOperator(); + if( !isRelevantFunc( op ) ){ + return false; + } + }else{ + return false; + } + } + for( unsigned i=0; i<t.getNumChildren(); i++ ){ + if( !isRelevantTerm( t[i] ) ){ + return false; + } + } + } + return true; +} + TermDb * TermGenEnv::getTermDatabase() { return d_cg->getTermDatabase(); } diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 6f99777f4..3aa932296 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -171,6 +171,7 @@ public: bool considerCurrentTermCanon( unsigned tg_id ); void changeContext( bool add ); bool isRelevantFunc( Node f ); + bool isRelevantTerm( Node t ); //carry TermDb * getTermDatabase(); Node getGroundEqc( TNode r ); @@ -307,14 +308,8 @@ private: //information regarding the conjectures /** conjecture index */ TheoremIndex d_thm_index; private: //free variable list - //free variables - std::map< TypeNode, std::vector< Node > > d_free_var; - //map from free variable to FV# - std::map< TNode, unsigned > d_free_var_num; // get canonical free variable #i of type tn Node getFreeVar( TypeNode tn, unsigned i ); - // get canonical term, return null if it contains a term apart from handled signature - Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ); private: //information regarding the terms //relevant patterns (the LHS's) std::map< TypeNode, std::vector< Node > > d_rel_patterns; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 5cb8cf278..346631889 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -675,10 +675,11 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { //check if it is a constant introduced as a representative not existing in the model's equality engine if( !d_rep_set.hasRep( tn, v ) ){ if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){ - //see full_model_check.cpp line 366 v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ]; }else{ - Assert( false ); + //can happen for types not involved in quantified formulas + Trace("fmc-model-func") << "No type rep for " << tn << std::endl; + v = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); } Trace("fmc-model-func") << "No term, assign " << v << std::endl; } diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp deleted file mode 100644 index 23e18bb02..000000000 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ /dev/null @@ -1,175 +0,0 @@ -/********************* */ -/*! \file first_order_reasoning.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief first order reasoning module - ** - **/ - -#include <vector> - -#include "theory/quantifiers/first_order_reasoning.h" -#include "theory/rewriter.h" -#include "proof/proof_manager.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - - -void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){ - if( n.getKind()==FORALL ){ - collectLits( n[1], lits ); - }else if( n.getKind()==OR ){ - for(unsigned j=0; j<n.getNumChildren(); j++) { - collectLits(n[j], lits ); - } - }else{ - lits.push_back( n ); - } -} - -void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){ - for( unsigned i=0; i<assertions.size(); i++) { - Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl; - } - - //process all assertions - int num_processed; - int num_true = 0; - int num_rounds = 0; - do { - num_processed = 0; - for( unsigned i=0; i<assertions.size(); i++ ){ - if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){ - std::vector< Node > fo_lits; - collectLits( assertions[i], fo_lits ); - Node unitLit = process( assertions[i], fo_lits ); - if( !unitLit.isNull() ){ - Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl; - bool pol = unitLit.getKind()!=NOT; - unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit; - if( unitLit.getKind()==EQUAL ){ - - }else if( unitLit.getKind()==APPLY_UF ){ - //make sure all are unique vars; - bool success = true; - std::vector< Node > unique_vars; - for( unsigned j=0; j<unitLit.getNumChildren(); j++) { - if( unitLit[j].getKind()==BOUND_VARIABLE ){ - if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){ - unique_vars.push_back( unitLit[j] ); - }else{ - success = false; - break; - } - }else{ - success = false; - break; - } - } - if( success ){ - d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol); - Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl; - Trace("fo-rsn") << " from : " << assertions[i] << std::endl; - d_assertion_true[assertions[i]] = true; - num_processed++; - } - }else if( unitLit.getKind()==VARIABLE ){ - d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol); - Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl; - Trace("fo-rsn") << " from : " << assertions[i] << std::endl; - d_assertion_true[assertions[i]] = true; - num_processed++; - } - } - if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){ - num_true++; - } - } - } - num_rounds++; - }while( num_processed>0 ); - Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl; - for( unsigned i=0; i<assertions.size(); i++ ){ - Node curr = simplify( assertions[i] ); - if( curr!=assertions[i] ){ - curr = Rewriter::rewrite( curr ); - PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); - assertions[i] = curr; - } - } -} - -Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) { - int index = -1; - for( unsigned i=0; i<lits.size(); i++) { - bool pol = lits[i].getKind()!=NOT; - Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i]; - Node litDef; - if( n.getKind()==APPLY_UF ){ - if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ - litDef = d_const_def[n.getOperator()]; - } - }else if( n.getKind()==VARIABLE ){ - if( d_const_def.find(n)!=d_const_def.end() ){ - litDef = d_const_def[n]; - } - } - if( !litDef.isNull() ){ - Node poln = NodeManager::currentNM()->mkConst( pol ); - if( litDef==poln ){ - Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl; - d_assertion_true[a] = true; - return Node::null(); - } - } - if( litDef.isNull() ){ - if( index==-1 ){ - //store undefined index - index = i; - }else{ - //two undefined, return null - return Node::null(); - } - } - } - if( index!=-1 ){ - return lits[index]; - }else{ - return Node::null(); - } -} - -Node FirstOrderPropagation::simplify( Node n ) { - if( n.getKind()==VARIABLE ){ - if( d_const_def.find(n)!=d_const_def.end() ){ - return d_const_def[n]; - } - }else if( n.getKind()==APPLY_UF ){ - if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ - return d_const_def[n.getOperator()]; - } - } - if( n.getNumChildren()==0 ){ - return n; - }else{ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - for(unsigned i=0; i<n.getNumChildren(); i++) { - children.push_back( simplify(n[i]) ); - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } -} diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h deleted file mode 100644 index 100cf34b6..000000000 --- a/src/theory/quantifiers/first_order_reasoning.h +++ /dev/null @@ -1,49 +0,0 @@ -/********************* */ -/*! \file first_order_reasoning.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Pre-process step for first-order reasoning - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__FIRST_ORDER_REASONING_H -#define __CVC4__FIRST_ORDER_REASONING_H - -#include <iostream> -#include <string> -#include <vector> -#include <map> -#include "expr/node.h" -#include "expr/type_node.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class FirstOrderPropagation { -private: - std::map< Node, Node > d_const_def; - std::map< Node, bool > d_assertion_true; - Node process(Node a, std::vector< Node > & lits); - void collectLits( Node n, std::vector<Node> & lits ); - Node simplify( Node n ); -public: - FirstOrderPropagation(){} - ~FirstOrderPropagation(){} - - void simplify( std::vector< Node >& assertions ); -}; - -} -} -} - -#endif 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/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 941eaf89b..f7dc709d9 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -463,13 +463,17 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE s = Rewriter::rewrite( s ); Trace("var-trigger-matching") << "...got " << s << std::endl; d_eq_class = Node::null(); - d_rm_prev = m.get( d_var_num[0] ).isNull(); - if( !m.set( qe, d_var_num[0], s ) ){ - return false; - }else{ - if( continueNextMatch( f, m, qe ) ){ - return true; + if( s.getType().isSubtypeOf( d_var.getType() ) ){ + d_rm_prev = m.get( d_var_num[0] ).isNull(); + if( !m.set( qe, d_var_num[0], s ) ){ + return false; + }else{ + if( continueNextMatch( f, m, qe ) ){ + return true; + } } + }else{ + Trace("var-trigger-matching") << "Violates type requirement." << std::endl; } } if( d_rm_prev ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index cbf0dbbd9..dab32af71 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -126,9 +126,9 @@ void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder< } int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ - if( e<2 ){ + if( e<1 ){ return STATUS_UNFINISHED; - }else if( e==2 ){ + }else if( e==1 ){ if( d_quantActive.find( f )!=d_quantActive.end() ){ //the point instantiation InstMatch m_point( f ); @@ -369,12 +369,13 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( q void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { d_check_delta_lemma = true; + d_check_delta_lemma_lc = true; } int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { - if( e<2 ){ + if( e<1 ){ return STATUS_UNFINISHED; - }else if( e==2 ){ + }else if( e==1 ){ CegInstantiator * cinst; std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f ); if( it==d_cinst.end() ){ @@ -383,6 +384,9 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" ); Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); d_quantEngine->getOutputChannel().lemma( delta_lem ); + d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); } cinst->d_n_delta = d_n_delta; for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ @@ -412,8 +416,19 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { } Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; d_curr_quant = f; - cinst->check(); + bool addedLemma = cinst->check(); + d_used_delta = d_used_delta || cinst->d_used_delta; d_curr_quant = Node::null(); + return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; + }else if( e==2 ){ + if( d_check_delta_lemma_lc && d_used_delta ){ + d_check_delta_lemma_lc = false; + d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub ); + d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub ); + Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } } return STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 586cd492c..d59690c84 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -100,8 +100,11 @@ private: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; Node d_n_delta; + Node d_n_delta_ub; Node d_curr_quant; bool d_check_delta_lemma; + bool d_check_delta_lemma_lc; + bool d_used_delta; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 81771c374..8958034df 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -467,12 +467,13 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ }else{ //first, try from relevant domain RelevantDomain * rd = d_quantEngine->getRelevantDomain(); - for( unsigned r=0; r<2; r++ ){ - if( rd || r==1 ){ + unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; + for( unsigned r=rstart; r<2; r++ ){ + if( rd || r>0 ){ if( r==0 ){ Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; }else{ - Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; + Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; } rd->compute(); unsigned final_max_i = 0; @@ -550,6 +551,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ } } if( r==0 ){ + //complete guess if( d_guessed.find( f )==d_guessed.end() ){ Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; d_guessed[f] = true; @@ -561,6 +563,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ } } } + //term enumerator? } return STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 4fbf298f4..631216507 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -66,11 +66,10 @@ void InstantiationEngine::finishInit(){ //counterexample-based quantifier instantiation if( options::cbqi() ){ - if( !options::cbqi2() || options::cbqi.wasSetByUser() ){ + if( !options::cbqi2() ){ d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ); d_instStrategies.push_back( d_i_splx ); - } - if( options::cbqi2() ){ + }else{ d_i_cegqi = new InstStrategyCegqi( d_quantEngine ); d_instStrategies.push_back( d_i_cegqi ); } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 53f55e70b..e297e138c 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -176,7 +176,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { } //if applicable, find exceptions to model via inst-gen - if( optInstGen() ){ + if( options::fmfInstGen() ){ d_didInstGen = true; d_instGenMatches = 0; d_numQuantSat = 0; @@ -201,7 +201,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { }else{ d_numQuantNoSelForm++; } - if( optOneQuantPerRoundInstGen() && lems>0 ){ + if( options::fmfInstGenOneQuantPerRound() && lems>0 ){ break; } }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ @@ -341,14 +341,6 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){ return false; } -bool QModelBuilderIG::optInstGen(){ - return options::fmfInstGen(); -} - -bool QModelBuilderIG::optOneQuantPerRoundInstGen(){ - return options::fmfInstGenOneQuantPerRound(); -} - QModelBuilderIG::Statistics::Statistics(): d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0), diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index d9ed3f092..8e84f15e2 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -123,10 +123,6 @@ public: QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); virtual ~QModelBuilderIG() throw() {} public: - //whether to add inst-gen lemmas - virtual bool optInstGen(); - //whether to only consider only quantifier per round of inst-gen - virtual bool optOneQuantPerRoundInstGen(); /** statistics class */ class Statistics { public: diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index ce780a29b..2ad8be3a1 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -157,15 +157,19 @@ int ModelEngine::checkModel(){ if( it->first.isSort() ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; if( Trace.isOn("model-engine-debug") ){ - Trace("model-engine-debug") << " "; - Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Reps : "; + for( size_t i=0; i<it->second.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; + } + Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Term reps : "; for( size_t i=0; i<it->second.size(); i++ ){ - //Trace("model-engine-debug") << it->second[i] << " "; Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; - Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; } } } @@ -200,6 +204,7 @@ int ModelEngine::checkModel(){ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); bool isAx = getTermDatabase()->isQAttrAxiom( f ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){ exhaustiveInstantiate( f, e ); @@ -214,7 +219,7 @@ int ModelEngine::checkModel(){ break; } }else{ - Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl; + Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } } } @@ -240,43 +245,46 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ mb->d_addedLemmas = 0; mb->d_incomplete_check = false; if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ - Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl; + Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; d_triedLemmas += mb->d_triedLemmas; d_addedLemmas += mb->d_addedLemmas; d_incomplete_check = d_incomplete_check || mb->d_incomplete_check; d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; }else{ - Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; - Debug("inst-fmf-ei") << " Instantiation Constants: "; + Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; + Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; } - Debug("inst-fmf-ei") << std::endl; + Trace("fmf-exh-inst-debug") << std::endl; //create a rep set iterator and iterate over the (relevant) domain of the quantifier RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ - Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; - int triedLemmas = 0; - int addedLemmas = 0; - while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ - //instantiation was not shown to be true, construct the match - InstMatch m( f ); - for( int i=0; i<riter.getNumTerms(); i++ ){ - m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) ); - } - Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; - triedLemmas++; - //add as instantiation - if( d_quantEngine->addInstantiation( f, m ) ){ - addedLemmas++; - }else{ - Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl; + if( !riter.d_incomplete || options::fmfFullSaturate() ){ + int triedLemmas = 0; + int addedLemmas = 0; + while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ + //instantiation was not shown to be true, construct the match + InstMatch m( f ); + for( int i=0; i<riter.getNumTerms(); i++ ){ + m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) ); + } + Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; + triedLemmas++; + //add as instantiation + if( d_quantEngine->addInstantiation( f, m ) ){ + addedLemmas++; + }else{ + Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + } + riter.increment(); } - riter.increment(); + d_addedLemmas += addedLemmas; + d_triedLemmas += triedLemmas; + d_statistics.d_exh_inst_lemmas += addedLemmas; } - d_addedLemmas += addedLemmas; - d_triedLemmas += triedLemmas; - d_statistics.d_exh_inst_lemmas += addedLemmas; + }else{ + Assert( riter.d_incomplete ); } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round d_incomplete_check = d_incomplete_check || riter.d_incomplete; diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 47cb62715..af2d88e94 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -143,6 +143,23 @@ typedef enum { TERM_DB_RELEVANT, } TermDbMode; +typedef enum { + /** do not lift ITEs in quantified formulas */ + ITE_LIFT_QUANT_MODE_NONE, + /** only lift ITEs in quantified formulas if reduces the term size */ + ITE_LIFT_QUANT_MODE_SIMPLE, + /** lift ITEs */ + ITE_LIFT_QUANT_MODE_ALL, +} IteLiftQuantMode; + +typedef enum { + /** synthesize I( x ) */ + SYGUS_INV_TEMPL_MODE_NONE, + /** synthesize ( pre( x ) V I( x ) ) */ + SYGUS_INV_TEMPL_MODE_PRE, + /** synthesize ( post( x ) ^ I( x ) ) */ + SYGUS_INV_TEMPL_MODE_POST, +} SygusInvTemplMode; }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index fe81df7f8..5cb9062e4 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -19,7 +19,7 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write disable miniscope quantifiers for ground subformulas # Whether to prenex (nested universal) quantifiers option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h" - disable prenexing of quantified formulas + prenex mode for quantified formulas # Whether to variable-eliminate quantifiers. # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to # forall y. P( c, y ) @@ -27,13 +27,16 @@ option varElimQuant --var-elim-quant bool :default true disable simple variable elimination for quantified formulas option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers +#ite lift mode for quantified formulas +option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h" + ite lifting mode for quantified formulas option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true split variables occurring as conditions of ITE in quantifiers -option simpleIteLiftQuant --ite-lift-quant bool :default true - disable simple ite lifting for quantified formulas +option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false + split ites with dt testers as conditions # Whether to CNF quantifier bodies -option cnfQuant --cnf-quant bool :default false - apply CNF conversion to quantified formulas +# option cnfQuant --cnf-quant bool :default false +# apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas @@ -54,10 +57,10 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false # Whether to perform quantifier macro expansion option macrosQuant --macros-quant bool :default false perform quantifiers macro expansions -# Whether to perform first-order propagation -option foPropQuant --fo-prop-quant bool :default false - perform first-order propagation on quantifiers - +# Whether to CNF quantifier bodies +option elimTautQuant --elim-taut-quant bool :default true + eliminate tautological disjuncts of quantified formulas + #### E-matching options option eMatching --e-matching bool :read-write :default true @@ -83,6 +86,8 @@ option purifyDtTriggers --purify-dt-triggers bool :default false :read-write purify dt triggers, match all constructors of correct form instead of selectors option pureThTriggers --pure-th-triggers bool :default false :read-write use pure theory terms as single triggers +option partialTriggers --partial-triggers bool :default false :read-write + use triggers that do not contain all free variables option multiTriggerWhenSingle --multi-trigger-when-single bool :default false select multi triggers when single triggers exist option multiTriggerPriority --multi-trigger-priority bool :default false @@ -110,6 +115,8 @@ option eagerInstQuant --eager-inst-quant bool :default false option fullSaturateQuant --full-saturate-quant bool :default false when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown +option fullSaturateQuantRd --full-saturate-quant-rd bool :default true + whether to use relevant domain first for full saturation instantiation strategy option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" choose literal matching mode @@ -137,8 +144,10 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding +option fmfFullSaturate --fmf-full-saturate bool :default false + instantiate with all known ground terms for infinite domain quantifiers when finite model finding option fmfInstGen --fmf-inst-gen bool :default true - disable Inst-Gen instantiation techniques for finite model finding + disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false @@ -160,6 +169,8 @@ option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode : when to invoke conflict find mechanism for quantifiers option qcfTConstraint --qcf-tconstraint bool :read-write :default false enable entailment checks for t-constraints in qcf algorithm +option qcfAllConflict --qcf-all-conflict bool :read-write :default false + add all available conflicting instances during conflict-based instantiation option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed @@ -192,7 +203,7 @@ option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write filter based on canonicity option conjectureFilterModel --conjecture-filter-model bool :read-write :default true filter based on model -option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0 +option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 number of ground terms to generate for model filtering option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false more aggressive merging for universal equality engine, introduces terms @@ -209,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 @@ -225,7 +240,10 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true generalize based on content in global search space narrowing -# older implementation +option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h" + template mode for sygus invariant synthesis + +# approach applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation option cbqi2 --cbqi2 bool :read-write :default false @@ -244,4 +262,14 @@ option ltePartialInst --lte-partial-inst bool :default false option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false treat arguments of inst closure as restricted terms for instantiation +### reduction options + +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/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 9fb5dd69d..4d2276621 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -204,6 +204,32 @@ relevant \n\ + Quantifiers module considers only ground terms connected to current assertions. \n\ \n\ "; +static const std::string iteLiftQuantHelp = "\ +Modes for term database, supported by --ite-lift-quant:\n\ +\n\ +all \n\ ++ Do not lift if-then-else in quantified formulas.\n\ +\n\ +simple \n\ ++ Lift if-then-else in quantified formulas if results in smaller term size.\n\ +\n\ +none \n\ ++ Lift if-then-else in quantified formulas. \n\ +\n\ +"; +static const std::string sygusInvTemplHelp = "\ +Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ +\n\ +none \n\ ++ Synthesize invariant directly.\n\ +\n\ +pre \n\ ++ Synthesize invariant based on weakening of precondition .\n\ +\n\ +post \n\ ++ Synthesize invariant based on strengthening of postcondition. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { @@ -414,6 +440,38 @@ inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, Smt } } +inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "all" ) { + return ITE_LIFT_QUANT_MODE_ALL; + } else if(optarg == "simple") { + return ITE_LIFT_QUANT_MODE_SIMPLE; + } else if(optarg == "none") { + return ITE_LIFT_QUANT_MODE_NONE; + } else if(optarg == "help") { + puts(iteLiftQuantHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --ite-lift-quant: `") + + optarg + "'. Try --ite-lift-quant help."); + } +} + +inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "none" ) { + return SYGUS_INV_TEMPL_MODE_NONE; + } else if(optarg == "pre") { + return SYGUS_INV_TEMPL_MODE_PRE; + } else if(optarg == "post") { + return SYGUS_INV_TEMPL_MODE_POST; + } else if(optarg == "help") { + puts(sygusInvTemplHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + + optarg + "'. Try --sygus-inv-templ help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 18bffe908..47c2e1c5b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1971,6 +1971,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { Trace("qcf-debug") << std::endl; } short end_e = getMaxQcfEffort(); + bool isConflict = false; for( short e = effort_conflict; e<=end_e; e++ ){ d_effort = e; Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl; @@ -2014,8 +2015,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { ++addedLemmas; if( e==effort_conflict ){ d_quant_order.insert( d_quant_order.begin(), q ); - d_conflict.set( true ); ++(d_statistics.d_conflict_inst); + if( options::qcfAllConflict() ){ + isConflict = true; + }else{ + d_conflict.set( true ); + } break; }else if( e==effort_prop_eq ){ ++(d_statistics.d_prop_inst); @@ -2044,6 +2049,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { break; } } + if( isConflict ){ + d_conflict.set( true ); + } if( Trace.isOn("qcf-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet); diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index ca24de5f7..5e0f511e0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -110,8 +110,6 @@ public: virtual eq::EqualityEngine* getEngine() = 0; /** get the equivalence class of a */ virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; - - virtual void setLiberal( bool l ) = 0; };/* class EqualityQuery */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0afdece82..6a95e243d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -340,64 +340,141 @@ Node QuantifiersRewriter::computeNNF( Node body ){ } } + +void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, + std::vector< Node >& conj ){ + if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ + Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; + Node x = n[0][0]; + std::map< Node, Node >::iterator itp = pcons.find( x ); + if( itp!=pcons.end() ){ + Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl; + computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj ); + }else{ + Expr testerExpr = n[0].getOperator().toExpr(); + int index = Datatype::indexOf( testerExpr ); + std::map< int, Node >::iterator itn = ncons[x].find( index ); + if( itn!=ncons[x].end() ){ + Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl; + computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj ); + }else{ + for( unsigned i=0; i<2; i++ ){ + if( i==0 ){ + pcons[x] = n[0]; + }else{ + pcons.erase( x ); + ncons[x][index] = n[0].negate(); + } + computeDtTesterIteSplit( n[i+1], pcons, ncons, conj ); + } + ncons[x].erase( index ); + } + } + }else{ + Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl; + std::vector< Node > children; + children.push_back( n ); + std::vector< Node > vars; + //add all positive testers + for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){ + children.push_back( it->second.negate() ); + vars.push_back( it->first ); + } + //add all negative testers + for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){ + Node x = it->first; + //only if we haven't settled on a positive tester + if( std::find( vars.begin(), vars.end(), x )==vars.end() ){ + //check if we have exhausted all options but one + const Datatype& dt = DatatypeType(x.getType().toType()).getDatatype(); + std::vector< Node > nchildren; + int pos_cons = -1; + for( int i=0; i<(int)dt.getNumConstructors(); i++ ){ + std::map< int, Node >::iterator itt = it->second.find( i ); + if( itt==it->second.end() ){ + pos_cons = pos_cons==-1 ? i : -2; + }else{ + nchildren.push_back( itt->second.negate() ); + } + } + if( pos_cons>=0 ){ + const DatatypeConstructor& c = dt[pos_cons]; + Expr tester = c.getTester(); + children.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), x ).negate() ); + }else{ + children.insert( children.end(), nchildren.begin(), nchildren.end() ); + } + } + } + //make condition/output pair + Node c = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + conj.push_back( c ); + } +} + Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) { if( body.getType().isBoolean() ){ - if( body.getKind()==EQUAL && options::simpleIteLiftQuant() ){ + if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){ for( size_t i=0; i<2; i++ ){ if( body[i].getKind()==ITE ){ Node no = i==0 ? body[1] : body[0]; - bool doRewrite = false; - std::vector< Node > children; - children.push_back( body[i][0] ); - for( size_t j=1; j<=2; j++ ){ - //check if it rewrites to a constant - Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); - nn = Rewriter::rewrite( nn ); - children.push_back( nn ); - if( nn.isConst() ){ - doRewrite = true; + if( no.getKind()!=ITE ){ + bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL; + std::vector< Node > children; + children.push_back( body[i][0] ); + for( size_t j=1; j<=2; j++ ){ + //check if it rewrites to a constant + Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); + nn = Rewriter::rewrite( nn ); + children.push_back( nn ); + if( nn.isConst() ){ + doRewrite = true; + } + } + if( doRewrite ){ + return NodeManager::currentNM()->mkNode( ITE, children ); } - } - if( doRewrite ){ - return NodeManager::currentNM()->mkNode( ITE, children ); } } } - }else if( body.getKind()==ITE && hasPol && options::iteCondVarSplitQuant() ){ - for( unsigned r=0; r<2; r++ ){ - //check if there is a variable elimination - Node b = r==0 ? body[0] : body[0].negate(); - QuantPhaseReq qpr( b ); - std::vector< Node > vars; - std::vector< Node > subs; - Trace("ite-var-split-quant") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; - for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ - Trace("ite-var-split-quant") << "phase req " << it->first << " -> " << it->second << std::endl; - if( it->second ){ - if( it->first.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( it->first[i].getKind()==BOUND_VARIABLE ){ - unsigned j = i==0 ? 1 : 0; - if( !hasArg1( it->first[i], it->first[j] ) ){ - vars.push_back( it->first[i] ); - subs.push_back( it->first[j] ); - break; + }else if( body.getKind()==ITE && hasPol ){ + if( options::iteCondVarSplitQuant() ){ + Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl; + for( unsigned r=0; r<2; r++ ){ + //check if there is a variable elimination + Node b = r==0 ? body[0] : body[0].negate(); + QuantPhaseReq qpr( b ); + std::vector< Node > vars; + std::vector< Node > subs; + Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ + Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl; + if( it->second ){ + if( it->first.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + if( it->first[i].getKind()==BOUND_VARIABLE ){ + unsigned j = i==0 ? 1 : 0; + if( !hasArg1( it->first[i], it->first[j] ) ){ + vars.push_back( it->first[i] ); + subs.push_back( it->first[j] ); + break; + } } } } } } - } - if( !vars.empty() ){ - //bool cpol = (r==1); - Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); - //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - //pos = Rewriter::rewrite( pos ); - Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); - //Trace("ite-var-split-quant") << "Split ITE " << body << " into : " << std::endl; - //Trace("ite-var-split-quant") << " " << pos << std::endl; - //Trace("ite-var-split-quant") << " " << neg << std::endl; - return NodeManager::currentNM()->mkNode( AND, pos, neg ); + if( !vars.empty() ){ + //bool cpol = (r==1); + Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); + //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + //pos = Rewriter::rewrite( pos ); + Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); + Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl; + Trace("quantifiers-rewrite-ite") << " " << pos << std::endl; + Trace("quantifiers-rewrite-ite") << " " << neg << std::endl; + return NodeManager::currentNM()->mkNode( AND, pos, neg ); + } } } } @@ -420,6 +497,26 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) return body; } +Node QuantifiersRewriter::computeProcessIte2( Node body ){ + if( body.getKind()==ITE ){ + if( options::iteDtTesterSplitQuant() ){ + Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; + std::map< Node, Node > pcons; + std::map< Node, std::map< int, Node > > ncons; + std::vector< Node > conj; + computeDtTesterIteSplit( body, pcons, ncons, conj ); + Assert( !conj.empty() ); + if( conj.size()>1 ){ + Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl; + for( unsigned i=0; i<conj.size(); i++ ){ + Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl; + } + return NodeManager::currentNM()->mkNode( AND, conj ); + } + } + } + return body; +} Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ @@ -677,6 +774,30 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b } } +Node QuantifiersRewriter::computeElimTaut( Node body ) { + if( body.getKind()==OR ){ + std::vector< Node > children; + std::map< Node, bool > lit_pol; + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node lit = body[i].getKind()==NOT ? body[i][0] : body[i]; + bool pol = body[i].getKind()!=NOT; + std::map< Node, bool >::iterator it = lit_pol.find( lit ); + if( it==lit_pol.end() ){ + lit_pol[lit] = pol; + children.push_back( body[i] ); + }else{ + if( it->second!=pol ){ + return NodeManager::currentNM()->mkConst( true ); + } + } + } + if( children.size()!=body.getNumChildren() ){ + return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + } + } + return body; +} + Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) { if( body.getKind()==OR ){ size_t var_found_count = 0; @@ -784,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{ @@ -1002,9 +1137,13 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_NNF ){ return options::nnfQuant(); }else if( computeOption==COMPUTE_PROCESS_ITE ){ - return options::iteCondVarSplitQuant() || options::simpleIteLiftQuant(); + return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); + }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){ + return options::iteDtTesterSplitQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); + }else if( computeOption==COMPUTE_ELIM_TAUT ){ + return options::elimTautQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant() || options::dtVarExpandQuant(); }else if( computeOption==COMPUTE_CNF ){ @@ -1041,8 +1180,12 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp n = computeNNF( n ); }else if( computeOption==COMPUTE_PROCESS_ITE ){ n = computeProcessIte( n, true, true ); + }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){ + n = computeProcessIte2( n ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); + }else if( computeOption==COMPUTE_ELIM_TAUT ){ + n = computeElimTaut( n ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ Node prev; do{ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 838eff57b..d01677171 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -40,15 +40,18 @@ private: static bool hasArg( std::vector< Node >& args, Node n ); static bool hasArg1( Node a, Node n ); static Node computeClause( Node n ); + static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); private: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); static Node computeNNF( Node body ); static Node computeProcessIte( Node body, bool hasPol, bool pol ); + static Node computeProcessIte2( Node body ); static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); + static Node computeElimTaut( Node body ); static Node computeSplit( Node f, Node body, std::vector< Node >& args ); private: enum{ @@ -57,7 +60,9 @@ private: COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, COMPUTE_PROCESS_ITE, + COMPUTE_PROCESS_ITE_2, COMPUTE_PRENEX, + COMPUTE_ELIM_TAUT, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, COMPUTE_CNF, diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2671f616b..c6115195d 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" @@ -77,7 +78,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) { +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); if( options::ceGuidedInst() ){ @@ -129,11 +130,12 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi bool rec = false; if( d_processed.find( n )==d_processed.end() ){ d_processed.insert(n); - d_type_map[ n.getType() ].push_back( n ); - //if this is an atomic trigger, consider adding it - //Call the children? - if( inst::Trigger::isAtomicTrigger( n ) ){ - if( !TermDb::hasInstConstAttr(n) ){ + if( !TermDb::hasInstConstAttr(n) ){ + Trace("term-db-debug") << "register term : " << n << std::endl; + d_type_map[ n.getType() ].push_back( n ); + //if this is an atomic trigger, consider adding it + //Call the children? + if( inst::Trigger::isAtomicTrigger( n ) ){ Trace("term-db") << "register term in db " << n << std::endl; Node op = getOperator( n ); /* @@ -166,7 +168,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi d_iclosure_processed.insert( n ); rec = true; } - if( rec ){ + if( rec && n.getKind()!=FORALL ){ for( size_t i=0; i<n.getNumChildren(); i++ ){ addTerm( n[i], added, withinQuant, withinInstClosure ); } @@ -409,7 +411,7 @@ bool TermDb::isInstClosure( Node r ) { return d_iclosure_processed.find( r )!=d_iclosure_processed.end(); } -//checks whether a type is reasonably small enough such that all of its domain elements can be enumerated +//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated bool TermDb::mayComplete( TypeNode tn ) { std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); if( it==d_may_complete.end() ){ @@ -779,6 +781,7 @@ Node TermDb::getCounterexampleLiteral( Node f ){ } Node TermDb::getInstConstantNode( Node n, Node f ){ + Assert( d_inst_constants.find( f )!=d_inst_constants.end() ); return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); } @@ -945,6 +948,7 @@ Node TermDb::getSkolemizedBody( Node f ){ } Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { + Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl; std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); unsigned teIndex; if( it==d_typ_enum_map.end() ){ @@ -1154,6 +1158,156 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){ nodes.insert( nodes.begin(), temp.begin(), temp.end() ); } +int TermDb::getIdForOperator( Node op ) { + std::map< Node, int >::iterator it = d_op_id.find( op ); + if( it==d_op_id.end() ){ + d_op_id[op] = d_op_id_count; + d_op_id_count++; + return d_op_id[op]; + }else{ + return it->second; + } +} + +int TermDb::getIdForType( TypeNode t ) { + std::map< TypeNode, int >::iterator it = d_typ_id.find( t ); + if( it==d_typ_id.end() ){ + d_typ_id[t] = d_typ_id_count; + d_typ_id_count++; + return d_typ_id[t]; + }else{ + return it->second; + } +} + +bool TermDb::getTermOrder( Node a, Node b ) { + if( a.getKind()==BOUND_VARIABLE ){ + if( b.getKind()==BOUND_VARIABLE ){ + return a.getAttribute(InstVarNumAttribute())<b.getAttribute(InstVarNumAttribute()); + }else{ + return true; + } + }else if( b.getKind()!=BOUND_VARIABLE ){ + Node aop = a.hasOperator() ? a.getOperator() : a; + Node bop = b.hasOperator() ? b.getOperator() : b; + Trace("aeq-debug2") << a << "...op..." << aop << std::endl; + Trace("aeq-debug2") << b << "...op..." << bop << std::endl; + if( aop==bop ){ + if( a.getNumChildren()==b.getNumChildren() ){ + for( unsigned i=0; i<a.getNumChildren(); i++ ){ + if( a[i]!=b[i] ){ + //first distinct child determines the ordering + return getTermOrder( a[i], b[i] ); + } + } + }else{ + return aop.getNumChildren()<bop.getNumChildren(); + } + }else{ + return getIdForOperator( aop )<getIdForOperator( bop ); + } + } + return false; +} + + + +Node TermDb::getCanonicalFreeVar( TypeNode tn, unsigned i ) { + Assert( !tn.isNull() ); + while( d_cn_free_var[tn].size()<=i ){ + std::stringstream oss; + oss << tn; + std::string typ_name = oss.str(); + while( typ_name[0]=='(' ){ + typ_name.erase( typ_name.begin() ); + } + std::stringstream os; + os << typ_name[0] << i; + Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn ); + InstVarNumAttribute ivna; + x.setAttribute(ivna,d_cn_free_var[tn].size()); + d_cn_free_var[tn].push_back( x ); + } + return d_cn_free_var[tn][i]; +} + +struct sortTermOrder { + TermDb* d_tdb; + //std::map< Node, std::map< Node, bool > > d_cache; + bool operator() (Node i, Node j) { + /* + //must consult cache since term order is partial? + std::map< Node, bool >::iterator it = d_cache[j].find( i ); + if( it!=d_cache[j].end() && it->second ){ + return false; + }else{ + bool ret = d_tdb->getTermOrder( i, j ); + d_cache[i][j] = ret; + return ret; + } + */ + return d_tdb->getTermOrder( i, j ); + } +}; + +//this function makes a canonical representation of a term ( +// - orders variables left to right +// - if apply_torder, then sort direct subterms of commutative operators +Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) { + Trace("canon-term-debug") << "Get canonical term for " << n << std::endl; + if( n.getKind()==BOUND_VARIABLE ){ + std::map< TNode, TNode >::iterator it = subs.find( n ); + if( it==subs.end() ){ + TypeNode tn = n.getType(); + //allocate variable + unsigned vn = var_count[tn]; + var_count[tn]++; + subs[n] = getCanonicalFreeVar( tn, vn ); + Trace("canon-term-debug") << "...allocate variable." << std::endl; + return subs[n]; + }else{ + Trace("canon-term-debug") << "...return variable in subs." << std::endl; + return it->second; + } + }else if( n.getNumChildren()>0 ){ + //collect children + Trace("canon-term-debug") << "Collect children" << std::endl; + std::vector< Node > cchildren; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + cchildren.push_back( n[i] ); + } + //if applicable, first sort by term order + if( apply_torder && isComm( n.getKind() ) ){ + Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl; + sortTermOrder sto; + sto.d_tdb = this; + std::sort( cchildren.begin(), cchildren.end(), sto ); + } + //now make canonical + Trace("canon-term-debug") << "Make canonical children" << std::endl; + for( unsigned i=0; i<cchildren.size(); i++ ){ + cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder ); + } + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl; + cchildren.insert( cchildren.begin(), n.getOperator() ); + } + Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl; + Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren ); + Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; + return ret; + }else{ + Trace("canon-term-debug") << "...return 0-child term." << std::endl; + return n; + } +} + +Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){ + std::map< TypeNode, unsigned > var_count; + std::map< TNode, TNode > subs; + return getCanonicalTerm( n, var_count, subs, apply_torder ); +} + bool TermDb::containsTerm( Node n, Node t ) { if( n==t ){ return true; @@ -1179,6 +1333,15 @@ Node TermDb::simpleNegate( Node n ){ } } +bool TermDb::isAssoc( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; +} + +bool TermDb::isComm( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; +} void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ @@ -1270,6 +1433,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 @@ -1417,7 +1581,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]; } @@ -1440,7 +1604,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect return p==n; }else if( n.getKind()==p.getKind() && n.getNumChildren()==p.getNumChildren() ){ //try both ways? - unsigned rmax = isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; + unsigned rmax = TermDb::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; std::vector< int > new_tmp; for( unsigned r=0; r<rmax; r++ ){ bool success = true; @@ -1579,7 +1743,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; */ } @@ -1591,6 +1755,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); if( it==d_sygus_to_builtin[tn].end() ){ + Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; Assert( n.getKind()==APPLY_CONSTRUCTOR ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); @@ -1666,7 +1831,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) { int end = d_const_list[tn1].size()-d_const_list_pos[tn1]; for( int i=start; i>=end; --i ){ Node c1 = d_const_list[tn1][i]; - //only consider if smaller than c, and + //only consider if smaller than c, and if( doCompare( c1, c, ck ) ){ Node c2 = NodeManager::currentNM()->mkNode( pkm, c, c1 ); c2 = Rewriter::rewrite( c2 ); @@ -1756,28 +1921,18 @@ Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool d } } -int TermDbSygus::getTermSize( Node n ){ +int TermDbSygus::getSygusTermSize( Node n ){ if( isVar( n ) ){ return 0; }else{ int sum = 0; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - sum += getTermSize( n[i] ); + sum += getSygusTermSize( n[i] ); } return 1+sum; } } -bool TermDbSygus::isAssoc( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; -} - -bool TermDbSygus::isComm( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; -} - bool TermDbSygus::isAntisymmetric( Kind k, Kind& dk ) { if( k==GT ){ dk = LT; @@ -1942,10 +2097,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() ) ); @@ -1956,14 +2111,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 ); @@ -1976,7 +2131,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() ){ @@ -1986,12 +2141,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++ ){ @@ -2008,6 +2163,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 ); @@ -2197,6 +2357,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){ @@ -2216,7 +2377,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 << " "; @@ -2225,9 +2399,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; @@ -2241,23 +2416,26 @@ 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(); - for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){ + 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]; std::stringstream new_str; @@ -2266,12 +2444,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 b7fa4e999..1ffe0e29e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -149,13 +149,13 @@ public: unsigned getNumGroundTerms( Node f ); /** count number of non-redundant ground terms per operator */ std::map< Node, int > d_op_nonred_count; - /** map from APPLY_UF operators to ground terms for that operator */ + /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; /** has map */ std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ std::map< Node, Node > d_term_elig_eqc; - /** map from APPLY_UF functions to trie */ + /** map from operators to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; /**mapping from UF terms to representatives of their arguments */ @@ -326,12 +326,42 @@ public: /** filter all nodes that have instances */ void filterInstances( std::vector< Node >& nodes ); +//for term ordering +private: + /** operator id count */ + int d_op_id_count; + /** map from operators to id */ + std::map< Node, int > d_op_id; + /** type id count */ + int d_typ_id_count; + /** map from type to id */ + std::map< TypeNode, int > d_typ_id; + //free variables + std::map< TypeNode, std::vector< Node > > d_cn_free_var; + // get canonical term, return null if it contains a term apart from handled signature + Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ); +public: + /** get id for operator */ + int getIdForOperator( Node op ); + /** get id for type */ + int getIdForType( TypeNode t ); + /** get term order */ + bool getTermOrder( Node a, Node b ); + /** get canonical free variable #i of type tn */ + Node getCanonicalFreeVar( TypeNode tn, unsigned i ); + /** get canonical term */ + Node getCanonicalTerm( TNode n, bool apply_torder = false ); + //general utilities public: /** simple check for contains term */ static bool containsTerm( Node n, Node t ); /** simple negate */ static Node simpleNegate( Node n ); + /** is assoc */ + static bool isAssoc( Kind k ); + /** is comm */ + static bool isComm( Kind k ); //for sygus private: @@ -403,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; @@ -425,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 ); @@ -441,10 +472,6 @@ public: void registerSygusType( TypeNode tn ); /** get arg type */ TypeNode getArgType( const DatatypeConstructor& c, int i ); - /** is assoc */ - bool isAssoc( Kind k ); - /** is comm */ - bool isComm( Kind k ); /** isAntisymmetric */ bool isAntisymmetric( Kind k, Kind& dk ); /** is idempotent arg */ @@ -459,13 +486,13 @@ 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 ); Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true ); - int getTermSize( Node n ); + int getSygusTermSize( Node n ); /** given a term, construct an equivalent smaller one that respects syntax */ Node minimizeBuiltinTerm( Node n ); /** given a term, expand it into more basic components */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c55ed27ea..e4d9a2730 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -145,7 +145,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& break; } } - if( varCount<f[0].getNumChildren() ){ + if( varCount<f[0].getNumChildren() && !options::partialTriggers() ){ Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl; for( unsigned i=0; i<nodes.size(); i++) { Trace("trigger-debug") << nodes[i] << " "; @@ -226,6 +226,12 @@ bool Trigger::isUsable( Node n, Node f ){ if( isBooleanTermTrigger( n ) ){ return true; } + if( options::purifyTriggers() ){ + Node x = getInversionVariable( n ); + if( !x.isNull() ){ + return true; + } + } } return false; }else{ @@ -247,6 +253,7 @@ bool nodeContainsVar( Node n, Node v ){ } Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { + Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl; if( options::relationalTriggers() ){ if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ Node rtr; @@ -287,7 +294,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { } } bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); - Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; + Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; if( usable ){ return n; }else{ @@ -512,13 +519,16 @@ Node Trigger::getInversionVariable( Node n ) { if( !n[i].isConst() ){ Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl; return Node::null(); - }else if( n.getType().isInteger() ){ + } + /* + else if( n.getType().isInteger() ){ Rational r = n[i].getConst<Rational>(); if( r!=Rational(-1) && r!=Rational(1) ){ Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl; return Node::null(); } } + */ } } return ret; @@ -539,8 +549,13 @@ Node Trigger::getInversion( Node n, Node x ) { x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] ); }else if( n.getKind()==MULT ){ Assert( n[i].isConst() ); - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() ); - x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + if( x.getType().isInteger() ){ + Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>() ); + x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff ); + }else{ + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() ); + x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + } } }else{ Assert( cindex==-1 ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e654a689d..54f2a16fe 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -32,10 +32,12 @@ #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/alpha_equivalence.h" #include "theory/uf/options.h" #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; @@ -99,7 +101,7 @@ d_lemmas_produced_c(u){ }else{ d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); } - if( !options::finiteModelFind() ){ + if( options::fullSaturateQuant() ){ d_rel_dom = new quantifiers::RelevantDomain( this, d_model ); }else{ d_rel_dom = NULL; @@ -163,6 +165,17 @@ d_lemmas_produced_c(u){ }else{ d_lte_part_inst = NULL; } + if( options::quantAlphaEquiv() ){ + d_alpha_equiv = new quantifiers::AlphaEquivalence( this ); + }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; @@ -202,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; } @@ -298,6 +312,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; } Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl; + Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl; Trace("quant-engine-debug") << "Resetting all modules..." << std::endl; } if( Trace.isOn("quant-engine-ee") ){ @@ -422,6 +437,38 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } +bool QuantifiersEngine::reduceQuantifier( Node q ) { + std::map< Node, bool >::iterator it = d_quants_red.find( q ); + if( it==d_quants_red.end() ){ + if( d_alpha_equiv ){ + Trace("quant-engine-debug") << "Alpha equivalence " << q << "?" << std::endl; + //add equivalence with another quantified formula + if( !d_alpha_equiv->registerQuantifier( q ) ){ + Trace("quant-engine-debug") << "...alpha equivalence success." << std::endl; + ++(d_statistics.d_red_alpha_equiv); + d_quants_red[q] = true; + return true; + } + } + if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){ + //will partially instantiate + Trace("quant-engine-debug") << "LTE: Partially instantiate " << q << "?" << std::endl; + if( d_lte_part_inst->addQuantifier( q ) ){ + Trace("quant-engine-debug") << "...LTE partially instantiate success." << std::endl; + //delayed reduction : assert to model + d_model->assertQuantifier( q, true ); + ++(d_statistics.d_red_lte_partial_inst); + d_quants_red[q] = true; + return true; + } + } + d_quants_red[q] = false; + return false; + }else{ + return it->second; + } +} + bool QuantifiersEngine::registerQuantifier( Node f ){ std::map< Node, bool >::iterator it = d_quants.find( f ); if( it==d_quants.end() ){ @@ -431,15 +478,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ Assert( f.getKind()==FORALL ); //check whether we should apply a reduction - bool reduced = false; - if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ - Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl; - if( d_lte_part_inst->addQuantifier( f ) ){ - reduced = true; - } - } - if( reduced ){ - d_model->assertQuantifier( f, true ); + if( reduceQuantifier( f ) ){ d_quants[f] = false; return false; }else{ @@ -482,30 +521,31 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) { void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ if( !pol ){ - //do skolemization - if( d_skolemized.find( f )==d_skolemized.end() ){ - Node body = d_term_db->getSkolemizedBody( f ); - NodeBuilder<> nb(kind::OR); - nb << f << body.notNode(); - Node lem = nb; - if( Trace.isOn("quantifiers-sk") ){ - Node slem = Rewriter::rewrite( lem ); - Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + //if not reduced + if( !reduceQuantifier( f ) ){ + //do skolemization + if( d_skolemized.find( f )==d_skolemized.end() ){ + Node body = d_term_db->getSkolemizedBody( f ); + NodeBuilder<> nb(kind::OR); + nb << f << body.notNode(); + Node lem = nb; + if( Trace.isOn("quantifiers-sk") ){ + Node slem = Rewriter::rewrite( lem ); + Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + } + getOutputChannel().lemma( lem, false, true ); + d_skolemized[f] = true; } - getOutputChannel().lemma( lem, false, true ); - d_skolemized[f] = true; } - } - //assert to modules TODO : handle !pol - if( pol ){ - //register the quantifier - bool nreduced = registerQuantifier( f ); - //assert it to each module - if( nreduced ){ + }else{ + //assert to modules TODO : also for !pol? + //register the quantifier, assert it to each module + if( registerQuantifier( f ) ){ d_model->assertQuantifier( f ); for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->assertNode( f ); } + addTermToDatabase( d_term_db->getInstConstantBody( f ), true ); } } } @@ -714,6 +754,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){ } Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) { + d_term_db->makeInstantiationConstantsFor( f ); return getInstantiation( f, d_term_db->d_inst_constants[f], terms ); } @@ -783,12 +824,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term - Node ti = d_eq_query->getInternalRepresentative( terms[i], f, i ); - //check if it is a subtype (can be violated in mixed int/real) FIXME : do this check inside getInternalRepresentative - if( ti.getType().isSubtypeOf( f[0][i].getType() ) ){ - terms[i] = ti; - Trace("inst-add-debug2") << " (" << terms[i] << ")"; - } + terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i ); } } Trace("inst-add-debug") << std::endl; @@ -980,7 +1016,9 @@ QuantifiersEngine::Statistics::Statistics(): d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0) + d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), + d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), + d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0) { StatisticsRegistry::registerStat(&d_num_quant); StatisticsRegistry::registerStat(&d_instantiation_rounds); @@ -992,6 +1030,8 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_simple_triggers); StatisticsRegistry::registerStat(&d_multi_triggers); StatisticsRegistry::registerStat(&d_multi_trigger_instantiations); + StatisticsRegistry::registerStat(&d_red_alpha_equiv); + StatisticsRegistry::registerStat(&d_red_lte_partial_inst); } QuantifiersEngine::Statistics::~Statistics(){ @@ -1005,6 +1045,8 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_simple_triggers); StatisticsRegistry::unregisterStat(&d_multi_triggers); StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations); + StatisticsRegistry::unregisterStat(&d_red_alpha_equiv); + StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst); } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ @@ -1070,16 +1112,12 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ return true; }else{ eq::EqualityEngine* ee = getEngine(); - if( d_liberal ){ - return true;//!areDisequal( a, b ); - }else{ - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - if( ee->areEqual( a, b ) ){ - return true; - } + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areEqual( a, b ) ){ + return true; } - return false; } + return false; } } @@ -1094,6 +1132,7 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ } Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ + Assert( f.isNull() || f.getKind()==FORALL ); Node r = getRepresentative( a ); if( !options::internalReps() ){ return r; @@ -1108,16 +1147,17 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, r = getRepresentative( r ); }else{ if( r.getType().isSort() ){ - //TODO : this can happen in rare cases - // say x:(Array Int U), select( x, 0 ), x assigned (const @u1). Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; + //should never happen : UF constants should never escape model + Assert( false ); } } } } } - std::map< Node, Node >::iterator itir = d_int_rep.find( r ); - if( itir==d_int_rep.end() ){ + TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType(); + std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r ); + if( itir==d_int_rep[v_tn].end() ){ //find best selection for representative Node r_best; //if( options::fmfRelevantDomain() && !f.isNull() ){ @@ -1135,7 +1175,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; for( size_t i=0; i<eqc.size(); i++ ){ - int score = getRepScore( eqc[i], f, index ); + int score = getRepScore( eqc[i], f, index, v_tn ); if( score!=-2 ){ if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){ r_best = eqc[i]; @@ -1144,12 +1184,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, } } if( r_best.isNull() ){ - if( !f.isNull() ){ - Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); - r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - }else{ - r_best = a; - } + Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl; + r_best = r; } //now, make sure that no other member of the class is an instance std::hash_map<TNode, Node, TNodeHashFunction> cache; @@ -1159,7 +1195,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, d_rep_score[ r_best ] = d_reset_count; } Trace("internal-rep-select") << "...Choose " << r_best << std::endl; - d_int_rep[r] = r_best; + d_int_rep[v_tn][r] = r_best; if( r_best!=a ){ Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; @@ -1181,8 +1217,10 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, } } Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; - for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ - Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; + } } //store representatives for newly created terms std::map< Node, Node > temp_rep_map; @@ -1190,51 +1228,55 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, bool success; do { success = false; - for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ - if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ - Node ni = it->second; - std::vector< Node > cc; - cc.push_back( it->second.getOperator() ); - bool changed = false; - for( unsigned j=0; j<ni.getNumChildren(); j++ ){ - if( ni[j].getType().isSort() ){ - Node r = getRepresentative( ni[j] ); - if( d_int_rep.find( r )==d_int_rep.end() ){ - Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); - r = temp_rep_map[r]; - } - if( r==ni ){ - //found sub-term as instance - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; - d_int_rep[it->first] = ni[j]; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ + Node ni = it->second; + std::vector< Node > cc; + cc.push_back( it->second.getOperator() ); + bool changed = false; + for( unsigned j=0; j<ni.getNumChildren(); j++ ){ + if( ni[j].getType().isSort() ){ + Node r = getRepresentative( ni[j] ); + if( itt->second.find( r )==itt->second.end() ){ + Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); + r = temp_rep_map[r]; + } + if( r==ni ){ + //found sub-term as instance + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; + itt->second[it->first] = ni[j]; + changed = false; + success = true; + break; + }else{ + Node ir = itt->second[r]; + cc.push_back( ir ); + if( ni[j]!=ir ){ + changed = true; + } + } + }else{ changed = false; - success = true; break; - }else{ - Node ir = d_int_rep[r]; - cc.push_back( ir ); - if( ni[j]!=ir ){ - changed = true; - } } - }else{ - changed = false; - break; } - } - if( changed ){ - Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; - success = true; - d_int_rep[it->first] = n; - temp_rep_map[n] = it->first; + if( changed ){ + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; + success = true; + itt->second[it->first] = n; + temp_rep_map[n] = it->first; + } } } } }while( success ); Trace("internal-rep-flatten") << "---After flattening : " << std::endl; - for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ - Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; + } } } @@ -1277,6 +1319,7 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod } } +/* int getDepth( Node n ){ if( n.getNumChildren()==0 ){ return 0; @@ -1291,10 +1334,13 @@ int getDepth( Node n ){ return maxDepth; } } +*/ -//smaller the score, the better -int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){ - if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ +//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better +int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){ + if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ //reject + return -2; + }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type return -2; }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ return -1; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d5887f907..54f63bfe0 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -92,6 +92,8 @@ namespace quantifiers { class ConjectureGenerator; class CegInstantiation; class LtePartialInst; + class AlphaEquivalence; + class FunDefEngine; }/* CVC4::theory::quantifiers */ namespace inst { @@ -119,6 +121,8 @@ private: QuantRelevance * d_quant_rel; /** relevant domain */ quantifiers::RelevantDomain* d_rel_dom; + /** alpha equivalence */ + quantifiers::AlphaEquivalence * d_alpha_equiv; /** model builder */ quantifiers::QModelBuilder* d_builder; /** phase requirements for each quantifier for each instantiation literal */ @@ -139,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, @@ -150,6 +156,8 @@ public: //effort levels private: /** list of all quantifiers seen */ std::map< Node, bool > d_quants; + /** quantifiers reduced */ + std::map< Node, bool > d_quants_red; /** list of all lemmas produced */ //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; @@ -186,8 +194,7 @@ public: ~QuantifiersEngine(); /** get theory engine */ TheoryEngine* getTheoryEngine() { return d_te; } - /** get equality query object for the given type. The default is the - generic one */ + /** get equality query */ EqualityQueryQuantifiersEngine* getEqualityQuery(); /** get default sat context for quantifiers engine */ context::Context* getSatContext(); @@ -224,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; @@ -250,6 +259,8 @@ public: /** get next decision request */ Node getNextDecisionRequest(); private: + /** reduce quantifier */ + bool reduceQuantifier( Node q ); /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** instantiate f with arguments terms */ @@ -322,6 +333,8 @@ public: IntStat d_simple_triggers; IntStat d_multi_triggers; IntStat d_multi_trigger_instantiations; + IntStat d_red_alpha_equiv; + IntStat d_red_lte_partial_inst; Statistics(); ~Statistics(); };/* class QuantifiersEngine::Statistics */ @@ -337,20 +350,18 @@ private: /** pointer to theory engine */ QuantifiersEngine* d_qe; /** internal representatives */ - std::map< Node, Node > d_int_rep; + std::map< TypeNode, std::map< Node, Node > > d_int_rep; /** rep score */ std::map< Node, int > d_rep_score; /** reset count */ int d_reset_count; - - bool d_liberal; private: /** node contains */ Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ); /** get score */ - int getRepScore( Node n, Node f, int index ); + int getRepScore( Node n, Node f, int index, TypeNode v_tn ); public: - EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){} + EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){} ~EqualityQueryQuantifiersEngine(){} /** reset */ void reset(); @@ -368,8 +379,6 @@ public: Node getInternalRepresentative( Node a, Node f, int index ); /** flatten representatives */ void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); - - void setLiberal( bool l ) { d_liberal = l; } }; /* EqualityQueryQuantifiersEngine */ }/* CVC4::theory namespace */ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index eb05564e5..6a64f762e 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -16,6 +16,7 @@ #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; using namespace CVC4; @@ -187,8 +188,14 @@ bool RepSetIterator::initialize(){ TypeNode tn = d_types[i]; Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl; if( tn.isSort() ){ + //must ensure uninterpreted type is non-empty. if( !d_rep_set->hasType( tn ) ){ - Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); + //FIXME: + // terms in rep_set are now constants which mapped to terms through TheoryModel + // thus, should introduce a constant and a term. for now, just a term. + + //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); + Node var = d_qe->getModel()->getSomeDomainElement( tn ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); } @@ -216,15 +223,18 @@ bool RepSetIterator::initialize(){ d_incomplete = true; } } - //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now + //enumerate if the sort is reasonably small }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; d_rep_set->complete( tn ); + //must have succeeded + Assert( d_rep_set->hasType( tn ) ); }else{ Trace("rsi") << " variable cannot be bounded." << std::endl; Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } + //if we have yet to determine the type of enumeration if( d_enum_type.size()<=i ){ d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); if( d_rep_set->hasType( tn ) ){ diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 551c0b0ee..fa8f108c3 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -62,6 +62,7 @@ public: // by the TypeEnumerator framework. SetEnumerator(const SetEnumerator& ae) throw() : TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)), + d_index(ae.d_index), d_constituentType(ae.d_constituentType), d_nm(ae.d_nm), d_indexVec(ae.d_indexVec), diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 52b018234..05d0c896a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -478,6 +478,14 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac cache.insert(n); } +void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) { + constantReps[eqc] = const_rep; + Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl; + if( !fullModel ){ + tm->d_rep_set.d_values_to_terms[const_rep] = eqc; + } +} + void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) { @@ -551,7 +559,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (!const_rep.isNull()) { // Theories should not specify a rep if there is already a constant in the EC Assert(rep.isNull() || rep == const_rep); - constantReps[eqc] = const_rep; + assignConstantRep( tm, constantReps, eqc, const_rep, fullModel ); typeConstSet.add(eqct.getBaseType(), const_rep); } else if (!rep.isNull()) { @@ -615,7 +623,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Node normalized = normalize(tm, n, constantReps, true); if (normalized.isConst()) { typeConstSet.add(tb, normalized); - constantReps[*i2] = normalized; + assignConstantRep( tm, constantReps, *i2, normalized, fullModel ); Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; changed = true; evaluated = true; @@ -648,7 +656,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (normalized.isConst()) { changed = true; typeConstSet.add(tb, normalized); - constantReps[*i] = normalized; + assignConstantRep( tm, constantReps, *i, normalized, fullModel ); assertedReps.erase(*i); i2 = i; ++i; @@ -727,11 +735,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) n = *te; } Assert(!n.isNull()); - constantReps[*i2] = n; - Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl; - if( !fullModel ){ - tm->d_rep_set.d_values_to_terms[n] = (*i2); - } + assignConstantRep( tm, constantReps, *i2, n, fullModel ); changed = true; noRepSet.erase(i2); if (assignOne) { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index be202fb69..a161f02f4 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -261,7 +261,7 @@ protected: Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly); bool isAssignable(TNode n); void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache); - + void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ); public: TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index 9aef059bd..c88d9adff 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -296,7 +296,7 @@ void SortInference::setEqual( int t1, int t2 ){ d_type_types[rt2] = it1->second; d_type_types.erase( rt1 ); }else{ - //may happen for mixed int/real + Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types[rt1] << " and " << d_type_types[rt2] << std::endl; return; } } @@ -361,14 +361,25 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ int retType; if( n.getKind()==kind::EQUAL ){ - //we only require that the left and right hand side must be equal - setEqual( child_types[0], child_types[1] ); + Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl; + //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction + if( n[0].getType()!=n[1].getType() ){ + //for now, assume the original types + for( unsigned i=0; i<2; i++ ){ + int ct = getIdForType( n[i].getType() ); + setEqual( child_types[i], ct ); + } + }else{ + //we only require that the left and right hand side must be equal + setEqual( child_types[0], child_types[1] ); + } //int eqType = getIdForType( n[0].getType() ); //setEqual( child_types[0], eqType ); //setEqual( child_types[1], eqType ); retType = getIdForType( n.getType() ); }else if( n.getKind()==kind::APPLY_UF ){ Node op = n.getOperator(); + TypeNode tn_op = op.getType(); if( d_op_return_types.find( op )==d_op_return_types.end() ){ if( n.getType().isBoolean() ){ //use booleans @@ -387,7 +398,17 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ } for( size_t i=0; i<n.getNumChildren(); i++ ){ //the argument of the operator must match the return type of the subterm - setEqual( child_types[i], d_op_arg_types[op][i] ); + if( n[i].getType()!=tn_op[i] ){ + //if type mismatch, assume original types + Trace("sort-inference-debug") << "Argument " << i << " of " << op << " " << n[i] << " has type " << n[i].getType(); + Trace("sort-inference-debug") << ", while operator arg has type " << tn_op[i] << std::endl; + int ct1 = getIdForType( n[i].getType() ); + setEqual( child_types[i], ct1 ); + int ct2 = getIdForType( tn_op[i] ); + setEqual( d_op_arg_types[op][i], ct2 ); + }else{ + setEqual( child_types[i], d_op_arg_types[op][i] ); + } } //return type is the return type retType = d_op_return_types[op]; |