diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/options/quantifiers_options | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 23 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 171 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_match.h | 53 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 343 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 15 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 102 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.h | 7 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 37 |
9 files changed, 471 insertions, 289 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 0b5474959..0a94ad890 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -26,6 +26,8 @@ option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMod # forall y. P( c, y ) option varElimQuant --var-elim-quant bool :default true enable simple variable elimination for quantified formulas +option varIneqElimQuant --var-ineq-elim-quant bool :default true + enable variable elimination based on infinite projection of unbound arithmetic variables option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers #ite lift mode for quantified formulas @@ -50,8 +52,6 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers option elimTautQuant --elim-taut-quant bool :default true eliminate tautological disjuncts of quantified formulas -option purifyQuant --purify-quant bool :default false - purify quantified formulas option elimExtArithQuant --elim-ext-arith-quant bool :default true eliminate extended arithmetic symbols in quantified formulas option condRewriteQuant --cond-rewrite-quant bool :default true @@ -328,4 +328,9 @@ option quantAntiSkolem --quant-anti-skolem bool :read-write :default false option quantEqualityEngine --quant-ee bool :default false maintain congrunce closure over universal equalities +### proof options + +option trackInstLemmas --track-inst-lemmas bool :default true + when proof is enabled, track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization) + endmodule diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 3177739ac..facd7bd2e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -662,7 +662,7 @@ Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices Assert( index<d_inst.size() ); Assert( i<d_inst[index].size() ); unsigned uindex = indices[index]; - if( index==d_inst.size()-1 ){ + if( index==indices.size()-1 ){ return d_inst[uindex][i]; }else{ Node cond = d_lemmas_produced[uindex]; @@ -753,12 +753,29 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& //construct the solution Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl; + bool useUnsatCore = false; + std::vector< Node > active_lemmas; + /* TODO? + //minimize based on unsat core, if possible + std::vector< Node > active_lemmas; + if( d_qe->getUnsatCoreLemmas( active_lemmas ) ){ + useUnsatCore = true; + } + */ Assert( d_lemmas_produced.size()==d_inst.size() ); std::vector< unsigned > indices; for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){ - Assert( sol_index<d_inst[i].size() ); - indices.push_back( i ); + bool incl = true; + if( useUnsatCore ){ + incl = std::find( active_lemmas.begin(), active_lemmas.end(), d_lemmas_produced[i] )!=active_lemmas.end(); + } + if( incl ){ + Assert( sol_index<d_inst[i].size() ); + indices.push_back( i ); + } } + Trace("csi-sol") << "...included " << indices.size() << " / " << d_lemmas_produced.size() << " instantiations." << std::endl; + Assert( !indices.empty() ); //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions) // TODO : to minimize solution size, put the largest term last sortSiInstanceIndices ssii; diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 8818175db..c419bbc46 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -199,31 +199,90 @@ bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< } } -void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const { +bool InstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio, int index ){ + if( index==(int)q[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){ + setInstLemma( lem ); + return true; + }else{ + int i_index = imtio ? imtio->d_order[index] : index; + std::map< Node, InstMatchTrie >::iterator it = d_data.find( m[i_index] ); + if( it!=d_data.end() ){ + return it->second.recordInstLemma( q, m, lem, imtio, index+1 ); + }else{ + return false; + } + } +} + +void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const { if( terms.size()==q[0].getNumChildren() ){ - out << " ( "; - for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ){ out << ", ";} - out << terms[i]; + bool print; + if( useActive ){ + if( hasInstLemma() ){ + Node lem = getInstLemma(); + print = std::find( active.begin(), active.end(), lem )!=active.end(); + }else{ + print = false; + } + }else{ + print = true; + } + if( print ){ + if( firstTime ){ + out << "Instantiations of " << q << " : " << std::endl; + firstTime = false; + } + out << " ( "; + for( unsigned i=0; i<terms.size(); i++ ){ + if( i>0 ){ out << ", ";} + out << terms[i]; + } + out << " )" << std::endl; } - out << " )" << std::endl; }else{ for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second.print( out, q, terms ); + it->second.print( out, q, terms, firstTime, useActive, active ); terms.pop_back(); } } } -void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const { +void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const { if( terms.size()==q[0].getNumChildren() ){ - //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); - insts.push_back( qe->getInstantiation( q, terms, true ) ); + if( useActive ){ + if( hasInstLemma() ){ + Node lem = getInstLemma(); + if( std::find( active.begin(), active.end(), lem )!=active.end() ){ + insts.push_back( lem ); + } + } + }else{ + insts.push_back( qe->getInstantiation( q, terms, true ) ); + } }else{ for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second.getInstantiations( insts, q, terms, qe ); + it->second.getInstantiations( insts, q, terms, qe, useActive, active ); + terms.pop_back(); + } + } +} + +void InstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const { + if( terms.size()==q[0].getNumChildren() ){ + if( hasInstLemma() ){ + Node lem = getInstLemma(); + if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){ + quant[lem] = q; + tvec[lem].clear(); + tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() ); + } + } + }else{ + for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second.getExplanationForInstLemmas( q, terms, lems, quant, tvec ); terms.pop_back(); } } @@ -301,8 +360,7 @@ bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vecto return false; } }else{ - Node n = m[index]; - std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] ); if( it!=d_data.end() ){ return it->second->removeInstMatch( qe, q, m, index+1 ); }else{ @@ -311,34 +369,99 @@ bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vecto } } -void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{ +bool CDInstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index ) { + if( index==(int)q[0].getNumChildren() ){ + if( d_valid.get() ){ + setInstLemma( lem ); + return true; + }else{ + return false; + } + }else{ + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] ); + if( it!=d_data.end() ){ + return it->second->recordInstLemma( q, m, lem, index+1 ); + }else{ + return false; + } + } +} + +void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ - out << " ( "; - for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ) out << ", "; - out << terms[i]; + bool print; + if( useActive ){ + if( hasInstLemma() ){ + Node lem = getInstLemma(); + print = std::find( active.begin(), active.end(), lem )!=active.end(); + }else{ + print = false; + } + }else{ + print = true; + } + if( print ){ + if( firstTime ){ + out << "Instantiations of " << q << " : " << std::endl; + firstTime = false; + } + out << " ( "; + for( unsigned i=0; i<terms.size(); i++ ){ + if( i>0 ) out << ", "; + out << terms[i]; + } + out << " )" << std::endl; } - out << " )" << std::endl; }else{ for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second->print( out, q, terms ); + it->second->print( out, q, terms, firstTime, useActive, active ); terms.pop_back(); } } } } -void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const{ +void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ - //insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); - insts.push_back( qe->getInstantiation( q, terms, true ) ); + if( useActive ){ + if( hasInstLemma() ){ + Node lem; + if( std::find( active.begin(), active.end(), lem )!=active.end() ){ + insts.push_back( lem ); + } + } + }else{ + insts.push_back( qe->getInstantiation( q, terms, true ) ); + } + }else{ + for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second->getInstantiations( insts, q, terms, qe, useActive, active ); + terms.pop_back(); + } + } + } +} + + +void CDInstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const { + if( d_valid.get() ){ + if( terms.size()==q[0].getNumChildren() ){ + if( hasInstLemma() ){ + Node lem; + if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){ + quant[lem] = q; + tvec[lem].clear(); + tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() ); + } + } }else{ for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second->getInstantiations( insts, q, terms, qe ); + it->second->getExplanationForInstLemmas( q, terms, lems, quant, tvec ); terms.pop_back(); } } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index ad287c1a3..68446922f 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -96,12 +96,19 @@ public: public: std::vector< int > d_order; };/* class InstMatchTrie ImtIndexOrder */ - /** the data */ std::map< Node, InstMatchTrie > d_data; private: - void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; - void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const; + void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const; + void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const; + void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const; +private: + void setInstLemma( Node n ){ + d_data.clear(); + d_data[n].clear(); + } + bool hasInstLemma() const { return !d_data.empty(); } + Node getInstLemma() const { return d_data.begin()->first; } public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -129,14 +136,19 @@ public: bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 ); - void print( std::ostream& out, Node q ) const{ + bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio = NULL, int index = 0 ); + void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{ std::vector< TNode > terms; - print( out, q, terms ); + print( out, q, terms, firstTime, useActive, active ); } - void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) { + void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) { std::vector< Node > terms; - getInstantiations( insts, q, terms, qe ); + getInstantiations( insts, q, terms, qe, useActive, active ); } + void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const { + std::vector< Node > terms; + getExplanationForInstLemmas( q, terms, lems, quant, tvec ); + } void clear() { d_data.clear(); } };/* class InstMatchTrie */ @@ -147,9 +159,17 @@ private: std::map< Node, CDInstMatchTrie* > d_data; /** is valid */ context::CDO< bool > d_valid; - - void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const; - void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe ) const; +private: + void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const; + void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const; + void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const; +private: + void setInstLemma( Node n ){ + d_data.clear(); + d_data[n] = NULL; + } + bool hasInstLemma() const { return !d_data.empty(); } + Node getInstLemma() const { return d_data.begin()->first; } public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(); @@ -177,14 +197,19 @@ public: bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, int index = 0, bool onlyExist = false ); bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 ); - void print( std::ostream& out, Node q ) const{ + bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index = 0 ); + void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{ std::vector< TNode > terms; - print( out, q, terms ); + print( out, q, terms, firstTime, useActive, active ); } - void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe ) { + void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) { std::vector< Node > terms; - getInstantiations( insts, q, terms, qe ); + getInstantiations( insts, q, terms, qe, useActive, active ); } + void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const { + std::vector< Node > terms; + getExplanationForInstLemmas( q, terms, lems, quant, tvec ); + } };/* class CDInstMatchTrie */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 2d56f2cdf..7e896d358 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -85,48 +85,6 @@ bool QuantifiersRewriter::isCube( Node n ){ } } -int QuantifiersRewriter::getPurifyId( Node n ){ - if( !TermDb::hasBoundVarAttr( n ) ){ - return 0; - }else if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ - return 1; - }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE ){ - return 0; - }else{ - return -1; - } -} - -int QuantifiersRewriter::getPurifyIdLit2( Node n, std::map< Node, int >& visited ) { - std::map< Node, int >::iterator it = visited.find( n ); - if( visited.find( n )==visited.end() ){ - int ret = 0; - if( TermDb::hasBoundVarAttr( n ) ){ - ret = getPurifyId( n ); - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - int cid = getPurifyIdLit2( n[i], visited ); - if( cid!=0 ){ - if( ret==0 ){ - ret = cid; - }else if( cid!=ret ){ - ret = -2; - break; - } - } - } - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - -int QuantifiersRewriter::getPurifyIdLit( Node n ) { - std::map< Node, int > visited; - return getPurifyIdLit2( n, visited ); -} - void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ if( n.getKind()==OR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ @@ -884,29 +842,53 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ return body; } -bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) { +bool QuantifiersRewriter::isVariableElim( Node v, Node s ) { if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ return false; }else{ - if( !var_parent.empty() ){ - std::map< Node, std::vector< int > >::iterator it = var_parent.find( v ); - if( it!=var_parent.end() ){ - Assert( !it->second.empty() ); - int id = getPurifyId( s ); - return it->second.size()==1 && it->second[0]==id; + return true; + } +} + +void QuantifiersRewriter::isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, + std::map< Node, bool >& elig_vars ) { + int vindex = hasPol ? ( pol ? 1 : -1 ) : 0; + if( visited[n].find( vindex )==visited[n].end() ){ + visited[n][vindex] = true; + if( elig_vars.find( n )!=elig_vars.end() ){ + //variable contained in a place apart from bounds, no longer eligible for elimination + elig_vars.erase( n ); + Trace("var-elim-ineq-debug") << "...found occurrence of " << n << ", mark ineligible" << std::endl; + }else{ + if( hasPol ){ + std::map< Node, int >::iterator itx = exclude.find( n ); + if( itx!=exclude.end() && itx->second==vindex ){ + //already processed this literal + return; + } + } + for( unsigned j=0; j<n.getNumChildren(); j++ ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( n, j, hasPol, pol, newHasPol, newPol ); + isVariableBoundElig( n[j], exclude, visited, newHasPol, newPol, elig_vars ); + if( elig_vars.empty() ){ + break; + } } } - return true; + }else{ + //already visited } } bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vector< Node >& args, std::vector< Node >& vars, std::vector< Node >& subs, - std::map< Node, std::vector< int > >& var_parent ) { - if( lit.getKind()==EQUAL && pol ){ + std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds ) { + if( lit.getKind()==EQUAL && pol && options::varElimQuant() ){ for( unsigned i=0; i<2; i++ ){ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] ); if( ita!=args.end() ){ - if( isVariableElim( lit[i], lit[1-i], var_parent ) ){ + if( isVariableElim( lit[i], lit[1-i] ) ){ Trace("var-elim-quant") << "Variable eliminate based on equality : " << lit[i] << " -> " << lit[1-i] << std::endl; vars.push_back( lit[i] ); subs.push_back( lit[1-i] ); @@ -915,28 +897,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto } } } - //for arithmetic, solve the equality - if( lit[0].getType().isReal() ){ - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( lit, msum ) ){ - for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ - std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first ); - if( ita!=args.end() ){ - Node veq_c; - Node val; - int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL ); - if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){ - Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl; - vars.push_back( itm->first ); - subs.push_back( val ); - args.erase( ita ); - return true; - } - } - } - } - } - }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE ){ + }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ){ Trace("var-elim-dt") << "Expand datatype variable based on : " << lit << std::endl; std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[0] ); if( ita!=args.end() ){ @@ -960,7 +921,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto args.insert( args.end(), newVars.begin(), newVars.end() ); return true; } - }else if( lit.getKind()==BOUND_VARIABLE ){ + }else if( lit.getKind()==BOUND_VARIABLE && options::varElimQuant() ){ std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit ); if( ita!=args.end() ){ Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl; @@ -970,24 +931,69 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto return true; } } + if( ( lit.getKind()==EQUAL && lit[0].getType().isReal() && pol ) || ( ( lit.getKind()==GEQ || lit.getKind()==GT ) && options::varIneqElimQuant() ) ){ + //for arithmetic, solve the (in)equality + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( lit, msum ) ){ + for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ + if( !itm->first.isNull() ){ + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first ); + if( ita!=args.end() ){ + if( lit.getKind()==EQUAL ){ + Assert( pol ); + Node veq_c; + Node val; + int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL ); + if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val ) ){ + Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl; + vars.push_back( itm->first ); + subs.push_back( val ); + args.erase( ita ); + return true; + } + }else{ + Assert( lit.getKind()==GEQ || lit.getKind()==GT ); + //store that this literal is upper/lower bound for itm->first + Node veq_c; + Node val; + int ires = QuantArith::isolate( itm->first, msum, veq_c, val, lit.getKind() ); + if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val ) ){ + bool is_upper = pol!=( ires==1 ); + Trace("var-elim-ineq-debug") << lit << " is a " << ( is_upper ? "upper" : "lower" ) << " bound for " << itm->first << std::endl; + Trace("var-elim-ineq-debug") << " pol/ires = " << pol << " " << ires << std::endl; + num_bounds[itm->first][is_upper][lit] = pol; + } + } + }else{ + //compute variables in itm->first, these are not eligible for elimination + std::vector< Node > bvs; + TermDb::getBoundVars( itm->first, bvs ); + for( unsigned j=0; j<bvs.size(); j++ ){ + num_bounds[bvs[j]][true].clear(); + num_bounds[bvs[j]][false].clear(); + } + } + } + } + } + } + return false; } -Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ){ +Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ){ Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; + std::map< Node, std::map< bool, std::map< Node, bool > > > num_bounds; QuantPhaseReq qpr( body ); std::vector< Node > vars; std::vector< Node > subs; for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ - //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; - if( ( it->first.getKind()==EQUAL && it->second && options::varElimQuant() ) || - ( it->first.getKind()==APPLY_TESTER && it->second && it->first[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ) || - ( it->first.getKind()==BOUND_VARIABLE && options::varElimQuant() ) ){ - if( computeVariableElimLit( it->first, it->second, args, vars, subs, var_parent ) ){ - break; - } + Trace("var-elim-quant-debug") << " phase req : " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; + if( computeVariableElimLit( it->first, it->second, args, vars, subs, num_bounds ) ){ + break; } } + if( !vars.empty() ){ Trace("var-elim-quant-debug") << "VE " << vars.size() << "/" << args.size() << std::endl; //remake with eliminated nodes @@ -997,21 +1003,65 @@ Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node > qa.d_ipl = qa.d_ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); } Trace("var-elim-quant") << "Return " << body << std::endl; + }else{ + //collect all variables that have only upper/lower bounds + std::map< Node, bool > elig_vars; + for( std::map< Node, std::map< bool, std::map< Node, bool > > >::iterator it = num_bounds.begin(); it != num_bounds.end(); ++it ){ + if( it->second.find( true )==it->second.end() ){ + Trace("var-elim-ineq-debug") << "Variable " << it->first << " has only lower bounds." << std::endl; + elig_vars[it->first] = false; + }else if( it->second.find( false )==it->second.end() ){ + Trace("var-elim-ineq-debug") << "Variable " << it->first << " has only upper bounds." << std::endl; + elig_vars[it->first] = true; + } + } + if( !elig_vars.empty() ){ + std::vector< Node > inactive_vars; + std::map< Node, std::map< int, bool > > visited; + std::map< Node, int > exclude; + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ + if( it->first.getKind()==GEQ || it->first.getKind()==GT ){ + exclude[ it->first ] = it->second ? -1 : 1; + Trace("var-elim-ineq-debug") << "...exclude " << it->first << " at polarity " << exclude[ it->first ] << std::endl; + } + } + //traverse the body, invalidate variables if they occur in places other than the bounds they occur in + isVariableBoundElig( body, exclude, visited, true, true, elig_vars ); + + if( !elig_vars.empty() ){ + if( !qa.d_ipl.isNull() ){ + isVariableBoundElig( qa.d_ipl, exclude, visited, false, true, elig_vars ); + } + for( std::map< Node, bool >::iterator itev = elig_vars.begin(); itev != elig_vars.end(); ++itev ){ + Node v = itev->first; + Trace("var-elim-ineq-debug") << v << " is eligible for elimination." << std::endl; + //do substitution corresponding to infinite projection, all literals involving unbounded variable go to true/false + std::vector< Node > terms; + std::vector< Node > subs; + for( std::map< Node, bool >::iterator itb = num_bounds[v][elig_vars[v]].begin(); itb != num_bounds[v][elig_vars[v]].end(); ++itb ){ + Trace("var-elim-ineq-debug") << " subs : " << itb->first << " -> " << itb->second << std::endl; + terms.push_back( itb->first ); + subs.push_back( NodeManager::currentNM()->mkConst( itb->second ) ); + } + body = body.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + Trace("var-elim-ineq-debug") << "Return " << body << std::endl; + //eliminate from args + std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), v ); + Assert( ita!=args.end() ); + args.erase( ita ); + } + } + } } return body; } Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ){ - //the parent id's for each variable, if using purifyQuant - std::map< Node, std::vector< int > > var_parent; - if( options::purifyQuant() ){ - body = computePurify( body, args, var_parent ); - } if( options::varElimQuant() || options::dtVarExpandQuant() ){ Node prev; do{ prev = body; - body = computeVarElimination2( body, args, qa, var_parent ); + body = computeVarElimination2( body, args, qa ); }while( prev!=body && !args.empty() ); } return body; @@ -1358,9 +1408,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ - return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std; - }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ - return options::purifyQuant() && is_std; + return ( options::varElimQuant() || options::dtVarExpandQuant() ) && is_std; }else{ return false; } @@ -1394,14 +1442,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ n = computeVarElimination( n, args, qa ); - }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ - std::vector< Node > conj; - computePurifyExpand( n, conj, args, qa ); - if( !conj.empty() ){ - return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); - }else{ - return f; - } } Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl; if( f[1]==n && args.size()==f[0].getNumChildren() ){ @@ -1633,104 +1673,3 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { return n; } -Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, - std::map< Node, std::vector< int > >& var_parent, int parentId ){ - std::map< Node, Node >::iterator it = visited.find( body ); - if( it!=visited.end() ){ - return it->second; - }else{ - Node ret = body; - if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::hasBoundVarAttr( ret ) ){ - std::vector< Node > children; - bool childrenChanged = false; - int id = getPurifyId( body ); - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - Node bi; - if( body.getKind()==EQUAL && i==1 ){ - int cid = getPurifyId( children[0] ); - bi = computePurify2( body[i], args, visited, var_to_term, var_parent, cid ); - if( children[0].getKind()==BOUND_VARIABLE ){ - cid = getPurifyId( bi ); - if( cid!=0 && std::find( var_parent[children[0]].begin(), var_parent[children[0]].end(), cid )==var_parent[children[0]].end() ){ - var_parent[children[0]].push_back( id ); - } - } - }else{ - bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id ); - } - childrenChanged = childrenChanged || bi!=body[i]; - children.push_back( bi ); - if( id!=0 && bi.getKind()==BOUND_VARIABLE ){ - if( std::find( var_parent[bi].begin(), var_parent[bi].end(), id )==var_parent[bi].end() ){ - var_parent[bi].push_back( id ); - } - } - } - if( childrenChanged ){ - if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.insert( children.begin(), body.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); - } - if( parentId!=0 && parentId!=id ){ - Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() ); - var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) ); - ret = v; - args.push_back( v ); - } - } - visited[body] = ret; - return ret; - } -} - -Node QuantifiersRewriter::computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) { - std::map< Node, Node > visited; - std::map< Node, Node > var_to_term; - Node pbody = computePurify2( body, args, visited, var_to_term, var_parent, 0 ); - if( pbody==body ){ - return body; - }else{ - Trace("quantifiers-rewrite-purify") << "Purify : " << body << std::endl; - Trace("quantifiers-rewrite-purify") << " Got : " << pbody << std::endl; - for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){ - Trace("quantifiers-rewrite-purify") << " " << it->first << " : " << it->second << std::endl; - } - Trace("quantifiers-rewrite-purify") << "Variable parents : " << std::endl; - for( std::map< Node, std::vector< int > >::iterator it = var_parent.begin(); it != var_parent.end(); ++it ){ - Trace("quantifiers-rewrite-purify") << " " << it->first << " -> "; - for( unsigned i=0; i<it->second.size(); i++ ){ - Trace("quantifiers-rewrite-purify") << it->second[i] << " "; - } - Trace("quantifiers-rewrite-purify") << std::endl; - } - Trace("quantifiers-rewrite-purify") << std::endl; - std::vector< Node > disj; - for( std::map< Node, Node >::iterator it = var_to_term.begin(); it != var_to_term.end(); ++it ){ - disj.push_back( it->second.negate() ); - } - Node res; - if( disj.empty() ){ - res = pbody; - }else{ - disj.push_back( pbody ); - res = NodeManager::currentNM()->mkNode( OR, disj ); - } - Trace("quantifiers-rewrite-purify") << "Constructed : " << res << std::endl << std::endl; - return res; - } -} - -void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ) { - if( body.getKind()==OR ){ - Trace("quantifiers-rewrite-purify-exp") << "Purify expansion : " << body << std::endl; - std::map< int, std::vector< Node > > disj; - std::map< int, std::vector< Node > > fvs; - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - int pid CVC4_UNUSED = getPurifyIdLit( body[i] ); - } - //mark as an attribute - //Node attr = NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, body ); - } -} - diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 776517109..60dc8ab10 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -35,8 +35,6 @@ public: static bool isClause( Node n ); static bool isLiteral( Node n ); static bool isCube( Node n ); - static int getPurifyId( Node n ); - static int getPurifyIdLit( Node n ); private: static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); @@ -49,12 +47,12 @@ private: std::vector< Node >& new_vars, std::vector< Node >& new_conds ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); static bool isConditionalVariableElim( Node n, int pol=0 ); - static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ); + static bool isVariableElim( Node v, Node s ); + static void isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, + std::map< Node, bool >& elig_vars ); static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs, - std::map< Node, std::vector< int > >& var_parent ); - static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, - std::map< Node, std::vector< int > >& var_parent, int parentId ); - static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ); + std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds ); + static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ); private: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); @@ -65,8 +63,6 @@ private: static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); - static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ); - static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ); private: enum{ COMPUTE_ELIM_SYMBOLS = 0, @@ -76,7 +72,6 @@ private: COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, COMPUTE_COND_SPLIT, - COMPUTE_PURIFY_EXPAND, //COMPUTE_FLATTEN_ARGS_UF, //COMPUTE_CNF, COMPUTE_LAST diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index d81efe1da..59fa3592d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -129,6 +129,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_fs = NULL; d_rel_dom = NULL; d_builder = NULL; + + d_trackInstLemmas = options::proof() && options::trackInstLemmas(); d_total_inst_count_debug = 0; //allow theory combination to go first, once initially @@ -224,6 +226,11 @@ void QuantifiersEngine::finishInit(){ } } } + if( options::ceGuidedInst() ){ + d_ceg_inst = new quantifiers::CegInstantiation( this, c ); + d_modules.push_back( d_ceg_inst ); + needsBuilder = true; + } //finite model finding if( options::finiteModelFind() ){ if( options::fmfBoundInt() ){ @@ -238,11 +245,6 @@ void QuantifiersEngine::finishInit(){ d_rr_engine = new quantifiers::RewriteEngine( c, this ); d_modules.push_back(d_rr_engine); } - if( options::ceGuidedInst() ){ - d_ceg_inst = new quantifiers::CegInstantiation( this, c ); - d_modules.push_back( d_ceg_inst ); - needsBuilder = true; - } if( options::ltePartialInst() ){ d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); d_modules.push_back( d_lte_part_inst ); @@ -719,7 +721,7 @@ void QuantifiersEngine::propagate( Theory::Effort level ){ } Node QuantifiersEngine::getNextDecisionRequest(){ - for( int i=0; i<(int)d_modules.size(); i++ ){ + for( unsigned i=0; i<d_modules.size(); i++ ){ Node n = d_modules[i]->getNextDecisionRequest(); if( !n.isNull() ){ return n; @@ -1168,6 +1170,16 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo } } } + if( d_trackInstLemmas ){ + bool recorded; + if( options::incrementalSolving() ){ + recorded = d_c_inst_match_trie[q]->recordInstLemma( q, terms, lem ); + }else{ + recorded = d_inst_match_trie[q].recordInstLemma( q, terms, lem ); + } + Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl; + Assert( recorded ); + } Trace("inst-add-debug") << " --> Success." << std::endl; ++(d_statistics.d_instantiations); return true; @@ -1273,7 +1285,56 @@ void QuantifiersEngine::flushLemmas(){ } } +bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) { + //TODO: only if unsat core available + bool isUnsatCoreAvailable = false; + //if( options::proof() ){ + //} + if( isUnsatCoreAvailable ){ + Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl; + ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas); + if( Trace.isOn("inst-unsat-core") ){ + Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " << std::endl; + for (unsigned i = 0; i < active_lemmas.size(); ++i) { + Trace("inst-unsat-core") << " " << active_lemmas[i] << std::endl; + } + Trace("inst-unsat-core") << std::endl; + } + return true; + }else{ + return false; + } +} + +void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) { + if( d_trackInstLemmas ){ + if( options::incrementalSolving() ){ + for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ + it->second->getExplanationForInstLemmas( it->first, lems, quant, tvec ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + it->second.getExplanationForInstLemmas( it->first, lems, quant, tvec ); + } + } +#ifdef CVC4_ASSERTIONS + for( unsigned j=0; j<lems.size(); j++ ){ + Assert( quant.find( lems[j] )!=quant.end() ); + Assert( tvec.find( lems[j] )!=tvec.end() ); + } +#endif + }else{ + Assert( false ); + } +} + void QuantifiersEngine::printInstantiations( std::ostream& out ) { + bool useUnsatCore = false; + std::vector< Node > active_lemmas; + if( d_trackInstLemmas && getUnsatCoreLemmas( active_lemmas ) ){ + useUnsatCore = true; + } + bool printed = false; for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){ Node q = (*it).first; @@ -1289,16 +1350,21 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { } if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - printed = true; - out << "Instantiations of " << it->first << " : " << std::endl; - it->second->print( out, it->first ); + bool firstTime = true; + it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas ); + if( !firstTime ){ + out << std::endl; + } + printed = printed || !firstTime; } }else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - printed = true; - out << "Instantiations of " << it->first << " : " << std::endl; - it->second.print( out, it->first ); - out << std::endl; + bool firstTime = true; + it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas ); + if( !firstTime ){ + out << std::endl; + } + printed = printed || !firstTime; } } if( !printed ){ @@ -1315,13 +1381,19 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { } void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { + bool useUnsatCore = false; + std::vector< Node > active_lemmas; + if( d_trackInstLemmas && getUnsatCoreLemmas( active_lemmas ) ){ + useUnsatCore = true; + } + if( options::incrementalSolving() ){ for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - it->second->getInstantiations( insts[it->first], it->first, this ); + it->second->getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas ); } }else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - it->second.getInstantiations( insts[it->first], it->first, this ); + it->second.getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas ); } } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 1f4a04218..1ba0b6572 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -143,6 +143,9 @@ private: quantifiers::QuantAntiSkolem * d_anti_skolem; /** quantifiers instantiation propagtor */ quantifiers::InstPropagator * d_inst_prop; +private: + /** whether we are tracking instantiation lemmas */ + bool d_trackInstLemmas; public: //effort levels enum { QEFFORT_CONFLICT, @@ -363,6 +366,10 @@ public: void printSynthSolution( std::ostream& out ); /** get instantiations */ void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + /** get unsat core lemmas */ + bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas ); + /** get inst for lemmas */ + void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ); /** statistics class */ class Statistics { public: diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index e8f1b879a..a697dad75 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -102,7 +102,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node b1 = NodeManager::currentNM()->mkNode( kind::AND, b11, b12, b13 ); Node b2 = skt.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ); - Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ) ); + Node lemma = NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ); new_nodes.push_back( lemma ); retNode = skt; } else if( t.getKind() == kind::STRING_STRIDOF ) { @@ -121,18 +121,18 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone ); new_nodes.push_back( krange ); - krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk) ); + krange = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk); new_nodes.push_back( krange ); - krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero) ); + krange = NodeManager::currentNM()->mkNode( kind::GT, NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero); new_nodes.push_back( krange ); - Node start_valid = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ, t[2], d_zero) ); + Node start_valid = NodeManager::currentNM()->mkNode( kind::GEQ, t[2], d_zero); //str.len(s1) < y + str.len(s2) - Node c1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::GT, - NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )), - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ))); + Node c1 = NodeManager::currentNM()->mkNode( kind::GT, + NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )), + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] )); //~contain(t234, s2) - Node c3 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, st, t[1] ).negate()); + Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, st, t[1] ).negate(); //left Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, c3, start_valid.negate() ); //t3 = s2 @@ -149,7 +149,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 )) ); //right - Node right = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::AND, c4, c5, c6, start_valid )); + Node right = NodeManager::currentNM()->mkNode( kind::AND, c4, c5, c6, start_valid ); Node cond = skk.eqNode( negone ); Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right ); new_nodes.push_back( rr ); @@ -186,8 +186,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { //non-neg Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); - Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ), - NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ) ); + Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ), + NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ); Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); @@ -256,7 +256,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { svec.push_back(cc1);svec.push_back(cc2); svec.push_back(cc21); svec.push_back(cc3);svec.push_back(cc4);svec.push_back(cc5); - Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) ); + Node conc = NodeManager::currentNM()->mkNode(kind::AND, svec); conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, nonneg, conc ); @@ -332,7 +332,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate(); vec_n.push_back(g); } - Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n)); + Node cc2 = NodeManager::currentNM()->mkNode(kind::AND, vec_n); //cc3 Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2); @@ -366,7 +366,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { ufMx))); vec_c3b.push_back(c3cc); c3cc = NodeManager::currentNM()->mkNode(kind::AND, vec_c3b); - c3cc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, c3cc) ); + c3cc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, c3cc); c3cc = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, c3cc); vec_c3.push_back(c3cc); //unbound @@ -389,6 +389,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" ); Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" ); Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y ); + cond = NodeManager::currentNM()->mkNode( kind::AND, cond, NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) ); Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) ); Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) ); Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, @@ -397,11 +398,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { NodeManager::currentNM()->mkNode(kind::MINUS, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate(); - Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, - NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3), - skw.eqNode(x) ) ); - new_nodes.push_back( rr ); - rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) ); + Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, + NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3), + skw.eqNode(x) ); new_nodes.push_back( rr ); retNode = skw; } else if( t.getKind() == kind::STRING_STRCTN ){ |