Commit d1efd522 authored by leberre's avatar leberre

Moved Constr, propagatable and MandatoryLiteralListener from core to specs...

Moved Constr, propagatable and MandatoryLiteralListener from core to specs package to avoid cyclic dependencies.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2143 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 17d406f3
......@@ -32,14 +32,14 @@ package org.sat4j.minisat.constraints;
import java.io.Serializable;
import org.sat4j.core.Vec;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.Learner;
import org.sat4j.minisat.core.Propagatable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -31,7 +31,7 @@ package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.card.AtLeast;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
......
......@@ -32,7 +32,7 @@ package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.card.MaxWatchCard;
import org.sat4j.minisat.constraints.card.MinWatchCard;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
......
......@@ -31,7 +31,7 @@ package org.sat4j.minisat.constraints;
import org.sat4j.minisat.constraints.card.MinWatchCard;
import org.sat4j.minisat.constraints.cnf.LearntWLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
......
......@@ -35,8 +35,8 @@ 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.UnitClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
......
......@@ -37,8 +37,8 @@ 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.ILits;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
......
......@@ -37,8 +37,8 @@ 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.UnitClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
......
......@@ -36,8 +36,8 @@ 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.UnitClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
......
......@@ -34,14 +34,14 @@ import java.io.Serializable;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.UnitClauses;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.minisat.core.Propagatable;
import org.sat4j.minisat.core.Undoable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -34,13 +34,13 @@ import java.math.BigInteger;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.UnitClauses;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.minisat.core.Propagatable;
import org.sat4j.minisat.core.Undoable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
public final class MaxWatchCard implements Propagatable, Constr, Undoable,
......
......@@ -33,13 +33,13 @@ import java.io.Serializable;
import org.sat4j.minisat.constraints.cnf.Lits;
import org.sat4j.minisat.constraints.cnf.UnitClauses;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.minisat.core.Propagatable;
import org.sat4j.minisat.core.Undoable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
public class MinWatchCard implements Propagatable, Constr, Undoable,
......
......@@ -33,11 +33,11 @@ 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.MandatoryLiteralListener;
import org.sat4j.minisat.core.Propagatable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -33,10 +33,10 @@ 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.Propagatable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -32,8 +32,8 @@ package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.core.LiteralsUtils.neg;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
/**
* @author daniel
......
......@@ -30,8 +30,8 @@
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
public final class LearntWLClause extends WLClause {
......
......@@ -33,11 +33,11 @@ import java.io.Serializable;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.core.Vec;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.Propagatable;
import org.sat4j.minisat.core.Undoable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.Propagatable;
/**
* @author laihem
......
......@@ -32,8 +32,8 @@ package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.core.LiteralsUtils.neg;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -30,8 +30,8 @@
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.UnitPropagationListener;
public final class OriginalWLClause extends WLClause {
......
......@@ -30,10 +30,10 @@
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -29,9 +29,9 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.MandatoryLiteralListener;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -31,10 +31,10 @@ package org.sat4j.minisat.constraints.cnf;
import java.io.Serializable;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.Propagatable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -32,6 +32,8 @@ package org.sat4j.minisat.core;
import java.io.Serializable;
import java.util.Comparator;
import org.sat4j.specs.Constr;
/**
* Utility class to sort the constraints according to their activity.
*
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
final class ActivityLCDS implements LearnedConstraintsDeletionStrategy {
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.specs.Constr;
/**
* @author leberre
*/
......
......@@ -32,6 +32,7 @@ package org.sat4j.minisat.core;
import static org.sat4j.core.LiteralsUtils.toInternal;
import org.sat4j.core.VecInt;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
......
......@@ -29,9 +29,11 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.UnitPropagationListener;
/**
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.specs.Constr;
class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
/**
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
class GlucoseLCDS<D extends DataStructureFactory> implements
......
......@@ -29,7 +29,9 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.Propagatable;
/**
* That interface manages the solver's internal vocabulary. Everything related
......
......@@ -31,6 +31,7 @@ package org.sat4j.minisat.core;
import java.io.Serializable;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
/**
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.specs.Constr;
/**
* Provide the learning service.
*
......
......@@ -31,6 +31,8 @@ package org.sat4j.minisat.core;
import java.io.Serializable;
import org.sat4j.specs.Constr;
/**
* Implementation of the strategy design pattern for allowing various learning
* schemes.
......
package org.sat4j.minisat.core;
/**
* Callback method called when a mandatory literal is found in a constraint.
*
* @author leberre
*
*/
public interface MandatoryLiteralListener {
/**
*
* @param p
* a literal in internal representation.
*/
void isMandatory(int p);
}
......@@ -31,6 +31,8 @@ package org.sat4j.minisat.core;
import java.io.Serializable;
import org.sat4j.specs.Constr;
/**
* Utility class to be used to return the two results of a conflict analysis.
*
......
......@@ -31,6 +31,8 @@ package org.sat4j.minisat.core;
import java.io.Serializable;
import org.sat4j.specs.Constr;
/**
* Abstraction allowing to choose various restarts strategies.
*
......
......@@ -52,6 +52,7 @@ import org.sat4j.core.ConstrGroup;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
import org.sat4j.specs.Constr;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ILogAble;
......@@ -61,6 +62,7 @@ import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
import org.sat4j.specs.Lbool;
import org.sat4j.specs.Propagatable;
import org.sat4j.specs.SearchListener;
import org.sat4j.specs.TimeoutException;
import org.sat4j.specs.UnitClauseProvider;
......
......@@ -33,7 +33,10 @@ import static org.sat4j.core.LiteralsUtils.toDimacs;
import static org.sat4j.core.LiteralsUtils.toInternal;
import static org.sat4j.core.LiteralsUtils.var;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
import org.sat4j.specs.MandatoryLiteralListener;
import org.sat4j.specs.Propagatable;
/**
* Watcher based implementation of the model minimization strategy to compute a
......
......@@ -29,11 +29,11 @@
*******************************************************************************/
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.specs.Constr;
/**
* An abstract learning strategy.
......
......@@ -29,10 +29,10 @@
*******************************************************************************/
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.Solver;
import org.sat4j.specs.Constr;
/**
* Learn clauses with a great number of active variables.
......
......@@ -30,8 +30,8 @@
package org.sat4j.minisat.learning;
import org.sat4j.minisat.constraints.cnf.WLClause;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.specs.Constr;
/**
* The solver only records among all the constraints only the clauses.
......
......@@ -29,8 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.specs.Constr;
/**
* A learning scheme for learning constraints of size smaller than a given
......
......@@ -29,13 +29,13 @@
*******************************************************************************/
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.core.SolverStats;
import org.sat4j.minisat.core.VarActivityListener;
import org.sat4j.specs.Constr;
/**
* Learn only clauses which size is smaller than a percentage of the number of
......
......@@ -29,9 +29,9 @@
*******************************************************************************/
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.Solver;
import org.sat4j.specs.Constr;
/**
* MiniSAT learning scheme.
......
......@@ -29,8 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.specs.Constr;
/**
* Allows MiniSAT to do backjumping without learning. The literals appearing in
......
......@@ -29,8 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.specs.Constr;
/**
* Allows MiniSAT to do backjumping without learning. The literals appearing in
......
......@@ -29,8 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.learning;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.specs.Constr;
/**
* Selects the constraints to learn according to its length as a percentage of
......
......@@ -29,10 +29,10 @@
*******************************************************************************/
package org.sat4j.minisat.restarts;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.SolverStats;
import org.sat4j.specs.Constr;
/**
* Rapid restart strategy presented by Armin Biere during it's SAT 07 invited
......
......@@ -29,10 +29,10 @@
*******************************************************************************/
package org.sat4j.minisat.restarts;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.SolverStats;
import org.sat4j.specs.Constr;
public class FixedPeriodRestarts implements RestartStrategy {
......
......@@ -30,10 +30,10 @@
package org.sat4j.minisat.restarts;
import org.sat4j.minisat.core.CircularBuffer;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.SolverStats;
import org.sat4j.specs.Constr;
/**
* Dynamic restart strategy of Glucose 2.1 as presented in Refining restarts
......
......@@ -29,10 +29,10 @@
*******************************************************************************/
package org.sat4j.minisat.restarts;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.SolverStats;
import org.sat4j.specs.Constr;
/**
* Luby series
......
......@@ -29,10 +29,10 @@
*******************************************************************************/
package org.sat4j.minisat.restarts;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.SolverStats;
import org.sat4j.specs.Constr;
/**
* Minisat original restart strategy.
......
......@@ -29,10 +29,10 @@
*******************************************************************************/
package org.sat4j.minisat.restarts;
import org.sat4j.minisat.core.Constr;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.SolverStats;
import org.sat4j.specs.Constr;
/**
* Disable restarts in the solver.
......
......@@ -27,11 +27,8 @@
* Contributors:
* CRIL - initial API and implementation
*******************************************************************************/
package org.sat4j.minisat.core;
package org.sat4j.specs;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.UnitPropagationListener;
/*
* Created on 16 oct. 2003
......
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
*
* 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