stmt ::= ... | foreach (fmla) {stmt+} | if (fmla) {stmt+} else {stmt+} | cond (fmla) {stmt+}+ else {stmt+} | switch (expr) (ptrn:fmla) {stmt+}+ default {stmt+} dcln ::= ... | predicate id(T x1, ..., T xn) [mode]+ {fmla}+ | predicate T id(T x1, ..., T xn) [mode]+ {fmla}+ ptrn ::= expr | T id | T | * | expr.id(ptrn+) | e[ptrn] | ptrn binop ptrn fmla ::= T id | fmla && fmla | fmla || fmla | forall (fmla) {fmla} | exists (fmla) {fmla} | expr.id(ptrn+) // id names a predicate | ptrn bincomp ptrn bincomp ::= == | != | < | <= | > | >= binop ::= + | - | * | / | %
Foreach
S foreach (F) {s}‘ = FMF‘s
If
S if (F) s1 else s2‘ =
boolean flag = true;
FSF‘{flag=false; s1};
if (flag) s2;Cond
S cond (F1) {s1} (F2) {s2} ... default sd‘ =
boolean flag = true;
FSF1‘{flag=false; s1};
if (flag) { FSF2‘{flag=false; s2};
...
if (flag) sd ...}}
Variable Introduction
FS[T id]s = {T id; s}
FM[T id]s = {T id; s}
Formula Conjunction
FSF1 && F2‘s = FSF1‘(FSF2‘s)
FMF1 && F2‘s = FMF1‘(FMF2‘s)
Notes: We need to create a dependency graph for two reasons:
- During type checking, it allows us to determine if formula is even solvable.
- Gives us an ordering on the conjuncts for translation.
Given a graph, two resulting errors are possible:
- No start state, meaning that not enough values exist to begin solving the formula.
- Not all nodes are reachable from the start states, meaning the formula is too complicated.
Ordering of the conjuncts is determined by a modified topological sort on the graph. Edges in this graph are determined by looking at the modes of each conjunct. A mode has a set of knowns and a set of unknowns. Any conjunct will have a mode that looks like X ! Y. An edge in the dependence graph, (F, F') exists if:
When the mode has an empty set of unknowns (the set on the left of the arrow), this corresponds to a start state in the graph
- X' ² Y
- F: X ! Y
- F': X' ! Y'
Formula Disjunction
FSF1 || F2‘s1s2 = FSF1‘s1(FSF2‘s1s2)
The above should be revised to avoid code duplication.
FMF1 || F2‘s = FMF1‘s; FMF2‘s
Notes: It must be the case that the yielded variables of F1 are the same as the yielded variables of F2.Formula Universal Quantifier
FSforall (F1) {F2}‘s =
FSF1‘ {T v1 = yielding of F1};
FSF2‘ {
boolean flag = true;
FMF1‘ {if (!F2) {flag=false; break;}}
if (flag) {s}
}FMforall (F1) {F2}‘s =
FSF1‘ {T v1 = yielding of F1};
FMF2‘ {
boolean flag = true;
FMF1‘ {if (!F2) {flag=false; break;}}
if (flag) {s}
}Formula Existential Quantifier
Predicate Invocation
FSid(p1, ..., pn)‘s =
Iterator g = new id$();
if (g.hasNext()) {
(x1, ..., xn) = g.next();
s;
}FMid(p1, ..., pn)‘s =
for (Iterator g=new id$(); g.hasNext(); ) {
(x1, ..., xn) = g.next();
s;
}