Skip to content

Commit

Permalink
support both upper and exact record sig scopes
Browse files Browse the repository at this point in the history
  • Loading branch information
@nmacedo
nmacedo committed Oct 28, 2022
1 parent c8492e1 commit dd4ea36
Show file tree
Hide file tree
Showing 4 changed files with 133 additions and 66 deletions.
11 changes: 11 additions & 0 deletions org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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));
Expand Down
39 changes: 24 additions & 15 deletions org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/BoundsComputer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Tuple> 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);
}
}
Expand Down Expand Up @@ -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);
Expand All @@ -501,20 +508,22 @@ private BoundsComputer(A4Reporter rep, A4Solution sol, ScopeComputer sc, Iterabl
}
}

for (Sig s : sigs) {
if (s.isRecord != null) {
List<Decl> 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<Decl> 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);
}
}

Expand All @@ -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);
Expand Down
3 changes: 2 additions & 1 deletion org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/ScopeComputer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -357,7 +357,8 @@ private boolean derive_record_scope(Iterable<Sig> sigs) throws Err {
cscp += n;
}
if (allfound) {
makeExact(null, s);
if (TranslateAlloyToKodkod.EXACT_REC_BOUNDS)
makeExact(null, s);
sig2scope(s, cscp);
changed = true;
} else {
Expand Down
146 changes: 96 additions & 50 deletions ...oytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -90,6 +89,8 @@

public final class TranslateAlloyToKodkod extends VisitReturn<Object> {

static public final boolean EXACT_REC_BOUNDS = false;

static int cnt = 0;

/**
Expand Down Expand Up @@ -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<Decl> 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);
}
Expand Down

0 comments on commit dd4ea36

Please sign in to comment.