summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorIavorDiatchki <>2019-02-15 18:34:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-02-15 18:34:00 (GMT)
commitfc782a4845e249fa44569cabc4ecc34c2d9e9edf (patch)
treedeecffd0c4821986329958e49dbe446373e08fd1
parent3d87ddcb0b91ee8fc93ec138d53954262614f576 (diff)
version 0.9.4HEAD0.9.4master
-rwxr-xr-x[-rw-r--r--]CHANGES1
-rw-r--r--SimpleSMT.hs10
-rw-r--r--simple-smt.cabal2
3 files changed, 12 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index a6c4e94..bedfdcb 100644..100755
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,4 @@
+0.9.4: Add `toInt` and `toReal`
0.9.3: Fix incorrect rendering or `real` literals
0.9.2: add ppSExpr
0.9: Support for working with unsat-cores
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
index d484ec6..cd0b3cf 100644
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -100,6 +100,8 @@ module SimpleSMT
, mod
, divisible
, realDiv
+ , toInt
+ , toReal
-- ** Bit Vectors
, concat
@@ -792,6 +794,14 @@ signExtend i x = List [ fam "sign_extend" [i], x ]
zeroExtend :: Integer -> SExpr -> SExpr
zeroExtend i x = List [ fam "zero_extend" [i], x ]
+-- | Satisfies @toInt x <= x@ (i.e., this is like Haskell's 'floor')
+toInt :: SExpr -> SExpr
+toInt e = fun "to_int" [e]
+
+-- | Promote an integer to a real
+toReal :: SExpr -> SExpr
+toReal e = fun "to_real" [e]
+
-- | Extract a sub-sequence of a bit vector.
extract :: SExpr -> Integer -> Integer -> SExpr
extract x y z = List [ fam "extract" [y,z], x ]
diff --git a/simple-smt.cabal b/simple-smt.cabal
index d812e9c..aad1467 100644
--- a/simple-smt.cabal
+++ b/simple-smt.cabal
@@ -1,5 +1,5 @@
name: simple-smt
-version: 0.9.3
+version: 0.9.4
synopsis: A simple way to interact with an SMT solver process.
description: A simple way to interact with an SMT solver process.
license: BSD3