diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 683af0c3b21..38cd650c899 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/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), diff --git a/proofs/eo/cpc/programs/Quantifiers.eo b/proofs/eo/cpc/programs/Quantifiers.eo index 42cb634cd93..1871b9d7c9a 100644 --- a/proofs/eo/cpc/programs/Quantifiers.eo +++ b/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))) ) ) diff --git a/src/rewriter/rewrite_db_term_process.cpp b/src/rewriter/rewrite_db_term_process.cpp index 03bf9d31926..670c95f009c 100644 --- a/src/rewriter/rewrite_db_term_process.cpp +++ b/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) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 579d1c15733..83e3b69e073 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -229,22 +229,16 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector& 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,9 +285,6 @@ 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) { @@ -301,21 +292,17 @@ void TheoryUF::preRegisterTerm(TNode node) // 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) diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index dbcc75957fc..80e14339d57 100644 --- a/src/theory/uf/theory_uf.h +++ b/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); diff --git a/src/theory/uf/theory_uf_rewriter.cpp b/src/theory/uf/theory_uf_rewriter.cpp index 138d9a589a4..e4d6ce84835 100644 --- a/src/theory/uf/theory_uf_rewriter.cpp +++ b/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 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 vars(lambda[0].begin(), lambda[0].end()); - std::vector subs(n.begin(), n.end()); - if (vars.size() != subs.size()) + std::vector vars; + std::vector 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 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; diff --git a/test/regress/cli/regress0/bv/holes/smod-eliminate-fewer-bitwise-ops.smt2 b/test/regress/cli/regress0/bv/holes/smod-eliminate-fewer-bitwise-ops.smt2 index 0f9dc3f7499..04cc67427d2 100644 --- a/test/regress/cli/regress0/bv/holes/smod-eliminate-fewer-bitwise-ops.smt2 +++ b/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) diff --git a/test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2 b/test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2 index c3db14e90ec..10858d651d9 100644 --- a/test/regress/cli/regress0/cores/dd.uc-min-wrong.smt2 +++ b/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) diff --git a/test/regress/cli/regress0/proofs/dd_bug787_beta_reduce.smt2 b/test/regress/cli/regress0/proofs/dd_bug787_beta_reduce.smt2 index 172ec142f69..135ec693679 100644 --- a/test/regress/cli/regress0/proofs/dd_bug787_beta_reduce.smt2 +++ b/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)) diff --git a/test/regress/cli/regress0/proofs/dd_fv-bvl.smt2 b/test/regress/cli/regress0/proofs/dd_fv-bvl.smt2 index 57b69011f60..67d3141e624 100644 --- a/test/regress/cli/regress0/proofs/dd_fv-bvl.smt2 +++ b/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) diff --git a/test/regress/cli/regress0/proofs/define-fun-shadow.smt2 b/test/regress/cli/regress0/proofs/define-fun-shadow.smt2 index 436fa2def74..679ff81aabc 100644 --- a/test/regress/cli/regress0/proofs/define-fun-shadow.smt2 +++ b/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) diff --git a/test/regress/cli/regress0/proofs/issue9770-open-sat-proof.smt2 b/test/regress/cli/regress0/proofs/issue9770-open-sat-proof.smt2 index 771cc57ee75..e6dfe8a9f84 100644 --- a/test/regress/cli/regress0/proofs/issue9770-open-sat-proof.smt2 +++ b/test/regress/cli/regress0/proofs/issue9770-open-sat-proof.smt2 @@ -1,3 +1,4 @@ +; DISABLE-TESTER: alethe ; EXPECT: unsat (set-logic QF_LIA) diff --git a/test/regress/cli/regress1/bv/bug787.smt2 b/test/regress/cli/regress1/bv/bug787.smt2 index d732b9ff082..bc64576a729 100644 --- a/test/regress/cli/regress1/bv/bug787.smt2 +++ b/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) diff --git a/test/regress/cli/regress1/bv2int-isabelle.smt2 b/test/regress/cli/regress1/bv2int-isabelle.smt2 index 3a88e75a33a..732cfcda064 100644 --- a/test/regress/cli/regress1/bv2int-isabelle.smt2 +++ b/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) diff --git a/test/regress/cli/regress1/proofs/add_two_base.smt2 b/test/regress/cli/regress1/proofs/add_two_base.smt2 index c8ec3226818..a945cee6953 100644 --- a/test/regress/cli/regress1/proofs/add_two_base.smt2 +++ b/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 diff --git a/test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2 b/test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2 index 07175db35b8..ebc5f36299f 100644 --- a/test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2 +++ b/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) diff --git a/test/regress/cli/regress1/quantifiers/proj-issue155.smt2 b/test/regress/cli/regress1/quantifiers/proj-issue155.smt2 index 559899ff149..a8aba351cf7 100644 --- a/test/regress/cli/regress1/quantifiers/proj-issue155.smt2 +++ b/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)