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<AstClafer, Integer> map = new HashMap<AstClafer, Integer>(); 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}