diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-18 22:33:22 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-18 22:33:22 +0100 |
commit | 4d3e24e52765b03d8e6f36afe7de6168e8740693 (patch) | |
tree | c5b3e7230e56db21cef630bbc95d94b7e3476618 /src | |
parent | 9d677333439c15677b6891ee8f6bd368a5df9f0a (diff) |
Bug fix rewriter for fun defs.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 36 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 8 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 1 |
3 files changed, 32 insertions, 13 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index b92d72ef4..fc5b692b2 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -557,15 +557,33 @@ void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::v } } -Node QuantifiersRewriter::computeProcessTerms( 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 ) { +Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q ){ + std::map< Node, bool > curr_cond; + std::map< Node, Node > cache; + std::map< Node, Node > icache; + Node h = TermDb::getFunDefHead( q ); + if( !h.isNull() ){ + // if it is a function definition, rewrite the body independently + Node fbody = TermDb::getFunDefBody( q ); + Assert( !body.isNull() ); + Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; + Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds ); + return Rewriter::rewrite( NodeManager::currentNM()->mkNode( h.getType().isBoolean() ? IFF : EQUAL, h, r ) ); + }else{ + return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds ); + } +} + +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 ) { Node ret; std::map< Node, Node >::iterator iti = cache.find( body ); if( iti!=cache.end() ){ ret = iti->second; }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; @@ -581,15 +599,15 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, bool hasPol, bool pol, bool newHasPol; bool newPol; QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); - Node nn = computeProcessTerms( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); if( body.getKind()==ITE ){ if( i==0 ){ int res = getEntailedCond( nn, currCond ); if( res==1 ){ - ret = computeProcessTerms( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); break; }else if( res==-1 ){ - ret = computeProcessTerms( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); break; } }else{ @@ -1478,11 +1496,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp }else if( computeOption==COMPUTE_NNF ){ n = computeNNF( n ); }else if( computeOption==COMPUTE_PROCESS_TERMS ){ - std::map< Node, bool > curr_cond; - std::map< Node, Node > cache; - std::map< Node, Node > icache; std::vector< Node > new_conds; - n = computeProcessTerms( n, true, true, curr_cond, 0, cache, icache, args, new_conds ); + n = computeProcessTerms( n, args, new_conds, f ); if( !new_conds.empty() ){ new_conds.push_back( n ); n = NodeManager::currentNM()->mkNode( OR, new_conds ); @@ -1823,3 +1838,4 @@ void QuantifiersRewriter::computePurifyExpand( Node body, std::vector< Node >& c //Node attr = NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, body ); } } + diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index f07b635dc..38c1bdd58 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -41,6 +41,9 @@ private: static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); + static Node 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 ); 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 ); @@ -56,9 +59,7 @@ private: static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); static Node computeNNF( Node body ); //cache is dependent upon currCond, icache is not, new_conds are negated conditions - static Node computeProcessTerms( 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 ); + static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q ); static Node computeCondSplit( Node body, Node ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); @@ -102,3 +103,4 @@ public: #endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ + diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 5ddb1c31a..2a8e21059 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -591,6 +591,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if( options::finiteModelFind() ){ tep.d_fixed_usort_card = true; for( std::map< TypeNode, unsigned >::iterator it = eqc_usort_count.begin(); it != eqc_usort_count.end(); ++it ){ + Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : " << it->second << std::endl; tep.d_fixed_card[it->first] = Integer(it->second); } typeConstSet.setTypeEnumeratorProperties( &tep ); |