Inox API

February 18, 2021 ยท View on GitHub

Trees

Extendability is core to the design of the Inox AST (Abstract Syntax Tree). The Trees trait can be extended with new constructs and provide useful override points to enable extensions with new features. See Stainless for some concrete examples.

Identifiers

Inox uses the Identifier type to represent symbols in the program. Note that no type is attached to an instance of Identifier. Values and variables will attach a type to their identifier, and function invocations will rely on the symbol table to compute their type. See the Definitions section for more information on the symbol table.

Expressions

The classes defined here correspond to the base expressions supported by Inox. Inox can currently handle

  • Type parametric recursive higher-order functions (see Definitions and FunctionInvocation expression)
  • First-class functions (see Lambda and Application expressions)
  • Mathematical integer arithmetic
  • Bitvector arithmetic
  • Algebraic datatypes (see Definitions and ADT, ADTSelector expressions)
  • Strings
  • Sets / Multisets
  • Total maps
  • Quantifiers (see Forall)

Note that Strings, Sets / Multisets and Total maps can all be implemented using recursive and first-class functions in conjunction with ADTs. We list them here as Inox uses the underlying SMT solvers' native theory APIs for these constructs.

The relevant type definitions associated with these expressions can be found in Types.

Definitions

Inox uses two main types of definitions: functions and ADTs. These definitions are stored in a symbol table of type Symbols which is used to lookup identifiers during typing, solving and evaluation.

Functions

Functions here refer to named functions as opposition to anonymous ones (lambdas). Named functions can be recursive and support type-parametric polymorphism. A function definition is an instance of

class FunDef(
  val id: Identifier,                 /* The symbol associated with this function. */
  val tparams: Seq[TypeParameterDef], /* The function's type parameters. */
  val params: Seq[ValDef],            /* The function's formal arguments. */
  val returnType: Type,               /* The return type of this function. */
  val fullBody: Expr,                 /* The body of this function. */
  val flags: Set[Flag]                /* Annotations associated to this definition. */)

As mentioned above in the identifier section, ValDef associates a type with an identifier and has the following signature:

class ValDef(val id: Identifier, val tpe: Type, val flags: Set[Flag])

ADTs

Algebraic datatype definitions can be recursive and support type-parametric polymorphism, as in the named function case. An ADT can either correspond to a sort, or a constructor. Sorts can be seen as abstract classes with constructors resembling final case classes.

ADT sort definitions take place using the following class:

class ADTSort(
  val id: Identifier,                 /* The symbol associated with this ADT sort. */
  val tparams: Seq[TypeParameterDef], /* The ADT's type parameters. */
  val cons: Seq[ADTConstructor],      /* The sort's constructors. */
  val flags: Set[Flag]                /* Annotations associated to this definition. */)

Note that the sort contains the definitions of all its constructors.

ADT constructor definitions then take place using the class:

class ADTConstructor(
  val id: Identifier,                 /* The symbol associated with this ADT sort. */
  val sort: Identifier,               /* The symbol of the constructor's sort. */
  val fields: Seq[ValDef]             /* The fields associated to this constructor. */)

Inox provides the utility types TypedFunDef, TypedADTSort and TypedADTConstructor that respectively correspond to function and ADT definitions whose type parameters have been instantiated with concrete types. One can use these to access parameters/fields and enclosed expressions with instantiated types.

Programs

As mentioned above, Inox expressions only make sense with a corresponding symbol table. Furthermore, the expression/definition/type instances themselves require an instance of Trees to exist due to path-dependence. Inox wraps all these concerns into an instance of Program with the following signature

trait Program {
  /* The instance of Trees in which the expressions/defininitions/types of this program live. */
  val trees: Trees
  /* The symbol table to be used for function and ADT lookups in this program. */
  val symbols: Symbols
  /* Wrapper for options and reporter. */
  val ctx: Context
  ... (some other useful stuff) ...
}

In general, Inox uses programs to make its path-dependant API feasible and both solvers and evaluators are bound to some program instance.

When in possession of an InoxProgram (namely a Program { val trees: inox.trees.type }), one further gains access to the following extra API:

def getSolver: solvers.SolverFactory
def getSolver(opts: Options): solvers.SolverFactory
def getEvaluator: evaluators.DeterministicEvaluator
def getEvaluator(opts: Options): evaluators.DeterministicEvaluator

Solvers

Inox solvers offer the following main API methods:

Assert constraint

def assertCnstr(expr: Expr): Unit

Adds the boolean-typed expression expr to the set of constraints the solver is trying to satisfy.

Check

def check(config: Configuration): config.Response[Model,Assumptions]

Queries the solver to determine whether the current set of constraints that have been asserted is satisfiable. The check method takes a config argument that determines the exact modalities of the check (see SolverResponses). The four configurations are Simple, Model, UnsatAssumptions and All. The result of the check then depends on the actual configuration provided, namely

  1. Simple will result in either Sat, Unsat or Unknown
  2. Model will result in either SatWithModel(model), Unsat or Unknown
  3. UnsatAssumptions will result in either Sat, UnsatWithAssumptions(assumptions) or Unknown
  4. All will result in either SatWithModel(model), UnsatWithAssumptions(assumptions) or Unknown

The Model and Assumptions type parameters given to config.Response[Model,Assumptions] correspond respectively to the type of model in SatWithModel(model) and assumptions in UnsatWithAssumptions(assumptions). Note that typically, we have

type Model = Map[ValDef, Expr]
type Assumptions = Set[Expr]

The "Assumptions" cases that appear above actually cannot take place during a call to check but only during a call to checkAssumptions.

Check Assumptions

def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions]

Queries the solver to determine whether the current set of constraints is satisfiable assuming all assumptions hold as well. When the query is unsatisfiable, the solver will try to determine which expressions in the assumptions set were at fault and return them in the UnsatWithAssumptions(assumptions) result.

Evaluators

The evaluator API consists simply of an eval method with the following signature

def eval(expr: Expr, model: Map[ValDef, Expr]): EvaluationResult

where the evaluation result is either an instance of Successful(value) or corresponds to an evaluation error.