diff options
44 files changed, 303 insertions, 201 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index cbef7109f..867feef6e 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -425,6 +425,24 @@ all \n\ \n\ "; +const std::string OptionsHandler::s_cegqiSingleInvHelp = "\ +Modes for single invocation techniques, supported by --cegqi-si:\n\ +\n\ +none \n\ ++ Do not use single invocation techniques.\n\ +\n\ +use (default) \n\ ++ Use single invocation techniques only if grammar is not restrictive.\n\ +\n\ +all-abort \n\ ++ Always use single invocation techniques, abort if solution reconstruction will likely fail,\ + for instance, when the grammar does not have ITE and solution requires it.\n\ +\n\ +all \n\ ++ Always use single invocation techniques. \n\ +\n\ +"; + const std::string OptionsHandler::s_sygusInvTemplHelp = "\ Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ \n\ @@ -700,6 +718,24 @@ theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(s } } +theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none" ) { + return theory::quantifiers::CEGQI_SI_MODE_NONE; + } else if(optarg == "use" || optarg == "default") { + return theory::quantifiers::CEGQI_SI_MODE_USE; + } else if(optarg == "all-abort") { + return theory::quantifiers::CEGQI_SI_MODE_ALL_ABORT; + } else if(optarg == "all") { + return theory::quantifiers::CEGQI_SI_MODE_ALL; + } else if(optarg == "help") { + puts(s_cegqiSingleInvHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --cegqi-si: `") + + optarg + "'. Try --cegqi-si help."); + } +} + theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) { if(optarg == "none" ) { return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE; diff --git a/src/options/options_handler.h b/src/options/options_handler.h index baa6cea96..8f23219eb 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -98,6 +98,7 @@ public: theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); + theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException); @@ -209,6 +210,7 @@ public: static const std::string s_qcfModeHelp; static const std::string s_qcfWhenModeHelp; static const std::string s_simplificationHelp; + static const std::string s_cegqiSingleInvHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_termDbModeHelp; static const std::string s_theoryOfModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 38308c9dc..65445be17 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -153,6 +153,17 @@ enum IteLiftQuantMode { ITE_LIFT_QUANT_MODE_ALL, }; +enum CegqiSingleInvMode { + /** do not use single invocation techniques */ + CEGQI_SI_MODE_NONE, + /** use single invocation techniques */ + CEGQI_SI_MODE_USE, + /** always use single invocation techniques, abort if solution reconstruction will fail */ + CEGQI_SI_MODE_ALL_ABORT, + /** always use single invocation techniques */ + CEGQI_SI_MODE_ALL, +}; + enum SygusInvTemplMode { /** synthesize I( x ) */ SYGUS_INV_TEMPL_MODE_NONE, diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 227540f45..456ab04c2 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -109,6 +109,9 @@ option instLevelInputOnly --inst-level-input-only bool :default true only input terms are assigned instantiation level zero option quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode selection mode for representatives in quantifiers engine +option instRelevantCond --inst-rlv-cond bool :default false + add relevancy conditions for instantiations + option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly @@ -229,8 +232,8 @@ option ceGuidedInst --cegqi bool :default false :read-write counterexample-guided quantifier instantiation option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler stringToCegqiFairMode if and how to apply fairness for cegqi -option cegqiSingleInv --cegqi-si bool :default false :read-write - process single invocation synthesis conjectures +option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write + mode for processing single invocation synthesis conjectures option cegqiSingleInvPartial --cegqi-si-partial bool :default false combined techniques for synthesis conjectures that are partially single invocation option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true @@ -239,8 +242,6 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default include constants when reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvAbort --cegqi-si-abort bool :default false 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 54deba78c..62afbf987 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1737,6 +1737,10 @@ void SmtEngine::setDefaults() { options::instMaxLevel.set( 0 ); } } + if( options::instMaxLevel()!=-1 ){ + Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl; + options::cbqi.set(false); + } if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) { options::fmfBoundInt.set( true ); @@ -1797,13 +1801,15 @@ void SmtEngine::setDefaults() { } //apply counterexample guided instantiation options - if( options::cegqiSingleInv() ){ - options::ceGuidedInst.set( true ); + if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){ + if( !options::ceGuidedInst.wasSetByUser() ){ + options::ceGuidedInst.set( true ); + } } if( options::ceGuidedInst() ){ //counterexample-guided instantiation for sygus - if( !options::cegqiSingleInv.wasSetByUser() ){ - options::cegqiSingleInv.set( true ); + if( !options::cegqiSingleInvMode.wasSetByUser() ){ + options::cegqiSingleInvMode.set( quantifiers::CEGQI_SI_MODE_USE ); } if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 8af11b1af..71bf7c426 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -48,7 +48,7 @@ void CegConjecture::assign( Node q ) { Assert( q.getKind()==FORALL ); d_assert_quant = q; //register with single invocation if applicable - if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){ + if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ){ d_ceg_si->initialize( q ); if( q!=d_ceg_si->d_quant ){ //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant ); diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index a5d4174dd..3177739ac 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -111,6 +111,7 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems void CegConjectureSingleInv::initialize( Node q ) { Assert( d_quant.isNull() ); + Assert( options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ); //initialize data d_quant = q; //process @@ -121,6 +122,7 @@ void CegConjectureSingleInv::initialize( Node q ) { std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke; std::vector< Node > progs; std::map< Node, std::map< Node, bool > > contains; + bool is_syntax_restricted = false; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ progs.push_back( q[0][i] ); //check whether all types have ITE @@ -131,161 +133,173 @@ void CegConjectureSingleInv::initialize( Node q ) { d_has_ites = false; } } + Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isSygus() ); + if( !dt.getSygusAllowAll() ){ + is_syntax_restricted = true; + } } - Node qq = q[1]; - if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){ - qq = q[1][0][1]; - }else{ - qq = TermDb::simpleNegate( qq ); - } - //remove the deep embedding - std::map< Node, Node > visited; - std::vector< TypeNode > types; - std::vector< Node > order_vars; - std::map< Node, Node > single_inv_app_map; - int type_valid = 0; - qq = removeDeepEmbedding( qq, progs, types, type_valid, visited ); - Trace("cegqi-si-debug") << "- Remove deep embedding, got : " << qq << ", type valid = " << type_valid << std::endl; + //abort if not aggressive bool singleInvocation = true; - if( type_valid==0 ){ - //process the single invocation-ness of the property - d_sip->init( types, qq ); - Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; - d_sip->debugPrint( "cegqi-si" ); - //map from program to bound variables - for( unsigned j=0; j<progs.size(); j++ ){ - Node prog = progs[j]; - std::map< Node, Node >::iterator it_nsi = d_nsi_op_map.find( prog ); - if( it_nsi!=d_nsi_op_map.end() ){ - Node op = it_nsi->second; - std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( op ); - if( it_fov!=d_sip->d_func_fo_var.end() ){ - Node pv = it_fov->second; - Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() ); - Node inv = d_sip->d_func_inv[op]; - single_inv_app_map[prog] = inv; - Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl; - d_prog_to_sol_index[prog] = order_vars.size(); - order_vars.push_back( pv ); + if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && is_syntax_restricted ){ + singleInvocation = false; + Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl; + }else{ + Node qq = q[1]; + if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){ + qq = q[1][0][1]; + }else{ + qq = TermDb::simpleNegate( qq ); + } + //remove the deep embedding + std::map< Node, Node > visited; + std::vector< TypeNode > types; + std::vector< Node > order_vars; + std::map< Node, Node > single_inv_app_map; + int type_valid = 0; + qq = removeDeepEmbedding( qq, progs, types, type_valid, visited ); + Trace("cegqi-si-debug") << "- Remove deep embedding, got : " << qq << ", type valid = " << type_valid << std::endl; + if( type_valid==0 ){ + //process the single invocation-ness of the property + d_sip->init( types, qq ); + Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; + d_sip->debugPrint( "cegqi-si" ); + //map from program to bound variables + for( unsigned j=0; j<progs.size(); j++ ){ + Node prog = progs[j]; + std::map< Node, Node >::iterator it_nsi = d_nsi_op_map.find( prog ); + if( it_nsi!=d_nsi_op_map.end() ){ + Node op = it_nsi->second; + std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( op ); + if( it_fov!=d_sip->d_func_fo_var.end() ){ + Node pv = it_fov->second; + Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() ); + Node inv = d_sip->d_func_inv[op]; + single_inv_app_map[prog] = inv; + Trace("cegqi-si") << " " << pv << ", " << inv << " is associated with program " << prog << std::endl; + d_prog_to_sol_index[prog] = order_vars.size(); + order_vars.push_back( pv ); + } + }else{ + //does not mention the function } - }else{ - //does not mention the function } - } - //reorder the variables - Assert( d_sip->d_func_vars.size()==order_vars.size() ); - d_sip->d_func_vars.clear(); - d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() ); + //reorder the variables + Assert( d_sip->d_func_vars.size()==order_vars.size() ); + d_sip->d_func_vars.clear(); + d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() ); - //check if it is single invocation - if( !d_sip->d_conjuncts[1].empty() ){ - singleInvocation = false; - if( options::cegqiSingleInvPartial() ){ - //this enables partially single invocation techniques - d_nsingle_inv = d_sip->getNonSingleInvocation(); - d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv ); - d_full_inv = d_sip->getFullSpecification(); - d_full_inv = TermDb::simpleNegate( d_full_inv ); - singleInvocation = true; - }else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ - //if we are doing invariant templates, then construct the template - std::map< Node, bool > has_inv; - std::map< Node, std::vector< Node > > inv_pre_post[2]; - for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){ - std::vector< Node > disjuncts; - Node func; - int pol = -1; - Trace("cegqi-inv") << "INV process " << d_sip->d_conjuncts[2][i] << std::endl; - d_sip->extractInvariant( d_sip->d_conjuncts[2][i], func, pol, disjuncts ); - if( pol>=0 ){ - Assert( d_nsi_op_map_to_prog.find( func )!=d_nsi_op_map_to_prog.end() ); - Node prog = d_nsi_op_map_to_prog[func]; - Trace("cegqi-inv") << "..." << ( pol==0 ? "pre" : "post" ) << "-condition for " << prog << "." << std::endl; - Node c = disjuncts.empty() ? d_qe->getTermDatabase()->d_false : ( disjuncts.size()==1 ? disjuncts[0] : NodeManager::currentNM()->mkNode( OR, disjuncts ) ); - c = pol==0 ? TermDb::simpleNegate( c ) : c; - Trace("cegqi-inv-debug") << "...extracted : " << c << std::endl; - inv_pre_post[pol][prog].push_back( c ); - has_inv[prog] = true; - }else{ - Trace("cegqi-inv") << "...no status." << std::endl; + //check if it is single invocation + if( !d_sip->d_conjuncts[1].empty() ){ + singleInvocation = false; + if( options::cegqiSingleInvPartial() ){ + //this enables partially single invocation techniques + d_nsingle_inv = d_sip->getNonSingleInvocation(); + d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv ); + d_full_inv = d_sip->getFullSpecification(); + d_full_inv = TermDb::simpleNegate( d_full_inv ); + singleInvocation = true; + }else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ + //if we are doing invariant templates, then construct the template + std::map< Node, bool > has_inv; + std::map< Node, std::vector< Node > > inv_pre_post[2]; + for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){ + std::vector< Node > disjuncts; + Node func; + int pol = -1; + Trace("cegqi-inv") << "INV process " << d_sip->d_conjuncts[2][i] << std::endl; + d_sip->extractInvariant( d_sip->d_conjuncts[2][i], func, pol, disjuncts ); + if( pol>=0 ){ + Assert( d_nsi_op_map_to_prog.find( func )!=d_nsi_op_map_to_prog.end() ); + Node prog = d_nsi_op_map_to_prog[func]; + Trace("cegqi-inv") << "..." << ( pol==0 ? "pre" : "post" ) << "-condition for " << prog << "." << std::endl; + Node c = disjuncts.empty() ? d_qe->getTermDatabase()->d_false : ( disjuncts.size()==1 ? disjuncts[0] : NodeManager::currentNM()->mkNode( OR, disjuncts ) ); + c = pol==0 ? TermDb::simpleNegate( c ) : c; + Trace("cegqi-inv-debug") << "...extracted : " << c << std::endl; + inv_pre_post[pol][prog].push_back( c ); + has_inv[prog] = true; + }else{ + Trace("cegqi-inv") << "...no status." << std::endl; + } } - } - Trace("cegqi-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-inv") << "...for " << prog << "..." << std::endl; - Trace("cegqi-inv") << " args : "; + Trace("cegqi-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-inv") << "...for " << prog << "..." << std::endl; + Trace("cegqi-inv") << " args : "; + for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){ + std::stringstream ss; + ss << "i_" << j; + Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ); + d_prog_templ_vars[prog].push_back( v ); + Trace("cegqi-inv") << v << " "; + } + Trace("cegqi-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( d_sip->d_si_vars.begin(), d_sip->d_si_vars.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( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; + Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + Node invariant = single_inv_app_map[prog]; + invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Trace("cegqi-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 ); + } + visited.clear(); + templ = addDeepEmbedding( templ, visited ); + Trace("cegqi-inv") << " template : " << templ << std::endl; + prog_templ[prog] = templ; + } + Node bd = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] ); + visited.clear(); + bd = addDeepEmbedding( bd, visited ); + Trace("cegqi-inv") << " body : " << bd << std::endl; + bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars ); + Trace("cegqi-inv-debug") << " templ-subs body : " << bd << std::endl; + //make inner existential + std::vector< Node > new_var_bv; for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){ std::stringstream ss; - ss << "i_" << j; - Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ); - d_prog_templ_vars[prog].push_back( v ); - Trace("cegqi-inv") << v << " "; + ss << "ss_" << j; + new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ) ); } - Trace("cegqi-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( d_sip->d_si_vars.begin(), d_sip->d_si_vars.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( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); - Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; - Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; - Node invariant = single_inv_app_map[prog]; - invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); - Trace("cegqi-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 ); + bd = bd.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_var_bv.begin(), new_var_bv.end() ); + Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ); + for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){ + new_var_bv.push_back( q[1][0][0][j] ); } - visited.clear(); - templ = addDeepEmbedding( templ, visited ); - Trace("cegqi-inv") << " template : " << templ << std::endl; - prog_templ[prog] = templ; - } - Node bd = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] ); - visited.clear(); - bd = addDeepEmbedding( bd, visited ); - Trace("cegqi-inv") << " body : " << bd << std::endl; - bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars ); - Trace("cegqi-inv-debug") << " templ-subs body : " << bd << std::endl; - //make inner existential - std::vector< Node > new_var_bv; - for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){ - std::stringstream ss; - ss << "ss_" << j; - new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ) ); - } - bd = bd.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_var_bv.begin(), new_var_bv.end() ); - Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ); - for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){ - new_var_bv.push_back( q[1][0][0][j] ); - } - if( !new_var_bv.empty() ){ - Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv ); - bd = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ).negate(); + if( !new_var_bv.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv ); + bd = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ).negate(); + } + //make outer universal + bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd ); + bd = Rewriter::rewrite( bd ); + Trace("cegqi-inv") << " rtempl-subs body : " << bd << std::endl; + d_quant = bd; } - //make outer universal - bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd ); - bd = Rewriter::rewrite( bd ); - Trace("cegqi-inv") << " rtempl-subs body : " << bd << std::endl; - d_quant = bd; + }else{ + //we are fully single invocation } }else{ - //we are fully single invocation + Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl; + singleInvocation = false; } - }else{ - Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl; - singleInvocation = false; } if( singleInvocation ){ d_single_inv = d_sip->getSingleInvocation(); @@ -829,8 +843,8 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec } bool CegConjectureSingleInv::needsCheck() { - if( options::cegqiSingleInvMultiInstAbort() ){ - if( !hasITEs() ){ + if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_ALL_ABORT ){ + if( !d_has_ites ){ return d_inst.empty(); } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e81245034..334e42375 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1865,6 +1865,18 @@ bool TermDb::getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& c } } +void TermDb::getRelevancyCondition( Node n, std::vector< Node >& cond ) { + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr()); + const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); + Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate(); + if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){ + cond.push_back( rc ); + } + getRelevancyCondition( n[0], cond ); + } +} + bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) { if( n==t ){ return true; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index b7b798cd4..3f931014b 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -462,6 +462,8 @@ public: static Node ensureType( Node n, TypeNode tn ); /** get ensure type condition */ static bool getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond ); + /** get relevancy condition */ + static void getRelevancyCondition( Node n, std::vector< Node >& cond ); private: //helper for contains term static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8984cc5f4..ebf89c0b8 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1010,6 +1010,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Assert( !d_conflict ); Assert( terms.size()==q[0].getNumChildren() ); Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; + std::vector< Node > rlv_cond; for( unsigned i=0; i<terms.size(); i++ ){ Trace("inst-add-debug") << " " << q[0][i]; Trace("inst-add-debug2") << " -> " << terms[i]; @@ -1027,6 +1028,11 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo if( terms[i].isNull() ){ Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl; return false; + }else{ + //get relevancy conditions + if( options::instRelevantCond() ){ + quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond ); + } } #ifdef CVC4_ASSERTIONS bool bad_inst = false; @@ -1092,14 +1098,21 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; Assert( d_term_db->d_vars[q].size()==terms.size() ); Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution + Node orig_body = body; body = quantifiers::QuantifiersRewriter::preprocess( body, true ); Trace("inst-debug") << "...preprocess to " << body << std::endl; //construct the lemma Trace("inst-assert") << "(assert " << body << ")" << std::endl; - Node orig_body = body; body = Rewriter::rewrite(body); - Node lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body ); + Node lem; + if( rlv_cond.empty() ){ + lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body ); + }else{ + rlv_cond.push_back( q.negate() ); + rlv_cond.push_back( body ); + lem = NodeManager::currentNM()->mkNode( kind::OR, rlv_cond ); + } lem = Rewriter::rewrite(lem); //check for lemma duplication @@ -1120,15 +1133,20 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } } if( options::instMaxLevel()!=-1 ){ - uint64_t maxInstLevel = 0; - for( unsigned i=0; i<terms.size(); i++ ){ - if( terms[i].hasAttribute(InstLevelAttribute()) ){ - if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ - maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + if( doVts ){ + //virtual term substitution/instantiation level features are incompatible + Assert( false ); + }else{ + uint64_t maxInstLevel = 0; + for( unsigned i=0; i<terms.size(); i++ ){ + if( terms[i].hasAttribute(InstLevelAttribute()) ){ + if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ + maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + } } } + setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 ); } - setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 ); } if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){ //notify listeners diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 56a30b210..e6683ced9 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --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 f6c0320e2..387ce9487 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --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/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy index 09bdb8b4d..3519319bd 100644 --- a/test/regress/regress0/sygus/clock-inc-tuple.sy +++ b/test/regress/regress0/sygus/clock-inc-tuple.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic ALL_SUPPORTED) (declare-var m Int) diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy index 46dbd2981..f675bddad 100644 --- a/test/regress/regress0/sygus/commutative.sy +++ b/test/regress/regress0/sygus/commutative.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) @@ -19,4 +19,4 @@ (check-synth) -; (+ x y) is a valid solution
\ No newline at end of file +; (+ x y) is a valid solution diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 428cb2adc..b79b7eeec 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy index 0059f6947..5c48f5e39 100644 --- a/test/regress/regress0/sygus/constant.sy +++ b/test/regress/regress0/sygus/constant.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) @@ -20,4 +20,4 @@ (check-synth) -; 0, 1, (- x x) are valid solutions
\ No newline at end of file +; 0, 1, (- x x) are valid solutions diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy index e0f8112ce..42382ac91 100644 --- a/test/regress/regress0/sygus/dt-no-syntax.sy +++ b/test/regress/regress0/sygus/dt-no-syntax.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy index ed17f4ff2..052065061 100644 --- a/test/regress/regress0/sygus/dt-test-ns.sy +++ b/test/regress/regress0/sygus/dt-test-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy index e5448d626..bed9972fd 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --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 cd129385e..7b59f5f1a 100644 --- a/test/regress/regress0/sygus/enum-test.sy +++ b/test/regress/regress0/sygus/enum-test.sy @@ -1,8 +1,8 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (define-sort D (Enum (a b))) (define-fun f ((x D)) Int (ite (= x D::a) 3 7)) (synth-fun g () D ((Start D (D::a D::b)))) (constraint (= (f g) 7)) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/hd-sdiv.sy b/test/regress/regress0/sygus/hd-sdiv.sy index 3ac9334b2..019b48a1c 100644 --- a/test/regress/regress0/sygus/hd-sdiv.sy +++ b/test/regress/regress0/sygus/hd-sdiv.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --no-dump-synth (set-logic BV) (define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001)) diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy index b07be0e98..74e054159 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 --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic BV) diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy index aafbbd987..b56425964 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 --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) (declare-primed-var x Int) @@ -9,4 +9,4 @@ (define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12))))) (define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x)) (inv-constraint inv-f pre-f trans-f post-f) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 4bae90b00..d5d40ace4 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --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 71cd27e8f..d07f6a717 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int ((Start Int (x diff --git a/test/regress/regress0/sygus/list-head-x.sy b/test/regress/regress0/sygus/list-head-x.sy index a5977d1e7..21362dc2c 100644 --- a/test/regress/regress0/sygus/list-head-x.sy +++ b/test/regress/regress0/sygus/list-head-x.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic ALL_SUPPORTED) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index dec4594d7..e6e3de5fc 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy index 3f8aac3b2..927148d81 100644 --- a/test/regress/regress0/sygus/max2-univ.sy +++ b/test/regress/regress0/sygus/max2-univ.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes) (set-logic LIA) (synth-fun max2 ((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 6d185ba3f..c238de5dd 100644 --- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy +++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) @@ -32,4 +32,4 @@ (check-synth) -; (x, y), (x-y, 0) ... are valid solutions
\ No newline at end of file +; (x, y), (x-y, 0) ... are valid solutions diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy index 9065a1025..d3624a731 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 --no-dump-synth +; COMMAND-LINE: --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 d211d475b..3f15d5915 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 --no-dump-synth +; COMMAND-LINE: --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 cb284b180..af1284f13 100644 --- 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 --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-mention.sy b/test/regress/regress0/sygus/no-mention.sy index 05dfbced3..60efc1b74 100644 --- a/test/regress/regress0/sygus/no-mention.sy +++ b/test/regress/regress0/sygus/no-mention.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-fun p ((x Int) (y Int)) Int) diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy index 4b3fa22e6..ee27b30eb 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 --no-dump-synth +; COMMAND-LINE: --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 86b60638b..bd8da1900 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 --no-dump-synth +; COMMAND-LINE: --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 b95f31aa7..2b3d5f3e9 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 --no-dump-synth +; COMMAND-LINE: --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 03d180634..3cc577bd8 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool @@ -27,4 +27,4 @@ ;(not ; (and ; (and (not (and (not a) b)) (not (and d (not c)))) -; (and (not (and (not b) a)) (not (and (not d) c))))))
\ No newline at end of file +; (and (not (and (not b) a)) (not (and (not d) c)))))) diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy index bc559f94a..40346bcdf 100644 --- a/test/regress/regress0/sygus/strings-small.sy +++ b/test/regress/regress0/sygus/strings-small.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic SLIA) (synth-fun f ((firstname String) (lastname String)) String ((Start String (ntString)) diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy index e842477e8..be6749139 100644 --- a/test/regress/regress0/sygus/sygus-dt.sy +++ b/test/regress/regress0/sygus/sygus-dt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) @@ -13,4 +13,4 @@ (declare-var x Int) (constraint (= (f x) (cons x nil))) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy index 1545f86cd..a6980425a 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=none --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 7f84ce06c..b016872b4 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 --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) ;; f1 is x plus 2 ;; f2 is 2x plus 5 diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy index 91bab5ece..70d1ffa02 100644 --- a/test/regress/regress0/sygus/twolets2-orig.sy +++ b/test/regress/regress0/sygus/twolets2-orig.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (synth-fun f1 ((x Int)) Int ( diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy index 9886f6a7b..e98be942b 100644 --- a/test/regress/regress0/sygus/uminus_one.sy +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((- 1))))) (declare-var x Int) (constraint (= (f x) (- 1))) -(check-synth)
\ No newline at end of file +(check-synth) diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy index 7c9d6c601..300b6b65c 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 --no-dump-synth +; COMMAND-LINE: --no-dump-synth (set-logic LIA) (synth-fun inv ((x Int)) Bool |