Fix for get constraints method in fmf-fun (#2399)

4 files changed, 111 insertions, 44 deletions

diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index c40a7c4d9..1671fa1a0 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -211,8 +211,8 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod
         }
       }else{
         //simplify term
-        std::map< Node, bool > visited;
-        simplifyTerm( n, constraints, visited );
+        std::map<Node, Node> visited;
+        getConstraints(n, constraints, visited);
       }
       if( !constraints.empty() && isBool && hasPol ){
         //conjoin with current
@@ -247,46 +247,92 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod
   }
 }
 
-void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints, std::map< Node, bool >& visited ) {
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    Trace("fmf-fun-def-debug") << "Simplify term " << n << std::endl;
-    if( n.getKind()==ITE ){
-      simplifyTerm( n[0], constraints, visited );
-      std::vector< Node > ccons1;
-      std::vector< Node > ccons2;
-      simplifyTerm( n[1], ccons1, visited );
-      simplifyTerm( n[2], ccons2, visited );
-      if( !ccons1.empty() || !ccons2.empty() ){
-        Node n1 = ccons1.empty() ? NodeManager::currentNM()->mkConst( true ) : ( ccons1.size()==1 ? ccons1[0] : NodeManager::currentNM()->mkNode( AND, ccons1 ) );
-        Node n2 = ccons2.empty() ? NodeManager::currentNM()->mkConst( true ) : ( ccons2.size()==1 ? ccons2[0] : NodeManager::currentNM()->mkNode( AND, ccons2 ) );
-        constraints.push_back( NodeManager::currentNM()->mkNode( ITE, n[0], n1, n2 ) );
+void FunDefFmf::getConstraints(Node n,
+                               std::vector<Node>& constraints,
+                               std::map<Node, Node>& visited)
+{
+  std::map<Node, Node>::iterator itv = visited.find(n);
+  if (itv != visited.end())
+  {
+    // already visited
+    if (!itv->second.isNull())
+    {
+      // add the cached constraint if it does not already occur
+      if (std::find(constraints.begin(), constraints.end(), itv->second)
+          == constraints.end())
+      {
+        constraints.push_back(itv->second);
       }
-    }else{
-      if( n.getKind()==APPLY_UF ){
-        //check if f is defined, if so, we must enforce domain constraints for this f-application
-        Node f = n.getOperator();
-        std::map< Node, TypeNode >::iterator it = d_sorts.find( f );
-        if( it!=d_sorts.end() ){
-          //create existential
-          Node z = NodeManager::currentNM()->mkBoundVar("?z", it->second );
-          Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, z );
-          std::vector< Node > children;
-          for( unsigned j=0; j<n.getNumChildren(); j++ ){
-            Node uz = NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], z );
-            children.push_back( uz.eqNode( n[j] ) );
-          }
-          Node bd = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
-          bd = bd.negate();
-          Node ex = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
-          ex = ex.negate();
-          constraints.push_back( ex );
-          Trace("fmf-fun-def-debug") << "---> add constraint " << ex << std::endl;
+    }
+    return;
+  }
+  visited[n] = Node::null();
+  std::vector<Node> currConstraints;
+  NodeManager* nm = NodeManager::currentNM();
+  if (n.getKind() == ITE)
+  {
+    // collect constraints for the condition
+    getConstraints(n[0], currConstraints, visited);
+    // collect constraints for each branch
+    Node cs[2];
+    for (unsigned i = 0; i < 2; i++)
+    {
+      std::vector<Node> ccons;
+      getConstraints(n[i + 1], ccons, visited);
+      cs[i] = ccons.empty()
+                  ? nm->mkConst(true)
+                  : (ccons.size() == 1 ? ccons[0] : nm->mkNode(AND, ccons));
+    }
+    if (!cs[0].isConst() || !cs[1].isConst())
+    {
+      Node itec = nm->mkNode(ITE, n[0], cs[0], cs[1]);
+      currConstraints.push_back(itec);
+      Trace("fmf-fun-def-debug")
+          << "---> add constraint " << itec << " for " << n << std::endl;
+    }
+  }
+  else
+  {
+    if (n.getKind() == APPLY_UF)
+    {
+      // check if f is defined, if so, we must enforce domain constraints for
+      // this f-application
+      Node f = n.getOperator();
+      std::map<Node, TypeNode>::iterator it = d_sorts.find(f);
+      if (it != d_sorts.end())
+      {
+        // create existential
+        Node z = nm->mkBoundVar("?z", it->second);
+        Node bvl = nm->mkNode(BOUND_VAR_LIST, z);
+        std::vector<Node> children;
+        for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
+        {
+          Node uz = nm->mkNode(APPLY_UF, d_input_arg_inj[f][j], z);
+          children.push_back(uz.eqNode(n[j]));
         }
+        Node bd =
+            children.size() == 1 ? children[0] : nm->mkNode(AND, children);
+        bd = bd.negate();
+        Node ex = nm->mkNode(FORALL, bvl, bd);
+        ex = ex.negate();
+        currConstraints.push_back(ex);
+        Trace("fmf-fun-def-debug")
+            << "---> add constraint " << ex << " for " << n << std::endl;
       }
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        simplifyTerm( n[i], constraints, visited );
-      }
     }
+    for (const Node& cn : n)
+    {
+      getConstraints(cn, currConstraints, visited);
+    }
+  }
+  // set the visited cache
+  if (!currConstraints.empty())
+  {
+    Node finalc = currConstraints.size() == 1
+                      ? currConstraints[0]
+                      : nm->mkNode(AND, currConstraints);
+    visited[n] = finalc;
+    // add to constraints
+    getConstraints(n, constraints, visited);
   }
 }
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
index b59c6199a..78adc710c 100644
--- a/src/theory/quantifiers/fun_def_process.h
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -49,11 +49,6 @@ private:
   Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def,
                         std::map< int, std::map< Node, Node > >& visited,
                         std::map< int, std::map< Node, Node > >& visited_cons );
