From c9e1adac517c5954e628c4088e4efb79b4ca8cec Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Fri, 24 Oct 2014 14:43:40 -0700 Subject: Add an option to use reduce Z3's knowledge of non-linear arithmetic. Results in more manual work, but it also produces more predictable behavior. --- Binaries/DafnyPrelude.bpl | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'Binaries/DafnyPrelude.bpl') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 9b410b1e..91d8a01a 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -1022,3 +1022,18 @@ axiom (forall m: Map U V, m': Map U V :: { Map#Disjoint(m, m') } Map#Disjoint(m, m') <==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o])); +// ------------------------------------------------------------------------- +// -- Provide arithmetic wrappers to improve triggering and non-linear math +// ------------------------------------------------------------------------- + +function INTERNAL_add_boogie(x:int, y:int) : int { x + y } +function INTERNAL_sub_boogie(x:int, y:int) : int { x - y } +function INTERNAL_mul_boogie(x:int, y:int) : int { x * y } +function INTERNAL_div_boogie(x:int, y:int) : int { x div y } +function INTERNAL_mod_boogie(x:int, y:int) : int { x mod y } +function {:never_pattern true} INTERNAL_lt_boogie(x:int, y:int) : bool { x < y } +function {:never_pattern true} INTERNAL_le_boogie(x:int, y:int) : bool { x <= y } +function {:never_pattern true} INTERNAL_gt_boogie(x:int, y:int) : bool { x > y } +function {:never_pattern true} INTERNAL_ge_boogie(x:int, y:int) : bool { x >= y } + +// ------------------------------------------------------------------------- -- cgit v1.2.3