edu.mit.csail.sdg.alloy4compiler.translator
Class Simplifier

java.lang.Object
  edu.mit.csail.sdg.alloy4compiler.translator.Simplifier

public class Simplifier
extends java.lang.Object

Immutable; this class shrinks the unknowns as much as possible in order to reduce the number of variables in final CNF.

Currently it recognizes the following patterns:

(1) When it sees "A in B", it will try to derive a safe upperbound for B, and then remove any excess unknowns from A's upperbound.

(2) When it sees "A = B", it will try to simplify A assuming "A in B", and then simplify B assuming "B in A".

Constructor Summary

Simplifier()
Construct a Simplifier object.

Method Summary

boolean

simplify(A4Reporter rep, A4Solution sol, java.util.List<kodkod.ast.Formula> formulas) Simplify sol.bounds() based on the set of formulas, or to modify the formulas list itself.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Simplifier

public Simplifier()

Construct a Simplifier object.

Method Detail

simplify

public boolean simplify(A4Reporter rep,
                        A4Solution sol,
                        java.util.List<kodkod.ast.Formula> formulas)
                 throws Err

Simplify sol.bounds() based on the set of formulas, or to modify the formulas list itself. Subclasses should override this method to implement different simplification algorithms. (Note: this method is allowed to modify the "formulas" array if it sees an opportunity for optimization)

Throws:

Err