diff --git a/src/main/java/de/stups/probkodkod/KodkodAnalysis.java b/src/main/java/de/stups/probkodkod/KodkodAnalysis.java
index 454fd7c157f78cb8259ae9f1d38b901dc7799515..43bbe1429a84d14e5293198dc22d28797fc6e85d 100644
--- a/src/main/java/de/stups/probkodkod/KodkodAnalysis.java
+++ b/src/main/java/de/stups/probkodkod/KodkodAnalysis.java
@@ -10,24 +10,6 @@ import java.util.List;
import java.util.Map;
import java.util.Stack;
-import kodkod.ast.Decl;
-import kodkod.ast.Decls;
-import kodkod.ast.Expression;
-import kodkod.ast.Formula;
-import kodkod.ast.IntConstant;
-import kodkod.ast.IntExpression;
-import kodkod.ast.Relation;
-import kodkod.ast.Variable;
-import kodkod.ast.operator.ExprCompOperator;
-import kodkod.ast.operator.ExprOperator;
-import kodkod.ast.operator.FormulaOperator;
-import kodkod.ast.operator.IntCastOperator;
-import kodkod.ast.operator.IntCompOperator;
-import kodkod.ast.operator.IntOperator;
-import kodkod.ast.operator.Multiplicity;
-import kodkod.ast.operator.Quantifier;
-import kodkod.instance.TupleSet;
-import kodkod.instance.Universe;
import de.prob.prolog.output.IPrologTermOutput;
import de.stups.probkodkod.parser.analysis.DepthFirstAdapter;
import de.stups.probkodkod.parser.node.AAddIntexprBinop;
@@ -128,6 +110,24 @@ import de.stups.probkodkod.parser.node.TIdentifier;
import de.stups.probkodkod.parser.node.TNumber;
import de.stups.probkodkod.types.TupleType;
import de.stups.probkodkod.types.Type;
+import kodkod.ast.Decl;
+import kodkod.ast.Decls;
+import kodkod.ast.Expression;
+import kodkod.ast.Formula;
+import kodkod.ast.IntConstant;
+import kodkod.ast.IntExpression;
+import kodkod.ast.Relation;
+import kodkod.ast.Variable;
+import kodkod.ast.operator.ExprCompOperator;
+import kodkod.ast.operator.ExprOperator;
+import kodkod.ast.operator.FormulaOperator;
+import kodkod.ast.operator.IntCastOperator;
+import kodkod.ast.operator.IntCompOperator;
+import kodkod.ast.operator.IntOperator;
+import kodkod.ast.operator.Multiplicity;
+import kodkod.ast.operator.Quantifier;
+import kodkod.instance.TupleSet;
+import kodkod.instance.Universe;
/**
* This is a visitor for the syntax tree of an input to the program.
@@ -160,53 +160,41 @@ public class KodkodAnalysis extends DepthFirstAdapter {
COMPOPS.put(AInLogopRel.class.getName(), ExprCompOperator.SUBSET);
COMPOPS.put(AEqualsLogopRel.class.getName(), ExprCompOperator.EQUALS);
BINFORMOPS.put(AOrLogopBinary.class.getName(), FormulaOperator.OR);
- BINFORMOPS.put(AImpliesLogopBinary.class.getName(),
- FormulaOperator.IMPLIES);
+ BINFORMOPS.put(AImpliesLogopBinary.class.getName(), FormulaOperator.IMPLIES);
BINFORMOPS.put(AIffLogopBinary.class.getName(), FormulaOperator.IFF);
QUANTIFIERS.put(AAllQuantifier.class.getName(), Quantifier.ALL);
QUANTIFIERS.put(AExistsQuantifier.class.getName(), Quantifier.SOME);
- QUANTIFIER_FOP.put(AAllQuantifier.class.getName(),
- FormulaOperator.IMPLIES);
- QUANTIFIER_FOP.put(AExistsQuantifier.class.getName(),
- FormulaOperator.AND);
+ QUANTIFIER_FOP.put(AAllQuantifier.class.getName(), FormulaOperator.IMPLIES);
+ QUANTIFIER_FOP.put(AExistsQuantifier.class.getName(), FormulaOperator.AND);
- MULTIEXPROPS.put(AProductExprMultop.class.getName(),
- ExprOperator.PRODUCT);
+ MULTIEXPROPS.put(AProductExprMultop.class.getName(), ExprOperator.PRODUCT);
MULTIEXPROPS.put(AUnionExprMultop.class.getName(), ExprOperator.UNION);
- MULTIEXPROPS.put(AInterExprMultop.class.getName(),
- ExprOperator.INTERSECTION);
+ MULTIEXPROPS.put(AInterExprMultop.class.getName(), ExprOperator.INTERSECTION);
BINEXPROPS.put(ADiffExprBinop.class.getName(), ExprOperator.DIFFERENCE);
BINEXPROPS.put(AJoinExprBinop.class.getName(), ExprOperator.JOIN);
- BINEXPROPS.put(AOverwriteExprBinop.class.getName(),
- ExprOperator.OVERRIDE);
+ BINEXPROPS.put(AOverwriteExprBinop.class.getName(), ExprOperator.OVERRIDE);
UNEXPROPS.put(AClosureExprUnop.class.getName(), ExprOperator.CLOSURE);
- UNEXPROPS.put(ATransposeExprUnop.class.getName(),
- ExprOperator.TRANSPOSE);
- MULTIPLICITIES
- .put(ALoneMultiplicity.class.getName(), Multiplicity.LONE);
+ UNEXPROPS.put(ATransposeExprUnop.class.getName(), ExprOperator.TRANSPOSE);
+ MULTIPLICITIES.put(ALoneMultiplicity.class.getName(), Multiplicity.LONE);
MULTIPLICITIES.put(ANoMultiplicity.class.getName(), Multiplicity.NO);
MULTIPLICITIES.put(AOneMultiplicity.class.getName(), Multiplicity.ONE);
MULTIPLICITIES.put(ASetMultiplicity.class.getName(), Multiplicity.SET);
- MULTIPLICITIES
- .put(ASomeMultiplicity.class.getName(), Multiplicity.SOME);
+ MULTIPLICITIES.put(ASomeMultiplicity.class.getName(), Multiplicity.SOME);
CONSTEXPR.put(AEmptyExprConst.class.getName(), Expression.NONE);
CONSTEXPR.put(AIdenExprConst.class.getName(), Expression.IDEN);
CONSTEXPR.put(AUnivExprConst.class.getName(), Expression.UNIV);
BININTEXPROPS.put(AAddIntexprBinop.class.getName(), IntOperator.PLUS);
BININTEXPROPS.put(ASubIntexprBinop.class.getName(), IntOperator.MINUS);
- BININTEXPROPS.put(AMulIntexprBinop.class.getName(),
- IntOperator.MULTIPLY);
+ BININTEXPROPS.put(AMulIntexprBinop.class.getName(), IntOperator.MULTIPLY);
BININTEXPROPS.put(ADivIntexprBinop.class.getName(), IntOperator.DIVIDE);
BININTEXPROPS.put(AModIntexprBinop.class.getName(), IntOperator.MODULO);
BININTCOMPS.put(AEqualsIntCompOp.class.getName(), IntCompOperator.EQ);
BININTCOMPS.put(AGreaterIntCompOp.class.getName(), IntCompOperator.GT);
- BININTCOMPS.put(AGreaterequalIntCompOp.class.getName(),
- IntCompOperator.GTE);
+ BININTCOMPS.put(AGreaterequalIntCompOp.class.getName(), IntCompOperator.GTE);
BININTCOMPS.put(ALesserIntCompOp.class.getName(), IntCompOperator.LT);
- BININTCOMPS.put(ALesserequalIntCompOp.class.getName(),
- IntCompOperator.LTE);
+ BININTCOMPS.put(ALesserequalIntCompOp.class.getName(), IntCompOperator.LTE);
INTCASTS.put(APow2ExprCast.class.getName(), IntCastOperator.BITSETCAST);
INTCASTS.put(AIntsetExprCast.class.getName(), IntCastOperator.INTCAST);
@@ -222,8 +210,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
private final Stack<IntExpression> intExpressionStack = new Stack<IntExpression>();
private Map<String, Expression> variables = new HashMap<String, Expression>();
- public KodkodAnalysis(final KodkodSession session,
- final IPrologTermOutput pto) {
+ public KodkodAnalysis(final KodkodSession session, final IPrologTermOutput pto) {
this.session = session;
this.pto = pto;
}
@@ -254,7 +241,9 @@ public class KodkodAnalysis extends DepthFirstAdapter {
problem.setFormula(formulaStack.pop());
long timeout = Long.parseLong(node.getTimeout().getText());
- session.addProblem(problem.createImmutable(), timeout);
+ int symmetry = Integer.parseInt(node.getSymmetry().getText());
+ SATSolver sat = SATSolver.valueOf(node.getSatsolver().getText());
+ session.addProblem(problem.createImmutable(), timeout, symmetry, sat);
}
private void registerTypes(final Collection<PType> types) {
@@ -268,8 +257,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final AIntsType type = (AIntsType) ptype;
addIntegerType(type);
} else
- throw new IllegalStateException("unexpected type case "
- + ptype.getClass().getName());
+ throw new IllegalStateException("unexpected type case " + ptype.getClass().getName());
}
}
@@ -283,9 +271,9 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final ImmutableProblem problem = session.getProblem(problemId);
if (problem != null) {
final boolean signum = getSignum(node.getReqtype());
- int size = extractInt(node.getSize()); // the maximum number of solutions to be computed
- final Map<String, TupleSet> args = extractArguments(
- node.getArguments(), problem);
+ int size = extractInt(node.getSize()); // the maximum number of
+ // solutions to be computed
+ final Map<String, TupleSet> args = extractArguments(node.getArguments(), problem);
session.request(problem, signum, args);
session.writeNextSolutions(problem, size, pto);
} else {
@@ -301,7 +289,9 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final String id = extractIdentifier(node.getProblem());
final ImmutableProblem problem = session.getProblem(id);
if (problem != null) {
- final int size = extractInt(node.getSize()); // the maximum number of solutions to be computed
+ final int size = extractInt(node.getSize()); // the maximum number
+ // of solutions to
+ // be computed
session.writeNextSolutions(problem, size, pto);
}
}
@@ -319,16 +309,14 @@ public class KodkodAnalysis extends DepthFirstAdapter {
session.reset();
}
- private Map<String, TupleSet> extractArguments(final List<PArgument> args,
- final ImmutableProblem problem) {
+ private Map<String, TupleSet> extractArguments(final List<PArgument> args, final ImmutableProblem problem) {
final Map<String, TupleSet> result = new HashMap<String, TupleSet>();
final Universe universe = problem.getUniverse();
for (final PArgument parg : args) {
final AArgument arg = (AArgument) parg;
final String id = extractIdentifier(arg.getIdentifier());
final RelationInfo info = problem.lookupRelationInfo(id);
- final TupleSet tupleSet = extractTuples(universe,
- info.getTupleType(), arg.getTuples());
+ final TupleSet tupleSet = extractTuples(universe, info.getTupleType(), arg.getTuples());
result.put(id, tupleSet);
}
return result;
@@ -357,8 +345,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final String name = node.getLogopRel().getClass().getName();
final ExprCompOperator op = COMPOPS.get(name);
if (op == null)
- throw new IllegalStateException("Unexpected relation operator "
- + name);
+ throw new IllegalStateException("Unexpected relation operator " + name);
final Expression b = expressionStack.pop();
final Expression a = expressionStack.pop();
formulaStack.push(a.compare(op, b));
@@ -412,10 +399,8 @@ public class KodkodAnalysis extends DepthFirstAdapter {
variables = new HashMap<String, Expression>(variables);
final Declaration decls = extractDecls(node.getDecls());
node.getFormula().apply(this);
- final Formula formula = decls.applyFormula(formulaStack.pop(),
- formulaOp);
- final Formula quantify = formula.quantify(quantifier,
- decls.getDeclarations());
+ final Formula formula = decls.applyFormula(formulaStack.pop(), formulaOp);
+ final Formula quantify = formula.quantify(quantifier, decls.getDeclarations());
formulaStack.push(quantify);
variables = oldVars;
}
@@ -425,8 +410,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final String name = node.getIntCompOp().getClass().getName();
final IntCompOperator op = BININTCOMPS.get(name);
if (op == null)
- throw new IllegalStateException(
- "Unexpected integer comparision operator " + name);
+ throw new IllegalStateException("Unexpected integer comparision operator " + name);
final IntExpression b = intExpressionStack.pop();
final IntExpression a = intExpressionStack.pop();
formulaStack.push(a.compare(op, b));
@@ -446,8 +430,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
} else if (op instanceof APartialLogopFunction) {
formula = rel.partialFunction(domain, range);
} else
- throw new IllegalStateException("unexpected function operator "
- + op.getClass().getName());
+ throw new IllegalStateException("unexpected function operator " + op.getClass().getName());
} else {
final Multiplicity mult;
if (op instanceof ATotalLogopFunction) {
@@ -455,8 +438,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
} else if (op instanceof APartialLogopFunction) {
mult = Multiplicity.LONE;
} else
- throw new IllegalStateException("unexpected function operator "
- + op.getClass().getName());
+ throw new IllegalStateException("unexpected function operator " + op.getClass().getName());
final Variable v = Variable.nary("__func", domain.arity());
final Decl decl = v.declare(Multiplicity.ONE, domain);
final Formula subset = obj.in(domain.product(range));
@@ -553,8 +535,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final String castName = node.getExprCast().getClass().getName();
final IntCastOperator op = INTCASTS.get(castName);
if (op == null)
- throw new IllegalStateException("Unexpected integer cast operator "
- + castName);
+ throw new IllegalStateException("Unexpected integer cast operator " + castName);
expressionStack.push(integer.cast(op));
}
@@ -573,13 +554,11 @@ public class KodkodAnalysis extends DepthFirstAdapter {
}
@Override
- public void outABinaryInnerintexpression(
- final ABinaryInnerintexpression node) {
+ public void outABinaryInnerintexpression(final ABinaryInnerintexpression node) {
final String name = node.getIntexprBinop().getClass().getName();
final IntOperator op = BININTEXPROPS.get(name);
if (op == null)
- throw new IllegalStateException("Unexpected integer operator "
- + name);
+ throw new IllegalStateException("Unexpected integer operator " + name);
final IntExpression b = intExpressionStack.pop();
final IntExpression a = intExpressionStack.pop();
intExpressionStack.push(a.compose(op, b));
@@ -596,8 +575,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
variables = new HashMap<String, Expression>(variables);
final Declaration decls = extractDecls(node.getDecls());
node.getFormula().apply(this);
- final Formula formula = decls.applyFormula(formulaStack.pop(),
- FormulaOperator.AND);
+ final Formula formula = decls.applyFormula(formulaStack.pop(), FormulaOperator.AND);
expressionStack.push(formula.comprehension(decls.getDeclarations()));
variables = oldVars;
}
@@ -618,8 +596,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final Multiplicity multiplicity = MULTIPLICITIES.get(mname);
if (multiplicity == null)
- throw new IllegalStateException("Unexpected multiplicity "
- + mname);
+ throw new IllegalStateException("Unexpected multiplicity " + mname);
if (arity > 1 && Multiplicity.ONE.equals(multiplicity)) {
createRelationDecl(id, arity, expression, declaration);
} else {
@@ -629,19 +606,17 @@ public class KodkodAnalysis extends DepthFirstAdapter {
node = cons.getDecls();
}
if (declaration.isEmpty())
- throw new IllegalStateException(
- "no declarations in quantified formula");
+ throw new IllegalStateException("no declarations in quantified formula");
return declaration;
}
- private void createRelationDecl(final String id, final int arity,
- Expression expression, final Declaration declaration) {
+ private void createRelationDecl(final String id, final int arity, Expression expression,
+ final Declaration declaration) {
Expression substitution = null;
for (int p = 0; p < arity; p++) {
final String tmpId = id + "_#_" + p;
final Expression prj = expression.project(IntConstant.constant(p));
- final Decl tmpDecl = declare(tmpId, 1, Multiplicity.ONE, prj,
- declaration);
+ final Decl tmpDecl = declare(tmpId, 1, Multiplicity.ONE, prj, declaration);
final Variable tmpVar = tmpDecl.variable();
if (substitution == null) {
substitution = tmpVar;
@@ -653,8 +628,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
declaration.addFormula(substitution.in(expression));
}
- private Decl declare(final String id, final int arity,
- final Multiplicity multiplicity, final Expression expression,
+ private Decl declare(final String id, final int arity, final Multiplicity multiplicity, final Expression expression,
final Declaration declaration) {
final Variable variable = Variable.nary(id, arity);
variables.put(id, variable);
@@ -674,20 +648,17 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final Universe universe = problem.getUniverse();
final PTupleset tupleset = rel.getElements();
final TupleType tupleType = new TupleType(types, isSingleton);
- final TupleSet ptset = extractTupleSet(universe, tupleset,
- tupleType);
+ final TupleSet ptset = extractTupleSet(universe, tupleset, tupleType);
problem.addRelation(id, isExact, tupleType, ptset);
}
}
- private void checkSingletonForTypes(final String id,
- final boolean isSingleton, final Type[] types) {
+ private void checkSingletonForTypes(final String id, final boolean isSingleton, final Type[] types) {
if (!isSingleton) {
for (final Type type : types) {
if (type.oneValueNeedsCompleteTupleSet())
- throw new IllegalArgumentException("Relation " + id
- + " makes use of type " + type
- + " but is not declared as singleton");
+ throw new IllegalArgumentException(
+ "Relation " + id + " makes use of type " + type + " but is not declared as singleton");
}
}
}
@@ -699,9 +670,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
} else if (extsub instanceof ASubsetReltype) {
result = false;
} else
- throw new IllegalStateException(
- "unexpected relation type (exact/sub) "
- + extsub.getClass().getName());
+ throw new IllegalStateException("unexpected relation type (exact/sub) " + extsub.getClass().getName());
return result;
}
@@ -709,8 +678,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final APowpart pow2spec = (APowpart) relnode.getPow2();
final ABitpart bitsspec = (ABitpart) relnode.getIntatoms();
final String pow2Name = extractIdentifier(pow2spec.getId());
- final IntegerIntervall pow2Interval = new IntegerIntervall(
- extractInt(pow2spec.getLower()),
+ final IntegerIntervall pow2Interval = new IntegerIntervall(extractInt(pow2spec.getLower()),
extractInt(pow2spec.getUpper()));
final String bitsName;
final IntegerIntervall intsetInterval;
@@ -725,12 +693,10 @@ public class KodkodAnalysis extends DepthFirstAdapter {
intsetInterval = null;
}
- problem.registerIntegerTypes(pow2Name, bitsName, intsetInterval,
- pow2Interval);
+ problem.registerIntegerTypes(pow2Name, bitsName, intsetInterval, pow2Interval);
}
- private TupleSet extractTupleSet(final Universe universe,
- final PTupleset node, final TupleType tupleType) {
+ private TupleSet extractTupleSet(final Universe universe, final PTupleset node, final TupleType tupleType) {
final TupleSet result;
if (node == null) {
result = tupleType.createAllTuples(universe);
@@ -749,13 +715,12 @@ public class KodkodAnalysis extends DepthFirstAdapter {
return type;
}
- private TupleSet extractTuples(final Universe universe,
- final TupleType tupleType, final Collection<PTuple> ptuples) {
+ private TupleSet extractTuples(final Universe universe, final TupleType tupleType,
+ final Collection<PTuple> ptuples) {
if (tupleType.isSingleton()) {
if (ptuples.size() != 1)
throw new IllegalArgumentException(
- "singleton type expects exactly one element, but there were "
- + ptuples.size());
+ "singleton type expects exactly one element, but there were " + ptuples.size());
}
final int arity = tupleType.getArity();
final Collection<int[]> tuples = new ArrayList<int[]>();
@@ -763,8 +728,8 @@ public class KodkodAnalysis extends DepthFirstAdapter {
final ATuple aTuple = (ATuple) pTuple;
final int[] numbers = extractNumbers(aTuple.getNumbers());
if (numbers.length != arity)
- throw new IllegalArgumentException("expected " + arity
- + "-tuple, but is a " + numbers.length + "-tuple");
+ throw new IllegalArgumentException(
+ "expected " + arity + "-tuple, but is a " + numbers.length + "-tuple");
tuples.add(numbers);
}
return tupleType.createTupleSet(universe, tuples);
@@ -794,8 +759,7 @@ public class KodkodAnalysis extends DepthFirstAdapter {
factor = -1;
numberNode = ((ANegZnumber) node).getNumber();
} else
- throw new IllegalStateException("Unexpected class "
- + node.getClass().getName());
+ throw new IllegalStateException("Unexpected class " + node.getClass().getName());
return factor * extractInt(numberNode);
}
diff --git a/src/main/java/de/stups/probkodkod/KodkodSession.java b/src/main/java/de/stups/probkodkod/KodkodSession.java
index 59d46c7e7c2224c314fe792243e41634d050f037..58ce1e56eb51126d4da2fdb8321eb4ea18d87bcf 100644
--- a/src/main/java/de/stups/probkodkod/KodkodSession.java
+++ b/src/main/java/de/stups/probkodkod/KodkodSession.java
@@ -5,10 +5,11 @@ import java.util.Map;
import java.util.logging.Level;
import java.util.logging.Logger;
-import kodkod.engine.Solver;
-import kodkod.instance.TupleSet;
import de.prob.prolog.output.IPrologTermOutput;
import de.stups.probkodkod.sat.SAT4JWithTimeoutFactory;
+import kodkod.engine.Solver;
+import kodkod.engine.satlab.SATFactory;
+import kodkod.instance.TupleSet;
/**
* The session contains all the information that is needed during an interaction
@@ -23,20 +24,35 @@ import de.stups.probkodkod.sat.SAT4JWithTimeoutFactory;
public class KodkodSession {
// private final SATFactory SOLVER = SolverChecker.determineSatFactory();
- private final Logger logger = Logger.getLogger(KodkodSession.class
- .getName());
+ private final Logger logger = Logger.getLogger(KodkodSession.class.getName());
private final Map<String, ImmutableProblem> problems = new HashMap<String, ImmutableProblem>();
private final Map<ImmutableProblem, Solver> solvers = new HashMap<ImmutableProblem, Solver>();
private final Map<ImmutableProblem, Request> currentRequests = new HashMap<ImmutableProblem, Request>();
private boolean stopped = false;
- public void addProblem(final ImmutableProblem problem, long timeout) {
+ public void addProblem(final ImmutableProblem problem, long timeout, int symmetry, SATSolver sat) {
String id = problem.getId();
problems.put(id, problem);
final Solver solver = new Solver();
- solver.options().setSolver(new SAT4JWithTimeoutFactory(timeout));
- solver.options().setSymmetryBreaking(0); // TO DO: provide preference for this; default int value for Kodkod is 20
+ switch (sat) {
+ case sat4j:
+ solver.options().setSolver(new SAT4JWithTimeoutFactory(timeout));
+ break;
+ case glucose:
+ solver.options().setSolver(SATFactory.Glucose);
+ break;
+ case lingeling:
+ solver.options().setSolver(SATFactory.Lingeling);
+ break;
+ case minisat:
+ solver.options().setSolver(SATFactory.MiniSat);
+ break;
+ default:
+ solver.options().setSolver(new SAT4JWithTimeoutFactory(timeout));
+ break;
+ }
+ solver.options().setSymmetryBreaking(symmetry);
final Integer bitwidth = problem.getBitwidth();
if (bitwidth != null) {
solver.options().setBitwidth(bitwidth);
@@ -53,8 +69,7 @@ public class KodkodSession {
info(problem, "deleted");
}
- public void request(final ImmutableProblem problem, final boolean signum,
- final Map<String, TupleSet> newBounds) {
+ public void request(final ImmutableProblem problem, final boolean signum, final Map<String, TupleSet> newBounds) {
final Solver solver = solvers.get(problem);
Request request = problem.createRequest(solver, signum, newBounds);
currentRequests.put(problem, request);
@@ -65,13 +80,11 @@ public class KodkodSession {
return problems.get(problemId);
}
- // size is the max number of solutions found
- public boolean writeNextSolutions(final ImmutableProblem problem,
- final int size, final IPrologTermOutput pto) {
+ // size is the max number of solutions found
+ public boolean writeNextSolutions(final ImmutableProblem problem, final int size, final IPrologTermOutput pto) {
Request request = currentRequests.get(problem);
if (request == null)
- throw new IllegalArgumentException("No request for "
- + problem.getId());
+ throw new IllegalArgumentException("No request for " + problem.getId());
info(problem, "list max " + size + " solutions");
boolean hasSolutions = request.writeNextSolutions(pto, size);
if (!hasSolutions) {
@@ -98,8 +111,7 @@ public class KodkodSession {
this.currentRequests.clear();
System.gc();
long after = Runtime.getRuntime().freeMemory();
- logger.info("session reseted (" + before
- + " bytes of free memory before and " + after
+ logger.info("session reseted (" + before + " bytes of free memory before and " + after
+ " bytes after reset (diff: " + (after - before) + " bytes)");
}
diff --git a/src/main/java/de/stups/probkodkod/SATSolver.java b/src/main/java/de/stups/probkodkod/SATSolver.java
new file mode 100644
index 0000000000000000000000000000000000000000..f784c2b0afefff2e39b1d4bdaa8db013c3513db7
--- /dev/null
+++ b/src/main/java/de/stups/probkodkod/SATSolver.java
@@ -0,0 +1,5 @@
+package de.stups.probkodkod;
+
+public enum SATSolver {
+ lingeling, minisat, sat4j, glucose
+}
diff --git a/src/main/resources/problem.grammar b/src/main/resources/problem.grammar
index 1d559d1259fa2126d26fba9a4e2cbd4b2e86a83a..11bb2d654616520bc18b90127b2b7ea7f497d2fa 100644
--- a/src/main/resources/problem.grammar
+++ b/src/main/resources/problem.grammar
@@ -81,6 +81,8 @@ Tokens
keyword_int2intset = 'int2intset';
keyword_expr2int = 'expr2int';
+ satsolver = 'lingeling' | 'sat4j' | 'minisat' | 'glucose';
+
minus = '-';
identifier = (alpha|digit|'_')+;
@@ -99,7 +101,7 @@ Productions
| {reset} reset
| {none};
- problem = keyword_problem [id]:identifier [timeout]:number
+ problem = keyword_problem [id]:identifier [timeout]:number [symmetry]:number satsolver
[tpl]:parenl [types]:type* [tpr]:parenr
[rpl]:parenl [relations]:relation* [rpr]:parenr formula;
diff --git a/src/test/resources/problems/functions.kodkod b/src/test/resources/problems/functions.kodkod
index 6e1d0894c4520dca0fc72829c3c0bbec88edf969..e5af0d6e2e3e7c9cd8be6f590e5aa292aa1ea377 100644
--- a/src/test/resources/problems/functions.kodkod
+++ b/src/test/resources/problems/functions.kodkod
@@ -1,4 +1,4 @@
-problem functions 3500
+problem functions 3500 0 sat4j
((d 2) (r 2))
diff --git a/src/test/resources/problems/integercast.kodkod b/src/test/resources/problems/integercast.kodkod
index 24695961317854f6c74432a89e29d435b7d95e78..a9baa49593b0bd3efc8b50a56d44d4207e800380 100644
--- a/src/test/resources/problems/integercast.kodkod
+++ b/src/test/resources/problems/integercast.kodkod
@@ -1,4 +1,4 @@
-problem integercast 3500
+problem integercast 3500 0 sat4j
((inttype (si 0 7) (ai 0 9)))
diff --git a/src/test/resources/problems/integers.kodkod b/src/test/resources/problems/integers.kodkod
index c060001888c5b8c34c237c5f7ee100df39952404..e5b934c6829cd9db7f4d5052a1b08be4a2b5587b 100644
--- a/src/test/resources/problems/integers.kodkod
+++ b/src/test/resources/problems/integers.kodkod
@@ -1,4 +1,4 @@
-problem integers 3500
+problem integers 3500 0 sat4j
((inttype (si 0 2))
(w 2))
diff --git a/src/test/resources/problems/intrange.kodkod b/src/test/resources/problems/intrange.kodkod
index 9c6e37d36527f4149f1925ab0456ad9069ed5c1a..c1b9c8603b6e182114f3b3069e4f838d2258f2fb 100644
--- a/src/test/resources/problems/intrange.kodkod
+++ b/src/test/resources/problems/intrange.kodkod
@@ -1,4 +1,4 @@
-problem intrange 3500
+problem intrange 3500 0 sat4j
((inttype (p2i 0 8) (is 0 8)))
diff --git a/src/test/resources/problems/intvar.kodkod b/src/test/resources/problems/intvar.kodkod
index b9c72b5eae5f1b0cdb3a6308aa558cc86a11c5b9..2824f1fb590889b4dabc1d5a1577f66ba892611c 100644
--- a/src/test/resources/problems/intvar.kodkod
+++ b/src/test/resources/problems/intvar.kodkod
@@ -1,4 +1,4 @@
-problem intvar 3500
+problem intvar 3500 0 sat4j
((inttype (si 0 7)))
diff --git a/src/test/resources/problems/loop.kodkod b/src/test/resources/problems/loop.kodkod
index 1725fe9f33dd7138143cbf5c185c0cb5a894b2b5..d78450c6c2e07cb8e740be926938694d7f110fb4 100644
--- a/src/test/resources/problems/loop.kodkod
+++ b/src/test/resources/problems/loop.kodkod
@@ -1,4 +1,4 @@
-problem loop 3500
+problem loop 3500 0 sat4j
((Blocks 8))
diff --git a/src/test/resources/problems/negative.kodkod b/src/test/resources/problems/negative.kodkod
index c0c873df2de0b1cd0c0c8eaee897fad784527666..55d9415bb98b54e5b8e0580dbf41b388a8a49fae 100644
--- a/src/test/resources/problems/negative.kodkod
+++ b/src/test/resources/problems/negative.kodkod
@@ -1,4 +1,4 @@
-problem negative 3500
+problem negative 3500 0 sat4j
((inttype (p2i -15 15)))
diff --git a/src/test/resources/problems/projection.kodkod b/src/test/resources/problems/projection.kodkod
index 05adb8a19abdcb39262161adabc0a1e1c116af47..2b6149c695bc001e45c696a45a88cb6f38459701 100644
--- a/src/test/resources/problems/projection.kodkod
+++ b/src/test/resources/problems/projection.kodkod
@@ -1,4 +1,4 @@
-problem projection 3500
+problem projection 3500 0 sat4j
((world 2))
diff --git a/src/test/resources/problems/relquant.kodkod b/src/test/resources/problems/relquant.kodkod
index 7448a38ef9b78a42c721cb4a748bf73be20fae53..2af010c9d9bfff538e704d522037aa90435115de 100644
--- a/src/test/resources/problems/relquant.kodkod
+++ b/src/test/resources/problems/relquant.kodkod
@@ -1,4 +1,4 @@
-problem relquant 3500
+problem relquant 3500 0 sat4j
((d 2) (r 2))
diff --git a/src/test/resources/problems/returnzero.kodkod b/src/test/resources/problems/returnzero.kodkod
index 82656ad46d19a3fbdfdbec5cb538d6b141f10116..9ce9fda03a1e91ae180778cf0fe5c26d4477e5e8 100644
--- a/src/test/resources/problems/returnzero.kodkod
+++ b/src/test/resources/problems/returnzero.kodkod
@@ -1,4 +1,4 @@
-problem returnzero 3500
+problem returnzero 3500 0 sat4j
( (inttype(p2i 0 0)) )
( (x singleton subset p2i) )
diff --git a/src/test/resources/problems/sendmoremoney.kodkod b/src/test/resources/problems/sendmoremoney.kodkod
index f3791fbd2fe75fc8e240dc59f25ca639355953d8..c46386f652d9b26ba99901a4b37002fed27872be 100644
--- a/src/test/resources/problems/sendmoremoney.kodkod
+++ b/src/test/resources/problems/sendmoremoney.kodkod
@@ -1,4 +1,4 @@
-problem sendmoremoney 3500
+problem sendmoremoney 3500 0 sat4j
((inttype(p2i 0 199980)))
diff --git a/src/test/resources/problems/simpletwovars.kodkod b/src/test/resources/problems/simpletwovars.kodkod
index f84e7ba0db78743207d10060489c4bb8260e9896..7d8d9bc418525eb5f30accfaf557123dc2b584bc 100644
--- a/src/test/resources/problems/simpletwovars.kodkod
+++ b/src/test/resources/problems/simpletwovars.kodkod
@@ -1,4 +1,4 @@
-problem simpletwovars 3500
+problem simpletwovars 3500 0 sat4j
((T 2))