From 4d3e24e52765b03d8e6f36afe7de6168e8740693 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 18 Jan 2016 22:33:22 +0100 Subject: [PATCH] Bug fix rewriter for fun defs. --- .../quantifiers/quantifiers_rewriter.cpp | 36 +++++++++++++------ src/theory/quantifiers/quantifiers_rewriter.h | 8 +++-- src/theory/theory_model.cpp | 1 + test/regress/regress0/fmf/Makefile.am | 6 ++-- test/regress/regress0/fmf/fd-false.smt2 | 6 ++++ test/regress/regress0/fmf/tail_rec.smt2 | 11 ++++++ 6 files changed, 53 insertions(+), 15 deletions(-) create mode 100644 test/regress/regress0/fmf/fd-false.smt2 create mode 100755 test/regress/regress0/fmf/tail_rec.smt2 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 ); diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 5abadbcb8..ff2591a5b 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -42,8 +42,10 @@ TESTS = \ syn002-si-real-int.smt2 \ krs-sat.smt2 \ forall_unit_data2.smt2 \ - sc_bad_model_1221.smt2 \ - dt-proper-model.smt2 + sc_bad_model_1221.smt2 \ + dt-proper-model.smt2 \ + fd-false.smt2 \ + tail_rec.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/fd-false.smt2 b/test/regress/regress0/fmf/fd-false.smt2 new file mode 100644 index 000000000..4e1ff64b5 --- /dev/null +++ b/test/regress/regress0/fmf/fd-false.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(define-fun-rec f ((x Int)) Bool false) +(assert (not (f 0))) +(check-sat) diff --git a/test/regress/regress0/fmf/tail_rec.smt2 b/test/regress/regress0/fmf/tail_rec.smt2 new file mode 100755 index 000000000..87b2d53a6 --- /dev/null +++ b/test/regress/regress0/fmf/tail_rec.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-sort elem 0) +(declare-datatypes () ((list (Nil) (Cons (hd elem) (tl list))))) +(define-fun-rec f ((x list)) elem + (ite (is-Nil x) (f x) (hd x)) +) +(declare-fun t () elem) +(assert (= t (f Nil))) +(check-sat) -- 2.30.2