blob: a85469cc67abe4aa3f8ee0875e2a0383d1b255ca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
(* Polymorphic First-Order Logic (that is Why's input logic) *)
type typ =
| Tvar of string
| Tid of string * typ list
type term =
| Cst of int
| Plus of term * term
| Moins of term * term
| Mult of term * term
| Div of term * term
| App of string * term list
and atom =
| Eq of term * term
| Le of term * term
| Lt of term * term
| Ge of term * term
| Gt of term * term
| Pred of string * term list
and form =
| Fatom of atom
| Imp of form * form
| Iff of form * form
| And of form * form
| Or of form * form
| Not of form
| Forall of string * typ * form
| Exists of string * typ * form
| True
| False
(* the integer indicates the number of type variables *)
type decl =
| DeclType of string * int
| DeclFun of string * int * typ list * typ
| DeclPred of string * int * typ list
| Axiom of string * form
type query = decl list * form
(* prover result *)
type prover_answer = Valid | Invalid | DontKnow | Timeout
|
