Minor fixes for rec-fun (#1616)

4 files changed, 65 insertions, 14 deletions

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index d80a7cf82..25e5bbb5f 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -14,12 +14,13 @@
 
 #include "theory/quantifiers/quantifiers_attributes.h"
 
-#include "theory/quantifiers_engine.h"
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/fun_def_engine.h"
 #include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -146,6 +147,21 @@ Node QuantAttributes::getFunDefBody( Node q ) {
       }else if( q[1][1]==h ){
         return q[1][0];
       }
+      else if (q[1][0].getType().isReal())
+      {
+        // solve for h in the equality
+        std::map<Node, Node> msum;
+        if (ArithMSum::getMonomialSum(q[1], msum))
+        {
+          Node veq;
+          int res = ArithMSum::isolate(h, msum, veq, EQUAL);
+          if (res != 0)
+          {
+            Assert(veq.getKind() == EQUAL);
+            return res == 1 ? veq[0] : veq[1];
+          }
+        }
+      }
     }else{
       Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
       bool pol = q[1].getKind()!=NOT;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 5586c04fb..bc298fa9c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -517,14 +517,36 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
     Assert( !h.isNull() );
     // if it is a function definition, rewrite the body independently
     Node fbody = QuantAttributes::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, false );
-    Assert( new_vars.size()==h.getNumChildren() );
-    return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) );
-  }else{
-    return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, options::elimExtArithQuant() );
-  }
+    if (!fbody.isNull())
+    {
+      Node r = computeProcessTerms2(fbody,
+                                    true,
+                                    true,
+                                    curr_cond,
+                                    0,
+                                    cache,
+                                    icache,
+                                    new_vars,
+                                    new_conds,
+                                    false);
+      Assert(new_vars.size() == h.getNumChildren());
+      return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r));
+    }
+    // It can happen that we can't infer the shape of the function definition,
+    // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to
+    // forall xy. false.
+  }
+  return computeProcessTerms2(body,
+                              true,
+                              true,
+                              curr_cond,
+                              0,
+                              cache,
+                              icache,
+                              new_vars,
+                              new_conds,
+                              options::elimExtArithQuant());
 }
 
 Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
@@ -1917,7 +1939,16 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs );
     return nn.negate();
   }else if( n.getKind()==kind::FORALL ){
-    if( polarity ){
+    if (n.getNumChildren() == 3)
+    {
+      // Do not pre-skolemize quantified formulas with three children.
+      // This includes non-standard quantified formulas
+      // like recursive function definitions, or sygus conjectures, and
+      // quantified formulas with triggers.
+      return n;
+    }
+    else if (polarity)
+    {
       if( options::preSkolemQuant() && options::preSkolemQuantNested() ){
         vector< Node > children;
         children.push_back( n[0] );
@@ -1932,9 +1963,6 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
         }
         //process body
         children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) );
-        if( n.getNumChildren()==3 ){
-          children.push_back( n[2] );
-        }
         //return processed quantifier
         return NodeManager::currentNM()->mkNode( kind::FORALL, children );
       }
diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am
index 7d3da3654..159f2e088 100644
--- a/test/regress/regress1/quantifiers/Makefile.am
+++ b/test/regress/regress1/quantifiers/Makefile.am
@@ -79,7 +79,8 @@ TESTS =	\
 	RND-small.smt2 \
 	RNDPRE_4_1-dd-nqe.smt2 \
 	set8.smt2 \
-	z3.620661-no-fv-trigger.smt2
+	z3.620661-no-fv-trigger.smt2 \
+	arith-rec-fun.smt2
 
 # removed because they take more than 20s
 #		javafe.ast.ArrayInit.35.smt2
diff --git a/test/regress/regress1/quantifiers/arith-rec-fun.smt2 b/test/regress/regress1/quantifiers/arith-rec-fun.smt2
new file mode 100644
index 000000000..8133db8dd
--- /dev/null
+++ b/test/regress/regress1/quantifiers/arith-rec-fun.smt2
@@ -0,0 +1,6 @@
+(set-logic UFLIA)
+(set-info :status unsat)
+(define-fun-rec sumr ((x Int)) Int 
+    (+ x (ite (> x 0) (sumr (- x 1)) 0)))
+(assert (= (sumr 2) 2))
+(check-sat)