From dd4ea3684216e48e75b433828b1594dfa1345bb4 Mon Sep 17 00:00:00 2001 From: nmacedo Date: Fri, 28 Oct 2022 14:47:42 -0400 Subject: [PATCH] support both upper and exact record sig scopes --- .../mit/csail/sdg/translator/A4Solution.java | 11 ++ .../csail/sdg/translator/BoundsComputer.java | 39 +++-- .../csail/sdg/translator/ScopeComputer.java | 3 +- .../translator/TranslateAlloyToKodkod.java | 146 ++++++++++++------ 4 files changed, 133 insertions(+), 66 deletions(-) diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java index 0871612e5..7b2de27f7 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java @@ -73,6 +73,7 @@ import edu.mit.csail.sdg.translator.A4Options.SatSolver; import kodkod.ast.BinaryExpression; import kodkod.ast.BinaryFormula; +import kodkod.ast.ConstantExpression; import kodkod.ast.Decl; import kodkod.ast.Expression; import kodkod.ast.Formula; @@ -2088,6 +2089,16 @@ public Expression visit(Relation rel) { else return rel; } + + @Override + public Expression visit(BinaryExpression bexp) { + if (bexp.left().equals(a2k) && bexp.right().equals(ConstantExpression.UNIV) && bexp.op().equals(ExprOperator.JOIN)) + return a2k.join(((BinaryExpression) ((BinaryExpression) fldDom).right()).right().union(A4Solution.KK_DUMMY)); + else + return super.visit(bexp); + } + + }; for (Expr exp : this.a2k.keySet()) this.a2k.put(exp, this.a2k.get(exp).accept(replacer)); diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/BoundsComputer.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/BoundsComputer.java index 73e3662fc..d3cceec78 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/BoundsComputer.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/BoundsComputer.java @@ -144,7 +144,14 @@ private void computeUpperBound(PrimSig sig) throws Err { // potentionally get any of the atom from X. for (PrimSig c : sig.children()) { if (sc.sig2scope(c) > lb.get(c).size()) - ub.get(c).addAll(x); + if (c.isRecord == null || TranslateAlloyToKodkod.EXACT_REC_BOUNDS) + ub.get(c).addAll(x); + else { + Iterator it = ub.get(sig).iterator(); + while (sc.sig2scope(c) > ub.get(c).size()) + ub.get(c).add(it.next()); + ub.get(sig).removeAll(ub.get(c)); + } computeUpperBound(c); } } @@ -491,7 +498,7 @@ private BoundsComputer(A4Reporter rep, A4Solution sol, ScopeComputer sc, Iterabl ub.add(sigTuple.product(factory.tuple(typeTupleSet_it.next().get(ctr)))); Relation r = (Relation) sol.a2k(lbl); if (r == null) { - r = sol.addRel(s.label + "." + lbl.label, ub, ub, true); + r = sol.addRel(((Field) lbl).sig.label + "." + lbl.label, ub, ub, true); sol.addField((Field) lbl, r); } else sol.updRel(r, ub, ub); @@ -501,20 +508,22 @@ private BoundsComputer(A4Reporter rep, A4Solution sol, ScopeComputer sc, Iterabl } } - for (Sig s : sigs) { - if (s.isRecord != null) { - List anc_fields = getAllFields((PrimSig) s); - Expression rel = sol.a2k(s); - if (rel instanceof BinaryExpression) - rel = ((BinaryExpression) rel).right(); - Expression fldDom = rel; - for (Decl dcl : anc_fields) { - for (ExprHasName lbl : dcl.names) { - Relation r = (Relation) sol.a2k(lbl); - fldDom = fldDom.intersection(r.join(ConstantExpression.UNIV)); + if (TranslateAlloyToKodkod.EXACT_REC_BOUNDS) { + for (Sig s : sigs) { + if (s.isRecord != null) { + List anc_fields = getAllFields((PrimSig) s); + Expression rel = sol.a2k(s); + if (rel instanceof BinaryExpression) + rel = ((BinaryExpression) rel).right(); + Expression fldDom = rel; + for (Decl dcl : anc_fields) { + for (ExprHasName lbl : dcl.names) { + Relation r = (Relation) sol.a2k(lbl); + fldDom = fldDom.intersection(r.join(ConstantExpression.UNIV)); + } } + sol.updateA2K(rel, fldDom); } - sol.updateA2K(rel, fldDom); } } @@ -530,7 +539,7 @@ private BoundsComputer(A4Reporter rep, A4Solution sol, ScopeComputer sc, Iterabl // Add any additional SIZE constraints for (Sig s : sigs) - if (!s.builtin && s.isRecord == null) { + if (!s.builtin && (s.isRecord == null && TranslateAlloyToKodkod.EXACT_REC_BOUNDS)) { Expression exp = sol.a2k(s); TupleSet upper = sol.query(true, exp, false), lower = sol.query(false, exp, false); final int n = sc.sig2scope(s); diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/ScopeComputer.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/ScopeComputer.java index db4cc9d24..dcaf54c8d 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/ScopeComputer.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/ScopeComputer.java @@ -357,7 +357,8 @@ private boolean derive_record_scope(Iterable sigs) throws Err { cscp += n; } if (allfound) { - makeExact(null, s); + if (TranslateAlloyToKodkod.EXACT_REC_BOUNDS) + makeExact(null, s); sig2scope(s, cscp); changed = true; } else { diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java index 473c50f94..8f917a15a 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java @@ -58,7 +58,6 @@ import edu.mit.csail.sdg.ast.Type; import edu.mit.csail.sdg.ast.VisitReturn; import kodkod.ast.BinaryExpression; -import kodkod.ast.ConstantExpression; import kodkod.ast.Decls; import kodkod.ast.ExprToIntCast; import kodkod.ast.Expression; @@ -90,6 +89,8 @@ public final class TranslateAlloyToKodkod extends VisitReturn { + static public final boolean EXACT_REC_BOUNDS = false; + static int cnt = 0; /** @@ -258,66 +259,111 @@ private void makeFacts(Expr facts) throws Err { facts = (new ConvToConjunction()).visitThis(facts); // add the field facts and appended facts for (Sig s : frame.getAllReachableSigs()) { - for (Decl d : s.getFieldDecls()) { - k2pos_enabled = false; - for (ExprHasName n : d.names) { - Field f = (Field) n; - Expr rhs; - if (s.isRecord == null) - rhs = d.expr; - else { - rhs = ((ExprUnary) d.expr.deNOP()).sub; - if (((ExprUnary) d.expr.deNOP()).op == Op.LONEOF) - rhs = rhs.plus(A4Solution.dummyS); - frame.updateA2K(a2k(f), a2k(f).intersection(ConstantExpression.UNIV.product(cset(rhs)))); - } - Expr form = s.decl.get().join(f).in(rhs); - form = s.isOne == null ? form.forAll(s.decl) : ExprLet.make(null, (ExprVar) (s.decl.get()), s, form); - Formula ff = cform(form); - if (TemporalTranslator.isTemporal(ff)) - ff = ff.always(); - frame.addFormula(ff, f); - // Given the above, we can be sure that every column is - // well-bounded (except possibly the first column). - // Thus, we need to add a bound that the first column is a - // subset of s. - // [electrum] mutable singletons sigs cannot be simplified - if ((s.isOne == null || s.isVariable != null) && s.isRecord == null) { - Expression sr = a2k(s), fr = a2k(f); - for (int i = f.type().arity(); i > 1; i--) - fr = fr.join(Expression.UNIV); - ff = fr.in(sr); + if (s.isRecord == null || !EXACT_REC_BOUNDS) { + for (Decl d : s.getFieldDecls()) { + k2pos_enabled = false; + for (ExprHasName n : d.names) { + Field f = (Field) n; + Expr rhs; + if (s.isRecord == null) + rhs = d.expr; + else { + rhs = ((ExprUnary) d.expr.deNOP()).sub; + if (((ExprUnary) d.expr.deNOP()).op == Op.LONEOF) + rhs = rhs.plus(A4Solution.dummyS); + } + Expr form = s.decl.get().join(f).in(rhs); + form = s.isOne == null ? form.forAll(s.decl) : ExprLet.make(null, (ExprVar) (s.decl.get()), s, form); + Formula ff = cform(form); if (TemporalTranslator.isTemporal(ff)) ff = ff.always(); frame.addFormula(ff, f); + // Given the above, we can be sure that every column is + // well-bounded (except possibly the first column). + // Thus, we need to add a bound that the first column is a + // subset of s. + // [electrum] mutable singletons sigs cannot be simplified + if ((s.isOne == null || s.isVariable != null) && s.isRecord == null) { + Expression sr = a2k(s), fr = a2k(f); + for (int i = f.type().arity(); i > 1; i--) + fr = fr.join(Expression.UNIV); + ff = fr.in(sr); + if (TemporalTranslator.isTemporal(ff)) + ff = ff.always(); + frame.addFormula(ff, f); + } } - } - if (s.isOne == null && d.disjoint2 != null) - for (ExprHasName f : d.names) { - Decl that = s.oneOf("that"); - Expr formula = s.decl.get().equal(that.get()).not().implies(s.decl.get().join(f).intersect(that.get().join(f)).no()); - Formula ff = cform(formula.forAll(that).forAll(s.decl)); + if (s.isOne == null && d.disjoint2 != null) + for (ExprHasName f : d.names) { + Decl that = s.oneOf("that"); + Expr formula = s.decl.get().equal(that.get()).not().implies(s.decl.get().join(f).intersect(that.get().join(f)).no()); + Formula ff = cform(formula.forAll(that).forAll(s.decl)); + if (d.isVar != null) + ff = ff.always(); + frame.addFormula(ff, d.disjoint2); + } + if (d.names.size() > 1 && d.disjoint != null) { + Formula ff = cform(ExprList.makeDISJOINT(d.disjoint, null, d.names)); if (d.isVar != null) ff = ff.always(); - frame.addFormula(ff, d.disjoint2); + frame.addFormula(ff, d.disjoint); + } + k2pos_enabled = true; + for (Expr f : s.getFacts()) { + Expr form = s.isOne == null ? f.forAll(s.decl) : ExprLet.make(null, (ExprVar) (s.decl.get()), s, f); + Formula kdorm = cform(form); + // [electrum] avoid "always" over statics (not only efficiency, total orders would not by detected in SB) + if (TemporalTranslator.isTemporal(kdorm)) + kdorm = kdorm.always(); + frame.addFormula(kdorm, f); } - if (d.names.size() > 1 && d.disjoint != null) { - Formula ff = cform(ExprList.makeDISJOINT(d.disjoint, null, d.names)); - if (d.isVar != null) - ff = ff.always(); - frame.addFormula(ff, d.disjoint); } } - k2pos_enabled = true; - for (Expr f : s.getFacts()) { - Expr form = s.isOne == null ? f.forAll(s.decl) : ExprLet.make(null, (ExprVar) (s.decl.get()), s, f); - Formula kdorm = cform(form); - // [electrum] avoid "always" over statics (not only efficiency, total orders would not by detected in SB) - if (TemporalTranslator.isTemporal(kdorm)) - kdorm = kdorm.always(); - frame.addFormula(kdorm, f); + } + for (Sig s : frame.getAllReachableSigs()) { + if (s.isRecord != null && s.isAbstract == null && !EXACT_REC_BOUNDS) { + + Decls ds = null; + Formula body = Formula.TRUE; + + List anc_fields = getAllFields((PrimSig) s); + if (anc_fields.isEmpty()) { + frame.addFormula(a2k(s).one().always(), s.pos); + } else { + Variable rv = Variable.unary("r"); + for (int i = 0; i < anc_fields.size(); i++) { + ExprUnary ft = (ExprUnary) anc_fields.get(i).expr; + Expression tp = cset(ft.sub); + if (ft.op == Op.LONEOF) + tp = tp.union(A4Solution.KK_DUMMY); + for (ExprHasName lbl : anc_fields.get(i).names) { + Variable v = Variable.unary("v" + i); + ds = ds == null ? v.oneOf(tp) : ds.and(v.oneOf(tp)); + body = body.and(rv.join(a2k((Field) lbl)).eq(v)); + } + } + + Expression sum = Expression.NONE; + for (Sig cs : ((PrimSig) s).children()) + sum = sum.union(a2k(cs)); + + frame.addFormula(body.forSome(rv.oneOf(a2k(s).difference(sum))).forAll(ds).always(), s.pos); + + } } } + for (Sig s : frame.getAllReachableSigs()) { + if (s.isRecord != null) + for (Decl d : s.getFieldDecls()) { + for (ExprHasName n : d.names) { + Field f = (Field) n; + Expr rhs = ((ExprUnary) d.expr.deNOP()).sub; + // if (((ExprUnary) d.expr.deNOP()).op == Op.LONEOF) + // rhs = rhs.plus(A4Solution.dummyS); + frame.updateA2K(a2k(f), a2k(f).intersection(a2k(s).product(cset(rhs)))); + } + } + } k2pos_enabled = true; recursiveAddFormula(facts); }