Skip to content

Commit

Permalink
Add proof support for several simple elimination theory rewrites (cvc…
Browse files Browse the repository at this point in the history 
…5#11303)

Covers 10 more trusted steps in our regressions.

Also makes it so that POW does not accept mixed arithmetic.
  • Loading branch information
@ajreynol
ajreynol authored Nov 4, 2024
1 parent 8bd4951 commit 67517cb
Show file tree
Hide file tree
Showing 15 changed files with 228 additions and 93 deletions.
104 changes: 83 additions & 21 deletions include/cvc5/cvc5_proof_rule.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2310,6 +2310,32 @@ enum ENUM(ProofRewriteRule)
* \endverbatim
*/
EVALUE(DISTINCT_ELIM),
/**
* \verbatim embed:rst:leading-asterisk
* **UF -- Bitvector to natural elimination**
*
* .. math::
* \texttt{bv2nat}(t) = t_1 + \ldots + t_n
*
* where for :math:`i=1, \ldots, n`, :math:`t_i` is
* :math:`\texttt{ite}(x[i-1, i-1] = 1, 2^i, 0)`.
*
* \endverbatim
*/
EVALUE(BV_TO_NAT_ELIM),
/**
* \verbatim embed:rst:leading-asterisk
* **UF -- Integer to bitvector elimination**
*
* .. math::
* \texttt{int2bv}_n(t) = (bvconcat t_1 \ldots t_n)
*
* where for :math:`i=1, \ldots, n`, :math:`t_i` is
* :math:`\texttt{ite}(\texttt{mod}(t,2^n) \geq 2^{n-1}, 1, 0)`.
*
* \endverbatim
*/
EVALUE(INT_TO_BV_ELIM),
/**
* \verbatim embed:rst:leading-asterisk
* **Booleans -- Negation Normal Form with normalization**
Expand Down Expand Up @@ -2338,7 +2364,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(ARITH_DIV_BY_CONST_ELIM),
/**
* \verbatim embed:rst:leading-asterisk
* **Arithmetic - strings predicate entailment**
* **Arithmetic -- strings predicate entailment**
*
* .. math::
* (= s t) = c
Expand All @@ -2358,7 +2384,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(MACRO_ARITH_STRING_PRED_ENTAIL),
/**
* \verbatim embed:rst:leading-asterisk
* **Arithmetic - strings predicate entailment**
* **Arithmetic -- strings predicate entailment**
*
* .. math::
* (>= n 0) = true
Expand All @@ -2372,7 +2398,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(ARITH_STRING_PRED_ENTAIL),
/**
* \verbatim embed:rst:leading-asterisk
* **Arithmetic - strings predicate entailment**
* **Arithmetic -- strings predicate entailment**
*
* .. math::
* (>= n 0) = (>= m 0)
Expand All @@ -2388,6 +2414,18 @@ enum ENUM(ProofRewriteRule)
* \endverbatim
*/
EVALUE(ARITH_STRING_PRED_SAFE_APPROX),
/**
* \verbatim embed:rst:leading-asterisk
* **Arithmetic -- power elimination**
*
* .. math::
* (^ x c) = (x \cdot \ldots \cdot x)
*
* where :math:`c` is a non-negative integer.
*
* \endverbatim
*/
EVALUE(ARITH_POW_ELIM),
/**
* \verbatim embed:rst:leading-asterisk
* **Equality -- Beta reduction**
Expand Down Expand Up @@ -2527,7 +2565,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(DT_INST),
/**
* \verbatim embed:rst:leading-asterisk
* **Datatypes - collapse selector**
* **Datatypes -- collapse selector**
*
* .. math::
* s_i(c(t_1, \ldots, t_n)) = t_i
Expand All @@ -2539,7 +2577,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(DT_COLLAPSE_SELECTOR),
/**
* \verbatim embed:rst:leading-asterisk
* **Datatypes - collapse tester**
* **Datatypes -- collapse tester**
*
* .. math::
* \mathit{is}_c(c(t_1, \ldots, t_n)) = true
Expand All @@ -2556,7 +2594,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(DT_COLLAPSE_TESTER),
/**
* \verbatim embed:rst:leading-asterisk
* **Datatypes - collapse tester**
* **Datatypes -- collapse tester**
*
* .. math::
* \mathit{is}_c(t) = true
Expand All @@ -2568,7 +2606,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(DT_COLLAPSE_TESTER_SINGLETON),
/**
* \verbatim embed:rst:leading-asterisk
* **Datatypes - constructor equality**
* **Datatypes -- constructor equality**
*
* .. math::
* (c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) =
Expand All @@ -2586,7 +2624,21 @@ enum ENUM(ProofRewriteRule)
EVALUE(DT_CONS_EQ),
/**
* \verbatim embed:rst:leading-asterisk
* **Bitvectors - Unsigned multiplication overflow detection elimination**
* **Datatypes -- match elimination**
*
* .. math::
* \texttt{match}(t ((p_1 c_1) \ldots (p_n c_n))) = \texttt{ite}(F_1, r_1, \texttt{ite}( \ldots, r_n))
*
* where for :math:`i=1, \ldots, n`, :math:`F_1` is a formula that holds iff
* :math:`t` matches :math:`p_i` and :math:`r_i` is the result of a
* substitution on :math:`c_i` based on this match.
*
* \endverbatim
*/
EVALUE(DT_MATCH_ELIM),
/**
* \verbatim embed:rst:leading-asterisk
* **Bitvectors -- Unsigned multiplication overflow detection elimination**
*
* See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication
* overflow detection circuits", 2001.
Expand All @@ -2596,7 +2648,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(BV_UMULO_ELIMINATE),
/**
* \verbatim embed:rst:leading-asterisk
* **Bitvectors - Unsigned multiplication overflow detection elimination**
* **Bitvectors -- Unsigned multiplication overflow detection elimination**
*
* See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication
* overflow detection circuits", 2001.
Expand All @@ -2606,13 +2658,13 @@ enum ENUM(ProofRewriteRule)
EVALUE(BV_SMULO_ELIMINATE),
/**
* \verbatim embed:rst:leading-asterisk
* **Bitvectors - Combine like terms during addition by counting terms**
* **Bitvectors -- Combine like terms during addition by counting terms**
* \endverbatim
*/
EVALUE(BV_ADD_COMBINE_LIKE_TERMS),
/**
* \verbatim embed:rst:leading-asterisk
* **Bitvectors - Extract negations from multiplicands**
* **Bitvectors -- Extract negations from multiplicands**
*
* .. math::
* bvmul(bvneg(a),\ b,\ c) = bvneg(bvmul(a,\ b,\ c))
Expand All @@ -2622,7 +2674,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(BV_MULT_SIMPLIFY),
/**
* \verbatim embed:rst:leading-asterisk
* **Bitvectors - Extract continuous substrings of bitvectors**
* **Bitvectors -- Extract continuous substrings of bitvectors**
*
* .. math::
* bvand(a,\ c) = concat(bvand(a[i_0:j_0],\ c_0) ... bvand(a[i_n:j_n],\ c_n))
Expand All @@ -2633,7 +2685,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(BV_BITWISE_SLICING),
/**
* \verbatim embed:rst:leading-asterisk
* **Strings - regular expression loop elimination**
* **Strings -- regular expression loop elimination**
*
* .. math::
* re.loop_{l,u}(R) = re.union(R^l, \ldots, R^u)
Expand All @@ -2645,7 +2697,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(RE_LOOP_ELIM),
/**
* \verbatim embed:rst:leading-asterisk
* **Strings - regular expression intersection/union inclusion**
* **Strings -- regular expression intersection/union inclusion**
*
* .. math::
* (re.inter\ R) = \mathit{re.inter}(\mathit{re.none}, R_0)
Expand All @@ -2668,7 +2720,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(RE_INTER_UNION_INCLUSION),
/**
* \verbatim embed:rst:leading-asterisk
* **Strings - regular expression membership evaluation**
* **Strings -- regular expression membership evaluation**
*
* .. math::
* \mathit{str.in\_re}(s, R) = c
Expand All @@ -2681,7 +2733,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(STR_IN_RE_EVAL),
/**
* \verbatim embed:rst:leading-asterisk
* **Strings - regular expression membership consume**
* **Strings -- regular expression membership consume**
*
* .. math::
* \mathit{str.in_re}(s, R) = b
Expand All @@ -2694,7 +2746,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(STR_IN_RE_CONSUME),
/**
* \verbatim embed:rst:leading-asterisk
* **Strings - string in regular expression concatenation star character**
* **Strings -- string in regular expression concatenation star character**
*
* .. math::
* \mathit{str.in\_re}(\mathit{str}.\text{++}(s_1, \ldots, s_n), \mathit{re}.\text{*}(R)) =\\ \mathit{str.in\_re}(s_1, \mathit{re}.\text{*}(R)) \wedge \ldots \wedge \mathit{str.in\_re}(s_n, \mathit{re}.\text{*}(R))
Expand All @@ -2706,7 +2758,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(STR_IN_RE_CONCAT_STAR_CHAR),
/**
* \verbatim embed:rst:leading-asterisk
* **Strings - string in regular expression sigma**
* **Strings -- string in regular expression sigma**
*
* .. math::
* \mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar})) = (\mathit{str.len}(s) = n)
Expand All @@ -2721,7 +2773,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(STR_IN_RE_SIGMA),
/**
* \verbatim embed:rst:leading-asterisk
* **Strings - string in regular expression sigma star**
* **Strings -- string in regular expression sigma star**
*
* .. math::
* \mathit{str.in\_re}(s, \mathit{re}.\text{*}(\mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}))) = (\mathit{str.len}(s) \ \% \ n = 0)
Expand All @@ -2734,7 +2786,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(STR_IN_RE_SIGMA_STAR),
/**
* \verbatim embed:rst:leading-asterisk
* **Strings - strings substring strip symbolic length**
* **Strings -- strings substring strip symbolic length**
*
* .. math::
* str.substr(s, n, m) = t
Expand All @@ -2747,7 +2799,7 @@ enum ENUM(ProofRewriteRule)
EVALUE(MACRO_SUBSTR_STRIP_SYM_LENGTH),
/**
* \verbatim embed:rst:leading-asterisk
* **Sets - empty tester evaluation**
* **Sets -- empty tester evaluation**
*
* .. math::
* \mathit{sets.is\_empty}(\epsilon) = \top
Expand All @@ -2762,6 +2814,16 @@ enum ENUM(ProofRewriteRule)
* \endverbatim
*/
EVALUE(SETS_IS_EMPTY_EVAL),
/**
* \verbatim embed:rst:leading-asterisk
* **Sets -- sets insert elimination**
*
* .. math::
* \mathit{sets.insert}(t_1, \ldots, t_n, S) = \texttt{set.union}(\texttt{sets.singleton}(t_1), \ldots, \texttt{sets.singleton}(t_n), S)
*
* \endverbatim
*/
EVALUE(SETS_INSERT_ELIM),
// RARE rules
// ${rules}$
/** Auto-generated from RARE rule arith-plus-zero */
Expand Down
4 changes: 2 additions & 2 deletions proofs/eo/cpc/theories/Arith.eo
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,8 +107,8 @@
; Power function.
; disclaimer: This function is not a function in SMT-LIB.
(declare-const ^ (-> (! Type :var T :implicit)
(! Type :var U :implicit)
T U ($arith_typeunion T U)))
(! T :requires (($is_arith_type T) true))
T T))