-  /** simplify term
-  * This computes constraints for the final else branch of A_0 in Figure 1 
-  * of Reynolds et al "Model Finding for Recursive Functions".
-  */
-  void simplifyTerm( Node n, std::vector< Node >& constraints, std::map< Node, bool >& visited );
 public:
   FunDefFmf(){}
   ~FunDefFmf(){}
@@ -70,6 +65,15 @@ public:
   * which are Sigma^{dfn} in that paper.
   */
   void simplify( std::vector< Node >& assertions );
+  /** get constraints
+   *
+   * This computes constraints for the final else branch of A_0 in Figure 1
+   * of Reynolds et al "Model Finding for Recursive Functions". The range of
+   * the cache visited stores the constraint (if any) for each node.
+   */
+  void getConstraints(Node n,
+                      std::vector<Node>& constraints,
+                      std::map<Node, Node>& visited);
 };
 
 
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 1c37669de..6187cb2fa 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1101,6 +1101,7 @@ REG1_TESTS = \
 	regress1/fmf/fib-core.smt2 \
 	regress1/fmf/fmf-bound-2dim.smt2 \
 	regress1/fmf/fmf-bound-int.smt2 \
+	regress1/fmf/fmf-fun-divisor-pp.smt2 \
 	regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 \
 	regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 \
 	regress1/fmf/fmf-strange-bounds.smt2 \
diff --git a/test/regress/regress1/fmf/fmf-fun-divisor-pp.smt2 b/test/regress/regress1/fmf/fmf-fun-divisor-pp.smt2
new file mode 100644
index 000000000..93bfb930d
--- /dev/null
+++ b/test/regress/regress1/fmf/fmf-fun-divisor-pp.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --fmf-fun
+; EXPECT: unsat
+(set-logic UFNIA)
+(set-info :status unsat)
+(define-fun-rec pow ((a Int)(b Int)) Int 
+    (ite (<= b 0) 
+         1 
+         (* a (pow a (- b 1)))))
+
+(declare-fun x () Int)
+
+(assert (>= x 0))
+(assert (< x (pow 2 2)))
+(assert (>= (mod (div x (pow 2 3)) (pow 2 2)) 2))
+
+(check-sat)