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

java.lang.Object
  extended by 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