Skip to content

Commit

Permalink
Merge pull request #43 from haslab/dev
Browse files Browse the repository at this point in the history 
Version 1.2.2
  • Loading branch information
@nmacedo
nmacedo authored Sep 24, 2020
2 parents 892ef18 + d23c002 commit 6e2c7ce
Show file tree
Hide file tree
Showing 12 changed files with 307 additions and 109 deletions.
2 changes: 1 addition & 1 deletion pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
<modelVersion>4.0.0</modelVersion>
<groupId>pt.uminho.haslab.pardinus</groupId>
<artifactId>pardinus</artifactId>
<version>1.2.1</version>
<version>1.2.2</version>
<packaging>jar</packaging>
<name>pardinus</name>
<profiles>
Expand Down
4 changes: 4 additions & 0 deletions src/main/java/kodkod/engine/TemporalPardinusSolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -563,6 +563,10 @@ private Solution nextNonTrivialSolution(int state, int steps, Set<Relation> fix,
private int iteration_stage = 0;

private Solution nextNonTrivialSolutionSAT(int state, int steps, Set<Relation> fix, Set<Relation> change) {
if (change.isEmpty()) {
translation = null;
return Solution.unsatisfiable(new Statistics(0, 0, 0, 0, 0), null);
}

boolean isSat = false;
long solveTime = 0;
Expand Down
4 changes: 2 additions & 2 deletions src/main/java/kodkod/engine/fol2sat/SymmetryBreaker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ final BooleanValue generateSBP(LeafInterpreter interpreter, Options options) {
int curIndex = indeces.next();
Iterator<Tuple> times = null;
if (bounds.relations().contains(TemporalTranslator.STATE))
bounds.lowerBound(TemporalTranslator.STATE).iterator();
times = bounds.lowerBound(TemporalTranslator.STATE).iterator();
Tuple time = null;
do {
for(Iterator<RelationParts> rIter = relParts.iterator(); rIter.hasNext() && original.size() < predLength;) {
Expand Down Expand Up @@ -239,7 +239,7 @@ final BooleanValue generateSBP(LeafInterpreter interpreter, Options options) {
continue;

boolean zzz = false;
if (times != null) {
if (times != null) {
TupleSet yyy = bounds.lowerBound(TemporalTranslator.STATE);
Tuple xxx = interpreter.universe().factory().tuple(interpreter.universe().factory().tuple(r.arity(), entry.index()).atom(r.arity()-1));
zzz = yyy.contains(xxx);
Expand Down
91 changes: 73 additions & 18 deletions src/main/java/kodkod/instance/Instance.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@
import kodkod.ast.ConstantExpression;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.IntConstant;
import kodkod.ast.NaryFormula;
import kodkod.ast.Relation;
import kodkod.ast.Variable;
Expand Down Expand Up @@ -235,37 +236,76 @@ public Instance clone() {
}
}


/**
* Converts an instance into a formula that exactly identifies it. Requires that
* every relevant atom be reified into a singleton relation, which may be
* re-used between calls. Relevant atoms are determined from the provided formulas.
* every relevant atom be reified into a singleton relation or quantified in a
* some-disj pattern, which may be re-used between calls. Relevant atoms are
* determined from the provided formulas.
*
* Will change <bounds> if not all atoms of the universe are present at <reif>.
* Will change <bounds> if not all atoms of the universe are present at <reif>
* and <someDisj> false.
*
* @assumes reif != null
* @param reif
* the previously reified atoms
* @throws NullPointerException
* reif = null
* @assumes reif != null
* @assumes !someDisj => bounds != null
* @param reif the previously reified atoms, as relations or quantified vars depending on <someDisj>
* @param formula a formula from which the relevant relations are identified
* @param someDisj whether the formula will use atoms reified as relations or a some-disj pattern
* @param bounds the problem's bounds, updated if !someDisj
* @throws NullPointerException reif = null
* @throws NullPointerException !someDisj && bounds == null
* @return the formula representing <this>
*/
public Formula formulate(Map<Object, Expression> reif, Formula formula, boolean someDisj, Bounds bounds) {
return formulate(reif,formula,someDisj,bounds,false);
}

/**
* Converts an instance into a formula that exactly identifies it. Requires that
* every relevant atom be reified into a singleton relation or quantified in a
* some-disj pattern, which may be re-used between calls. Relevant atoms are
* determined from the provided formulas.
*
* Will change <bounds> if not all atoms of the universe are present at <reif>
* and <someDisj> false.
*
* @assumes reif != null
* @assumes !someDisj => bounds != null
* @param reif the previously reified atoms, as relations or quantified vars depending on <someDisj>
* @param formula a formula from which the relevant relations are identified
* @param someDisj whether the formula will use atoms reified as relations or a some-disj pattern
* @param bounds the problem's bounds, updated if !someDisj
* @param localUniv whether to restrict the universe of atoms locally, only relevant if some-disj pattern
* @throws NullPointerException reif = null
* @throws NullPointerException !someDisj && bounds == null
* @return the formula representing <this>
*/
// [HASLab]
public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula formula, boolean someDisj) {

public Formula formulate(Map<Object, Expression> reif, Formula formula, boolean someDisj, Bounds bounds, boolean localUniv) {
Set<Relation> relevants = formula.accept(new RelationCollector(new HashSet<>()));
// reify atoms not yet reified
for (int i = 0; i < universe().size(); i++) {
Expression r;
if (reif.keySet().contains(universe().atom(i)))
r = reif.get(universe().atom(i));
else {
r = Relation.atom(universe().atom(i).toString());
reif.put(universe().atom(i), r);
// integers do not need to be quantified
if (!universe().atom(i).toString().matches("-?\\d+")) {
Expression r;
if (reif.keySet().contains(universe().atom(i)))
r = reif.get(universe().atom(i));
else {
if (someDisj) {
r = Variable.unary(universe().atom(i).toString());
} else {
r = Relation.atom(universe().atom(i).toString());
}
reif.put(universe().atom(i), r);
}
if (!someDisj && !bounds.relations.contains(r))
bounds.boundExactly((Relation) r, bounds.universe().factory().setOf(universe().atom(i)));
}
if (r instanceof Relation && !bounds.relations.contains(r))
bounds.boundExactly((Relation) r, bounds.universe().factory().setOf(universe().atom(i)));
}

List<Expression> locals = new ArrayList<Expression>();

// create an equality for every relation
// a = A + ... && r = A -> B + ...
List<Formula> res = new ArrayList<Formula>();
Expand All @@ -281,6 +321,7 @@ public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula fo
if (it.hasNext()) {
Tuple u = it.next();
Expression r1 = reif.get(u.atom(0));
locals.add(r1);
for (int i = 1; i < u.arity(); i++)
r1 = r1.product(reif.get(u.atom(i)));
r = r1;
Expand All @@ -293,12 +334,26 @@ public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula fo
while (it.hasNext()) {
Tuple u = it.next();
Expression r1 = reif.get(u.atom(0));
locals.add(r1);
for (int i = 1; i < u.arity(); i++)
r1 = r1.product(reif.get(u.atom(i)));
r = r.union(r1);
}
res.add(rel.eq(r));
}

if (someDisj && localUniv) {
Expression al = null;
for (Expression e : locals)
al = al == null? e : al.union(e);
for (int i = 0; i < universe().size(); i++)
if (universe().atom(i).toString().matches("-?\\d+")) {
Expression intexp = IntConstant.constant(Integer.valueOf(universe().atom(i).toString())).toExpression();
al = al == null ? intexp : al.union(intexp);
}
res.add(al.eq(Expression.UNIV));
}

return NaryFormula.and(res);
}

Expand Down
60 changes: 38 additions & 22 deletions src/main/java/kodkod/instance/TemporalInstance.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@
import kodkod.ast.Decls;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.IntConstant;
import kodkod.ast.Relation;
import kodkod.ast.Variable;
import kodkod.engine.Evaluator;
Expand Down Expand Up @@ -235,16 +236,25 @@ public TemporalInstance(Instance instance, PardinusBounds extbounds) {
* Will change <bounds> if not all atoms of the universe are present at <reif>.
*
* @assumes reif != null
* @param bounds the declaration of the relations
* @param reif the previously reified atoms
* @param formula formula used to identify the relevant relations
* @param bounds the declaration of the relations
* @throws NullPointerException reif = null
* @return the formula representing <this>
*/
// [HASLab]
@Override
public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula formula, boolean someDisj) {
return formulate(bounds, reif, formula, -1, null, someDisj);
public Formula formulate(Map<Object, Expression> reif, Formula formula, boolean someDisj, Bounds bounds) {
return formulate(bounds, reif, formula, -1, null, someDisj, true);
}

@Override
public Formula formulate(Map<Object, Expression> reif, Formula formula, boolean someDisj, Bounds bounds, boolean localUniv) {
return formulate(bounds, reif, formula, -1, null, someDisj, localUniv);
}

public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula formula, int start, Integer end, boolean someDisj) {
return formulate(bounds, reif, formula, start, end, someDisj, true);
}

/**
Expand Down Expand Up @@ -274,7 +284,7 @@ public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula fo
* @return the formula representing <this>
*/
// [HASLab]
public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula formula, int start, Integer end, boolean someDisj) {
public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula formula, int start, Integer end, boolean someDisj, boolean localUniv) {
if (start < -1)
throw new IllegalArgumentException("Segment start must be >= -1.");
if (end != null && end < start)
Expand All @@ -283,22 +293,24 @@ public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula fo
// reify atoms not yet reified
Universe sta_uni = states.get(0).universe();
for (int i = 0; i < sta_uni.size(); i++) {
Expression r;
if (!reif.keySet().contains(sta_uni.atom(i))) {
if (someDisj) {
r = Variable.unary(sta_uni.atom(i).toString());
// integers do not need to be quantified
if (!sta_uni.atom(i).toString().matches("-?\\d+")) {
Expression r;
if (!reif.keySet().contains(sta_uni.atom(i))) {
if (someDisj) {
r = Variable.unary(sta_uni.atom(i).toString());
} else {
r = Relation.atom(sta_uni.atom(i).toString());
}
reif.put(sta_uni.atom(i), r);
} else {
r = Relation.atom(sta_uni.atom(i).toString());
r = reif.get(sta_uni.atom(i));
}
reif.put(sta_uni.atom(i), r);
} else {
r = reif.get(sta_uni.atom(i));
if (!someDisj && !bounds.relations.contains(r))
bounds.boundExactly((Relation) r, bounds.universe().factory().setOf(sta_uni.atom(i)));
}
if (!someDisj && !bounds.relations.contains((Relation) r))
bounds.boundExactly((Relation) r, bounds.universe().factory().setOf(sta_uni.atom(i)));
}


Set<Relation> staticss = new HashSet<Relation>();
for (Relation r : states.get(0).relations())
if (!r.isVariable())
Expand All @@ -318,11 +330,11 @@ public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula fo
// TODO: the looping formula should also be offset in this case!
if (j == null)
j = Integer.max(start + (prefixLength() - 1) - loop, prefixLength() - 1);
if (j >= 0) {
if (j != null && j >= 0) {
// the state formulas, start from the end and accumulate afters
res = state(j--).formulate(bounds, reif, slcs.getValue(), someDisj);
res = state(j--).formulate(reif, slcs.getValue(), someDisj, bounds, !localUniv);
for (; j >= Integer.max(0, start); j--)
res = state(j).formulate(bounds, reif, slcs.getValue(), someDisj).and(res.after());
res = state(j).formulate(reif, slcs.getValue(), someDisj, bounds, !localUniv).and(res.after());
// after offset when start > 0
for (; j >= 0; j--)
res = res.after();
Expand All @@ -331,7 +343,7 @@ public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula fo

// the configuration formula, if start = -1
if (start < 0 && !slcs.getKey().equals(Formula.TRUE)) {
Formula sres = states.get(prefixLength() - 1).formulate(bounds, reif, slcs.getKey(), someDisj);
Formula sres = states.get(prefixLength() - 1).formulate(reif, slcs.getKey(), someDisj, bounds, false);
res = res.equals(Formula.TRUE) ? sres : sres.and(res);
}

Expand All @@ -340,14 +352,14 @@ public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula fo
// create the looping constraint
// after^loop always (Sloop => after^(end-loop) Sloop && Sloop+1 =>
// after^(end-loop) Sloop+1 && ...)
Formula rei = states.get(loop).formulate(bounds, reif, slcs.getValue(), someDisj);
Formula rei = states.get(loop).formulate(reif, slcs.getValue(), someDisj, bounds, !localUniv);
Formula rei2 = rei;
for (int i = loop; i < prefixLength(); i++)
rei2 = rei2.after();

Formula looping = rei.implies(rei2);
for (int i = loop + 1; i < prefixLength(); i++) {
rei = states.get(i).formulate(bounds, reif, slcs.getValue(), someDisj);
rei = states.get(i).formulate(reif, slcs.getValue(), someDisj, bounds, !localUniv);
rei2 = rei;
for (int k = loop; k < prefixLength(); k++)
rei2 = rei2.after();
Expand All @@ -372,7 +384,11 @@ public Formula formulate(Bounds bounds, Map<Object, Expression> reif, Formula fo
decls = decls.and(((Variable) e).oneOf(Expression.UNIV));
}
}
res = (al.eq(Expression.UNIV)).and(res);
for (int i = 0; i < sta_uni.size(); i++)
if (sta_uni.atom(i).toString().matches("-?\\d+"))
al = al.union(IntConstant.constant(Integer.valueOf(sta_uni.atom(i).toString())).toExpression());
if (localUniv)
res = (al.eq(Expression.UNIV)).and(res);
res = res.forSome(decls);
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/main/java/kodkod/util/nodes/PrettyPrinter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -349,8 +349,8 @@ public void visit(UnaryTempFormula node) {
* parenthesized if it's an instance of binary expression or an if expression. **/
// [HASLab]
public void visit(TempExpression node) {
keyword(node.op());
visitChild(node.expression(), parenthesize(node.op(), node.expression()));
append(node.op());
}


Expand Down
Loading

0 comments on commit 6e2c7ce

Please sign in to comment.