diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-11 10:54:32 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-11 10:54:32 +0100 |
commit | 97470da31e14104f807fb33b2b3423e583e10726 (patch) | |
tree | 516e79d981cfaa0c59c6b51981ebb2fcd4c1a698 /src/theory/quantifiers | |
parent | 81dca680f6c88d10b56a0ed065d470d907766e21 (diff) |
Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 46 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 4 |
4 files changed, 54 insertions, 28 deletions
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; j<sf.d_subs.size(); j++ ){ Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() ); if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){ @@ -705,12 +706,16 @@ bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int b } if( sf.d_subs[j]!=prev_subs[j] ){ computeProgVars( sf.d_subs[j] ); + Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() ); } + Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl; }else{ - Trace("cbqi-inst-debug") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl; + Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl; success = false; break; } + }else{ + Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl; } if( options::cbqiSymLia() && pv_coeff.isNull() ){ //apply simple substitutions also to sym_subs @@ -1483,7 +1488,13 @@ int CegInstantiator::isolate( Node pv, Node atom, Node& veq_c, Node& val, Node& ires = QuantArith::isolate( pv, msum, veq_c, val, atom.getKind() ); if( ires!=0 ){ Node realPart; - Trace("cbqi-inst-debug") << "Isolate : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; + if( Trace.isOn("cbqi-inst-debug") ){ + Trace("cbqi-inst-debug") << "Isolate : "; + if( !veq_c.isNull() ){ + Trace("cbqi-inst-debug") << veq_c << " * "; + } + Trace("cbqi-inst-debug") << pv << " " << atom.getKind() << " " << val << std::endl; + } if( options::cbqiAll() ){ // when not pure LIA/LRA, we must check whether the lhs contains pv if( TermDb::containsTerm( val, pv ) ){ @@ -1529,8 +1540,9 @@ int CegInstantiator::isolate( Node pv, Node atom, Node& veq_c, Node& val, Node& Trace("cbqi-inst-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; Trace("cbqi-inst-debug") << " real part : " << realPart << std::endl; if( ires!=0 ){ - val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires==-1 ? PLUS : MINUS, - NodeManager::currentNM()->mkNode( ires==-1 ? MINUS : PLUS, val, realPart ), + int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().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<body.getNumChildren(); i++ ){ - Node bi = computePurify2( body[i], args, visited, var_to_term, var_parent, id ); + Node bi; + if( body.getKind()==EQUAL && i==1 ){ + int cid = getPurifyId( children[0], args ); + bi = computePurify2( body[i], args, visited, var_to_term, var_parent, cid ); + if( children[0].getKind()==BOUND_VARIABLE ){ + cid = getPurifyId( bi, args ); + 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 ){ @@ -1709,13 +1722,10 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& 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, |