A4Solution

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

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

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

public final class A4Solution
extends java.lang.Object
extends java.lang.Object

This class stores a SATISFIABLE or UNSATISFIABLE solution. It is also used as a staging area for the solver before generating the solution. Once solve() has been called, then this object becomes immutable after that.

Method Summary
`java.lang.String`	`debugExtractKInput()` Returns the Kodkod input used to generate this solution; returns "" if unknown.
`kodkod.instance.Instance`	`debugExtractKInstance()` Returns the Kodkod instance represented by this solution; throws an exception if the problem is not yet solved or if it is unsatisfiable.
`java.lang.Object`	`eval(Expr expr)` If this solution is solved and satisfiable, evaluates the given expression and returns an A4TupleSet, a java Integer, or a java Boolean.
`A4TupleSet`	`eval(Sig.Field field)` Return the A4TupleSet for the given field (if solution not yet solved, or unsatisfiable, or field not found, then return an empty tupleset)
`A4TupleSet`	`eval(Sig sig)` Return the A4TupleSet for the given sig (if solution not yet solved, or unsatisfiable, or sig not found, then return an empty tupleset)
`java.lang.Iterable<ExprVar>`	`getAllAtoms()` Returns an unmodifiable copy of the list of all atoms if the problem is solved and is satisfiable; else returns an empty list.
`SafeList<Sig>`	`getAllReachableSigs()` Returns an unmodifiable copy of the list of all sigs in this solution's model; always contains UNIV+SIGINT+SEQIDX+STRING+NONE and has no duplicates.
`java.lang.Iterable<ExprVar>`	`getAllSkolems()` Returns an unmodifiable copy of the list of all skolems if the problem is solved and is satisfiable; else returns an empty list.
`int`	`getBitwidth()` Returns the bitwidth; always between 1 and 30.
`int`	`getMaxSeq()` Returns the maximum allowed sequence length; always between 0 and 2^(bitwidth-1)-1.
`java.lang.String`	`getOriginalCommand()` Returns the original command that generated this solution; can be "" if unknown.
`java.lang.String`	`getOriginalFilename()` Returns the original Alloy file name that generated this solution; can be "" if unknown.
`Pair<java.util.Set<Pos>,java.util.Set<Pos>>`	`highLevelCore()` If this solution is unsatisfiable and its unsat core is available, then return the core; else return an empty set.
`boolean`	`isIncremental()` Returns true if this solution was generated by an incremental SAT solver.
`java.util.Set<Pos>`	`lowLevelCore()` If this solution is unsatisfiable and its unsat core is available, then return the core; else return an empty set.
`int`	`max()` Returns the largest allowed integer, or -1 if no integers are allowed.
`int`	`min()` Returns the smallest allowed integer, or 0 if no integers are allowed
`A4Solution`	`next()` If this solution is UNSAT, return itself; else return the next solution (which could be SAT or UNSAT).
`boolean`	`satisfiable()` Returns true iff the problem has been solved and the result is satisfiable.
`java.lang.String`	`toString()` Dumps the Kodkod solution into String.
`int`	`unrolls()` Returns the maximum number of allowed loop unrolling or recursion level.
`void`	`writeXML(A4Reporter rep, java.io.PrintWriter writer, java.lang.Iterable<Func> macros, java.util.Map<java.lang.String,java.lang.String> sourceFiles)` Helper method to write out a full XML file.
`void`	`writeXML(A4Reporter rep, java.lang.String filename, java.lang.Iterable<Func> macros, java.util.Map<java.lang.String,java.lang.String> sourceFiles)` Helper method to write out a full XML file.
`void`	`writeXML(java.io.PrintWriter writer, java.lang.Iterable<Func> macros, java.util.Map<java.lang.String,java.lang.String> sourceFiles)` Helper method to write out a full XML file.
`void`	`writeXML(java.lang.String filename)` Helper method to write out a full XML file.
`void`	`writeXML(java.lang.String filename, java.lang.Iterable<Func> macros)` Helper method to write out a full XML file.
`void`	`writeXML(java.lang.String filename, java.lang.Iterable<Func> macros, java.util.Map<java.lang.String,java.lang.String> sourceFiles)` Helper method to write out a full XML file.

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait`

Method Detail

getBitwidth

public int getBitwidth()

Returns the bitwidth; always between 1 and 30.

getMaxSeq

public int getMaxSeq()

Returns the maximum allowed sequence length; always between 0 and 2^(bitwidth-1)-1.

max

public int max()

Returns the largest allowed integer, or -1 if no integers are allowed.

min

public int min()

Returns the smallest allowed integer, or 0 if no integers are allowed

unrolls

public int unrolls()

Returns the maximum number of allowed loop unrolling or recursion level.

getOriginalFilename

public java.lang.String getOriginalFilename()

Returns the original Alloy file name that generated this solution; can be "" if unknown.

getOriginalCommand

public java.lang.String getOriginalCommand()

Returns the original command that generated this solution; can be "" if unknown.

debugExtractKInput

public java.lang.String debugExtractKInput()

Returns the Kodkod input used to generate this solution; returns "" if unknown.

satisfiable

public boolean satisfiable()

Returns true iff the problem has been solved and the result is satisfiable.

getAllReachableSigs

public SafeList<Sig> getAllReachableSigs()

Returns an unmodifiable copy of the list of all sigs in this solution's model; always contains UNIV+SIGINT+SEQIDX+STRING+NONE and has no duplicates.

getAllSkolems

public java.lang.Iterable<ExprVar> getAllSkolems()

Returns an unmodifiable copy of the list of all skolems if the problem is solved and is satisfiable; else returns an empty list.

getAllAtoms

public java.lang.Iterable<ExprVar> getAllAtoms()

Returns an unmodifiable copy of the list of all atoms if the problem is solved and is satisfiable; else returns an empty list.

eval

public A4TupleSet eval(Sig sig)

Return the A4TupleSet for the given sig (if solution not yet solved, or unsatisfiable, or sig not found, then return an empty tupleset)

eval

public A4TupleSet eval(Sig.Field field)

Return the A4TupleSet for the given field (if solution not yet solved, or unsatisfiable, or field not found, then return an empty tupleset)

eval

public java.lang.Object eval(Expr expr)
                      throws Err

If this solution is solved and satisfiable, evaluates the given expression and returns an A4TupleSet, a java Integer, or a java Boolean.

Throws:: Err

debugExtractKInstance

public kodkod.instance.Instance debugExtractKInstance()
                                               throws Err

Returns the Kodkod instance represented by this solution; throws an exception if the problem is not yet solved or if it is unsatisfiable.

Throws:: Err

toString

public java.lang.String toString()

Dumps the Kodkod solution into String.

Overrides:: toString in class java.lang.Object

public A4Solution next()
                throws Err

If this solution is UNSAT, return itself; else return the next solution (which could be SAT or UNSAT).

Throws:: ErrorAPI - if the solver was not an incremental solver; Err

isIncremental

public boolean isIncremental()

Returns true if this solution was generated by an incremental SAT solver.

lowLevelCore

public java.util.Set<Pos> lowLevelCore()

If this solution is unsatisfiable and its unsat core is available, then return the core; else return an empty set.

highLevelCore

public Pair<java.util.Set<Pos>,java.util.Set<Pos>> highLevelCore()

If this solution is unsatisfiable and its unsat core is available, then return the core; else return an empty set.