Skip to content

Commit

Permalink
More updates
Browse files Browse the repository at this point in the history
  • Loading branch information
@ajreynol
ajreynol committed Feb 24, 2025
1 parent 88aba05 commit 81525a7
Show file tree
Hide file tree
Showing 5 changed files with 100 additions and 91 deletions.
13 changes: 12 additions & 1 deletion include/cvc5/cvc5_proof_rule.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3236,7 +3236,12 @@ enum ENUM(ProofRewriteRule)
/**
* \verbatim embed:rst:leading-asterisk
* **Bitvectors -- Unsigned multiplication overflow detection elimination**
*
* .. math::
* \texttt{bvumulo}(x,y) = t
*
* where :math:`t` is the result of eliminating the application
* of :math:`\texttt{bvumulo}`.
*
* See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication
* overflow detection circuits", 2001.
Expand All @@ -3248,6 +3253,12 @@ enum ENUM(ProofRewriteRule)
* \verbatim embed:rst:leading-asterisk
* **Bitvectors -- Unsigned multiplication overflow detection elimination**
*
* .. math::
* \texttt{bvsmulo}(x,y) = t
*
* where :math:`t` is the result of eliminating the application
* of :math:`\texttt{bvsmulo}`.
*
* See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication
* overflow detection circuits", 2001.
* http://ieeexplore.ieee.org/document/987767
Expand Down
89 changes: 0 additions & 89 deletions proofs/eo/cpc/programs/BitVectors.eo
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,92 +112,3 @@
; children.
(define $nary_app ((T Type :implicit) (U Type :implicit) (V Type :implicit) (f (-> T U V)) (a T) (b U))
(f a (f b (eo::nil f a b))))


;;;;; evaluation utils

; define: $bv_smulo_elim
; args:
; - xa (BitVec n): An xor term involving the first argument to bvsmulo
; - xb (BitVec n): An xor term involving the second argument to bvsmulo
; - ppc (BitVec 1): An intermediate bitvector term accumulated to help construct the result.
; - res (BitVec 1): The current accumulated result.
; - i Int: The current bit we are processing.
; - nm2 Int: The bitwidth of a and b minus 2.
; return: >
; A portion of the result of eliminating (bvsmulo a b).
(program $bv_smulo_elim_rec ((n Int) (xa (BitVec n)) (xb (BitVec n))
(ppc (BitVec 1)) (res (BitVec 1)) (i Int) (nm2 Int))
((BitVec n) (BitVec n) (BitVec 1) (BitVec 1) Int Int) (BitVec 1)
(
(($bv_smulo_elim_rec xa xb ppc res nm2 nm2) res)
(($bv_smulo_elim_rec xa xb ppc res i nm2)
(eo::define ((ia (eo::add nm2 (eo::neg i))))
(eo::define ((ip1 (eo::add i 1)))
(eo::define ((ppcn (bvor ppc (extract ia ia xa))))
($bv_smulo_elim_rec xa xb ppcn (bvor res (bvand (extract ip1 ip1 xb) ppcn)) ip1 nm2)))))
)
)

; define: $bv_smulo_elim
; args:
; - a (BitVec n): The first argument to bvsmulo
; - b (BitVec n): The second argument to bvsmulo
; return: >
; The result of eliminating (bvsmulo a b).
(define $bv_smulo_elim ((n Int :implicit) (a (BitVec n)) (b (BitVec n)))
(eo::define ((w ($bv_bitwidth (eo::typeof a))))
(eo::define ((wm1 (eo::add w -1)))
(eo::define ((one (eo::to_bin 1 1)))
(eo::ite (eo::is_eq w 1)
(= (bvand a b) one)
(eo::define ((mul (bvmul (sign_extend 1 a) (sign_extend 1 b))))
(eo::ite (eo::is_eq w 2)
(= (bvxor (extract w w mul) (extract wm1 wm1 mul)) one)
(eo::define ((xa (bvxor a (sign_extend wm1 (extract wm1 wm1 a)))))
(eo::define ((xb (bvxor b (sign_extend wm1 (extract wm1 wm1 b)))))
(eo::define ((wm2 (eo::add w -2)))
(eo::define ((ppc (extract wm2 wm2 xa)))
(eo::define ((res ($bv_smulo_elim_rec xa xb ppc (bvand (extract 1 1 xb) ppc) 1 wm2)))
(= (bvor res (bvxor (extract w w mul) (extract wm1 wm1 mul))) one))))))))))))
)

; define: $bv_umulo_elim_rec
; args:
; - xa (BitVec n): An xor term involving the first argument to bvumulo
; - xb (BitVec n): An xor term involving the second argument to bvumulo
; - ppc (BitVec 1): An intermediate bitvector term accumulated to help construct the result.
; - res (BitVec 1): The current accumulated result.
; - i Int: The current bit we are processing.
; - nm2 Int: The bitwidth of a and b minus 2.
; return: >
; A portion of the result of eliminating (bvsmulo a b).
(program $bv_umulo_elim_rec ((n Int) (a (BitVec n)) (b (BitVec n))
(uppc (BitVec 1)) (res (BitVec 1)) (i Int))
((BitVec n) (BitVec n) (BitVec 1) (BitVec 1) Int Int) (BitVec 1)
(
(($bv_umulo_elim_rec a b uppc res n n) res)
(($bv_umulo_elim_rec a b uppc res i n)
(eo::define ((ia (eo::add n -1 (eo::neg i))))
(eo::define ((ip1 (eo::add i 1)))
(eo::define ((uppcn (bvor (extract ia ia a) uppc)))
(eo::cons bvor (bvand (extract i i b) uppc) ($bv_umulo_elim_rec a b uppcn res ip1 n))))))
)
)

; define: $bv_umulo_elim
; args:
; - a (BitVec n): The first argument to bvumulo
; - b (BitVec n): The second argument to bvumulo
; return: >
; The result of eliminating (bvumulo a b).
(define $bv_umulo_elim ((n Int :implicit) (a (BitVec n)) (b (BitVec n)))
(eo::define ((w ($bv_bitwidth (eo::typeof a))))
(eo::ite (eo::is_eq w 1)
false
(eo::define ((wm1 (eo::add w -1)))
(eo::define ((zero (eo::to_bin 1 0)))
(eo::define ((uppc (extract wm1 wm1 a)))
(eo::define ((mul (bvmul (concat zero a) (concat zero b))))
(eo::define ((res ($bv_umulo_elim_rec a b uppc (bvor (extract w w mul)) 1 w)))
(= res (eo::to_bin 1 1))))))))))
86 changes: 86 additions & 0 deletions proofs/eo/cpc/rules/BitVectors.eo
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,52 @@

;;;;; ProofRewriteRule::BV_SMULO_ELIM

; define: $bv_smulo_elim
; args:
; - xa (BitVec n): An xor term involving the first argument to bvsmulo
; - xb (BitVec n): An xor term involving the second argument to bvsmulo
; - ppc (BitVec 1): An intermediate bitvector term accumulated to help construct the result.
; - res (BitVec 1): The current accumulated result.
; - i Int: The current bit we are processing.
; - nm2 Int: The bitwidth of a and b minus 2.
; return: >
; A portion of the result of eliminating (bvsmulo a b).
(program $bv_smulo_elim_rec ((n Int) (xa (BitVec n)) (xb (BitVec n))
(ppc (BitVec 1)) (res (BitVec 1)) (i Int) (nm2 Int))
((BitVec n) (BitVec n) (BitVec 1) (BitVec 1) Int Int) (BitVec 1)
(
(($bv_smulo_elim_rec xa xb ppc res nm2 nm2) res)
(($bv_smulo_elim_rec xa xb ppc res i nm2)
(eo::define ((ia (eo::add nm2 (eo::neg i))))
(eo::define ((ip1 (eo::add i 1)))
(eo::define ((ppcn (bvor ppc (extract ia ia xa))))
($bv_smulo_elim_rec xa xb ppcn (bvor res (bvand (extract ip1 ip1 xb) ppcn)) ip1 nm2)))))
)
)

; define: $bv_smulo_elim
; args:
; - a (BitVec n): The first argument to bvsmulo
; - b (BitVec n): The second argument to bvsmulo
; return: >
; The result of eliminating (bvsmulo a b).
(define $bv_smulo_elim ((n Int :implicit) (a (BitVec n)) (b (BitVec n)))
(eo::define ((w ($bv_bitwidth (eo::typeof a))))
(eo::define ((wm1 (eo::add w -1)))
(eo::define ((one (eo::to_bin 1 1)))
(eo::ite (eo::is_eq w 1)
(= (bvand a b) one)
(eo::define ((mul (bvmul (sign_extend 1 a) (sign_extend 1 b))))
(eo::ite (eo::is_eq w 2)
(= (bvxor (extract w w mul) (extract wm1 wm1 mul)) one)
(eo::define ((xa (bvxor a (sign_extend wm1 (extract wm1 wm1 a)))))
(eo::define ((xb (bvxor b (sign_extend wm1 (extract wm1 wm1 b)))))
(eo::define ((wm2 (eo::add w -2)))
(eo::define ((ppc (extract wm2 wm2 xa)))
(eo::define ((res ($bv_smulo_elim_rec xa xb ppc (bvand (extract 1 1 xb) ppc) 1 wm2)))
(= (bvor res (bvxor (extract w w mul) (extract wm1 wm1 mul))) one))))))))))))
)

; rule: bv-smulo-elim
; implements: ProofRewriteRule::BV_SMULO_ELIM
; args:
Expand All @@ -32,6 +78,46 @@

;;;;; ProofRewriteRule::BV_UMULO_ELIM

; define: $bv_umulo_elim_rec
; args:
; - xa (BitVec n): An xor term involving the first argument to bvumulo
; - xb (BitVec n): An xor term involving the second argument to bvumulo
; - ppc (BitVec 1): An intermediate bitvector term accumulated to help construct the result.
; - res (BitVec 1): The current accumulated result.
; - i Int: The current bit we are processing.
; - nm2 Int: The bitwidth of a and b minus 2.
; return: >
; A portion of the result of eliminating (bvsmulo a b).
(program $bv_umulo_elim_rec ((n Int) (a (BitVec n)) (b (BitVec n))
(uppc (BitVec 1)) (res (BitVec 1)) (i Int))
((BitVec n) (BitVec n) (BitVec 1) (BitVec 1) Int Int) (BitVec 1)
(
(($bv_umulo_elim_rec a b uppc res n n) res)
(($bv_umulo_elim_rec a b uppc res i n)
(eo::define ((ia (eo::add n -1 (eo::neg i))))
(eo::define ((ip1 (eo::add i 1)))
(eo::define ((uppcn (bvor (extract ia ia a) uppc)))
(eo::cons bvor (bvand (extract i i b) uppc) ($bv_umulo_elim_rec a b uppcn res ip1 n))))))
)
)

; define: $bv_umulo_elim
; args:
; - a (BitVec n): The first argument to bvumulo
; - b (BitVec n): The second argument to bvumulo
; return: >
; The result of eliminating (bvumulo a b).
(define $bv_umulo_elim ((n Int :implicit) (a (BitVec n)) (b (BitVec n)))
(eo::define ((w ($bv_bitwidth (eo::typeof a))))
(eo::ite (eo::is_eq w 1)
false
(eo::define ((wm1 (eo::add w -1)))
(eo::define ((zero (eo::to_bin 1 0)))
(eo::define ((uppc (extract wm1 wm1 a)))
(eo::define ((mul (bvmul (concat zero a) (concat zero b))))
(eo::define ((res ($bv_umulo_elim_rec a b uppc (bvor (extract w w mul)) 1 w)))
(= res (eo::to_bin 1 1))))))))))

; rule: bv-umulo-elim
; implements: ProofRewriteRule::BV_UMULO_ELIM
; args:
Expand Down
2 changes: 1 addition & 1 deletion proofs/eo/cpc/rules/Rewrites.eo
View file
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,7 @@
(declare-rule arith-divisible-elim ((n1 Int) (t1 Int))
:premises ((= (= n1 0) false))
:args (n1 t1)
:conclusion (= (DIVISIBLE n1 t1) (= (mod_total t1 n1) 0))
:conclusion (= (divisible n1 t1) (= (mod_total t1 n1) 0))
)
(declare-rule arith-abs-eq ((@T0 Type) (@T1 Type) (x1 @T0) (y1 @T1))
:args (x1 y1)
Expand Down
1 change: 1 addition & 0 deletions src/printer/smt2/smt2_printer.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1217,6 +1217,7 @@ std::string Smt2Printer::smtKindString(Kind k)
case Kind::TO_INTEGER: return "to_int";
case Kind::TO_REAL: return "to_real";
case Kind::POW: return "^";
case Kind::DIVISIBLE: return "divisible";

// arrays theory
case Kind::SELECT: return "select";
Expand Down

0 comments on commit 81525a7

Please sign in to comment.