New beta-reduction for HOL solving (#2869)

3 files changed, 110 insertions, 11 deletions

diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 3eb59e5fc..0583cfa1a 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -20,8 +20,10 @@
 #ifndef __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
 #define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
 
+#include "expr/node_algorithm.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
+#include "options/uf_options.h"
 
 namespace CVC4 {
 namespace theory {
@@ -46,19 +48,52 @@ public:
     }
     if(node.getKind() == kind::APPLY_UF) {
       if( node.getOperator().getKind() == kind::LAMBDA ){
+        Trace("uf-ho-beta")
+          << "uf-ho-beta : beta-reducing all args of : " << node << "\n";
         TNode lambda = node.getOperator();
-        std::vector<TNode> vars;
-        std::vector<TNode> subs;
-        for (const TNode& v : lambda[0])
+        Node ret;
+        // build capture-avoiding substitution since in HOL shadowing may have
+        // been introduced
+        if (options::ufHo())
         {
-          vars.push_back(v);
+          std::vector<Node> vars;
+          std::vector<Node> subs;
+          for (const Node& v : lambda[0])
+          {
+            vars.push_back(v);
+          }
+          for (const Node& s : node)
+          {
+            subs.push_back(s);
+          }
+          if (Trace.isOn("uf-ho-beta"))
+          {
+            Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size()
+                                << " vars into " << subs.size() << " terms :\n";
+            for (unsigned i = 0, size = subs.size(); i < size; ++i)
+            {
+              Trace("uf-ho-beta") << "uf-ho-beta: .... " << vars[i] << " |-> "
+                                  << subs[i] << "\n";
+            }
+          }
+          ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs);
+          Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n";
         }
-        for (const TNode& s : node)
+        else
         {
-          subs.push_back(s);
+          std::vector<TNode> vars;
+          std::vector<TNode> subs;
+          for (const TNode& v : lambda[0])
+          {
+            vars.push_back(v);
+          }
+          for (const TNode& s : node)
+          {
+            subs.push_back(s);
+          }
+          ret = lambda[1].substitute(
+              vars.begin(), vars.end(), subs.begin(), subs.end());
         }
-        Node ret = lambda[1].substitute(
-            vars.begin(), vars.end(), subs.begin(), subs.end());
         return RewriteResponse(REWRITE_AGAIN_FULL, ret);
       }else if( !canUseAsApplyUfOperator( node.getOperator() ) ){
         return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node));
@@ -66,9 +101,12 @@ public:
     }else if( node.getKind() == kind::HO_APPLY ){
       if( node[0].getKind() == kind::LAMBDA ){
         // resolve one argument of the lambda
-        TNode arg = Rewriter::rewrite( node[1] );
-        TNode var = node[0][0][0];
-        Node new_body = node[0][1].substitute( var, arg );
+        Trace("uf-ho-beta")
+            << "uf-ho-beta : beta-reducing one argument of : " << node[0]
+            << " with " << node[1] << "\n";
+
+        // reconstruct the lambda first to avoid variable shadowing
+        Node new_body = node[0][1];
         if( node[0][0].getNumChildren()>1 ){
           std::vector< Node > new_vars;
           for( unsigned i=1; i<node[0][0].getNumChildren(); i++ ){
@@ -78,7 +116,26 @@ public:
           largs.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, new_vars ) );
           largs.push_back( new_body );
           new_body = NodeManager::currentNM()->mkNode( kind::LAMBDA, largs );
+          Trace("uf-ho-beta")
+            << "uf-ho-beta : ....new lambda : " << new_body << "\n";
+        }
+
+        // build capture-avoiding substitution since in HOL shadowing may have
+        // been introduced
+        if (options::ufHo())
+        {
+          Node arg = Rewriter::rewrite(node[1]);
+          Node var = node[0][0][0];
+          new_body = expr::substituteCaptureAvoiding(new_body, var, arg);
+        }
+        else
+        {
+          TNode arg = Rewriter::rewrite(node[1]);
+          TNode var = node[0][0][0];
+          new_body = new_body.substitute(var, arg);
         }
+        Trace("uf-ho-beta")
+            << "uf-ho-beta : ..new body : " << new_body << "\n";
         return RewriteResponse( REWRITE_AGAIN_FULL, new_body );
       }
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9b1ce17e4..fb0e358e2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -476,6 +476,7 @@ set(regress_0_tests
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
   regress0/ho/modulo-func-equality.smt2
+  regress0/ho/shadowing-defs.smt2
   regress0/ho/simple-matching-partial.smt2
   regress0/ho/simple-matching.smt2
   regress0/ho/trans.smt2
diff --git a/test/regress/regress0/ho/shadowing-defs.smt2 b/test/regress/regress0/ho/shadowing-defs.smt2
new file mode 100644
index 000000000..722e970b6
--- /dev/null
+++ b/test/regress/regress0/ho/shadowing-defs.smt2
@@ -0,0 +1,41 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unknown
+(set-logic ALL)
+(declare-sort $$unsorted 0)
+(declare-sort mu 0)
+
+(declare-fun mnot ((-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mnot (lambda ((Phi (-> $$unsorted Bool)) (W $$unsorted)) (not (Phi W)))))
+
+(declare-fun mor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mor (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) (or (Phi W) (Psi W)))))
+
+(declare-fun mand ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mand (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mor (mnot Phi) (mnot Psi)) __flatten_var_0))))
+
+(declare-fun mimplies ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mimplies (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mor (mnot Phi) Psi __flatten_var_0))))
+
+(declare-fun mforall_ind ((-> mu $$unsorted Bool) $$unsorted) Bool)
+(assert (= mforall_ind (lambda ((Phi (-> mu $$unsorted Bool)) (W $$unsorted)) (forall ((X mu)) (Phi X W) ))))
+
+(declare-fun mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mbox (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) ))))
+
+(declare-fun mvalid ((-> $$unsorted Bool)) Bool)
+(assert (= mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (Phi W) ))))
+
+(declare-fun a1 ($$unsorted $$unsorted) Bool)
+(declare-fun a2 ($$unsorted $$unsorted) Bool)
+(declare-fun a3 ($$unsorted $$unsorted) Bool)
+
+(declare-fun jan () mu)
+(declare-fun cola () mu)
+
+(declare-fun likes (mu mu $$unsorted) Bool)
+
+(declare-fun very_much_likes (mu mu $$unsorted) Bool)
+
+(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mbox a3 (mimplies (mand (likes X Y) (mand (mbox a1 (likes X Y)) (mbox a2 (likes X Y)))) (very_much_likes X Y)) __flatten_var_0)) __flatten_var_0)))))
+
+(check-sat)
\ No newline at end of file