From 7acc2844df65ab6fdbf8166653c71eaa26d4d151 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 11 Feb 2016 15:07:37 -0600 Subject: More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc. --- src/theory/quantifiers/full_model_check.cpp | 4 +- src/theory/quantifiers/quant_util.cpp | 3 + src/theory/quantifiers/quantifiers_rewriter.cpp | 136 ++++++++++++++++-------- 3 files changed, 97 insertions(+), 46 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 00a5241f5..ff0da13e1 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -819,8 +819,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No } } d_addedLemmas += addedLemmas; - Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl; - return true; + Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl; + return addedLemmas>0 || !riter.d_incomplete; }else{ Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl; return false; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index fc1f052c3..bf91f74c6 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -349,6 +349,9 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& }else if( n.getKind()==ITE ){ newHasPol = (child!=0) && hasPol; newPol = pol; + }else if( n.getKind()==FORALL ){ + newHasPol = (child==1) && hasPol; + newPol = pol; }else{ newHasPol = false; newPol = pol; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 462f8377f..afe8cd598 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -391,7 +391,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ){ if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ - Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; + Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; Node x = n[0][0]; std::map< Node, Node >::iterator itp = pcons.find( x ); if( itp!=pcons.end() ){ @@ -506,35 +506,42 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ return 0; } -bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) { +bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) { std::map< Node, bool >::iterator it = currCond.find( n ); if( it==currCond.end() ){ - Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl; + Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl; new_cond.push_back( n ); currCond[n] = pol; return true; }else{ - Assert( it->second==pol ); + if( it->second!=pol ){ + Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl; + conflict = true; + } return false; } } -void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) { +void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) { if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){ for( unsigned i=0; i& currCond, std::v for( unsigned i=0; imkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] ); - addEntailedCond( t, false, currCond, new_cond ); + addEntailedCond( t, false, currCond, new_cond, conflict ); } } }else{ if( dt.getNumConstructors()==2 ){ int oindex = 1-index; Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] ); - addEntailedCond( t, true, currCond, new_cond ); + addEntailedCond( t, true, currCond, new_cond, conflict ); } } } @@ -577,59 +584,100 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds ) { + Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body << " " << hasPol << " " << pol << std::endl; Node ret; std::map< Node, Node >::iterator iti = cache.find( body ); if( iti!=cache.end() ){ ret = iti->second; + Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl; }else{ - bool do_ite = false; - //only do context dependent processing up to ITE depth 8 - if( body.getKind()==ITE && nCurrCond<8 ){ - do_ite = true; - nCurrCond = nCurrCond + 1; - } + bool firstTimeCD = true; bool changed = false; std::vector< Node > children; for( size_t i=0; i new_cond; - if( do_ite && i>0 ){ - setEntailedCond( children[0], i==1, currCond, new_cond ); - cache.clear(); + bool conflict = false; + //only do context dependent processing up to depth 8 + if( nCurrCond<8 ){ + if( firstTimeCD ){ + firstTimeCD = false; + nCurrCond = nCurrCond + 1; + } + if( Trace.isOn("quantifiers-rewrite-term-debug") ){ + //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){ + if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ + Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl; + } + } + if( body.getKind()==ITE && i>0 ){ + setEntailedCond( children[0], i==1, currCond, new_cond, conflict ); + //should not conflict (entailment check failed) + Assert( !conflict ); + } + //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){ + // bool use_pol = !pol; + if( body.getKind()==OR || body.getKind()==AND ){ + bool use_pol = body.getKind()==AND; + for( unsigned j=0; ji ){ + setEntailedCond( body[j], use_pol, currCond, new_cond, conflict ); + } + } + if( conflict ){ + Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl; + ret = NodeManager::currentNM()->mkConst( !use_pol ); + } + } + if( !new_cond.empty() ){ + cache.clear(); + } + if( Trace.isOn("quantifiers-rewrite-term-debug") ){ + //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){ + if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ + Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl; + } + } } - bool newHasPol; - bool newPol; - QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); - Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - if( body.getKind()==ITE ){ - if( i==0 ){ + if( !conflict ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); + Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + if( body.getKind()==ITE && i==0 ){ int res = getEntailedCond( nn, currCond ); + Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl; if( res==1 ){ ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - break; }else if( res==-1 ){ ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - break; - } - }else{ - if( !new_cond.empty() ){ - for( unsigned j=0; jmkNode( body.getKind(), children ); + }else{ + ret = body; } - ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); - }else{ - ret = body; } + Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl; cache[body] = ret; } -- cgit v1.2.3