Skip to content

Commit

Permalink
Refactor congruence proof rules (cvc5#11501)
Browse files Browse the repository at this point in the history 
This refactors the congruence rules of CPC.

The motivation is:
1. We should not export "Kind" nodes to the API as these are not useful
to a user.
2. We no longer have to disambiguate operators when applying congruence.
This includes parameterized operators like bvadd, binary vs unary minus,
as well as uninterpreted functions with overloaded symbols (the latter
is currently broken in cpc output since it is not possible to tell from
cvc5's internals whether a UF was overloaded).
3. Efficiency, as the proofs contain one fewer argument and the
resulting proof checkers should be more efficient.

One question is whether we should further introduce a `BINDER_CONG` for
congruence over binders. These are currently a special case of `CONG`.

This PR enables the cpc tester for 13 regressions that could not be
checked due to congruence on overloaded UF.

---------

Co-authored-by: Haniel Barbosa <[email protected]>
  • Loading branch information
@ajreynol @HanielB
ajreynol and HanielB authored Jan 17, 2025
1 parent ca078a5 commit 6e83633
Show file tree
Hide file tree
Showing 27 changed files with 150 additions and 248 deletions.
38 changes: 17 additions & 21 deletions include/cvc5/cvc5_proof_rule.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1043,22 +1043,20 @@ enum ENUM(ProofRule)
*
* .. math::
*
* \inferrule{t_1=s_1,\dots,t_n=s_n\mid k, f?}{k(f?, t_1,\dots, t_n) =
* k(f?, s_1,\dots, s_n)}
*
* where :math:`k` is the application kind. Notice that :math:`f` must be
* provided iff :math:`k` is a parameterized kind, e.g.
* `cvc5::Kind::APPLY_UF`. The actual node for
* :math:`k` is constructible via ``ProofRuleChecker::mkKindNode``.
* If :math:`k` is a binder kind (e.g. ``cvc5::Kind::FORALL``) then :math:`f`
* is a term of kind ``cvc5::Kind::VARIABLE_LIST``
* denoting the variables bound by both sides of the conclusion.
* This rule is used for kinds that have a fixed arity, such as
* ``cvc5::Kind::ITE``, ``cvc5::Kind::EQUAL``, and so on. It is also used for
* ``cvc5::Kind::APPLY_UF`` where :math:`f` must be provided.
* It is not used for equality between
* ``cvc5::Kind::HO_APPLY`` terms, which should
* use the :cpp:enumerator:`HO_CONG <cvc5::ProofRule::HO_CONG>` proof rule.
* \inferrule{t_1=s_1,\dots,t_n=s_n\mid f(t_1,\dots, t_n)}{f(t_1,\dots, t_n) = f(s_1,\dots, s_n)}
*
* This rule is used when the kind of :math:`f(t_1,\dots, t_n)` has a fixed
* arity. This includes kinds such as ``cvc5::Kind::ITE``,
* ``cvc5::Kind::EQUAL``, as well as indexed functions such as
* ``cvc5::Kind::BITVECTOR_EXTRACT``.
*
* It is also used for ``cvc5::Kind::APPLY_UF``, where :math:`f` is an
* uninterpreted function.
*
* It is not used for kinds with variadic arity, or for kind
* ``cvc5::Kind::HO_APPLY``, which respectively use the rules
* :cpp:enumerator:`NARY_CONG <cvc5::ProofRule::NARY_CONG>` and
* :cpp:enumerator:`HO_CONG <cvc5::ProofRule::HO_CONG>` below.
* \endverbatim
*/
EVALUE(CONG),
Expand All @@ -1068,12 +1066,10 @@ enum ENUM(ProofRule)
*
* .. math::
*
* \inferrule{t_1=s_1,\dots,t_n=s_n\mid k}{k(t_1,\dots, t_n) =
* k(s_1,\dots, s_n)}
* \inferrule{t_1=s_1,\dots,t_n=s_n\mid f(t_1,\dots, t_n)}{f(t_1,\dots, t_n) = f(s_1,\dots, s_n)}
*
* where :math:`k` is the application kind. The actual node for :math:`k` is
* constructible via ``ProofRuleChecker::mkKindNode``. This rule is used for
* kinds that have variadic arity, such as ``cvc5::Kind::AND``,
* This rule is used for terms :math:`f(t_1,\dots, t_n)` whose kinds
* :math:`k` have variadic arity, such as ``cvc5::Kind::AND``,
* ``cvc5::Kind::PLUS`` and so on.
* \endverbatim
*/
Expand Down
126 changes: 65 additions & 61 deletions proofs/eo/cpc/rules/Uf.eo
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
(include "../theories/Builtin.eo")

;;;;; ProofRule::REFL

; rule: refl
; implements: ProofRule::REFL
; args:
Expand All @@ -10,6 +12,8 @@
:conclusion (= t t)
)

;;;;; ProofRule::SYMM

; rule: symm
; implements: ProofRule::SYMM
; args:
Expand All @@ -26,6 +30,8 @@
))
)

