diff options
39 files changed, 498 insertions, 187 deletions
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/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b8c4793d4..9ee6d24b4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -517,7 +517,7 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin 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(); @@ -525,13 +525,13 @@ void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::strin types.push_back( t ); } } - + //name of boolean sort std::stringstream ssb; ssb << fun << "_Bool"; std::string dbname = ssb.str(); Type unres_bt = mkUnresolvedType(ssb.str()); - + std::vector< Type > unres_types; for( unsigned i=0; i<types.size(); i++ ){ std::stringstream ss; @@ -700,7 +700,7 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& o // 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, +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, @@ -708,14 +708,37 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, 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, + std::vector<CVC4::Expr>& sygus_vars, + std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, CVC4::Type& ret, bool isNested ){ if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){ Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl; - //convert to UMINUS if one child of - + 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) ){ - sgt.d_expr = getExprManager()->operatorOf(kind::UMINUS); + 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 ); @@ -730,16 +753,16 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, 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, + 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, + 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, + 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 ){ @@ -790,7 +813,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, unresolved_gterm_sym[index].push_back(sgt.d_name); } }else if( sgt.d_gterm_type==SygusGTerm::gterm_ignore ){ - + } } @@ -828,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, @@ -836,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 "; @@ -907,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 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; @@ -953,30 +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; @@ -997,12 +1020,12 @@ 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, +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 ) { @@ -1093,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; @@ -1149,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; @@ -1206,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, 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 921583ed2..fa145813c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1465,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() ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 045407bf0..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 ); @@ -211,7 +219,7 @@ 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; } } @@ -229,7 +237,7 @@ Node CegInstantiation::getNextDecisionRequest() { 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 ) ) { @@ -251,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++ ){ @@ -263,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 ); @@ -303,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() ); @@ -334,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 ); @@ -497,11 +507,12 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { // 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() ); @@ -514,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")) ){ diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 5f393626c..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; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index b7bbf8a93..ef2e3005e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -810,6 +810,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { } //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 @@ -826,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]; @@ -840,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() ); @@ -868,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]; @@ -897,7 +910,6 @@ 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; Node pbvl; if( !pbvs.empty() ){ pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); @@ -906,6 +918,8 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { //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; @@ -917,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; } @@ -941,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; @@ -948,75 +981,163 @@ 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 ); - 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; + 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; + } } } + */ } - */ } } } @@ -1146,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 ) ){ @@ -1371,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; @@ -1429,4 +1612,5 @@ bool CegConjectureSingleInv::needsCheck() { 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 f8e3879ac..f0d00b61c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -111,6 +111,9 @@ 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 ); @@ -141,7 +144,7 @@ private: public: //lemmas produced std::vector< Node > d_lemmas_produced; - std::vector< std::vector< Node > > d_inst; + std::vector< std::vector< Node > > d_inst; private: std::vector< Node > d_curr_lemmas; //add instantiation @@ -156,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 ); @@ -165,6 +172,8 @@ 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 diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 97ad3e8ea..af2d88e94 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -152,6 +152,15 @@ typedef enum { 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 ab0526471..5cb9062e4 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -32,7 +32,7 @@ option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuan 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 iteDtTesterSplitQuant --ite-dtt-split-quant bool :default false +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 @@ -240,6 +240,9 @@ 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 +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 diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index c518813a0..4d2276621 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -217,6 +217,19 @@ 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") { @@ -443,6 +456,22 @@ inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string } } +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/term_database.cpp b/src/theory/quantifiers/term_database.cpp index fa0e211b3..c6115195d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -781,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 ]); } @@ -1754,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() ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ccbbd5bd5..54f2a16fe 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -754,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 ); } diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 5d8cd8752..56a30b210 100644 --- a/test/regress/regress0/sygus/array_search_2.sy +++ b/test/regress/regress0/sygus/array_search_2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy index 48b5c8a4d..f6c0320e2 100644 --- a/test/regress/regress0/sygus/array_sum_2_5.sy +++ b/test/regress/regress0/sygus/array_sum_2_5.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy index 15567b0a8..46dbd2981 100644 --- a/test/regress/regress0/sygus/commutative.sy +++ b/test/regress/regress0/sygus/commutative.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 0d753bdf1..428cb2adc 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy index ddc12a6a9..0059f6947 100644 --- a/test/regress/regress0/sygus/constant.sy +++ b/test/regress/regress0/sygus/constant.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy index dbf415986..e5448d626 100644 --- a/test/regress/regress0/sygus/dup-op.sy +++ b/test/regress/regress0/sygus/dup-op.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si +; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ Start Start) x)) diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy index 52a72c07d..cd129385e 100644 --- a/test/regress/regress0/sygus/enum-test.sy +++ b/test/regress/regress0/sygus/enum-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (define-sort D (Enum (a b))) (define-fun f ((x D)) Int (ite (= x D::a) 3 7)) diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy index a58bc2f64..2e6c6ef81 100644 --- a/test/regress/regress0/sygus/hd-01-d1-prog.sy +++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic BV) @@ -8,12 +8,12 @@ (synth-fun f ((x (BitVec 32))) (BitVec 32) ((Start (BitVec 32) ((bvand Start Start) (bvsub Start Start) - (bvor Start Start) - (bvadd Start Start) - (bvxor Start Start) + (bvor Start Start) + (bvadd Start Start) + (bvxor Start Start) x - #x00000000 - #xFFFFFFFF + #x00000000 + #xFFFFFFFF #x00000001)))) (declare-var x (BitVec 32)) diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy index 6e1610337..b07be0e98 100644 --- a/test/regress/regress0/sygus/icfp_28_10.sy +++ b/test/regress/regress0/sygus/icfp_28_10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic BV) @@ -14,14 +14,14 @@ (Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) (shl1 Start) - (shr1 Start) - (shr4 Start) - (shr16 Start) - (bvand Start Start) - (bvor Start Start) - (bvxor Start Start) - (bvadd Start Start) - (if0 Start Start Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) )) ) ) diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy index dda8e0ed5..aafbbd987 100644 --- a/test/regress/regress0/sygus/inv-example.sy +++ b/test/regress/regress0/sygus/inv-example.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) (declare-primed-var x Int) diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 046d074d9..4bae90b00 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (synth-fun f ((x Int)) Int diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index daca906a2..71cd27e8f 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int ((Start Int (x diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index 4fc515353..dec4594d7 100644 --- a/test/regress/regress0/sygus/max.sy +++ b/test/regress/regress0/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy index 24d49ee4e..6d185ba3f 100644 --- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy +++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy @@ -1,13 +1,13 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun addExpr1 ((x Int) (y Int)) Int ((Start Int (x y - 0 - 1 + 0 + 1 (+ Start Start) (- Start Start) )) @@ -16,8 +16,8 @@ (synth-fun addExpr2 ((x Int) (y Int)) Int ((Start Int (x y - 0 - 1 + 0 + 1 (+ Start Start) (- Start Start) )) diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy index bd7c79e3e..9065a1025 100644 --- a/test/regress/regress0/sygus/nflat-fwd-3.sy +++ b/test/regress/regress0/sygus/nflat-fwd-3.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ (+ Con Con) Con) x)) diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy index 0f9d46215..d211d475b 100644 --- a/test/regress/regress0/sygus/nflat-fwd.sy +++ b/test/regress/regress0/sygus/nflat-fwd.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x)) diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy index 81f90e2aa..cb284b180 100755 --- a/test/regress/regress0/sygus/no-flat-simp.sy +++ b/test/regress/regress0/sygus/no-flat-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy index cc3855ad1..4b3fa22e6 100644 --- a/test/regress/regress0/sygus/no-syntax-test-bool.sy +++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy index 21788426c..86b60638b 100644 --- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy +++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy index 95f9b7c11..b95f31aa7 100644 --- a/test/regress/regress0/sygus/no-syntax-test.sy +++ b/test/regress/regress0/sygus/no-syntax-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy index c4fbd1c17..03d180634 100644 --- a/test/regress/regress0/sygus/parity-AIG-d0.sy +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy index a8da13742..1545f86cd 100644 --- a/test/regress/regress0/sygus/tl-type.sy +++ b/test/regress/regress0/sygus/tl-type.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si +; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int (Term (+ Start Start))) diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy index 24b0f2c09..7f84ce06c 100644 --- a/test/regress/regress0/sygus/twolets1.sy +++ b/test/regress/regress0/sygus/twolets1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) ;; f1 is x plus 2 ;; f2 is 2x plus 5 @@ -7,27 +7,27 @@ (define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) (synth-fun f1 ((x Int)) Int - ( - (Start Int ( - (let0 Intx CInt CInt) - ) - ) - (Intx Int (x)) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - - ) + ( + (Start Int ( + (let0 Intx CInt CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) ) (synth-fun f2 ((x Int)) Int - ( - (Start Int (x - (let0 Intx Start CInt) - ) - ) + ( + (Start Int (x + (let0 Intx Start CInt) + ) + ) (Intx Int (x)) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy index c1066277e..91bab5ece 100644 --- a/test/regress/regress0/sygus/twolets2-orig.sy +++ b/test/regress/regress0/sygus/twolets2-orig.sy @@ -1,25 +1,25 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f1 ((x Int)) Int - ( - (Start Int ( - (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) - ) - ) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + ( + (Start Int ( + (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) (synth-fun f2 ((x Int)) Int - ( - (Start Int (x - (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) - ) - ) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + ( + (Start Int (x + (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) (declare-var x1 Int) (declare-var x2 Int) diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy index b020c0bee..9886f6a7b 100644 --- a/test/regress/regress0/sygus/uminus_one.sy +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((- 1))))) (declare-var x Int) diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy index dc39efd84..7c9d6c601 100644 --- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy +++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun inv ((x Int)) Bool |