From d39210bb485c13e7f3290e4e7faab9c5830f437d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Feb 2018 22:50:47 -0600
Subject: Minor fixes for rec-fun (#1616)

---
 src/theory/quantifiers/quantifiers_attributes.cpp | 20 ++++++++-
 src/theory/quantifiers/quantifiers_rewriter.cpp   | 50 ++++++++++++++++++-----
 2 files changed, 57 insertions(+), 13 deletions(-)

(limited to 'src/theory/quantifiers')

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 );
       }
-- 
cgit v1.2.3