;;;;; ProofRule::TRANS

; program: $mk_trans
; args:
; - t1 U: The current left hand side of the equality we have proven.
Expand Down Expand Up @@ -60,21 +66,19 @@
(((and (= t1 t2) tail) ($mk_trans t1 t2 tail))))
)

;;;;; ProofRule::CONG

; program: $mk_cong
; program: $mk_cong_rhs
; args:
; - t1 U: The current left hand side of the equality we have proven.
; - t2 U: The current right hand side of the equality we have proven.
; - E Bool: A conjunction of the remaining equalities we have left to process.
; - t U: The left hand side of the equality we have yet to process.
; - E Bool: A conjunction of the remaining equalities we have left to process, in reverse order.
; return: >
; An equality where the original terms are applied to the left and
; right hand sides of the equalities given by E.
(program $mk_cong ((T Type) (U Type) (f1 (-> T U)) (f2 (-> T U)) (t1 U) (t2 U) (tail Bool :list))
(U U Bool) Bool
; The right hand side of the equality.
(program $mk_cong_rhs ((T Type) (U Type) (f (-> T U)) (t1 U) (t2 U) (t3 U) (tail Bool :list))
(U Bool) U
(
(($mk_cong f1 f2 (and (= t1 t2) tail)) ($mk_cong (f1 t1) (f2 t2) tail))
(($mk_cong t1 t2 true) (= t1 t2))
(($mk_cong f1 f2 (= t1 t2)) (= (f1 t1) (f2 t2)))
(($mk_cong_rhs (f t1) (and (= t1 t2) tail)) (_ ($mk_cong_rhs f tail) t2))
(($mk_cong_rhs f true) f)
)
)

Expand All @@ -83,57 +87,34 @@
; premises:
; - E [:list]: A conjunction of equalities to apply congruence to.
; args:
; - f (-> T U): >
; The function to apply congruence to. This is assumed to be
; - t U: >
; The term to apply congruence to. This is assumed to be an application of
; a function that is not n-ary, e.g. it is not marked :right-assoc-nil.
; Congruence for n-ary operators requires a different rule (nary_cong) below.
; conclusion: >
; An equality between applications of f whose arguments are given
; by the equalities in E.
; disclaimer: >
; This proof rule takes only the function to do congruence over,
; whereas the internal proof calculus takes an internal value denoting its
; cvc5::Kind along with an (optional) function if the kind if parameterized.
(declare-rule cong ((T Type) (U Type) (E Bool) (f (-> T U)))
; An equality between applications of the operator of t whose arguments are
; given by the equalities in E.
; note: >
; Congruence for n-ary operators requires a different rule (nary_cong) below.
(declare-rule cong ((U Type) (E Bool) (t U))
:premise-list E and
:args (f)
:conclusion ($mk_cong f f E)
:args (t)
:conclusion (= t ($mk_cong_rhs t ($nary_reverse E)))
)

; program: $mk_nary_cong_lhs
; args:
; - f (-> U U U): >
; The function we are applying congruence over. This is
; assumed to be a right-associative n-ary operator with nil terminator, i.e.
; marked with :right-assoc-nil.
; - E Bool: A conjunction of the remaining equalities we have left to process.
; return: >
; The left hand side of the equality proven by nary_cong for f and
; the given premises E.
; note: >
; We use two side conditions for computing each side of the returned
; equality. This avoids constructing equalities between intermediate terms.
(program $mk_nary_cong_lhs ((U Type) (f (-> U U U)) (s1 U) (s2 U) (tail Bool :list))
((-> U U U) Bool) Bool
(
(($mk_nary_cong_lhs f (and (= s1 s2) tail)) (eo::cons f s1 ($mk_nary_cong_lhs f tail)))
(($mk_nary_cong_lhs f true) (eo::nil f))
)
)
;;;;; ProofRule::NARY_CONG

; program: $mk_nary_cong_rhs
; args:
; - f (-> U U U): The function we are applying congruence over.
; - t U: The term (left hand side of the equality) we are applying congruence over.
; - E Bool: A conjunction of the remaining equalities we have left to process.
; return: >
; The right hand side of the equality proven by nary_cong for f and
; the given premises E.
; note: This program is analogous to $mk_nary_cong_lhs.
(program $mk_nary_cong_rhs ((U Type) (f (-> U U U)) (s1 U) (s2 U) (tail Bool :list))
((-> U U U) Bool) Bool
(program $mk_nary_cong_rhs ((U Type) (f (-> U U U)) (s1 U) (s2 U) (t U :list) (tail Bool :list) (nil U))
(U Bool) U
(
(($mk_nary_cong_rhs f (and (= s1 s2) tail)) (eo::cons f s2 ($mk_nary_cong_rhs f tail)))
(($mk_nary_cong_rhs f true) (eo::nil f))
(($mk_nary_cong_rhs (f s1 t) (and (= s1 s2) tail)) (eo::cons f s2 ($mk_nary_cong_rhs t tail)))
(($mk_nary_cong_rhs nil true) nil)
)
)

Expand All @@ -142,23 +123,22 @@
; premises:
; - E [:list]: A conjunction of equalities to apply nary-congruence to.
; args:
; - f (-> T U): >
; The function to apply congruence to. This is assumed to be
; a function that is right-associative n-ary operator with nil terminator, e.g.
; it is marked :right-assoc-nil.
; - t U: >
; The term to apply congruence to. This is assumed to be an application of
; a function that is a right-associative n-ary operator with nil terminator,
; i.e. it is marked :right-assoc-nil. It is required to be the left hand side
; of the equality we are proving.
; conclusion: >
; An equality between applications of f whose arguments are given
; by the equalities in E.
; disclaimer: >
; This proof rule takes as argument the function to do congruence
; over, whereas the internal proof calculus takes an internal value denoting its
; cvc5::Kind.
(declare-rule nary_cong ((U Type) (E Bool) (f (-> U U)) (nil U))
(declare-rule nary_cong ((U Type) (E Bool) (t U))
:premise-list E and
:args (f)
:conclusion (= ($mk_nary_cong_lhs f E) ($mk_nary_cong_rhs f E))
:args (t)
:conclusion (= t ($mk_nary_cong_rhs t E))
)

;;;;; ProofRule::TRUE_INTRO

; rule: true_intro
; implements: ProofRule::TRUE_INTRO
; premises:
Expand All @@ -169,6 +149,8 @@
:conclusion (= F true)
)

;;;;; ProofRule::TRUE_ELIM

; rule: true_elim
; implements: ProofRule::TRUE_ELIM
; premises:
Expand All @@ -179,6 +161,8 @@
:conclusion F
)

;;;;; ProofRule::FALSE_INTRO

; rule: false_intro
; implements: ProofRule::FALSE_INTRO
; premises:
Expand All @@ -189,6 +173,7 @@
:conclusion (= F false)
)

;;;;; ProofRule::FALSE_ELIM

; rule: false_elim
; implements: ProofRule::FALSE_ELIM
Expand All @@ -200,6 +185,25 @@
:conclusion (not F)
)