; Unary negation, which is overloaded with binary subtraction. We distinguish
; these two operators in EunoiaC based on their arity when applied, and with
Expand Down
6 changes: 6 additions & 0 deletions src/api/cpp/cvc5_proof_rule_template.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -220,6 +220,8 @@ const char* toString(cvc5::ProofRewriteRule rule)
case ProofRewriteRule::NONE: return "NONE";
//================================================= ad-hoc rules
case ProofRewriteRule::DISTINCT_ELIM: return "distinct-elim";
case ProofRewriteRule::BV_TO_NAT_ELIM: return "bv-to-nat-elim";
case ProofRewriteRule::INT_TO_BV_ELIM: return "int-to-bv-elim";
case ProofRewriteRule::MACRO_BOOL_NNF_NORM: return "macro-bool-nnf-norm";
case ProofRewriteRule::ARITH_DIV_BY_CONST_ELIM:
return "arith-div-by-const-elim";
Expand All @@ -229,6 +231,7 @@ const char* toString(cvc5::ProofRewriteRule rule)
return "arith-string-pred-safe-approx";
case ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL:
return "macro-arith-string-pred-entail";
case ProofRewriteRule::ARITH_POW_ELIM: return "arith-pow-elim";
case ProofRewriteRule::BETA_REDUCE: return "beta-reduce";
case ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND:
return "arrays-eq-range-expand";
Expand All @@ -249,6 +252,7 @@ const char* toString(cvc5::ProofRewriteRule rule)
case ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON:
return "dt-collapse-tester-singleton";
case ProofRewriteRule::DT_CONS_EQ: return "dt-cons-eq";
case ProofRewriteRule::DT_MATCH_ELIM: return "dt-match-elim";
case ProofRewriteRule::BV_UMULO_ELIMINATE: return "bv-umulo-eliminate";
case ProofRewriteRule::BV_SMULO_ELIMINATE: return "bv-smulo-eliminate";
case ProofRewriteRule::BV_ADD_COMBINE_LIKE_TERMS:
Expand All @@ -268,6 +272,8 @@ const char* toString(cvc5::ProofRewriteRule rule)
return "macro-substr-strip-sym-length";
case ProofRewriteRule::SETS_IS_EMPTY_EVAL:
return "sets-is-empty-eval";
case ProofRewriteRule::SETS_INSERT_ELIM:
return "sets-insert-elim";
//================================================= RARE rules
// clang-format off
${printer}$
Expand Down
Loading

0 comments on commit 67517cb

Please sign in to comment.