diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/kinds | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 128 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 116 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 143 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
10 files changed, 278 insertions, 154 deletions
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; j<d_candidates.size(); j++ ){ - lem_c.push_back( NodeManager::currentNM()->mkNode( 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; i<conj->d_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; j<conj->d_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; j<eager_eval_lem.size(); j++ ){ + Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << eager_eval_lem[j] << std::endl; + d_quantEngine->addLemma( 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; i<eager_lems.size(); i++ ){ - Trace("cegqi-lemma") << "Cegqi::Lemma : eager unfold : " << eager_lems[i] << std::endl; - d_quantEngine->addLemma( 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; j<n.getNumChildren(); j++ ){ + Node nc = getEagerUnfold( n[j], visited ); if( var_list[j-1].getType().isBoolean() ){ //TODO: remove this case when boolean term conversion is eliminated Node c = NodeManager::currentNM()->mkConst(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<n.getNumChildren(); i++ ){ - getEagerUnfoldLemmas( lems, n[i], visited ); + if( ret.isNull() ){ + if( n.getKind()!=FORALL ){ + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nc = getEagerUnfold( n[i], visited ); + childChanged = childChanged || n[i]!=nc; + children.push_back( nc ); + } + if( childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( 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<d_children.size(); i++ ){ - // d_children_order.push_back( i ); - //} - //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){ - //sort based on the type of the constraint : ground comes first, then literals, then others - //MatchGenSort mgs; - //mgs.d_mg = this; - //std::sort( d_children_order.begin(), d_children_order.end(), mgs ); - //} - //} - //} } Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = "; debugPrintType( "qcf-qregister-debug", d_type, true ); @@ -1201,22 +1147,21 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& 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; i<c_to_vars[min_score_index].size(); i++ ){ - int v = c_to_vars[min_score_index][i]; - if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){ - for( unsigned j=0; j<vars_to_c[v].size(); j++ ){ - int vc = vars_to_c[v][j]; - vu_count[vc]--; - vb_count[vc]++; + if( vu_count[min_score_index]>0 ){ + for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){ + int v = c_to_vars[min_score_index][i]; + if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){ + for( unsigned j=0; j<vars_to_c[v].size(); j++ ){ + int vc = vars_to_c[v][j]; + vu_count[vc]--; + vb_count[vc]++; + } + bvars.push_back( v ); } - bvars.push_back( v ); } } Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl; @@ -1908,7 +1853,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return n.getType().isBoolean() && TermDb::isBoolConnective( n.getKind() ); + return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ); } bool MatchGen::isHandledUfTerm( TNode n ) { @@ -1964,28 +1909,31 @@ void QuantConflictFind::registerQuantifier( Node q ) { if( d_quantEngine->hasOwnership( 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(); j<d_qinfo[q].d_vars.size(); j++ ){ - Trace("qcf-qregister") << " ?x" << j << " = "; - debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false ); - Trace("qcf-qregister") << std::endl; - } - } - - Trace("qcf-qregister") << "Done registering quantifier." << std::endl; + if( Trace.isOn("qcf-qregister") ){ + 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(); j<d_qinfo[q].d_vars.size(); j++ ){ + Trace("qcf-qregister") << " ?x" << j << " = "; + debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false ); + Trace("qcf-qregister") << std::endl; + } + } + Trace("qcf-qregister") << "Done registering quantifier." << std::endl; + } } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 7b4719878..eff641736 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -90,7 +90,7 @@ TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* d_zero = NodeManager::currentNM()->mkConst( 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<n.getNumChildren(); i++ ){ @@ -537,7 +541,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& 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; i<n.getNumChildren(); i++ ){ - cchildren.push_back( n[i] ); - } - //if applicable, first sort by term order - if( apply_torder && isComm( n.getKind() ) ){ - Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl; - sortTermOrder sto; - sto.d_tdb = this; - std::sort( cchildren.begin(), cchildren.end(), sto ); - } - //now make canonical - Trace("canon-term-debug") << "Make canonical children" << std::endl; - for( unsigned i=0; i<cchildren.size(); i++ ){ - cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder ); - } - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl; - cchildren.insert( cchildren.begin(), n.getOperator() ); - } - Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl; - Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren ); - Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; - return ret; + 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; i<n.getNumChildren(); i++ ){ + cchildren.push_back( n[i] ); + } + //if applicable, first sort by term order + if( apply_torder && isComm( n.getKind() ) ){ + Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl; + sortTermOrder sto; + sto.d_tdb = this; + std::sort( cchildren.begin(), cchildren.end(), sto ); + } + //now make canonical + Trace("canon-term-debug") << "Make canonical children" << std::endl; + for( unsigned i=0; i<cchildren.size(); i++ ){ + cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder, visited ); + } + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl; + cchildren.insert( cchildren.begin(), n.getOperator() ); + } + Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl; + Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren ); + Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; + 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; j<n.getNumChildren(); j++ ){ + if( var_list[j-1].getType().isBoolean() ){ + //TODO: remove this case when boolean term conversion is eliminated + Node c = NodeManager::currentNM()->mkConst(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; j<var_list.getNumChildren(); j++ ){ + vars.push_back( var_list[j] ); + } + //for each evaluation + for( unsigned i=start; i<it->second.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 */ |