blob: 4fb763a6d1e69de1a330555cb7957ee0df90d194 (
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
49
50
51
52
53
54
55
56
57
58
|
(* Polymorphic First-Order Logic (that is Why's input logic) *)
type typ =
| Tvar of string
| Tid of string * typ list
type term =
| Cst of Big_int.big_int
| RCst of Big_int.big_int
| Power2 of Big_int.big_int
| Plus of term * term
| Moins of term * term
| Mult of term * term
| Div of term * term
| Opp of 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 of string option
| Invalid
| DontKnow
| Timeout
| NoAnswer
| Failure of string
|
