Skip to content

Commit

Permalink
SNL導出を実装
Browse files Browse the repository at this point in the history
  • Loading branch information
@moratori
moratori committed Jun 19, 2022
1 parent 4e7b209 commit 46eba0e
Show file tree
Hide file tree
Showing 6 changed files with 395 additions and 112 deletions.
94 changes: 60 additions & 34 deletions src/clover.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,25 +2,25 @@
(:use :cl
:clover.property
:clover.search.common
:clover.search.iddfs
:clover.search.astar
:clover.search.extractor
:clover.search.iddfs
:clover.search.dfs
:clover.types
:clover.resolution
:clover.util
)
(:import-from :alexandria
:median
:variance
:compose)
:variance)
(:import-from :clover.unify
:alphabet=)
(:import-from :clover.rewrite
:rewrite-final)
(:import-from :clover.multiprocess
:initialize-lparallel-kernel)
(:export
:start_resolution
:start_trs
:find-lemmas
))
(in-package :clover.clover)

Expand All @@ -45,7 +45,7 @@
(defmethod cost-to-goal ((node clause-set))
(loop
:for clause :in (clause-set.clauses node)
:minimize (length (clause.literals clause))))
:minimize (clause-length clause)))

(defmethod cost-to-neighbor ((node1 clause-set) (node2 clause-set))
(let ((clauses (clause-set.clauses node2)))
Expand All @@ -54,7 +54,7 @@
(length clauses)
(median
(mapcar
(compose #'length #'clause.literals)
#'clause-length
clauses))
(1+ (variance
(mapcar #'clause.used-cnt clauses))))
Expand All @@ -72,36 +72,62 @@
(values (term= final-left final-right)
(equation negation final-left final-right)))))


(defmethod prepare-resolution ((clause-set clause-set))
"頂節とresolution-modeを決定し、clause-setを返却する"
(let* ((clauses
(clause-set.clauses clause-set))
(conseq
(find-if (lambda (clause)
(eq :conseq (clause.clause-type clause)))
clauses))
(base-clauses
(progn
(when (null conseq)
(error "consequent clause is required"))
(remove conseq clauses :test #'clause=)))
(centerlized-clause
(clause
(clause.literals conseq)
(clause.parent1 conseq)
(clause.parent2 conseq)
(clause.unifier conseq)
:center)))
(clause-set
(cons centerlized-clause base-clauses)
(cond
((and (horn-p clause-set) (goal-clause-p conseq))
:snl)
(t :default)))))

(defmethod start_resolution ((clause-set clause-set))

(when (some
(lambda (c) (null (clause.clause-type c)))
(clause-set.clauses clause-set))
(error "clause type must not be null"))
(cond
(t
(default-resolution clause-set))))


(defmethod default-resolution ((clause-set clause-set))
(let ((clauses (clause-set.clauses clause-set)))
(loop
:named exit
:for raw :in (append (remove-if-not #'conseq-clause-p clauses)
(remove-if #'conseq-clause-p clauses))
:for centerlized-clause := (clause
(clause.literals raw)
(clause.parent1 raw)
(clause.parent2 raw)
(clause.unifier raw)
:center)
:for centerlized-clauses := (cons centerlized-clause
(remove raw
clauses
:test #'clause=))
:do
(multiple-value-bind
(foundp value) (astar (clause-set centerlized-clauses
:default))
(when foundp
(return-from exit (values foundp value)))))))

(when (< 1
(count-if
(lambda (clause)
(eq (clause.clause-type clause) :conseq))
(clause-set.clauses clause-set)))
(error "multiple consequence clause found"))

(let* ((target
(prepare-resolution clause-set))
(available-search
(list
#'astar))
(result
(some
(lambda (fn)
(multiple-value-bind (foundp node)
(funcall fn target)
(when foundp
(list foundp node))))
available-search)))
(if result
(values-list result)
(values nil nil))))

109 changes: 93 additions & 16 deletions src/resolution.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,20 +12,19 @@
(:import-from :alexandria
:shuffle)
(:export
:%collect-resolutable-literal
:%resolution
:resolution
:resolution-wrapper
:opener_clause-set
:comprehensive-resolvent
)
)
(in-package :clover.resolution)



(defmethod %resolution ((parent1 clause) (parent2 clause) &optional
(get-resolvent-type (lambda (c) :resolvent))
(get-parent1-type (lambda (c) :resolvent))
(get-parent2-type (lambda (c) :resolvent)))
(defmethod resolution ((parent1 clause) (parent2 clause) (resolution-mode (eql :default)) &optional
(get-resolvent-type (lambda (c) :resolvent))
(get-parent1-type (lambda (c) :resolvent))
(get-parent2-type (lambda (c) :resolvent)))
(let ((literals1 (clause.literals parent1))
(literals2 (clause.literals parent2)))
(values
Expand Down Expand Up @@ -78,15 +77,70 @@
(funcall get-resolvent-type resolvent)))))))


(defmethod comprehensive-resolvent ((clause-set clause-set)
(defmethod resolution ((parent1 clause) (parent2 clause) (resolution-mode (eql :snl)) &optional
(get-resolvent-type (lambda (c) :resolvent))
(get-parent1-type (lambda (c) :resolvent))
(get-parent2-type (lambda (c) :resolvent)))

(assert (and (goal-clause-p parent1)
(or (rule-clause-p parent2)
(fact-clause-p parent2))))

(let* ((literals1 (clause.literals parent1))
(literals2 (clause.literals parent2))
(last-literal (first (last literals1)))
(last-literal-negation (literal.negation last-literal))
; last-literalと相補的な関係になるのは、literals2中に1つしかない
(opposite
(find-if (lambda (x) (eq nil (literal.negation x)))
literals2))
(us
(handler-case
(find-most-general-unifier-set
last-literal opposite)
(ununifiable-error (e) nil)))
(result
(when us
(let* ((res-clause-left (apply-unifier-set parent1 us))
(res-clause-left-literals (clause.literals res-clause-left))
(res-clause-right (apply-unifier-set parent2 us))
(res-clause-right-literals (clause.literals res-clause-right))
(target-literal (apply-unifier-set last-literal us))
(resolvent (append (remove target-literal res-clause-left-literals
:test #'literal=)
(remove target-literal res-clause-right-literals
:test #'complement-literal-p))))
(clause
resolvent
(when *save-resolution-history* parent1)
(when *save-resolution-history* parent2)
(when *save-resolution-history* us)
(funcall get-resolvent-type resolvent))))))
(values
(clause
(clause.literals parent1)
(clause.parent1 parent1)
(clause.parent2 parent1)
(clause.unifier parent1)
(funcall get-parent1-type parent1)
(1+ (clause.used-cnt parent1)))
(clause
(clause.literals parent2)
(clause.parent1 parent2)
(clause.parent2 parent2)
(clause.unifier parent2)
(funcall get-parent2-type parent2)
(1+ (clause.used-cnt parent2)))
(when result (list result)))))


(defmethod resolution-wrapper ((clause-set clause-set)
(parent1 clause)
(parent2 clause)
resolution-mode
(resolvent-type function)
(parent1-type function)
(parent2-type function))
"節parent1,parent2の導出結果(resolvent)を網羅的に計算し、
各resolventをclause-setに追加して返却する"
(let ((base-clauses
(remove-if
(lambda (clause)
Expand All @@ -95,12 +149,13 @@
(clause-set.clauses clause-set))))
(multiple-value-bind
(new-parent1 new-parent2 resoluted-clauses)
(%resolution parent1 parent2 resolvent-type parent1-type parent2-type)
(resolution parent1 parent2 resolution-mode resolvent-type parent1-type parent2-type)
(mapcar
(lambda (clause)
(clause-set
(append base-clauses
(list clause new-parent1 new-parent2))
(append (list clause new-parent2)
base-clauses
(list new-parent1))
resolution-mode))
resoluted-clauses))))

Expand All @@ -112,8 +167,7 @@
resolution-mode))



(defmethod opener_clause-set :before ((clause-set clause-set) (resolution-mode (eql :default)))
(defmethod opener_clause-set :before ((clause-set clause-set) resolution-mode)
(when (< 1 (count-if
(lambda (c)
(eq (clause.clause-type c) :center))
Expand All @@ -135,7 +189,7 @@
:for clause-type := (clause.clause-type clause)
:unless (eq clause-type :center)
:append
(comprehensive-resolvent
(resolution-wrapper
clause-set
center-clause
clause
Expand All @@ -144,3 +198,26 @@
(lambda (x) :resolvent)
(lambda (x) clause-type))))))


(defmethod opener_clause-set ((clause-set clause-set) (resolution-mode (eql :snl)))
(let* ((clauses
(clause-set.clauses clause-set))
(center-clause
(find-if
(lambda (c) (eq (clause.clause-type c) :center))
clauses)))
(when center-clause
(loop
:for clause :in clauses
:for clause-type := (clause.clause-type clause)
:if (eq clause-type :premise)
:append
(resolution-wrapper
clause-set
center-clause
clause
resolution-mode
(lambda (x) :center)
(lambda (x) :resolvent)
(lambda (x) :premise))))))

19 changes: 19 additions & 0 deletions src/util.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@
:consistent-unifier-set-p
:horn-p
:goal-clause-p
:rule-clause-p
:fact-clause-p
:clause-subset
:term=
:term/=
Expand Down Expand Up @@ -249,6 +251,23 @@
(eq (literal.negation lit) t))
(clause.literals clause)))

(defmethod rule-clause-p ((clause clause))
(let ((len (clause-length clause)))
(and
(= 1
(count-if
(lambda (x) (eq (literal.negation x) nil))
(clause.literals clause)))
(= (1- len)
(count-if
(lambda (x) (eq (literal.negation x) t))
(clause.literals clause))))))

(defmethod fact-clause-p ((clause clause))
(and
(= 1 (clause-length clause))
(eq nil (literal.negation (first (clause.literals clause))))))

(defmethod conseq-clause-p ((clause clause))
(eq (clause.clause-type clause) :conseq))

Expand Down
Loading

0 comments on commit 46eba0e

Please sign in to comment.