From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 21 Jan 2021 18:07:50 +0000 (-0600)
Subject: Add div, mod, abs in non-strict parsing mode (#5793)
X-Git-Tag: cvc5-1.0.0~2368
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98d2ca3ee48cb87e8baa7537c97016cc85ab048d;p=cvc5.git

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 0c67299ab..9c5474a47 100644
--- 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 58a8a3e76..9c3751a8c 100644
--- 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 219b59d44..f031cded8 100644
--- 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 893708b61..adaa0aff4 100644
--- 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 89748b36f..d875e4cbe 100644
--- 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