1(* ========================================================================= *) 2(* CLAUSE = ID + THEOREM + CONSTRAINTS *) 3(* Copyright (c) 2002-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6signature mlibClause = 7sig 8 9type ('a,'b) maplet = ('a,'b) mlibUseful.maplet 10type 'a pp = 'a mlibUseful.pp 11type term = mlibTerm.term 12type formula = mlibTerm.formula 13type subst = mlibSubst.subst 14type thm = mlibThm.thm 15type termorder = mlibTermorder.termorder 16 17type parameters = 18 {term_order : bool, 19 literal_order : bool, 20 order_stickiness : int, (* Stickiness of ordering constraints: 0..3 *) 21 termorder_parm : mlibTermorder.parameters} 22 23type 'a parmupdate = ('a -> 'a) -> parameters -> parameters 24val defaults : parameters 25val update_term_order : bool parmupdate 26val update_literal_order : bool parmupdate 27val update_order_stickiness : int parmupdate 28val update_termorder_parm : mlibTermorder.parameters parmupdate 29 30type clause 31 32(* Basic operations *) 33type bits = {parm : parameters, id : int, thm : thm, order : termorder} 34val mk_clause : parameters -> thm -> clause 35val dest_clause : clause -> bits 36val literals : clause -> formula list 37val is_empty : clause -> bool 38val dest_rewr : clause -> int * thm 39val is_rewr : clause -> bool 40val rebrand : parameters -> clause -> clause 41 42(* Using ordering constraints to cut down the set of possible inferences *) 43val largest_lits : clause -> (clause * int, formula) maplet list 44val largest_eqs : clause -> (clause * int * bool, term) maplet list 45val largest_tms : clause -> (clause * int * int list, term) maplet list 46val drop_order : clause -> clause 47 48(* Subsumption *) 49val subsumes : clause -> clause -> bool 50 51(* mlibClause rewriting *) 52type rewrs 53val empty : parameters -> rewrs 54val size : rewrs -> int 55val peek : rewrs -> int -> ((term * term) * mlibRewrite.orient) option 56val add : clause -> rewrs -> rewrs 57val reduce : rewrs -> rewrs * int list 58val reduced : rewrs -> bool 59val pp_rewrs : rewrs pp 60 61(* Simplifying rules: these preserve the clause id *) 62val INST : subst -> clause -> clause 63val FRESH_VARS : clause -> clause 64val NEQ_VARS : clause -> clause 65val DEMODULATE : mlibUnits.units -> clause -> clause 66val QREWRITE : rewrs -> clause -> clause 67val REWRITE : rewrs -> clause -> clause 68 69(* Ordered resolution and paramodulation: these generate new clause ids *) 70val FACTOR : clause -> clause list 71val RESOLVE : clause * int -> clause * int -> clause 72val PARAMODULATE : clause * int * bool -> clause * int * int list -> clause 73 74(* mlibClause derivations *) 75datatype derivation = 76 Axiom 77| mlibResolution of clause * clause 78| Paramodulation of clause * clause 79| Factor of clause 80val derivation : clause -> derivation 81 82(* Pretty printing *) 83val show_id : bool ref 84val show_constraint : bool ref 85val pp_clause : clause pp 86 87end 88