package dolmen
Implementation requirement for the Smtlib format.
(Re)starting and terminating
Modifying the assertion stack
Introducing new symbols
Defines an alias for types. type_def f args body
is such that later occurences of f
applied to a list of arguments l
should be replaced by body
where the args
have been substituted by their value in l
.
Inductive type definitions.
Declares a new term symbol, and its type. fun_decl f ty_args args ret
declares f
as a new function symbol which takes arguments of types described in args
, and with return type ret
.
Defines a new function. fun_def f ty_args args ret body
is such that applications of f
are equal to body
(module substitution of the arguments), which should be of type ret
.
Declare a list of mutually recursive functions.
Asserting and inspecting formulas
Checking for satisfiablity
Solve the current set of assertions for satisfiability, under the local assumptions specified.
Models
Return the value of the given terms in the current model of the solver.
Return the values of asserted propositions which have been labelled using the ":named" attribute.
Proofs
Return the proof of the lastest check_sat
if it returned unsat, else is undefined.
Return the unsat core of the latest check_sat
if it returned unsat, else is undefined.
Return a list of local assumptions (as givne in check_sat
, that is enough to deduce unsat.
Inspecting settings
Scripts commands