From 97470da31e14104f807fb33b2b3423e583e10726 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 11 Nov 2015 10:54:32 +0100 Subject: Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation. --- src/theory/quantifiers/ceg_instantiator.cpp | 24 +++++++++---- src/theory/quantifiers/inst_strategy_cbqi.cpp | 8 +++-- src/theory/quantifiers/quantifiers_rewriter.cpp | 46 +++++++++++++++---------- src/theory/quantifiers/quantifiers_rewriter.h | 4 +-- src/theory/quantifiers_engine.cpp | 11 +++++- 5 files changed, 64 insertions(+), 29 deletions(-) (limited to 'src/theory') diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 2530402ff..47281819f 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -321,8 +321,7 @@ bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::ve bool pol = lit.getKind()!=NOT; if( pvtn.isReal() ){ //arithmetic inequalities and disequalities - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ - Assert( atom[0].getType().isInteger() || atom[0].getType().isReal() ); + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ Assert( atom.getKind()!=GEQ || atom[1].isConst() ); Node atom_lhs; Node atom_rhs; @@ -664,6 +663,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b } //must ensure variables have been computed for n computeProgVars( n ); + Assert( d_inelig.find( n )==d_inelig.end() ); //substitute into previous substitutions, when applicable std::vector< Node > a_subs; @@ -681,6 +681,7 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b std::map< int, Node > prev_coeff; std::map< int, Node > prev_sym_subs; std::vector< Node > new_has_coeff; + Trace("cbqi-inst-debug2") << "Applying substitutions..." << std::endl; for( unsigned j=0; jmkNode( ires==-1 ? PLUS : MINUS, - NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ), + int ires_use = ( msum[pv].isNull() || msum[pv].getConst().sgn()==1 ) ? 1 : -1; + val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, + NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); Trace("cbqi-inst-debug") << "result : " << val << std::endl; Assert( val.getType().isInteger() ); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 39cde56e8..b26f24c63 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -621,8 +621,12 @@ bool InstStrategyCegqi::addLemma( Node lem ) { bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){ - //only legal if current quantified formula contains n - return TermDb::containsTerm( d_curr_quant, n ); + if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){ + return true; + }else{ + //only legal if current quantified formula contains n + return TermDb::containsTerm( d_curr_quant, n ); + } }else{ return true; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index dcf58e692..8f055473d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -83,10 +83,10 @@ bool QuantifiersRewriter::isCube( Node n ){ } } -int QuantifiersRewriter::getPurifyId( Node n ){ +int QuantifiersRewriter::getPurifyId( Node n, std::vector< Node >& args ){ if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){ return 1; - }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL ){ + }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::containsTerms( n, args ) ){ return 0; }else{ return -1; @@ -196,7 +196,6 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; - Trace("quantifiers-rewrite-debug") << "Attributes : " << std::endl; if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){ RewriteStatus status = REWRITE_DONE; Node ret = in; @@ -769,7 +768,7 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){ return body; } -bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) { +bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) { if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){ return false; }else{ @@ -777,7 +776,7 @@ bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::v 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 ); + int id = getPurifyId( s, args ); return it->second.size()==1 && it->second[0]==id; } } @@ -791,7 +790,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto 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], args, var_parent ) ){ + 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] ); args.erase( ita ); @@ -809,7 +809,8 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto 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 ) ){ + if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, args, 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 ); @@ -873,7 +874,7 @@ Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node > } } if( !vars.empty() ){ - Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl; + Trace("var-elim-quant-debug") << "VE " << vars.size() << "/" << args.size() << std::endl; //remake with eliminated nodes body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); body = Rewriter::rewrite( body ); @@ -1688,12 +1689,24 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, return it->second; }else{ Node ret = body; - if( body.getNumChildren()>0 && body.getKind()!=FORALL ){ + if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::containsTerms( ret, args ) ){ std::vector< Node > children; bool childrenChanged = false; - int id = getPurifyId( body ); + int id = getPurifyId( body, args ); for( unsigned i=0; i& args, ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); } if( parentId!=0 && parentId!=id ){ - //must purify if this has a bound variable - if( TermDb::containsTerms( ret, args ) ){ - Node v = NodeManager::currentNM()->mkBoundVar( ret.getType() ); - var_to_term[v] = Rewriter::rewrite( v.eqNode( ret ) ); - ret = v; - args.push_back( v ); - } + 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; diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index daf5a8bad..607fd9191 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -31,7 +31,7 @@ public: static bool isClause( Node n ); static bool isLiteral( Node n ); static bool isCube( Node n ); - static int getPurifyId( Node n ); + static int getPurifyId( Node n, std::vector< Node >& args ); private: static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); @@ -41,7 +41,7 @@ private: static Node computeClause( Node n ); 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, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ); 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, diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 990d3389e..584295c17 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -709,7 +709,16 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v Trace("inst") << std::endl; } if( options::cbqi() ){ - if( quantifiers::TermDb::getInstConstAttr(terms[i])==f ){ + Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]); + bool bad_inst = false; + if( !icf.isNull() ){ + if( icf==f ){ + bad_inst = true; + }else{ + bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[f] ); + } + } + if( bad_inst ){ Trace("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; for( unsigned i=0; i