SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)

This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.

More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.

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

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d35758d5c200a2bafa7b96c4a7e61877c956a00a..328f7df8c8e0fcd658f849d2e925b5ca475faa26 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -722,6 +722,9 @@ set(regress_0_tests
   regress0/parser/force_logic_set_logic.smt2
   regress0/parser/force_logic_success.smt2
   regress0/parser/issue5163.smt2
+  regress0/parser/linear_arithmetic_err1.smt2
+  regress0/parser/linear_arithmetic_err2.smt2
+  regress0/parser/linear_arithmetic_err3.smt2
   regress0/parser/shadow_fun_symbol_all.smt2
   regress0/parser/shadow_fun_symbol_nirat.smt2
   regress0/parser/strings20.smt2

diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2
index c7771d5c9c8953ff4c2da0adddcb3655f917fb76..90aca07c3a9a2ccb9264538949191f3202bb16c0 100644 (file)
--- a/test/regress/regress0/arith/div-chainable.smt2
+++ b/test/regress/regress0/arith/div-chainable.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: -q
 ; EXPECT: sat
-(set-logic QF_LIA)
+(set-logic QF_NIA)
 (set-info :status sat)
 
 (declare-fun x () Int)

diff --git a/test/regress/regress0/arith/issue1399.smt2 b/test/regress/regress0/arith/issue1399.smt2
index 80305260e19c4ac5ec73bf8f39224262286eb995..d19addf9190e3a677fdaa7f8cf303c779b7e7e9b 100644 (file)
--- a/test/regress/regress0/arith/issue1399.smt2
+++ b/test/regress/regress0/arith/issue1399.smt2
@@ -1,4 +1,4 @@
-(set-logic LIA)
+(set-logic NIA)
 (set-info :status sat)
 
 (define-fun findIdx ((y1 Int)(y2 Int)(k1 Int)) Int (div (* (- 7) (mod y1 (- 5))) 2))

diff --git a/test/regress/regress0/arith/mod-simp.smt2 b/test/regress/regress0/arith/mod-simp.smt2
index 1a9c50590d49a694b1e2131c34e81a5d0b1eec5c..57ccd465213fe0c3f76b5e756938e50104a0a076 100644 (file)
--- a/test/regress/regress0/arith/mod-simp.smt2
+++ b/test/regress/regress0/arith/mod-simp.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_LIA)
+(set-logic QF_NIA)
 (set-info :status unsat)
 
 (declare-fun x () Int)

diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2
index 581c34f2dfc44de5ec64069bc7c313c87926d37b..0c4f1f4542964ef153c41f9745f8c647a1d096d9 100644 (file)
--- a/test/regress/regress0/bug548a.smt2
+++ b/test/regress/regress0/bug548a.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --tlimit 1000
 ; EXPECT: unknown
-(set-logic AUFLIA)
+(set-logic AUFNIA)
 (declare-fun f (Int) Int)
 
 

diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 592189df25c65f5afd7ed1b7e9f7e4f1e6d4b3c4..58a8a3e76aed5aceb11419092ef75a7f2d91ca3e 100644 (file)
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,8 +1,7 @@
+; REQUIRES: no-competition
 ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --no-sygus-repair-const
-; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
-; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
-; EXPECT: The fact in question: TERM
-; EXPECT: ")
+; ERROR-SCRUBBER: grep -o "Symbol 'div' not declared as a variable"
+; EXPECT-ERROR: Symbol 'div' not declared as a variable
 ; EXIT: 1
 (set-logic LIA)
 (declare-var n Int)

diff --git a/test/regress/regress0/parser/linear_arithmetic_err1.smt2 b/test/regress/regress0/parser/linear_arithmetic_err1.smt2
new file mode 100644 (file)
index 0000000..219b59d
--- /dev/null
+++ b/test/regress/regress0/parser/linear_arithmetic_err1.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "Symbol 'div' not declared as a variable"
+; EXPECT: Symbol 'div' not declared as a variable
+; EXIT: 1
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(check-sat-assuming ( (and (= z 0) (>= (+ (- (div 2 x) (* 2 y)) z) 1)) ))

