Type Members

1.  class APIStack extends AnyRef
2.  class Evaluator extends AnyRef

   A class representing a first-order model of some formula.

   A class representing a first-order model of some formula. The class will internally start from the partial model computed by a SimpleAPI, and extend this model on demand. The class will make use of the SimpleAPI instance to compute missing parts of the model, and can therefore mutate the state of the SimpleAPI. To reset the SimpleAPI to the state before creating the Evaluator, use the method resetModelExtension; a safer way is to apply the method SimpleAPI.withCompleteModel to spawn the Evaluator.

3.  class PartialModel extends AnyRef

   Class representing (usually partial) models of formulas computed through the API.

   Class representing (usually partial) models of formulas computed through the API. Partial models represent values/individuals as constructor terms, in case of integers as instances of IIntLit

4.  class ProofThreadRunnable extends Runnable
5.  class SimpleAPI extends AnyRef

   API that simplifies the use of the prover; this tries to collect various functionality in one place, and provides an imperative API similar to the SMT-LIB command language.