Commit f5721b64 authored by delorme's avatar delorme

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/branches/PROOF_LOGGING@71 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 39fa54ff
package org.sat4j;
import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.IProofDelegate;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.proof.ProofDelegate;
import org.sat4j.specs.ISolver;
public class ProofLauncher<T extends ISolver> extends BasicLauncher {
private static final long serialVersionUID = 1L;
private final IProofDelegate proof;
private Solver solver;
public ProofLauncher(ASolverFactory<T> factory){
super(factory);
proof = new ProofDelegate();
}
protected ISolver configureSolver(String[] args) {
solver = (Solver) SolverFactory.newDefault();
solver.setTimeout(Integer.MAX_VALUE);
solver.setProof(proof);
proof.setSolver(solver);
log(solver.toString(COMMENT_PREFIX)); //$NON-NLS-1$
return solver;
}
protected void check(){
proof.check();
}
public ISolver getSolver(){
return this.solver;
}
public static void main (String args[]){
ProofLauncher<ISolver> pl = new ProofLauncher<ISolver>(SolverFactory.instance());
pl.run(args);
if (pl.getExitCode() == ExitCode.UNSATISFIABLE){
pl.check();
}
System.exit(pl.getExitCode().value());
}
}
package org.sat4j.minisat;
import org.sat4j.minisat.proof.ProofAssertionError;
import org.sat4j.specs.IVecInt;
public interface IProof {
public static final int CLAUSE_ID_NULL = -1;
int addRoot (IVecInt clause);
void beginChain (int start);
void resolve (int next, int var);
int endChain();
void deleted(int gone);
int last();
void traverse (IProofTraverser pt);
void traverse (IProofTraverser pt, int goal);
void check () throws ProofAssertionError;
void check (int goal) throws ProofAssertionError;
}
package org.sat4j.minisat;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.proof.ProofAssertionError;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVecInt;
public interface IProofDelegate {
//Constr newClause(IVecInt vlits, Constr clause);
/**
* Informs the proof delegate a new clause has been taken into account
* @param vlits literals of the clause
* @param voc the current vocabulary
* @return id of the new clause, or CLAUSE_ID_NULL
* @throws ProofAssertionError
*/
int newClause(IVecInt vlits);
void setSolver (Solver s);
void setId (IConstr clause, int id);
void deleted (IConstr gone);
void beginChain (IConstr start);
void resolveFromId (int var);
void resolve(IConstr next, int var);
void newVar(int howmany);
void onPropagate(IConstr c, int[] lits);
int afterAnalyze(IVecInt outLearnt, IVecInt analyzetoclear);
void check() throws ProofAssertionError;
void check(int goalId) throws ProofAssertionError;
}
package org.sat4j.minisat;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
public interface IProofTraverser {
void root(IVecInt c);
void chain(IVecInt clauseIds, IVecInt vars);
void deleted(int clauseId);
void done();
IVec<IVecInt> getClauses();
}
......@@ -29,9 +29,12 @@ package org.sat4j.minisat.constraints.cnf;
import java.io.Serializable;
import org.sat4j.minisat.IProof;
import org.sat4j.minisat.IProofDelegate;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.UnitPropagationListener;
import org.sat4j.minisat.proof.NullProofDelegate;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
......@@ -49,6 +52,18 @@ public abstract class WLClause implements Constr, Serializable {
protected final int[] lits;
protected final ILits voc;
/**
* @author Fabien Delorme
* ID of the current clause, used for proof logging
*/
private int id = IProof.CLAUSE_ID_NULL;
/**
* @author delorme
* Proof to propagate infos to
*/
private static IProofDelegate proof = new NullProofDelegate();
/**
* Creates a new basic clause
......@@ -64,7 +79,48 @@ public abstract class WLClause implements Constr, Serializable {
assert ps.size() == 0;
this.voc = voc;
activity = 0;
}
}
/**
* @author Fabien Delorme
* Creates a clause with an ID
* @param ps
* @param voc
* @param id id of the clause
*/
public WLClause(IVecInt ps, ILits voc, int id){
this(ps, voc);
this.id = id;
}
/**
* @author Fabien Delorme
* Returns the id of the clause
* @return
*/
public int getId(){
return this.id;
}
/**
* @author Fabien Delorme
* sets the ID of the clause. Should not be called more than once on a given clause...
* @param id
*/
public void setId(int id){
// id should not be changed once set...
assert this.id == IProof.CLAUSE_ID_NULL;
this.id = id;
}
/**
* @author delorme
* sets the IProofDelegate instances will have to give informations to
*/
public static void setProof(IProofDelegate proof){
assert proof != null;
WLClause.proof = proof;
}
/**
* Perform some sanity check before constructing a clause a) if a literal is
......
......@@ -49,6 +49,7 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import static org.sat4j.core.LiteralsUtils.var;
import java.io.PrintStream;
......@@ -64,6 +65,8 @@ import java.util.TimerTask;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.IProofDelegate;
import org.sat4j.minisat.proof.NullProofDelegate;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
......@@ -171,6 +174,11 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
private int learnedLiterals = 0;
/** Used for proof logging
* @author Fabien Delorme
*/
private IProofDelegate proof;
protected IVecInt dimacs2internal(IVecInt in) {
// if (voc.nVars() == 0) {
// throw new RuntimeException(
......@@ -195,21 +203,41 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
* an asserting clause generator
*/
public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
D dsf, IOrder<L> order, RestartStrategy restarter) {
this(acg, learner, dsf, new SearchParams(), order, restarter);
}
public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
D dsf, SearchParams params, IOrder<L> order,
RestartStrategy restarter) {
analyzer = acg;
this.learner = learner;
this.order = order;
this.params = params;
setDataStructureFactory(dsf);
this.restarter = restarter;
}
public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
D dsf, IOrder<L> order, RestartStrategy restarter) {
this(acg, learner, dsf, new SearchParams(), order, restarter, new NullProofDelegate());
}
public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
D dsf, SearchParams params, IOrder<L> order,
RestartStrategy restarter) {
this(acg, learner, dsf, params, order, restarter, new NullProofDelegate());
}
public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
D dsf, IOrder<L> order, RestartStrategy restarter, IProofDelegate proof) {
this(acg, learner, dsf, new SearchParams(), order, restarter, proof);
}
public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
D dsf, SearchParams params, IOrder<L> order,
RestartStrategy restarter, IProofDelegate proof) {
analyzer = acg;
this.learner = learner;
this.order = order;
this.params = params;
setDataStructureFactory(dsf);
this.restarter = restarter;
this.proof = proof;
this.proof.setSolver(this);
}
public void setProof (IProofDelegate proof){
this.proof = proof;
this.proof.setSolver(this);
}
/**
* Change the internal representation of the contraints. Note that the
......@@ -290,17 +318,24 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
public int newVar() {
int index = voc.nVars() + 1;
voc.ensurePool(index);
proof.newVar(1);
return index;
}
public int newVar(int howmany) {
voc.ensurePool(howmany);
proof.newVar(howmany);
return voc.nVars();
}
public IConstr addClause(IVecInt literals) throws ContradictionException {
IVecInt vlits = dimacs2internal(literals);
return addConstr(dsfactory.createClause(vlits));
IVecInt vlits = dimacs2internal(literals);
int id = proof.newClause(vlits); // Proof logger must know about this clause & the literals associated
Constr clause = dsfactory.createClause(vlits);
proof.setId(clause, id);
return addConstr(clause);
}
public boolean removeConstr(IConstr co) {
......@@ -308,11 +343,15 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
throw new IllegalArgumentException(
"Reference to the constraint to remove needed!"); //$NON-NLS-1$
}
Constr c = (Constr) co;
c.remove();
constrs.remove(c);
clearLearntClauses();
cancelLearntLiterals();
proof.deleted(c);
return true;
}
......@@ -427,6 +466,7 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
private final IVecInt outLearnt = new VecInt();
public void analyze(Constr confl, Pair results) {
boolean again = true; // analyzer.clauseNonAssertive(confl), without the side effect...
assert confl != null;
outLearnt.clear();
......@@ -437,6 +477,7 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
seen[i] = false;
}
proof.beginChain(confl);
analyzer.initAnalyze();
int p = ILits.UNDEFINED;
......@@ -456,13 +497,18 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
order.updateVar(q);
if (!seen[q >> 1]) {
// order.updateVar(q); // MINISAT
seen[q >> 1] = true;
if (voc.getLevel(q) == decisionLevel()) {
analyzer.onCurrentDecisionLevelLiteral(q);
} else if (voc.getLevel(q) > 0) {
// ajoute les variables depuis le niveau de d?cision 0
outLearnt.push(q ^ 1);
outBtlevel = Math.max(outBtlevel, voc.getLevel(q));
if (voc.getLevel(q) > 0){
seen[q >> 1] = true;
if (voc.getLevel(q) == decisionLevel()) {
analyzer.onCurrentDecisionLevelLiteral(q);
} else {
// ajoute les variables depuis le niveau de d?cision 0
outLearnt.push(q ^ 1);
outBtlevel = Math.max(outBtlevel, voc.getLevel(q));
}
}
else {
proof.resolveFromId(q >> 1);
}
}
}
......@@ -479,12 +525,20 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
} while (!seen[p >> 1]);
// seen[p.var] indique que p se trouve dans outLearnt ou dans
// le dernier niveau de d?cision
} while (analyzer.clauseNonAssertive(confl));
again = analyzer.clauseNonAssertive(confl);
if (again){
proof.resolve(confl, p >> 1);
}
} while (again);
outLearnt.set(0, p ^ 1);
simplifier.simplify(outLearnt);
int id = proof.afterAnalyze(outLearnt, analyzetoclear);
Constr c = dsfactory.createUnregisteredClause(outLearnt);
proof.setId(c, id);
slistener.learn(c);
results.reason = c;
......@@ -633,7 +687,8 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
int i, j;
// (maintain an abstraction of levels involved in conflict)
analyzetoclear.clear();
outLearnt.copyTo(analyzetoclear);
// TODO FD : removed because conflicts with proof logging
// outLearnt.copyTo(analyzetoclear);
for (i = 1, j = 1; i < outLearnt.size(); i++)
if (voc.getReason(outLearnt.get(i)) == null
|| !analyzeRemovable(outLearnt.get(i)))
......@@ -758,8 +813,10 @@ public class Solver<L extends ILits, D extends DataStructureFactory<L>>
IVec<Propagatable> constrs = dsfactory.getWatchesFor(p);
final int size = constrs.size();
for (int i = 0; i < size; i++) {
stats.inspects++;
if (!constrs.get(i).propagate(this, p)) {
// Constraint is conflicting: copy remaining watches to
// watches[p]
......@@ -1344,10 +1401,6 @@ interface ConflictTimer {
}
abstract class ConflictTimerAdapter implements Serializable, ConflictTimer {
/**
*
*/
private static final long serialVersionUID = 1L;
private int counter;
......@@ -1375,10 +1428,6 @@ abstract class ConflictTimerAdapter implements Serializable, ConflictTimer {
}
class ConflictTimerContainer implements Serializable, ConflictTimer {
/**
*
*/
private static final long serialVersionUID = 1L;
private final IVec<ConflictTimer> timers = new Vec<ConflictTimer>();
......
package org.sat4j.minisat.proof;
import java.util.Iterator;
/**
* Keeps track of a proof
* @author delorme
*
*/
public interface IProofKeeper {
void putInt(int i);
Iterator<Integer> iterator();
}
package org.sat4j.minisat.proof;
import java.io.Serializable;
import java.util.Iterator;
import org.sat4j.core.VecInt;
import org.sat4j.specs.IVecInt;
public class MemoryProofKeeper implements IProofKeeper, Serializable {
private static final long serialVersionUID = 1L;
private IVecInt content;
public MemoryProofKeeper(){
this.content = new VecInt();
}
public Iterator<Integer> iterator(){
return new MemoryProofKeeperIterator(this.content);
}
public void putInt(int i) {
this.content.push(i);
}
public String toString(){
StringBuffer sb = new StringBuffer();
int index = 0;
boolean displayIndex = true;
for (int i = 0 ; i < this.content.size() ; i++){
if (displayIndex){
sb.append (index++ + " : ");
displayIndex = false;
}
if (this.content.get(i) == 0){
sb.append ("\n");
displayIndex = true;
}
else{
sb.append(this.content.get(i) + " ");
}
}
return sb.toString();
}
}
package org.sat4j.minisat.proof;
import java.util.Iterator;
import org.sat4j.specs.IVecInt;
public class MemoryProofKeeperIterator implements Iterator<Integer> {
private IVecInt content;
private int index;
public MemoryProofKeeperIterator(IVecInt content){
this.content = content;
this.index = 0;
}
public boolean hasNext() {
return this.index < this.content.size();
}
public Integer next() {
return this.content.get(this.index++);
}
public void remove() {
}
}
package org.sat4j.minisat.proof;
import java.util.Iterator;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
public class MemoryProofKeeperVecIterator implements Iterator<IVecInt> {
private final IVec<IVecInt> content;
private int index;
public MemoryProofKeeperVecIterator(IVecInt content){
this.index = 0;
this.content = new Vec<IVecInt>();
IVecInt current = new VecInt();
for (int i = 0 ; i < content.size() ; i++){
if (content.get(i) != 0){
current.push(content.get(i));
}
else{
this.content.push(current);
current.clear();
}
}
}
public boolean hasNext() {
return index == content.size();
}
public IVecInt next() {
return content.get(index++);
}
public void remove() {
}
}
package org.sat4j.minisat.proof;
import org.sat4j.minisat.IProof;
import org.sat4j.minisat.IProofDelegate;
import org.sat4j.minisat.core.Solver;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVecInt;
public final class NullProofDelegate implements IProofDelegate {
public NullProofDelegate(){}
public void deleted(IConstr gone) {}
public void beginChain (IConstr start){}
public int newClause(IVecInt vlits) {