# 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
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
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
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];
//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;
}
}
-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();
}
}
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{
}
}
-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();
}
}
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(){}
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 */
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();
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 */
}
}
-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++ ){
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] );
}
}
}
- //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() ){
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;
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
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;
}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;
}
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() ){
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 );
- }
-}
-
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 );
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 );
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,
COMPUTE_PRENEX,
COMPUTE_VAR_ELIMINATION,
COMPUTE_COND_SPLIT,
- COMPUTE_PURIFY_EXPAND,
//COMPUTE_FLATTEN_ARGS_UF,
//COMPUTE_CNF,
COMPUTE_LAST
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
}
}
}
+ 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() ){
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 );
}
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;
}
}
}
+ 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;
}
}
+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;
}
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 ){
}
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 );
}
}
}
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,
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:
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 ) {
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
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 );
//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) );
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 );
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);
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
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,
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 ){
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
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff