Coverage report: /home/ati/workspace/perec/util/logic.lisp

Kind	Covered	All	%
expression	185	254	72.8
branch	26	40	65.0

Key

Not instrumented

Conditionalized out

Executed

Not executed

Both branches taken

One branch taken

Neither branch taken

1

;; -*- mode: Lisp; Syntax: Common-Lisp; -*-

2

;;;

3

4

;;;

5

;;; See LICENCE for details.

6

7

(in-package :cl-perec)

8

9

;;;;;;;;;;

10

;;; Syntax

11

12

(defun make-exp (op &rest args)

13

(cons op args))

14

15

(defun op (sentence)

16

(if (atomic-clause? sentence)

17

sentence

18

(car sentence)))

19

20

(defun args (sentence)

21

(cdr sentence))

22

23

(defun arg1 (sentence)

24

(second sentence))

25

26

(defun atomic-clause? (sentence)

27

"An atomic clause has no connectives or quantifiers."

28

(or (atom sentence)

29

(not (member (car sentence) '(and or not)))))

30

31

(defun literal-clause? (sentence)

32

"A literal is an atomic clause or a negated atomic clause."

33

(or (atomic-clause? sentence)

34

(and (negative-clause? sentence) (atomic-clause? (arg1 sentence)))))

35

36

(defun negative-clause? (sentence)

37

"A negative clause has NOT as the operator."

38

(eq (car sentence) 'not))

39

40

;;;;;;;;;;;;;;;;;;;;;;;;;;;

41

;;; Conjunctive normal form

42

43

(defun ->cnf (p)

44

"Convert a sentence p to conjunctive normal form [p 279-280]."

45

;; That is, return (and (or ...) ...) where

46

;; each of the conjuncts has all literal disjuncts.

47

(case (op p)

48

((not) (let ((p2 (move-not-inwards (arg1 p))))

49

(if (literal-clause? p2) p2 (->cnf p2))))

50

((and) (conjunction (mappend #L(conjuncts (->cnf !1)) (args p))))

51

((or) (merge-disjuncts (mapcar '->cnf (args p))))

52

(otherwise p)))

53

54

(defun ->dnf (p)

55

"Convert a sentence p to disjunctive normal form [p 279-280]."

56

;; That is, return (and (or ...) ...) where

57

;; each of the disjuncts has all literal conjuncts.

58

(case (op p)

59

((not) (let ((p2 (move-not-inwards (arg1 p))))

60

(if (literal-clause? p2) p2 (->dnf p2))))

61

((or) (disjunction (mappend #L(disjuncts (->dnf !1)) (args p))))

62

((and) (merge-conjuncts (mapcar '->dnf (args p))))

63

(otherwise p)))

64

65

(defun move-not-inwards (p)

66

"Given P, return ~P, but with the negation moved as far in as possible."

67

(case (op p)

68

((#t) #f)

69

((#f) #t)

70

((not) (arg1 p))

71

((and) (disjunction (mapcar #'move-not-inwards (args p))))

72

((or) (conjunction (mapcar #'move-not-inwards (args p))))

73

(otherwise (make-exp 'not p))))

74

75

(defun merge-disjuncts (disjuncts)

76

"Return a CNF expression for the disjunction."

77

;; The argument is a list of disjuncts, each in CNF.

78

(case (length disjuncts)

79

(0 #f)

80

(1 (first disjuncts))

81

(t (conjunction

82

(iter outer (for y in (conjuncts (merge-disjuncts (rest disjuncts))))

83

(iter (for x in (conjuncts (first disjuncts)))

84

                     (in outer (collect (disjunction (append (disjuncts x) (disjuncts y)))))))))))

85

86

(defun merge-conjuncts (conjuncts)

87

"Return a DNF expression for the conjunction."

88

;; The argument is a list of disjuncts, each in CNF.

89

(case (length conjuncts)

90

(0 #t)

91

(1 (first conjuncts))

92

(t (disjunction

93

(iter outer (for y in (disjuncts (merge-conjuncts (rest conjuncts))))

94

(iter (for x in (disjuncts (first conjuncts)))

95

                     (in outer (collect (conjunction (append (conjuncts x) (conjuncts y)))))))))))

96

97

;;;;;;;;;;;

98

;;; Helpers

99

100

(defun conjuncts (sentence)

101

"Return a list of the conjuncts in this sentence."

102

(cond ((eq (op sentence) 'and) (args sentence))

103

((eq sentence #t) nil)

104

(t (list sentence))))

105

106

(defun disjuncts (sentence)

107

"Return a list of the disjuncts in this sentence."

108

(cond ((eq (op sentence) 'or) (args sentence))

109

((eq sentence #f) nil)

110

(t (list sentence))))

111

112

(defun conjunction (args)

113

"Form a disjunction with these args."

114

(case (length args)

115

(0 #t)

116

(1 (first args))

117

(otherwise `(and ,@args))))

118

119

(defun disjunction (args)

120

"Form a disjunction with these args."

121

(case (length args)

122

(0 #f)

123

(1 (first args))

124

(otherwise `(or ,@args))))

125

126

(defun simplify-boolean-form (form)

127

"Makes the following simplifications on form:

128

(not false) -> true

129

(not true) -> false

130

(not (not x)) -> x

131

(or) -> false

132

(or x) -> x

133

(or x... false y...) -> (or x... y...)

134

(or x... true y...) -> true

135

(or x... (or y...) z...) -> (or x... y... z...)

136

(and) -> true

137

(and x) -> x

138

(and x... true y...) -> (and x... y...)

139

(and x... false y...) -> false

140

(and x... (and y...) z...) -> (and x... y... z...)

141

142

where x, y and z are arbitrary objects and '...' means zero or more occurence,

143

and false/true means a generalized boolean literal."

144

(flet ((simplify-args (operator args)

145

(iter (for arg in args)

146

(for simplified = (simplify-boolean-form arg))

147

(if (and (listp simplified) (eq (first simplified) operator))

148

(appending (cdr simplified))

149

(collect simplified)))))

150

(case (and (listp form)

151

(first form))

152

(not

153

(bind ((arg (simplify-boolean-form (first (cdr form)))))

154

(cond ((and (listp arg)

155

(eq 'not (first arg)))

156

(second arg))

157

((eq #f arg)

158

#t)

159

((eq #t arg)

160

#f)

161

(t form))))

162

(or

163

(bind ((operands (remove #f (simplify-args 'or (cdr form)))))

164

(cond

165

((null operands) #f)

166

((length=1 operands) (first operands))

167

((some #L(eq !1 #t) operands) #t)

168

(t `(or ,@operands)))))

169

(and

170

(bind ((operands (remove #t (simplify-args 'and (cdr form)))))

171

(cond

172

((null operands) #t)

173

((length=1 operands) (first operands))

174

((some #L(eq !1 #f) operands) #f)

175

(t `(and ,@operands)))))

176

(t

177

form))))