From: ajreynol Date: Tue, 19 Jul 2016 15:32:37 +0000 (-0500) Subject: Add infrastructure for tracking instantiation lemmas (for proofs, and minimization... X-Git-Tag: cvc5-1.0.0~6040^2~43 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=06d91e9121ecdadfc96d6175792992395833329f;p=cvc5.git Add infrastructure for tracking instantiation lemmas (for proofs, and minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup. --- 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 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& 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; i0 ){ 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; i0 ){ 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; i0 ) 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; i0 ) 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; isecond; - } -} - -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& 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& 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; imkNode( 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; isecond.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; imkNode( 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; igetNextDecisionRequest(); 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 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 ){ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 7d02af77d..a477b9f2f 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -84,7 +84,8 @@ TESTS = \ inst-max-level-segf.smt2 \ small-bug1-fixpoint-3.smt2 \ z3.620661-no-fv-trigger.smt2 \ - bug_743.smt2 + bug_743.smt2 \ + quaternion_ds1_symm_0428.fof.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 b/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 new file mode 100644 index 000000000..9b0216e58 --- /dev/null +++ b/test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2 @@ -0,0 +1,49 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat +(set-logic AUFLIRA) +(set-info :status unsat) +(declare-fun def () Real) +(declare-fun h_ds1_filter () (Array Int (Array Int Real))) +(declare-fun id_ds1_filter () (Array Int (Array Int Real))) +(declare-fun pminus_ds1_filter () (Array Int (Array Int Real))) +(declare-fun pv5 () Int) +(declare-fun q_ds1_filter () (Array Int (Array Int Real))) +(declare-fun r_ds1_filter () (Array Int (Array Int Real))) +(declare-fun use () Real) +(declare-fun uniform_int_rnd (Int Int) Int) +(declare-fun abs_ (Real) Real) +(declare-fun log (Real) Real) +(declare-fun exp (Real) Real) +(declare-fun cos (Real) Real) +(declare-fun sin (Real) Real) +(declare-fun sqrt (Real) Real) +(declare-fun divide (Real Real) Real) +(declare-fun cond (Int Real Real) Real) +(declare-fun tptp_term_equal (Real Real) Int) +(declare-fun tptp_term_equals (Real Real) Int) +(declare-fun tptp_term_and (Real Real) Int) +(declare-fun sum (Int Int Real) Real) +(declare-fun dim (Int Int) Int) +(declare-fun trans ((Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun inv ((Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun tptp_mmul ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun tptp_madd ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun tptp_msub ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real))) +(declare-fun tptp_const_array1 (Int Real) (Array Int Real)) +(declare-fun tptp_const_array2 (Int Int Real) (Array Int (Array Int Real))) +(assert (forall ((?X_0 Int) (?C_1 Int)) (=> (>= ?X_0 0) (<= (uniform_int_rnd ?C_1 ?X_0) ?X_0)))) +(assert (forall ((?X_2 Int) (?C_3 Int)) (=> (>= ?X_2 0) (>= (uniform_int_rnd ?C_3 ?X_2) 0)))) +(assert (forall ((?I_4 Int) (?L_5 Int) (?U_6 Int) (?Val_7 Real)) (=> (and (<= ?L_5 ?I_4) (<= ?I_4 ?U_6)) (= (select (tptp_const_array1 (dim ?L_5 ?U_6) ?Val_7) ?I_4) ?Val_7)))) +(assert (forall ((?I_8 Int) (?L1_9 Int) (?U1_10 Int) (?J_11 Int) (?L2_12 Int) (?U2_13 Int) (?Val_14 Real)) (=> (and (and (and (<= ?L1_9 ?I_8) (<= ?I_8 ?U1_10)) (<= ?L2_12 ?J_11)) (<= ?J_11 ?U2_13)) (= (select (select (tptp_const_array2 (dim ?L1_9 ?U1_10) (dim ?L2_12 ?U2_13) ?Val_14) ?I_8) ?J_11) ?Val_14)))) +(assert (forall ((?I0_15 Int) (?J0_16 Int) (?A_17 (Array Int (Array Int Real))) (?B_18 (Array Int (Array Int Real))) (?N_19 Int)) (let ((?v_0 (tptp_mmul ?A_17 (tptp_mmul ?B_18 (trans ?A_17))))) (=> (and (and (and (and (>= ?I0_15 0) (<= ?I0_15 ?N_19)) (>= ?J0_16 0)) (<= ?J0_16 ?N_19)) (= (select (select ?B_18 ?I0_15) ?J0_16) (select (select ?B_18 ?J0_16) ?I0_15))) (= (select (select ?v_0 ?I0_15) ?J0_16) (select (select ?v_0 ?J0_16) ?I0_15)))))) +(assert (forall ((?I0_20 Int) (?J0_21 Int) (?I_22 Int) (?J_23 Int) (?A_24 (Array Int (Array Int Real))) (?B_25 (Array Int (Array Int Real))) (?N_26 Int) (?M_27 Int)) (let ((?v_0 (tptp_mmul ?A_24 (tptp_mmul ?B_25 (trans ?A_24))))) (=> (and (and (and (and (and (and (and (and (>= ?I0_20 0) (<= ?I0_20 ?N_26)) (>= ?J0_21 0)) (<= ?J0_21 ?N_26)) (>= ?I_22 0)) (<= ?I_22 ?M_27)) (>= ?J_23 0)) (<= ?J_23 ?M_27)) (= (select (select ?B_25 ?I_22) ?J_23) (select (select ?B_25 ?J_23) ?I_22))) (= (select (select ?v_0 ?I0_20) ?J0_21) (select (select ?v_0 ?J0_21) ?I0_20)))))) +(assert (forall ((?I_28 Int) (?J_29 Int) (?A_30 (Array Int (Array Int Real))) (?B_31 (Array Int (Array Int Real))) (?N_32 Int)) (let ((?v_0 (tptp_madd ?A_30 ?B_31))) (=> (and (and (and (and (and (>= ?I_28 0) (<= ?I_28 ?N_32)) (>= ?J_29 0)) (<= ?J_29 ?N_32)) (= (select (select ?A_30 ?I_28) ?J_29) (select (select ?A_30 ?J_29) ?I_28))) (= (select (select ?B_31 ?I_28) ?J_29) (select (select ?B_31 ?J_29) ?I_28))) (= (select (select ?v_0 ?I_28) ?J_29) (select (select ?v_0 ?J_29) ?I_28)))))) +(assert (forall ((?I_33 Int) (?J_34 Int) (?A_35 (Array Int (Array Int Real))) (?B_36 (Array Int (Array Int Real))) (?N_37 Int)) (let ((?v_0 (tptp_msub ?A_35 ?B_36))) (=> (and (and (and (and (and (>= ?I_33 0) (<= ?I_33 ?N_37)) (>= ?J_34 0)) (<= ?J_34 ?N_37)) (= (select (select ?A_35 ?I_33) ?J_34) (select (select ?A_35 ?J_34) ?I_33))) (= (select (select ?B_36 ?I_33) ?J_34) (select (select ?B_36 ?J_34) ?I_33))) (= (select (select ?v_0 ?I_33) ?J_34) (select (select ?v_0 ?J_34) ?I_33)))))) +(assert (forall ((?I_38 Int) (?J_39 Int) (?A_40 (Array Int (Array Int Real))) (?N_41 Int)) (let ((?v_0 (trans ?A_40))) (=> (and (and (and (and (>= ?I_38 0) (<= ?I_38 ?N_41)) (>= ?J_39 0)) (<= ?J_39 ?N_41)) (= (select (select ?A_40 ?I_38) ?J_39) (select (select ?A_40 ?J_39) ?I_38))) (= (select (select ?v_0 ?I_38) ?J_39) (select (select ?v_0 ?J_39) ?I_38)))))) +(assert (forall ((?I_42 Int) (?J_43 Int) (?A_44 (Array Int (Array Int Real))) (?N_45 Int)) (let ((?v_0 (inv ?A_44))) (=> (and (and (and (and (>= ?I_42 0) (<= ?I_42 ?N_45)) (>= ?J_43 0)) (<= ?J_43 ?N_45)) (= (select (select ?A_44 ?I_42) ?J_43) (select (select ?A_44 ?J_43) ?I_42))) (= (select (select ?v_0 ?I_42) ?J_43) (select (select ?v_0 ?J_43) ?I_42)))))) +(assert (forall ((?I0_46 Int) (?J0_47 Int) (?I_48 Int) (?J_49 Int) (?A_50 (Array Int (Array Int Real))) (?B_51 (Array Int (Array Int Real))) (?C_52 (Array Int (Array Int Real))) (?D_53 (Array Int (Array Int Real))) (?E_54 (Array Int (Array Int Real))) (?F_55 (Array Int (Array Int Real))) (?N_56 Int) (?M_57 Int)) (let ((?v_0 (tptp_madd ?A_50 (tptp_mmul ?B_51 (tptp_mmul (tptp_madd (tptp_mmul ?C_52 (tptp_mmul ?D_53 (trans ?C_52))) (tptp_mmul ?E_54 (tptp_mmul ?F_55 (trans ?E_54)))) (trans ?B_51)))))) (=> (and (and (and (and (and (and (and (and (and (and (>= ?I0_46 0) (<= ?I0_46 ?N_56)) (>= ?J0_47 0)) (<= ?J0_47 ?N_56)) (>= ?I_48 0)) (<= ?I_48 ?M_57)) (>= ?J_49 0)) (<= ?J_49 ?M_57)) (= (select (select ?D_53 ?I_48) ?J_49) (select (select ?D_53 ?J_49) ?I_48))) (= (select (select ?A_50 ?I0_46) ?J0_47) (select (select ?A_50 ?J0_47) ?I0_46))) (= (select (select ?F_55 ?I0_46) ?J0_47) (select (select ?F_55 ?J0_47) ?I0_46))) (= (select (select ?v_0 ?I0_46) ?J0_47) (select (select ?v_0 ?J0_47) ?I0_46)))))) +(assert (forall ((?Body_58 Real)) (= (sum 0 (- 1) ?Body_58) 0.0))) +(assert (not (= def use))) +(assert (not (=> (and (and (and (and (and (and (>= pv5 0) (<= pv5 998)) (> pv5 0)) (forall ((?A_59 Int) (?B_60 Int)) (=> (and (and (and (>= ?A_59 0) (>= ?B_60 0)) (<= ?A_59 5)) (<= ?B_60 5)) (= (select (select q_ds1_filter ?A_59) ?B_60) (select (select q_ds1_filter ?B_60) ?A_59))))) (forall ((?C_61 Int) (?D_62 Int)) (=> (and (and (and (>= ?C_61 0) (>= ?D_62 0)) (<= ?C_61 2)) (<= ?D_62 2)) (= (select (select r_ds1_filter ?C_61) ?D_62) (select (select r_ds1_filter ?D_62) ?C_61))))) (forall ((?E_63 Int) (?F_64 Int)) (=> (and (and (and (>= ?E_63 0) (>= ?F_64 0)) (<= ?E_63 5)) (<= ?F_64 5)) (= (select (select pminus_ds1_filter ?E_63) ?F_64) (select (select pminus_ds1_filter ?F_64) ?E_63))))) (forall ((?G_65 Int)) (=> (and (>= ?G_65 0) (<= ?G_65 5)) (forall ((?H_66 Int)) (=> (and (>= ?H_66 0) (<= ?H_66 5)) (= (select (select id_ds1_filter ?G_65) ?H_66) (select (select id_ds1_filter ?H_66) ?G_65))))))) (forall ((?I_67 Int) (?J_68 Int)) (let ((?v_0 (trans h_ds1_filter))) (let ((?v_1 (tptp_mmul pminus_ds1_filter (tptp_mmul ?v_0 (inv (tptp_madd r_ds1_filter (tptp_mmul h_ds1_filter (tptp_mmul pminus_ds1_filter ?v_0)))))))) (let ((?v_2 (tptp_mmul ?v_1 (tptp_mmul r_ds1_filter (trans ?v_1))))) (=> (and (and (and (>= ?I_67 0) (>= ?J_68 0)) (<= ?I_67 5)) (<= ?J_68 5)) (= (select (select ?v_2 ?I_67) ?J_68) (select (select ?v_2 ?J_68) ?I_67)))))))))) +(check-sat) +(exit)