1(* ========================================================================= *) 2(* CNF PROBLEMS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Problem = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* Problems. *) 11(* ------------------------------------------------------------------------- *) 12 13type problem = 14 {axioms : Thm.clause list, 15 conjecture : Thm.clause list} 16 17val size : problem -> {clauses : int, 18 literals : int, 19 symbols : int, 20 typedSymbols : int} 21 22val freeVars : problem -> NameSet.set 23 24val toClauses : problem -> Thm.clause list 25 26val toFormula : problem -> Formula.formula 27 28val toGoal : problem -> Formula.formula 29 30val toString : problem -> string 31 32(* ------------------------------------------------------------------------- *) 33(* Categorizing problems. *) 34(* ------------------------------------------------------------------------- *) 35 36datatype propositional = 37 Propositional 38 | EffectivelyPropositional 39 | NonPropositional 40 41datatype equality = 42 NonEquality 43 | Equality 44 | PureEquality 45 46datatype horn = 47 Trivial 48 | Unit 49 | DoubleHorn 50 | Horn 51 | NegativeHorn 52 | NonHorn 53 54type category = 55 {propositional : propositional, 56 equality : equality, 57 horn : horn} 58 59val categorize : problem -> category 60 61val categoryToString : category -> string 62 63end 64