(* Title: Tools/Argo/argo_proof.ML
Author: Sascha Boehme
The proof language of the Argo solver.
Proofs trace the inferences of the solver. They can be used to check unsatisfiability results.
The proof language is inspired by:
Leonardo de Moura and Nikolaj Bjørner. Proofs and Refutations, and Z3. In
Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof
Assistants, and the 7th International Workshop on the Implementation of Logics,
volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008.
*)
signature ARGO_PROOF =
sig
(* types *)
type proof_id
datatype tautology =
Taut_And_1 of int | Taut_And_2 of int * int | Taut_Or_1 of int * int | Taut_Or_2 of int |
Taut_Iff_1 | Taut_Iff_2 | Taut_Iff_3 | Taut_Iff_4 | Taut_Ite_Then | Taut_Ite_Else
datatype side = Left | Right
datatype inequality = Le | Lt
datatype rewrite =
Rewr_Not_True | Rewr_Not_False | Rewr_Not_Not | Rewr_Not_And of int | Rewr_Not_Or of int |
Rewr_Not_Iff |
Rewr_And_False of int | Rewr_And_Dual of int * int | Rewr_And_Sort of int * int list list |
Rewr_Or_True of int | Rewr_Or_Dual of int * int | Rewr_Or_Sort of int * int list list |
Rewr_Iff_True | Rewr_Iff_False | Rewr_Iff_Not_Not | Rewr_Iff_Refl | Rewr_Iff_Symm |
Rewr_Iff_Dual |
Rewr_Imp | Rewr_Ite_Prop | Rewr_Ite_True | Rewr_Ite_False | Rewr_Ite_Eq |
Rewr_Eq_Refl | Rewr_Eq_Symm |
Rewr_Neg | Rewr_Add of (Rat.rat * int option) list * (Rat.rat * int option) list | Rewr_Sub |
Rewr_Mul_Nums of Rat.rat * Rat.rat | Rewr_Mul_Zero | Rewr_Mul_One | Rewr_Mul_Comm |
Rewr_Mul_Assoc of side | Rewr_Mul_Sum of side | Rewr_Mul_Div of side |
Rewr_Div_Zero | Rewr_Div_One | Rewr_Div_Nums of Rat.rat * Rat.rat |
Rewr_Div_Num of side * Rat.rat | Rewr_Div_Mul of side * Rat.rat | Rewr_Div_Div of side |
Rewr_Div_Sum | Rewr_Min_Eq | Rewr_Min_Lt | Rewr_Min_Gt | Rewr_Max_Eq | Rewr_Max_Lt |
Rewr_Max_Gt | Rewr_Abs | Rewr_Eq_Nums of bool | Rewr_Eq_Sub | Rewr_Eq_Le |
Rewr_Ineq_Nums of inequality * bool | Rewr_Ineq_Add of inequality * Rat.rat |
Rewr_Ineq_Sub of inequality | Rewr_Ineq_Mul of inequality * Rat.rat |
Rewr_Not_Ineq of inequality
datatype conv =
Keep_Conv | Then_Conv of conv * conv | Args_Conv of Argo_Expr.kind * conv list |
Rewr_Conv of rewrite
datatype rule =
Axiom of int | Taut of tautology * Argo_Expr.expr | Conjunct of int * int | Rewrite of conv |
Hyp of int * Argo_Expr.expr | Clause of int list | Lemma of int list | Unit_Res of int |
Refl of Argo_Expr.expr | Symm | Trans | Cong | Subst | Linear_Comb
type proof
(* equalities and orders *)
val eq_proof_id: proof_id * proof_id -> bool
val proof_id_ord: proof_id ord
(* conversion constructors *)
val keep_conv: conv
val mk_then_conv: conv -> conv -> conv
val mk_args_conv: Argo_Expr.kind -> conv list -> conv
val mk_rewr_conv: rewrite -> conv
(* context *)
type context
val cdcl_context: context
val cc_context: context
val simplex_context: context
val solver_context: context
(* proof constructors *)
val mk_axiom: int -> context -> proof * context
val mk_taut: tautology -> Argo_Expr.expr -> context -> proof * context
val mk_conj: int -> int -> proof -> context -> proof * context
val mk_rewrite: conv -> proof -> context -> proof * context
val mk_hyp: Argo_Lit.literal -> context -> proof * context
val mk_clause: Argo_Lit.literal list -> proof -> context -> proof * context
val mk_lemma: Argo_Lit.literal list -> proof -> context -> proof * context
val mk_unit_res: Argo_Lit.literal -> proof -> proof -> context -> proof * context
val mk_refl: Argo_Term.term -> context -> proof * context
val mk_symm: proof -> context -> proof * context
val mk_trans: proof -> proof -> context -> proof * context
val mk_cong: proof -> proof -> context -> proof * context
val mk_subst: proof -> proof -> proof -> context -> proof * context
val mk_linear_comb: proof list -> context -> proof * context
(* proof destructors *)
val id_of: proof -> proof_id
val dest: proof -> proof_id * rule * proof list
(* string representations *)
val string_of_proof_id: proof_id -> string
val string_of_taut: tautology -> string
val string_of_rule: rule -> string
(* unsatisfiability *)
exception UNSAT of proof
val unsat: proof -> 'a (* raises UNSAT *)
end
structure Argo_Proof: ARGO_PROOF =
struct
(* types *)
datatype tautology =
Taut_And_1 of int | Taut_And_2 of int * int | Taut_Or_1 of int * int | Taut_Or_2 of int |
Taut_Iff_1 | Taut_Iff_2 | Taut_Iff_3 | Taut_Iff_4 | Taut_Ite_Then | Taut_Ite_Else
datatype side = Left | Right
datatype inequality = Le | Lt
datatype rewrite =
Rewr_Not_True | Rewr_Not_False | Rewr_Not_Not | Rewr_Not_And of int | Rewr_Not_Or of int |
Rewr_Not_Iff |
Rewr_And_False of int | Rewr_And_Dual of int * int | Rewr_And_Sort of int * int list list |
Rewr_Or_True of int | Rewr_Or_Dual of int * int | Rewr_Or_Sort of int * int list list |
Rewr_Iff_True | Rewr_Iff_False | Rewr_Iff_Not_Not | Rewr_Iff_Refl | Rewr_Iff_Symm |
Rewr_Iff_Dual |
Rewr_Imp | Rewr_Ite_Prop | Rewr_Ite_True | Rewr_Ite_False | Rewr_Ite_Eq |
Rewr_Eq_Refl | Rewr_Eq_Symm |
Rewr_Neg | Rewr_Add of (Rat.rat * int option) list * (Rat.rat * int option) list | Rewr_Sub |
Rewr_Mul_Nums of Rat.rat * Rat.rat | Rewr_Mul_Zero | Rewr_Mul_One | Rewr_Mul_Comm |
Rewr_Mul_Assoc of side | Rewr_Mul_Sum of side | Rewr_Mul_Div of side |
Rewr_Div_Zero | Rewr_Div_One | Rewr_Div_Nums of Rat.rat * Rat.rat |
Rewr_Div_Num of side * Rat.rat | Rewr_Div_Mul of side * Rat.rat | Rewr_Div_Div of side |
Rewr_Div_Sum | Rewr_Min_Eq | Rewr_Min_Lt | Rewr_Min_Gt | Rewr_Max_Eq | Rewr_Max_Lt |
Rewr_Max_Gt | Rewr_Abs | Rewr_Eq_Nums of bool | Rewr_Eq_Sub | Rewr_Eq_Le |
Rewr_Ineq_Nums of inequality * bool | Rewr_Ineq_Add of inequality * Rat.rat |
Rewr_Ineq_Sub of inequality | Rewr_Ineq_Mul of inequality * Rat.rat |
Rewr_Not_Ineq of inequality
datatype conv =
Keep_Conv | Then_Conv of conv * conv | Args_Conv of Argo_Expr.kind * conv list |
Rewr_Conv of rewrite
datatype rule =
Axiom of int | Taut of tautology * Argo_Expr.expr | Conjunct of int * int | Rewrite of conv |
Hyp of int * Argo_Expr.expr | Clause of int list | Lemma of int list | Unit_Res of int |
Refl of Argo_Expr.expr | Symm | Trans | Cong | Subst | Linear_Comb
(*
Proof identifiers are intentially hidden to prevent that functions outside of this structure
are able to build proofs. Proof can hence only be built by the functions provided by
this structure.
*)
datatype proof_id = Cdcl of int | Cc of int | Simplex of int | Solver of int
datatype proof = Proof of proof_id * rule * proof list
(* internal functions *)
val proof_id_card = 4
fun raw_proof_id (Cdcl i) = i
| raw_proof_id (Cc i) = i
| raw_proof_id (Simplex i) = i
| raw_proof_id (Solver i) = i
(* equalities and orders *)
fun int_of_proof_id (Cdcl _) = 0
| int_of_proof_id (Cc _) = 1
| int_of_proof_id (Simplex _) = 2
| int_of_proof_id (Solver _) = 3
fun eq_proof_id (Cdcl i1, Cdcl i2) = (i1 = i2)
| eq_proof_id (Cc i1, Cc i2) = (i1 = i2)
| eq_proof_id (Simplex i1, Simplex i2) = (i1 = i2)
| eq_proof_id (Solver i1, Solver i2) = (i1 = i2)
| eq_proof_id _ = false
fun proof_id_ord (Cdcl i1, Cdcl i2) = int_ord (i1, i2)
| proof_id_ord (Cc i1, Cc i2) = int_ord (i1, i2)
| proof_id_ord (Simplex i1, Simplex i2) = int_ord (i1, i2)
| proof_id_ord (Solver i1, Solver i2) = int_ord (i1, i2)
| proof_id_ord (id1, id2) = int_ord (int_of_proof_id id1, int_of_proof_id id2)
(* conversion constructors *)
val keep_conv = Keep_Conv
fun mk_then_conv Keep_Conv c = c
| mk_then_conv c Keep_Conv = c
| mk_then_conv c1 c2 = Then_Conv (c1, c2)
fun mk_args_conv k cs =
if forall (fn Keep_Conv => true | _ => false) cs then Keep_Conv
else Args_Conv (k, cs)
fun mk_rewr_conv r = Rewr_Conv r
(* context *)
(*
The proof context stores the next unused identifier. Incidentally, the same type as
for the proof identifier can be used as context. Every proof-producing module of the
solver has its own proof identifier domain to ensure globally unique identifiers
without sharing a single proof context.
*)
type context = proof_id
val cdcl_context = Cdcl 0
val cc_context = Cc 0
val simplex_context = Simplex 0
val solver_context = Solver 0
fun next_id (id as Cdcl i) = (id, Cdcl (i + 1))
| next_id (id as Cc i) = (id, Cc (i + 1))
| next_id (id as Simplex i) = (id, Simplex (i + 1))
| next_id (id as Solver i) = (id, Solver (i + 1))
(* proof destructors *)
fun id_of (Proof (id, _, _)) = id
fun dest (Proof p) = p
(* proof constructors *)
fun mk_proof r ps cx =
let val (id, cx) = next_id cx
in (Proof (id, r, ps), cx) end
fun mk_axiom i = mk_proof (Axiom i) []
fun mk_taut t e = mk_proof (Taut (t, e)) []
fun mk_conj i n p = mk_proof (Conjunct (i, n)) [p]
fun mk_rewrite Keep_Conv p cx = (p, cx)
| mk_rewrite c p cx = mk_proof (Rewrite c) [p] cx
fun mk_hyp lit = mk_proof (Hyp (Argo_Lit.signed_id_of lit, Argo_Lit.signed_expr_of lit)) []
fun mk_clause lits p cx = mk_proof (Clause (map Argo_Lit.signed_id_of lits)) [p] cx
fun mk_lemma lits p = mk_proof (Lemma (map Argo_Lit.signed_id_of lits)) [p]
(*
Replay of unit-resolution steps can be optimized if all premises follow a specific form.
Therefore, each premise is checked if it is in clausal form.
*)
fun check_clause (p as Proof (_, Clause _, _)) = p
| check_clause (p as Proof (_, Lemma _, _)) = p
| check_clause (p as Proof (_, Unit_Res _, _)) = p
| check_clause _ = raise Fail "bad clause proof"
fun mk_unit t p1 p2 = mk_proof (Unit_Res (Argo_Term.id_of t)) (map check_clause [p1, p2])
fun mk_unit_res (Argo_Lit.Pos t) p1 p2 = mk_unit t p1 p2
| mk_unit_res (Argo_Lit.Neg t) p1 p2 = mk_unit t p2 p1
fun mk_refl t = mk_proof (Refl (Argo_Term.expr_of t)) []
fun mk_symm p = mk_proof Symm [p]
fun mk_trans (Proof (_, Refl _, _)) p2 = pair p2
| mk_trans p1 (Proof (_, Refl _, _)) = pair p1
| mk_trans p1 p2 = mk_proof Trans [p1, p2]
fun mk_cong p1 p2 = mk_proof Cong [p1, p2]
fun mk_subst p1 (Proof (_, Refl _, _)) (Proof (_, Refl _, _)) = pair p1
| mk_subst p1 p2 p3 = mk_proof Subst [p1, p2, p3]
fun mk_linear_comb ps = mk_proof Linear_Comb ps
(* string representations *)
fun string_of_proof_id id = string_of_int (proof_id_card * raw_proof_id id + int_of_proof_id id)
fun string_of_list l r f xs = enclose l r (space_implode ", " (map f xs))
fun parens f xs = string_of_list "(" ")" f xs
fun brackets f xs = string_of_list "[" "]" f xs
fun string_of_taut (Taut_And_1 n) = "and " ^ string_of_int n
| string_of_taut (Taut_And_2 (i, n)) = "and " ^ parens string_of_int [i, n]
| string_of_taut (Taut_Or_1 (i, n)) = "or " ^ parens string_of_int [i, n]
| string_of_taut (Taut_Or_2 n) = "or " ^ string_of_int n
| string_of_taut Taut_Iff_1 = "(p1 == p2) | p1 | p2"
| string_of_taut Taut_Iff_2 = "(p1 == p2) | ~p1 | ~p2"
| string_of_taut Taut_Iff_3 = "~(p1 == p2) | ~p1 | p2"
| string_of_taut Taut_Iff_4 = "~(p1 == p2) | p1 | ~p2"
| string_of_taut Taut_Ite_Then = "~p | (ite p t1 t2) = t1"
| string_of_taut Taut_Ite_Else = "p | (ite p t1 t2) = t2"
fun string_of_rewr Rewr_Not_True = "~T = F"
| string_of_rewr Rewr_Not_False = "~F = T"
| string_of_rewr Rewr_Not_Not = "~~p = p"
| string_of_rewr (Rewr_Not_And n) =
"~(and [" ^ string_of_int n ^ "]) = (or [" ^ string_of_int n ^ "])"
| string_of_rewr (Rewr_Not_Or n) =
"~(or [" ^ string_of_int n ^ "]) = (and [" ^ string_of_int n ^ "])"
| string_of_rewr Rewr_Not_Iff = "~(p1 == p2) = (~p1 == ~p2)"
| string_of_rewr (Rewr_And_False i) = "(and ... F(" ^ string_of_int i ^ ") ...) = F"
| string_of_rewr (Rewr_And_Dual (i1, i2)) =
"(and ... p(" ^ string_of_int i1 ^ ") ... ~p(" ^ string_of_int i2 ^ ") ...) = F"
| string_of_rewr (Rewr_And_Sort (n, iss)) =
"(and [" ^ string_of_int n ^ "]) = " ^
"(and " ^ brackets (brackets string_of_int) iss ^ ")"
| string_of_rewr (Rewr_Or_True i) = "(or ... T(" ^ string_of_int i ^ ") ...) = T"
| string_of_rewr (Rewr_Or_Dual (i1, i2)) =
"(or ... p(" ^ string_of_int i1 ^ ") ... ~p(" ^ string_of_int i2 ^ ") ...) = T"
| string_of_rewr (Rewr_Or_Sort (n, iss)) =
"(or [" ^ string_of_int n ^ "]) = " ^
"(or " ^ brackets (brackets string_of_int) iss ^ ")"
| string_of_rewr Rewr_Iff_True = "(p == T) = p"
| string_of_rewr Rewr_Iff_False = "(p == F) = ~p"
| string_of_rewr Rewr_Iff_Not_Not = "(~p1 == ~p2) = (p1 == p2)"
| string_of_rewr Rewr_Iff_Refl = "(p == p) = T"
| string_of_rewr Rewr_Iff_Symm = "(p1 == p2) = (p2 == p1)"
| string_of_rewr Rewr_Iff_Dual = "(p == ~p) = F"
| string_of_rewr Rewr_Imp = "(p1 --> p2) = (~p1 | p2)"
| string_of_rewr Rewr_Ite_Prop = "(if p1 p2 p2) = ((~p1 | p2) & (p1 | p3) & (p2 | p3))"
| string_of_rewr Rewr_Ite_True = "(if T t1 t2) = t1"
| string_of_rewr Rewr_Ite_False = "(if F t1 t2) = t2"
| string_of_rewr Rewr_Ite_Eq = "(if p t t) = t"
| string_of_rewr Rewr_Eq_Refl = "(e = e) = T"
| string_of_rewr Rewr_Eq_Symm = "(e1 = e2) = (e2 = e1)"
| string_of_rewr Rewr_Neg = "-e = -1 * e"
| string_of_rewr (Rewr_Add (p1, p2)) =
let
fun string_of_monom (n, NONE) = Rat.string_of_rat n
| string_of_monom (n, SOME i) =
(if n = @1 then "" else Rat.string_of_rat n ^ " * ") ^ "e" ^ string_of_int i
fun string_of_polynom ms = space_implode " + " (map string_of_monom ms)
in string_of_polynom p1 ^ " = " ^ string_of_polynom p2 end
| string_of_rewr Rewr_Sub = "e1 - e2 = e1 + -1 * e2"
| string_of_rewr (Rewr_Mul_Nums (n1, n2)) =
Rat.string_of_rat n1 ^ " * " ^ Rat.string_of_rat n2 ^ " = " ^ Rat.string_of_rat (n1 * n2)
| string_of_rewr Rewr_Mul_Zero = "0 * e = 0"
| string_of_rewr Rewr_Mul_One = "1 * e = e"
| string_of_rewr Rewr_Mul_Comm = "e1 * e2 = e2 * e1"
| string_of_rewr (Rewr_Mul_Assoc Left) = "(e1 * e2) * e3 = e1 * (e2 * e3)"
| string_of_rewr (Rewr_Mul_Assoc Right) = "e1 * (n * e2) = (e1 * n) * e2"
| string_of_rewr (Rewr_Mul_Sum Left) = "(e1 + ... + em) * e = e1 * e + ... em * e"
| string_of_rewr (Rewr_Mul_Sum Right) = "e * (e1 + ... + em) = e * e1 + ... e * em"
| string_of_rewr (Rewr_Mul_Div Left) = "(e1 / e2) * e3 = (e1 * e3) / e2"
| string_of_rewr (Rewr_Mul_Div Right) = "e1 * (e2 / * e3) = (e1 * e2) / e3"
| string_of_rewr Rewr_Div_Zero = "0 / e = 0"
| string_of_rewr Rewr_Div_One = "e / 1 = e"
| string_of_rewr (Rewr_Div_Nums (n1, n2)) =
Rat.string_of_rat n1 ^ " / " ^ Rat.string_of_rat n2 ^ " = " ^ Rat.string_of_rat (n1 / n2)
| string_of_rewr (Rewr_Div_Num (Left, n)) =
Rat.string_of_rat n ^ " / e = " ^ Rat.string_of_rat n ^ " * (1 / e)"
| string_of_rewr (Rewr_Div_Num (Right, n)) =
"e / " ^ Rat.string_of_rat n ^ " = " ^ Rat.string_of_rat (Rat.inv n) ^ " * e"
| string_of_rewr (Rewr_Div_Mul (Left, n)) =
"(" ^ Rat.string_of_rat n ^ " * e1) / e2 = " ^ Rat.string_of_rat n ^ " * (e1 / e2)"
| string_of_rewr (Rewr_Div_Mul (Right, n)) =
"e1 / (" ^ Rat.string_of_rat n ^ " * e2) = " ^ Rat.string_of_rat (Rat.inv n) ^ " * (e1 / e2)"
| string_of_rewr (Rewr_Div_Div Left) = "(e1 / e2) / e3 = e1 / (e2 * e3)"
| string_of_rewr (Rewr_Div_Div Right) = "e1 / (e2 / e3) = (e1 * e3) / e2"
| string_of_rewr Rewr_Div_Sum = "(e1 + ... + em) / e = e1 / e + ... + em / e"
| string_of_rewr Rewr_Min_Eq = "min e e = e"
| string_of_rewr Rewr_Min_Lt = "min e1 e2 = (if e1 <= e2 then e1 else e2)"
| string_of_rewr Rewr_Min_Gt = "min e1 e2 = (if e2 <= e1 then e2 else e1)"
| string_of_rewr Rewr_Max_Eq = "max e e = e"
| string_of_rewr Rewr_Max_Lt = "max e1 e2 = (if e1 < e2 then e2 else e1)"
| string_of_rewr Rewr_Max_Gt = "max e1 e2 = (if e2 < e1 then e1 else e2)"
| string_of_rewr Rewr_Abs = "abs e = (if 0 <= e then e else -e)"
| string_of_rewr (Rewr_Eq_Nums true) = "(n1 = n2) = true"
| string_of_rewr (Rewr_Eq_Nums false) = "(n1 ~= n2) = false"
| string_of_rewr Rewr_Eq_Sub = "(e1 = e2) = (e1 - e2 = 0)"
| string_of_rewr Rewr_Eq_Le = "(e1 = e2) = (and (e1 <= e2) (e2 <= e1))"
| string_of_rewr (Rewr_Ineq_Nums (Le, true)) = "(n1 <= n2) = true"
| string_of_rewr (Rewr_Ineq_Nums (Le, false)) = "(n1 <= n2) = false"
| string_of_rewr (Rewr_Ineq_Nums (Lt, true)) = "(n1 < n2) = true"
| string_of_rewr (Rewr_Ineq_Nums (Lt, false)) = "(n1 < n2) = false"
| string_of_rewr (Rewr_Ineq_Add (Le, _)) = "(e1 <= e2) = (e1 + n <= e2 + n)"
| string_of_rewr (Rewr_Ineq_Add (Lt, _)) = "(e1 < e2) = (e1 + n < e2 + n)"
| string_of_rewr (Rewr_Ineq_Sub Le) = "(e1 <= e2) = (e1 - e2 <= 0)"
| string_of_rewr (Rewr_Ineq_Sub Lt) = "(e1 < e2) = (e1 - e2 < 0)"
| string_of_rewr (Rewr_Ineq_Mul (Le, _)) = "(e1 <= e2) = (n * e1 <= n * e2)"
| string_of_rewr (Rewr_Ineq_Mul (Lt, _)) = "(e1 < e2) = (n * e1 < n * e2)"
| string_of_rewr (Rewr_Not_Ineq Le) = "~(e1 <= e2) = (e2 < e1)"
| string_of_rewr (Rewr_Not_Ineq Lt) = "~(e1 < e2) = (e2 <= e1)"
fun flatten_then_conv (Then_Conv (c1, c2)) = flatten_then_conv c1 @ flatten_then_conv c2
| flatten_then_conv c = [c]
fun string_of_conv Keep_Conv = "_"
| string_of_conv (c as Then_Conv _) =
space_implode " then " (map (enclose "(" ")" o string_of_conv) (flatten_then_conv c))
| string_of_conv (Args_Conv (k, cs)) =
"args " ^ Argo_Expr.string_of_kind k ^ " " ^ brackets string_of_conv cs
| string_of_conv (Rewr_Conv r) = string_of_rewr r
fun string_of_rule (Axiom i) = "axiom " ^ string_of_int i
| string_of_rule (Taut (t, _)) = "tautology: " ^ string_of_taut t
| string_of_rule (Conjunct (i, n)) = "conjunct " ^ string_of_int i ^ " of " ^ string_of_int n
| string_of_rule (Rewrite c) = "rewrite: " ^ string_of_conv c
| string_of_rule (Hyp (i, _)) = "hypothesis " ^ string_of_int i
| string_of_rule (Clause is) = "clause " ^ brackets string_of_int is
| string_of_rule (Lemma is) = "lemma " ^ brackets string_of_int is
| string_of_rule (Unit_Res i) = "unit-resolution " ^ string_of_int i
| string_of_rule (Refl _) = "reflexivity"
| string_of_rule Symm = "symmetry"
| string_of_rule Trans = "transitivity"
| string_of_rule Cong = "congruence"
| string_of_rule Subst = "substitution"
| string_of_rule Linear_Comb = "linear-combination"
(* unsatisfiability *)
exception UNSAT of proof
fun unsat p = raise UNSAT p
end