Switch to th_lira.plf (#3741)

Switches arith_proof.cpp from th_lra to th_lira.

Changes:

Eliminate the d_realMode hack.
instead: modify printOwnedTermAsType prints as integers OR
reals, depending on expectedType.
simultaneously: write printOwnedTermAsType more concisely
also: reimplement printOwnedSort.
Change to the LIRA axioms:
Because they reason about bound types using side conditions, we
no longer need to worry about choosing the correct strictness for
our axiom.
This allows us to cut out a lot of code, rewriting & shrinking
printTheoryLemmaProof.
They also have different names.
This requires us to change a lot of string literals
enable proof-checking for many tests.

11 files changed, 33 insertions, 19 deletions

diff --git a/test/regress/regress0/arith/arith-eq.smt2 b/test/regress/regress0/arith/arith-eq.smt2
index 661c3f242..38de29734 100644
--- a/test/regress/regress0/arith/arith-eq.smt2
+++ b/test/regress/regress0/arith/arith-eq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LRA)
 
diff --git a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
index a06621224..2f02c9d1e 100644
--- a/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
+++ b/test/regress/regress0/arith/arith-mixed-types-no-tighten.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LIRA)
 
diff --git a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2 b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
index 2f737d5c5..627118777 100644
--- a/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
+++ b/test/regress/regress0/arith/arith-mixed-types-tighten.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LIRA)
 
diff --git a/test/regress/regress0/arith/arith-mixed.smt2 b/test/regress/regress0/arith/arith-strict-relaxed.smt2
index 5869a51bd..fe17aa536 100644
--- a/test/regress/regress0/arith/arith-mixed.smt2
+++ b/test/regress/regress0/arith/arith-strict-relaxed.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LRA)
 
diff --git a/test/regress/regress0/arith/arith-strict.smt2 b/test/regress/regress0/arith/arith-strict.smt2
index 969cfd0bb..b1477732c 100644
--- a/test/regress/regress0/arith/arith-strict.smt2
+++ b/test/regress/regress0/arith/arith-strict.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LRA)
 
diff --git a/test/regress/regress0/arith/arith-tighten-1.smt2 b/test/regress/regress0/arith/arith-tighten-1.smt2
index 237d5b144..a8a5234a0 100644
--- a/test/regress/regress0/arith/arith-tighten-1.smt2
+++ b/test/regress/regress0/arith/arith-tighten-1.smt2
@@ -1,17 +1,19 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_LIRA)
 
-(declare-fun n () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun x () Real)
+(declare-fun y () Real)
 
-; tests tightenings of the form [Int] >= r   to [Int] >= ceiling(r)
-; where r is a real.
-(assert
-    (and
-        (>= n 1.5)
-        (<= n 1.9)
-    )
-)
+
+
+(assert (= x y))
+(assert (= x (- 2.5 y)))
+(assert (>= (+ i j) x))
+(assert (<= j (+ x 0.5)))
+(assert (<= i 0))
 
 (check-sat)
 
diff --git a/test/regress/regress0/arith/arith-tighten-2.smt2 b/test/regress/regress0/arith/arith-tighten-2.smt2
new file mode 100644
index 000000000..24eec2977
--- /dev/null
+++ b/test/regress/regress0/arith/arith-tighten-2.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_LIA)
+
+(declare-fun i () Int)
+(declare-fun j () Int)
+
+(assert (> (+ i j) 1))
+(assert (< i 1))
+(assert (< j 1))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2
index 1a63f265b..e1ca49ac5 100644
--- a/test/regress/regress0/arith/bug569.smt2
+++ b/test/regress/regress0/arith/bug569.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_AUFLIRA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/arith/integers/ackermann4.smt2 b/test/regress/regress0/arith/integers/ackermann4.smt2
index 1b76e1075..34aa56480 100644
--- a/test/regress/regress0/arith/integers/ackermann4.smt2
+++ b/test/regress/regress0/arith/integers/ackermann4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_ALIA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/arith/integers/ackermann5.smt2 b/test/regress/regress0/arith/integers/ackermann5.smt2
index 8b93a3c35..debd29344 100644
--- a/test/regress/regress0/arith/integers/ackermann5.smt2
+++ b/test/regress/regress0/arith/integers/ackermann5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models
 ; EXPECT: sat
 (set-logic QF_UFLIA)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/arith/integers/ackermann6.smt2 b/test/regress/regress0/arith/integers/ackermann6.smt2
index 62f2f1276..78f5a3658 100644
--- a/test/regress/regress0/arith/integers/ackermann6.smt2
+++ b/test/regress/regress0/arith/integers/ackermann6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFLIA)
 (set-info :smt-lib-version 2.0)