diff options
-rwxr-xr-x[-rw-r--r--] | contrib/run-script-smtcomp2017-application | 10 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 4 | ||||
-rw-r--r-- | src/proof/sat_proof_implementation.h | 18 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 7 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/bug639.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/simple_unsat_cores.smt2 | 10 |
9 files changed, 39 insertions, 22 deletions
diff --git a/contrib/run-script-smtcomp2017-application b/contrib/run-script-smtcomp2017-application index 528a5deab..ddcc1f0c6 100644..100755 --- a/contrib/run-script-smtcomp2017-application +++ b/contrib/run-script-smtcomp2017-application @@ -2,13 +2,19 @@ cvc4=./cvc4-application -read line +line="" +while [[ -z "$line" ]]; do + read line +done if [ "$line" != '(set-option :print-success true)' ]; then echo 'ERROR: first line supposed to be set-option :print-success, but got: "'"$line"'"' >&2 exit 1 fi echo success -read line +line="" +while [[ -z "$line" ]]; do + read line +done logic=$(expr "$line" : ' *(set-logic *\([A-Z_]*\) *) *$') if [ -z "$logic" ]; then echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 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/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 2c7418a77..e712a51b6 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1704,7 +1704,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) // so we take its representative to be safe. a = d_equalityEngine.getRepresentative(a); Assert(d_equalityEngine.getRepresentative(b) == a); - Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: " << a << "," << b << ")\n"; + Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: (" << a << ", " << b << ")\n"; if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) { checkRIntro1(a, b); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 574702368..48da4c681 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -309,7 +309,6 @@ class TheoryArrays : public Theory { Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { if (t1.getType().isArray()) { - d_arrays.mergeArrays(t1, t2); if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { return true; } @@ -334,7 +333,11 @@ class TheoryArrays : public Theory { void eqNotifyNewClass(TNode t) { } void eqNotifyPreMerge(TNode t1, TNode t2) { } - void eqNotifyPostMerge(TNode t1, TNode t2) { } + void eqNotifyPostMerge(TNode t1, TNode t2) { + if (t1.getType().isArray()) { + d_arrays.mergeArrays(t1, t2); + } + } void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } }; diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 98be91454..9a16f68ca 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -179,6 +179,7 @@ BUG_TESTS = \ bug596.cvc \ bug596b.cvc \ bug605.cvc \ + bug639.smt2 \ bt-test-00.smt2 \ bt-test-01.smt2 #bug590.smt2 @@ -189,9 +190,7 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) # we have a minimized version still getting tested # bug639 -- still fails, reopened bug DISABLED_TESTS = \ - bug512.smt2 \ - bug639.smt2 - + bug512.smt2 EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ diff --git a/test/regress/regress0/bug639.smt2 b/test/regress/regress0/bug639.smt2 index 9e31e75cd..907568d73 100644 --- a/test/regress/regress0/bug639.smt2 +++ b/test/regress/regress0/bug639.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_AUFLIA) +(set-logic QF_AUFNIA) (set-info :status unsat) (declare-fun i () Int) (declare-fun j () Int) 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) |