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).

diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt
index 6e9c8947d82e3ac5212ccaa0bcec9b5184ce0632..86474585c1c8ed027f4e0beeb6ac1064c63d2123 100644 (file)
--- 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 8f2d95a0f47ef49d295375d15e26940da2867b6c..3032951129c50f5c15e7b866c89af48f50534716 100644 (file)
--- 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 1712bb30adce1c7832d7c8291003606add864253..e21d1f6309a18743d9dccf92b7304ade8a71f4b0 100644 (file)
--- 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 170239e6f217f30c6b2dae4a3f154f98d73f1d65..a14c745a31fd3d4bae4390fa0020596f587a7f8e 100644 (file)
--- 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 b07a6bc4e43f565b7f4406d3050aec6857dbe234..87d762e54224935eaa4893c85f18838da03fc9c2 100644 (file)
--- 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 4508d1f8525363bf06620a6808333838b13bc6bf..2c762a941da9cffdcf8c2800b0766ee6273e2b70 100644 (file)
--- 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 d0e9bfed6b5d7de0a27c9ef284b42514e6f16ebd..84519b5cbe668b006d6edb863be7c8153bcb96e4 100644 (file)
--- 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 5985c500bdf5b10654c7452005c79931804f54ad..efdbc017ca43f19940a63041a8011ad41ab3f661 100644 (file)
--- 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 506b99b467a027ef4dce2a58bad654806628a682..ee04fbf3430ea8f3b846854c201a8e76a6398d4e 100644 (file)
--- 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 1c12e0770d388aa3ef9cec52fb709c98db17fc31..e6365f24c57069abcd309bdad2f4970b079b81c8 100644 (file)
--- 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 8f79b3d92005636a282ae66c4c7bd381e4575246..56ebea0669feaf16710cf1cd07fa7be45e812d43 100644 (file)
--- 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 b55197e50bc1b0eb217f21a7bc9024f01cc238f9..2cc53bef3d03536ea016dd9e7c63a6ebaeae4554 100644 (file)
--- 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 */