Up  

Module type Stmt_intf.Logic

module type Logic = sig .. end

Signature used by the Logic class, which parses languages such as tptp, smtlib, etc... Statements of dirrent languages currently have a lot less in common than terms, so this interface looks a lot more like a patchwork of different logical framework directives than it should.
type t
The type of statements.
type id
The type of identifiers.
type term
The type of terms used in statements.
type location
The type of locations attached to statements.

Optional infos for statements


val annot : ?loc:location ->
       term -> term list -> term
Constructors for annotations. Annotations are mainly used in TPTP.

Generic statements


val include_ : ?loc:location ->
       string -> id list -> t
Inlcude directive. include file l means to include in the current scope the directives from file file that appear in l. If l is the empty list, all directives should be imported.

Dimacs Statements


val clause : ?loc:location ->
       term list -> t
Add to the current set of assertions the given list of terms as a clause.

Smtlib statements


val pop : ?loc:location -> int -> t
val push : ?loc:location -> int -> t
Directives for manipulating the set of assertions. Push directives creates backtrack point that can be reached using Pop directives.
val assert_ : ?loc:location -> term -> t
Add an assertion to the current set of assertions.
val check_sat : ?loc:location -> unit -> t
Directive that instructs the prover to solve the current set of assertions.
val set_logic : ?loc:location -> string -> t
Set the logic to be used for solving.
val get_info : ?loc:location -> string -> t
val set_info : ?loc:location ->
       string * term option -> t
Getter and setter for various informations (see smtlib manual).
val get_option : ?loc:location -> string -> t
val set_option : ?loc:location ->
       string * term option -> t
Getter and setter for prover options (see smtlib manual).
val type_decl : ?loc:location ->
       id -> int -> t
Type declaration. type_decl s n declare s as a type constructor with arity n.
val type_def : ?loc:location ->
       id ->
       id list -> term -> t
Type definition. type_def f args body declare that f(args) = body, i.e any occurence of "f(l)" should be replaced by body where the "args" have been substituted by their corresponding value in l.
val fun_decl : ?loc:location ->
       id ->
       term list -> term -> t
Symbol declaration. fun_decl f args ret defines f as a function which takes arguments of type as described in args and which returns a value of type ret.
val fun_def : ?loc:location ->
       id ->
       term list ->
       term -> term -> t
Symbol definition. fun_def f args ret body means that "f(args) = (body : ret)", i.e f is a function symbol with arguments args, and which returns the value body which is of type ret.
val get_proof : ?loc:location -> unit -> t
If the last call to check_sat returned UNSAT, then instruct the prover to return the proof of unsat.
val get_unsat_core : ?loc:location -> unit -> t
If the last call to check_sat returned UNSAT, then instruct the prover to return the unsat core of the unsatisfiability proof, i.e the smallest set of assertions needed to prove false.
val get_value : ?loc:location ->
       term list -> t
Instructs the prover to return the values of the given closed quantifier-free terms.
val get_assignment : ?loc:location -> unit -> t
Instructs the prover to return truth assignemnt for labelled formulas (see smtlib manual for more information).
val get_assertions : ?loc:location -> unit -> t
Instructs the prover to print all current assertions.
val exit : ?loc:location -> unit -> t
Exit directive (used in interactive mode).

TPTP Statements


val tpi : ?loc:location ->
       ?annot:term ->
       id -> string -> term -> t
val thf : ?loc:location ->
       ?annot:term ->
       id -> string -> term -> t
val tff : ?loc:location ->
       ?annot:term ->
       id -> string -> term -> t
val fof : ?loc:location ->
       ?annot:term ->
       id -> string -> term -> t
val cnf : ?loc:location ->
       ?annot:term ->
       id -> string -> term -> t
TPTP directives. tptp name role t instructs the prover to register a new directive with the given name, role and term. Current tptp roles are:

Zipperposition statements


val inductive : ?loc:location ->
       id ->
       term list ->
       (id * term list) list -> t
Inductive type definitions. inductive name vars l defines aan inductive type name, with polymorphic variables vars, and with a list of inductive constructors l.
val data : ?loc:location -> t list -> t
Packs a list of mutually recursive inductive type declarations. into a single declaration.
val decl : ?loc:location ->
       id -> term -> t
Symbol declaration. decl name ty declares a new symbol name with type ty.
val definition : ?loc:location ->
       id ->
       term -> term -> t
Symbol definition. def name ty term defines a new symbol name of type ty which is equal to term.
val goal : ?loc:location ->
       ?attr:term -> term -> t
The goal, i.e the propositional formula to prove.
val assume : ?loc:location ->
       ?attr:term -> term -> t
Adds an hypothesis.
val rewrite : ?loc:location ->
       ?attr:term -> term -> t
Declare a rewrite rule, i.e a universally quantified equality or equivalence that can be oriented according to a specific ordering.