001package org.clafer.scope;
002
003import java.util.Collections;
004import java.util.HashMap;
005import java.util.Map;
006import java.util.Map.Entry;
007import java.util.Set;
008import org.clafer.ast.AstClafer;
009import org.clafer.common.Check;
010
011/**
012 * <p>
013 * An immutable mapping from Clafers to their scope. Also contains the scope of
014 * integers for solving, like the bit-width in Alloy, but more flexible because
015 * the lowest and highest integers can be set independently and does not have to
016 * be a power of 2.
017 * </p>
018 * <p>
019 * The scope is built through the constructor or {@link ScopeBuilder}, whichever
020 * is mort convenient.
021 * </p>
022 * <p>
023 * Example 1:
024 * <pre>
025 * Map&lt;AstClafer, Integer&gt; map = new HashMap&lt;AstClafer, Integer&gt();
026 * map.put(claferA, 3);
027 * map.put(claferB, 2);
028 * Scope scope = new Scope(map, 3, -16, 16);
029 * </pre>
030 * </p>
031 * <p>
032 * Example 2:
033 * <pre>
034 * Scope scope = Scope.set(claferA, 3).set(claferB).defaultScope(3).intLow(-16).intHigh(16).toScope();
035 * </pre>
036 * </p>
037 * <p>
038 * Both examples construct the same scope.
039 * </p>
040 *
041 * <p>
042 * What is scope? Because of the expressiveness of Clafer, reasoning is too
043 * difficult in general. The scope is a limitation of the solver so that
044 * reasoning feasible.
045 * <p>
046 * Example 1:
047 * <pre>
048 * A : int
049 * B : int
050 * C : int
051 * [A * A * A + B * B * B = C * C * C]
052 * </pre>
053 * </p>
054 * <p>
055 * Example 2:
056 * <pre>
057 * A *
058 * B *
059 * C *
060 * [#A * #A * #A + #B * #B * #B = #C * #C * #C]
061 * </pre>
062 * </p>
063 * Both examples are attempting to prove/disprove Fermat's last theorem for k=3,
064 * although this easily generalizes for any k. Unfortunately this is too
065 * difficult, so the solver only attempts to prove/disprove upto a certain
066 * scope. In example 1, a scope of
067 * {@code Scope.intLow(-16).intHigh(16).toScope()} would only attempt the proof
068 * for integers between negative and positive 16. In example 2, a scope of
069 * {@code Scope.defaultScope(16).toScope()} would only attempt the proof for
070 * integers between 0 and positive 16 (the example uses encodes integers using
071 * cardinality).
072 *
073 * @author jimmy
074 * @see ScopeBuilder
075 */
076public class Scope implements Scopable {
077
078    private final Map<AstClafer, Integer> scopes;
079    private final int defaultScope;
080    private final int intLow, intHigh;
081
082    /**
083     * Construct a new scope. Altering the map has no affect once the scope is
084     * constructed.
085     *
086     * @param scopes a map of Clafers to their scopes
087     * @param defaultScope the scope for unspecified Clafers
088     * @param intLow the lowest (inclusive) integer used for solving
089     * @param intHigh the highest (inclusive) integer used for solving
090     */
091    public Scope(Map<AstClafer, Integer> scopes, int defaultScope, int intLow, int intHigh) {
092        if (defaultScope <= 0) {
093            throw new IllegalArgumentException("Default scope must be positive");
094        }
095        for (Entry<AstClafer, Integer> entry : scopes.entrySet()) {
096            if (entry.getValue() < 0) {
097                throw new IllegalArgumentException(entry.getKey().getName() + " scope set to " + entry.getValue() + ". Scope must be non-negative.");
098            }
099        }
100        if (intLow > intHigh) {
101            throw new IllegalArgumentException("intLow(" + intLow + " > intHigh(" + intHigh + ")");
102        }
103        this.scopes = new HashMap<>(scopes);
104        this.defaultScope = defaultScope;
105        this.intLow = intLow;
106        this.intHigh = intHigh;
107    }
108
109    /**
110     * Returns the set of Clafers that have an explicit scope.
111     *
112     * @return the scoped Clafers
113     */
114    public Set<AstClafer> getScoped() {
115        return Collections.unmodifiableSet(scopes.keySet());
116    }
117
118    /**
119     * Returns the scope of the Clafer. If the Clafer is not specified a
120     * specific scope during the construction of this object, then the default
121     * scope is returned.
122     *
123     * @param clafer the Clafer
124     * @return the scope of the Clafer
125     */
126    public int getScope(AstClafer clafer) {
127        Integer scope = scopes.get(Check.notNull(clafer));
128        return scope == null ? defaultScope : scope.intValue();
129    }
130
131    /**
132     * The scope for unspecified Clafers.
133     *
134     * @return the default scope
135     */
136    public int getDefaultScope() {
137        return defaultScope;
138    }
139
140    /**
141     * Returns the lowest (inclusive) integer used for solving.
142     *
143     * @return the lowest integer
144     */
145    public int getIntLow() {
146        return intLow;
147    }
148
149    /**
150     * Returns the highest (inclusive) integer used for solving.
151     *
152     * @return the highest integer
153     */
154    public int getIntHigh() {
155        return intHigh;
156    }
157
158    /**
159     * Construct the scope using the builder pattern.
160     *
161     * @see ScopeBuilder
162     * @return a new builder
163     */
164    public static ScopeBuilder builder() {
165        return new ScopeBuilder();
166    }
167
168    /**
169     * Equivalent to {@code builder().setScope(clafer, scope)}.
170     *
171     * @param clafer the Clafer
172     * @param scope the scope of the clafer
173     * @return a new builder
174     */
175    public static ScopeBuilder setScope(AstClafer clafer, int scope) {
176        return builder().setScope(clafer, scope);
177    }
178
179    /**
180     * Equivalent to {@code builder().defaultScope(defaultScope)}.
181     *
182     * @param defaultScope the default scope
183     * @return a new builder
184     */
185    public static ScopeBuilder defaultScope(int defaultScope) {
186        return builder().defaultScope(defaultScope);
187    }
188
189    /**
190     * Equivalent to {@code builder().intLow(intLow)}.
191     *
192     * @param intLow the lowest integer
193     * @return a new builder
194     */
195    public static ScopeBuilder intLow(int intLow) {
196        return builder().intLow(intLow);
197    }
198
199    /**
200     * Equivalent to {@code builder().intHigh(intHigh)}.
201     *
202     * @param intHigh the highest integer
203     * @return a new builder
204     */
205    public static ScopeBuilder intHigh(int intHigh) {
206        return builder().intHigh(intHigh);
207    }
208
209    /**
210     * {@inheritDoc}
211     */
212    @Override
213    public Scope toScope() {
214        return this;
215    }
216
217    public ScopeBuilder toBuilder() {
218        return new ScopeBuilder(scopes, defaultScope, intLow, intHigh);
219    }
220
221    /**
222     * {@inheritDoc}
223     */
224    @Override
225    public String toString() {
226        StringBuilder result = new StringBuilder().append('{');
227        result.append("default:").append(defaultScope);
228        for (Entry<AstClafer, Integer> entry : scopes.entrySet()) {
229            result.append(", ").append(entry.getKey()).append(':').append(entry.getValue());
230        }
231        return result.append('}').toString();
232    }
233}