diff --git a/test/regress/regress0/parser/linear_arithmetic_err2.smt2 b/test/regress/regress0/parser/linear_arithmetic_err2.smt2
new file mode 100644 (file)
index 0000000..893708b
--- /dev/null
+++ b/test/regress/regress0/parser/linear_arithmetic_err2.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "Symbol 'mod' not declared as a variable"
+; EXPECT: Symbol 'mod' not declared as a variable
+; EXIT: 1
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(check-sat-assuming ( (and (= z 0) (>= (+ (- (mod 2 x) (* 2 y)) z) 1)) ))

diff --git a/test/regress/regress0/parser/linear_arithmetic_err3.smt2 b/test/regress/regress0/parser/linear_arithmetic_err3.smt2
new file mode 100644 (file)
index 0000000..89748b3
--- /dev/null
+++ b/test/regress/regress0/parser/linear_arithmetic_err3.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "Symbol 'abs' not declared as a variable"
+; EXPECT: Symbol 'abs' not declared as a variable
+; EXIT: 1
+(set-option :incremental false)
+(set-info :status sat)
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(check-sat-assuming ( (and (= z 0) (>= (+ (- (abs 2 x) (* 2 y)) z) 1)) ))

diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
index dd9cb68863a4dd40d97edace39cc0d001207dfdf..efcae64bcf9f15b3e1a620aab5a117d7bf82981f 100644 (file)
--- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
+++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --fmf-fun --no-check-models
 ; EXPECT: sat
-(set-logic UFLIA)
+(set-logic UFNIA)
 (set-info :status sat)
 (define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool (
     or

diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
index ea5a5e4b74807bc4ad0568272e3b5e01a29a393c..32e9d4178f03a59adc9ac0fce73ca65cdb02234f 100644 (file)
--- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
+++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --fmf-fun --no-check-models
 ; EXPECT: sat
-(set-logic UFLIA)
+(set-logic UFNIA)
 (set-info :status sat)
 (define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool (
     or

diff --git a/test/regress/regress1/quantifiers/issue5484-qe.smt2 b/test/regress/regress1/quantifiers/issue5484-qe.smt2
index c2499ed169927cbbdf51ba12fccde87dcba7a681..9fcc7dcba46738293a5528705a2f6d1c115dde55 100644 (file)
--- a/test/regress/regress1/quantifiers/issue5484-qe.smt2
+++ b/test/regress/regress1/quantifiers/issue5484-qe.smt2
@@ -1,7 +1,8 @@
+; COMMAND-LINE: -q
 ; SCRUBBER: sed 's/(.*)/()/g'
 ; EXPECT: ()
 ; EXIT: 0
-(set-logic LIA)
+(set-logic NIA)
 (declare-fun v9 () Bool)
 (declare-fun v18 () Bool)
 (declare-fun i2 () Int)

diff --git a/test/regress/regress1/quantifiers/issue5484b-qe.smt2 b/test/regress/regress1/quantifiers/issue5484b-qe.smt2
index 86f999504bf4f87439588135fbddc566bef614a5..754603135f9b12a93f52578edc2dfb6393d3856e 100644 (file)
--- a/test/regress/regress1/quantifiers/issue5484b-qe.smt2
+++ b/test/regress/regress1/quantifiers/issue5484b-qe.smt2
@@ -1,7 +1,8 @@
+; COMMAND-LINE: -q
 ; SCRUBBER: sed 's/(.*)/()/g'
 ; EXPECT: ()
 ; EXIT: 0
-(set-logic LIA)
+(set-logic NIA)
 (declare-fun v0 () Bool)
 (declare-fun v1 () Bool)
 (declare-fun v2 () Bool)

diff --git a/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 b/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2
index bd42e35969dfebad28ff3fcd6966a91ee6a740e4..62babf518a54cc7f467bf64320c9bc46b035afd9 100644 (file)
--- a/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2
+++ b/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.6)
-(set-logic LIA)
+(set-logic NIA)
 (set-info :status unsat)
 (declare-fun c_main_~x~0 () Int)
 (declare-fun c_main_~y~0 () Int)

diff --git a/test/regress/regress2/sygus/three.sy b/test/regress/regress2/sygus/three.sy
index 44974caf1a171c6fe2a38f93349cd78566551ea7..239f7f49810d74f5dc9ef67acd4d28693bc655f2 100644 (file)
--- a/test/regress/regress2/sygus/three.sy
+++ b/test/regress/regress2/sygus/three.sy
@@ -1,7 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
-(set-logic LIA)
+(set-logic NIA)
 
 (synth-fun f ((x Int)) Int
     ((Start Int))