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