src/HOL/Tools/prop_logic.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 22441 7da872d34ace
child 31220 f1c0ed85a33b
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     1
(*  Title:      HOL/Tools/prop_logic.ML
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     2
    ID:         $Id$
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     3
    Author:     Tjark Weber
16907
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
     4
    Copyright   2004-2005
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     5
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     6
Formulas of propositional logic.
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     7
*)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     8
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
     9
signature PROP_LOGIC =
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    10
sig
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    11
	datatype prop_formula =
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    12
		  True
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    13
		| False
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    14
		| BoolVar of int  (* NOTE: only use indices >= 1 *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    15
		| Not of prop_formula
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    16
		| Or of prop_formula * prop_formula
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    17
		| And of prop_formula * prop_formula
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    18
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    19
	val SNot     : prop_formula -> prop_formula
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    20
	val SOr      : prop_formula * prop_formula -> prop_formula
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    21
	val SAnd     : prop_formula * prop_formula -> prop_formula
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    22
	val simplify : prop_formula -> prop_formula  (* eliminates True/False and double-negation *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    23
14681
16fcef3a3174 comments modified
webertj
parents: 14452
diff changeset
    24
	val indices : prop_formula -> int list  (* set of all variable indices *)
15301
26724034de5e comment modified
webertj
parents: 14964
diff changeset
    25
	val maxidx  : prop_formula -> int       (* maximal variable index *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    26
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    27
	val exists      : prop_formula list -> prop_formula  (* finite disjunction *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    28
	val all         : prop_formula list -> prop_formula  (* finite conjunction *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    29
	val dot_product : prop_formula list * prop_formula list -> prop_formula
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    30
22441
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
    31
	val is_nnf : prop_formula -> bool  (* returns true iff the formula is in negation normal form *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
    32
	val is_cnf : prop_formula -> bool  (* returns true iff the formula is in conjunctive normal form *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
    33
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    34
	val nnf    : prop_formula -> prop_formula  (* negation normal form *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    35
	val cnf    : prop_formula -> prop_formula  (* conjunctive normal form *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    36
	val auxcnf : prop_formula -> prop_formula  (* cnf with auxiliary variables *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    37
	val defcnf : prop_formula -> prop_formula  (* definitional cnf *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    38
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    39
	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
    40
20442
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
    41
	(* propositional representation of HOL terms *)
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
    42
	val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
20442
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
    43
	(* HOL term representation of propositional formulae *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
    44
	val term_of_prop_formula : prop_formula -> Term.term
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    45
end;
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    46
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    47
structure PropLogic : PROP_LOGIC =
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    48
struct
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    49
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    50
(* ------------------------------------------------------------------------- *)
14753
f40b45db8cf0 Comments fixed
webertj
parents: 14681
diff changeset
    51
(* prop_formula: formulas of propositional logic, built from Boolean         *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    52
(*               variables (referred to by index) and True/False using       *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    53
(*               not/or/and                                                  *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    54
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    55
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    56
	datatype prop_formula =
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    57
		  True
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    58
		| False
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    59
		| BoolVar of int  (* NOTE: only use indices >= 1 *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    60
		| Not of prop_formula
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    61
		| Or of prop_formula * prop_formula
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    62
		| And of prop_formula * prop_formula;
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    63
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    64
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    65
(* The following constructor functions make sure that True and False do not  *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    66
(* occur within any of the other connectives (i.e. Not, Or, And), and        *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    67
(* perform double-negation elimination.                                      *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    68
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    69
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    70
	(* prop_formula -> prop_formula *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    71
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    72
	fun SNot True     = False
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    73
	  | SNot False    = True
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    74
	  | SNot (Not fm) = fm
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    75
	  | SNot fm       = Not fm;
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    76
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    77
	(* prop_formula * prop_formula -> prop_formula *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    78
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    79
	fun SOr (True, _)   = True
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    80
	  | SOr (_, True)   = True
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    81
	  | SOr (False, fm) = fm
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    82
	  | SOr (fm, False) = fm
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    83
	  | SOr (fm1, fm2)  = Or (fm1, fm2);
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    84
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    85
	(* prop_formula * prop_formula -> prop_formula *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    86
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    87
	fun SAnd (True, fm) = fm
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    88
	  | SAnd (fm, True) = fm
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    89
	  | SAnd (False, _) = False
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    90
	  | SAnd (_, False) = False
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    91
	  | SAnd (fm1, fm2) = And (fm1, fm2);
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    92
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
    93
(* ------------------------------------------------------------------------- *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    94
(* simplify: eliminates True/False below other connectives, and double-      *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    95
(*      negation                                                             *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    96
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    97
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    98
	(* prop_formula -> prop_formula *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
    99
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   100
	fun simplify (Not fm)         = SNot (simplify fm)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   101
	  | simplify (Or (fm1, fm2))  = SOr (simplify fm1, simplify fm2)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   102
	  | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   103
	  | simplify fm               = fm;
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   104
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   105
(* ------------------------------------------------------------------------- *)
14753
f40b45db8cf0 Comments fixed
webertj
parents: 14681
diff changeset
   106
(* indices: collects all indices of Boolean variables that occur in a        *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   107
(*      propositional formula 'fm'; no duplicates                            *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   108
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   109
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   110
	(* prop_formula -> int list *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   111
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   112
	fun indices True             = []
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   113
	  | indices False            = []
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   114
	  | indices (BoolVar i)      = [i]
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   115
	  | indices (Not fm)         = indices fm
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   116
	  | indices (Or (fm1, fm2))  = (indices fm1) union_int (indices fm2)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   117
	  | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   118
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   119
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   120
(* maxidx: computes the maximal variable index occuring in a formula of      *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   121
(*      propositional logic 'fm'; 0 if 'fm' contains no variable             *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   122
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   123
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   124
	(* prop_formula -> int *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   125
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   126
	fun maxidx True             = 0
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   127
	  | maxidx False            = 0
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   128
	  | maxidx (BoolVar i)      = i
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   129
	  | maxidx (Not fm)         = maxidx fm
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   130
	  | maxidx (Or (fm1, fm2))  = Int.max (maxidx fm1, maxidx fm2)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   131
	  | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   132
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   133
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   134
(* exists: computes the disjunction over a list 'xs' of propositional        *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   135
(*      formulas                                                             *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   136
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   137
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   138
	(* prop_formula list -> prop_formula *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   139
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   140
	fun exists xs = Library.foldl SOr (False, xs);
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   141
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   142
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   143
(* all: computes the conjunction over a list 'xs' of propositional formulas  *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   144
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   145
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   146
	(* prop_formula list -> prop_formula *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   147
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   148
	fun all xs = Library.foldl SAnd (True, xs);
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   149
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   150
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   151
(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn                *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   152
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   153
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   154
	(* prop_formula list * prop_formula list -> prop_formula *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   155
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   156
	fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   157
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   158
(* ------------------------------------------------------------------------- *)
22441
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   159
(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e.   *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   160
(*         only variables may be negated, but not subformulas).              *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   161
(* ------------------------------------------------------------------------- *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   162
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   163
	local
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   164
		fun is_literal (BoolVar _)       = true
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   165
		  | is_literal (Not (BoolVar _)) = true
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   166
		  | is_literal _                 = false
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   167
		fun is_conj_disj (Or (fm1, fm2))  =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   168
			is_conj_disj fm1 andalso is_conj_disj fm2
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   169
		  | is_conj_disj (And (fm1, fm2)) =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   170
			is_conj_disj fm1 andalso is_conj_disj fm2
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   171
		  | is_conj_disj fm               =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   172
			is_literal fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   173
	in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   174
		fun is_nnf True  = true
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   175
		  | is_nnf False = true
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   176
		  | is_nnf fm    = is_conj_disj fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   177
	end;
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   178
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   179
(* ------------------------------------------------------------------------- *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   180
(* is_cnf: returns 'true' iff the formula is in conjunctive normal form      *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   181
(*         (i.e. a conjunction of disjunctions).                             *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   182
(* ------------------------------------------------------------------------- *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   183
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   184
	local
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   185
		fun is_literal (BoolVar _)       = true
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   186
		  | is_literal (Not (BoolVar _)) = true
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   187
		  | is_literal _                 = false
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   188
		fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   189
		  | is_disj fm              = is_literal fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   190
		fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   191
		  | is_conj fm               = is_disj fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   192
	in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   193
		fun is_cnf True             = true
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   194
		  | is_cnf False            = true
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   195
		  | is_cnf fm               = is_conj fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   196
	end;
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   197
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   198
(* ------------------------------------------------------------------------- *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   199
(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   200
(*      logic (i.e. only variables may be negated, but not subformulas).     *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   201
(*      Simplification (c.f. 'simplify') is performed as well.               *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   202
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   203
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   204
	(* prop_formula -> prop_formula *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   205
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   206
	fun
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   207
	(* constants *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   208
	    nnf True                   = True
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   209
	  | nnf False                  = False
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   210
	(* variables *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   211
	  | nnf (BoolVar i)            = (BoolVar i)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   212
	(* 'or' and 'and' as outermost connectives are left untouched *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   213
	  | nnf (Or  (fm1, fm2))       = SOr  (nnf fm1, nnf fm2)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   214
	  | nnf (And (fm1, fm2))       = SAnd (nnf fm1, nnf fm2)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   215
	(* 'not' + constant *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   216
	  | nnf (Not True)             = False
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   217
	  | nnf (Not False)            = True
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   218
	(* 'not' + variable *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   219
	  | nnf (Not (BoolVar i))      = Not (BoolVar i)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   220
	(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   221
	  | nnf (Not (Or  (fm1, fm2))) = SAnd (nnf (SNot fm1), nnf (SNot fm2))
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   222
	  | nnf (Not (And (fm1, fm2))) = SOr  (nnf (SNot fm1), nnf (SNot fm2))
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   223
	(* double-negation elimination *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   224
	  | nnf (Not (Not fm))         = nnf fm;
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   225
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   226
(* ------------------------------------------------------------------------- *)
14681
16fcef3a3174 comments modified
webertj
parents: 14452
diff changeset
   227
(* cnf: computes the conjunctive normal form (i.e. a conjunction of          *)
16fcef3a3174 comments modified
webertj
parents: 14452
diff changeset
   228
(*      disjunctions) of a formula 'fm' of propositional logic.  The result  *)
16fcef3a3174 comments modified
webertj
parents: 14452
diff changeset
   229
(*      formula may be exponentially longer than 'fm'.                       *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   230
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   231
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   232
	(* prop_formula -> prop_formula *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   233
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   234
	fun cnf fm =
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   235
	let
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   236
		fun
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   237
		(* constants *)
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   238
		    cnf_from_nnf True             = True
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   239
		  | cnf_from_nnf False            = False
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   240
		(* literals *)
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   241
		  | cnf_from_nnf (BoolVar i)      = BoolVar i
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   242
		  | cnf_from_nnf (Not fm1)        = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   243
		(* pushing 'or' inside of 'and' using distributive laws *)
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   244
		  | cnf_from_nnf (Or (fm1, fm2))  =
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   245
			let
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   246
				fun cnf_or (And (fm11, fm12), fm2) =
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   247
					And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   248
				  | cnf_or (fm1, And (fm21, fm22)) =
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   249
					And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   250
				(* neither subformula contains 'and' *)
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   251
				  | cnf_or (fm1, fm2) =
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   252
					Or (fm1, fm2)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   253
			in
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   254
				cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   255
			end
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   256
		(* 'and' as outermost connective is left untouched *)
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   257
		  | cnf_from_nnf (And (fm1, fm2)) = And (cnf_from_nnf fm1, cnf_from_nnf fm2)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   258
	in
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   259
		(cnf_from_nnf o nnf) fm
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   260
	end;
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   261
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   262
(* ------------------------------------------------------------------------- *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   263
(* auxcnf: computes the definitional conjunctive normal form of a formula    *)
14681
16fcef3a3174 comments modified
webertj
parents: 14452
diff changeset
   264
(*      'fm' of propositional logic, introducing auxiliary variables if      *)
16fcef3a3174 comments modified
webertj
parents: 14452
diff changeset
   265
(*      necessary to avoid an exponential blowup of the formula.  The result *)
16fcef3a3174 comments modified
webertj
parents: 14452
diff changeset
   266
(*      formula is satisfiable if and only if 'fm' is satisfiable.           *)
16907
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   267
(*      Auxiliary variables are introduced as switches for OR-nodes, based   *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   268
(*      on the observation that e.g. "fm1 OR (fm21 AND fm22)" is             *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   269
(*      equisatisfiable with "(fm1 OR ~aux) AND (fm21 OR aux) AND (fm22 OR   *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   270
(*      aux)".                                                               *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   271
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   272
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   273
(* ------------------------------------------------------------------------- *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   274
(* Note: 'auxcnf' tends to use fewer variables and fewer clauses than        *)
16913
1d8a8d010e69 comment modified
webertj
parents: 16909
diff changeset
   275
(*      'defcnf' below, but sometimes generates much larger SAT problems     *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   276
(*      overall (hence it must sometimes generate longer clauses than        *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   277
(*      'defcnf' does).  It is currently not quite clear to me if one of the *)
16913
1d8a8d010e69 comment modified
webertj
parents: 16909
diff changeset
   278
(*      algorithms is clearly superior to the other, but I suggest using     *)
1d8a8d010e69 comment modified
webertj
parents: 16909
diff changeset
   279
(*      'defcnf' instead.                                                    *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   280
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   281
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   282
	(* prop_formula -> prop_formula *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   283
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   284
	fun auxcnf fm =
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   285
	let
16907
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   286
		(* convert formula to NNF first *)
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   287
		val fm' = nnf fm
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   288
		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
16907
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   289
		(* int ref *)
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   290
		val new = ref (maxidx fm' + 1)
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   291
		(* unit -> int *)
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   292
		fun new_idx () = let val idx = !new in new := idx+1; idx end
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   293
		(* prop_formula -> prop_formula *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   294
		fun
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   295
		(* constants *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   296
		    auxcnf_from_nnf True  = True
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   297
		  | auxcnf_from_nnf False = False
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   298
		(* literals *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   299
		  | auxcnf_from_nnf (BoolVar i) = BoolVar i
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   300
		  | auxcnf_from_nnf (Not fm1)   = Not fm1  (* 'fm1' must be a variable since the formula is in NNF *)
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   301
		(* pushing 'or' inside of 'and' using auxiliary variables *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   302
		  | auxcnf_from_nnf (Or (fm1, fm2)) =
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   303
			let
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   304
				val fm1' = auxcnf_from_nnf fm1
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   305
				val fm2' = auxcnf_from_nnf fm2
16907
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   306
				(* prop_formula * prop_formula -> prop_formula *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   307
				fun auxcnf_or (And (fm11, fm12), fm2) =
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   308
					(case fm2 of
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   309
					(* do not introduce an auxiliary variable for literals *)
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   310
					  BoolVar _ =>
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   311
							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   312
					| Not _ =>
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   313
							And (auxcnf_or (fm11, fm2), auxcnf_or (fm12, fm2))
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   314
					| _ =>
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   315
						let
16907
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   316
							val aux = BoolVar (new_idx ())
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   317
						in
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   318
							And (And (auxcnf_or (fm11, aux), auxcnf_or (fm12, aux)), auxcnf_or (fm2, Not aux))
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   319
						end)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   320
				  | auxcnf_or (fm1, And (fm21, fm22)) =
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   321
					(case fm1 of
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   322
					(* do not introduce an auxiliary variable for literals *)
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   323
					  BoolVar _ =>
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   324
							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   325
					| Not _ =>
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   326
							And (auxcnf_or (fm1, fm21), auxcnf_or (fm1, fm22))
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   327
					| _ =>
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   328
						let
16907
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   329
							val aux = BoolVar (new_idx ())
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   330
						in
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   331
							And (auxcnf_or (fm1, Not aux), And (auxcnf_or (fm21, aux), auxcnf_or (fm22, aux)))
14964
2c1456d705e9 improved defcnf conversion
webertj
parents: 14939
diff changeset
   332
						end)
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   333
				(* neither subformula contains 'and' *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   334
				  | auxcnf_or (fm1, fm2) =
16907
2187e3f94761 defcnf modified to internally use a reference
webertj
parents: 15570
diff changeset
   335
					Or (fm1, fm2)
14939
29fe4a9a7cb5 faster defcnf conversion
webertj
parents: 14753
diff changeset
   336
			in
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   337
				auxcnf_or (fm1', fm2')
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   338
			end
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   339
		(* 'and' as outermost connective is left untouched *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   340
		  | auxcnf_from_nnf (And (fm1, fm2)) =
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   341
				And (auxcnf_from_nnf fm1, auxcnf_from_nnf fm2)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   342
	in
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   343
		auxcnf_from_nnf fm'
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   344
	end;
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   345
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   346
(* ------------------------------------------------------------------------- *)
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   347
(* defcnf: computes the definitional conjunctive normal form of a formula    *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   348
(*      'fm' of propositional logic, introducing auxiliary variables to      *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   349
(*      avoid an exponential blowup of the formula.  The result formula is   *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   350
(*      satisfiable if and only if 'fm' is satisfiable.  Auxiliary variables *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   351
(*      are introduced as abbreviations for AND-, OR-, and NOT-nodes, based  *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   352
(*      on the following equisatisfiabilities (+/- indicates polarity):      *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   353
(*      LITERAL+       == LITERAL                                            *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   354
(*      LITERAL-       == NOT LITERAL                                        *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   355
(*      (NOT fm1)+     == aux AND (NOT aux OR fm1-)                          *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   356
(*      (fm1 OR fm2)+  == aux AND (NOT aux OR fm1+ OR fm2+)                  *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   357
(*      (fm1 AND fm2)+ == aux AND (NOT aux OR fm1+) AND (NOT aux OR fm2+)    *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   358
(*      (NOT fm1)-     == aux AND (NOT aux OR fm1+)                          *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   359
(*      (fm1 OR fm2)-  == aux AND (NOT aux OR fm1-) AND (NOT aux OR fm2-)    *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   360
(*      (fm1 AND fm2)- == aux AND (NOT aux OR fm1- OR fm2-)                  *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   361
(*      Example:                                                             *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   362
(*      NOT (a AND b) == aux1 AND (NOT aux1 OR aux2)                         *)
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   363
(*                            AND (NOT aux2 OR NOT a OR NOT b)               *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   364
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   365
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   366
	(* prop_formula -> prop_formula *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   367
16909
acbc7a9c3864 defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
webertj
parents: 16907
diff changeset
   368
	fun defcnf fm =
22441
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   369
		if is_cnf fm then
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   370
			fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   371
		else let
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   372
			(* simplify formula first *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   373
			val fm' = simplify fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   374
			(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   375
			(* int ref *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   376
			val new = ref (maxidx fm' + 1)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   377
			(* unit -> int *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   378
			fun new_idx () = let val idx = !new in new := idx+1; idx end
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   379
			(* optimization for n-ary disjunction/conjunction *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   380
			(* prop_formula -> prop_formula list *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   381
			fun disjuncts (Or (fm1, fm2)) = (disjuncts fm1) @ (disjuncts fm2)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   382
			| disjuncts fm1             = [fm1]
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   383
			(* prop_formula -> prop_formula list *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   384
			fun conjuncts (And (fm1, fm2)) = (conjuncts fm1) @ (conjuncts fm2)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   385
			| conjuncts fm1              = [fm1]
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   386
			(* polarity -> formula -> (defining clauses, literal) *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   387
			(* bool -> prop_formula -> prop_formula * prop_formula *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   388
			fun
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   389
			(* constants *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   390
				defcnf' true  True  = (True, True)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   391
			| defcnf' false True  = (*(True, False)*) error "formula is not simplified, True occurs with negative polarity"
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   392
			| defcnf' true  False = (True, False)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   393
			| defcnf' false False = (*(True, True)*) error "formula is not simplified, False occurs with negative polarity"
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   394
			(* literals *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   395
			| defcnf' true  (BoolVar i)       = (True, BoolVar i)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   396
			| defcnf' false (BoolVar i)       = (True, Not (BoolVar i))
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   397
			| defcnf' true  (Not (BoolVar i)) = (True, Not (BoolVar i))
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   398
			| defcnf' false (Not (BoolVar i)) = (True, BoolVar i)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   399
			(* 'not' *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   400
			| defcnf' polarity (Not fm1) =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   401
				let
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   402
					val (def1, aux1) = defcnf' (not polarity) fm1
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   403
					val aux          = BoolVar (new_idx ())
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   404
					val def          = Or (Not aux, aux1)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   405
				in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   406
					(SAnd (def1, def), aux)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   407
				end
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   408
			(* 'or' *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   409
			| defcnf' polarity (Or (fm1, fm2)) =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   410
				let
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   411
					val fms          = disjuncts (Or (fm1, fm2))
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   412
					val (defs, auxs) = split_list (map (defcnf' polarity) fms)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   413
					val aux          = BoolVar (new_idx ())
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   414
					val def          = if polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   415
				in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   416
					(SAnd (all defs, def), aux)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   417
				end
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   418
			(* 'and' *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   419
			| defcnf' polarity (And (fm1, fm2)) =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   420
				let
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   421
					val fms          = conjuncts (And (fm1, fm2))
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   422
					val (defs, auxs) = split_list (map (defcnf' polarity) fms)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   423
					val aux          = BoolVar (new_idx ())
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   424
					val def          = if not polarity then Or (Not aux, exists auxs) else all (map (fn a => Or (Not aux, a)) auxs)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   425
				in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   426
					(SAnd (all defs, def), aux)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   427
				end
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   428
			(* optimization: do not introduce auxiliary variables for parts of the formula that are in CNF already *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   429
			(* prop_formula -> prop_formula * prop_formula *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   430
			fun defcnf_or (Or (fm1, fm2)) =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   431
				let
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   432
					val (def1, aux1) = defcnf_or fm1
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   433
					val (def2, aux2) = defcnf_or fm2
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   434
				in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   435
					(SAnd (def1, def2), Or (aux1, aux2))
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   436
				end
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   437
			| defcnf_or fm =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   438
				defcnf' true fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   439
			(* prop_formula -> prop_formula * prop_formula *)
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   440
			fun defcnf_and (And (fm1, fm2)) =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   441
				let
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   442
					val (def1, aux1) = defcnf_and fm1
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   443
					val (def2, aux2) = defcnf_and fm2
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   444
				in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   445
					(SAnd (def1, def2), And (aux1, aux2))
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   446
				end
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   447
			| defcnf_and (Or (fm1, fm2)) =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   448
				let
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   449
					val (def1, aux1) = defcnf_or fm1
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   450
					val (def2, aux2) = defcnf_or fm2
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   451
				in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   452
					(SAnd (def1, def2), Or (aux1, aux2))
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   453
				end
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   454
			| defcnf_and fm =
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   455
				defcnf' true fm
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   456
		in
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   457
			SAnd (defcnf_and fm')
7da872d34ace is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
webertj
parents: 20442
diff changeset
   458
		end;
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   459
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   460
(* ------------------------------------------------------------------------- *)
14753
f40b45db8cf0 Comments fixed
webertj
parents: 14681
diff changeset
   461
(* eval: given an assignment 'a' of Boolean values to variable indices, the  *)
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   462
(*      truth value of a propositional formula 'fm' is computed              *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   463
(* ------------------------------------------------------------------------- *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   464
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   465
	(* (int -> bool) -> prop_formula -> bool *)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   466
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   467
	fun eval a True            = true
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   468
	  | eval a False           = false
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   469
	  | eval a (BoolVar i)     = (a i)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   470
	  | eval a (Not fm)        = not (eval a fm)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   471
	  | eval a (Or (fm1,fm2))  = (eval a fm1) orelse (eval a fm2)
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   472
	  | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   473
17809
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   474
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   475
(* prop_formula_of_term: returns the propositional structure of a HOL term,  *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   476
(*      with subterms replaced by Boolean variables.  Also returns a table   *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   477
(*      of terms and corresponding variables that extends the table that was *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   478
(*      given as an argument.  Usually, you'll just want to use              *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   479
(*      'Termtab.empty' as value for 'table'.                                *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   480
(* ------------------------------------------------------------------------- *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   481
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   482
(* Note: The implementation is somewhat optimized; the next index to be used *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   483
(*       is computed only when it is actually needed.  However, when         *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   484
(*       'prop_formula_of_term' is invoked many times, it might be more      *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   485
(*       efficient to pass and return this value as an additional parameter, *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   486
(*       so that it does not have to be recomputed (by folding over the      *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   487
(*       table) for each invocation.                                         *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   488
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   489
	(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   490
	fun prop_formula_of_term t table =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   491
	let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   492
		val next_idx_is_valid = ref false
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   493
		val next_idx          = ref 0
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   494
		fun get_next_idx () =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   495
			if !next_idx_is_valid then
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   496
				inc next_idx
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   497
			else (
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   498
				next_idx          := Termtab.fold (curry Int.max o snd) table 0;
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   499
				next_idx_is_valid := true;
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   500
				inc next_idx
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   501
			)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   502
		fun aux (Const ("True", _))         table =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   503
			(True, table)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   504
		  | aux (Const ("False", _))        table =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   505
			(False, table)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   506
		  | aux (Const ("Not", _) $ x)      table =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   507
			apfst Not (aux x table)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   508
		  | aux (Const ("op |", _) $ x $ y) table =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   509
			let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   510
				val (fm1, table1) = aux x table
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   511
				val (fm2, table2) = aux y table1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   512
			in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   513
				(Or (fm1, fm2), table2)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   514
			end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   515
		  | aux (Const ("op &", _) $ x $ y) table =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   516
			let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   517
				val (fm1, table1) = aux x table
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   518
				val (fm2, table2) = aux y table1
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   519
			in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   520
				(And (fm1, fm2), table2)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   521
			end
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   522
		  | aux x                           table =
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   523
			(case Termtab.lookup table x of
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   524
			  SOME i =>
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   525
				(BoolVar i, table)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   526
			| NONE   =>
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   527
				let
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   528
					val i = get_next_idx ()
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   529
				in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   530
					(BoolVar i, Termtab.update (x, i) table)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   531
				end)
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   532
	in
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   533
		aux t table
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   534
	end;
195045659c06 Tactics sat and satx reimplemented, several improvements
webertj
parents: 16913
diff changeset
   535
20442
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   536
(* ------------------------------------------------------------------------- *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   537
(* term_of_prop_formula: returns a HOL term that corresponds to a            *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   538
(*      propositional formula, with Boolean variables replaced by Free's     *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   539
(* ------------------------------------------------------------------------- *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   540
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   541
(* Note: A more generic implementation should take another argument of type  *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   542
(*       Term.term Inttab.table (or so) that specifies HOL terms for some    *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   543
(*       Boolean variables in the formula, similar to 'prop_formula_of_term' *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   544
(*       (but the other way round).                                          *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   545
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   546
	(* prop_formula -> Term.term *)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   547
	fun term_of_prop_formula True             =
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   548
			HOLogic.true_const
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   549
		| term_of_prop_formula False            =
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   550
			HOLogic.false_const
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   551
		| term_of_prop_formula (BoolVar i)      =
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   552
			Free ("v" ^ Int.toString i, HOLogic.boolT)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   553
		| term_of_prop_formula (Not fm)         =
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   554
			HOLogic.mk_not (term_of_prop_formula fm)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   555
		| term_of_prop_formula (Or (fm1, fm2))  =
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   556
			HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   557
		| term_of_prop_formula (And (fm1, fm2)) =
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   558
			HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
04621ea9440e term_of_prop_formula added
webertj
parents: 17809
diff changeset
   559
14452
c24d90dbf0c9 Formulas of propositional logic
webertj
parents:
diff changeset
   560
end;