From f58c881034d3b0193dfee8fabf451cc0e9ea20ab Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 15 May 2016 12:34:51 -0500 Subject: [PATCH] Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable e-matching when --strings-exp is enabled. --- contrib/run-script-cascj8-fof | 19 +-- contrib/run-script-cascj8-tfa | 8 +- src/options/options_handler.cpp | 4 +- src/options/quantifiers_modes.h | 2 + src/options/quantifiers_options | 6 +- src/parser/smt2/Smt2.g | 4 + src/smt/smt_engine.cpp | 5 +- src/theory/datatypes/kinds | 2 +- .../datatypes/theory_datatypes_type_rules.h | 3 +- .../quantifiers/ce_guided_instantiation.cpp | 128 ++++++++++++---- .../quantifiers/ce_guided_instantiation.h | 5 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 6 +- .../quantifiers/quant_conflict_find.cpp | 116 ++++---------- src/theory/quantifiers/term_database.cpp | 143 ++++++++++++++---- src/theory/quantifiers/term_database.h | 20 ++- src/theory/quantifiers/theory_quantifiers.cpp | 7 +- src/theory/quantifiers_engine.h | 2 +- 17 files changed, 308 insertions(+), 172 deletions(-) diff --git a/contrib/run-script-cascj8-fof b/contrib/run-script-cascj8-fof index f8d79b1de..fe18c3ed0 100644 --- a/contrib/run-script-cascj8-fof +++ b/contrib/run-script-cascj8-fof @@ -30,18 +30,19 @@ function finishwith { } # designed for 300 seconds -trywith 20 --relevant-triggers --full-saturate-quant +trywith 20 --relational-triggers --full-saturate-quant trywith 20 --no-e-matching --full-saturate-quant -trywith 20 --finite-model-find --mbqi=abs +trywith 15 --finite-model-find --mbqi=abs trywith 5 --multi-trigger-when-single --full-saturate-quant trywith 5 --trigger-sel=max --full-saturate-quant -trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant -trywith 5 --relational-triggers --full-saturate-quant -trywith 15 --term-db-mode=relevant --full-saturate-quant -trywith 15 --pre-quant=none --full-saturate-quant -trywith 15 --finite-model-find --uf-ss=no-minimal -trywith 30 --decision=internal --full-saturate-quant +trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant +trywith 10 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair +trywith 10 --term-db-mode=relevant --full-saturate-quant +trywith 15 --prenex-quant=none --full-saturate-quant +trywith 15 --decision=internal --full-saturate-quant +trywith 30 --relevant-triggers --full-saturate-quant +trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair trywith 30 --fs-inst --full-saturate-quant trywith 30 --no-quant-cf --full-saturate-quant -finishwith --relational-triggers --full-saturate-quant +finishwith --qcf-vo-exp --full-saturate-quant # echo "% SZS status" "GaveUp for $filename" diff --git a/contrib/run-script-cascj8-tfa b/contrib/run-script-cascj8-tfa index a7a97a44d..da4056466 100644 --- a/contrib/run-script-cascj8-tfa +++ b/contrib/run-script-cascj8-tfa @@ -31,10 +31,10 @@ function finishwith { trywith 10 --decision=internal --full-saturate-quant trywith 10 --finite-model-find --decision=internal -trywith 10 ---purify-quant --full-saturate-quant -trywith 10 ---partial-triggers --full-saturate-quant -trywith 10 ---no-e-matching --full-saturate-quant +trywith 10 --purify-quant --full-saturate-quant +trywith 10 --partial-triggers --full-saturate-quant +trywith 10 --no-e-matching --full-saturate-quant trywith 30 --cbqi-all --purify-triggers --full-saturate-quant -trywith 60 --cbqi-all ---fs-inst --full-saturate-quant +trywith 60 --cbqi-all --fs-inst --full-saturate-quant finishwith --full-saturate-quant # echo "% SZS status" "GaveUp for $filename" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 7d41ae862..cbef7109f 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -390,7 +390,7 @@ uf-dt-size \n\ + Enforce fairness using an uninterpreted function for datatypes size.\n\ \n\ default | dt-size \n\ -+ Default, enforce fairness using size theory operator.\n\ ++ Default, enforce fairness using size operator.\n\ \n\ dt-height-bound \n\ + Enforce fairness by height bound predicate.\n\ @@ -657,6 +657,8 @@ theory::quantifiers::CegqiFairMode OptionsHandler::stringToCegqiFairMode(std::st return theory::quantifiers::CEGQI_FAIR_DT_SIZE; } else if(optarg == "dt-height-bound" ){ return theory::quantifiers::CEGQI_FAIR_DT_HEIGHT_PRED; + //} else if(optarg == "dt-size-bound" ){ + // return theory::quantifiers::CEGQI_FAIR_DT_SIZE_PRED; } else if(optarg == "none") { return theory::quantifiers::CEGQI_FAIR_NONE; } else if(optarg == "help") { diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index b4b9abdaf..38308c9dc 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -131,6 +131,8 @@ enum CegqiFairMode { CEGQI_FAIR_DT_SIZE, /** enforce fairness by datatypes height bound */ CEGQI_FAIR_DT_HEIGHT_PRED, + /** enforce fairness by datatypes size bound */ + CEGQI_FAIR_DT_SIZE_PRED, /** do not use fair strategy for CEGQI */ CEGQI_FAIR_NONE, }; diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 19d6885b7..34f399f45 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -144,7 +144,7 @@ option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default fa option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false only add instantiations for one quantifier per round for mbqi -option fmfInstEngine --fmf-inst-engine bool :default false +option fmfInstEngine --fmf-inst-engine bool :default false :read-write use instantiation engine in conjunction with finite model finding option fmfInstGen --fmf-inst-gen bool :default true enable Inst-Gen instantiation techniques for finite model finding @@ -258,8 +258,8 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToSygusInvTemplMode template mode for sygus invariant synthesis -option sygusEagerUnfold --sygus-eager-unfold bool :default false - eager unfold evaluation functions +option sygusDirectEval --sygus-direct-eval bool :default false + direct unfolding of evaluation functions # approach applied to general quantified formulas option cbqiSplx --cbqi-splx bool :read-write :default false diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 78975bbe6..41428ed89 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -802,6 +802,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] //since we enforce satisfaction completeness, immediately convert to total version if( k==CVC4::kind::BITVECTOR_UDIV ){ k = CVC4::kind::BITVECTOR_UDIV_TOTAL; + }else if( k==CVC4::kind::BITVECTOR_UREM ){ + k = CVC4::kind::BITVECTOR_UREM_TOTAL; } sgt.d_name = kind::kindToString(k); sgt.d_gterm_type = SygusGTerm::gterm_op; @@ -837,6 +839,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] k = PARSER_STATE->getOperatorKind(name); if( k==CVC4::kind::BITVECTOR_UDIV ){ k = CVC4::kind::BITVECTOR_UDIV_TOTAL; + }else if( k==CVC4::kind::BITVECTOR_UREM ){ + k = CVC4::kind::BITVECTOR_UREM_TOTAL; } sgt.d_name = kind::kindToString(k); sgt.d_gterm_type = SygusGTerm::gterm_op; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3a138e4b7..54deba78c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1343,6 +1343,10 @@ void SmtEngine::setDefaults() { options::fmfBoundInt.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } + if(! options::fmfInstEngine.wasSetByUser()) { + options::fmfInstEngine.set( true ); + Trace("smt") << "turning on fmf-inst-engine, for strings-exp" << std::endl; + } /* if(! options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); @@ -3895,7 +3899,6 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - dumpAssertions("pre-constrain-subtypes", d_assertions); { // Any variables of subtype types need to be constrained properly. diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index d035f0fa7..3338e5f31 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -105,7 +105,7 @@ typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule operator DT_SIZE 1 "datatypes size" typerule DT_SIZE ::CVC4::theory::datatypes::DtSizeTypeRule -operator DT_HEIGHT_BOUND 1 "datatypes height bound" +operator DT_HEIGHT_BOUND 2 "datatypes height bound" typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule endtheory diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 5a3645691..9c8387958 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -299,11 +299,10 @@ public: throw TypeCheckingExceptionPrivate(n, "datatype height bound must be non-negative"); } } - return nodeManager->integerType(); + return nodeManager->booleanType(); } };/* class DtHeightBoundTypeRule */ - }/* CVC4::theory::datatypes namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index ad900ee82..cae3e730e 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -131,14 +131,18 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { qe->getOutputChannel().lemma( lem ); qe->getOutputChannel().requirePhase( lit, true ); - if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){ + if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){ //implies height bounds on each candidate variable std::vector< Node > lem_c; for( unsigned j=0; jmkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) ); + if( getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){ + lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) ); + }else{ + //lem_c.push_back( NodeManager::currentNM()->mkNode( DT_SIZE_BOUND, d_candidates[j], c ) ); + } } Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) ); - Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (dt-height-pred) : " << hlem << std::endl; + Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (pred) : " << hlem << std::endl; qe->getOutputChannel().lemma( hlem ); } return lit; @@ -258,8 +262,28 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { } } +void CegInstantiation::preRegisterQuantifier( Node q ) { + if( options::sygusDirectEval() ){ + if( q.getNumChildren()==3 && q[2].getKind()==INST_PATTERN_LIST && q[2][0].getKind()==INST_PATTERN ){ + //check whether it is an evaluation axiom + Node pat = q[2][0][0]; + if( pat.getKind()==APPLY_UF ){ + TypeNode tn = pat[0].getType(); + if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isSygus() ){ + //take ownership of this quantified formula (will use direct evaluation instead of instantiation) + d_quantEngine->setOwner( q, this ); + d_eval_axioms[q] = true; + } + } + } + } + } +} + void CegInstantiation::registerQuantifier( Node q ) { - if( d_quantEngine->getOwner( q )==this ){ + if( d_quantEngine->getOwner( q )==this && d_eval_axioms.find( q )==d_eval_axioms.end() ){ if( !d_conj->isAssigned() ){ Trace("cegqi") << "Register conjecture : " << q << std::endl; d_conj->assign( q ); @@ -279,7 +303,7 @@ void CegInstantiation::registerQuantifier( Node q ) { if( it!=d_uf_measure.end() ){ mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) ); } - }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED ){ + }else if( d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_HEIGHT_PRED || d_conj->getCegqiFairMode()==CEGQI_FAIR_DT_SIZE_PRED ){ //measure term is a fresh constant mc.push_back( NodeManager::currentNM()->mkSkolem( "K", NodeManager::currentNM()->integerType() ) ); } @@ -353,6 +377,11 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-engine-debug") << conj->d_candidates[i] << " "; } Trace("cegqi-engine-debug") << std::endl; + Trace("cegqi-engine-debug") << " * Candidate ce skolems : "; + for( unsigned i=0; id_ce_sk.size(); i++ ){ + Trace("cegqi-engine-debug") << conj->d_ce_sk[i] << " "; + } + Trace("cegqi-engine-debug") << std::endl; if( conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ Trace("cegqi-engine") << " * Current term size : " << conj->d_curr_lit.get() << std::endl; } @@ -377,6 +406,19 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } std::vector< Node > model_values; if( getModelValues( conj, conj->d_candidates, model_values ) ){ + if( options::sygusDirectEval() ){ + std::vector< Node > eager_eval_lem; + for( unsigned j=0; jd_candidates.size(); j++ ){ + d_quantEngine->getTermDatabaseSygus()->registerModelValue( conj->d_candidates[j], model_values[j], eager_eval_lem ); + } + if( !eager_eval_lem.empty() ){ + for( unsigned j=0; jaddLemma( eager_eval_lem[j] ); + } + return; + } + } //check if we must apply fairness lemmas if( conj->getCegqiFairMode()==CEGQI_FAIR_UF_DT_SIZE ){ std::vector< Node > lems; @@ -425,18 +467,28 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Node lem = NodeManager::currentNM()->mkNode( OR, ic ); lem = Rewriter::rewrite( lem ); d_last_inst_si = false; + //eagerly unfold applications of evaluation function + if( options::sygusDirectEval() ){ + Trace("cegqi-eager") << "pre-unfold counterexample : " << lem << std::endl; + std::map< Node, Node > visited_n; + lem = getEagerUnfold( lem, visited_n ); + } + Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl; - d_quantEngine->addLemma( lem ); - ++(d_statistics.d_cegqi_lemmas_ce); - Trace("cegqi-engine") << " ...find counterexample." << std::endl; - //optimization : eagerly unfold applications of evaluation function - if( options::sygusEagerUnfold() ){ - std::vector< Node > eager_lems; - std::map< Node, bool > visited; - getEagerUnfoldLemmas( eager_lems, lem, visited ); - for( unsigned i=0; iaddLemma( eager_lems[i] ); + if( d_quantEngine->addLemma( lem ) ){ + ++(d_statistics.d_cegqi_lemmas_ce); + Trace("cegqi-engine") << " ...find counterexample." << std::endl; + }else{ + //this may happen if we eagerly unfold, simplify to true + if( !options::sygusDirectEval() ){ + Trace("cegqi-engine") << " ...FAILED to add candidate!" << std::endl; + }else{ + Trace("cegqi-engine-debug") << " ...FAILED to add candidate!" << std::endl; + } + if( conj->d_refine_count==0 ){ + //immediately go to refine candidate + checkCegConjecture( conj ); + return; } } } @@ -602,16 +654,17 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le } } -void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - Trace("cegqi-eager-debug") << "getEagerUnfoldLemmas " << n << std::endl; - visited[n] = true; +Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) { + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv==visited.end() ){ + Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl; + Node ret; if( n.getKind()==APPLY_UF ){ TypeNode tn = n[0].getType(); Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl; if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( dt.isSygus() ){ + if( dt.isSygus() ){ Trace("cegqi-eager") << "Unfold eager : " << n << std::endl; Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( n[0], tn ); Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl; @@ -623,12 +676,13 @@ void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, vars.push_back( var_list[j] ); } for( unsigned j=1; jmkConst(BitVector(1u, 1u)); - subs.push_back( n[j].eqNode( c ) ); + subs.push_back( nc.eqNode( c ) ); }else{ - subs.push_back( n[j] ); + subs.push_back( nc ); } Assert( subs[j-1].getType()==var_list[j-1].getType() ); } @@ -636,16 +690,34 @@ void CegInstantiation::getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl; Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl; Assert( n.getType()==bTerm.getType() ); - Node lem = Rewriter::rewrite( NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bTerm ) ); - lems.push_back( lem ); + ret = bTerm; } } } - if( n.getKind()!=FORALL ){ - for( unsigned i=0; i children; + for( unsigned i=0; imkNode( n.getKind(), children ); + } + } + if( ret.isNull() ){ + ret = n; } } + visited[n] = ret; + return ret; + }else{ + return itv->second; } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 81f70d600..c8b41c035 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -126,6 +126,8 @@ private: CegConjecture * d_conj; /** last instantiation by single invocation module? */ bool d_last_inst_si; + /** evaluation axioms */ + std::map< Node, bool > d_eval_axioms; private: //for enforcing fairness /** measure functions */ std::map< TypeNode, Node > d_uf_measure; @@ -140,7 +142,7 @@ private: //for enforcing fairness /** get measure lemmas */ void getMeasureLemmas( Node n, Node v, std::vector< Node >& lems ); /** get eager unfolding */ - void getEagerUnfoldLemmas( std::vector< Node >& lems, Node n, std::map< Node, bool >& visited ); + Node getEagerUnfold( Node n, std::map< Node, Node >& visited ); private: /** check conjecture */ void checkCegConjecture( CegConjecture * conj ); @@ -158,6 +160,7 @@ public: /* Call during quantifier engine's check */ void check( Theory::Effort e, unsigned quant_e ); /* Called for new quantifiers */ + void preRegisterQuantifier( Node q ); void registerQuantifier( Node q ); void assertNode( Node n ); Node getNextDecisionRequest(); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 149330c61..d2637a555 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -692,8 +692,10 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { void InstStrategyCegqi::registerQuantifier( Node q ) { if( options::cbqiPreRegInst() ){ - //just get the instantiator - getInstantiator( q ); + if( doCbqi( q ) ){ + //just get the instantiator + getInstantiator( q ); + } } } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 9450c5daa..bac2aa35c 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -219,7 +219,6 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) { if( n.getKind()==BOUND_VARIABLE ){ d_inMatchConstraint[n] = true; } - //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){ if( d_var_num.find( n )==d_var_num.end() ){ Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl; d_var_num[n] = d_vars.size(); @@ -987,26 +986,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) if( isVar ){ Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() ); if( n.getKind()==ITE ){ - /* - d_type = typ_ite_var; - d_type_not = false; - d_n = n; - d_children.push_back( MatchGen( qi, d_n[0] ) ); - if( d_children[0].isValid() ){ - d_type = typ_ite_var; - for( unsigned i=1; i<=2; i++ ){ - Node nn = n.eqNode( n[i] ); - d_children.push_back( MatchGen( qi, nn ) ); - d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 ); - if( !d_children[d_children.size()-1].isValid() ){ - setInvalid(); - break; - } - } - }else{ -*/ - d_type = typ_invalid; - //} + d_type = typ_invalid; }else{ d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym; d_qni_var_num[0] = qi->getVarNum( n ); @@ -1049,26 +1029,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) break; } } - /* - else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){ - Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl; - //if variable equality/disequality at top level, remove immediately - bool cIsNot = d_children[d_children.size()-1].d_type_not; - Node cn = d_children[d_children.size()-1].d_n; - Assert( cn.getKind()==EQUAL ); - Assert( p->d_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) ); - //make it a built-in constraint instead - for( unsigned i=0; i<2; i++ ){ - if( p->d_qinfo[q].isVar( cn[i] ) ){ - int v = p->d_qinfo[q].getVarNum( cn[i] ); - Node cno = cn[i==0 ? 1 : 0]; - p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno ); - break; - } - } - d_children.pop_back(); - } - */ } }else{ d_type = typ_invalid; @@ -1104,20 +1064,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) d_type = typ_ground; qi->setGroundSubterm( d_n ); } - //if( d_type!=typ_invalid ){ - //determine an efficient children ordering - //if( !d_children.empty() ){ - //for( unsigned i=0; i& bvars //add to children order d_children_order.push_back( min_score_index ); assigned[min_score_index] = true; - //if( vb_count[min_score_index]==0 ){ - // d_independent.push_back( min_score_index ); - //} //determine order internal to children d_children[min_score_index].determineVariableOrder( qi, bvars ); Trace("qcf-qregister-debug") << "...bind variables" << std::endl; //now, make it a bound variable - for( unsigned i=0; i0 ){ + for( unsigned i=0; ihasOwnership( q, this ) ){ d_quants.push_back( q ); d_quant_id[q] = d_quants.size(); - Trace("qcf-qregister") << "Register "; - debugPrintQuant( "qcf-qregister", q ); - Trace("qcf-qregister") << " : " << q << std::endl; + if( Trace.isOn("qcf-qregister") ){ + Trace("qcf-qregister") << "Register "; + debugPrintQuant( "qcf-qregister", q ); + Trace("qcf-qregister") << " : " << q << std::endl; + } //make QcfNode structure Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl; d_qinfo[q].initialize( this, q, q[1] ); //debug print - Trace("qcf-qregister") << "- Flattened structure is :" << std::endl; - Trace("qcf-qregister") << " "; - debugPrintQuantBody( "qcf-qregister", q, q[1] ); - Trace("qcf-qregister") << std::endl; - if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){ - Trace("qcf-qregister") << " with additional constraints : " << std::endl; - for( unsigned j=q[0].getNumChildren(); jq[0].getNumChildren() ){ + Trace("qcf-qregister") << " with additional constraints : " << std::endl; + for( unsigned j=q[0].getNumChildren(); jmkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); if( options::ceGuidedInst() ){ - d_sygus_tdb = new TermDbSygus; + d_sygus_tdb = new TermDbSygus( c, qe ); }else{ d_sygus_tdb = NULL; } @@ -170,6 +170,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi Node op = getMatchOperator( n ); d_op_map[op].push_back( n ); added.insert( n ); + + if( d_sygus_tdb ){ + d_sygus_tdb->registerEvalTerm( n ); + } if( options::eagerInstQuant() ){ for( unsigned i=0; i& subs, bool subsRep, return qy->getEngine()->getRepresentative( n1 ) == ( pol ? d_true : d_false ); } } - }else if( n.getKind()==FORALL ){ + }else if( n.getKind()==FORALL && !pol ){ return isEntailed2( n[1], subs, subsRep, hasSubs, pol, qy ); } return false; @@ -1576,7 +1580,7 @@ struct sortTermOrder { //this function makes a canonical representation of a term ( // - orders variables left to right // - if apply_torder, then sort direct subterms of commutative operators -Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) { +Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) { Trace("canon-term-debug") << "Get canonical term for " << n << std::endl; if( n.getKind()==BOUND_VARIABLE ){ std::map< TNode, TNode >::iterator it = subs.find( n ); @@ -1593,32 +1597,38 @@ Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_coun return it->second; } }else if( n.getNumChildren()>0 ){ - //collect children - Trace("canon-term-debug") << "Collect children" << std::endl; - std::vector< Node > cchildren; - for( unsigned i=0; imkNode( n.getKind(), cchildren ); - Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; - return ret; + std::map< TNode, Node >::iterator it = visited.find( n ); + if( it!=visited.end() ){ + return it->second; + }else{ + //collect children + Trace("canon-term-debug") << "Collect children" << std::endl; + std::vector< Node > cchildren; + for( unsigned i=0; imkNode( n.getKind(), cchildren ); + Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; + visited[n] = ret; + return ret; + } }else{ Trace("canon-term-debug") << "...return 0-child term." << std::endl; return n; @@ -1628,7 +1638,8 @@ Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_coun Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){ std::map< TypeNode, unsigned > var_count; std::map< TNode, TNode > subs; - return getCanonicalTerm( n, var_count, subs, apply_torder ); + std::map< TNode, Node > visited; + return getCanonicalTerm( n, var_count, subs, apply_torder, visited ); } void TermDb::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) { @@ -2249,11 +2260,15 @@ bool TermDb::isQAttrQuantElimPartial( Node q ) { } } -TermDbSygus::TermDbSygus(){ +TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){ d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); } +bool TermDbSygus::reset( Theory::Effort e ) { + return true; +} + TNode TermDbSygus::getVar( TypeNode tn, int i ) { while( i>=(int)d_fv[tn].size() ){ std::stringstream ss; @@ -3184,3 +3199,69 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > out << n; } } + +void TermDbSygus::registerEvalTerm( Node n ) { + if( options::sygusDirectEval() ){ + if( n.getKind()==APPLY_UF ){ + Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl; + TypeNode tn = n[0].getType(); + if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isSygus() ){ + Node f = n.getOperator(); + Trace("sygus-eager") << "...the evaluation function is : " << f << std::endl; + Assert( n[0].getKind()!=APPLY_CONSTRUCTOR ); + d_evals[n[0]].push_back( n ); + TypeNode tn = n[0].getType(); + Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Node var_list = Node::fromExpr( dt.getSygusVarList() ); + Assert( dt.isSygus() ); + d_eval_args[n[0]].push_back( std::vector< Node >() ); + for( unsigned j=1; jmkConst(BitVector(1u, 1u)); + d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) ); + }else{ + d_eval_args[n[0]].back().push_back( n[j] ); + } + } + + } + } + } + } +} + +void TermDbSygus::registerModelValue( Node n, Node v, std::vector< Node >& lems ) { + std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n ); + if( it!=d_eval_args.end() && !it->second.empty() ){ + unsigned start = d_node_mv_args_proc[n][v]; + Node antec = n.eqNode( v ).negate(); + TypeNode tn = n.getType(); + Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( dt.isSygus() ); + Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << v << " for " << n << std::endl; + Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl; + Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( v, tn ); + Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl; + std::vector< Node > vars; + Node var_list = Node::fromExpr( dt.getSygusVarList() ); + for( unsigned j=0; jsecond.size(); i++ ){ + Assert( vars.size()==it->second[i].size() ); + Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() ); + Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); + lem = NodeManager::currentNM()->mkNode( OR, antec, lem ); + Trace("sygus-eager") << "Lemma : " << lem << std::endl; + lems.push_back( lem ); + } + d_node_mv_args_proc[n][v] = it->second.size(); + } +} + diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 684b6cf83..4291587a4 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -419,7 +419,8 @@ private: //free variables std::map< TypeNode, std::vector< Node > > d_cn_free_var; // get canonical term, return null if it contains a term apart from handled signature - Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ); + Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, + std::map< TNode, Node >& visited ); public: /** get id for operator */ int getIdForOperator( Node op ); @@ -541,6 +542,8 @@ public: class TermDbSygus { private: + /** reference to the quantifiers engine */ + QuantifiersEngine* d_quantEngine; std::map< TypeNode, std::vector< Node > > d_fv; std::map< Node, TypeNode > d_fv_stype; std::map< Node, int > d_fv_num; @@ -581,7 +584,11 @@ private: std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin; std::map< TypeNode, std::map< Node, Node > > d_builtin_const_to_sygus; public: - TermDbSygus(); + TermDbSygus( context::Context* c, QuantifiersEngine* qe ); + ~TermDbSygus(){} + bool reset( Theory::Effort e ); + std::string identify() const { return "TermDbSygus"; } + bool isRegistered( TypeNode tn ); TypeNode sygusToBuiltinType( TypeNode tn ); int getKindArg( TypeNode tn, Kind k ); @@ -633,6 +640,15 @@ public: static Kind getOperatorKind( Node op ); /** print sygus term */ static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ); + +//for eager instantiation +private: + std::map< Node, std::vector< Node > > d_evals; + std::map< Node, std::vector< std::vector< Node > > > d_eval_args; + std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc; +public: + void registerEvalTerm( Node n ); + void registerModelValue( Node n, Node v, std::vector< Node >& lems ); }; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index efe40aaa8..7ad13b3a8 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -72,8 +72,11 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { void TheoryQuantifiers::preRegisterTerm(TNode n) { Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; - if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){ - getQuantifiersEngine()->registerQuantifier( n ); + if( n.getKind()==FORALL ){ + if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ + getQuantifiersEngine()->registerQuantifier( n ); + Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() done " << n << endl; + } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7522c633b..1f4a04218 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -295,9 +295,9 @@ private: bool removeInstantiationInternal( Node q, std::vector< Node >& terms ); /** set instantiation level attr */ static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); +public: /** flush lemmas */ void flushLemmas(); -public: /** get instantiation */ Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); /** get instantiation */ -- 2.30.2