Refactor parser to define fewer tokens for symbols (#2936)

21 files changed, 26 insertions, 20 deletions

diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2
index c7a5a605f..1e2bcde68 100644
--- a/test/regress/regress0/bv/core/constant_core.smt2
+++ b/test/regress/regress0/bv/core/constant_core.smt2
@@ -12,4 +12,4 @@
 (not (= (_ bv0 3) x))
 ))
 (check-sat)
-(exit)
\ No newline at end of file
+(exit)
diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 24a0aab2e..aec265f2b 100644
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -8,5 +8,5 @@
 (declare-var n Int)
 
 (synth-fun f ((n Int)) Int)
-(constraint (= (/ n n) 1))
+(constraint (= (div n n) 1))
 (check-synth)
diff --git a/test/regress/regress0/nl/nta/real-pi.smt2 b/test/regress/regress0/nl/nta/real-pi.smt2
index a303f48b1..4163e09f9 100644
--- a/test/regress/regress0/nl/nta/real-pi.smt2
+++ b/test/regress/regress0/nl/nta/real-pi.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --no-check-models
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (assert (<= 3.0 real.pi))
 (assert (<= real.pi 4.0))
diff --git a/test/regress/regress0/strings/bug613.smt2 b/test/regress/regress0/strings/bug613.smt2
index 506076cd6..09c5e9a2a 100644
--- a/test/regress/regress0/strings/bug613.smt2
+++ b/test/regress/regress0/strings/bug613.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
 
diff --git a/test/regress/regress0/strings/str004.smt2 b/test/regress/regress0/strings/str004.smt2
index 8a03f4481..21570a2da 100644
--- a/test/regress/regress0/strings/str004.smt2
+++ b/test/regress/regress0/strings/str004.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
index 89191ac34..36a6aaec1 100644
--- a/test/regress/regress0/strings/type001.smt2
+++ b/test/regress/regress0/strings/type001.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
 
diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2
index 2b25e6dc8..9c91d135f 100644
--- a/test/regress/regress0/strings/unsound-0908.smt2
+++ b/test/regress/regress0/strings/unsound-0908.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (declare-const x String)
 (assert (= (str.len x) 1))
diff --git a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
index a3cca23a2..328317ea4 100644
--- a/test/regress/regress1/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
 
diff --git a/test/regress/regress1/strings/at001.smt2 b/test/regress/regress1/strings/at001.smt2
index 2ecbcc993..04933b8f7 100644
--- a/test/regress/regress1/strings/at001.smt2
+++ b/test/regress/regress1/strings/at001.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress1/strings/fmf002.smt2 b/test/regress/regress1/strings/fmf002.smt2
index ab3dc2ae2..2f2209ae7 100644
--- a/test/regress/regress1/strings/fmf002.smt2
+++ b/test/regress/regress1/strings/fmf002.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/issue2429-code.smt2 b/test/regress/regress1/strings/issue2429-code.smt2
index 2d906c1fd..9dc29794e 100644
--- a/test/regress/regress1/strings/issue2429-code.smt2
+++ b/test/regress/regress1/strings/issue2429-code.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-option :produce-models true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/kaluza-fl.smt2 b/test/regress/regress1/strings/kaluza-fl.smt2
index 20c2e6aa4..d277d85e6 100644
--- a/test/regress/regress1/strings/kaluza-fl.smt2
+++ b/test/regress/regress1/strings/kaluza-fl.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 
 (declare-fun I0_15 () Int)
diff --git a/test/regress/regress1/strings/loop005.smt2 b/test/regress/regress1/strings/loop005.smt2
index 039409ea6..cc115ebf4 100644
--- a/test/regress/regress1/strings/loop005.smt2
+++ b/test/regress/regress1/strings/loop005.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress1/strings/loop007.smt2 b/test/regress/regress1/strings/loop007.smt2
index a97d97d54..492162ae6 100644
--- a/test/regress/regress1/strings/loop007.smt2
+++ b/test/regress/regress1/strings/loop007.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/loop008.smt2 b/test/regress/regress1/strings/loop008.smt2
index f84ba442b..672ecd371 100644
--- a/test/regress/regress1/strings/loop008.smt2
+++ b/test/regress/regress1/strings/loop008.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/re-agg-total1.smt2 b/test/regress/regress1/strings/re-agg-total1.smt2
index 4e5b21c0f..2950066a0 100644
--- a/test/regress/regress1/strings/re-agg-total1.smt2
+++ b/test/regress/regress1/strings/re-agg-total1.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.6)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)
 (set-option :re-elim-agg true)
diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2
index 967e564ce..22537b957 100644
--- a/test/regress/regress1/strings/reloop.smt2
+++ b/test/regress/regress1/strings/reloop.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/substr001.smt2 b/test/regress/regress1/strings/substr001.smt2
index 78f3ffee7..47fa995ff 100644
--- a/test/regress/regress1/strings/substr001.smt2
+++ b/test/regress/regress1/strings/substr001.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress1/strings/type002.smt2 b/test/regress/regress1/strings/type002.smt2
index 458ac75fe..3b46b25a8 100644
--- a/test/regress/regress1/strings/type002.smt2
+++ b/test/regress/regress1/strings/type002.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
 
diff --git a/test/regress/regress1/strings/type003.smt2 b/test/regress/regress1/strings/type003.smt2
index 4185041f7..332ec3ec3 100644
--- a/test/regress/regress1/strings/type003.smt2
+++ b/test/regress/regress1/strings/type003.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
 
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 33ad3740a..f2f5f24b6 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -138,6 +138,12 @@ class ParserBlack
                            .withInputLanguage(d_lang)
                            .build();
 
+      if (d_lang == LANG_SMTLIB_V2)
+      {
+        // Use QF_LIA to make multiplication ("*") available
+        static_cast<Smt2*>(parser)->setLogic("QF_LIA");
+      }
+
       TS_ASSERT(!parser->done());
       setupContext(*parser);
       TS_ASSERT(!parser->done());