1(* ========================================================================= *) 2(* CNF PROBLEMS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Problem :> Problem = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* Problems. *) 13(* ------------------------------------------------------------------------- *) 14 15type problem = 16 {axioms : Thm.clause list, 17 conjecture : Thm.clause list}; 18 19fun toClauses {axioms,conjecture} = axioms @ conjecture; 20 21fun size prob = 22 let 23 fun lits (cl,n) = n + LiteralSet.size cl 24 25 fun syms (cl,n) = n + LiteralSet.symbols cl 26 27 fun typedSyms (cl,n) = n + LiteralSet.typedSymbols cl 28 29 val cls = toClauses prob 30 in 31 {clauses = length cls, 32 literals = List.foldl lits 0 cls, 33 symbols = List.foldl syms 0 cls, 34 typedSymbols = List.foldl typedSyms 0 cls} 35 end; 36 37fun freeVars {axioms,conjecture} = 38 NameSet.union 39 (LiteralSet.freeVarsList axioms) 40 (LiteralSet.freeVarsList conjecture); 41 42local 43 fun clauseToFormula cl = 44 Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl); 45in 46 fun toFormula prob = 47 Formula.listMkConj (List.map clauseToFormula (toClauses prob)); 48 49 fun toGoal {axioms,conjecture} = 50 let 51 val clToFm = Formula.generalize o clauseToFormula 52 val clsToFm = Formula.listMkConj o List.map clToFm 53 54 val fm = Formula.False 55 val fm = 56 if List.null conjecture then fm 57 else Formula.Imp (clsToFm conjecture, fm) 58 val fm = Formula.Imp (clsToFm axioms, fm) 59 in 60 fm 61 end; 62end; 63 64fun toString prob = Formula.toString (toFormula prob); 65 66(* ------------------------------------------------------------------------- *) 67(* Categorizing problems. *) 68(* ------------------------------------------------------------------------- *) 69 70datatype propositional = 71 Propositional 72 | EffectivelyPropositional 73 | NonPropositional; 74 75datatype equality = 76 NonEquality 77 | Equality 78 | PureEquality; 79 80datatype horn = 81 Trivial 82 | Unit 83 | DoubleHorn 84 | Horn 85 | NegativeHorn 86 | NonHorn; 87 88type category = 89 {propositional : propositional, 90 equality : equality, 91 horn : horn}; 92 93fun categorize prob = 94 let 95 val cls = toClauses prob 96 97 val rels = 98 let 99 fun f (cl,set) = NameAritySet.union set (LiteralSet.relations cl) 100 in 101 List.foldl f NameAritySet.empty cls 102 end 103 104 val funs = 105 let 106 fun f (cl,set) = NameAritySet.union set (LiteralSet.functions cl) 107 in 108 List.foldl f NameAritySet.empty cls 109 end 110 111 val propositional = 112 if NameAritySet.allNullary rels then Propositional 113 else if NameAritySet.allNullary funs then EffectivelyPropositional 114 else NonPropositional 115 116 val equality = 117 if not (NameAritySet.member Atom.eqRelation rels) then NonEquality 118 else if NameAritySet.size rels = 1 then PureEquality 119 else Equality 120 121 val horn = 122 if List.exists LiteralSet.null cls then Trivial 123 else if List.all (fn cl => LiteralSet.size cl = 1) cls then Unit 124 else 125 let 126 fun pos cl = LiteralSet.count Literal.positive cl <= 1 127 fun neg cl = LiteralSet.count Literal.negative cl <= 1 128 in 129 case (List.all pos cls, List.all neg cls) of 130 (true,true) => DoubleHorn 131 | (true,false) => Horn 132 | (false,true) => NegativeHorn 133 | (false,false) => NonHorn 134 end 135 in 136 {propositional = propositional, 137 equality = equality, 138 horn = horn} 139 end; 140 141fun categoryToString {propositional,equality,horn} = 142 (case propositional of 143 Propositional => "propositional" 144 | EffectivelyPropositional => "effectively propositional" 145 | NonPropositional => "non-propositional") ^ 146 ", " ^ 147 (case equality of 148 NonEquality => "non-equality" 149 | Equality => "equality" 150 | PureEquality => "pure equality") ^ 151 ", " ^ 152 (case horn of 153 Trivial => "trivial" 154 | Unit => "unit" 155 | DoubleHorn => "horn (and negative horn)" 156 | Horn => "horn" 157 | NegativeHorn => "negative horn" 158 | NonHorn => "non-horn"); 159 160end 161