Skip to content
Snippets Groups Projects
Commit d3b45da7 authored by Daniel Plagge's avatar Daniel Plagge
Browse files

Kodkod: Added optional use of SAT4J if Minisat is not usable

parent 06c6477c
Branches
No related tags found
No related merge requests found
......@@ -10,6 +10,7 @@
<property name="main.class" value="de.stups.probkodkod.KodkodInteraction"/>
<property name="lib" value="lib"/>
<property name="kodkod" value="${lib}/kodkod.jar"/>
<property name="sat4j" value="${lib}/org.sat4j.core.jar"/>
<property name="prolog" value="${lib}/prolog.jar"/>
<property name="junit" value="${lib}/junit-4.8.2.jar"/>
<property name="uptodate" value="uptodate"/>
......@@ -20,18 +21,21 @@
<target name="init">
<mkdir dir="${build}"/>
<mkdir dir="${jar}"/>
</target>
<target name="is_uptodate">
<uptodate property="parser.uptodate">
<srcfiles dir="${src}" includes="*.grammar"/>
<mapper type="merge" to="../${parser}/${uptodate}"/>
</uptodate>
</target>
<target name="clear">
<target name="clear" depends="init">
<delete> <fileset dir="${build}" includes="**/*"/> </delete>
<delete includeemptydirs="yes"> <fileset dir="${parser}" includes="**/*"/> </delete>
</target>
<target name="parser" depends="init" unless="parser.uptodate" description="Generate the parser classes">
<target name="parser" depends="is_uptodate,init" unless="parser.uptodate" description="Generate the parser classes">
<delete> <fileset dir="${parser}" includes="**/*"/> </delete>
<sablecc src="${src}" includes="*.grammar" outputdirectory="${parser}"/>
<touch file="${parser}/${uptodate}"/>
......@@ -74,6 +78,7 @@
<classpath location="${kodkod}"/>
<classpath location="${prolog}"/>
<classpath location="${junit}"/>
<classpath location="${sat4j}"/>
<classpath location="${jar}"/>
<jvmarg value="-Djava.library.path=${lib}"/>
<formatter type="plain" usefile="true" />
......
File added
......@@ -21,6 +21,8 @@ import de.prob.prolog.output.IPrologTermOutput;
*
*/
public class KodkodSession {
private final SATFactory SOLVER = SolverChecker.determineSatFactory();
private final Logger logger = Logger.getLogger(KodkodSession.class
.getName());
private final Map<String, ImmutableProblem> problems = new HashMap<String, ImmutableProblem>();
......@@ -33,7 +35,7 @@ public class KodkodSession {
problems.put(id, problem);
final Solver solver = new Solver();
solver.options().setSolver(SATFactory.MiniSat);
solver.options().setSolver(SOLVER);
solver.options().setSymmetryBreaking(0);
final Integer bitwidth = problem.getBitwidth();
if (bitwidth != null) {
......
/**
*
*/
package de.stups.probkodkod;
import java.util.HashMap;
import java.util.Map;
import java.util.logging.Level;
import java.util.logging.Logger;
import kodkod.ast.Formula;
import kodkod.ast.IntConstant;
import kodkod.ast.Relation;
import kodkod.engine.Solver;
import kodkod.engine.satlab.SATFactory;
import kodkod.instance.Bounds;
import kodkod.instance.Universe;
/**
* Here we determine if we use Minisat or SAT4J as back-end. We do this by
* trying to load minisat.
*
* @author plagge
*/
public class SolverChecker {
private static final Logger LOGGER = Logger
.getLogger("de.stups.probkodkod");
private static final SATFactory[] FACTORIES = { SATFactory.MiniSat,
SATFactory.DefaultSAT4J };
public static SATFactory determineSatFactory() {
Map<String, Throwable> throwables = new HashMap<String, Throwable>();
for (final SATFactory factory : FACTORIES) {
try {
check(factory);
// the factory seems to work, we use it
LOGGER.info("Using SAT solver back-end: " + factory);
return factory;
} catch (Throwable t) {
// the factory does not work, we store the stack-trace for the
// case that no solvers are found
throwables.put(factory.toString(), t);
}
}
LOGGER.severe("No SAT solver back-end found.");
for (final Map.Entry<String, Throwable> entry : throwables.entrySet()) {
final String msg = "Error when trying to use solver: "
+ entry.getKey();
LOGGER.log(Level.SEVERE, msg, entry.getValue());
}
throw new Error("No SAT solver back-end for Kodkod found.");
}
private static void check(SATFactory factory) {
final Solver solver = new Solver();
solver.options().setSolver(factory);
final Universe universe = new Universe("a", "b");
final Relation relation = Relation.unary("relation");
final Formula formula = relation.count().eq(IntConstant.constant(2));
final Bounds bounds = new Bounds(universe);
bounds.bound(relation, universe.factory().allOf(1));
solver.solve(formula, bounds);
}
}
......@@ -10,7 +10,6 @@ import kodkod.ast.IntConstant;
import kodkod.ast.Relation;
import kodkod.engine.Solution;
import kodkod.engine.Solver;
import kodkod.engine.satlab.SATFactory;
import kodkod.instance.Bounds;
import kodkod.instance.Instance;
import kodkod.instance.Tuple;
......@@ -46,7 +45,7 @@ public class NegativeIntTest {
bounds.bound(x, factory.allOf(1));
final Formula formula = x.sum().eq(IntConstant.constant(value));
final Solver solver = new Solver();
solver.options().setSolver(SATFactory.MiniSat);
solver.options().setSolver(SolverChecker.determineSatFactory());
solver.options().setBitwidth(5);
final Iterator<Solution> iterator = solver.solveAll(formula, bounds);
Assert.assertTrue("solution expected", iterator.hasNext());
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment