From a753ff51be2438ed4210475d3af10a420c4a18ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Zbyn=C4=9Bk=20Jir=C3=A1=C4=8Dek?= Date: Fri, 26 Feb 2016 17:02:22 +0100 Subject: [PATCH] Modification to Z3 code (replaced ArrayExpr by BoolExpr[]). --- .../z3/Z3IntelligentEnsembleFactory.java | 43 +++++++++++-------- .../ensembles/intelligent/z3/pendolino.edl | 2 +- 2 files changed, 25 insertions(+), 20 deletions(-) diff --git a/jdeeco-ensembles-intelligent-z3/src/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/Z3IntelligentEnsembleFactory.java b/jdeeco-ensembles-intelligent-z3/src/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/Z3IntelligentEnsembleFactory.java index e8fc1e292..03a5dfc0a 100644 --- a/jdeeco-ensembles-intelligent-z3/src/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/Z3IntelligentEnsembleFactory.java +++ b/jdeeco-ensembles-intelligent-z3/src/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/Z3IntelligentEnsembleFactory.java @@ -50,12 +50,14 @@ private void initConfiguration() { ctx = new Context(cfg); opt = ctx.mkOptimize(); } - - // assignments for each component and ensemble instance: bool[#ensembles][#components] - private ArrayExpr[] createAssignmentMatrix(String roleName, int maxEnsembleCount) { - ArrayExpr[] assignments = new ArrayExpr[maxEnsembleCount]; + + private BoolExpr[][] createAssignmentMatrix(String roleName, int maxEnsembleCount, int componentCount) { + BoolExpr[][] assignments = new BoolExpr[maxEnsembleCount][]; for (int i = 0; i < maxEnsembleCount; i++) { - assignments[i] = ctx.mkArrayConst("assignment_" + roleName + "_" + i, ctx.getIntSort(), ctx.getBoolSort()); + assignments[i] = new BoolExpr[componentCount]; + for (int j = 0; j < componentCount; j++) { + assignments[i][j] = ctx.mkBoolConst("assignment_" + roleName + "_e" + i + "_c" + j); + } } return assignments; @@ -65,14 +67,14 @@ private ArrayExpr[] createAssignmentMatrix(String roleName, int maxEnsembleCount // assignmentTempCounters[T][0] = 0 if not assignments[T][0], otherwise 1 // assignmentTempCounters[T][R] = assignmentTempCounters[T][R-1], if not assignments[T][R], otherwise it's +1 // therefore assignmentTempCounters[T][#rescuers-1] = number of rescuers for train T - private IntExpr createCounter(ArrayExpr assignments, int length, int index) { + private IntExpr createCounter(BoolExpr[] assignments, int length, int index) { ArrayExpr tempCounts = ctx.mkArrayConst("_tmp_ensemble_assignment_count_" + index, ctx.getIntSort(), ctx.getIntSort()); - BoolExpr firstInSet = (BoolExpr) ctx.mkSelect(assignments, ctx.mkInt(0)); + BoolExpr firstInSet = assignments[0]; opt.Add(ctx.mkImplies(firstInSet, ctx.mkEq(ctx.mkSelect(tempCounts, ctx.mkInt(0)), ctx.mkInt(1)))); opt.Add(ctx.mkImplies(ctx.mkNot(firstInSet), ctx.mkEq(ctx.mkSelect(tempCounts, ctx.mkInt(0)), ctx.mkInt(0)))); for (int j = 1; j < length; j++) { - BoolExpr isInSet = (BoolExpr) ctx.mkSelect(assignments, ctx.mkInt(j)); + BoolExpr isInSet = assignments[j]; IntExpr current = (IntExpr) ctx.mkSelect(tempCounts, ctx.mkInt(j)); IntExpr prev = (IntExpr) ctx.mkSelect(tempCounts, ctx.mkInt(j-1)); opt.Add(ctx.mkImplies(isInSet, @@ -112,7 +114,8 @@ public Collection createInstances(KnowledgeContainer container }*/ // assignments for each rescuer and train: bool[#trains][#rescuers] - ArrayExpr[] assignments = createAssignmentMatrix("rescuer", maxEnsembleCount); + //ArrayExpr[] assignments = createAssignmentMatrix_("rescuer", maxEnsembleCount); + BoolExpr[][] assignments = createAssignmentMatrix("rescuer", maxEnsembleCount, positions.length); // existence of individual ensembles BoolExpr[] ensembleExists = new BoolExpr[maxEnsembleCount]; @@ -145,7 +148,7 @@ public Collection createInstances(KnowledgeContainer container IntNum posExpr = ctx.mkInt(i); BoolExpr[] assigned = new BoolExpr[maxEnsembleCount]; for (int j = 0; j < maxEnsembleCount; j++) { - assigned[j] = ctx.mkSetMembership(posExpr, assignments[j]); + assigned[j] = assignments[j][i]; } opt.Add(ctx.mkOr(assigned)); @@ -165,22 +168,24 @@ else if (k > j) Status status = opt.Check(); if (status == Status.SATISFIABLE) { Model m = opt.getModel(); - for (int i = 0; i < maxEnsembleCount; i++) - System.out.println("train " + i + ": " + m.getFuncInterp(assignments[i].getFuncDecl())); + for (int i = 0; i < maxEnsembleCount; i++) { + System.out.print("train " + i + ": ["); + for (int j = 0; j < positions.length; j++) { + System.out.print(m.getConstInterp(assignments[i][j]).getBoolValue() + " "); + } + + System.out.println("]"); + } // create ensembles List result = new ArrayList<>(); for (int i = 0; i < maxEnsembleCount; i++) { IntelligentEnsemble ie = new IntelligentEnsemble(i + 1); ie.members = new ArrayList<>(); - FuncInterp fi = m.getFuncInterp(assignments[i].getFuncDecl()); - Entry[] entries = fi.getEntries(); - for (int j = 0; j < fi.getNumEntries(); j++) { - Expr[] a = entries[j].getArgs(); - Expr v = entries[j].getValue(); + for (int j = 0; j < positions.length; j++) { + Expr v = m.getConstInterp(assignments[i][j]); if (v.getBoolValue() == Z3_lbool.Z3_L_TRUE) { - int componentId = Integer.parseInt(a[0].toString()); - ie.members.add(rescuers[componentId]); + ie.members.add(rescuers[j]); } } diff --git a/jdeeco-ensembles-intelligent-z3/test/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/pendolino.edl b/jdeeco-ensembles-intelligent-z3/test/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/pendolino.edl index 73f9bcaa6..b72c76db2 100644 --- a/jdeeco-ensembles-intelligent-z3/test/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/pendolino.edl +++ b/jdeeco-ensembles-intelligent-z3/test/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/pendolino.edl @@ -4,7 +4,7 @@ ensemble PendolinoEnsemble id trainId : int membership roles - rescuers [6..15] : Rescuer + rescuers [6..7] : Rescuer fitness 0 knowledge exchange