Added declare-sort and define-sort to the SMT2 frontend

SRI-CSL · Jun 18, 2017 · 6c24d78 · 6c24d78 · dddejan · Jun 18, 2017
1 parent 90fd296
commit 6c24d78
Show file tree

Hide file tree

Showing 11 changed files with 204 additions and 132 deletions.
diff --git a/Makefile.build b/Makefile.build
@@ -451,7 +451,6 @@ install-default: $(build_dir) $(dist_dir)
 	$(INSTALL) $(dist_dir)/bin/* $(DESTDIR)$(bindir)
 	$(INSTALL) $(dist_dir)/lib/* $(DESTDIR)$(libdir)
 
-
 install-darwin: install-default
 	(cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.$(MAJOR).dylib libyices.dylib)
 

diff --git a/src/frontend/smt2/smt2_expressions.c b/src/frontend/smt2/smt2_expressions.c
@@ -73,8 +73,10 @@ void push_smt2_token(etk_queue_t *queue, smt2_token_t tk, const char *str, uint3
   case SMT2_TK_ASSERT:
   case SMT2_TK_CHECK_SAT:
   case SMT2_TK_DECLARE_SORT:
+  case SMT2_TK_DECLARE_CONST:
   case SMT2_TK_DECLARE_FUN:
   case SMT2_TK_DEFINE_SORT:
+  case SMT2_TK_DEFINE_CONST:
   case SMT2_TK_DEFINE_FUN:
   case SMT2_TK_EXIT:
   case SMT2_TK_GET_ASSERTIONS:
@@ -149,8 +151,10 @@ static void pp_smt2_token(yices_pp_t *printer, etoken_t *token) {
   case SMT2_TK_ASSERT:
   case SMT2_TK_CHECK_SAT:
   case SMT2_TK_DECLARE_SORT:
+  case SMT2_TK_DECLARE_CONST:
   case SMT2_TK_DECLARE_FUN:
   case SMT2_TK_DEFINE_SORT:
+  case SMT2_TK_DEFINE_CONST:
   case SMT2_TK_DEFINE_FUN:
   case SMT2_TK_EXIT:
   case SMT2_TK_GET_ASSERTIONS:

diff --git a/src/frontend/smt2/smt2_lexer.c b/src/frontend/smt2/smt2_lexer.c
@@ -60,8 +60,10 @@ static const char * const smt2_token_string[NUM_SMT2_TOKENS] = {
   "assert",                // SMT2_TK_ASSERT
   "check-sat",             // SMT2_TK_CHECK_SAT
   "declare-sort",          // SMT2_TK_DECLARE_SORT
+  "declare-const",         // SMT2_TK_DECLARE_CONST
   "declare-fun",           // SMT2_TK_DECLARE_FUN
   "define-sort",           // SMT2_TK_DEFINE_SORT
+  "define-const",          // SMT2_TK_DEFINE_CONST
   "define-fun",            // SMT2_TK_DEFINE_FUN
   "exit",                  // SMT2_TK_EXIT
   "get-assertions",        // SMT2_TK_GET_ASSERTIONS

diff --git a/src/frontend/smt2/smt2_lexer.h b/src/frontend/smt2/smt2_lexer.h
@@ -71,8 +71,10 @@ enum smt2_token {
   SMT2_TK_ASSERT,
   SMT2_TK_CHECK_SAT,
   SMT2_TK_DECLARE_SORT,
+  SMT2_TK_DECLARE_CONST,
   SMT2_TK_DECLARE_FUN,
   SMT2_TK_DEFINE_SORT,
+  SMT2_TK_DEFINE_CONST,
   SMT2_TK_DEFINE_FUN,
   SMT2_TK_EXIT,
   SMT2_TK_GET_ASSERTIONS,