Bug fix rewriter for fun defs.

6 files changed, 53 insertions, 15 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 );
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)