;;;;; ProofRule::HO_CONG

; program: $mk_ho_cong
; args:
; - t1 U: The current left hand side of the equality we have proven.
; - t2 U: The current right hand side of the equality we have proven.
; - E Bool: A conjunction of the remaining equalities we have left to process.
; return: >
; An equality where the original terms are applied to the left and
; right hand sides of the equalities given by E.
(program $mk_ho_cong ((T Type) (U Type) (f1 (-> T U)) (f2 (-> T U)) (t1 U) (t2 U) (tail Bool :list))
(U U Bool) Bool
(
(($mk_ho_cong f1 f2 (and (= t1 t2) tail)) ($mk_ho_cong (f1 t1) (f2 t2) tail))
(($mk_ho_cong t1 t2 true) (= t1 t2))
(($mk_ho_cong f1 f2 (= t1 t2)) (= (f1 t1) (f2 t2)))
)
)

; rule: ho_cong
; implements: ProofRule::HO_CONG
; premises:
Expand All @@ -215,7 +219,7 @@
:conclusion
(eo::match ((t1 U) (t2 U) (tail Bool :list))
E
(((and (= t1 t2) tail) ($mk_cong t1 t2 tail))))
(((and (= t1 t2) tail) ($mk_ho_cong t1 t2 tail))))
)

