summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorIavorDiatchki <>2019-01-10 23:16:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-01-10 23:16:00 (GMT)
commitccf851fe42ffdd879812a368f053ae40cfc6769c (patch)
tree993839436700368d642ccad793f93fcdbd5023cf
parent19635dcf8860641b8c65d3ea16cc51cdbddc3202 (diff)
version 1.1HEAD1.1master
-rwxr-xr-x[-rw-r--r--]CHANGES1
-rwxr-xr-x[-rw-r--r--]LICENSE0
-rw-r--r--smtLib.cabal2
-rw-r--r--src/SMTLib2/AST.hs1
-rw-r--r--src/SMTLib2/PP.hs1
5 files changed, 4 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index ea6ed95..c893540 100644..100755
--- a/CHANGES
+++ b/CHANGES
@@ -1 +1,2 @@
+1.1: Add declare-const
1.0: First release.
diff --git a/LICENSE b/LICENSE
index 174a268..174a268 100644..100755
--- a/LICENSE
+++ b/LICENSE
diff --git a/smtLib.cabal b/smtLib.cabal
index 9f8b8d6..9976ce8 100644
--- a/smtLib.cabal
+++ b/smtLib.cabal
@@ -1,5 +1,5 @@
Name: smtLib
-Version: 1.0.9
+Version: 1.1
License: BSD3
License-file: LICENSE
Author: Iavor S. Diatchki
diff --git a/src/SMTLib2/AST.hs b/src/SMTLib2/AST.hs
index 19d7e97..8ec0a13 100644
--- a/src/SMTLib2/AST.hs
+++ b/src/SMTLib2/AST.hs
@@ -85,6 +85,7 @@ data Command
| CmdSetInfo Attr
| CmdDeclareType Name Integer
| CmdDefineType Name [Name] Type
+ | CmdDeclareConst Name Type
| CmdDeclareFun Name [Type] Type
| CmdDefineFun Name [Binder] Type Expr
| CmdPush Integer
diff --git a/src/SMTLib2/PP.hs b/src/SMTLib2/PP.hs
index d25a726..156e73e 100644
--- a/src/SMTLib2/PP.hs
+++ b/src/SMTLib2/PP.hs
@@ -145,6 +145,7 @@ instance PP Command where
CmdSetInfo a -> std "set-info" a
CmdDeclareType x n -> mk "declare-sort" (pp x <+> integer n)
CmdDefineType x as t -> fun "define-sort" x as (pp t)
+ CmdDeclareConst x t -> mk "declare-const" (pp x <+> pp t)
CmdDeclareFun x ts t -> fun "declare-fun" x ts (pp t)
CmdDefineFun x bs t e -> fun "define-fun" x bs (pp t $$ nest 2 (pp e))
CmdPush n -> std "push" n