1(* ========================================================================= *) 2(* THE ACTIVE SET OF CLAUSES *) 3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Active = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* A type of active clause sets. *) 11(* ------------------------------------------------------------------------- *) 12 13type simplify = 14 {subsume : bool, 15 reduce : bool, 16 rewrite : bool} 17 18type parameters = 19 {clause : Clause.parameters, 20 prefactor : simplify, 21 postfactor : simplify} 22 23type active 24 25(* ------------------------------------------------------------------------- *) 26(* Basic operations. *) 27(* ------------------------------------------------------------------------- *) 28 29val default : parameters 30 31val size : active -> int 32 33val saturation : active -> Clause.clause list 34 35(* ------------------------------------------------------------------------- *) 36(* Create a new active clause set and initialize clauses. *) 37(* ------------------------------------------------------------------------- *) 38 39val new : 40 parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} -> 41 active * {axioms : Clause.clause list, conjecture : Clause.clause list} 42 43(* ------------------------------------------------------------------------- *) 44(* Add a clause into the active set and deduce all consequences. *) 45(* ------------------------------------------------------------------------- *) 46 47val add : active -> Clause.clause -> active * Clause.clause list 48 49(* ------------------------------------------------------------------------- *) 50(* Pretty printing. *) 51(* ------------------------------------------------------------------------- *) 52 53val pp : active Print.pp 54 55end 56