diff options
-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 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 11 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/RND_4_16.smt2 | 10 |
7 files changed, 76 insertions, 30 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, 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<terms.size(); i++ ){ Trace("inst") << " " << terms[i] << std::endl; diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 939b0d22c..7178710cb 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -63,7 +63,8 @@ TESTS = \ mix-match.smt2 \ ari056.smt2 \ ext-ex-deq-trigger.smt2 \ - matching-lia-1arg.smt2 + matching-lia-1arg.smt2 \ + RND_4_16.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/RND_4_16.smt2 b/test/regress/regress0/quantifiers/RND_4_16.smt2 new file mode 100644 index 000000000..2bdb1f56e --- /dev/null +++ b/test/regress/regress0/quantifiers/RND_4_16.smt2 @@ -0,0 +1,10 @@ +(set-logic LRA) +(set-info :status unsat) +(declare-fun y2 () Real) +(declare-fun y3 () Real) +(declare-fun y4 () Real) +(declare-fun x1 () Real) +(declare-fun y1 () Real) +(assert (or (and (and (and (exists ((?y2 Real)) (or (forall ((?y3 Real)) (forall ((?y4 Real)) (or (< (+ (+ (* (- 53) ?y4) (* 77 ?y3)) (* 51 ?y2)) 79) (not (= (* (- 56) ?y4) 0))))) (or (exists ((?y3 Real)) (not (= (+ (* (- 94) ?y2) (* 90 x1)) (- 54)))) (and (<= (+ (* (- 28) ?y2) (* 4 x1)) 62) (exists ((?y3 Real)) (>= (+ (+ (* (- 83) ?y3) (* (- 2) ?y2)) (* 78 x1)) 34)))))) (forall ((?y1 Real)) (forall ((?y2 Real)) (and (forall ((?y4 Real)) (or (= (+ (* (- 27) ?y1) (* (- 64) x1)) 12) (< (+ (+ (* (- 91) ?y4) (* (- 61) ?y1)) (* 20 x1)) 25))) (or (forall ((?y4 Real)) (> (+ (+ (+ (* 22 ?y4) (* (- 35) ?y2)) (* (- 77) ?y1)) (* (- 78) x1)) (- 49))) (and (= (+ (* (- 55) ?y1) (* (- 71) x1)) 51) (<= (* (- 2) ?y1) 0))))))) (or (and (forall ((?y1 Real)) (exists ((?y2 Real)) (forall ((?y3 Real)) (and (>= (+ (* (- 42) ?y2) (* (- 88) ?y1)) 0) (not (= (+ (* 94 ?y3) (* (- 41) ?y2)) 20)))))) (exists ((?y1 Real)) (forall ((?y2 Real)) (exists ((?y3 Real)) (forall ((?y4 Real)) (or (<= (+ (+ (* 84 ?y4) (* 79 ?y3)) (* 42 ?y2)) 5) (= (+ (+ (* (- 58) ?y3) (* (- 13) ?y2)) (* 93 x1)) (- 1)))))))) (or (and (or (= (* 21 x1) (- 18)) (>= (* 76 x1) 0)) (or (>= (* (- 79) x1) 61) (>= (* (- 32) x1) (- 26)))) (and (and (or (>= (* (- 44) x1) 58) (not (= (* (- 68) x1) (- 93)))) (forall ((?y3 Real)) (>= (* (- 14) x1) 91))) (forall ((?y2 Real)) (and (and (> (* (- 65) x1) 74) (>= (+ (* 27 ?y2) (* (- 84) x1)) (- 68))) (and (>= (+ (* 11 ?y2) (* (- 77) x1)) 0) (< (+ (* (- 67) ?y2) (* (- 42) x1)) 88)))))))) (forall ((?y1 Real)) (exists ((?y2 Real)) (exists ((?y3 Real)) (forall ((?y4 Real)) (let ((?v_0 (* 66 ?y4))) (and (or (>= (+ (+ (+ (* 48 ?y4) (* (- 47) ?y3)) (* 1 ?y1)) (* 38 x1)) 61) (>= (+ (+ (* (- 19) ?y4) (* (- 80) ?y3)) (* (- 66) ?y2)) 25)) (or (or (and (<= (+ (+ (* (- 4) ?y4) (* (- 22) ?y2)) (* (- 18) ?y1)) (- 28)) (not (= (+ (+ (+ (* 1 ?y3) (* 20 ?y2)) (* (- 42) ?y1)) (* 74 x1)) (- 63)))) (and (= (+ (+ (+ (* 13 ?y3) (* (- 7) ?y2)) (* 52 ?y1)) (* 94 x1)) 0) (< (+ (+ (+ (+ (* 87 ?y4) (* (- 36) ?y3)) (* 55 ?y2)) (* (- 99) ?y1)) (* (- 56) x1)) (- 98)))) (or (or (not (= (+ (+ (+ (+ (* 73 ?y4) (* (- 15) ?y3)) (* 52 ?y2)) (* 12 ?y1)) (* 69 x1)) 72)) (<= (+ (+ ?v_0 (* (- 89) ?y1)) (* (- 49) x1)) 47)) (and (>= (+ (+ (* 82 ?y3) (* 69 ?y2)) (* 67 ?y1)) 10) (= (+ (+ (+ ?v_0 (* 4 ?y3)) (* 21 ?y2)) (* (- 35) ?y1)) 77))))))))))) (exists ((?y1 Real)) (forall ((?y2 Real)) (and (forall ((?y3 Real)) (forall ((?y4 Real)) (let ((?v_1 (* (- 41) ?y2))) (or (and (and (not (= (+ (+ (+ (* 33 ?y3) (* 7 ?y2)) (* 84 ?y1)) (* (- 79) x1)) 0)) (and (< (+ (+ (+ (* 57 ?y4) ?v_1) (* (- 82) ?y1)) (* (- 5) x1)) 40) (>= (+ (+ (+ (* 18 ?y3) (* (- 64) ?y2)) (* (- 87) ?y1)) (* (- 37) x1)) 16))) (and (or (not (= (+ (+ (+ (+ (* (- 19) ?y4) (* (- 74) ?y3)) (* 40 ?y2)) (* (- 73) ?y1)) (* (- 81) x1)) (- 6))) (< (+ (+ (+ (* (- 86) ?y4) (* (- 83) ?y2)) (* 46 ?y1)) (* (- 74) x1)) 94)) (or (> (+ (* (- 69) ?y2) (* (- 45) ?y1)) 0) (>= (+ (+ (* 16 ?y4) (* (- 18) ?y3)) (* (- 92) ?y2)) (- 32))))) (and (and (or (not (= (+ (+ (+ (* 11 ?y4) (* 75 ?y3)) (* 6 ?y1)) (* (- 63) x1)) 57)) (not (= (+ (+ (+ (+ (* (- 90) ?y4) (* 48 ?y3)) (* (- 94) ?y2)) (* (- 48) ?y1)) (* 96 x1)) (- 45)))) (or (>= (+ (+ (+ (* 36 ?y4) (* 67 ?y3)) (* 11 ?y2)) (* (- 84) x1)) (- 8)) (>= (+ (+ (* 75 ?y4) (* (- 65) ?y2)) (* (- 77) x1)) 34))) (or (or (> (+ (* 70 ?y1) (* (- 85) x1)) 0) (<= (+ (* 3 ?y2) (* (- 78) ?y1)) (- 7))) (and (= (+ (+ (* 44 ?y4) ?v_1) (* 48 x1)) 0) (< (+ (+ (+ (+ (* 27 ?y4) (* (- 24) ?y3)) (* 89 ?y2)) (* (- 93) ?y1)) (* 65 x1)) (- 17))))))))) (forall ((?y4 Real)) (let ((?v_2 (* 11 x1))) (and (and (or (and (< (* 99 ?y4) (- 32)) (<= (+ (+ (* 47 ?y4) (* (- 90) ?y1)) (* 78 x1)) (- 33))) (= (+ (* (- 19) ?y2) (* (- 97) ?y1)) 5)) (and (and (<= (+ (+ (* (- 54) ?y2) (* (- 87) ?y1)) (* (- 32) x1)) 51) (> (+ (+ (+ (* 46 ?y4) (* (- 11) ?y2)) (* (- 68) ?y1)) (* 77 x1)) 77)) (and (< (+ (+ (* 1 ?y4) (* 53 ?y2)) (* (- 60) x1)) (- 86)) (< (+ (* (- 12) ?y2) (* 38 x1)) 79)))) (or (or (>= (+ (* (- 46) ?y2) ?v_2) 37) (= (* (- 2) ?y1) 50)) (or (not (= (+ (+ (+ (* (- 95) ?y4) (* (- 96) ?y2)) (* (- 74) ?y1)) (* 59 x1)) (- 24))) (< (+ (* (- 70) ?y1) ?v_2) 0))))))))))) +(check-sat) +(exit) |