Eliminate nested call to rewriter for beta reduction, generalize `Pro…

…ofRule::BETA_REDUCE` (cvc5#11329)

This PR does two things:
(1) 

For handling beta reductions for lambdas that are not already rewritten,
previously we would rewrite `(APPLY_UF (lambda x P) t)` ---> `(APPLY_UF
r t)` where `r` was the result of a nested call to the rewriter for
`(lambda x P)`. This is required since the rewriter does not rewrite
inside of operators. However this made it impossible to reconstruct
proofs in general.

We now rewrite `(APPLY_UF (lambda x P) t)` ---> `(HO_APPLY (lambda x P)
t)` for such cases. This allows the lambda to be rewritten naturally and
this step is easy to justify.

The caveat now is that `HO_APPLY` may be introduced for non-HO logics.
We add a case to `ppRewrite` to convert any such fully applied
`HO_APPLY` term back to `APPLY_UF`. The guarding cases in the UF solver
are changed to accomodate this.

(2) 
Generalizes `ProofRule::BETA_REDUCE` to handle (single argument) beta
reduction for `HO_APPLY`.

include/cvc5/cvc5_proof_rule.h

@@ -2471,8 +2471,18 @@ enum ENUM(ProofRewriteRule)
    *   ((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = t\{x_1 \mapsto t_1,
    *   \ldots, x_n \mapsto t_n\}
    *
-   * The right hand side of the equality in the conclusion is computed using
-   * standard substitution via ``Node::substitute``.
+   * or alternatively
+   *
+   * .. math::
+   *   ((\lambda x_1 \ldots x_n.\> t) \ t_1) = (\lambda x_2 \ldots x_n.\> t)\{x_1 \mapsto t_1\}
+   *
+   * In the former case, the left hand side may either be a term of kind
+   * `cvc5::Kind::APPLY_UF` or `cvc5::Kind::HO_APPLY`. The latter case is used
+   * only if the term has kind `cvc5::Kind::HO_APPLY`.
+   *
+   * In either case, the right hand side of the equality in the conclusion is
+   * computed using standard substitution via ``Node::substitute``.
+   *
    * \endverbatim
    */
   EVALUE(BETA_REDUCE),

proofs/eo/cpc/programs/Quantifiers.eo

@@ -87,10 +87,14 @@
 ;   whose arguments have been partially accumulated into ss.
 ; - ss @List: The accumulated list of arguments to pass to the lambda.
 ; return: the result of beta reduction.
-(program $beta_reduce ((U Type) (T Type) (S Type) (f (-> T U)) (a T) (t S) (xs @List) (ss @List :list))
+(program $beta_reduce ((U Type) (T Type) (S Type) (f (-> T U)) (a T) (t S) (x T) (xs @List :list) (ss @List :list))
   (U @List) U
   (
-  (($beta_reduce (lambda xs t) ss) ($substitute_simul t xs ss))
-  (($beta_reduce (f a) ss)         ($beta_reduce f (@list a ss)))
+  ; handle higher-order case: if lambda is applied to one argument, it may be a partial application
+  (($beta_reduce (_ (lambda (@list x xs) t) a) @list.nil)
+                                    (eo::define ((st ($substitute x a t)))
+                                      (eo::ite (eo::is_eq xs @list.nil) st (lambda xs st))))
+  (($beta_reduce (lambda xs t) ss)  ($substitute_simul t xs ss))
+  (($beta_reduce (f a) ss)          ($beta_reduce f (@list a ss)))
   )
 )

src/rewriter/rewrite_db_term_process.cpp

@@ -86,8 +86,7 @@ Node RewriteDbNodeConverter::postConvert(Node n)
   {
     Node ret = theory::uf::FunctionConst::toLambda(n);
     recordProofStep(n, ret, ProofRule::ENCODE_EQ_INTRO);
-    // must convert again
-    return convert(ret);
+    return ret;
   }
   else if (k == Kind::FORALL)
   {

src/theory/uf/theory_uf.cpp

@@ -229,22 +229,16 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
     ss << "Cannot process term of abstract type " << node;
     throw LogicException(ss.str());
   }
-  if (k == Kind::HO_APPLY || node.getType().isFunction())
+  if (k == Kind::HO_APPLY)
   {
     if (!isHol)
     {
-      std::stringstream ss;
-      if (k == Kind::HO_APPLY)
-      {
-        ss << "Partial function applications";
-      }
-      else
+      if (!node.getType().isFunction())
       {
-        ss << "Function terms";
+        // If not HO logic, we convert to APPLY_UF
+        Node ret = TheoryUfRewriter::getApplyUfForHoApply(node);
+        return TrustNode::mkTrustRewrite(node, ret);
       }
-      ss << " are only supported with "
-            "higher-order logic. Try adding the logic prefix HO_.";
-      throw LogicException(ss.str());
     }
   }
   else if (k == Kind::APPLY_UF)
@@ -291,31 +285,24 @@ void TheoryUF::preRegisterTerm(TNode node)
     d_thss->preRegisterTerm(node);
   }
 
-  // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order
-  Assert(node.getKind() != Kind::HO_APPLY || logicInfo().isHigherOrder());
-
   Kind k = node.getKind();
   switch (k)
   {
     case Kind::EQUAL:
       // Add the trigger for equality
       d_state.addEqualityEngineTriggerPredicate(node);
       break;
-    case Kind::APPLY_UF:
+    case Kind::APPLY_UF: preRegisterFunctionTerm(node); break;
     case Kind::HO_APPLY:
     {
-      // Maybe it's a predicate
-      if (node.getType().isBoolean())
+      if (!logicInfo().isHigherOrder())
       {
-        d_state.addEqualityEngineTriggerPredicate(node);
+        std::stringstream ss;
+        ss << "Partial function applications are only supported with "
+              "higher-order logic. Try adding the logic prefix HO_.";
+        throw LogicException(ss.str());
       }
-      else
-      {
-        // Function applications/predicates
-        d_equalityEngine->addTerm(node);
-      }
-      // Remember the function and predicate terms
-      d_functionsTerms.push_back(node);
+      preRegisterFunctionTerm(node);
     }
     break;
     case Kind::INT_TO_BITVECTOR:
@@ -355,20 +342,43 @@ void TheoryUF::preRegisterTerm(TNode node)
     default:
       // Variables etc
       d_equalityEngine->addTerm(node);
+      if (logicInfo().isHigherOrder())
+      {
+        // When using lazy lambda handling, if node is a lambda function, it must
+        // be marked as a shared term. This is to ensure we split on the equality
+        // of lambda functions with other functions when doing care graph
+        // based theory combination.
+        if (d_lambdaLift->isLambdaFunction(node))
+        {
+          addSharedTerm(node);
+        }
+      }
+      else if (node.getType().isFunction())
+      {
+        std::stringstream ss;
+        ss << "Function terms are only supported with higher-order logic. Try "
+              "adding the logic prefix HO_.";
+        throw LogicException(ss.str());
+      }
       break;
   }
 
-  if (logicInfo().isHigherOrder())
+}
+
+void TheoryUF::preRegisterFunctionTerm(TNode node)
+{
+  // Maybe it's a predicate
+  if (node.getType().isBoolean())
   {
-    // When using lazy lambda handling, if node is a lambda function, it must
-    // be marked as a shared term. This is to ensure we split on the equality
-    // of lambda functions with other functions when doing care graph
-    // based theory combination.
-    if (d_lambdaLift->isLambdaFunction(node))
-    {
-      addSharedTerm(node);
-    }
+    d_state.addEqualityEngineTriggerPredicate(node);
+  }
+  else
+  {
+    // Function applications/predicates
+    d_equalityEngine->addTerm(node);
   }
+  // Remember the function and predicate terms
+  d_functionsTerms.push_back(node);
 }
 
 void TheoryUF::explain(TNode literal, Node& exp)

src/theory/uf/theory_uf.h

@@ -153,6 +153,8 @@ class TheoryUF : public Theory {
 
   std::string identify() const override { return "THEORY_UF"; }
  private:
+  /** Called when preregistering terms of kind APPLY_UF or HO_APPLY */
+  void preRegisterFunctionTerm(TNode node);
   /** Explain why this literal is true by building an explanation */
   void explain(TNode literal, Node& exp);
 

src/theory/uf/theory_uf_rewriter.cpp

@@ -69,18 +69,16 @@ RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
     {
       // Note that the rewriter does not rewrite inside of operators, so the
       // lambda we receive here may not be in rewritten form, and thus may
-      // contain variable shadowing. We rewrite the operator explicitly here.
+      // contain variable shadowing. We first check if the lambda can be
+      // rewritten.
       Node lambdaRew = d_rr->rewrite(lambda);
       // We compare against the original operator, if it is different, then
-      // we rewrite again.
+      // we convert to its HO_APPLY form, after which the lambda will occur
+      // in an ordinary term position and thus will be rewritten.
       if (lambdaRew != node.getOperator())
       {
-        std::vector<TNode> args;
-        args.push_back(lambdaRew);
-        args.insert(args.end(), node.begin(), node.end());
-        NodeManager* nm = nodeManager();
-        Node ret = nm->mkNode(Kind::APPLY_UF, args);
-        Assert(ret != node);
+        Node ret = getHoApplyForApplyUf(node);
+        Trace("uf-ho-beta") << "Lift " << node << " to HO " << ret << std::endl;
         return RewriteResponse(REWRITE_AGAIN_FULL, ret);
       }
       Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing all args of : "
@@ -194,27 +192,50 @@ Node TheoryUfRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
   {
     case ProofRewriteRule::BETA_REDUCE:
     {
-      if (n.getKind() != Kind::APPLY_UF)
+      Kind k = n.getKind();
+      Node lambda;
+      if (k == Kind::APPLY_UF)
       {
-        return Node::null();
+        lambda = uf::FunctionConst::toLambda(n.getOperator());
+      }
+      else if (k == Kind::HO_APPLY)
+      {
+        lambda = uf::FunctionConst::toLambda(n[0]);
       }
-      Node lambda = uf::FunctionConst::toLambda(n.getOperator());
       if (lambda.isNull())
       {
         return Node::null();
       }
-      std::vector<TNode> vars(lambda[0].begin(), lambda[0].end());
-      std::vector<TNode> subs(n.begin(), n.end());
-      if (vars.size() != subs.size())
+      std::vector<Node> vars;
+      std::vector<Node> subs;
+      Node body = lambda[1];
+      if (k == Kind::APPLY_UF)
       {
-        return Node::null();
+        vars.insert(vars.end(), lambda[0].begin(), lambda[0].end());
+        subs.insert(subs.end(), n.begin(), n.end());
+        if (vars.size() != subs.size())
+        {
+          return Node::null();
+        }
+      }
+      else
+      {
+        Assert(k == Kind::HO_APPLY);
+        vars.push_back(lambda[0][0]);
+        subs.push_back(n[1]);
+        if (lambda[0].getNumChildren() > 1)
+        {
+          std::vector<Node> newVars(lambda[0].begin() + 1, lambda[0].end());
+          Node bvl = d_nm->mkNode(Kind::BOUND_VAR_LIST, newVars);
+          body = d_nm->mkNode(Kind::LAMBDA, bvl, body);
+        }
       }
       // Note that we do not check for variable shadowing in the lambda here.
       // This rule will only be used to express valid instances of beta
       // reduction. If a beta reduction had to eliminate shadowing, then it
       // will not be inferred by this rule as is.
-      Node ret = lambda[1].substitute(
-          vars.begin(), vars.end(), subs.begin(), subs.end());
+      Node ret =
+          body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
       return ret;
     }
     break;

test/regress/cli/regress0/bv/holes/smod-eliminate-fewer-bitwise-ops.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic  QF_BV)
 

test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 ; COMMAND-LINE: --minimal-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL)

test/regress/cli/regress0/proofs/dd_bug787_beta_reduce.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-const _vp1-1 (_ BitVec 1))

test/regress/cli/regress0/proofs/dd_fv-bvl.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic ALL)
 (define-fun b ((bv (_ BitVec 4))) (_ BitVec 4) bv)

test/regress/cli/regress0/proofs/define-fun-shadow.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-const x2 Bool)

test/regress/cli/regress0/proofs/issue9770-open-sat-proof.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 ; EXPECT: unsat
 (set-logic QF_LIA)
 

test/regress/cli/regress1/bv/bug787.smt2

@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --bitblast=eager 
 ; EXPECT: unsat
+; DISABLE-TESTER: alethe
 (set-logic QF_BV)
 (set-info :status unsat)
 (define-fun hamming-weight ((bv (_ BitVec 4))) (_ BitVec 4)

test/regress/cli/regress1/bv2int-isabelle.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 ; COMMAND-LINE: --solve-bv-as-int=sum
 ; EXPECT: unsat
 (set-logic ALL)

test/regress/cli/regress1/proofs/add_two_base.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 ; COMMAND-LINE: --lfsc-flatten --lfsc-expand-trust
 ; EXPECT: unsat
 

test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe	
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-sort integer 0)

test/regress/cli/regress1/quantifiers/proj-issue155.smt2

@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :miniscope-quant agg)