diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/dp/fol.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/dp/fol.mli')
-rw-r--r-- | plugins/dp/fol.mli | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/plugins/dp/fol.mli b/plugins/dp/fol.mli new file mode 100644 index 00000000..4fb763a6 --- /dev/null +++ b/plugins/dp/fol.mli @@ -0,0 +1,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 + |