Enable proof checking for QF_LRA benchmarks (#2928)

Due to issues in the current proof code, this commit also disables proof
checking for five QF_LRA benchmarks (see issue #2855).

12 files changed, 38 insertions, 15 deletions

diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt
index 6e9c8947d..86474585c 100644
--- a/proofs/signatures/CMakeLists.txt
+++ b/proofs/signatures/CMakeLists.txt
@@ -16,6 +16,7 @@ set(core_signature_files
     th_bv_rewrites.plf
     th_real.plf
     th_int.plf
+    th_lra.plf
 )
 
 set(CORE_SIGNATURES "")
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8f2d95a0f..303295112 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4437,13 +4437,7 @@ void SmtEngine::checkProof()
 
   std::string logicString = d_logic.getLogicString();
 
-  if (!(
-          // Pure logics
-          logicString == "QF_UF" || logicString == "QF_AX"
-          || logicString == "QF_BV" ||
-          // Non-pure logics
-          logicString == "QF_AUF" || logicString == "QF_UFBV"
-          || logicString == "QF_ABV" || logicString == "QF_AUFBV"))
+  if (!(d_logic <= LogicInfo("QF_AUFBVLRA")))
   {
     // This logic is not yet supported
     Notice() << "Notice: no proof-checking for " << logicString << " proofs yet"
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 1712bb30a..e21d1f630 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -17,9 +17,10 @@
  **/
 #include "theory/logic_info.h"
 
-#include <string>
 #include <cstring>
+#include <iostream>
 #include <sstream>
+#include <string>
 
 #include "base/cvc4_assert.h"
 #include "expr/kind.h"
@@ -207,13 +208,15 @@ bool LogicInfo::operator==(const LogicInfo& other) const {
 
   PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = d_cardinalityConstraints == other.d_cardinalityConstraints
+             && d_higherOrder == other.d_higherOrder;
   if(isTheoryEnabled(theory::THEORY_ARITH)) {
     return d_integers == other.d_integers && d_reals == other.d_reals
            && d_transcendentals == other.d_transcendentals
            && d_linear == other.d_linear
-           && d_differenceLogic == other.d_differenceLogic;
+           && d_differenceLogic == other.d_differenceLogic && res;
   } else {
-    return true;
+    return res;
   }
 }
 
@@ -227,13 +230,15 @@ bool LogicInfo::operator<=(const LogicInfo& other) const {
   }
   PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = (!d_cardinalityConstraints || other.d_cardinalityConstraints)
+             && (!d_higherOrder || other.d_higherOrder);
   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
     return (!d_integers || other.d_integers) && (!d_reals || other.d_reals)
            && (!d_transcendentals || other.d_transcendentals)
            && (d_linear || !other.d_linear)
-           && (d_differenceLogic || !other.d_differenceLogic);
+           && (d_differenceLogic || !other.d_differenceLogic) && res;
   } else {
-    return true;
+    return res;
   }
 }
 
@@ -247,13 +252,15 @@ bool LogicInfo::operator>=(const LogicInfo& other) const {
   }
   PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this,
                       "LogicInfo internal inconsistency");
+  bool res = (d_cardinalityConstraints || !other.d_cardinalityConstraints)
+             && (d_higherOrder || !other.d_higherOrder);
   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
     return (d_integers || !other.d_integers) && (d_reals || !other.d_reals)
            && (d_transcendentals || !other.d_transcendentals)
            && (!d_linear || other.d_linear)
-           && (!d_differenceLogic || other.d_differenceLogic);
+           && (!d_differenceLogic || other.d_differenceLogic) && res;
     } else {
-    return true;
+      return res;
   }
 }
 
diff --git a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt
index 170239e6f..a14c745a3 100644
--- a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt
+++ b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark sc_init_frame_gap.induction.smt
   :source {
 The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html.
diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt
index b07a6bc4e..87d762e54 100644
--- a/test/regress/regress0/uflra/constants0.smt
+++ b/test/regress/regress0/uflra/constants0.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark mathsat
 :logic QF_UFLRA
 :status unsat 
@@ -12,4 +13,4 @@
      (implies (= (f 3) (f x)) (= (f 5) (f x)))
      (implies (= (f 3) (f y)) (= (f 5) (f y)))
 )
-)
\ No newline at end of file
+)
diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt
index 4508d1f85..2c762a941 100644
--- a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt
+++ b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark mathsat
 :source { MathSat group }
 :logic QF_UFLRA
diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt
index d0e9bfed6..84519b5cb 100644
--- a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt
+++ b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark mathsat
 :source { MathSat group }
 :logic QF_UFLRA
diff --git a/test/regress/regress1/lemmas/pursuit-safety-8.smt b/test/regress/regress1/lemmas/pursuit-safety-8.smt
index 5985c500b..efdbc017c 100644
--- a/test/regress/regress1/lemmas/pursuit-safety-8.smt
+++ b/test/regress/regress1/lemmas/pursuit-safety-8.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark pursuit_safety_8.smt
   :source {
 SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt
index 506b99b46..ee04fbf34 100644
--- a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt
+++ b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark tta_startup
   :source { TTA Startup. Bruno Dutertre (bruno@csl.sri.com) }
 
diff --git a/test/regress/regress2/arith/pursuit-safety-11.smt b/test/regress/regress2/arith/pursuit-safety-11.smt
index 1c12e0770..e6365f24c 100644
--- a/test/regress/regress2/arith/pursuit-safety-11.smt
+++ b/test/regress/regress2/arith/pursuit-safety-11.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark pursuit_safety_11.smt
   :source {
 SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
diff --git a/test/regress/regress2/arith/pursuit-safety-12.smt b/test/regress/regress2/arith/pursuit-safety-12.smt
index 8f79b3d92..56ebea066 100644
--- a/test/regress/regress2/arith/pursuit-safety-12.smt
+++ b/test/regress/regress2/arith/pursuit-safety-12.smt
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --no-check-proofs
 (benchmark pursuit_safety_12.smt
   :source {
 SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index b55197e50..2cc53bef3 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -732,6 +732,10 @@ public:
   }
 
   void testComparison() {
+    LogicInfo ufHo = LogicInfo("QF_UF").getUnlockedCopy();
+    ufHo.enableHigherOrder();
+    ufHo.lock();
+
     eq("QF_UF", "QF_UF");
     nc("QF_UF", "QF_LRA");
     nc("QF_UF", "QF_LIA");
@@ -756,6 +760,9 @@ public:
     lt("QF_UF", "AUFLIA");
     lt("QF_UF", "AUFLIRA");
     lt("QF_UF", "AUFNIRA");
+    lt("QF_UF", "QF_UFC");
+    lt("QF_UF", ufHo);
+    nc("QF_UFC", ufHo);
 
     nc("QF_LRA", "QF_UF");
     eq("QF_LRA", "QF_LRA");
@@ -781,6 +788,7 @@ public:
     nc("QF_LRA", "AUFLIA");
     lt("QF_LRA", "AUFLIRA");
     lt("QF_LRA", "AUFNIRA");
+    lt("QF_LRA", "QF_UFCLRA");
 
     nc("QF_LIA", "QF_UF");
     nc("QF_LIA", "QF_LRA");
@@ -1335,6 +1343,11 @@ public:
     gt("AUFNIRA", "AUFLIRA");
     eq("AUFNIRA", "AUFNIRA");
     lt("AUFNIRA", "AUFNIRAT");
+
+    gt("QF_UFC", "QF_UF");
+    gt("QF_UFCLRA", "QF_UFLRA");
+
+    gt(ufHo, "QF_UF");
   }
 
 };/* class LogicInfoWhite */