Options

Forge has a number of options that affect how it functions and how its solver is configured. They all have the same form: option <key> <value>. The available setting keys are:

Options

verbose: governs the amount of information provided in the REPL. 1 is standard; 0 will omit statistical information (useful for test suites); 10 will print exceedingly verbose debugging information. Values between 1 and 10 gradually increase verbosity

solver: sets the solver used by Forge's worker process. The default is SAT4J, a Java-based solver. The native solvers MiniSat and Glucose are often more performant. MiniSatProver will enable extraction of unsat cores.

logtranslation: controls how much of the translation from Forge to boolean logic is logged. The default is 0; must be 1 or higher to extract unsatisfiable cores.

coregranularity: controls how fine-grained an unsatisfiable core will be returned. Default is 0. Suggested value is 1 if you want to see cores.

core_minimization: controls whether cores are guaranteed minimal. Default is off. For minimal cores, use rce; hybrid is not guaranteed minimal but is often better than off while being faster than rce.

sb: controls maximum size of symmetry-breaking predicate. 20 is default. Higher numbers increase Forge's ability to rule out equivalent instances.

skolem_depth: gives how many layers of universal quantifiers to Skolemize past. Default is 0; to disable Skolemization, give -1.

(Some other undocumented options will be discussed later in class, at which point they'll be added.)

Location, Location, Location

Options do not apply globally, but rather only from the point they occur onward until either the file ends or the same setting is changed. For instance, only the second run command in this example will print verbose debugging information.

sig Node {edges: set Node}
run {} 
option verbose 10
run {} 
option verbose 1
run {}