Commit a6d684d2 authored by leberre's avatar leberre

Huge internal changes:

- Removed specific binary and ternary clause representations
- Removed associated ILits2 and ILits23 interfaces
- Removed class parameters for Solver and a few related classes.
- Removed unused classes such as the old VarOrder.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@310 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent bb66a105
......@@ -35,7 +35,7 @@ import org.sat4j.minisat.core.ILits;
* Window - Preferences - Java - Code Generation - Code and Comments
*/
public abstract class AbstractCardinalityDataStructure extends
AbstractDataStructureFactory<ILits> {
AbstractDataStructureFactory {
/**
*
......
......@@ -44,8 +44,8 @@ import org.sat4j.specs.IVecInt;
* @author leberre To change the template for this generated type comment go to
* Window&gt;Preferences&gt;Java&gt;Code Generation&gt;Code and Comments
*/
public abstract class AbstractDataStructureFactory<L extends ILits> implements
DataStructureFactory<L>, Serializable {
public abstract class AbstractDataStructureFactory implements
DataStructureFactory, Serializable {
/**
*
......@@ -74,13 +74,13 @@ public abstract class AbstractDataStructureFactory<L extends ILits> implements
return tmp;
}
protected L lits;
protected ILits lits;
protected AbstractDataStructureFactory() {
lits = createLits();
}
protected abstract L createLits();
protected abstract ILits createLits();
private final IVec<Propagatable> tmp = new Vec<Propagatable>();
......@@ -89,7 +89,7 @@ public abstract class AbstractDataStructureFactory<L extends ILits> implements
*
* @see org.sat4j.minisat.DataStructureFactory#createVocabulary()
*/
public L getVocabulary() {
public ILits getVocabulary() {
return lits;
}
......
......@@ -28,8 +28,8 @@
package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.cnf.CBClause;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.Propagatable;
......@@ -41,7 +41,7 @@ import org.sat4j.specs.IVecInt;
* @author parrain To change the template for this generated type comment go to
* Window - Preferences - Java - Code Generation - Code and Comments
*/
public class ClausalDataStructureCB extends AbstractDataStructureFactory<ILits> {
public class ClausalDataStructureCB extends AbstractDataStructureFactory {
private static final long serialVersionUID = 1L;
......@@ -72,7 +72,7 @@ public class ClausalDataStructureCB extends AbstractDataStructureFactory<ILits>
* @see org.sat4j.minisat.core.DataStructureFactory#createClause(org.sat4j.specs.VecInt)
*/
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = WLClause.sanityCheck(literals, getVocabulary(), solver);
IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
if (v == null)
return null;
return CBClause.brandNewClause(solver, getVocabulary(), v);
......
......@@ -27,10 +27,10 @@
*******************************************************************************/
package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.MixableCBClause;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.ContradictionException;
......@@ -41,7 +41,7 @@ import org.sat4j.specs.IVecInt;
* the database and uses Watched Literals Data structure for learned
* clauses.
*/
public class ClausalDataStructureCBWL extends AbstractDataStructureFactory<ILits> {
public class ClausalDataStructureCBWL extends AbstractDataStructureFactory {
private static final long serialVersionUID = 1L;
......@@ -51,7 +51,7 @@ public class ClausalDataStructureCBWL extends AbstractDataStructureFactory<ILits
* @see org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype.VecInt)
*/
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = WLClause.sanityCheck(literals, getVocabulary(), solver);
IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
if (v == null)
return null;
return MixableCBClause.brandNewClause(solver, getVocabulary(), v);
......
......@@ -27,10 +27,10 @@
*******************************************************************************/
package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.OriginalWLClause;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.ContradictionException;
......@@ -40,7 +40,7 @@ import org.sat4j.specs.IVecInt;
* @author leberre To change the template for this generated type comment go to
* Window - Preferences - Java - Code Generation - Code and Comments
*/
public class ClausalDataStructureWL extends AbstractDataStructureFactory<ILits> {
public class ClausalDataStructureWL extends AbstractDataStructureFactory {
private static final long serialVersionUID = 1L;
......@@ -50,7 +50,7 @@ public class ClausalDataStructureWL extends AbstractDataStructureFactory<ILits>
* @see org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype.VecInt)
*/
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = WLClause.sanityCheck(literals, getVocabulary(), solver);
IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
if (v == null)
return null;
return OriginalWLClause.brandNewClause(solver, getVocabulary(), v);
......
......@@ -27,19 +27,19 @@
*******************************************************************************/
package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.minisat.constraints.cnf.MixableCBClause;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
public class MixedDataStructureDanielCBWL extends MixedDataStructureDaniel {
public class MixedDataStructureDanielCBWL extends MixedDataStructureDanielWL {
private static final long serialVersionUID = 1L;
@Override
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = WLClause.sanityCheck(literals, getVocabulary(), solver);
IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
if (v == null)
return null;
return MixableCBClause.brandNewClause(solver, getVocabulary(), v);
......
......@@ -27,25 +27,38 @@
*******************************************************************************/
package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.constraints.cnf.Lits2;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.constraints.card.AtLeast;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.minisat.constraints.cnf.LearntBinaryClause;
import org.sat4j.minisat.constraints.cnf.LearntHTClause;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.OriginalBinaryClause;
import org.sat4j.minisat.constraints.cnf.OriginalHTClause;
import org.sat4j.minisat.constraints.cnf.UnitClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits2;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
/**
* @author leberre To change the template for this generated type comment go to
* Window&gt;Preferences&gt;Java&gt;Code Generation&gt;Code and Comments
* Uses specific data structure for cardinality constraints.
*
* @author leberre
*/
public class MixedDataStructureWithBinary extends AbstractDataStructureFactory<ILits2> {
public class MixedDataStructureDanielHT extends AbstractDataStructureFactory {
private static final long serialVersionUID = 1L;
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.DataStructureFactory#createCardinalityConstraint(org.sat4j.datatype.VecInt,
* int)
*/
@Override
public ILits2 createLits() {
return new Lits2();
public Constr createCardinalityConstraint(IVecInt literals, int degree)
throws ContradictionException {
return AtLeast.atLeastNew(solver, getVocabulary(), literals, degree);
}
/*
......@@ -53,33 +66,28 @@ public class MixedDataStructureWithBinary extends AbstractDataStructureFactory<I
*
* @see org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype.VecInt)
*/
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = WLClause.sanityCheck(literals, lits, solver);
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
if (v == null)
return null;
if (v.size() == 2) {
lits.binaryClauses(v.get(0), v.get(1));
return null;
}
return WLClause.brandNewClause(solver, lits, v);
if (v.size()==2) {
return OriginalBinaryClause.brandNewClause(solver, getVocabulary(), v);
}
return OriginalHTClause.brandNewClause(solver, getVocabulary(), v);
}
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.DataStructureFactory#learnContraint(org.sat4j.minisat.Constr)
*/
@Override
public void learnConstraint(Constr constr) {
if (constr.size() == 2) {
lits.binaryClauses(constr.get(0), constr.get(1));
// solver.getStats().learnedbinaryclauses++;
} else {
super.learnConstraint(constr);
}
public Constr createUnregisteredClause(IVecInt literals) {
if (literals.size()==1) {
return new UnitClause(literals.last());
}
if (literals.size()==2) {
return new LearntBinaryClause(literals,getVocabulary());
}
return new LearntHTClause(literals, getVocabulary());
}
public Constr createUnregisteredClause(IVecInt literals) {
return new LearntWLClause(literals, getVocabulary());
@Override
protected ILits createLits() {
return new Lits();
}
}
......@@ -28,10 +28,13 @@
package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.card.AtLeast;
import org.sat4j.minisat.constraints.cnf.Clauses;
import org.sat4j.minisat.constraints.cnf.LearntBinaryClause;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.OriginalBinaryClause;
import org.sat4j.minisat.constraints.cnf.OriginalWLClause;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.constraints.cnf.UnitClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.ContradictionException;
......@@ -41,7 +44,7 @@ import org.sat4j.specs.IVecInt;
* @author leberre To change the template for this generated type comment go to
* Window - Preferences - Java - Code Generation - Code and Comments
*/
public class MixedDataStructureDaniel extends AbstractDataStructureFactory<ILits> {
public class MixedDataStructureDanielWL extends AbstractDataStructureFactory {
private static final long serialVersionUID = 1L;
......@@ -63,13 +66,22 @@ public class MixedDataStructureDaniel extends AbstractDataStructureFactory<ILits
* @see org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype.VecInt)
*/
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = WLClause.sanityCheck(literals, getVocabulary(), solver);
IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
if (v == null)
return null;
if (v.size()==2) {
return OriginalBinaryClause.brandNewClause(solver, getVocabulary(), v);
}
return OriginalWLClause.brandNewClause(solver, getVocabulary(), v);
}
public Constr createUnregisteredClause(IVecInt literals) {
if (literals.size()==1) {
return new UnitClause(literals.last());
}
if (literals.size()==2) {
return new LearntBinaryClause(literals,getVocabulary());
}
return new LearntWLClause(literals, getVocabulary());
}
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*
*******************************************************************************/
package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.constraints.cnf.Lits23;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits23;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
/**
* @author leberre To change the template for this generated type comment go to
* Window&gt;Preferences&gt;Java&gt;Code Generation&gt;Code and Comments
*/
public class MixedDataStructureWithBinaryAndTernary extends
AbstractDataStructureFactory<ILits23> {
private static final long serialVersionUID = 1L;
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype.VecInt)
*/
public Constr createClause(IVecInt literals) throws ContradictionException {
IVecInt v = WLClause.sanityCheck(literals, lits, solver);
if (v == null)
return null;
if (v.size() == 2) {
lits.binaryClauses(v.get(0), v.get(1));
return null;
}
if (v.size() == 3) {
lits.ternaryClauses(v.get(0), v.get(1), v.get(2));
return null;
}
return WLClause.brandNewClause(solver, lits, v);
}
/*
* (non-Javadoc)
*
* @see org.sat4j.minisat.DataStructureFactory#learnContraint(org.sat4j.minisat.Constr)
*/
@Override
public void learnConstraint(Constr constr) {
if (constr.size() == 2) {
lits.binaryClauses(constr.get(0), constr.get(1));
// solver.getStats().learnedbinaryclauses++;
} else if (constr.size() == 3) {
lits.ternaryClauses(constr.get(0), constr.get(1), constr.get(2));
// solver.getStats().learnedternaryclauses++;
} else {
super.learnConstraint(constr);
}
}
@Override
protected ILits23 createLits() {
return new Lits23();
}
public Constr createUnregisteredClause(IVecInt literals) {
return new LearntWLClause(literals, getVocabulary());
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.core.LiteralsUtils.neg;
import java.io.Serializable;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.UnitPropagationListener;
import org.sat4j.specs.IVecInt;
/**
* Data structure for binary clause.
*
* @author leberre
*/
public abstract class BinaryClause implements Constr, Serializable {
private static final long serialVersionUID = 1L;
private double activity;
private final ILits voc;
private int head;
private int tail;
/**
* Creates a new basic clause
*
* @param voc
* the vocabulary of the formula
* @param ps
* A VecInt that WILL BE EMPTY after calling that method.
*/
public BinaryClause(IVecInt ps, ILits voc) {
assert ps.size() == 2;
head = ps.get(0);
tail = ps.get(1);
this.voc = voc;
activity = 0;
}
/*
* (non-Javadoc)
*
* @see Constr#calcReason(Solver, Lit, Vec)
*/
public void calcReason(int p, IVecInt outReason) {
if (voc.isFalsified(head)) {
outReason.push(neg(head));
}
if (voc.isFalsified(tail)) {
outReason.push(neg(tail));
}
}
/*
* (non-Javadoc)
*
* @see Constr#remove(Solver)
*/
public void remove() {
voc.watches(neg(head)).remove(this);
voc.watches(neg(tail)).remove(this);
}
/*
* (non-Javadoc)
*
* @see Constr#simplify(Solver)
*/
public boolean simplify() {
if (voc.isSatisfied(head) || voc.isSatisfied(tail)) {
return true;
}
return false;
}
public boolean propagate(UnitPropagationListener s, int p) {
voc.watch(p, this);
if (head == neg(p)) {
return s.enqueue(tail, this);
}
assert tail == neg(p);
return s.enqueue(head, this);
}
/*
* For learnt clauses only @author leberre
*/
public boolean locked() {
return voc.getReason(head) == this || voc.getReason(tail) == this;
}
/**
* @return the activity of the clause
*/
public double getActivity() {
return activity;
}
@Override
public String toString() {
StringBuffer stb = new StringBuffer();
stb.append(Lits.toString(head));
stb.append("["); //$NON-NLS-1$
stb.append(voc.valueToString(head));
stb.append("]"); //$NON-NLS-1$
stb.append(" "); //$NON-NLS-1$
stb.append(Lits.toString(tail));
stb.append("["); //$NON-NLS-1$
stb.append(voc.valueToString(tail));
stb.append("]"); //$NON-NLS-1$
return stb.toString();
}
/**
* Retourne le ieme literal de la clause. Attention, cet ordre change durant
* la recherche.
*
* @param i
* the index of the literal
* @return the literal
*/
public int get(int i) {
if (i == 0)
return head;
assert i == 1;
return tail;
}
/**
* @param claInc
*/
public void incActivity(double claInc) {
activity += claInc;
}
/**
* @param d
*/
public void rescaleBy(double d) {
activity *= d;
}
public int size() {
return 2;
}
public void assertConstraint(UnitPropagationListener s) {
boolean ret;
if (voc.isUnassigned(head)) {
ret = s.enqueue(head, this);
} else {
assert voc.isUnassigned(tail);
ret = s.enqueue(tail, this);
}
assert ret;
}
public ILits getVocabulary() {
return voc;
}
public int[] getLits() {
int[] tmp = new int[2];
tmp[0] = head;
tmp[1] = tail;
return tmp;
}
@Override
public boolean equals(Object obj) {
if (obj == null)
return false;
try {
BinaryClause wcl = (BinaryClause) obj;
if (wcl.head != head || wcl.tail != tail) {
return false;
}
return true;
} catch (ClassCastException e) {
return false;
}
}
@Override
public int hashCode() {
long sum = head + tail;
return (int) sum / 2;
}
public void register() {
voc.watch(neg(head), this);
voc.watch(neg(tail), this);
}
}
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*