org.clafer.scope

Class Scope

java.lang.Object

org.clafer.scope.Scope

All Implemented Interfaces:

Scopable

public class Scope
extends Object
implements Scopable

An immutable mapping from Clafers to their scope. Also contains the scope of integers for solving, like the bit-width in Alloy, but more flexible because the lowest and highest integers can be set independently and does not have to be a power of 2.

The scope is built through the constructor or ScopeBuilder, whichever is mort convenient.

Example 1:

 Map<AstClafer, Integer> map = new HashMap<AstClafer, Integer>();
 map.put(claferA, 3);
 map.put(claferB, 2);
 Scope scope = new Scope(map, 3, -16, 16);
 

Example 2:

 Scope scope = Scope.set(claferA, 3).set(claferB).defaultScope(3).intLow(-16).intHigh(16).toScope();
 

Both examples construct the same scope.

What is scope? Because of the expressiveness of Clafer, reasoning is too difficult in general. The scope is a limitation of the solver so that reasoning feasible.

Example 1:

 A : int
 B : int
 C : int
 [A * A * A + B * B * B = C * C * C]
 

Example 2:

 A *
 B *
 C *
 [#A * #A * #A + #B * #B * #B = #C * #C * #C]
 

Both examples are attempting to prove/disprove Fermat's last theorem for k=3, although this easily generalizes for any k. Unfortunately this is too difficult, so the solver only attempts to prove/disprove upto a certain scope. In example 1, a scope of Scope.intLow(-16).intHigh(16).toScope() would only attempt the proof for integers between negative and positive 16. In example 2, a scope of Scope.defaultScope(16).toScope() would only attempt the proof for integers between 0 and positive 16 (the example uses encodes integers using cardinality).

Author:

jimmy

See Also:

ScopeBuilder

Constructor Summary

Constructors

Constructor and Description
Scope(Map<AstClafer,Integer> scopes, int defaultScope, int intLow, int intHigh) Construct a new scope.

Method Summary

Methods

Modifier and Type	Method and Description
static ScopeBuilder	builder() Construct the scope using the builder pattern.
static ScopeBuilder	defaultScope(int defaultScope) Equivalent to builder().defaultScope(defaultScope).
int	getDefaultScope() The scope for unspecified Clafers.
int	getIntHigh() Returns the highest (inclusive) integer used for solving.
int	getIntLow() Returns the lowest (inclusive) integer used for solving.
int	getScope(AstClafer clafer) Returns the scope of the Clafer.
Set<AstClafer>	getScoped() Returns the set of Clafers that have an explicit scope.
static ScopeBuilder	intHigh(int intHigh) Equivalent to builder().intHigh(intHigh).
static ScopeBuilder	intLow(int intLow) Equivalent to builder().intLow(intLow).
static ScopeBuilder	setScope(AstClafer clafer, int scope) Equivalent to builder().setScope(clafer, scope).
ScopeBuilder	toBuilder()
Scope	toScope() Convert to scope.
String	toString()

Methods inherited from class java.lang.Object

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

Constructor Detail

Scope

public Scope(Map<AstClafer,Integer> scopes,
     int defaultScope,
     int intLow,
     int intHigh)

Construct a new scope. Altering the map has no affect once the scope is constructed.

Parameters:

scopes - a map of Clafers to their scopes

defaultScope - the scope for unspecified Clafers

intLow - the lowest (inclusive) integer used for solving

intHigh - the highest (inclusive) integer used for solving

Method Detail

getScoped

public Set<AstClafer> getScoped()

Returns the set of Clafers that have an explicit scope.

Returns:

the scoped Clafers

getScope

public int getScope(AstClafer clafer)

Returns the scope of the Clafer. If the Clafer is not specified a specific scope during the construction of this object, then the default scope is returned.

Parameters:

clafer - the Clafer

Returns:

the scope of the Clafer

getDefaultScope

public int getDefaultScope()

The scope for unspecified Clafers.

Returns:

the default scope

getIntLow

public int getIntLow()

Returns the lowest (inclusive) integer used for solving.

Returns:

the lowest integer

getIntHigh

public int getIntHigh()

Returns the highest (inclusive) integer used for solving.

Returns:

the highest integer

builder

public static ScopeBuilder builder()

Construct the scope using the builder pattern.

Returns:

a new builder

See Also:

ScopeBuilder

setScope

public static ScopeBuilder setScope(AstClafer clafer,
                    int scope)

Equivalent to builder().setScope(clafer, scope).

Parameters:

clafer - the Clafer

scope - the scope of the clafer

Returns:

a new builder

defaultScope

public static ScopeBuilder defaultScope(int defaultScope)

Equivalent to builder().defaultScope(defaultScope).

Parameters:

defaultScope - the default scope

Returns:

a new builder

intLow

public static ScopeBuilder intLow(int intLow)

Equivalent to builder().intLow(intLow).

Parameters:

intLow - the lowest integer

Returns:

a new builder

intHigh

public static ScopeBuilder intHigh(int intHigh)

Equivalent to builder().intHigh(intHigh).

Parameters:

intHigh - the highest integer

Returns:

a new builder

toScope

public Scope toScope()

Convert to scope.

Specified by:

toScope in interface Scopable

Returns:

the scope

toBuilder

public ScopeBuilder toBuilder()

toString

public String toString()

Overrides:

toString in class Object