[proof-new] Catch trivial cycles in SAT proof generation (#5853)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from

       l1 v l2   ~l1 v l3   ~l2 v l3
(ok) ------------------------------
                  l3
in which l3 = l1 v l2, to

         l1 v l2   ~l1 v l3   ~l2 v l3
(bad) ------------------------------
               l3 v l3
              ---------
                 l3
This commit now catches the trivial cycle before it's generated.

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index aae11ae51b3393575fd3a1fe1e4c7812eaf494f1..dd7e94f0398e879b66acbd3c1197b6d3c2752738 100644 (file)
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -228,6 +228,17 @@ void SatProofManager::endResChain(Node conclusion,
                        << children[0] << "\n";
     return;
   }
+  // whether trivial cycle
+  for (const Node& child : children)
+  {
+    if (conclusion == child)
+    {
+      Trace("sat-proof")
+          << "SatProofManager::endResChain: no-op. The conclusion "
+          << conclusion << " is equal to a premise\n";
+      return;
+    }
+  }
   if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion))
   {
     Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of "

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5e0fa2495140209bb1173c9cc59e28bbdeec6399..e158f629a0f528c97c33cf5cfa28eead47d41365 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1633,6 +1633,7 @@ set(regress_1_tests
   regress1/proof00.smt2
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
   regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
+  regress1/proofs/sat-trivial-cycle.smt2
   regress1/push-pop/arith_lra_01.smt2
   regress1/push-pop/arith_lra_02.smt2
   regress1/push-pop/bug-fmf-fun-skolem.smt2

diff --git a/test/regress/regress1/proofs/sat-trivial-cycle.smt2 b/test/regress/regress1/proofs/sat-trivial-cycle.smt2
new file mode 100644 (file)
index 0000000..e8d163c
--- /dev/null
+++ b/test/regress/regress1/proofs/sat-trivial-cycle.smt2
@@ -0,0 +1,189 @@
+; EXPECT: unsat
+;; minimized from UFLIA/tokeneer/enclave/progressadminactivity-3.smt2
+(set-info :smt-lib-version 2.6)
+(set-logic UFLIA)
+(set-info :source |
+      Tokeneer case study <http://www.adacore.com/home/products/gnatpro/tokeneer/>
+  |)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun field.statetype.status () Int)
+(declare-fun admin__archivelog () Int)
+(declare-fun admin__nullop () Int)
+(declare-fun admin__opandnullt__base__first () Int)
+(declare-fun admin__opandnullt__base__last () Int)
+(declare-fun admin__opandnullt__first () Int)
+(declare-fun admin__opandnullt__last () Int)
+(declare-fun admin__opandnullt__size () Int)
+(declare-fun admin__overridelock () Int)
+(declare-fun admin__shutdownop () Int)
+(declare-fun admin__updateconfigdata () Int)
+(declare-fun alarmtypes__alarming () Int)
+(declare-fun alarmtypes__silent () Int)
+(declare-fun alarmtypes__statust__base__first () Int)
+(declare-fun alarmtypes__statust__base__last () Int)
+(declare-fun alarmtypes__statust__first () Int)
+(declare-fun alarmtypes__statust__last () Int)
+(declare-fun alarmtypes__statust__size () Int)
+(declare-fun door__closed () Int)
+(declare-fun door__open () Int)
+(declare-fun door__t__base__first () Int)
+(declare-fun door__t__base__last () Int)
+(declare-fun door__t__first () Int)
+(declare-fun door__t__last () Int)
+(declare-fun door__t__size () Int)
+(declare-fun enclavequiescent () Int)
+(declare-fun gotadmintoken () Int)
+(declare-fun nonquiescentstates__base__first () Int)
+(declare-fun nonquiescentstates__base__last () Int)
+(declare-fun nonquiescentstates__first () Int)
+(declare-fun nonquiescentstates__last () Int)
+(declare-fun nonquiescentstates__size () Int)
+(declare-fun notenrolled () Int)
+(declare-fun privtypes__auditmanager () Int)
+(declare-fun privtypes__guard () Int)
+(declare-fun privtypes__privileget__base__first () Int)
+(declare-fun privtypes__privileget__base__last () Int)
+(declare-fun privtypes__privileget__first () Int)
+(declare-fun privtypes__privileget__last () Int)
+(declare-fun privtypes__privileget__size () Int)
+(declare-fun privtypes__securityofficer () Int)
+(declare-fun privtypes__useronly () Int)
+(declare-fun shutdown () Int)
+(declare-fun statust__base__first () Int)
+(declare-fun statust__base__last () Int)
+(declare-fun statust__first () Int)
+(declare-fun statust__last () Int)
+(declare-fun statust__size () Int)
+(declare-fun waitingendenrol () Int)
+(declare-fun waitingenrol () Int)
+(declare-fun waitingfinishadminop () Int)
+(declare-fun waitingremoveadmintokenfail () Int)
+(declare-fun waitingstartadminop () Int)
+(declare-fun admintoken__state () Int)
+(declare-fun admintoken__state__1 () Int)
+(declare-fun init.admintoken__state__1 () Int)
+(declare-fun admintoken__state__2 () Int)
+(declare-fun init.admintoken__state__2 () Int)
+(declare-fun admintoken__state__3 () Int)
+(declare-fun init.admintoken__state__3 () Int)
+(declare-fun init.admintoken__state () Int)
+(declare-fun clock__currenttime () Int)
+(declare-fun init.clock__currenttime () Int)
+(declare-fun door__state () Int)
+(declare-fun door__state__3 () Int)
+(declare-fun init.door__state__3 () Int)
+(declare-fun init.door__state () Int)
+(declare-fun latch__state () Int)
+(declare-fun latch__state__3 () Int)
+(declare-fun init.latch__state__3 () Int)
+(declare-fun init.latch__state () Int)
+(declare-fun state () Int)
+(declare-fun init.state () Int)
+(declare-fun |status'| () Int)
+(declare-fun status__1 () Int)
+(declare-fun init.status__1 () Int)
+(declare-fun status__2 () Int)
+(declare-fun init.status__2 () Int)
+(declare-fun status__3 () Int)
+(declare-fun init.status__3 () Int)
+(declare-fun init.status () Int)
+(declare-fun theadmin () Int)
+(declare-fun theadmin__1 () Int)
+(declare-fun init.theadmin__1 () Int)
+(declare-fun theadmin__3 () Int)
+(declare-fun init.theadmin__3 () Int)
+(declare-fun init.theadmin () Int)
+(declare-fun admin__opandnullt__pos (Int) Int)
+(declare-fun admin__opandnullt__pred (Int) Int)
+(declare-fun admin__opandnullt__succ (Int) Int)
+(declare-fun admin__opandnullt__val (Int) Int)
+(declare-fun admin__prf_rolepresent (Int) Int)
+(declare-fun admin__thecurrentop (Int) Int)
+(declare-fun admintoken__theauthcertrole (Int) Int)
+(declare-fun alarmtypes__statust__pos (Int) Int)
+(declare-fun alarmtypes__statust__pred (Int) Int)
+(declare-fun alarmtypes__statust__succ (Int) Int)
+(declare-fun alarmtypes__statust__val (Int) Int)
+(declare-fun bit__and (Int Int) Int)
+(declare-fun bit__not (Int Int) Int)
+(declare-fun bit__or (Int Int) Int)
+(declare-fun bit__xor (Int Int) Int)
+(declare-fun character__pos (Int) Int)
+(declare-fun character__val (Int) Int)
+(declare-fun clock__thecurrenttime (Int) Int)
+(declare-fun door__prf_alarmtimeout (Int) Int)
+(declare-fun door__t__pos (Int) Int)
+(declare-fun door__t__pred (Int) Int)
+(declare-fun door__t__succ (Int) Int)
+(declare-fun door__t__val (Int) Int)
+(declare-fun door__thecurrentdoor (Int) Int)
+(declare-fun door__thedooralarm (Int) Int)
+(declare-fun integer__pred (Int) Int)
+(declare-fun integer__succ (Int) Int)
+(declare-fun privtypes__privileget__pos (Int) Int)
+(declare-fun privtypes__privileget__pred (Int) Int)
+(declare-fun privtypes__privileget__succ (Int) Int)
+(declare-fun privtypes__privileget__val (Int) Int)
+(declare-fun round__ (Int) Int)
+(declare-fun statust__pos (Int) Int)
+(declare-fun statust__pred (Int) Int)
+(declare-fun statust__succ (Int) Int)
+(declare-fun statust__val (Int) Int)
+(declare-fun i.div (Int Int) Int)
+(declare-fun i.mod (Int Int) Int)
+(declare-fun i.mult (Int Int) Int)
+(declare-fun i.exp (Int Int) Int)
+(declare-fun tm.true () Int)
+(declare-fun tm.false () Int)
+(declare-fun tm.not (Int) Int)
+(declare-fun tm.and (Int Int) Int)
+(declare-fun tm.or (Int Int) Int)
+(declare-fun tm.iff (Int Int) Int)
+(declare-fun tm.eq (Int Int) Int)
+(declare-fun tm.ne (Int Int) Int)
+(declare-fun tm.lt (Int Int) Int)
+(declare-fun tm.le (Int Int) Int)
+(declare-fun tuple.2 (Int Int) Int)
+(declare-fun a.store (Int Int Int) Int)
+(declare-fun a.select (Int Int) Int)
+(declare-fun a.mk_const_array (Int) Int)
+(declare-fun a.default_array () Int)
+(declare-fun r.default_record () Int)
+(declare-fun admin__isdoingop (Int) Bool)
+(declare-fun admin__ispresent (Int) Bool)
+(declare-fun admin__opandnullt__LE (Int Int) Bool)
+(declare-fun admin__opandnullt__LT (Int Int) Bool)
+(declare-fun admintoken__prf_authcertvalid (Int) Bool)
+(declare-fun admintoken__prf_isgood (Int) Bool)
+(declare-fun alarmtypes__statust__LE (Int Int) Bool)
+(declare-fun alarmtypes__statust__LT (Int Int) Bool)
+(declare-fun clock__greaterthanorequal (Int Int) Bool)
+(declare-fun currentadminactivitypossible (Int Int) Bool)
+(declare-fun door__t__LE (Int Int) Bool)
+(declare-fun door__t__LT (Int Int) Bool)
+(declare-fun enclave__currentadminactivitypossible (Int Int) Bool)
+(declare-fun enclave__enrolmentisinprogress (Int) Bool)
+(declare-fun enrolmentisinprogress (Int) Bool)
+(declare-fun latch__islocked (Int) Bool)
+(declare-fun prf_statusisenclavequiescent (Int) Bool)
+(declare-fun prf_statusisgotadmintoken (Int) Bool)
+(declare-fun prf_statusisshutdown (Int) Bool)
+(declare-fun prf_statusiswaitingfinishadminop (Int) Bool)
+(declare-fun prf_statusiswaitingremoveadmintokenfail (Int) Bool)
+(declare-fun prf_statusiswaitingstartadminop (Int) Bool)
+(declare-fun privtypes__privileget__LE (Int Int) Bool)
+(declare-fun privtypes__privileget__LT (Int Int) Bool)
+(declare-fun statust__LE (Int Int) Bool)
+(declare-fun statust__LT (Int Int) Bool)
+(assert (= (and (latch__islocked latch__state) (and (= (door__thecurrentdoor door__state) door__open) (clock__greaterthanorequal (clock__thecurrenttime clock__currenttime) (door__prf_alarmtimeout door__state)))) (= (door__thedooralarm door__state) alarmtypes__alarming)))
+(assert (=> (not (admin__ispresent theadmin)) (not (admin__isdoingop theadmin))))
+(assert (=> (or (= |status'| waitingstartadminop) (= |status'| waitingfinishadminop)) (and (admin__ispresent theadmin) (admin__isdoingop theadmin))))
+(assert (=> (and (admin__isdoingop theadmin) (= (admin__thecurrentop theadmin) admin__shutdownop)) (= |status'| waitingstartadminop)))
+(assert (=> (= (admin__prf_rolepresent theadmin) privtypes__guard) (and (admintoken__prf_isgood admintoken__state) (and (admintoken__prf_authcertvalid admintoken__state) (= (admintoken__theauthcertrole admintoken__state) privtypes__guard)))))
+(assert (=> (and (admin__isdoingop theadmin) (= (admin__thecurrentop theadmin) admin__overridelock)) (= (admin__prf_rolepresent theadmin) privtypes__guard)))
+(assert (let ((?v_0 (admin__isdoingop theadmin))) (=> (= (admin__prf_rolepresent theadmin) privtypes__guard) (or (and ?v_0 (= (admin__thecurrentop theadmin) admin__overridelock)) (not ?v_0)))))
+(assert (or (= |status'| waitingstartadminop) (= |status'| waitingfinishadminop)))
+(assert (let ((?v_1 (admin__isdoingop theadmin)) (?v_0 (= |status'| waitingstartadminop)) (?v_2 (admin__thecurrentop theadmin)) (?v_3 (= (admin__prf_rolepresent theadmin) privtypes__guard))) (let ((?v_4 (and ?v_1 (= ?v_2 admin__overridelock)))) (not (and (or ?v_0 (= |status'| waitingfinishadminop)) (=> (and ?v_1 (= ?v_2 admin__shutdownop)) ?v_0) (admin__ispresent theadmin) ?v_1 (= (and (latch__islocked latch__state) (and (= (door__thecurrentdoor door__state) door__open) (clock__greaterthanorequal (clock__thecurrenttime clock__currenttime) (door__prf_alarmtimeout door__state)))) (= (door__thedooralarm door__state) alarmtypes__alarming)) (=> ?v_3 (and (admintoken__prf_isgood admintoken__state) (and (admintoken__prf_authcertvalid admintoken__state) (= (admintoken__theauthcertrole admintoken__state) privtypes__guard)))) (=> ?v_4 ?v_3) (=> ?v_3 (or ?v_4 (not ?v_1))))))))
+(check-sat)
+(exit)