;;-------------------- Instances of THEORY_REWRITE
Expand Down
5 changes: 1 addition & 4 deletions src/proof/alethe/alethe_node_converter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,10 +73,7 @@ class AletheNodeConverter : public BaseAlfNodeConverter
TypeNode tn,
bool useRawSym = true) override;

Node getOperatorOfTerm(Node n, bool reqCast = false) override
{
return Node::null();
};
Node getOperatorOfTerm(Node n) override { return Node::null(); };

Node typeAsNode(TypeNode tni) override { return Node::null(); };

Expand Down
68 changes: 2 additions & 66 deletions src/proof/alf/alf_node_converter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -455,7 +455,7 @@ Node AlfNodeConverter::mkInternalApp(const std::string& name,
return mkInternalSymbol(name, ret, useRawSym);
}

Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast)
Node AlfNodeConverter::getOperatorOfTerm(Node n)
{
Assert(n.hasOperator());
Kind k = n.getKind();
Expand Down Expand Up @@ -586,60 +586,7 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast)
}
else
{
bool isParameterized = false;
if (reqCast)
{
// If the operator is a parameterized constant and reqCast is true,
// then we must apply the parameters of the operator, e.g. such that
// bvor becomes (eo::_ bvor 32) where 32 is the bitwidth of the first
// argument.
if (k == Kind::BITVECTOR_ADD || k == Kind::BITVECTOR_MULT
|| k == Kind::BITVECTOR_OR || k == Kind::BITVECTOR_AND
|| k == Kind::BITVECTOR_XOR)
{
TypeNode tna = n[0].getType();
indices.push_back(d_nm->mkConstInt(tna.getBitVectorSize()));
isParameterized = true;
}
else if (k == Kind::FINITE_FIELD_ADD || k == Kind::FINITE_FIELD_BITSUM
|| k == Kind::FINITE_FIELD_MULT)
{
TypeNode tna = n[0].getType();
indices.push_back(d_nm->mkConstInt(tna.getFfSize()));
isParameterized = true;
}
else if (k == Kind::STRING_CONCAT)
{
// String concatenation is parameterized by the character type, which
// is the "Char" type in the ALF signature for String (which note does
// not exist internally in cvc5). Otherwise it is the sequence element
// type.
TypeNode tna = n[0].getType();
Node cht;
if (tna.isString())
{
cht = mkInternalSymbol("Char", d_sortType);
}
else
{
cht = typeAsNode(tna.getSequenceElementType());
}
indices.push_back(cht);
isParameterized = true;
}
}
if (isParameterized)
{
opName << "eo::_";
std::stringstream oppName;
oppName << printer::smt2::Smt2Printer::smtKindString(k);
Node opp = mkInternalSymbol(oppName.str(), n.getType());
indices.insert(indices.begin(), opp);
}
else
{
opName << printer::smt2::Smt2Printer::smtKindString(k);
}
opName << printer::smt2::Smt2Printer::smtKindString(k);
}
std::vector<Node> args(n.begin(), n.end());
Node app = mkInternalApp(opName.str(), args, n.getType());
Expand All @@ -662,17 +609,6 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast)
{
ret = args.empty() ? app : app.getOperator();
}
if (reqCast)
{
// - prints as e.g. (eo::as - (-> Int Int)).
if (k == Kind::NEG || k == Kind::SUB)
{
std::vector<Node> asChildren;
asChildren.push_back(ret);
asChildren.push_back(typeAsNode(ret.getType()));
ret = mkInternalApp("eo::as", asChildren, n.getType());
}
}
Trace("alf-term-process-debug2") << "...return " << ret << std::endl;
return ret;
}
Expand Down
Loading

0 comments on commit 6e83633

Please sign in to comment.