diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-16 17:30:59 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-16 17:30:59 -0500 |
commit | 246fffffafba07aaeadd0d0c99a2e1c4b589a63c (patch) | |
tree | 5d2b41e264fc2039da115556befa7fe487a12bb7 /src/theory/quantifiers | |
parent | f58c881034d3b0193dfee8fabf451cc0e9ea20ab (diff) |
Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure. Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 40 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 114 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 5 |
4 files changed, 113 insertions, 53 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index cae3e730e..8af11b1af 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" #include "prop/prop_engine.h" +#include "theory/bv/theory_bv_rewriter.h" using namespace CVC4::kind; using namespace std; @@ -56,12 +57,15 @@ void CegConjecture::assign( Node q ) { } } d_quant = q; + Assert( d_candidates.empty() ); + std::vector< Node > vars; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + vars.push_back( q[0][i] ); d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) ); } Trace("cegqi") << "Base quantified formula is : " << q << std::endl; //construct base instantiation - d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, d_candidates ) ); + d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) ); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj ); @@ -272,9 +276,26 @@ void CegInstantiation::preRegisterQuantifier( Node q ) { 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; + //do unfolding if it induces Boolean structure, + //do direct evaluation if it does not induce Boolean structure, + // the reasoning is unfolding over these terms does not lead to helpful conflict analysis, and introduces many shared terms + bool directEval = true; + TypeNode ptn = pat.getType(); + if( ptn.isBoolean() || ptn.isBitVector() ){ + directEval = false; + }else{ + unsigned cindex = Datatype::indexOf(pat[0].getOperator().toExpr() ); + Node base = d_quantEngine->getTermDatabaseSygus()->getGenericBase( tn, dt, cindex ); + Trace("cegqi-debug") << "Generic base term for " << pat[0] << " is " << base << std::endl; + if( base.getKind()==ITE ){ + directEval = false; + } + } + if( directEval ){ + //take ownership of this quantified formula (will use direct evaluation instead of unfolding instantiation) + d_quantEngine->setOwner( q, this ); + d_eval_axioms[q] = true; + } } } } @@ -413,8 +434,13 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } 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] ); + Node lem = eager_eval_lem[j]; + if( d_quantEngine->getTheoryEngine()->isTheoryEnabled(THEORY_BV) ){ + //FIXME: hack to incorporate hacks from BV for division by zero + lem = bv::TheoryBVRewriter::eliminateBVSDiv( lem ); + } + Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem << std::endl; + d_quantEngine->addLemma( lem ); } return; } @@ -435,6 +461,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } } //must get a counterexample to the value of the current candidate + Assert( conj->d_candidates.size()==model_values.size() ); Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() ); //check whether we will run CEGIS on inner skolem variables bool sk_refine = ( !conj->isGround() || conj->d_refine_count==0 ); @@ -686,6 +713,7 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) } Assert( subs[j-1].getType()==var_list[j-1].getType() ); } + Assert( vars.size()==subs.size() ); bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl; Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 33856d226..a5d4174dd 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -534,6 +534,7 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){ return false; }else{ Trace("cegqi-engine") << siss.str() << std::endl; + Assert( d_single_inv_var.size()==subs.size() ); Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); if( d_qe->getTermDatabase()->containsVtsTerm( lem ) ){ Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; @@ -595,6 +596,7 @@ bool CegConjectureSingleInv::check( std::vector< Node >& lems ) { for( unsigned i=0; i<d_sip->d_all_vars.size(); i++ ){ subs.push_back( NodeManager::currentNM()->mkSkolem( "kv", d_sip->d_all_vars[i].getType(), "created for verifying nsi" ) ); } + Assert( d_sip->d_all_vars.size()==subs.size() ); inst = inst.substitute( d_sip->d_all_vars.begin(), d_sip->d_all_vars.end(), subs.begin(), subs.end() ); Trace("cegqi-nsi") << "NSI : verification : " << inst << std::endl; Trace("cegqi-lemma") << "Cegqi::Lemma : verification lemma : " << inst << std::endl; @@ -751,6 +753,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& std::sort( indices.begin(), indices.end(), ssii ); Trace("csi-sol") << "Construct solution" << std::endl; s = constructSolution( indices, sol_index, 0 ); + Assert( vars.size()==d_sol->d_varList.size() ); s = s.substitute( vars.begin(), vars.end(), d_sol->d_varList.begin(), d_sol->d_varList.end() ); } d_orig_solution = s; @@ -922,6 +925,7 @@ void SingleInvocationPartition::process( Node n ) { std::vector< Node > funcs; //normalize the invocations if( !terms.empty() ){ + Assert( terms.size()==subs.size() ); cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); } std::vector< Node > children; @@ -940,6 +944,7 @@ void SingleInvocationPartition::process( Node n ) { } Trace("si-prt") << std::endl; cr = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + Assert( terms.size()==subs.size() ); cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl; //now must check if it has other bound variables @@ -974,6 +979,7 @@ void SingleInvocationPartition::process( Node n ) { } } } + Assert( terms.size()==subs.size() ); cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); } cr = Rewriter::rewrite( cr ); @@ -982,6 +988,7 @@ void SingleInvocationPartition::process( Node n ) { TermDb::getBoundVars( cr, d_all_vars ); if( singleInvocation ){ //replace with single invocation formulation + Assert( si_terms.size()==si_subs.size() ); cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() ); cr = Rewriter::rewrite( cr ); Trace("si-prt") << ".....si version=" << cr << std::endl; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index eff641736..e81245034 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -2480,8 +2480,8 @@ Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); if( it==d_sygus_to_builtin[tn].end() ){ Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; - Assert( n.getKind()==APPLY_CONSTRUCTOR ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + Assert( n.getKind()==APPLY_CONSTRUCTOR ); unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); Assert( n.getNumChildren()==dt[i].getNumArgs() ); std::map< TypeNode, int > var_count; @@ -3200,9 +3200,17 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > } } +Node TermDbSygus::getAnchor( Node n ) { + if( n.getKind()==APPLY_SELECTOR_TOTAL ){ + return getAnchor( n[0] ); + }else{ + return n; + } +} + void TermDbSygus::registerEvalTerm( Node n ) { if( options::sygusDirectEval() ){ - if( n.getKind()==APPLY_UF ){ + if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){ Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl; TypeNode tn = n[0].getType(); if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){ @@ -3210,58 +3218,72 @@ void TermDbSygus::registerEvalTerm( Node n ) { 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] ); + if( 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] ); + } } + Node a = getAnchor( n[0] ); + d_subterms[a][n[0]] = true; } - } } } } } -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(); +void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems ) { + std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a ); + if( its!=d_subterms.end() ){ + Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl; + for( std::map< Node, bool >::iterator itss = its->second.begin(); itss != its->second.end(); ++itss ){ + Node n = itss->first; + Trace("sygus-eager-debug") << "...process : " << n << std::endl; + std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n ); + if( it!=d_eval_args.end() && !it->second.empty() ){ + TNode at = a; + TNode vt = v; + Node vn = n.substitute( at, vt ); + vn = Rewriter::rewrite( vn ); + unsigned start = d_node_mv_args_proc[n][vn]; + Node antec = n.eqNode( vn ).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 : " << vn << " for " << n << std::endl; + Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl; + Node bTerm = d_quantEngine->getTermDatabaseSygus()->sygusToBuiltin( vn, 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][vn] = it->second.size(); + } + } } } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 4291587a4..b7b798cd4 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -557,7 +557,6 @@ public: private: std::map< TypeNode, std::map< int, Node > > d_generic_base; std::map< TypeNode, std::vector< Node > > d_generic_templ; - Node getGenericBase( TypeNode tn, const Datatype& dt, int c ); bool getMatch( Node p, Node n, std::map< int, Node >& s ); bool getMatch2( Node p, Node n, std::map< int, Node >& s, std::vector< int >& new_s ); public: @@ -622,6 +621,7 @@ public: /** get value */ Node getTypeMaxValue( TypeNode tn ); TypeNode getSygusTypeForVar( Node v ); + Node getGenericBase( TypeNode tn, const Datatype& dt, int c ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); Node sygusToBuiltin( Node n, TypeNode tn ); Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 ); @@ -641,8 +641,11 @@ public: /** print sygus term */ static void printSygusTerm( std::ostream& out, Node n, std::vector< Node >& lvs ); + /** get anchor */ + static Node getAnchor( Node n ); //for eager instantiation private: + std::map< Node, std::map< Node, bool > > d_subterms; 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; |