Merge pull request #43 from haslab/dev

Version 1.2.2

Author: Nuno Macedo

pom.xml

@@ -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>

src/main/java/kodkod/engine/TemporalPardinusSolver.java

@@ -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;

src/main/java/kodkod/engine/fol2sat/SymmetryBreaker.java

@@ -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;) {
@@ -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);	

src/main/java/kodkod/instance/Instance.java

@@ -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;
@@ -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>();
@@ -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;
@@ -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);
 	}
 

src/main/java/kodkod/instance/TemporalInstance.java

@@ -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;
@@ -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);
 	}
 
 	/**
@@ -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)
@@ -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())
@@ -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();
@@ -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);
 			}
 
@@ -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();
@@ -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);
 			}
 		}

src/main/java/kodkod/util/nodes/PrettyPrinter.java

@@ -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());
 		}