From: Andres Noetzli Date: Tue, 4 Jun 2019 23:37:27 +0000 (-0700) Subject: Enable proof checking for QF_LRA benchmarks (#2928) X-Git-Tag: cvc5-1.0.0~4125 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0536a743411b882cda88b18ca21cd5dc29828f54;p=cvc5.git 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 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 #include +#include #include +#include #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 */