summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp34
-rw-r--r--src/prop/bvminisat/bvminisat.h9
-rw-r--r--src/prop/bvminisat/core/Solver.cc403
-rw-r--r--src/prop/bvminisat/core/Solver.h50
-rw-r--r--src/prop/bvminisat/core/SolverTypes.h49
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.cc55
-rw-r--r--src/prop/cadical.cpp1
-rw-r--r--src/prop/cnf_stream.cpp60
-rw-r--r--src/prop/cnf_stream.h14
-rw-r--r--src/prop/cryptominisat.cpp44
-rw-r--r--src/prop/cryptominisat.h3
-rw-r--r--src/prop/kissat.cpp1
-rw-r--r--src/prop/minisat/core/Solver.cc313
-rw-r--r--src/prop/minisat/core/Solver.h6
-rw-r--r--src/prop/minisat/core/SolverTypes.h64
-rw-r--r--src/prop/minisat/minisat.cpp2
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc96
-rw-r--r--src/prop/prop_engine.cpp23
-rw-r--r--src/prop/prop_engine.h6
-rw-r--r--src/prop/sat_solver.h12
-rw-r--r--src/prop/theory_proxy.cpp20
21 files changed, 541 insertions, 724 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index c1aac33be..0b531c498 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -18,7 +18,6 @@
#include "prop/bvminisat/simp/SimpSolver.h"
#include "proof/clause_id.h"
-#include "proof/sat_proof.h"
#include "util/statistics_registry.h"
namespace CVC4 {
@@ -66,7 +65,6 @@ ClauseId BVMinisatSatSolver::addClause(SatClause& clause,
// }
ClauseId clause_id = ClauseIdError;
d_minisat->addClause(minisat_clause, clause_id);
- THEORY_PROOF(Assert(clause_id != ClauseIdError););
return clause_id;
}
@@ -76,14 +74,14 @@ SatValue BVMinisatSatSolver::propagate() {
void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
- markUnremovable(lit);
+ markUnremovable(lit);
}
void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) {
std::vector<BVMinisat::Lit> minisat_explanation;
d_minisat->explain(toMinisatLit(lit), minisat_explanation);
for (unsigned i = 0; i < minisat_explanation.size(); ++i) {
- explanation.push_back(toSatLiteral(minisat_explanation[i]));
+ explanation.push_back(toSatLiteral(minisat_explanation[i]));
}
}
@@ -104,12 +102,6 @@ void BVMinisatSatSolver::popAssumption() {
d_minisat->popAssumption();
}
-void BVMinisatSatSolver::setResolutionProofLog(
- proof::ResolutionBitVectorProof* bvp)
-{
- d_minisat->setProofLog( bvp );
-}
-
SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
return d_minisat->newVar(true, true, !canErase);
}
@@ -148,9 +140,7 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
return result;
}
-bool BVMinisatSatSolver::ok() const {
- return d_minisat->okay();
-}
+bool BVMinisatSatSolver::ok() const { return d_minisat->okay(); }
void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
// TODO add assertion to check the call was after an unsat call
@@ -160,11 +150,11 @@ void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
}
SatValue BVMinisatSatSolver::value(SatLiteral l){
- return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
+ return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
}
SatValue BVMinisatSatSolver::modelValue(SatLiteral l){
- return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
+ return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
}
void BVMinisatSatSolver::unregisterVar(SatLiteral lit) {
@@ -309,17 +299,3 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
} /* namespace CVC4::prop */
} /* namespace CVC4 */
-
-namespace CVC4 {
-template<>
-prop::SatLiteral toSatLiteral< BVMinisat::Solver>(BVMinisat::Solver::TLit lit) {
- return prop::BVMinisatSatSolver::toSatLiteral(lit);
-}
-
-template<>
-void toSatClause< BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl,
- prop::SatClause& sat_cl) {
- prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl);
-}
-
-}
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 01a0a518e..f93dc8048 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -21,8 +21,6 @@
#include <memory>
#include "context/cdo.h"
-#include "proof/clause_id.h"
-#include "proof/resolution_bitvector_proof.h"
#include "prop/bv_sat_solver_notify.h"
#include "prop/bvminisat/simp/SimpSolver.h"
#include "prop/sat_solver.h"
@@ -57,8 +55,8 @@ class BVMinisatSatSolver : public BVSatSolverInterface,
}
};
- std::unique_ptr<BVMinisat::SimpSolver> d_minisat;
- std::unique_ptr<MinisatNotify> d_minisatNotify;
+ std::unique_ptr<BVMinisat::SimpSolver> d_minisat;
+ std::unique_ptr<MinisatNotify> d_minisatNotify;
unsigned d_assertionsCount;
context::CDO<unsigned> d_assertionsRealCount;
@@ -79,6 +77,7 @@ public:
ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
{
Unreachable() << "Minisat does not support native XOR reasoning";
+ return ClauseIdError;
}
SatValue propagate() override;
@@ -123,8 +122,6 @@ public:
void popAssumption() override;
- void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) override;
-
private:
/* Disable the default constructor. */
BVMinisatSatSolver() = delete;
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 84ab62fd8..f7ba14acd 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -29,11 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "base/output.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
-#include "proof/clause_id.h"
-#include "proof/proof_manager.h"
-#include "proof/resolution_bitvector_proof.h"
-#include "proof/sat_proof.h"
-#include "proof/sat_proof_implementation.h"
#include "prop/bvminisat/mtl/Sort.h"
#include "theory/interrupted.h"
#include "util/utility.h"
@@ -170,8 +165,7 @@ Solver::Solver(CVC4::context::Context* context)
,
conflict_budget(-1),
propagation_budget(-1),
- asynch_interrupt(false),
- d_bvp(NULL)
+ asynch_interrupt(false)
{
// Create the constant variables
varTrue = newVar(true, false);
@@ -220,7 +214,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
if (decisionLevel() > 0) {
cancelUntil(0);
}
-
+
if (!ok) {
id = ClauseIdUndef;
return false;
@@ -231,7 +225,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
sort(ps);
Lit p; int i, j;
int falseLiteralsCount = 0;
-
+
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
// tautologies are ignored
if (value(ps[i]) == l_True || ps[i] == ~p) {
@@ -245,82 +239,30 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
}
if (value(ps[i]) == l_False) {
- if (!THEORY_PROOF_ON())
- continue;
- ++falseLiteralsCount;
+ continue;
}
ps[j++] = p = ps[i];
}
-
+
ps.shrink(i - j);
clause_added = true;
- Assert(falseLiteralsCount == 0 || THEORY_PROOF_ON());
-
if(falseLiteralsCount == 0) {
if (ps.size() == 0) {
- Assert(!THEORY_PROOF_ON());
return ok = false;
}
else if (ps.size() == 1){
- if(d_bvp){ id = d_bvp->getSatProof()->registerUnitClause(ps[0], INPUT);}
uncheckedEnqueue(ps[0]);
CRef confl_ref = propagate();
ok = (confl_ref == CRef_Undef);
- if(d_bvp){ if (!ok) d_bvp->getSatProof()->finalizeProof(confl_ref); }
return ok;
} else {
CRef cr = ca.alloc(ps, false);
clauses.push(cr);
attachClause(cr);
- if(d_bvp){ id = d_bvp->getSatProof()->registerClause(cr, INPUT);}
- }
- return ok;
- }
-
- if (falseLiteralsCount != 0 && THEORY_PROOF_ON()) {
- // we are in a conflicting state
- if (ps.size() == falseLiteralsCount && falseLiteralsCount == 1) {
- if(d_bvp){ id = d_bvp->getSatProof()->storeUnitConflict(ps[0], INPUT); }
- if(d_bvp){ d_bvp->getSatProof()->finalizeProof(CVC4::BVMinisat::CRef_Lazy); }
- return ok = false;
- }
-
- assign_lt lt(*this);
- sort(ps, lt);
-
- CRef cr = ca.alloc(ps, false);
- clauses.push(cr);
- attachClause(cr);
-
- if(d_bvp){id = d_bvp->getSatProof()->registerClause(cr, INPUT);}
-
- if(ps.size() == falseLiteralsCount) {
- if(d_bvp){ d_bvp->getSatProof()->finalizeProof(cr); }
- return ok = false;
- }
-
- // Check if it propagates
- if (ps.size() == falseLiteralsCount + 1) {
- Clause& cl = ca[cr];
-
- Assert(value(cl[0]) == l_Undef);
- uncheckedEnqueue(cl[0], cr);
- Assert(cl.size() > 1);
- CRef confl = propagate();
- ok = (confl == CRef_Undef);
- if(!ok) {
- if(d_bvp){
- if(ca[confl].size() == 1) {
- id = d_bvp->getSatProof()->storeUnitConflict(ca[confl][0], LEARNT);
- d_bvp->getSatProof()->finalizeProof(CVC4::BVMinisat::CRef_Lazy);
- } else {
- d_bvp->getSatProof()->finalizeProof(confl);
- }
- }
- }
}
+ return ok;
}
return ok;
}
@@ -338,9 +280,6 @@ void Solver::attachClause(CRef cr) {
void Solver::detachClause(CRef cr, bool strict) {
const Clause& clause = ca[cr];
- if (d_bvp)
- {
- d_bvp->getSatProof()->markDeleted(cr); }
assert(clause.size() > 1);
@@ -425,23 +364,24 @@ Lit Solver::pickBranchLit()
return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
}
-
/*_________________________________________________________________________________________________
|
-| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
-|
+| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) ->
+[void]
+|
| Description:
| Analyze conflict and produce a reason clause.
-|
+|
| Pre-conditions:
| * 'out_learnt' is assumed to be cleared.
| * Current decision level must be greater than root level.
-|
+|
| Post-conditions:
| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
-| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
-| rest of literals. There may be others from the same level though.
-|
+| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision
+level of the | rest of literals. There may be others from the same level
+though.
+|
|________________________________________________________________________________________________@*/
void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip)
{
@@ -454,8 +394,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
int index = trail.size() - 1;
bool done = false;
-
- if(d_bvp){ d_bvp->getSatProof()->startResChain(confl); }
do{
assert(confl != CRef_Undef); // (otherwise should be UIP)
@@ -477,13 +415,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
out_learnt.push(q);
}
- if (level(var(q)) == 0)
- {
- if (d_bvp)
- {
- d_bvp->getSatProof()->resolveOutUnit(q);
- }
- }
}
// Select next clause to look at:
@@ -493,10 +424,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
seen[var(p)] = 0;
pathC--;
- if ( pathC > 0 && confl != CRef_Undef ) {
- if(d_bvp){ d_bvp->getSatProof()->addResolutionStep(p, confl, sign(p));}
- }
-
switch (uip) {
case UIP_FIRST:
done = pathC == 0;
@@ -536,13 +463,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
// Literal is not redundant
out_learnt[j++] = out_learnt[i1];
}
- else
- {
- if (d_bvp)
- {
- d_bvp->getSatProof()->storeLitRedundant(out_learnt[i1]);
- }
- }
}
}
}else if (ccmin_mode == 1){
@@ -640,10 +560,10 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
return true;
}
-/**
+/**
* Specialized analyzeFinal procedure where we test the consistency
* of the assumptions before backtracking bellow the assumption level.
- *
+ *
* @param p the original uip (may be unit)
* @param confl_clause the conflict clause
* @param out_conflict the conflict in terms of assumptions we are building
@@ -653,14 +573,14 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
assert (decisionLevel() == assumptions.size());
assert (level(var(p)) == assumptions.size());
- out_conflict.clear();
-
+ out_conflict.clear();
+
Clause& cl = ca[confl_clause];
for (int i = 0; i < cl.size(); ++i) {
seen[var(cl[i])] = 1;
}
- int end = options::proof() ? 0 : trail_lim[0];
+ int end = trail_lim[0];
for (int i = trail.size() - 1; i >= end; i--) {
Var x = var(trail[i]);
if (seen[x]) {
@@ -670,44 +590,31 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
if (marker[x] == 2) {
assert (level(x) > 0);
out_conflict.push(~trail[i]);
- } else {
- if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); }
}
- } else {
- if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~p);}
}
} else {
Clause& clause = ca[reason(x)];
- if(d_bvp){d_bvp->getSatProof()->addResolutionStep(trail[i],reason(x), sign(trail[i]));}
for (int j = 1; j < clause.size(); j++)
{
if (level(var(clause[j])) > 0) seen[var(clause[j])] = 1;
- if(d_bvp){
- if (level(var(clause[j])) == 0)
- {
- d_bvp->getSatProof()->resolveOutUnit(clause[j]);
- seen[var(clause[j])] =
- 0; // we don't need to resolve it out again
- }
- }
}
}
seen[x] = 0;
}
- assert (seen[x] == 0);
+ assert(seen[x] == 0);
}
- assert (out_conflict.size());
+ assert(out_conflict.size());
}
/*_________________________________________________________________________________________________
|
| analyzeFinal : (p : Lit) -> [void]
-|
+|
| Description:
-| Specialized analysis procedure to express the final conflict in terms of assumptions.
-| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
-| stores the result in 'out_conflict'.
+| Specialized analysis procedure to express the final conflict in terms of
+assumptions. | Calculates the (possibly empty) set of assumptions that led to
+the assignment of 'p', and | stores the result in 'out_conflict'.
|________________________________________________________________________________________________@*/
void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
{
@@ -716,22 +623,14 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
out_conflict.push(p);
}
- if(d_bvp){
- if (level(var(p)) == 0 && d_bvp->isAssumptionConflict()) {
- Assert(marker[var(p)] == 2);
- if (reason(var(p)) == CRef_Undef) {
- d_bvp->startBVConflict(p);
- }
- }
- }
-
- if (decisionLevel() == 0 && !options::proof()) {
+ if (decisionLevel() == 0)
+ {
return;
}
seen[var(p)] = 1;
- int end = options::proof() ? 0 : trail_lim[0];
-
+ int end = trail_lim[0];
+
for (int i = trail.size()-1; i >= end; i--){
Var x = var(trail[i]);
if (seen[x]) {
@@ -744,26 +643,12 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
}
} else {
Clause& clause = ca[reason(x)];
- if(d_bvp){
- if (d_bvp->isAssumptionConflict() &&
- trail[i] == p) {
- d_bvp->startBVConflict(reason(x));
- } else {
- d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i]));
- }
- }
for (int j = 1; j < clause.size(); j++)
{
if (level(var(clause[j])) > 0)
{
seen[var(clause[j])] = 1;
}
- if(d_bvp){
- if (level(var(clause[j])) == 0)
- {
- d_bvp->getSatProof()->resolveOutUnit(clause[j]);
- }
- }
}
}
seen[x] = 0;
@@ -805,10 +690,9 @@ lbool Solver::propagateAssumptions() {
lbool Solver::assertAssumption(Lit p, bool propagate) {
// TODO need to somehow mark the assumption as unit in the current context?
// it's not always unit though, but this would be useful for debugging
-
+
// assert(marker[var(p)] == 1);
-
if (decisionLevel() > assumptions.size()) {
cancelUntil(assumptions.size());
}
@@ -829,9 +713,9 @@ lbool Solver::assertAssumption(Lit p, bool propagate) {
// run the propagation
if (propagate) {
only_bcp = true;
- ccmin_mode = 0;
+ ccmin_mode = 0;
lbool result = search(-1);
- return result;
+ return result;
} else {
return l_True;
}
@@ -841,18 +725,16 @@ void Solver::addMarkerLiteral(Var var) {
// make sure it wasn't already marked
Assert(marker[var] == 0);
marker[var] = 1;
- if(d_bvp){d_bvp->getSatProof()->registerAssumption(var);}
}
-
/*_________________________________________________________________________________________________
|
| propagate : [void] -> [Clause*]
-|
+|
| Description:
-| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
-| otherwise CRef_Undef.
-|
+| Propagates all enqueued facts. If a conflict arises, the conflicting clause
+is returned, | otherwise CRef_Undef.
+|
| Post-conditions:
| * the propagation queue is empty, even if there was a conflict.
|________________________________________________________________________________________________@*/
@@ -920,20 +802,24 @@ CRef Solver::propagate()
return confl;
}
-
/*_________________________________________________________________________________________________
|
| reduceDB : () -> [void]
-|
+|
| Description:
-| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
-| clauses are clauses that are reason to some assignment. Binary clauses are never removed.
+| Remove half of the learnt clauses, minus the clauses locked by the current
+assignment. Locked | clauses are clauses that are reason to some assignment.
+Binary clauses are never removed.
|________________________________________________________________________________________________@*/
-struct reduceDB_lt {
- ClauseAllocator& ca;
- reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
- bool operator () (CRef x, CRef y) {
- return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
+struct reduceDB_lt
+{
+ ClauseAllocator& ca;
+ reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
+ bool operator()(CRef x, CRef y)
+ {
+ return ca[x].size() > 2
+ && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity());
+ }
};
void Solver::reduceDB()
{
@@ -963,14 +849,6 @@ void Solver::removeSatisfied(vec<CRef>& cs)
Clause& clause = ca[cs[i]];
if (satisfied(clause))
{
- if (locked(clause))
- {
- // store a resolution of the literal clause propagated
- if (d_bvp)
- {
- d_bvp->getSatProof()->storeUnitResolution(clause[0]);
- }
- }
removeClause(cs[i]);
}
else
@@ -989,14 +867,14 @@ void Solver::rebuildOrderHeap()
order_heap.build(vs);
}
-
/*_________________________________________________________________________________________________
|
| simplify : [void] -> [bool]
-|
+|
| Description:
-| Simplify the clause database according to the current top-level assigment. Currently, the only
-| thing done here is the removal of satisfied clauses, but more things can be put here.
+| Simplify the clause database according to the current top-level assigment.
+Currently, the only | thing done here is the removal of satisfied clauses,
+but more things can be put here.
|________________________________________________________________________________________________@*/
bool Solver::simplify()
{
@@ -1021,19 +899,19 @@ bool Solver::simplify()
return true;
}
-
/*_________________________________________________________________________________________________
|
| search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
-|
+|
| Description:
-| Search for a model the specified number of conflicts.
+| Search for a model the specified number of conflicts.
| NOTE! Use negative value for 'nof_conflicts' indicate infinity.
-|
+|
| Output:
-| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
-| all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
-| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
+| 'l_True' if a partial assigment that is consistent with respect to the
+clauseset is found. If | all variables are decision variables, this means
+that the clause set is satisfiable. 'l_False' | if the clause set is
+unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
|________________________________________________________________________________________________@*/
lbool Solver::search(int nof_conflicts, UIP uip)
{
@@ -1051,7 +929,6 @@ lbool Solver::search(int nof_conflicts, UIP uip)
if (decisionLevel() == 0) {
// can this happen for bv?
- if(d_bvp){ d_bvp->getSatProof()->finalizeProof(confl);}
return l_False;
}
@@ -1067,59 +944,34 @@ lbool Solver::search(int nof_conflicts, UIP uip)
learnts.push(cr);
attachClause(cr);
claBumpActivity(ca[cr]);
- if(d_bvp){
- ClauseId id = d_bvp->getSatProof()->registerClause(cr, LEARNT);
- PSTATS(
- std::unordered_set<int> cl_levels;
- for (int i = 0; i < learnt_clause.size(); ++i) {
- cl_levels.insert(level(var(learnt_clause[i])));
- }
- if( d_bvp ){ d_bvp->getSatProof()->storeClauseGlue(id, cl_levels.size()); }
- )
- d_bvp->getSatProof()->endResChain(id);
- }
}
-
+
if (learnt_clause.size() == 1) {
// learning a unit clause
- if(d_bvp){ d_bvp->getSatProof()->endResChain(learnt_clause[0]);}
}
-
+
// if the uip was an assumption we are unsat
if (level(var(p)) <= assumptions.size()) {
for (int i = 0; i < learnt_clause.size(); ++i) {
- assert (level(var(learnt_clause[i])) <= decisionLevel());
+ assert(level(var(learnt_clause[i])) <= decisionLevel());
seen[var(learnt_clause[i])] = 1;
}
- // Starting new resolution chain for bit-vector proof
- if( d_bvp ){
- if (cr == CRef_Undef) {
- d_bvp->startBVConflict(learnt_clause[0]);
- }
- else {
- d_bvp->startBVConflict(cr);
- }
- }
analyzeFinal(p, conflict);
- if(d_bvp){ d_bvp->endBVConflict(conflict); }
Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl;
return l_False;
}
if (!CVC4::options::bvEagerExplanations()) {
- // check if uip leads to a conflict
+ // check if uip leads to a conflict
if (backtrack_level < assumptions.size()) {
cancelUntil(assumptions.size());
uncheckedEnqueue(p, cr);
-
+
CRef new_confl = propagate();
if (new_confl != CRef_Undef) {
// we have a conflict we now need to explain it
- // TODO: proof for analyzeFinal2
- if(d_bvp){ d_bvp->startBVConflict(new_confl); }
analyzeFinal2(p, new_confl, conflict);
- if(d_bvp){ d_bvp->endBVConflict(conflict); }
return l_False;
}
}
@@ -1127,8 +979,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
cancelUntil(backtrack_level);
uncheckedEnqueue(p, cr);
-
-
+
varDecayActivity();
claDecayActivity();
@@ -1138,10 +989,17 @@ lbool Solver::search(int nof_conflicts, UIP uip)
max_learnts *= learntsize_inc;
if (verbosity >= 1)
- printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
- (int)conflicts,
- (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
- (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
+ printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
+ (int)conflicts,
+ (int)dec_vars
+ - (trail_lim.size() == 0 ? trail.size()
+ : trail_lim[0]),
+ nClauses(),
+ (int)clauses_literals,
+ (int)max_learnts,
+ nLearnts(),
+ (double)learnts_literals / nLearnts(),
+ progressEstimate() * 100);
}
}else{
@@ -1152,9 +1010,9 @@ lbool Solver::search(int nof_conflicts, UIP uip)
withinBudget(ResourceManager::Resource::BvSatConflictsStep);
}
catch (const CVC4::theory::Interrupted& e) {
- // do some clean-up and rethrow
- cancelUntil(assumptions.size());
- throw e;
+ // do some clean-up and rethrow
+ cancelUntil(assumptions.size());
+ throw e;
}
if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
@@ -1192,10 +1050,8 @@ lbool Solver::search(int nof_conflicts, UIP uip)
newDecisionLevel();
}else if (value(p) == l_False){
marker[var(p)] = 2;
-
- if(d_bvp){ d_bvp->markAssumptionConflict(); }
+
analyzeFinal(~p, conflict);
- if(d_bvp){ d_bvp->endBVConflict(conflict); }
Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl;
return l_False;
}else{
@@ -1283,7 +1139,7 @@ lbool Solver::solve_()
conflict.clear();
ccmin_mode = 0;
-
+
if (!ok) return l_False;
solves++;
@@ -1324,31 +1180,20 @@ lbool Solver::solve_()
//=================================================================================================
// Bitvector propagations
-//
+//
void Solver::explain(Lit p, std::vector<Lit>& explanation) {
Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl;
// top level fact, no explanation necessary
if (level(var(p)) == 0) {
- if(d_bvp){
- // the only way a marker variable is
- if (reason(var(p)) == CRef_Undef) {
- d_bvp->startBVConflict(p);
- vec<Lit> confl;
- confl.push(p);
- d_bvp->endBVConflict(confl);
- return;
- }
- }
- if (!THEORY_PROOF_ON())
- return;
+ return;
}
-
+
seen[var(p)] = 1;
// if we are called at decisionLevel = 0 trail_lim is empty
- int bottom = options::proof() ? 0 : trail_lim[0];
+ int bottom = trail_lim[0];
for (int i = trail.size()-1; i >= bottom; i--){
Var x = var(trail[i]);
if (seen[x]) {
@@ -1358,21 +1203,12 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
explanation.push_back(trail[i]);
} else {
Assert(level(x) == 0);
- if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); }
}
-
} else {
Clause& clause = ca[reason(x)];
- if(d_bvp){
- if (p == trail[i]) {
- d_bvp->startBVConflict(reason(var(p)));
- } else {
- d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i]));
- }
- }
for (int j = 1; j < clause.size(); j++)
{
- if (level(var(clause[j])) > 0 || options::proof())
+ if (level(var(clause[j])) > 0)
{
seen[var(clause[j])] = 1;
}
@@ -1382,28 +1218,11 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
}
}
seen[var(p)] = 0;
-
- if(d_bvp){
- vec<Lit> conflict_clause;
- conflict_clause.push(p);
- for(unsigned i = 0; i < explanation.size(); ++i) {
- conflict_clause.push(~explanation[i]);
- }
- d_bvp->endBVConflict(conflict_clause);
- }
-}
-
-void Solver::setProofLog(proof::ResolutionBitVectorProof* bvp)
-{
- d_bvp = bvp;
- d_bvp->initSatProof(this);
- d_bvp->getSatProof()->registerTrueLit(mkLit(varTrue, false));
- d_bvp->getSatProof()->registerFalseLit(mkLit(varFalse, true));
}
//=================================================================================================
// Writing CNF to DIMACS:
-//
+//
// FIXME: this needs to be rewritten completely.
static Var mapVar(Var x, vec<Var>& map, Var& max)
@@ -1454,7 +1273,7 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
for (int i = 0; i < clauses.size(); i++)
if (!satisfied(ca[clauses[i]]))
cnt++;
-
+
for (int i = 0; i < clauses.size(); i++)
if (!satisfied(ca[clauses[i]])){
Clause& clause = ca[clauses[i]];
@@ -1494,8 +1313,7 @@ void Solver::relocAll(ClauseAllocator& to)
Lit p = mkLit(v, s);
// printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
vec<Watcher>& ws = watches[p];
- for (int j = 0; j < ws.size(); j++)
- ca.reloc(ws[j].cref, to, d_bvp ? d_bvp->getSatProof() : NULL);
+ for (int j = 0; j < ws.size(); j++) ca.reloc(ws[j].cref, to);
}
// All reasons:
@@ -1504,20 +1322,16 @@ void Solver::relocAll(ClauseAllocator& to)
Var v = var(trail[i]);
if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
- ca.reloc(vardata[v].reason, to, d_bvp ? d_bvp->getSatProof() : NULL);
+ ca.reloc(vardata[v].reason, to);
}
// All learnt:
//
- for (int i = 0; i < learnts.size(); i++)
- ca.reloc(learnts[i], to, d_bvp ? d_bvp->getSatProof() : NULL);
+ for (int i = 0; i < learnts.size(); i++) ca.reloc(learnts[i], to);
// All original:
//
- for (int i = 0; i < clauses.size(); i++)
- ca.reloc(clauses[i], to, d_bvp ? d_bvp->getSatProof() : NULL);
-
- if(d_bvp){ d_bvp->getSatProof()->finishUpdateCRef(); }
+ for (int i = 0; i < clauses.size(); i++) ca.reloc(clauses[i], to);
}
@@ -1525,33 +1339,28 @@ void Solver::garbageCollect()
{
// Initialize the next region to a size corresponding to the estimated utilization degree. This
// is not precise but should avoid some unnecessary reallocations for the new region:
- ClauseAllocator to(ca.size() - ca.wasted());
- Debug("bvminisat") << " BVMinisat::Garbage collection \n";
+ ClauseAllocator to(ca.size() - ca.wasted());
+ Debug("bvminisat") << " BVMinisat::Garbage collection \n";
relocAll(to);
if (verbosity >= 2)
- printf("| Garbage collection: %12d bytes => %12d bytes |\n",
- ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ printf(
+ "| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size() * ClauseAllocator::Unit_Size,
+ to.size() * ClauseAllocator::Unit_Size);
to.moveTo(ca);
}
-void ClauseAllocator::reloc(CRef& cr,
- ClauseAllocator& to,
- CVC4::TSatProof<Solver>* proof)
+void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to)
{
- CRef old = cr; // save the old reference
-
Clause& c = operator[](cr);
if (c.reloced()) { cr = c.relocation(); return; }
-
+
cr = to.alloc(c, c.learnt());
c.relocate(cr);
- if (proof)
- {
- proof->updateCRef(old, cr);
- }
-
- // Copy extra data-fields:
- // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
+
+ // Copy extra data-fields:
+ // (This could be cleaned-up. Generalize Clause-constructor to be applicable
+ // here instead?)
to[cr].mark(c.mark());
if (to[cr].learnt()) to[cr].activity() = c.activity();
else if (to[cr].has_extra()) to[cr].calcAbstraction();
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 7fad72d6d..f2721c88d 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -25,7 +25,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "context/context.h"
#include "proof/clause_id.h"
-#include "proof/sat_proof.h"
#include "prop/bvminisat/core/SolverTypes.h"
#include "prop/bvminisat/mtl/Alg.h"
#include "prop/bvminisat/mtl/Heap.h"
@@ -39,11 +38,6 @@ namespace BVMinisat {
class Solver;
}
-// TODO (aozdemir) replace this forward declaration with an include
-namespace proof {
-class ResolutionBitVectorProof;
-}
-
namespace BVMinisat {
/** Interface for minisat callbacks */
@@ -71,11 +65,10 @@ public:
//=================================================================================================
// Solver -- the main class:
class Solver {
- friend class CVC4::TSatProof< CVC4::BVMinisat::Solver>;
public:
typedef Var TVar;
typedef Lit TLit;
- typedef Clause TClause;
+ typedef Clause TClause;
typedef CRef TCRef;
typedef vec<Lit> TLitVec;
@@ -109,12 +102,17 @@ public:
Var trueVar() const { return varTrue; }
Var falseVar() const { return varFalse; }
-
- bool addClause (const vec<Lit>& ps, ClauseId& id); // Add a clause to the solver.
+ bool addClause(const vec<Lit>& ps,
+ ClauseId& id); // Add a clause to the solver.
bool addEmptyClause(); // Add the empty clause, making the solver contradictory.
- bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver.
- bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver.
- bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver.
+ bool addClause(Lit p, ClauseId& id); // Add a unit clause to the solver.
+ bool addClause(Lit p,
+ Lit q,
+ ClauseId& id); // Add a binary clause to the solver.
+ bool addClause(Lit p,
+ Lit q,
+ Lit r,
+ ClauseId& id); // Add a ternary clause to the solver.
bool addClause_( vec<Lit>& ps, ClauseId& id); // Add a clause to the solver without making superflous internal copy. Will
// change the passed vector 'ps'.
@@ -141,9 +139,9 @@ public:
void toDimacs (const char* file, Lit p);
void toDimacs (const char* file, Lit p, Lit q);
void toDimacs (const char* file, Lit p, Lit q, Lit r);
-
+
// Variable mode:
- //
+ //
void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
@@ -211,13 +209,12 @@ public:
void addMarkerLiteral(Var var);
- bool need_to_propagate; // true if we added new clauses, set to true in propagation
+ bool need_to_propagate; // true if we added new clauses, set to true in
+ // propagation
bool only_bcp; // solving mode in which only boolean constraint propagation is done
void setOnlyBCP (bool val) { only_bcp = val;}
void explain(Lit l, std::vector<Lit>& explanation);
- void setProofLog(CVC4::proof::ResolutionBitVectorProof* bvp);
-
protected:
// has a clause been added
@@ -293,9 +290,6 @@ public:
int64_t conflict_budget; // -1 means no budget.
int64_t propagation_budget; // -1 means no budget.
bool asynch_interrupt;
-
- //proof log
- CVC4::proof::ResolutionBitVectorProof* d_bvp;
// Main internal methods:
//
@@ -458,13 +452,15 @@ inline int Solver::nLearnts () const { return learnts.size(); }
inline int Solver::nVars () const { return vardata.size(); }
inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
-inline void Solver::setDecisionVar(Var v, bool b)
-{
- if ( b && !decision[v]) dec_vars++;
- else if (!b && decision[v]) dec_vars--;
+inline void Solver::setDecisionVar(Var v, bool b)
+{
+ if (b && !decision[v])
+ dec_vars++;
+ else if (!b && decision[v])
+ dec_vars--;
- decision[v] = b;
- insertVarOrder(v);
+ decision[v] = b;
+ insertVarOrder(v);
}
inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index 302db104f..cf9ce7e15 100644
--- a/src/prop/bvminisat/core/SolverTypes.h
+++ b/src/prop/bvminisat/core/SolverTypes.h
@@ -86,15 +86,14 @@ struct LitHashFunction {
const Lit lit_Undef = { -2 }; // }- Useful special constants.
const Lit lit_Error = { -1 }; // }
-
//=================================================================================================
// Lifted booleans:
//
-// NOTE: this implementation is optimized for the case when comparisons between values are mostly
-// between one variable and one constant. Some care had to be taken to make sure that gcc
-// does enough constant propagation to produce sensible code, and this appears to be somewhat
-// fragile unfortunately.
-
+// NOTE: this implementation is optimized for the case when comparisons between
+// values are mostly
+// between one variable and one constant. Some care had to be taken to
+// make sure that gcc does enough constant propagation to produce sensible
+// code, and this appears to be somewhat fragile unfortunately.
#ifndef l_True
#define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
@@ -121,10 +120,12 @@ public:
bool operator != (lbool b) const { return !(*this == b); }
lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
- lbool operator && (lbool b) const {
- uint8_t sel = (this->value << 1) | (b.value << 3);
- uint8_t v = (0xF7F755F4 >> sel) & 3;
- return lbool(v); }
+ lbool operator&&(lbool b) const
+ {
+ uint8_t sel = (this->value << 1) | (b.value << 3);
+ uint8_t v = (0xF7F755F4 >> sel) & 3;
+ return lbool(v);
+ }
lbool operator || (lbool b) const {
uint8_t sel = (this->value << 1) | (b.value << 3);
@@ -163,14 +164,14 @@ class Clause {
header.reloced = 0;
header.size = ps.size();
- for (int i = 0; i < ps.size(); i++)
- data[i].lit = ps[i];
+ for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i];
if (header.has_extra){
if (header.learnt)
- data[header.size].act = 0;
- else
- calcAbstraction(); }
+ data[header.size].act = 0;
+ else
+ calcAbstraction();
+ }
}
public:
@@ -256,9 +257,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
}
- void reloc(CRef& cr,
- ClauseAllocator& to,
- CVC4::TSatProof<Solver>* proof = NULL);
+ void reloc(CRef& cr, ClauseAllocator& to);
};
@@ -275,7 +274,7 @@ class OccLists
public:
OccLists(const Deleted& d) : deleted(d) {}
-
+
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
@@ -334,13 +333,12 @@ class CMap
typedef Map<CRef, T, CRefHash> HashTable;
HashTable map;
-
+
public:
// Size-operations:
void clear () { map.clear(); }
int size () const { return map.elems(); }
-
// Insert/Remove/Test mapping:
void insert (CRef cr, const T& t){ map.insert(cr, t); }
void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
@@ -363,15 +361,14 @@ class CMap
printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
};
-
/*_________________________________________________________________________________________________
|
| subsumes : (other : const Clause&) -> Lit
-|
+|
| Description:
-| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
-| by subsumption resolution.
-|
+| Checks if clause subsumes 'other', and at the same time, if it can be
+used to simplify 'other' | by subsumption resolution.
+|
| Result:
| lit_Error - No subsumption or simplification
| lit_Undef - Clause subsumes 'other'
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 6641310cc..9429e4ced 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -23,7 +23,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "options/bv_options.h"
#include "options/smt_options.h"
#include "proof/clause_id.h"
-#include "proof/proof.h"
#include "prop/bvminisat/mtl/Sort.h"
#include "prop/bvminisat/utils/System.h"
@@ -64,7 +63,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context)
asymm_lits(0),
eliminated_vars(0),
elimorder(1),
- use_simplification(!PROOF_ON()),
+ use_simplification(true),
occurs(ClauseDeleted(ca)),
elim_heap(ElimLt(n_occ)),
bwdsub_assigns(0),
@@ -94,7 +93,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context)
SimpSolver::~SimpSolver()
{
- // CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time);
+ // CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time);
}
@@ -111,7 +110,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) {
touched .push(0);
elim_heap .insert(v);
if (freeze) {
- setFrozen(v, true);
+ setFrozen(v, true);
}
}
return v;
@@ -122,7 +121,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) {
lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
{
only_bcp = false;
-
+
vec<Var> extra_frozen;
lbool result = l_True;
@@ -210,14 +209,15 @@ void SimpSolver::removeClause(CRef cr)
const Clause& clause = ca[cr];
if (use_simplification)
+ {
for (int i = 0; i < clause.size(); i++)
{
n_occ[toInt(clause[i])]--;
updateElimHeap(var(clause[i]));
occurs.smudge(var(clause[i]));
}
-
- Solver::removeClause(cr);
+ }
+ Solver::removeClause(cr);
}
@@ -546,9 +546,10 @@ bool SimpSolver::eliminateVar(Var v)
for (int i = 0; i < pos.size(); i++)
for (int j = 0; j < neg.size(); j++)
- if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
- (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
- return true;
+ if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+ && (++cnt > cls.size() + grow
+ || (clause_lim != -1 && clause_size > clause_lim)))
+ return true;
// Delete and store old clauses:
eliminated[v] = true;
@@ -565,8 +566,7 @@ bool SimpSolver::eliminateVar(Var v)
mkElimClause(elimclauses, ~mkLit(v));
}
- for (int i = 0; i < cls.size(); i++)
- removeClause(cls[i]);
+ for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
// Produce clauses in cross product:
vec<Lit>& resolvent = add_tmp;
@@ -580,7 +580,7 @@ bool SimpSolver::eliminateVar(Var v)
// Free occurs list for this variable:
occurs[v].clear(true);
-
+
// Free watchers lists for this variable, if possible:
if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
@@ -600,7 +600,7 @@ bool SimpSolver::substitute(Var v, Lit x)
eliminated[v] = true;
setDecisionVar(v, false);
const vec<CRef>& cls = occurs.lookup(v);
-
+
vec<Lit>& subst_clause = add_tmp;
for (int i = 0; i < cls.size(); i++){
Clause& clause = ca[cls[i]];
@@ -643,7 +643,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
{
// CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time);
-
+
if (!simplify())
return false;
else if (!use_simplification)
@@ -655,9 +655,12 @@ bool SimpSolver::eliminate(bool turn_off_elim)
gatherTouchedClauses();
// printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
- if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
- !backwardSubsumptionCheck(true)){
- ok = false; goto cleanup; }
+ if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
+ && !backwardSubsumptionCheck(true))
+ {
+ ok = false;
+ goto cleanup;
+ }
// Empty elim_heap and return immediately on user-interrupt:
if (asynch_interrupt){
@@ -670,7 +673,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
// printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
for (int cnt = 0; !elim_heap.empty(); cnt++){
Var elim = elim_heap.removeMin();
-
+
if (asynch_interrupt) break;
if (isEliminated(elim) || value(elim) != l_Undef) continue;
@@ -720,8 +723,10 @@ bool SimpSolver::eliminate(bool turn_off_elim)
}
if (verbosity >= 1 && elimclauses.size() > 0)
- printf("| Eliminated clauses: %10.2f Mb |\n",
- double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+ printf(
+ "| Eliminated clauses: %10.2f Mb "
+ " |\n",
+ double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
return ok;
@@ -772,15 +777,17 @@ void SimpSolver::garbageCollect()
{
// Initialize the next region to a size corresponding to the estimated utilization degree. This
// is not precise but should avoid some unnecessary reallocations for the new region:
- ClauseAllocator to(ca.size() - ca.wasted());
+ ClauseAllocator to(ca.size() - ca.wasted());
cleanUpClauses();
to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
relocAll(to);
Solver::relocAll(to);
if (verbosity >= 2)
- printf("| Garbage collection: %12d bytes => %12d bytes |\n",
- ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ printf(
+ "| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size() * ClauseAllocator::Unit_Size,
+ to.size() * ClauseAllocator::Unit_Size);
to.moveTo(ca);
}
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index ca447cea8..7cc5b16cd 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -19,7 +19,6 @@
#ifdef CVC4_USE_CADICAL
#include "base/check.h"
-#include "proof/sat_proof.h"
namespace CVC4 {
namespace prop {
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index a6a4b6859..c46cd5136 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -83,22 +83,13 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
}
}
- if (PROOF_ON() && d_cnfProof)
- {
- d_cnfProof->pushCurrentDefinition(node);
- }
-
ClauseId clause_id = d_satSolver->addClause(c, d_removable);
if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
- if (PROOF_ON() && d_cnfProof)
+ if (d_cnfProof && clause_id != ClauseIdError)
{
- if (clause_id != ClauseIdError)
- {
- d_cnfProof->registerConvertedClause(clause_id);
- }
- d_cnfProof->popCurrentDefinition();
- };
+ d_cnfProof->registerConvertedClause(clause_id);
+ }
}
void CnfStream::assertClause(TNode node, SatLiteral a) {
@@ -171,11 +162,17 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
// non-empty and that we are not associating a bogus assertion with the
// clause. This should be ok because we use the mapping back to assertions
// for clauses from input assertions only.
- PROOF(if (d_cnfProof) { d_cnfProof->pushCurrentAssertion(Node::null()); });
+ if (d_cnfProof)
+ {
+ d_cnfProof->pushCurrentAssertion(Node::null());
+ }
lit = toCNF(n, false);
- PROOF(if (d_cnfProof) { d_cnfProof->popCurrentAssertion(); });
+ if (d_cnfProof)
+ {
+ d_cnfProof->popCurrentAssertion();
+ }
// Store backward-mappings
// These may already exist
@@ -547,7 +544,6 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
// If the node is a conjunction, we handle each conjunct separately
for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
conjunct != node_end; ++conjunct ) {
- PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(*conjunct, node););
convertAndAssert(*conjunct, false);
}
} else {
@@ -581,7 +577,6 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
// If the node is a conjunction, we handle each conjunct separately
for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
conjunct != node_end; ++conjunct ) {
- PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence((*conjunct).negate(), node.negate()););
convertAndAssert(*conjunct, true);
}
}
@@ -658,8 +653,6 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
clause[1] = q;
assertClause(node, clause);
} else {// Construct the
- PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[0], node.negate()););
- PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[1].negate(), node.negate()););
// !(p => q) is the same as (p && ~q)
convertAndAssert(node[0], false);
convertAndAssert(node[1], true);
@@ -693,32 +686,23 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
void TseitinCnfStream::convertAndAssert(TNode node,
bool removable,
bool negated,
- ProofRule proof_id,
- TNode from) {
+ bool input)
+{
Debug("cnf") << "convertAndAssert(" << node
<< ", removable = " << (removable ? "true" : "false")
<< ", negated = " << (negated ? "true" : "false") << ")" << endl;
d_removable = removable;
- PROOF
- (if (d_cnfProof) {
- Node assertion = negated ? node.notNode() : (Node)node;
- Node from_assertion = negated? from.notNode() : (Node) from;
-
- if (proof_id != RULE_INVALID) {
- d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
- d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
- }
- else {
- d_cnfProof->pushCurrentAssertion(assertion);
- d_cnfProof->registerAssertion(assertion, proof_id);
- }
- });
+ if (d_cnfProof)
+ {
+ d_cnfProof->pushCurrentAssertion(negated ? node.notNode() : (Node)node,
+ input);
+ }
convertAndAssert(node, negated);
- PROOF
- (if (d_cnfProof) {
- d_cnfProof->popCurrentAssertion();
- });
+ if (d_cnfProof)
+ {
+ d_cnfProof->popCurrentAssertion();
+ }
}
void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 40243e5b9..aec4257f2 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -186,10 +186,13 @@ class CnfStream {
* @param node node to convert and assert
* @param removable whether the sat solver can choose to remove the clauses
* @param negated whether we are asserting the node negated
+ * @param input whether it is an input assertion (rather than a lemma). This
+ * information is only relevant for unsat core tracking.
*/
- virtual void convertAndAssert(TNode node, bool removable, bool negated,
- ProofRule proof_id,
- TNode from = TNode::null()) = 0;
+ virtual void convertAndAssert(TNode node,
+ bool removable,
+ bool negated,
+ bool input = false) = 0;
/**
* Get the node that is represented by the given SatLiteral.
@@ -269,12 +272,13 @@ class TseitinCnfStream : public CnfStream {
* @param node the formula to assert
* @param removable is this something that can be erased
* @param negated true if negated
+ * @param input whether it is an input assertion (rather than a lemma). This
+ * information is only relevant for unsat core tracking.
*/
void convertAndAssert(TNode node,
bool removable,
bool negated,
- ProofRule rule,
- TNode from = TNode::null()) override;
+ bool input = false) override;
private:
/**
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index cf23758f1..92817a70c 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -19,8 +19,6 @@
#include "prop/cryptominisat.h"
#include "base/check.h"
-#include "proof/clause_id.h"
-#include "proof/sat_proof.h"
#include <cryptominisat5/cryptominisat.h>
@@ -87,8 +85,9 @@ void CryptoMinisatSolver::init()
CryptoMinisatSolver::~CryptoMinisatSolver() {}
ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
- bool rhs,
- bool removable) {
+ bool rhs,
+ bool removable)
+{
Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n";
if (!d_okay) {
@@ -97,7 +96,7 @@ ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
}
++(d_statistics.d_xorClausesAdded);
-
+
// ensure all sat literals have positive polarity by pushing
// the negation on the result
std::vector<CMSatVar> xor_clause;
@@ -119,36 +118,19 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
}
++(d_statistics.d_clausesAdded);
-
+
std::vector<CMSat::Lit> internal_clause;
toInternalClause(clause, internal_clause);
bool nowOkay = d_solver->add_clause(internal_clause);
ClauseId freshId;
- if (THEORY_PROOF_ON())
- {
- freshId = ClauseId(ProofManager::currentPM()->nextId());
- // If this clause results in a conflict, then `nowOkay` may be false, but
- // we still need to register this clause as used. Thus, we look at
- // `d_okay` instead
- if (d_bvp && d_okay)
- {
- d_bvp->registerUsedClause(freshId, clause);
- }
- }
- else
- {
- freshId = ClauseIdError;
- }
+ freshId = ClauseIdError;
d_okay &= nowOkay;
return freshId;
}
-bool CryptoMinisatSolver::ok() const {
- return d_okay;
-}
-
+bool CryptoMinisatSolver::ok() const { return d_okay; }
SatVariable CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
d_solver->new_var();
@@ -208,19 +190,11 @@ SatValue CryptoMinisatSolver::value(SatLiteral l){
return toSatLiteralValue(value);
}
-SatValue CryptoMinisatSolver::modelValue(SatLiteral l){
- return value(l);
-}
+SatValue CryptoMinisatSolver::modelValue(SatLiteral l) { return value(l); }
unsigned CryptoMinisatSolver::getAssertionLevel() const {
Unreachable() << "No interface to get assertion level in Cryptominisat";
- return -1;
-}
-
-void CryptoMinisatSolver::setClausalProofLog(proof::ClausalBitVectorProof* bvp)
-{
- d_bvp = bvp;
- d_solver->set_drat(&bvp->getDratOstream(), false);
+ return -1;
}
// Satistics for CryptoMinisatSolver
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index d60855654..6d3b351b0 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -21,7 +21,6 @@
#ifdef CVC4_USE_CRYPTOMINISAT
-#include "proof/clausal_bitvector_proof.h"
#include "prop/sat_solver.h"
// Cryptominisat has name clashes with the other Minisat implementations since
@@ -68,7 +67,6 @@ class CryptoMinisatSolver : public SatSolver
SatValue modelValue(SatLiteral l) override;
unsigned getAssertionLevel() const override;
- void setClausalProofLog(proof::ClausalBitVectorProof* bvp) override;
private:
class Statistics
@@ -97,7 +95,6 @@ class CryptoMinisatSolver : public SatSolver
void init();
std::unique_ptr<CMSat::SATSolver> d_solver;
- proof::ClausalBitVectorProof* d_bvp;
unsigned d_numVariables;
bool d_okay;
SatVariable d_true;
diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp
index 0440fcd4e..544a37a3e 100644
--- a/src/prop/kissat.cpp
+++ b/src/prop/kissat.cpp
@@ -19,7 +19,6 @@
#ifdef CVC4_USE_KISSAT
#include "base/check.h"
-#include "proof/sat_proof.h"
namespace CVC4 {
namespace prop {
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index f56f6a447..311224a03 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -30,6 +30,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "options/prop_options.h"
#include "options/smt_options.h"
#include "proof/clause_id.h"
+#include "proof/cnf_proof.h"
#include "proof/proof_manager.h"
#include "proof/sat_proof.h"
#include "proof/sat_proof_implementation.h"
@@ -217,7 +218,10 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
propagation_budget(-1),
asynch_interrupt(false)
{
- PROOF(ProofManager::currentPM()->initSatProof(this);)
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->initSatProof(this);
+ }
// Create the constant variables
varTrue = newVar(true, false, false);
@@ -227,11 +231,11 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy,
uncheckedEnqueue(mkLit(varTrue, false));
uncheckedEnqueue(mkLit(varFalse, true));
// FIXME: these should be axioms I believe
- PROOF
- (
- ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
- ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
- );
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
+ ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
+ }
}
@@ -390,15 +394,20 @@ CRef Solver::reason(Var x) {
// FIXME: at some point will need more information about where this explanation
// came from (ie. the theory/sharing)
Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
- PROOF(ClauseId id = ProofManager::getSatProof()->registerClause(
- real_reason, THEORY_LEMMA);
- ProofManager::getCnfProof()->registerConvertedClause(id, true);
- // explainPropagation() pushes the explanation on the assertion stack
- // in CnfProof, so we need to pop it here. This is important because
- // reason() may be called indirectly while adding a clause, which can
- // lead to a wrong assertion being associated with the clause being
- // added (see issue #2137).
- ProofManager::getCnfProof()->popCurrentAssertion(););
+ if (options::unsatCores())
+ {
+ ClauseId id = ProofManager::getSatProof()->registerClause(real_reason,
+ THEORY_LEMMA);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ // explainPropagation() pushes the explanation on the assertion stack
+ // in CnfProof, so we need to pop it here. This is important because
+ // reason() may be called indirectly while adding a clause, which can
+ // lead to a wrong assertion being associated with the clause being
+ // added (see issue #2137).
+ ProofManager::getCnfProof()->popCurrentAssertion();
+ }
vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
clauses_removable.push(real_reason);
attachClause(real_reason);
@@ -441,9 +450,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
}
// If a literal is false at 0 level (both sat and user level) we also ignore it
if (value(ps[i]) == l_False) {
- if (!PROOF_ON() && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
+ if (!options::unsatCores() && level(var(ps[i])) == 0
+ && user_level(var(ps[i])) == 0)
+ {
continue;
- } else {
+ }
+ else
+ {
// If we decide to keep it, we count it into the false literals
falseLiteralsCount ++;
}
@@ -467,34 +480,46 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
lemmas.push();
ps.copyTo(lemmas.last());
lemmas_removable.push(removable);
- PROOF(
- // Store the expression being converted to CNF until
- // the clause is actually created
- Node assertion = ProofManager::getCnfProof()->getCurrentAssertion();
- Node def = ProofManager::getCnfProof()->getCurrentDefinition();
- lemmas_cnf_assertion.push_back(std::make_pair(assertion, def));
- id = ClauseIdUndef;
- );
- // does it have to always be a lemma?
- // PROOF(id = ProofManager::getSatProof()->registerUnitClause(ps[0], THEORY_LEMMA););
- // PROOF(id = ProofManager::getSatProof()->registerTheoryLemma(ps););
- // Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
- // lemmas_proof_id.push(proof_id);
+ if (options::unsatCores())
+ {
+ // Store the expression being converted to CNF until
+ // the clause is actually created
+ lemmas_cnf_assertion.push_back(
+ ProofManager::getCnfProof()->getCurrentAssertion());
+ id = ClauseIdUndef;
+ }
} else {
assert(decisionLevel() == 0);
// If all false, we're in conflict
if (ps.size() == falseLiteralsCount) {
- if(PROOF_ON()) {
+ if (options::unsatCores())
+ {
// Take care of false units here; otherwise, we need to
// construct the clause below to give to the proof manager
// as the final conflict.
if(falseLiteralsCount == 1) {
- PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); )
- PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
+ if (options::unsatCores())
+ {
+ ClauseKind ck =
+ ProofManager::getCnfProof()->getCurrentAssertionKind()
+ ? INPUT
+ : THEORY_LEMMA;
+ id = ProofManager::getSatProof()->storeUnitConflict(ps[0], ck);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ if (ck == THEORY_LEMMA)
+ {
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ }
+ ProofManager::getSatProof()->finalizeProof(
+ CVC4::Minisat::CRef_Lazy);
+ }
return ok = false;
}
- } else {
+ }
+ else
+ {
return ok = false;
}
}
@@ -509,14 +534,23 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
cr = ca.alloc(clauseLevel, ps, false);
clauses_persistent.push(cr);
- attachClause(cr);
-
- if(PROOF_ON()) {
- PROOF(
- id = ProofManager::getSatProof()->registerClause(cr, INPUT);
- )
- if(ps.size() == falseLiteralsCount) {
- PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
+ attachClause(cr);
+
+ if (options::unsatCores())
+ {
+ ClauseKind ck = ProofManager::getCnfProof()->getCurrentAssertionKind()
+ ? INPUT
+ : THEORY_LEMMA;
+ id = ProofManager::getSatProof()->registerClause(cr, ck);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ if (ck == THEORY_LEMMA)
+ {
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ }
+ if (ps.size() == falseLiteralsCount)
+ {
+ ProofManager::getSatProof()->finalizeProof(cr);
return ok = false;
}
}
@@ -527,15 +561,25 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
if(assigns[var(ps[0])] == l_Undef) {
assert(assigns[var(ps[0])] != l_False);
uncheckedEnqueue(ps[0], cr);
- Debug("cores") << "i'm registering a unit clause, input" << std::endl;
- PROOF(
- if(ps.size() == 1) {
- id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT);
- }
- );
+ Debug("cores") << "i'm registering a unit clause, maybe input"
+ << std::endl;
+ if (options::unsatCores() && ps.size() == 1)
+ {
+ ClauseKind ck =
+ ProofManager::getCnfProof()->getCurrentAssertionKind()
+ ? INPUT
+ : THEORY_LEMMA;
+ id = ProofManager::getSatProof()->registerUnitClause(ps[0], ck);
+ // map id to assertion, which may be required if looking for
+ // lemmas in unsat core
+ if (ck == THEORY_LEMMA)
+ {
+ ProofManager::getCnfProof()->registerConvertedClause(id);
+ }
+ }
CRef confl = propagate(CHECK_WITHOUT_THEORY);
if(! (ok = (confl == CRef_Undef)) ) {
- if (PROOF_ON())
+ if (options::unsatCores())
{
if (ca[confl].size() == 1)
{
@@ -552,7 +596,10 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
}
return ok;
} else {
- PROOF(id = ClauseIdUndef;);
+ if (options::unsatCores())
+ {
+ id = ClauseIdUndef;
+ }
return ok;
}
}
@@ -575,7 +622,10 @@ void Solver::attachClause(CRef cr) {
void Solver::detachClause(CRef cr, bool strict) {
const Clause& c = ca[cr];
- PROOF( ProofManager::getSatProof()->markDeleted(cr); );
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->markDeleted(cr);
+ }
Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
assert(c.size() > 1);
@@ -826,7 +876,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
int max_resolution_level = 0; // Maximal level of the resolved clauses
- PROOF( ProofManager::getSatProof()->startResChain(confl); )
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->startResChain(confl);
+ }
do{
assert(confl != CRef_Undef); // (otherwise should be UIP)
@@ -867,9 +920,9 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
}
// FIXME: can we do it lazily if we actually need the proof?
- if (level(var(q)) == 0)
+ if (options::unsatCores() && level(var(q)) == 0)
{
- PROOF(ProofManager::getSatProof()->resolveOutUnit(q);)
+ ProofManager::getSatProof()->resolveOutUnit(q);
}
}
}
@@ -881,8 +934,9 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
seen[var(p)] = 0;
pathC--;
- if ( pathC > 0 && confl != CRef_Undef ) {
- PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); )
+ if (options::unsatCores() && pathC > 0 && confl != CRef_Undef)
+ {
+ ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
}
}while (pathC > 0);
@@ -905,7 +959,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
// Literal is not redundant
out_learnt[j++] = out_learnt[i];
} else {
- PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); )
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
+ }
// Literal is redundant, to be safe, mark the level as current assertion level
// TODO: maybe optimize
max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i])));
@@ -1169,7 +1226,10 @@ void Solver::propagateTheory() {
addClause(explanation, true, id);
// explainPropagation() pushes the explanation on the assertion
// stack in CnfProof, so we need to pop it here.
- PROOF(ProofManager::getCnfProof()->popCurrentAssertion();)
+ if (options::unsatCores())
+ {
+ ProofManager::getCnfProof()->popCurrentAssertion();
+ }
}
}
}
@@ -1310,9 +1370,10 @@ void Solver::removeSatisfied(vec<CRef>& cs)
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (satisfied(c)) {
- if (locked(c)) {
+ if (options::unsatCores() && locked(c))
+ {
// store a resolution of the literal c propagated
- PROOF( ProofManager::getSatProof()->storeUnitResolution(c[0]); )
+ ProofManager::getSatProof()->storeUnitResolution(c[0]);
}
removeClause(cs[i]);
}
@@ -1412,8 +1473,11 @@ lbool Solver::search(int nof_conflicts)
conflicts++; conflictC++;
if (decisionLevel() == 0) {
- PROOF( ProofManager::getSatProof()->finalizeProof(confl); )
- return l_False;
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->finalizeProof(confl);
+ }
+ return l_False;
}
// Analyze the conflict
@@ -1425,8 +1489,10 @@ lbool Solver::search(int nof_conflicts)
if (learnt_clause.size() == 1) {
uncheckedEnqueue(learnt_clause[0]);
- PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); )
-
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->endResChain(learnt_clause[0]);
+ }
} else {
CRef cr =
ca.alloc(assertionLevelOnly() ? assertionLevel : max_level,
@@ -1436,15 +1502,12 @@ lbool Solver::search(int nof_conflicts)
attachClause(cr);
claBumpActivity(ca[cr]);
uncheckedEnqueue(learnt_clause[0], cr);
- PROOF(ClauseId id =
- ProofManager::getSatProof()->registerClause(cr, LEARNT);
- PSTATS(std::unordered_set<int> cl_levels;
- for (int i = 0; i < learnt_clause.size(); ++i) {
- cl_levels.insert(level(var(learnt_clause[i])));
- } ProofManager::getSatProof()
- ->storeClauseGlue(id, cl_levels.size());)
- ProofManager::getSatProof()
- ->endResChain(id););
+ if (options::unsatCores())
+ {
+ ClauseId id =
+ ProofManager::getSatProof()->registerClause(cr, LEARNT);
+ ProofManager::getSatProof()->endResChain(id);
+ }
}
varDecayActivity();
@@ -1469,25 +1532,33 @@ lbool Solver::search(int nof_conflicts)
}
} else {
-
- // If this was a final check, we are satisfiable
- if (check_type == CHECK_FINAL) {
- bool decisionEngineDone = d_proxy->isDecisionEngineDone();
- // Unless a lemma has added more stuff to the queues
- if (!decisionEngineDone &&
- (!order_heap.empty() || qhead < trail.size()) ) {
- check_type = CHECK_WITH_THEORY;
- continue;
- } else if (recheck) {
- // There some additional stuff added, so we go for another full-check
- continue;
- } else {
- // Yes, we're truly satisfiable
- return l_True;
- }
- } else if (check_type == CHECK_FINAL_FAKE) {
+ // If this was a final check, we are satisfiable
+ if (check_type == CHECK_FINAL)
+ {
+ bool decisionEngineDone = d_proxy->isDecisionEngineDone();
+ // Unless a lemma has added more stuff to the queues
+ if (!decisionEngineDone
+ && (!order_heap.empty() || qhead < trail.size()))
+ {
check_type = CHECK_WITH_THEORY;
+ continue;
+ }
+ else if (recheck)
+ {
+ // There some additional stuff added, so we go for another
+ // full-check
+ continue;
}
+ else
+ {
+ // Yes, we're truly satisfiable
+ return l_True;
+ }
+ }
+ else if (check_type == CHECK_FINAL_FAKE)
+ {
+ check_type = CHECK_WITH_THEORY;
+ }
if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
|| !withinBudget(ResourceManager::Resource::SatConflictStep))
@@ -1744,7 +1815,10 @@ void Solver::relocAll(ClauseAllocator& to)
// printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
vec<Watcher>& ws = watches[p];
for (int j = 0; j < ws.size(); j++)
- ca.reloc(ws[j].cref, to, NULLPROOF(ProofManager::getSatProof()));
+ ca.reloc(ws[j].cref,
+ to,
+ CVC4::options::unsatCores() ? ProofManager::getSatProof()
+ : nullptr);
}
// All reasons:
@@ -1753,22 +1827,31 @@ void Solver::relocAll(ClauseAllocator& to)
Var v = var(trail[i]);
if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
- ca.reloc(
- vardata[v].d_reason, to, NULLPROOF(ProofManager::getSatProof()));
+ ca.reloc(vardata[v].d_reason,
+ to,
+ CVC4::options::unsatCores() ? ProofManager::getSatProof()
+ : nullptr);
}
// All learnt:
//
for (int i = 0; i < clauses_removable.size(); i++)
ca.reloc(
- clauses_removable[i], to, NULLPROOF(ProofManager::getSatProof()));
+ clauses_removable[i],
+ to,
+ CVC4::options::unsatCores() ? ProofManager::getSatProof() : nullptr);
// All original:
//
for (int i = 0; i < clauses_persistent.size(); i++)
ca.reloc(
- clauses_persistent[i], to, NULLPROOF(ProofManager::getSatProof()));
+ clauses_persistent[i],
+ to,
+ CVC4::options::unsatCores() ? ProofManager::getSatProof() : nullptr);
- PROOF(ProofManager::getSatProof()->finishUpdateCRef();)
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->finishUpdateCRef();
+ }
}
@@ -1874,7 +1957,7 @@ CRef Solver::updateLemmas() {
// If it's an empty lemma, we have a conflict at zero level
if (lemma.size() == 0) {
- Assert(!PROOF_ON());
+ Assert(!options::unsatCores());
conflict = CRef_Lazy;
backtrackLevel = 0;
Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -1904,7 +1987,8 @@ CRef Solver::updateLemmas() {
// Last index in the trail
int backtrack_index = trail.size();
- PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
+ Assert(!options::unsatCores()
+ || lemmas.size() == (int)lemmas_cnf_assertion.size());
// Attach all the clauses and enqueue all the propagations
for (int j = 0; j < lemmas.size(); ++j)
@@ -1928,15 +2012,16 @@ CRef Solver::updateLemmas() {
}
lemma_ref = ca.alloc(clauseLevel, lemma, removable);
- PROOF(TNode cnf_assertion = lemmas_cnf_assertion[j].first;
- TNode cnf_def = lemmas_cnf_assertion[j].second;
-
- Debug("pf::sat")
- << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
- ClauseId id = ProofManager::getSatProof()->registerClause(
- lemma_ref, THEORY_LEMMA);
- ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
- ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def););
+ if (options::unsatCores())
+ {
+ TNode cnf_assertion = lemmas_cnf_assertion[j];
+
+ Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)"
+ << std::endl;
+ ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref,
+ THEORY_LEMMA);
+ ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+ }
if (removable) {
clauses_removable.push(lemma_ref);
} else {
@@ -1948,17 +2033,15 @@ CRef Solver::updateLemmas() {
// If the lemma is propagating enqueue its literal (or set the conflict)
if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
- if (PROOF_ON() && lemma.size() == 1)
+ if (options::unsatCores() && lemma.size() == 1)
{
- Node cnf_assertion = lemmas_cnf_assertion[j].first;
- Node cnf_def = lemmas_cnf_assertion[j].second;
+ Node cnf_assertion = lemmas_cnf_assertion[j];
Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) "
<< cnf_assertion << value(lemma[0]) << std::endl;
ClauseId id = ProofManager::getSatProof()->registerUnitClause(
lemma[0], THEORY_LEMMA);
ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
- ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
}
if (value(lemma[0]) == l_False) {
@@ -1969,7 +2052,10 @@ CRef Solver::updateLemmas() {
} else {
Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
conflict = CRef_Lazy;
- PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); );
+ if (options::unsatCores())
+ {
+ ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
+ }
}
} else {
Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
@@ -1979,7 +2065,8 @@ CRef Solver::updateLemmas() {
}
}
- PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size()););
+ Assert(!options::unsatCores()
+ || lemmas.size() == (int)lemmas_cnf_assertion.size());
// Clear the lemmas
lemmas.clear();
lemmas_cnf_assertion.clear();
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 508947456..a5f3664e8 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -63,7 +63,7 @@ public:
typedef Var TVar;
typedef Lit TLit;
- typedef Clause TClause;
+ typedef Clause TClause;
typedef CRef TCRef;
typedef vec<Lit> TLitVec;
@@ -98,7 +98,7 @@ public:
vec<bool> lemmas_removable;
/** Nodes being converted to CNF */
- std::vector<std::pair<CVC4::Node, CVC4::Node> > lemmas_cnf_assertion;
+ std::vector<CVC4::Node> lemmas_cnf_assertion;
/** Do a another check if FULL_EFFORT was the last one */
bool recheck;
@@ -203,7 +203,7 @@ public:
lbool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions.
bool okay () const; // FALSE means solver is in a conflicting state
- void toDimacs ();
+ void toDimacs();
void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format.
void toDimacs (const char *file, const vec<Lit>& assumps);
void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index bbd6e17a2..b30d97aee 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -73,9 +73,14 @@ inline bool sign (Lit p) { return p.x & 1; }
inline int var (Lit p) { return p.x >> 1; }
// Mapping Literals to and from compact integers suitable for array indexing:
-inline int toInt (Var v) { return v; }
-inline int toInt (Lit p) { return p.x; }
-inline Lit toLit (int i) { Lit p; p.x = i; return p; }
+inline int toInt(Var v) { return v; }
+inline int toInt(Lit p) { return p.x; }
+inline Lit toLit(int i)
+{
+ Lit p;
+ p.x = i;
+ return p;
+}
//const Lit lit_Undef = mkLit(var_Undef, false); // }- Useful special constants.
//const Lit lit_Error = mkLit(var_Undef, true ); // }
@@ -83,20 +88,19 @@ inline Lit toLit (int i) { Lit p; p.x = i; return p; }
const Lit lit_Undef = { -2 }; // }- Useful special constants.
const Lit lit_Error = { -1 }; // }
-
//=================================================================================================
// Lifted booleans:
//
-// NOTE: this implementation is optimized for the case when comparisons between values are mostly
-// between one variable and one constant. Some care had to be taken to make sure that gcc
-// does enough constant propagation to produce sensible code, and this appears to be somewhat
-// fragile unfortunately.
+// NOTE: this implementation is optimized for the case when comparisons between
+// values are mostly
+// between one variable and one constant. Some care had to be taken to
+// make sure that gcc does enough constant propagation to produce sensible
+// code, and this appears to be somewhat fragile unfortunately.
/*
- This is to avoid multiple definitions of l_True, l_False and l_Undef if using multiple copies of
- Minisat.
- IMPORTANT: if we you change the value of the constants so that it is not the same in all copies
- of Minisat this breaks!
+ This is to avoid multiple definitions of l_True, l_False and l_Undef if using
+ multiple copies of Minisat. IMPORTANT: if we you change the value of the
+ constants so that it is not the same in all copies of Minisat this breaks!
*/
#ifndef l_True
@@ -124,10 +128,12 @@ public:
bool operator != (lbool b) const { return !(*this == b); }
lbool operator ^ (bool b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
- lbool operator && (lbool b) const {
- uint8_t sel = (this->value << 1) | (b.value << 3);
- uint8_t v = (0xF7F755F4 >> sel) & 3;
- return lbool(v); }
+ lbool operator&&(lbool b) const
+ {
+ uint8_t sel = (this->value << 1) | (b.value << 3);
+ uint8_t v = (0xF7F755F4 >> sel) & 3;
+ return lbool(v);
+ }
lbool operator || (lbool b) const {
uint8_t sel = (this->value << 1) | (b.value << 3);
@@ -163,7 +169,7 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::vec<Minisat::Lit>&
}
inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
- std::string val_str;
+ std::string val_str;
if( val == l_False ) {
val_str = "0";
} else if (val == l_True ) {
@@ -208,14 +214,14 @@ class Clause {
header.size = ps.size();
header.level = level;
- for (int i = 0; i < ps.size(); i++)
- data[i].lit = ps[i];
+ for (int i = 0; i < ps.size(); i++) data[i].lit = ps[i];
if (header.has_extra){
if (header.removable)
- data[header.size].act = 0;
- else
- calcAbstraction(); }
+ data[header.size].act = 0;
+ else
+ calcAbstraction();
+ }
}
public:
@@ -321,7 +327,7 @@ class OccLists
public:
OccLists(const Deleted& d) : deleted(d) {}
-
+
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
void resizeTo (const Idx& idx);
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
@@ -394,13 +400,12 @@ class CMap
typedef Map<CRef, T, CRefHash> HashTable;
HashTable map;
-
+
public:
// Size-operations:
void clear () { map.clear(); }
int size () const { return map.elems(); }
-
// Insert/Remove/Test mapping:
void insert (CRef cr, const T& t){ map.insert(cr, t); }
void growTo (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
@@ -423,15 +428,14 @@ class CMap
printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
};
-
/*_________________________________________________________________________________________________
|
| subsumes : (other : const Clause&) -> Lit
-|
+|
| Description:
-| Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
-| by subsumption resolution.
-|
+| Checks if clause subsumes 'other', and at the same time, if it can be
+used to simplify 'other' | by subsumption resolution.
+|
| Result:
| lit_Error - No subsumption or simplification
| lit_Undef - Clause subsumes 'other'
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index a4d2dce8a..25353e416 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -154,7 +154,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
return ClauseIdUndef;
}
d_minisat->addClause(minisat_clause, removable, clause_id);
- PROOF(Assert(clause_id != ClauseIdError););
+ Assert(!CVC4::options::unsatCores() || clause_id != ClauseIdError);
return clause_id;
}
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 23f97b5d5..0ec8981ca 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -21,8 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/simp/SimpSolver.h"
#include "options/prop_options.h"
+#include "options/smt_options.h"
#include "proof/clause_id.h"
-#include "proof/proof.h"
#include "prop/minisat/mtl/Sort.h"
#include "prop/minisat/utils/System.h"
@@ -47,25 +47,30 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
//=================================================================================================
// Constructor/Destructor:
-
-SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental) :
- Solver(proxy, context, enableIncremental)
- , grow (opt_grow)
- , clause_lim (opt_clause_lim)
- , subsumption_lim (opt_subsumption_lim)
- , simp_garbage_frac (opt_simp_garbage_frac)
- , use_asymm (opt_use_asymm)
- , use_rcheck (opt_use_rcheck)
- , use_elim (options::minisatUseElim() && !enableIncremental)
- , merges (0)
- , asymm_lits (0)
- , eliminated_vars (0)
- , elimorder (1)
- , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially
- , occurs (ClauseDeleted(ca))
- , elim_heap (ElimLt(n_occ))
- , bwdsub_assigns (0)
- , n_touched (0)
+SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy,
+ CVC4::context::Context* context,
+ bool enableIncremental)
+ : Solver(proxy, context, enableIncremental),
+ grow(opt_grow),
+ clause_lim(opt_clause_lim),
+ subsumption_lim(opt_subsumption_lim),
+ simp_garbage_frac(opt_simp_garbage_frac),
+ use_asymm(opt_use_asymm),
+ use_rcheck(opt_use_rcheck),
+ use_elim(options::minisatUseElim() && !enableIncremental),
+ merges(0),
+ asymm_lits(0),
+ eliminated_vars(0),
+ elimorder(1),
+ use_simplification(
+ !enableIncremental
+ && !options::unsatCores()) // TODO: turn off simplifications if
+ // proofs are on initially
+ ,
+ occurs(ClauseDeleted(ca)),
+ elim_heap(ElimLt(n_occ)),
+ bwdsub_assigns(0),
+ n_touched(0)
{
if(options::minisatUseElim() &&
options::minisatUseElim.wasSetByUser() &&
@@ -117,8 +122,8 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister
lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
{
if (options::minisatDumpDimacs()) {
- toDimacs();
- return l_Undef;
+ toDimacs();
+ return l_Undef;
}
assert(decisionLevel() == 0);
@@ -533,9 +538,10 @@ bool SimpSolver::eliminateVar(Var v)
for (int i = 0; i < pos.size(); i++)
for (int j = 0; j < neg.size(); j++)
- if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
- (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
- return true;
+ if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+ && (++cnt > cls.size() + grow
+ || (clause_lim != -1 && clause_size > clause_lim)))
+ return true;
// Delete and store old clauses:
eliminated[v] = true;
@@ -552,10 +558,9 @@ bool SimpSolver::eliminateVar(Var v)
mkElimClause(elimclauses, ~mkLit(v));
}
- for (int i = 0; i < cls.size(); i++)
- removeClause(cls[i]);
+ for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
- ClauseId id = ClauseIdUndef;
+ ClauseId id = ClauseIdUndef;
// Produce clauses in cross product:
vec<Lit>& resolvent = add_tmp;
for (int i = 0; i < pos.size(); i++)
@@ -569,7 +574,7 @@ bool SimpSolver::eliminateVar(Var v)
// Free occurs list for this variable:
occurs[v].clear(true);
-
+
// Free watchers lists for this variable, if possible:
if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
@@ -589,7 +594,7 @@ bool SimpSolver::substitute(Var v, Lit x)
eliminated[v] = true;
setDecisionVar(v, false);
const vec<CRef>& cls = occurs.lookup(v);
-
+
vec<Lit>& subst_clause = add_tmp;
for (int i = 0; i < cls.size(); i++){
Clause& c = ca[cls[i]];
@@ -641,9 +646,12 @@ bool SimpSolver::eliminate(bool turn_off_elim)
gatherTouchedClauses();
// printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
- if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
- !backwardSubsumptionCheck(true)){
- ok = false; goto cleanup; }
+ if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
+ && !backwardSubsumptionCheck(true))
+ {
+ ok = false;
+ goto cleanup;
+ }
// Empty elim_heap and return immediately on user-interrupt:
if (asynch_interrupt){
@@ -656,7 +664,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
// printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
for (int cnt = 0; !elim_heap.empty(); cnt++){
Var elim = elim_heap.removeMin();
-
+
if (asynch_interrupt) break;
if (isEliminated(elim) || value(elim) != l_Undef) continue;
@@ -706,8 +714,10 @@ bool SimpSolver::eliminate(bool turn_off_elim)
}
if (verbosity >= 1 && elimclauses.size() > 0)
- printf("| Eliminated clauses: %10.2f Mb |\n",
- double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+ printf(
+ "| Eliminated clauses: %10.2f Mb "
+ " |\n",
+ double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
return ok;
}
@@ -744,11 +754,11 @@ void SimpSolver::relocAll(ClauseAllocator& to)
//
for (int i = 0; i < subsumption_queue.size(); i++)
ca.reloc(subsumption_queue[i], to);
- // TODO reloc now takes the proof form the core solver
+ // TODO reloc now takes the proof form the core solver
// Temporary clause:
//
ca.reloc(bwdsub_tmpunit, to);
- // TODO reloc now takes the proof form the core solver
+ // TODO reloc now takes the proof form the core solver
}
@@ -756,15 +766,17 @@ void SimpSolver::garbageCollect()
{
// Initialize the next region to a size corresponding to the estimated utilization degree. This
// is not precise but should avoid some unnecessary reallocations for the new region:
- ClauseAllocator to(ca.size() - ca.wasted());
+ ClauseAllocator to(ca.size() - ca.wasted());
cleanUpClauses();
to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
relocAll(to);
Solver::relocAll(to);
if (verbosity >= 2)
- printf("| Garbage collection: %12d bytes => %12d bytes |\n",
- ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ printf(
+ "| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size() * ClauseAllocator::Unit_Size,
+ to.size() * ClauseAllocator::Unit_Size);
to.moveTo(ca);
- // TODO: proof.finalizeUpdateId();
+ // TODO: proof.finalizeUpdateId();
}
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index f74e52509..e71e681e5 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -99,17 +99,17 @@ PropEngine::PropEngine(TheoryEngine* te,
d_decisionEngine->setSatSolver(d_satSolver);
d_decisionEngine->setCnfStream(d_cnfStream);
- PROOF (
- ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
- );
+ if (options::unsatCores())
+ {
+ ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
+ }
}
void PropEngine::finishInit()
{
NodeManager* nm = NodeManager::currentNM();
- d_cnfStream->convertAndAssert(nm->mkConst(true), false, false, RULE_GIVEN);
- d_cnfStream->convertAndAssert(
- nm->mkConst(false).notNode(), false, false, RULE_GIVEN);
+ d_cnfStream->convertAndAssert(nm->mkConst(true), false, false);
+ d_cnfStream->convertAndAssert(nm->mkConst(false).notNode(), false, false);
}
PropEngine::~PropEngine() {
@@ -126,18 +126,15 @@ void PropEngine::assertFormula(TNode node) {
Assert(!d_inCheckSat) << "Sat solver in solve()!";
Debug("prop") << "assertFormula(" << node << ")" << endl;
// Assert as non-removable
- d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN);
+ d_cnfStream->convertAndAssert(node, false, false, true);
}
-void PropEngine::assertLemma(TNode node, bool negated,
- bool removable,
- ProofRule rule,
- TNode from) {
- //Assert(d_inCheckSat, "Sat solver should be in solve()!");
+void PropEngine::assertLemma(TNode node, bool negated, bool removable)
+{
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
// Assert as (possibly) removable
- d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
+ d_cnfStream->convertAndAssert(node, removable, negated);
}
void PropEngine::addAssertionsToDecisionEngine(
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 9a2daee49..1df862568 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -103,11 +103,7 @@ class PropEngine
* @param removable whether this lemma can be quietly removed based
* on an activity heuristic (or not)
*/
- void assertLemma(TNode node,
- bool negated,
- bool removable,
- ProofRule rule,
- TNode from = TNode::null());
+ void assertLemma(TNode node, bool negated, bool removable);
/**
* Pass a list of assertions from an AssertionPipeline to the decision engine.
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index d4b08ab71..1526e91b9 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -33,11 +33,6 @@
namespace CVC4 {
-namespace proof {
-class ClausalBitVectorProof;
-class ResolutionBitVectorProof;
-} // namespace proof
-
namespace prop {
class TheoryProxy;
@@ -58,7 +53,7 @@ public:
/** Add a clause corresponding to rhs = l1 xor .. xor ln */
virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
-
+
/**
* Create a new boolean variable in the solver.
* @param isTheoryAtom is this a theory atom that needs to be asserted to theory
@@ -84,6 +79,7 @@ public:
virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
{
Unimplemented() << "Solving under assumptions not implemented";
+ return SAT_VALUE_UNKNOWN;
};
/** Interrupt the solver */
@@ -101,10 +97,6 @@ public:
/** Check if the solver is in an inconsistent state */
virtual bool ok() const = 0;
- virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {}
-
- virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {}
-
};/* class SatSolver */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 41da4546e..d0ba4ca71 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -76,22 +76,12 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
TNode lNode = d_cnfStream->getNode(l);
Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
- LemmaProofRecipe* proofRecipe = NULL;
- PROOF(proofRecipe = new LemmaProofRecipe;);
+ Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
- Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
-
- PROOF({
- ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
- ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
-
- Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: "
- << std::endl;
- proofRecipe->dump("pf::sat");
-
- delete proofRecipe;
- proofRecipe = NULL;
- });
+ if (options::unsatCores())
+ {
+ ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
+ }
Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
if (theoryExplanation.getKind() == kind::AND) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback