1(* Title: Tools/Argo/argo_proof.ML 2 Author: Sascha Boehme 3 4The proof language of the Argo solver. 5 6Proofs trace the inferences of the solver. They can be used to check unsatisfiability results. 7 8The proof language is inspired by: 9 10 Leonardo de Moura and Nikolaj Bj/orner. Proofs and Refutations, and Z3. In 11 Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof 12 Assistants, and the 7th International Workshop on the Implementation of Logics, 13 volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. 14*) 15 16signature ARGO_PROOF = 17sig 18 (* types *) 19 type proof_id 20 datatype tautology = 21 Taut_And_1 of int | Taut_And_2 of int * int | Taut_Or_1 of int * int | Taut_Or_2 of int | 22 Taut_Iff_1 | Taut_Iff_2 | Taut_Iff_3 | Taut_Iff_4 | Taut_Ite_Then | Taut_Ite_Else 23 datatype side = Left | Right 24 datatype inequality = Le | Lt 25 datatype rewrite = 26 Rewr_Not_True | Rewr_Not_False | Rewr_Not_Not | Rewr_Not_And of int | Rewr_Not_Or of int | 27 Rewr_Not_Iff | 28 Rewr_And_False of int | Rewr_And_Dual of int * int | Rewr_And_Sort of int * int list list | 29 Rewr_Or_True of int | Rewr_Or_Dual of int * int | Rewr_Or_Sort of int * int list list | 30 Rewr_Iff_True | Rewr_Iff_False | Rewr_Iff_Not_Not | Rewr_Iff_Refl | Rewr_Iff_Symm | 31 Rewr_Iff_Dual | 32 Rewr_Imp | Rewr_Ite_Prop | Rewr_Ite_True | Rewr_Ite_False | Rewr_Ite_Eq | 33 Rewr_Eq_Refl | Rewr_Eq_Symm | 34 Rewr_Neg | Rewr_Add of (Rat.rat * int option) list * (Rat.rat * int option) list | Rewr_Sub | 35 Rewr_Mul_Nums of Rat.rat * Rat.rat | Rewr_Mul_Zero | Rewr_Mul_One | Rewr_Mul_Comm | 36 Rewr_Mul_Assoc of side | Rewr_Mul_Sum of side | Rewr_Mul_Div of side | 37 Rewr_Div_Zero | Rewr_Div_One | Rewr_Div_Nums of Rat.rat * Rat.rat | 38 Rewr_Div_Num of side * Rat.rat | Rewr_Div_Mul of side * Rat.rat | Rewr_Div_Div of side | 39 Rewr_Div_Sum | Rewr_Min_Eq | Rewr_Min_Lt | Rewr_Min_Gt | Rewr_Max_Eq | Rewr_Max_Lt | 40 Rewr_Max_Gt | Rewr_Abs | Rewr_Eq_Nums of bool | Rewr_Eq_Sub | Rewr_Eq_Le | 41 Rewr_Ineq_Nums of inequality * bool | Rewr_Ineq_Add of inequality * Rat.rat | 42 Rewr_Ineq_Sub of inequality | Rewr_Ineq_Mul of inequality * Rat.rat | 43 Rewr_Not_Ineq of inequality 44 datatype conv = 45 Keep_Conv | Then_Conv of conv * conv | Args_Conv of Argo_Expr.kind * conv list | 46 Rewr_Conv of rewrite 47 datatype rule = 48 Axiom of int | Taut of tautology * Argo_Expr.expr | Conjunct of int * int | Rewrite of conv | 49 Hyp of int * Argo_Expr.expr | Clause of int list | Lemma of int list | Unit_Res of int | 50 Refl of Argo_Expr.expr | Symm | Trans | Cong | Subst | Linear_Comb 51 type proof 52 53 (* equalities and orders *) 54 val eq_proof_id: proof_id * proof_id -> bool 55 val proof_id_ord: proof_id * proof_id -> order 56 57 (* conversion constructors *) 58 val keep_conv: conv 59 val mk_then_conv: conv -> conv -> conv 60 val mk_args_conv: Argo_Expr.kind -> conv list -> conv 61 val mk_rewr_conv: rewrite -> conv 62 63 (* context *) 64 type context 65 val cdcl_context: context 66 val cc_context: context 67 val simplex_context: context 68 val solver_context: context 69 70 (* proof constructors *) 71 val mk_axiom: int -> context -> proof * context 72 val mk_taut: tautology -> Argo_Expr.expr -> context -> proof * context 73 val mk_conj: int -> int -> proof -> context -> proof * context 74 val mk_rewrite: conv -> proof -> context -> proof * context 75 val mk_hyp: Argo_Lit.literal -> context -> proof * context 76 val mk_clause: Argo_Lit.literal list -> proof -> context -> proof * context 77 val mk_lemma: Argo_Lit.literal list -> proof -> context -> proof * context 78 val mk_unit_res: Argo_Lit.literal -> proof -> proof -> context -> proof * context 79 val mk_refl: Argo_Term.term -> context -> proof * context 80 val mk_symm: proof -> context -> proof * context 81 val mk_trans: proof -> proof -> context -> proof * context 82 val mk_cong: proof -> proof -> context -> proof * context 83 val mk_subst: proof -> proof -> proof -> context -> proof * context 84 val mk_linear_comb: proof list -> context -> proof * context 85 86 (* proof destructors *) 87 val id_of: proof -> proof_id 88 val dest: proof -> proof_id * rule * proof list 89 90 (* string representations *) 91 val string_of_proof_id: proof_id -> string 92 val string_of_taut: tautology -> string 93 val string_of_rule: rule -> string 94 95 (* unsatisfiability *) 96 exception UNSAT of proof 97 val unsat: proof -> 'a (* raises UNSAT *) 98end 99 100structure Argo_Proof: ARGO_PROOF = 101struct 102 103(* types *) 104 105datatype tautology = 106 Taut_And_1 of int | Taut_And_2 of int * int | Taut_Or_1 of int * int | Taut_Or_2 of int | 107 Taut_Iff_1 | Taut_Iff_2 | Taut_Iff_3 | Taut_Iff_4 | Taut_Ite_Then | Taut_Ite_Else 108 109datatype side = Left | Right 110 111datatype inequality = Le | Lt 112 113datatype rewrite = 114 Rewr_Not_True | Rewr_Not_False | Rewr_Not_Not | Rewr_Not_And of int | Rewr_Not_Or of int | 115 Rewr_Not_Iff | 116 Rewr_And_False of int | Rewr_And_Dual of int * int | Rewr_And_Sort of int * int list list | 117 Rewr_Or_True of int | Rewr_Or_Dual of int * int | Rewr_Or_Sort of int * int list list | 118 Rewr_Iff_True | Rewr_Iff_False | Rewr_Iff_Not_Not | Rewr_Iff_Refl | Rewr_Iff_Symm | 119 Rewr_Iff_Dual | 120 Rewr_Imp | Rewr_Ite_Prop | Rewr_Ite_True | Rewr_Ite_False | Rewr_Ite_Eq | 121 Rewr_Eq_Refl | Rewr_Eq_Symm | 122 Rewr_Neg | Rewr_Add of (Rat.rat * int option) list * (Rat.rat * int option) list | Rewr_Sub | 123 Rewr_Mul_Nums of Rat.rat * Rat.rat | Rewr_Mul_Zero | Rewr_Mul_One | Rewr_Mul_Comm | 124 Rewr_Mul_Assoc of side | Rewr_Mul_Sum of side | Rewr_Mul_Div of side | 125 Rewr_Div_Zero | Rewr_Div_One | Rewr_Div_Nums of Rat.rat * Rat.rat | 126 Rewr_Div_Num of side * Rat.rat | Rewr_Div_Mul of side * Rat.rat | Rewr_Div_Div of side | 127 Rewr_Div_Sum | Rewr_Min_Eq | Rewr_Min_Lt | Rewr_Min_Gt | Rewr_Max_Eq | Rewr_Max_Lt | 128 Rewr_Max_Gt | Rewr_Abs | Rewr_Eq_Nums of bool | Rewr_Eq_Sub | Rewr_Eq_Le | 129 Rewr_Ineq_Nums of inequality * bool | Rewr_Ineq_Add of inequality * Rat.rat | 130 Rewr_Ineq_Sub of inequality | Rewr_Ineq_Mul of inequality * Rat.rat | 131 Rewr_Not_Ineq of inequality 132 133datatype conv = 134 Keep_Conv | Then_Conv of conv * conv | Args_Conv of Argo_Expr.kind * conv list | 135 Rewr_Conv of rewrite 136 137datatype rule = 138 Axiom of int | Taut of tautology * Argo_Expr.expr | Conjunct of int * int | Rewrite of conv | 139 Hyp of int * Argo_Expr.expr | Clause of int list | Lemma of int list | Unit_Res of int | 140 Refl of Argo_Expr.expr | Symm | Trans | Cong | Subst | Linear_Comb 141 142(* 143 Proof identifiers are intentially hidden to prevent that functions outside of this structure 144 are able to build proofs. Proof can hence only be built by the functions provided by 145 this structure. 146*) 147 148datatype proof_id = Cdcl of int | Cc of int | Simplex of int | Solver of int 149 150datatype proof = Proof of proof_id * rule * proof list 151 152 153(* internal functions *) 154 155val proof_id_card = 4 156 157fun raw_proof_id (Cdcl i) = i 158 | raw_proof_id (Cc i) = i 159 | raw_proof_id (Simplex i) = i 160 | raw_proof_id (Solver i) = i 161 162 163(* equalities and orders *) 164 165fun int_of_proof_id (Cdcl _) = 0 166 | int_of_proof_id (Cc _) = 1 167 | int_of_proof_id (Simplex _) = 2 168 | int_of_proof_id (Solver _) = 3 169 170fun eq_proof_id (Cdcl i1, Cdcl i2) = (i1 = i2) 171 | eq_proof_id (Cc i1, Cc i2) = (i1 = i2) 172 | eq_proof_id (Simplex i1, Simplex i2) = (i1 = i2) 173 | eq_proof_id (Solver i1, Solver i2) = (i1 = i2) 174 | eq_proof_id _ = false 175 176fun proof_id_ord (Cdcl i1, Cdcl i2) = int_ord (i1, i2) 177 | proof_id_ord (Cc i1, Cc i2) = int_ord (i1, i2) 178 | proof_id_ord (Simplex i1, Simplex i2) = int_ord (i1, i2) 179 | proof_id_ord (Solver i1, Solver i2) = int_ord (i1, i2) 180 | proof_id_ord (id1, id2) = int_ord (int_of_proof_id id1, int_of_proof_id id2) 181 182 183(* conversion constructors *) 184 185val keep_conv = Keep_Conv 186 187fun mk_then_conv Keep_Conv c = c 188 | mk_then_conv c Keep_Conv = c 189 | mk_then_conv c1 c2 = Then_Conv (c1, c2) 190 191fun mk_args_conv k cs = 192 if forall (fn Keep_Conv => true | _ => false) cs then Keep_Conv 193 else Args_Conv (k, cs) 194 195fun mk_rewr_conv r = Rewr_Conv r 196 197 198(* context *) 199 200(* 201 The proof context stores the next unused identifier. Incidentally, the same type as 202 for the proof identifier can be used as context. Every proof-producing module of the 203 solver has its own proof identifier domain to ensure globally unique identifiers 204 without sharing a single proof context. 205*) 206 207type context = proof_id 208 209val cdcl_context = Cdcl 0 210val cc_context = Cc 0 211val simplex_context = Simplex 0 212val solver_context = Solver 0 213 214fun next_id (id as Cdcl i) = (id, Cdcl (i + 1)) 215 | next_id (id as Cc i) = (id, Cc (i + 1)) 216 | next_id (id as Simplex i) = (id, Simplex (i + 1)) 217 | next_id (id as Solver i) = (id, Solver (i + 1)) 218 219 220(* proof destructors *) 221 222fun id_of (Proof (id, _, _)) = id 223 224fun dest (Proof p) = p 225 226 227(* proof constructors *) 228 229fun mk_proof r ps cx = 230 let val (id, cx) = next_id cx 231 in (Proof (id, r, ps), cx) end 232 233fun mk_axiom i = mk_proof (Axiom i) [] 234fun mk_taut t e = mk_proof (Taut (t, e)) [] 235fun mk_conj i n p = mk_proof (Conjunct (i, n)) [p] 236 237fun mk_rewrite Keep_Conv p cx = (p, cx) 238 | mk_rewrite c p cx = mk_proof (Rewrite c) [p] cx 239 240fun mk_hyp lit = mk_proof (Hyp (Argo_Lit.signed_id_of lit, Argo_Lit.signed_expr_of lit)) [] 241fun mk_clause lits p cx = mk_proof (Clause (map Argo_Lit.signed_id_of lits)) [p] cx 242fun mk_lemma lits p = mk_proof (Lemma (map Argo_Lit.signed_id_of lits)) [p] 243 244(* 245 Replay of unit-resolution steps can be optimized if all premises follow a specific form. 246 Therefore, each premise is checked if it is in clausal form. 247*) 248 249fun check_clause (p as Proof (_, Clause _, _)) = p 250 | check_clause (p as Proof (_, Lemma _, _)) = p 251 | check_clause (p as Proof (_, Unit_Res _, _)) = p 252 | check_clause _ = raise Fail "bad clause proof" 253 254fun mk_unit t p1 p2 = mk_proof (Unit_Res (Argo_Term.id_of t)) (map check_clause [p1, p2]) 255 256fun mk_unit_res (Argo_Lit.Pos t) p1 p2 = mk_unit t p1 p2 257 | mk_unit_res (Argo_Lit.Neg t) p1 p2 = mk_unit t p2 p1 258 259fun mk_refl t = mk_proof (Refl (Argo_Term.expr_of t)) [] 260fun mk_symm p = mk_proof Symm [p] 261 262fun mk_trans (Proof (_, Refl _, _)) p2 = pair p2 263 | mk_trans p1 (Proof (_, Refl _, _)) = pair p1 264 | mk_trans p1 p2 = mk_proof Trans [p1, p2] 265 266fun mk_cong p1 p2 = mk_proof Cong [p1, p2] 267 268fun mk_subst p1 (Proof (_, Refl _, _)) (Proof (_, Refl _, _)) = pair p1 269 | mk_subst p1 p2 p3 = mk_proof Subst [p1, p2, p3] 270 271fun mk_linear_comb ps = mk_proof Linear_Comb ps 272 273 274(* string representations *) 275 276fun string_of_proof_id id = string_of_int (proof_id_card * raw_proof_id id + int_of_proof_id id) 277 278fun string_of_list l r f xs = enclose l r (space_implode ", " (map f xs)) 279fun parens f xs = string_of_list "(" ")" f xs 280fun brackets f xs = string_of_list "[" "]" f xs 281 282fun string_of_taut (Taut_And_1 n) = "and " ^ string_of_int n 283 | string_of_taut (Taut_And_2 (i, n)) = "and " ^ parens string_of_int [i, n] 284 | string_of_taut (Taut_Or_1 (i, n)) = "or " ^ parens string_of_int [i, n] 285 | string_of_taut (Taut_Or_2 n) = "or " ^ string_of_int n 286 | string_of_taut Taut_Iff_1 = "(p1 == p2) | p1 | p2" 287 | string_of_taut Taut_Iff_2 = "(p1 == p2) | ~p1 | ~p2" 288 | string_of_taut Taut_Iff_3 = "~(p1 == p2) | ~p1 | p2" 289 | string_of_taut Taut_Iff_4 = "~(p1 == p2) | p1 | ~p2" 290 | string_of_taut Taut_Ite_Then = "~p | (ite p t1 t2) = t1" 291 | string_of_taut Taut_Ite_Else = "p | (ite p t1 t2) = t2" 292 293fun string_of_rewr Rewr_Not_True = "~T = F" 294 | string_of_rewr Rewr_Not_False = "~F = T" 295 | string_of_rewr Rewr_Not_Not = "~~p = p" 296 | string_of_rewr (Rewr_Not_And n) = 297 "~(and [" ^ string_of_int n ^ "]) = (or [" ^ string_of_int n ^ "])" 298 | string_of_rewr (Rewr_Not_Or n) = 299 "~(or [" ^ string_of_int n ^ "]) = (and [" ^ string_of_int n ^ "])" 300 | string_of_rewr Rewr_Not_Iff = "~(p1 == p2) = (~p1 == ~p2)" 301 | string_of_rewr (Rewr_And_False i) = "(and ... F(" ^ string_of_int i ^ ") ...) = F" 302 | string_of_rewr (Rewr_And_Dual (i1, i2)) = 303 "(and ... p(" ^ string_of_int i1 ^ ") ... ~p(" ^ string_of_int i2 ^ ") ...) = F" 304 | string_of_rewr (Rewr_And_Sort (n, iss)) = 305 "(and [" ^ string_of_int n ^ "]) = " ^ 306 "(and " ^ brackets (brackets string_of_int) iss ^ ")" 307 | string_of_rewr (Rewr_Or_True i) = "(or ... T(" ^ string_of_int i ^ ") ...) = T" 308 | string_of_rewr (Rewr_Or_Dual (i1, i2)) = 309 "(or ... p(" ^ string_of_int i1 ^ ") ... ~p(" ^ string_of_int i2 ^ ") ...) = T" 310 | string_of_rewr (Rewr_Or_Sort (n, iss)) = 311 "(or [" ^ string_of_int n ^ "]) = " ^ 312 "(or " ^ brackets (brackets string_of_int) iss ^ ")" 313 | string_of_rewr Rewr_Iff_True = "(p == T) = p" 314 | string_of_rewr Rewr_Iff_False = "(p == F) = ~p" 315 | string_of_rewr Rewr_Iff_Not_Not = "(~p1 == ~p2) = (p1 == p2)" 316 | string_of_rewr Rewr_Iff_Refl = "(p == p) = T" 317 | string_of_rewr Rewr_Iff_Symm = "(p1 == p2) = (p2 == p1)" 318 | string_of_rewr Rewr_Iff_Dual = "(p == ~p) = F" 319 | string_of_rewr Rewr_Imp = "(p1 --> p2) = (~p1 | p2)" 320 | string_of_rewr Rewr_Ite_Prop = "(if p1 p2 p2) = ((~p1 | p2) & (p1 | p3) & (p2 | p3))" 321 | string_of_rewr Rewr_Ite_True = "(if T t1 t2) = t1" 322 | string_of_rewr Rewr_Ite_False = "(if F t1 t2) = t2" 323 | string_of_rewr Rewr_Ite_Eq = "(if p t t) = t" 324 | string_of_rewr Rewr_Eq_Refl = "(e = e) = T" 325 | string_of_rewr Rewr_Eq_Symm = "(e1 = e2) = (e2 = e1)" 326 | string_of_rewr Rewr_Neg = "-e = -1 * e" 327 | string_of_rewr (Rewr_Add (p1, p2)) = 328 let 329 fun string_of_monom (n, NONE) = Rat.string_of_rat n 330 | string_of_monom (n, SOME i) = 331 (if n = @1 then "" else Rat.string_of_rat n ^ " * ") ^ "e" ^ string_of_int i 332 fun string_of_polynom ms = space_implode " + " (map string_of_monom ms) 333 in string_of_polynom p1 ^ " = " ^ string_of_polynom p2 end 334 | string_of_rewr Rewr_Sub = "e1 - e2 = e1 + -1 * e2" 335 | string_of_rewr (Rewr_Mul_Nums (n1, n2)) = 336 Rat.string_of_rat n1 ^ " * " ^ Rat.string_of_rat n2 ^ " = " ^ Rat.string_of_rat (n1 * n2) 337 | string_of_rewr Rewr_Mul_Zero = "0 * e = 0" 338 | string_of_rewr Rewr_Mul_One = "1 * e = e" 339 | string_of_rewr Rewr_Mul_Comm = "e1 * e2 = e2 * e1" 340 | string_of_rewr (Rewr_Mul_Assoc Left) = "(e1 * e2) * e3 = e1 * (e2 * e3)" 341 | string_of_rewr (Rewr_Mul_Assoc Right) = "e1 * (n * e2) = (e1 * n) * e2" 342 | string_of_rewr (Rewr_Mul_Sum Left) = "(e1 + ... + em) * e = e1 * e + ... em * e" 343 | string_of_rewr (Rewr_Mul_Sum Right) = "e * (e1 + ... + em) = e * e1 + ... e * em" 344 | string_of_rewr (Rewr_Mul_Div Left) = "(e1 / e2) * e3 = (e1 * e3) / e2" 345 | string_of_rewr (Rewr_Mul_Div Right) = "e1 * (e2 / * e3) = (e1 * e2) / e3" 346 | string_of_rewr Rewr_Div_Zero = "0 / e = 0" 347 | string_of_rewr Rewr_Div_One = "e / 1 = e" 348 | string_of_rewr (Rewr_Div_Nums (n1, n2)) = 349 Rat.string_of_rat n1 ^ " / " ^ Rat.string_of_rat n2 ^ " = " ^ Rat.string_of_rat (n1 / n2) 350 | string_of_rewr (Rewr_Div_Num (Left, n)) = 351 Rat.string_of_rat n ^ " / e = " ^ Rat.string_of_rat n ^ " * (1 / e)" 352 | string_of_rewr (Rewr_Div_Num (Right, n)) = 353 "e / " ^ Rat.string_of_rat n ^ " = " ^ Rat.string_of_rat (Rat.inv n) ^ " * e" 354 | string_of_rewr (Rewr_Div_Mul (Left, n)) = 355 "(" ^ Rat.string_of_rat n ^ " * e1) / e2 = " ^ Rat.string_of_rat n ^ " * (e1 / e2)" 356 | string_of_rewr (Rewr_Div_Mul (Right, n)) = 357 "e1 / (" ^ Rat.string_of_rat n ^ " * e2) = " ^ Rat.string_of_rat (Rat.inv n) ^ " * (e1 / e2)" 358 | string_of_rewr (Rewr_Div_Div Left) = "(e1 / e2) / e3 = e1 / (e2 * e3)" 359 | string_of_rewr (Rewr_Div_Div Right) = "e1 / (e2 / e3) = (e1 * e3) / e2" 360 | string_of_rewr Rewr_Div_Sum = "(e1 + ... + em) / e = e1 / e + ... + em / e" 361 | string_of_rewr Rewr_Min_Eq = "min e e = e" 362 | string_of_rewr Rewr_Min_Lt = "min e1 e2 = (if e1 <= e2 then e1 else e2)" 363 | string_of_rewr Rewr_Min_Gt = "min e1 e2 = (if e2 <= e1 then e2 else e1)" 364 | string_of_rewr Rewr_Max_Eq = "max e e = e" 365 | string_of_rewr Rewr_Max_Lt = "max e1 e2 = (if e1 < e2 then e2 else e1)" 366 | string_of_rewr Rewr_Max_Gt = "max e1 e2 = (if e2 < e1 then e1 else e2)" 367 | string_of_rewr Rewr_Abs = "abs e = (if 0 <= e then e else -e)" 368 | string_of_rewr (Rewr_Eq_Nums true) = "(n1 = n2) = true" 369 | string_of_rewr (Rewr_Eq_Nums false) = "(n1 ~= n2) = false" 370 | string_of_rewr Rewr_Eq_Sub = "(e1 = e2) = (e1 - e2 = 0)" 371 | string_of_rewr Rewr_Eq_Le = "(e1 = e2) = (and (e1 <= e2) (e2 <= e1))" 372 | string_of_rewr (Rewr_Ineq_Nums (Le, true)) = "(n1 <= n2) = true" 373 | string_of_rewr (Rewr_Ineq_Nums (Le, false)) = "(n1 <= n2) = false" 374 | string_of_rewr (Rewr_Ineq_Nums (Lt, true)) = "(n1 < n2) = true" 375 | string_of_rewr (Rewr_Ineq_Nums (Lt, false)) = "(n1 < n2) = false" 376 | string_of_rewr (Rewr_Ineq_Add (Le, _)) = "(e1 <= e2) = (e1 + n <= e2 + n)" 377 | string_of_rewr (Rewr_Ineq_Add (Lt, _)) = "(e1 < e2) = (e1 + n < e2 + n)" 378 | string_of_rewr (Rewr_Ineq_Sub Le) = "(e1 <= e2) = (e1 - e2 <= 0)" 379 | string_of_rewr (Rewr_Ineq_Sub Lt) = "(e1 < e2) = (e1 - e2 < 0)" 380 | string_of_rewr (Rewr_Ineq_Mul (Le, _)) = "(e1 <= e2) = (n * e1 <= n * e2)" 381 | string_of_rewr (Rewr_Ineq_Mul (Lt, _)) = "(e1 < e2) = (n * e1 < n * e2)" 382 | string_of_rewr (Rewr_Not_Ineq Le) = "~(e1 <= e2) = (e2 < e1)" 383 | string_of_rewr (Rewr_Not_Ineq Lt) = "~(e1 < e2) = (e2 <= e1)" 384 385fun flatten_then_conv (Then_Conv (c1, c2)) = flatten_then_conv c1 @ flatten_then_conv c2 386 | flatten_then_conv c = [c] 387 388fun string_of_conv Keep_Conv = "_" 389 | string_of_conv (c as Then_Conv _) = 390 space_implode " then " (map (enclose "(" ")" o string_of_conv) (flatten_then_conv c)) 391 | string_of_conv (Args_Conv (k, cs)) = 392 "args " ^ Argo_Expr.string_of_kind k ^ " " ^ brackets string_of_conv cs 393 | string_of_conv (Rewr_Conv r) = string_of_rewr r 394 395fun string_of_rule (Axiom i) = "axiom " ^ string_of_int i 396 | string_of_rule (Taut (t, _)) = "tautology: " ^ string_of_taut t 397 | string_of_rule (Conjunct (i, n)) = "conjunct " ^ string_of_int i ^ " of " ^ string_of_int n 398 | string_of_rule (Rewrite c) = "rewrite: " ^ string_of_conv c 399 | string_of_rule (Hyp (i, _)) = "hypothesis " ^ string_of_int i 400 | string_of_rule (Clause is) = "clause " ^ brackets string_of_int is 401 | string_of_rule (Lemma is) = "lemma " ^ brackets string_of_int is 402 | string_of_rule (Unit_Res i) = "unit-resolution " ^ string_of_int i 403 | string_of_rule (Refl _) = "reflexivity" 404 | string_of_rule Symm = "symmetry" 405 | string_of_rule Trans = "transitivity" 406 | string_of_rule Cong = "congruence" 407 | string_of_rule Subst = "substitution" 408 | string_of_rule Linear_Comb = "linear-combination" 409 410 411(* unsatisfiability *) 412 413exception UNSAT of proof 414 415fun unsat p = raise UNSAT p 416 417end 418