diff options
| -rw-r--r-- | src/proof/sat_proof.h | 4 | ||||
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 18 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/simple_unsat_cores.smt2 | 10 |
4 files changed, 22 insertions, 13 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 5691d1bd2..36de6278a 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -29,6 +29,7 @@ #include <vector> #include "context/cdhashmap.h" +#include "context/cdmaybe.h" #include "expr/expr.h" #include "proof/clause_id.h" #include "proof/proof_manager.h" @@ -349,8 +350,7 @@ class TSatProof { IdCRefMap d_temp_idClause; // unit conflict - ClauseId d_unitConflictId; - bool d_storedUnitConflict; + context::CDMaybe<ClauseId> d_unitConflictId; ClauseId d_trueLit; ClauseId d_falseLit; diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index eb4e04d13..6cb10450a 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -218,8 +218,7 @@ TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context, d_nullId(-2), d_temp_clauseId(), d_temp_idClause(), - d_unitConflictId(), - d_storedUnitConflict(false), + d_unitConflictId(context), d_trueLit(ClauseIdUndef), d_falseLit(ClauseIdUndef), d_name(name), @@ -867,12 +866,11 @@ template <class Solver> ClauseId TSatProof<Solver>::storeUnitConflict( typename Solver::TLit conflict_lit, ClauseKind kind) { Debug("cores") << "STORE UNIT CONFLICT" << std::endl; - Assert(!d_storedUnitConflict); - d_unitConflictId = registerUnitClause(conflict_lit, kind); - d_storedUnitConflict = true; - Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId + Assert(!d_unitConflictId.isSet()); + d_unitConflictId.set(registerUnitClause(conflict_lit, kind)); + Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId.get() << "\n"; - return d_unitConflictId; + return d_unitConflictId.get(); } template <class Solver> @@ -881,8 +879,8 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { Assert(conflict_ref != Solver::TCRef_Undef); ClauseId conflict_id; if (conflict_ref == Solver::TCRef_Lazy) { - Assert(d_storedUnitConflict); - conflict_id = d_unitConflictId; + Assert(d_unitConflictId.isSet()); + conflict_id = d_unitConflictId.get(); ResChain<Solver>* res = new ResChain<Solver>(conflict_id); typename Solver::TLit lit = d_idUnit[conflict_id]; @@ -892,7 +890,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { return; } else { - Assert(!d_storedUnitConflict); + Assert(!d_unitConflictId.isSet()); conflict_id = registerClause(conflict_ref, LEARNT); // FIXME } diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 262132779..197f81d63 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -48,7 +48,8 @@ BUG_TESTS = \ inc-define.smt2 \ bug765.smt2 \ bug691.smt2 \ - bug694-Unapply1.scala-0.smt2 + bug694-Unapply1.scala-0.smt2 \ + simple_unsat_cores.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/simple_unsat_cores.smt2 b/test/regress/regress0/push-pop/simple_unsat_cores.smt2 new file mode 100644 index 000000000..e85a546d8 --- /dev/null +++ b/test/regress/regress0/push-pop/simple_unsat_cores.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: unsat +(set-logic UF) +(push 1) +(assert false) +(check-sat) +(pop 1) +(assert false) +(check-sat) |