Add div, mod, abs in non-strict parsing mode (#5793)

The recent change to the parser currently breaks our performance on several critical applications, including the use of CVC4 in Facebook. We should only throw a parse error for div in linear logics when strict mode is enabled.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 0c67299ab54abee17fede0e32adf37fa4a66f274..9c5474a4785a41dd59d4b04b18c0208b107a6934 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -550,7 +550,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     if(d_logic.areIntegersUsed()) {
       defineType("Int", d_solver->getIntegerSort(), true, true);
       addArithmeticOperators();
-      if (!d_logic.isLinear())
+      if (!strictModeEnabled() || !d_logic.isLinear())
       {
         addOperator(api::INTS_DIVISION, "div");
         addOperator(api::INTS_MODULUS, "mod");

diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 58a8a3e76aed5aceb11419092ef75a7f2d91ca3e..9c3751a8c57d9d95e6fb5610b91ac8ab9a4f94c9 100644 (file)
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,5 +1,5 @@
 ; REQUIRES: no-competition
-; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --no-sygus-repair-const
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --no-sygus-repair-const --strict-parsing
 ; ERROR-SCRUBBER: grep -o "Symbol 'div' not declared as a variable"
 ; EXPECT-ERROR: Symbol 'div' not declared as a variable
 ; EXIT: 1

diff --git a/test/regress/regress0/parser/linear_arithmetic_err1.smt2 b/test/regress/regress0/parser/linear_arithmetic_err1.smt2
index 219b59d445f405a22a2b7bc642d27f56996a2f0c..f031cded8505fd3dd5508945d6280d91de472dea 100644 (file)
--- a/test/regress/regress0/parser/linear_arithmetic_err1.smt2
+++ b/test/regress/regress0/parser/linear_arithmetic_err1.smt2
@@ -1,4 +1,5 @@
 ; REQUIRES: no-competition
+; COMMAND-LINE: --strict-parsing
 ; SCRUBBER: grep -o "Symbol 'div' not declared as a variable"
 ; EXPECT: Symbol 'div' not declared as a variable
 ; EXIT: 1

diff --git a/test/regress/regress0/parser/linear_arithmetic_err2.smt2 b/test/regress/regress0/parser/linear_arithmetic_err2.smt2
index 893708b618a56a6901ad5208a1103cab3bdbf830..adaa0aff4c5d96e088ec3eb1a4ca8a6bd65971df 100644 (file)
--- a/test/regress/regress0/parser/linear_arithmetic_err2.smt2
+++ b/test/regress/regress0/parser/linear_arithmetic_err2.smt2
@@ -1,4 +1,5 @@
 ; REQUIRES: no-competition
+; COMMAND-LINE: --strict-parsing
 ; SCRUBBER: grep -o "Symbol 'mod' not declared as a variable"
 ; EXPECT: Symbol 'mod' not declared as a variable
 ; EXIT: 1

diff --git a/test/regress/regress0/parser/linear_arithmetic_err3.smt2 b/test/regress/regress0/parser/linear_arithmetic_err3.smt2
index 89748b36f973aaeef17084adc5e047857e9e5126..d875e4cbe92e224af34886337597dd6ea844d9f6 100644 (file)
--- a/test/regress/regress0/parser/linear_arithmetic_err3.smt2
+++ b/test/regress/regress0/parser/linear_arithmetic_err3.smt2
@@ -1,4 +1,5 @@
 ; REQUIRES: no-competition
+; COMMAND-LINE: --strict-parsing
 ; SCRUBBER: grep -o "Symbol 'abs' not declared as a variable"
 ; EXPECT: Symbol 'abs' not declared as a variable
 ; EXIT: 1