package dolmen
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.
Optional infos for statements
Constructors for annotations. Annotations are mainly used in TPTP.
Generic statements
Import directive. Same as include_
but without filtering on the statements to import.
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.
Alt-ergo Statements
Functions type definition. Allows to specify whether a list of symbol is ac or not
Declares a new record type, with first a list of type variables, and then the list of the record fields.
Declare a new abstract type, quantified over the given list of type variables.
Defines a new algebraic datatype, quantified over the lsit of type variables, and with a list of cases each containing a constructor id and a list of fields.
Create a theory, extending another, with the given list of declarations.
Dimacs&iCNF Statements
Header of dimacs files. First argument is the number of variables, second is the number of clauses.
Add to the current set of assertions the given list of terms as a clause.
Solve the current set of assertions, with the given assumptions.
Smtlib statements
Directives for manipulating the set of assertions. Push directives creates backtrack point that can be reached using Pop directives.
Directive that instructs the prover to solve the current set of assertions, undr some local assumptions.
Type declaration. type_decl s n
declare s
as a type constructor with arity n
.
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
.
Inductive type definitions. TODO: some more documentation.
Symbol declaration. fun_decl f vars args ret
defines f
as a function which takes arguments of type as described in args
and which returns a value of type ret
.
Symbol definition. fun_def f vars 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
.
Define a list of mutually recursive functions. Each functions has the same definition as in fun_def
If the last call to check_sat
returned UNSAT, then instruct the prover to return the proof of unsat.
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
.
If the last call to check_sat
returned UNSAT, then instruct the prover to return a subset of the local assumptions that is sufficient to deduce UNSAT.
If the last call to check_sat
returned SAT, then return the associated model.
Instructs the prover to return the values of the given closed quantifier-free terms.
Instructs the prover to return truth assignemnt for labelled formulas (see smtlib manual for more information).
TPTP Statements
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:
"axiom", "hypothesis", "definition", "lemma", "theorem"
acts as new assertions/declartions"assumption", "conjecture"
are proposition that need to be proved, and then can be used to prove other propositions. They are equivalent to the following sequence of smtlib statements:push 1
assert (not t)
check_sat
pop 1
assert t
"negated_conjecture"
is the same as"conjecture"
, but the given proposition is false (i.e its negation is the proposition to prove)."type"
declares a new symbol and its type"plain", "unknown", "fi_domain", "fi_functors", "fi_predicates"
are valid roles with no specified semantics- any other role is an error
Zipperposition statements
Packs a list of mutually recursive inductive type declarations into a single statement.
Packs a list of mutually recursive definitions into a single statement.
Declare a rewrite rule, i.e a universally quantified equality or equivalence that can be oriented according to a specific ordering.
Symbol declaration. decl name ty
declares a new symbol name
with type ty
.
Symbol definition. def name ty term
defines a new symbol name
of type ty
which is equal to term
.