From ca532c106c1d23982661d04adbe6e8117d8b6319 Mon Sep 17 00:00:00 2001 From: Jonathan Schwarz Date: Thu, 4 Mar 2021 09:28:30 +0000 Subject: [PATCH] Crediting Alex Matthews as a code contributor PiperOrigin-RevId: 360859332 --- .../frcl.ipynb | 3 +- satore/Clause.rkt | 246 +++++ satore/README.md | 50 + satore/clause-format.rkt | 41 + satore/clause.rkt | 197 ++++ satore/examples/binary30.p | 62 ++ satore/examples/socrates.p | 3 + satore/info.rkt | 30 + satore/interact.rkt | 96 ++ satore/json-output.rkt | 65 ++ satore/log.rkt | 57 ++ satore/main.rkt | 42 + satore/misc.rkt | 90 ++ satore/rewrite-tree.rkt | 668 +++++++++++++ satore/saturation.rkt | 895 ++++++++++++++++++ satore/scribblings/satore.scrbl | 5 + satore/tests/Clause.rkt | 12 + satore/tests/clause.rkt | 197 ++++ satore/tests/confluence.rkt | 118 +++ satore/tests/interact.rkt | 34 + satore/tests/misc.rkt | 5 + satore/tests/rewrite-tree.rkt | 250 +++++ satore/tests/saturation.rkt | 348 +++++++ satore/tests/stress-test1.rkt | 34 + satore/tests/timeplus.rkt | 13 + satore/tests/trie.rkt | 81 ++ satore/tests/unification-tree.rkt | 69 ++ satore/tests/unification.rkt | 381 ++++++++ satore/tptp.rkt | 218 +++++ satore/trie.rkt | 220 +++++ satore/unification-tree.rkt | 346 +++++++ satore/unification.rkt | 705 ++++++++++++++ 32 files changed, 5580 insertions(+), 1 deletion(-) create mode 100644 satore/Clause.rkt create mode 100644 satore/README.md create mode 100644 satore/clause-format.rkt create mode 100644 satore/clause.rkt create mode 100644 satore/examples/binary30.p create mode 100644 satore/examples/socrates.p create mode 100644 satore/info.rkt create mode 100644 satore/interact.rkt create mode 100644 satore/json-output.rkt create mode 100644 satore/log.rkt create mode 100755 satore/main.rkt create mode 100644 satore/misc.rkt create mode 100644 satore/rewrite-tree.rkt create mode 100644 satore/saturation.rkt create mode 100644 satore/scribblings/satore.scrbl create mode 100644 satore/tests/Clause.rkt create mode 100644 satore/tests/clause.rkt create mode 100644 satore/tests/confluence.rkt create mode 100644 satore/tests/interact.rkt create mode 100644 satore/tests/misc.rkt create mode 100644 satore/tests/rewrite-tree.rkt create mode 100644 satore/tests/saturation.rkt create mode 100644 satore/tests/stress-test1.rkt create mode 100644 satore/tests/timeplus.rkt create mode 100644 satore/tests/trie.rkt create mode 100644 satore/tests/unification-tree.rkt create mode 100644 satore/tests/unification.rkt create mode 100644 satore/tptp.rkt create mode 100644 satore/trie.rkt create mode 100644 satore/unification-tree.rkt create mode 100644 satore/unification.rkt diff --git a/functional_regularisation_for_continual_learning/frcl.ipynb b/functional_regularisation_for_continual_learning/frcl.ipynb index 415ef02..5eb2ed0 100644 --- a/functional_regularisation_for_continual_learning/frcl.ipynb +++ b/functional_regularisation_for_continual_learning/frcl.ipynb @@ -60,7 +60,8 @@ "code authors:\n", "\n", "* Jonathan Schwarz (schwarzjn@google.com)\n", - "* Michalis Titsias (mtitsias@google.com)" + "* Michalis Titsias (mtitsias@google.com)\n", + "* Alex Matthews (alexmatthews@google.com)" ] }, { diff --git a/satore/Clause.rkt b/satore/Clause.rkt new file mode 100644 index 0000000..41e3de8 --- /dev/null +++ b/satore/Clause.rkt @@ -0,0 +1,246 @@ +#lang racket/base + +;**************************************************************************************; +;**** Clause: Clauses With Additional Properties In A Struct ****; +;**************************************************************************************; + +(require define2 + define2/define-wrapper + global + racket/format + racket/list + racket/string + satore/clause + satore/clause-format + satore/misc + satore/unification + text-table) + +(provide (all-defined-out)) + +;==============; +;=== Clause ===; +;==============; + +;; TODO: A lot of space is wasted in Clause (boolean flags?) +;; What's the best way to gain space without losing time or readability? + +;; parents : (listof Clause?) ; The first parent is the 'mother'. +;; binary-rewrite-rule? : Initiually #false, set to #true if the clause has been added (at some point) +;; to the binary rewrite rules (but may not be in the set anymore if subsumed). +;; size: tree-size of the clause. +;; depth: Maternal-path depth. +;; cost: Maternal-path cost. +(struct Clause (idx + parents + clause + type + [binary-rewrite-rule? #:mutable] + [candidate? #:mutable] + [discarded? #:mutable] + n-literals + size + depth + [cost #:mutable] + [g-cost #:mutable]) + #:prefab) + +(define-counter clause-index 0) + +(define (make-Clause cl + [parents '()] + #:type [type '?] + #:candidate? [candidate? #false] + #:n-literals [n-literals (length cl)] + #:size [size (clause-size cl)] + #:depth [depth (if (empty? parents) 1 (+ 1 (Clause-depth (first parents))))]) + (++clause-index) + (when-debug>= steps + (define cl2 (clause-normalize cl)) ; costly, hence done only in debug mode + (unless (= (tree-size cl) (tree-size cl2)) + (displayln "Assertion failed: clause is in normal form") + (printf "Clause (type: ~a):\n~a\n" type (clause->string cl)) + (displayln "Parents:") + (print-Clauses parents) + (error (format "Assertion failed: (= (tree-size cl) (tree-size cl2)): ~a ~a" + (tree-size cl) (tree-size cl2))))) + ; Notice: Variables are ASSUMED freshed. Freshing is not performed here. + (Clause clause-index + parents + cl + type + #false ; binary-rewrite-rule + candidate? + #false ; discarded? + n-literals + size + depth ; depth (C0 is of depth 0, axioms are of depth 1) + 0. ; cost + 0. ; g-cost + )) + +(define (discard-Clause! C) (set-Clause-discarded?! C #true)) + +(define true-Clause (make-Clause (list ltrue))) + +;; For temporary converse Clauses for binary clauses. +(define (make-converse-Clause C #:candidate? [candidate? #false]) + (if (unit-Clause? C) + true-Clause ; If C has 1 literal A, then C = A | false, and converse is ~A | true = true + (make-Clause (fresh (clause-converse (Clause-clause C))) + (list C) + #:type 'converse + #:candidate? candidate? + ))) + +(define Clause->string-all-fields '(idx parents clause type binary-rw? depth size cost)) + +;; If what is a list, each element is printed (possibly multiple times). +;; If what is 'all, all fields are printed. +(define (Clause->list C [what '(idx parents clause)]) + (when (eq? what 'all) + (set! what Clause->string-all-fields)) + (for/list ([w (in-list what)]) + (case w + [(idx) (~a (Clause-idx C))] + [(parents) (~a (map Clause-idx (Clause-parents C)))] + [(clause) (clause->string (Clause-clause C))] + [(clause-pretty) (clause->string/pretty (Clause-clause C))] + [(type) (~a (Clause-type C))] + [(binary-rw?) (~a (Clause-binary-rewrite-rule? C))] + [(depth) (~r (Clause-depth C))] + [(size) (~r (Clause-size C))] + [(cost) (~r2 (Clause-cost C))]))) + +(define (Clause->string C [what '(idx parents clause)]) + (string-join (Clause->list C what) " ")) + +(define (Clause->string/alone C [what '(idx parents clause)]) + (when (eq? what 'all) + (set! what Clause->string-all-fields)) + (string-join (map (λ (f w) (format "~a: ~a " w f)) + (Clause->list C what) + what) + " ")) + +(define (print-Clauses Cs [what '(idx parents clause)]) + (when (eq? what 'all) + (set! what Clause->string-all-fields)) + (print-simple-table + (cons what + (map (λ (C) (Clause->list C what)) Cs)))) + +;; <=> to avoid hard-to-debug mistakes where Clause-subsumes is used instead of Clause<-subsumes +;; for example. +;; Notice: This is an approximation of the correct subsumption based on multisets, and may not +;; be confluent. +(define (Clause<=>-subsumes C1 C2) + (clause-subsumes (Clause-clause C1) (Clause-clause C2))) + +;; Use atom<=> ? +(define Clause-cmp-key Clause-size) +(define (Clause<= C1 C2) (<= (Clause-cmp-key C1) (Clause-cmp-key C2))) +(define (Clause< C1 C2) (< (Clause-cmp-key C1) (Clause-cmp-key C2))) + +(define (Clause<=-subsumes C1 C2) + (and (Clause<= C1 C2) + (Clause<=>-subsumes C1 C2))) + +(define (Clause<-subsumes C1 C2) + (and (Clause< C1 C2) + (Clause<=>-subsumes C1 C2))) + +;; Useful for rewrite rules +(define (Clause<=>-converse-subsumes C1 C2) + (clause-subsumes (clause-converse (Clause-clause C1)) + (Clause-clause C2))) + +(define (unit-Clause? C) + (= 1 (Clause-n-literals C))) + +(define (binary-Clause? C) + (= 2 (Clause-n-literals C))) + +(define (Clause-tautology? C) + (clause-tautology? (Clause-clause C))) + +;; Returns the tree of ancestor Clauses of C up to init Clauses, +;; but each Clause appears only once in the tree. +;; (The full tree can be further retrieved from the Clause-parents.) +;; Used for proofs. +(define (Clause-ancestor-graph C #:depth [dmax +inf.0]) + (define h (make-hasheq)) + (let loop ([C C] [depth 0]) + (cond + [(or (> depth dmax) + (hash-has-key? h C)) + #false] + [else + (hash-set! h C #true) + (cons C (filter-map (λ (C2) (loop C2 (+ depth 1))) + (Clause-parents C)))]))) + +(define (Clause-ancestor-graph-string C + #:? [depth +inf.0] + #:? [prefix ""] + #:? [tab " "] + #:? [what '(idx parents type clause)]) + (define h (make-hasheq)) + (define str-out "") + (let loop ([C C] [d 0]) + (unless (or (> d depth) + (hash-has-key? h C)) + (set! str-out (string-append str-out + prefix + (string-append* (make-list d tab)) + (Clause->string C what) + "\n")) + (hash-set! h C #true) + (for ([P (in-list (Clause-parents C))]) + (loop P (+ d 1))))) + str-out) + +(define-wrapper (display-Clause-ancestor-graph + (Clause-ancestor-graph-string C #:? depth #:? prefix #:? tab #:? what)) + #:call-wrapped call + (display (call))) + +(define (Clause-age<= C1 C2) + (<= (Clause-idx C1) (Clause-idx C2))) + +(define (save-Clauses! Cs f #:? exists) + (save-clauses! (map Clause-clause Cs) f #:exists exists)) + +(define (load-Clauses f #:? [sort? #true] #:? [type 'load]) + (define Cs (map (λ (c) (make-Clause c #:type type)) + (load-clauses f))) + (if sort? + (sort Cs Clause<=) + Cs)) + +(define (Clause-equivalence? C1 C2) + (and (Clause<=>-subsumes C1 C2) + (Clause<=>-subsumes C2 C1))) + +;; Provides testing utilities. Use with `(require (submod "Clause.rkt" test))`. +(module+ test + (require rackunit) + (provide Clausify + check-Clause-set-equivalent?) + + (define Clausify (compose make-Clause clausify)) + + (define-check (check-Clause-set-equivalent? Cs1 Cs2) + (unless (= (length Cs1) (length Cs2)) + (fail-check "not =")) + (for/fold ([Cs2 Cs2]) + ([C1 (in-list Cs1)]) + (define C1b + (for/first ([C2 (in-list Cs2)] #:when (Clause-equivalence? C1 C2)) + C2)) + (unless C1b + (printf "Cannot find equivalence Clause for ~a\n" (Clause->string C1)) + (print-Clauses Cs1) + (print-Clauses Cs2) + (fail-check)) + (remq C1b Cs2)))) diff --git a/satore/README.md b/satore/README.md new file mode 100644 index 0000000..555b8ff --- /dev/null +++ b/satore/README.md @@ -0,0 +1,50 @@ +# Satore: First-order logic saturation with atomic rewriting + +This is a first-order logic resolution based theorem prover in CNF without +equality, but with atom rewrite rules. New rewrite rules can be +discovered during the proof search, potentially reducing exponentially the +search space. + +Satore stands for Saturation with Atom Rewriting. + +## Installation + +### Install racket (Apache2/MIT): +* Windows, MacOS X: https://download.racket-lang.org +* Ubuntu/Debian: `[sudo] apt install racket` +* Linux (other): [Download](https://download.racket-lang.org) the `.sh` and + install it with `[sudo] sh racket-.sh` + +You may need to configure the PATH environment variable to include the +directory containing the `racket` and `raco` executables. +For Windows this directory should be something like +`C:>Program Files\Racket`. + +### Install satore and its dependencies (all are Apache2/MIT licensed): + +In a directory of your choice, type: + +```shell +git clone https://github.com/deepmind/deepmind-research/tree/master/satore +raco pkg install --auto --link satore +``` + +## Running Satore + +Run a trivial example: + +```shell +racket -l- satore -p satore/examples/socrates.p --proof +``` + +To see the various flags: + +```shell +racket -l- satore --help +``` + +The .p file is assumed to be a standalone file with only comments and +`cnf(…).` lines without equality, where the logic clause must be surrounded by +parentheses. All axioms must be included. (This will likely be improved soon.) + +Note that `racket -l- satore` can be invoked from anywhere. diff --git a/satore/clause-format.rkt b/satore/clause-format.rkt new file mode 100644 index 0000000..30cd2ef --- /dev/null +++ b/satore/clause-format.rkt @@ -0,0 +1,41 @@ +#lang racket/base + +;***************************************************************************************; +;**** Clause <-> String Conversions ****; +;***************************************************************************************; + +;;; In a separate file because of cyclic dependencies with "tptp.rkt" if in "clause.rkt" + +(require racket/format + racket/list + racket/pretty + satore/clause + satore/tptp + satore/unification + text-table) + +(provide (all-defined-out)) + +(define (clause->string cl) + ((if (*tptp-out?*) + clause->tptp-string + ~a) + (Vars->symbols cl))) + +(define (clause->string/pretty cl) + (pretty-format (Vars->symbols cl))) + +(define (print-clause cl) + (displayln (clause->string cl))) + +(define (print-clauses cls #:sort? [sort? #false]) + (unless (empty? cls) + (print-table + (for/list ([cl (in-list (if sort? + (sort cls < #:key tree-size #:cache-keys? #true) + cls))] + [i (in-naturals)]) + (cons i (Vars->symbols cl))) + #:border-style 'space + #:row-sep? #false + #:framed? #false))) diff --git a/satore/clause.rkt b/satore/clause.rkt new file mode 100644 index 0000000..f67b0a6 --- /dev/null +++ b/satore/clause.rkt @@ -0,0 +1,197 @@ +#lang racket/base + +;***************************************************************************************; +;**** Operations on clauses ****; +;***************************************************************************************; + +(require bazaar/cond-else + bazaar/debug + bazaar/list + bazaar/loop + bazaar/mutation + (except-in bazaar/order atom<=>) + define2 + global + racket/file + racket/format + racket/list + racket/pretty + satore/misc + satore/trie + satore/unification + syntax/parse/define + text-table) + +(provide (all-defined-out)) + +(define-global *subsumes-iter-limit* 0 + '("Number of iterations in the θ-subsumption loop before failing." + "May help in cases where subsumption take far too long." + "0 = no limit.") + exact-nonnegative-integer? + string->number) + +(define-counter n-tautologies 0) + +(define (sort-clause cl) + (sort cl literal p n)) + #:cond + [(order? c) (loop pos (rest pneg))] + [(literal==? p n)] + #:else (error "uh?")))) + (begin (++n-tautologies) #true))) + +;; NOTICE: This does *not* rename the variables. +(define (clause-converse cl) + (sort-clause (map lnot cl))) + +;; Assumes that cl is sorted according to `sort-clause`. +(define (remove-duplicate-literals cl) + (zip-loop ([(x r) cl] [res '()] #:result (reverse res)) + (cond/else + [(empty? r) (cons x res)] + #:else + (define y (first r)) + #:cond + [(literal==? x y) res] + #:else (cons x res)))) + +(define (predicate.arity lit) + (cond [(list? lit) (cons (first lit) (length lit))] + [else (cons lit 0)])) + + +(define-counter n-subsumes-checks 0) +(define-counter n-subsumes-steps 0) +(define-counter n-subsumes-breaks 0) +(define (reset-subsumes-stats!) + (reset-n-subsumes-checks!) + (reset-n-subsumes-steps!) + (reset-n-subsumes-breaks!)) + + +;; θ-subsumption. +;; ca θ-subsumes cb if there exists a substitution α such that ca[α] ⊆ cb +;; (requires removing duplicate literals as in FOL clauses are assumed to be sets of literals). +;; Assumes vars(ca) ∩ vars(cb) = ∅. + +(define (clause-subsumes ca cb) + (++n-subsumes-checks) + ; For every each la of ca with current substitution β, we need to find a literal lb of cb + ; such that we can extend β to β' so that la[β'] = lb. + ; TODO: order the groups by smallest size for cb. + ; TODO: need to split by polarity first, or sort by (polarity predicate arity) + ; For each literal of ca, obtain the list of literals of cb that unify with it. + ; place cb in a trie + ; then retrieve + + (define cbtrie (make-trie #:variable? Var?)) + (for ([litb (in-list cb)]) + ; the key must be a list, but a literal may be just a constant, so we need to `list` it. + (trie-insert! cbtrie (list litb) litb)) + + ;; Each literal lita of ca is paired with a list of potential literals in cb that lita matches, + ;; for subsequent left-unification. + ;; We sort the groups by smallest size first, to fail fast. + (define groups + (sort + (for/list ([lita (in-list ca)]) + ; lita must match litb, hence inverse-ref + (cons lita (append* (trie-inverse-ref cbtrie (list lita))))) + < #:key length #:cache-keys? #true)) + + ;; Depth-first search while trying to find a substitution that works for all literals of ca. + ;; TODO: if number of iterations is larger than threshold, abort (use let/ec) + (define n-iter-max (*subsumes-iter-limit*)) + (define n-iter 0) + + (let/ec return + (let loop ([groups groups] [subst '()]) + (++ n-iter) + (when (= n-iter n-iter-max) ; if n-iter-max = 0 then no limit + (++n-subsumes-breaks) + (return #false)) + (++n-subsumes-steps) + (cond + [(empty? groups) subst] + [else + (define-values (lita litbs) (car+cdr (first groups))) + (for/or ([litb (in-list litbs)]) + ; We use a immutable substitution to let racket handle copies when needed. + (define new-subst (left-unify/assoc lita litb subst)) + (and new-subst (loop (rest groups) new-subst)))])))) + +;; Assumes that the clause cl is sorted according to `sort-clause`. +;; A safe factor f of cl is such that f[α] ⊆ cl for some subst α, that is, +;; f θ-subsumes cl. But since cl necessarily θ-subsumes all of its factors XXX +;; - The return value is eq? to the argument cl if no safe-factoring is possible. +;; - Applies safe-factoring as much as possible. +(define (safe-factoring cl) + (let/ec return + (zip-loop ([(l x r) cl]) + (define pax (predicate.arity x)) + (zip-loop ([(l2 y r2) r] #:break (not (equal? pax (predicate.arity y)))) + ; To avoid code duplication: + (define-simple-macro (attempt a b) + (begin + (define s (left-unify a b)) + (when s + (define new-cl + (sort-clause + (fresh ; required for clause-subsumes below + (left-substitute (rev-append l (rev-append l2 (cons a r2))) ; remove b + s)))) + (when (clause-subsumes new-cl cl) + ; Try one more time with new-cl. + (return (safe-factoring new-cl)))))) + + (attempt x y) + (attempt y x))) + cl)) + +(define (clause-equivalence? A B) + (and (clause-subsumes A B) + (clause-subsumes B A))) + +;==============; +;=== Saving ===; +;==============; + +(define (save-clauses! cls f #:? [exists 'replace]) + (with-output-to-file f #:exists exists + (λ () (for-each writeln cls)))) + +(define (load-clauses f) + (map clausify (file->list f))) diff --git a/satore/examples/binary30.p b/satore/examples/binary30.p new file mode 100644 index 0000000..7ebc8bb --- /dev/null +++ b/satore/examples/binary30.p @@ -0,0 +1,62 @@ +cnf(i_0, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a))). +cnf(i_1, plain, (~num(b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27, X28) | num(a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27, X28))). +cnf(i_2, plain, (num(b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27, X28) | ~num(a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27, X28))). +cnf(i_3, plain, (~num(a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27) | num(b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27))). +cnf(i_4, plain, (num(a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27) | ~num(b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27))). +cnf(i_5, plain, (~num(a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26) | num(b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26))). +cnf(i_6, plain, (num(a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26) | ~num(b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26))). +cnf(i_7, plain, (~num(a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25) | num(b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25))). +cnf(i_8, plain, (num(a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25) | ~num(b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25))). +cnf(i_9, plain, (~num(a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24) | num(b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24))). +cnf(i_10, plain, (num(a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24) | ~num(b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24))). +cnf(i_11, plain, (~num(a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23) | num(b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23))). +cnf(i_12, plain, (num(a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23) | ~num(b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23))). +cnf(i_13, plain, (~num(a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22) | num(b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22))). +cnf(i_14, plain, (num(a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22) | ~num(b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22))). +cnf(i_15, plain, (~num(a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21) | num(b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21))). +cnf(i_16, plain, (num(a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21) | ~num(b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21))). +cnf(i_17, plain, (~num(a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20) | num(b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20))). +cnf(i_18, plain, (num(a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20) | ~num(b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20))). +cnf(i_19, plain, (~num(a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19) | num(b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19))). +cnf(i_20, plain, (num(a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19) | ~num(b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19))). +cnf(i_21, plain, (~num(a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18) | num(b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18))). +cnf(i_22, plain, (num(a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18) | ~num(b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18))). +cnf(i_23, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17) | num(b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17))). +cnf(i_24, plain, (num(a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17) | ~num(b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17))). +cnf(i_25, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16) | num(b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16))). +cnf(i_26, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16))). +cnf(i_27, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15))). +cnf(i_28, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15))). +cnf(i_29, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14))). +cnf(i_30, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14))). +cnf(i_31, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13))). +cnf(i_32, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13))). +cnf(i_33, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12))). +cnf(i_34, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12))). +cnf(i_35, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11))). +cnf(i_36, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11))). +cnf(i_37, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10))). +cnf(i_38, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9, X10))). +cnf(i_39, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9))). +cnf(i_40, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8, X9))). +cnf(i_41, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8))). +cnf(i_42, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7, X8) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7, X8))). +cnf(i_43, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7))). +cnf(i_44, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6, X7) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6, X7))). +cnf(i_45, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6))). +cnf(i_46, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5, X6) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5, X6))). +cnf(i_47, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5))). +cnf(i_48, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4, X5) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4, X5))). +cnf(i_49, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4))). +cnf(i_50, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3, X4) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3, X4))). +cnf(i_51, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3))). +cnf(i_52, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2, X3) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2, X3))). +cnf(i_53, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2))). +cnf(i_54, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1, X2) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1, X2))). +cnf(i_55, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1))). +cnf(i_56, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0, X1) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0, X1))). +cnf(i_57, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0))). +cnf(i_58, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b, X0) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a, X0))). +cnf(i_59, plain, (~num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b) | num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a))). +cnf(i_60, plain, (num(a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, b) | ~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, a))). +cnf(i_0, negated_conjecture, (~num(b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b, b))). diff --git a/satore/examples/socrates.p b/satore/examples/socrates.p new file mode 100644 index 0000000..ef3df55 --- /dev/null +++ b/satore/examples/socrates.p @@ -0,0 +1,3 @@ +cnf(humans_are_mortal, axiom, (~human(X) | mortal(X))). +cnf(socrates_is_human, hypothesis, (human(c))). +cnf(socrates_is_mortal, negated_conjecture, (~mortal(c))). diff --git a/satore/info.rkt b/satore/info.rkt new file mode 100644 index 0000000..cba2d0a --- /dev/null +++ b/satore/info.rkt @@ -0,0 +1,30 @@ +#lang info +(define collection "satore") +(define deps '("bazaar" + "data-lib" + "define2" + "global" + "math-lib" + "text-table" + "base")) +(define build-deps '("rackunit-lib" + "scribble-lib" + )) +(define scribblings '(("scribblings/satore.scrbl" ()))) +(define pkg-desc "First-order logic prover in CNF without equality, but with atom rewrite rules") +(define version "0.1") +(define pkg-authors '(orseau)) + +(define racket-launcher-names '("satore")) +(define racket-launcher-libraries '("satore.rkt")) + +(define test-omit-paths '("info.rkt" + "last-results.rkt" + "parse-log.rkt" + "in-progress/" + "find-rules.rkt" + "print-rules.rkt" + "run-eprover.rkt" + "rules/" + "logs/" + "scribblings/")) diff --git a/satore/interact.rkt b/satore/interact.rkt new file mode 100644 index 0000000..87cd02b --- /dev/null +++ b/satore/interact.rkt @@ -0,0 +1,96 @@ +#lang racket/base + +;***************************************************************************************; +;**** User Interaction Commands ****; +;***************************************************************************************; + +(require (for-syntax racket/base syntax/parse) + racket/format + racket/list + racket/match + racket/port) + +(provide (all-defined-out)) + +;; Notice: variables set via eval or only set locally, in the local namespace, +;; and not in the main namespace. +;; variables set via the (list 'var val) pattern are set in the main namespace. +;; Even though the namespace is at the module level, the variables +;; are set in the namespace with their value so they can be used with eval. +;; TODO: When a ns-anchor is given, commands are eval'ed by default, and to directly modify +;; variables one must use ! (where the second argument is evaled) +(define-syntax (interact stx) + (syntax-parse stx + #:literals (list) + [(_ (~alt (~optional (~seq #:prompt prompt:expr)) ; must evaluate to a string, default "> " + (~optional (~seq #:command command:expr)) + (~optional (~seq #:namespace-anchor ns-anchor:expr)) ; default #false + (~optional (~seq #:variables (var:id ...))) ; must be bound identifiers + (~optional (~seq #:readline? readline?:expr))) ; start with readline enabled? (#false) + ... + [(list pat ...) help-string body ...+] ...) ; match patterns + (with-syntax ([(var ...) #'(~? (var ...) ())]) + #'(begin + (define names (list 'var ...)) + (define nsa (~? ns-anchor #false)) + (define ns (and nsa (namespace-anchor->namespace nsa))) + (when (~? readline? #false) (eval '(require readline) ns)) + (when ns + (namespace-set-variable-value! 'var var #false ns) ... + (void)) ; to avoid bad 'when' form if no variable + (define the-prompt (~? prompt "> ")) + (let loop () + (with-handlers ([exn:fail? (λ (e) + (displayln (exn-message e)) + (loop))]) + (define cmd (~? command #false)) + (when (and cmd (not (string? cmd))) + (error "command must be a string")) + (unless cmd (display the-prompt)) + (define cmd-str (or cmd (read-line))) + (unless (eof-object? cmd-str) + (define cmd (with-input-from-string (string-append "(" cmd-str ")") read)) + (match cmd + ['() (void)] + ['(help) + (unless (empty? names) + (printf "Available variables: ~a\n" names)) + (displayln "Other commands:") + (parameterize ([print-reader-abbreviations #true] + [print-as-expression #false]) + (void) + (begin + (displayln (string-append " " (apply ~v '(pat ...) #:separator " "))) + (displayln (string-append " " help-string))) + ...) + (when ns + (displayln " eval expr") + (displayln + " Evaluate expr in a namespace that is local to this interaction loop.")) + (loop)] + [(list 'eval cmd) + (if ns + (call-with-values (λ () (eval cmd ns)) + (λ l (if (= 1 (length l)) + (unless (void? (first l)) + (displayln (first l))) + (for-each displayln l)))) + (displayln "Cannot use eval without a namespace-anchor")) + (loop)] + ['(var) (println var) (loop)] ... + [(list 'var val) (set! var val) (loop)] ... + [(list pat ...) body ... (loop)] ... + [else (printf "Unknown command: ~a\n" cmd) + (loop)]))))))])) + +(module+ drracket + (define-namespace-anchor ns-anchor) ; optional, to use the eval command + + (let ([x 3] [y 'a]) + (interact + #:prompt ">> " + #:namespace-anchor ns-anchor + #:variables (x y) + ;; All patterns must be of the form (list ....) + [(list 'yo) "prints yo" (displayln "yo")] + [(list 'yo (? number? n)) "prints multiple yos" (displayln (make-list n 'yo))]))) diff --git a/satore/json-output.rkt b/satore/json-output.rkt new file mode 100644 index 0000000..12cbf44 --- /dev/null +++ b/satore/json-output.rkt @@ -0,0 +1,65 @@ +#lang racket/base + +;***************************************************************************************; +;**** Json Output ****; +;***************************************************************************************; + +(require bazaar/debug + racket/dict + racket/string) + +(provide (all-defined-out)) + +(define status-dict + '((running . UNSPECIFIED_PROOF_STATUS) + (refuted . REFUTATION_FOUND) + (time . TIME_LIMIT_REACHED) + (memory . MEMORY_LIMIT_REACHED) + (steps . STEP_LIMIT_REACHED) + (saturated . COUNTER_SATISFIABLE))) + +(define (saturation-result->json res) + (define d + (let* ([res (dict-remove res 'name)] + [res (dict-remove res 'file)] + [res (dict-update res 'status (λ (v) (dict-ref status-dict v)))]) + res)) + (string-join + #:before-first "{\n " + (for/list ([(k v) (in-dict d)]) + (define kstr (regexp-replace* #px"-|:" (symbol->string k) "_")) + (format "~s: ~s" kstr (if (symbol? v) (symbol->string v) v))) + ",\n " + #:after-last "\n}")) + +(module+ drracket + (define res + '((name . "GEO170+1.p") + (file . "data/tptp_geo/GEO170+1.p") + (status . refuted) + (steps . 205) + (generated . 3186) + (actives . 106) + (candidates . 2651) + (priority-remaining . 0) + (tautologies . 156) + (rules . 30) + (unit-rules . 24) + (binary-rules . 6) + (binary-rules-static . 0) + (binary-rules-dynamic . 6) + (binary-rewrites . 164) + (forward-subsumed . 96) + (backward-subsumed . 0) + (subsumes-checks . 7654) + (subsumes-steps . 13268) + (subsumes-breaks . 0) + (L-resolvent-pruning . 0) + (memory . 181509744) + (time . 196) + (proof-length . 12) + (proof-inferences . 5) + (proof-type:in . 7) + (proof-type:res . 4) + (proof-type:rw . 1))) + (displayln (saturation-result->json res))) diff --git a/satore/log.rkt b/satore/log.rkt new file mode 100644 index 0000000..4bd0457 --- /dev/null +++ b/satore/log.rkt @@ -0,0 +1,57 @@ +#lang racket/base + +;***************************************************************************************; +;**** Logging To File With Consistent Debugging Information ****; +;***************************************************************************************; + +(require bazaar/date + bazaar/debug + define2 + global + racket/file + racket/port + racket/pretty + racket/string + racket/system) + +(provide call-with-log + *log*) + +(define-global:boolean *log* #false + "Output to a log file?") + +(define-global:boolean *git?* #false + "Commit to git if needed and include the last git commit hash in the globals.") + +(define (call-with-log thunk + #:? [dir "logs"] + #:? [filename (string-append "log-" (date-iso-file) ".txt")] + ; if given, dir and filename have no effect: + #:? [filepath (build-path dir filename)] + #:? [log? (*log*)] + #:? [quiet? #false]) + + (when (*git?*) + (define cmd "git commit -am \".\" ") + (displayln cmd) + (system cmd)) + + ;; Non-quiet mode. + (define (thunk2) + ; Also write the last commit hash for easy retrieval. + (pretty-write + (list* `(cmd-line . ,(current-command-line-arguments)) + `(git-commit . ,(and (*git?*) + (string-normalize-spaces + (with-output-to-string (λ () (system "git rev-parse HEAD")))))) + (globals->assoc))) + (thunk)) + + (cond [log? + (make-parent-directory* filepath) + (assert (not (file-exists? filepath)) filepath) + (printf "Logging to: ~a\n" filepath) + (pretty-write (globals->assoc)) + (with-output-to-file filepath thunk2)] + [quiet? (thunk)] + [else (thunk2)])) diff --git a/satore/main.rkt b/satore/main.rkt new file mode 100755 index 0000000..a2b404b --- /dev/null +++ b/satore/main.rkt @@ -0,0 +1,42 @@ +#!/usr/bin/env racket +#lang racket/base + +;**************************************************************************************; +;**** Satore ****; +;**************************************************************************************; + +(module+ main + (require global + racket/file + racket/port + satore/misc + satore/rewrite-tree + satore/saturation + satore/unification) + + (define-global *prog* #false + '("Data file containing a single TPTP program." + "If not provided, reads from the input port.") + file-exists? + values + '("-p")) + + ;; If -p is not specified, reads from current-input-port + (void (globals->command-line #:program "satore")) + + ;; No validation here yet. + (define program + (if (*prog*) + (file->string (*prog*)) + (port->string))) + + (iterative-saturation + (λ (#:clauses input-clauses #:cpu-limit cpu-limit #:rwtree-in rwtree-in #:rwtree-out rwtree-out) + (saturation input-clauses + #:cpu-limit cpu-limit + #:rwtree rwtree-in + #:rwtree-out rwtree-out)) + #:tptp-program program + #:rwtree-in (make-rewrite-tree #:atom<=> (get-atom<=>) + #:dynamic-ok? (*dynamic-rules?*) + #:rules-file (*input-rules*)))) diff --git a/satore/misc.rkt b/satore/misc.rkt new file mode 100644 index 0000000..23bdd56 --- /dev/null +++ b/satore/misc.rkt @@ -0,0 +1,90 @@ +#lang racket/base + +;***************************************************************************************; +;**** Various Utilities ****; +;***************************************************************************************; + +(require (for-syntax racket/base racket/port racket/syntax syntax/parse) + (except-in bazaar/order atom<=>) + global + racket/contract + racket/format + racket/list + racket/match + racket/port + racket/struct + racket/stxparam) + +(provide (all-defined-out)) + +(print-boolean-long-form #true) + +(define-syntax-rule (begin-for-both e) + (begin + e + (begin-for-syntax e))) + +(begin-for-both + (define (debug-level->number lev) + (cond + [(number? lev) lev] + [(string? lev) (debug-level->number (with-input-from-string lev read))] + [else + (case lev + [(none) 0] + [(init) 1] + [(step steps) 2] + [(interact) 3] + [else (error "unknown debug level" lev)])]))) + +(define-global *debug-level* 0 + "Number or one of (none=0 init=1 steps interact)." + exact-nonnegative-integer? + debug-level->number + '("--debug")) + +(define (debug>= lev) + (>= (*debug-level*) (debug-level->number lev))) + +;; TODO: Make faster +(define-syntax (when-debug>= stx) + (syntax-case stx () + [(_ lev body ...) + (with-syntax ([levv (debug-level->number (syntax-e #'lev))]) + #'(when (>= (*debug-level*) levv) + body ...))])) + +(define (thunk? p) + (and (procedure? p) + (procedure-arity-includes? p 0))) + +;; Defines a counter with a reset function and an increment function +;; Ex: +;; (define-counter num 0) +;; (++num) +;; (++num 3) +;; (reset-num!) +(define-syntax (define-counter stx) + (syntax-case stx () + [(_ name init) + (with-syntax ([reset (format-id stx #:source stx "reset-~a!" (syntax-e #'name))] + [++ (format-id stx #:source stx "++~a" (syntax-e #'name))]) + #'(begin + (define name init) + (define (reset) + (set! name init)) + (define (++ [n 1]) + (set! name (+ name n)))))])) + + +(define (current-memory-use-MB) + (arithmetic-shift (current-memory-use) -20)) + +(define (car+cdr p) + (values (car p) (cdr p))) + +(define (~r2 x #:precision [precision 2]) + (if (rational? x) + (~r x #:precision precision) + (~a x))) + diff --git a/satore/rewrite-tree.rkt b/satore/rewrite-tree.rkt new file mode 100644 index 0000000..036ecad --- /dev/null +++ b/satore/rewrite-tree.rkt @@ -0,0 +1,668 @@ +#lang racket/base + +;***************************************************************************************; +;**** Binary Rewrite Tree ****; +;***************************************************************************************; + +(require bazaar/cond-else + bazaar/mutation + (except-in bazaar/order atom<=>) + define2 + define2/define-wrapper + global + racket/file + racket/list + racket/string + satore/Clause + satore/clause-format + satore/clause + satore/misc + satore/trie + satore/unification) + +(provide (all-defined-out) + (all-from-out satore/trie)) + +;===============; +;=== Globals ===; +;===============; + +(define-counter n-rule-added 0) +(define-counter n-binary-rewrites 0) + +(define-global:boolean *bounded-confluence?* #true + '("When performing confluence, should the size of the critical pairs " + "be bounded by the size of parent rules?")) + +(define-global *confluence-max-steps* 10 + "Maximum number of confluence steps" + number? + string->number) + +;====================; +;=== Rewrite tree ===; +;====================; + +;; atom<=> : comparator? +;; dynamic-ok? : whether we keep dynamic rules +;; rules-file : if not #false, loads rules from the given file +(struct rewrite-tree trie (atom<=> dynamic?)) + +(define (make-rewrite-tree #:? [constructor rewrite-tree] + #:! atom<=> + #:? [dynamic-ok? #true] + #:? [rules-file #false] + . other-args) + (define rwtree + (apply make-trie + #:constructor constructor + #:variable? Var? + atom<=> + dynamic-ok? + other-args)) + (when rules-file + (load-rules! rwtree #:rules-file rules-file #:rewrite? #true)) + rwtree) + +;; Returns a new rewrite-tree. +;; Duplicates the structure of rwtree, but the Clauses and rules are shared. +;; This means that the Clause ancestors of the rules are preserved. +(define (rewrite-tree-shallow-copy rwtree) + (define new-rwtree (make-rewrite-tree #:atom<=> (rewrite-tree-atom<=> rwtree) + #:dynamic-ok? (rewrite-tree-dynamic? rwtree))) + (for ([rl (in-list (rewrite-tree-rules rwtree))]) + (add-rule! new-rwtree rl)) + new-rwtree) + +(define (rewrite-tree-ref rwtree t) + ; Node values are lists of rules, and trie-ref returns a list of node-values, + ; hence the append*. + (append* (trie-ref rwtree t))) + +;; Clause : The Clause from which this rule originates +;; NOTICE: Clause may subsume the rule, and can be *more* general if the rule is asymmetric. +;; from-literal : heavy-side +;; to-literal : light side +;; to-fresh : variables of to-literal not in from-literal that need to be freshed +;; after applying the rule +(struct rule (Clause rule-group from-literal to-literal to-fresh static?) + #:prefab) + +;; A rule group holds all the rules that have been created by a single call to +;; Clause->rules. +;; A rule also has a reference to its rule group, so it makes it easy to find +;; the other rules of the same group from a given group. +;; A single group can have 2 or 4 rules: 2 for static rules or dynamic self-converse rules, +;; and 4 for dynamic non-self-converse rules. +(struct rule-group (Clause Converse [rules #:mutable]) #:prefab) + + +(define (make-rule C rule-gp from to static?) + (define-values (lit1 lit2) (apply values (fresh (list from to)))) + (rule C rule-gp lit1 lit2 (variables-minus lit2 lit1) static?)) + +(define (unit-rule? rl) + (memq (rule-to-literal rl) (list lfalse ltrue))) + +(define (rule-tautology? rl) + (equal? (rule-from-literal rl) (rule-to-literal rl))) + +(define (left-linear? rl) + (define occs (var-occs (rule-from-literal rl))) + (for/and ([(v n) (in-hash occs)]) + (<= n 1))) + +(define (rule-subsumes rl1 rl2) + (define subst (left-unify (rule-from-literal rl1) (rule-from-literal rl2))) + (and subst (left-unify (rule-to-literal rl1) (rule-to-literal rl2) subst))) + +;; A binary Clause [lit1 lit2] is treated as an *equivalence* (4 implications) +;; rather than two implications, +;; which means that a converse Clause or one that subsumes the latter MUST have been proven too +;; before adding the rules. +;; Thus: (Clause->rules C <=>) == (Clause->rules (make-converse-Clause C) <=>). +;; That is, if C = ~q | p, the converse C' = q | ~p MUST have been proven. +;; We MUST add the four rules at the same time, because the if we add just the (max 2) rules +;; corresponding to the implications of C only, and then add the rules for C', +;; then C' is going to be rewritten to a tautology before it has a chance to propose its rules +;; (since resolution(C, converse(C)) = tautology). +;; The number of returned rules is either 2 or 4. +;; Conv is either the converse Clause of C, or a Clause that subsumes it, and is used +;; as a parent reference (for proofs), even if converse(C) is more specific than Conv. +;; Conv is *not* used to generate the rules themselves (only C), so if Conv is more general than C +;; (as for asymmetric rules) the generated rules will *not* be more general than those of C. +(define (Clause->rules C Conv #:! atom<=> #:? [dynamic-ok? #true]) + (define cl (Clause-clause C)) + (define unit? (unit-Clause? C)) + (define lit1 (first cl)) + (define lit2 (if unit? lfalse (second cl))) + + (define rg (rule-group C Conv #false)) + ; Not the most efficient. The last 2 cases can be deduced from the first 2, + ; as long as atom<=> does not count polarity (which SHOULD be the case). + (define rules + (for/list ([parent + (in-list (cond [unit? + (list C #false C)] + [(eq? C Conv) ; self-converse, no need to duplicate the rules + (list C C)] + [else + (list C C Conv Conv)]))] + [from (in-list (list (lnot lit1) (lnot lit2) lit1 lit2))] + [to (in-list (list lit2 lit1 (lnot lit2) (lnot lit1)))] + ; if Conv is #false for example, skip it (see force-add-binary-Clause!) + ; also useful for unit? + #:when parent + [c (in-value (atom<=> from to))] + #:when (and (not (order? c)))) + ; rule cannot be oriented to → from, + ; so the rule from → to is valid. + ; It is 'static' if it can be oriented from → to, 'dynamic' otherwise. + (make-rule parent rg from to (order>? c)))) + (set-rule-group-rules! rg rules) + rules) + +;; a is left-unify< to b if a left-unifies with b. +(define left-unify<=> (make<=> left-unify) ; left-unify is <=? + ; equivalent to: + #;(if (left-unify c1 c2) + (if (left-unify c2 c1) + '= + '<) + (if (left-unify c2 c1) + '> + #false))) + +;;; What we want to assess is whether +;;; when applying rl1 to any clause c to get c1, +;;; c1 is always necessarily better than c2 when applying rl2 to c. + +;; Compares 2 rules. May help decide if one should be discarded. +;; rl1 <= rl2 if the heavyside of rl1 subsumes that of rl2, +;; and its light side is no heavier than that of rl2. +;; NOTICE: A return value of '= does not mean that rl1 and rl2 are equal or equivalent; +;; it only means that either can be used. It does mean that their heavy sides are equivalent though. +(define (rule<=> rl1 rl2 atom<=>) + (chain-comparisons + (left-unify<=> (rule-from-literal rl1) (rule-from-literal rl2)) + (atom<=> (rule-to-literal rl1) (rule-to-literal rl2)))) + +(define (find-rule<=> order? rwtree rl) + (define atom<=> (rewrite-tree-atom<=> rwtree)) + (for/or ([rl2 (in-list (rewrite-tree-ref rwtree (rule-from-literal rl)))]) + (and (order? (rule<=> rl2 rl atom<=>)) + rl2))) + +(define (find-subsuming-rule rwtree rl) + (for/or ([rl2 (in-list (rewrite-tree-ref rwtree (rule-from-literal rl)))]) + (and (rule-subsumes rl2 rl) rl2))) + +;; If there is a substitution α such that rule-from[α] = lit, then rule-to[α] is returned, +;; otherwise #false is returned. +;; If the rule introduces variables, these are freshed. +(define (rule-rewrite-literal rl lit) + (define subst (left-unify (rule-from-literal rl) lit)) + (cond [subst + ; NOTICE: We need to fresh the variables + ; that are introduced by the rule. + ; Ex: + ; clause: [(p a) (p b)] rule: (p X) -> (q Y) + ; Then this must be rewritten to: + ; [(q A) (q B)] and NOT [(q Y) (q Y)] + (for ([v (in-list (rule-to-fresh rl))]) + (subst-set!/name subst v (new-Var))) + (left-substitute (rule-to-literal rl) subst)] + [else #false])) + +;; Recursively rewrites the given literal lit from the rules in rwtree. +;; Returns the new literal and the sequence of rules used to rewrite it +;; (may contain duplicate rules). +;; lit: literal? +;; C: The Clause containing the literal lit. Used to avoid backward rewriting C to a tautology. +(define (binary-rewrite-literal rwtree lit C) + (define atom<=> (rewrite-tree-atom<=> rwtree)) + (let loop ([lit lit] [rules '()]) + (define candidate-rules (rewrite-tree-ref rwtree lit)) + ; Find the best rewrite of lit according to atom<=>. + ; Q: Can we rewrite more greedily, that is, applied each rewrite asap? + ; A: if the set of rules is confluent, yes, since they are all equivalent (although + ; choosing the one that leads to the smallest literal may still be faster) + ; But if the rules are not confluent then we may have a problem. + (for/fold ([best-lit lit] + [best-rule #false] + #:result (if best-rule + (loop best-lit (cons best-rule rules)) ; try once more + (values best-lit (reverse rules)))) ; no more rewrites + ([r (in-list candidate-rules)] + #:unless (let ([g (rule-rule-group r)]) + ; Don't rewrite yourself or your converse! + (or (eq? C (rule-group-Clause g)) + (eq? C (rule-group-Converse g))))) + (define new-lit (rule-rewrite-literal r lit)) + (if (and new-lit (order new-lit best-lit))) + (values new-lit r) + (values best-lit best-rule))))) + +;; Returns a rewritten clause and the set (without duplicates) of rules used for rewriting. +;; Rewriting a clause is a simple as rewriting each literal, because +;; only left-unification is used, so the substitution cannot apply to the rest of the clause. +;; NOTICE: The variables of the resulting clause are not freshed. +(define (binary-rewrite-clause rwtree cl C) + (let/ec return + (for/fold ([lits '()] + [rules '()] + #:result (values (sort-clause lits) + (remove-duplicates rules eq?))) + ([lit (in-list cl)]) + (define-values (new-lit new-rules) (binary-rewrite-literal rwtree lit C)) + (values (cond [(ltrue? new-lit) (return (list new-lit) new-rules)] ; tautology shortcut + [(lfalse? new-lit) lits] + [else (cons new-lit lits)]) + (append new-rules rules))))) + +(define Clause-type-rw 'rw) + +(define (Clause-type-rw? C) + (eq? (Clause-type C) Clause-type-rw)) + +;; Returns a new Clause if C can be rewritten, C otherwise. +;; The parents of the new Clause are C followed by the set of clauses from which the rules +;; used for rewriting C originate. +(define (binary-rewrite-Clause rwtree C) + (define-values (new-cl rules) (binary-rewrite-clause rwtree (Clause-clause C) C)) + (cond [(empty? rules) + C] + [else + (++n-binary-rewrites) + (make-Clause (clause-normalize new-cl) + (cons C (remove-duplicates (map rule-Clause rules) eq?)) + #:type Clause-type-rw)])) + +;; Returns whether the clause cl would be rewritten. Does not perform the rewriting. +(define (binary-rewrite-clause? rwtree cl C) + (for/or ([lit (in-list cl)]) + ; We need to perform the literal rewriting anyway, because + ; we need to check if the result is order (rewrite-tree-atom<=> rwtree)) + (unless (or (rule-tautology? rl) + (find-subsuming-rule rwtree rl)) + ;; Remove existing rules that are subsumed by rl. + (define from-lit (rule-from-literal rl)) + (trie-inverse-find rwtree from-lit + (λ (nd) + (define matches (trie-node-value nd)) + (when (list? matches) ; o.w. no-value + (define new-value + (for/list ([rl2 (in-list matches)] + #:unless (rule-subsumes rl rl2)) + rl2)) + ;; TODO: If new-value is '(), the node should be removed from the trie, + ;; along with any similar parent. + ;; (this could be made automatic?) + (set-trie-node-value! nd new-value)))) + + ;; NOTICE: No need to backward-rewrite the rules. + ;; Resolution (in the saturation loop) will take care of generating new rules + ;; and rewriting both their heavy sides and the light sides, + ;; while add-rule! takes care of subsumption on the heavy side. + ;; Letting the resolution loop take care of this is much safer, as it ensures + ;; that rwtree and utree are in sync, and that rwtree is not going to rewrite + ;; clauses before utree has a chance to generate new candidates via resolution. + ;; That is, if we only *remove* stuff from rwtree, and not do the job of resolution + ;; (apart from forward rewriting), then we should be fine? + (++n-rule-added) + (trie-insert! rwtree from-lit rl))) + +;; Unconditionally removes a single (oriented) rule from the tree. +;; Use with caution and see instead remove-rule-group!. +(define (remove-rule! rwtree rl) + (trie-find rwtree (rule-from-literal rl) + (λ (nd) + (define old-value (trie-node-value nd)) + (when (list? old-value) ; o.w. no-value + ;; TODO: If new-value is '(), the node should be removed from the trie, + ;; along with any similar parent. + ;; (this could be made automatic?) + (set-trie-node-value! nd (remove rl old-value eq?)))))) + +;; Removes a group of rules that were added at the same time via Clause->rules +;; (via add-binary-Clause!). +(define (remove-rule-group! rwtree gp) + (for ([rl (in-list (rule-group-rules gp))]) + (remove-rule! rwtree rl))) + +;; Turn the unit Clause into a binary Clause before adding it. +;; As for self-converses, we say that C is its own converse but that's a lie; +;; This is to avoid problems and specific cases when loading/saving rules. +;; A self-converse rule is necessarily dynamic (unless commutativity can be handled statically?),. +;; A unit rule is necessarily static (since $false is the bottom element). +;; Hence a 'self-converse' static rule is necessarily a unit rule (for now). +(define (rewrite-tree-add-unit-Clause! rwtree C #:? rewrite?) + (unless (unit-Clause? C) (error "Non-unit Clause v" C)) + (rewrite-tree-add-binary-Clause! rwtree C C #:rewrite? rewrite?)) + +;; Rewriting of the clause C must be done prior to calling this function. +;; Conv: Converse of C. See Clause->rules. +;; Returns the new rules (use these to obtain the rewritten Clauses). +(define (rewrite-tree-add-binary-Clause! rwtree C Conv #:? [rewrite? #true]) + (cond + [(Clause-binary-rewrite-rule? C) ; already added as a rule in the past? + (when-debug>= steps + (displayln "Clause has already been added before. Skipping.")) + '()] + [else + (let-values + ([(C Conv) + (cond/else + [(not rewrite?) (values C Conv)] + #:else ; Rewriting + (define C2 (binary-rewrite-Clause rwtree C)) + (when-debug>= steps + (displayln "Considering binary Clause for a rule (before rewriting):") + (display-Clause-ancestor-graph C #:depth 0) + (displayln "After rewriting:") + (display-Clause-ancestor-graph C2) + (when (Clause-tautology? C2) + (displayln "...but tautology."))) + #:cond + [(Clause-tautology? C2) + (values #false #false)] + #:else + ; Rewritten rule can still be used, rewrite the converse too. Not very efficient. + (define Conv2 (if (eq? C Conv) Conv (binary-rewrite-Clause rwtree Conv))) + (values C2 Conv2))]) + + (cond + [(not C) '()] + [(empty-clause? (Clause-clause C)) + ; Refutation found! + (when-debug>= steps + (displayln "Refutation found while adding rules!") + (display-Clause-ancestor-graph C)) + ; TODO: Let's just discard it for now. A refutation will probably be found very early + ; at the next saturation iteration. + '()] + [else + (define atom<=> (rewrite-tree-atom<=> rwtree)) + (define dynamic-ok? (rewrite-tree-dynamic? rwtree)) + (define rls (Clause->rules C Conv #:atom<=> atom<=> #:dynamic-ok? dynamic-ok?)) + (when-debug>= steps + (displayln "Adding the following rules:") + (display-rules rls)) + (for ([rl (in-list rls)]) + (add-rule! rwtree rl)) + ; We set the bit to #true, *even if* no rule has been added, + ; because the purpose of this bit is to avoid considering + ; C later again to save time. + ; TODO: We could set Conv as a rewrite-rule too but ONLY if C also subsumes the converse + ; of conv. + (set-Clause-binary-rewrite-rule?! C #true) + rls]))])) + +;; Adds the binary Clauses Cs as rules and returns the corresponding rules. +;; If rewrite? is not #false, the clauses are rewritten beforehand using the rules in the tree +;; (the order of the rules in Cs does matter as of now) +;; and tautologies are filtered out. +;; The default rewrite = #true is 'safe' because when considering A->B, Clause->rules also considers +;; B->A because we provide it with the converse equivalence (that is, the proof that B->A is valid). +;; Hence even converse implications can safely be rewritten to tautologies without losing rules. +;; Conv: MUST Subsumes the converse clause of each of Cs. +(define (rewrite-tree-add-binary-Clauses! rwtree Cs Conv #:? rewrite?) + (for/fold ([rules '()]) + ([C (in-list Cs)]) + (define rls (rewrite-tree-add-binary-Clause! rwtree C Conv #:rewrite? rewrite?)) + (append rls rules))) + +(define (rewrite-tree-rules rwtree) + (remove-duplicates (append* (trie-values rwtree)) eq?)) + +(define (rewrite-tree-rule-groups rwtree) + (remove-duplicates (map rule-rule-group (append* (trie-values rwtree))) eq?)) + +(define (rule-groups-original-Clauses groups) + (remove-duplicates (append (map rule-group-Clause groups) + (map rule-group-Converse groups)) + eq?)) + +(define (rules-original-Clauses rules) + (rule-groups-original-Clauses (map rule-rule-group rules))) + +(define (rewrite-tree-original-Clauses rwtree) + (rule-groups-original-Clauses (rewrite-tree-rule-groups rwtree))) + +(define (rule->clause r) + (list (lnot (rule-from-literal r)) (rule-to-literal r))) + +(define (rewrite-tree-count rwtree) + (length (rewrite-tree-rules rwtree))) ; not efficient + +(define (rewrite-tree-stats rwtree) + (define rules (rewrite-tree-rules rwtree)) + (define n-rules (length rules)) + (define n-dyn (count (λ (r) (not (rule-static? r))) rules)) + (define n-unit (count unit-rule? rules)) + (define n-bin (- n-rules n-unit)) + `((rules . ,n-rules) + (unit-rules . ,n-unit) + (binary-rules . ,n-bin) + (binary-rules-static . ,(- n-bin n-dyn)) + (binary-rules-dynamic . ,n-dyn))) + + +;; Attempts to simplify the rules by successively removing each rule, +;; rewrite its underlying Clause and add the rule again—checking for subsumption. +;; Since all rules are processed, the new set of rules can be obtained via rewrite-tree-rules. +;; WARNING: Not (currently) suitable for use *inside* the saturation loop because the new Clauses +;; (as per `eq?` are not part of the active set or candidates. +(define (re-add-rules! rwtree) + (define groups (rewrite-tree-rule-groups rwtree)) + (for ([gp (in-list groups)]) + (remove-rule-group! rwtree gp) + (define C (rule-group-Clause gp)) + (set-Clause-binary-rewrite-rule?! C #false) ; otherwise will not be added + (rewrite-tree-add-binary-Clause! rwtree C (rule-group-Converse gp) #:rewrite? #true))) + +;===================; +;=== Save / load ===; +;===================; + +;; Save the rules to file f (as clauses). +(define (save-rules! rwtree #:! rules-file #:? [exists 'replace]) + (define groups (rewrite-tree-rule-groups rwtree)) + ; We use hash to avoid duplicating clauses, so that we also avoid loading + ; the same clause under different names. + (define-counter idx 0) + (define h (make-hasheq)) + (define (get-clause C) + (if (hash-has-key? h C) + (hash-ref h C) + (begin0 (Clause-clause C) + (++idx) + (hash-set! h C idx)))) + + (make-parent-directory* rules-file) ; ensure the path exists + (with-output-to-file rules-file #:exists exists + (λ () (for ([gp (in-list groups)]) + (define C (rule-group-Clause gp)) + (define Conv (rule-group-Converse gp)) + (writeln (if (eq? C Conv) + (list (get-clause C)) ; self-converse + (list (get-clause C) + (get-clause Conv)))))))) + +;; Private. +(define (load-rule-Clause-lists #:! rules-file) + (define-counter idx 0) + ; Each clause has a number (local to the file) and if a number appears while reading + ; then we must load the saved clause of the same number. + (define h (make-hasheqv)) + (define (get-Clause! x) + (cond [(number? x) + (hash-ref h x)] + [else + (++idx) + (define C (make-Clause x #:type 'load)) + (hash-set! h idx C) + C])) + + (for/list ([cls (in-list (file->list rules-file))]) + (map get-Clause! cls))) + +;; Load the rules from file into the rewrite-tree. +;; Optionally: rewrites the rules before adding them; returns the set of new rules. +(define (load-rules! rwtree #:! rules-file #:? [rewrite? #true]) + (define Crules (load-rule-Clause-lists #:rules-file rules-file)) + (for/fold ([rules '()]) + ([Cs (in-list Crules)]) + (define C (first Cs)) + (define Conv + (if (= (length Cs) 1) + C ; self-converse + (second Cs))) + (define new-rules (rewrite-tree-add-binary-Clause! rwtree C Conv #:rewrite? rewrite?)) + (append new-rules rules))) + +;=======================; +;=== Filtering rules ===; +;=======================; + +;; Returns a new rwtree containing only the filtered rules +(define (filter-rule-groups rwtree proc) + (define rwtree2 (make-rewrite-tree #:atom<=> (rewrite-tree-atom<=> rwtree) + #:dynamic-ok? (rewrite-tree-dynamic? rwtree))) + (define groups (rewrite-tree-rule-groups rwtree)) + (for ([gp (in-list groups)]) + (when (proc gp) + ; Copy the clauses (shallow) + (define C (make-Clause (Clause-clause (rule-group-Clause gp)) #:type 'filter-rule-groups)) + (define Conv (make-Clause (Clause-clause (rule-group-Converse gp)) #:type 'filter-rule-groups)) + (rewrite-tree-add-binary-Clause! rwtree2 C Conv #:rewrite? #true))) + rwtree2) + +;==================; +;=== Confluence ===; +;==================; + +;; Unifies (resolves) only with the lhs of rules and returns +;; the new set of Clauses (and converse Clauses). +;; If bounded? is not #false, then Clauses which have a literal +;; that is heavier (in literal-size) than a `from' literal of its parent rules +;; are discarded. +(define (find-critical-pairs rwtree rl #:? [bounded? (*bounded-confluence?*)]) + (define lnot-from-lit1 (lnot (rule-from-literal rl))) + (define to-lit1 (rule-to-literal rl)) + (define new-Clauses '()) + ; Resolution (like unification with the converse) + ; to ensure that the Clause parents are correct + (trie-both-find rwtree lnot-from-lit1 + (λ (nd) + (define rls (trie-node-value nd)) + (when (list? rls) + (for ([rl2 (in-list rls)] + #:unless (eq? rl rl2)) + (define from-lit2 (rule-from-literal rl2)) + (define to-lit2 (rule-to-literal rl2)) + (define s (unify lnot-from-lit1 from-lit2)) + (when s + (define cl (clausify (substitute (list to-lit1 to-lit2) s))) + (define C (make-Clause cl (list (rule-Clause rl) (rule-Clause rl2)) + #:type 'c-p)) ; critical-pair + (define max-size (max (literal-size (rule-from-literal rl)) + (literal-size from-lit2))) + (unless (or (Clause-tautology? C) + (and bounded? + (> (max (literal-size (first cl)) + (literal-size (second cl))) + max-size))) + (cons! C new-Clauses))))))) + new-Clauses) + +;; This is a bad fix. Instead we should find the correct converse Clause (via rule groups) +;; Returns the list of rules that were added, or '() if none. +(define (force-add-binary-Clause! rwtree C) + (define Conv (make-converse-Clause C)) + (rewrite-tree-add-binary-Clause! rwtree C (if (Clause-equivalence? C Conv) C Conv))) + +;; Add all critical pairs between existing rules. +;; This procedure may need to be called several times, but such a loop may not terminate +;; as some rules can be inductive. +;; It is recommended to call `simplify-rewrite-tree!` before and after calling this procedure. +;; Returns #true if any rules has been added. +(define (rewrite-tree-confluence-step! rwtree #:? bounded?) + (define rules (rewrite-tree-rules rwtree)) + (for/fold ([any-change? #false]) + ([rl (in-list rules)]) + (define pairs (find-critical-pairs rwtree rl #:bounded? bounded?)) + (for/fold ([any-change? any-change?]) + ([C (in-list pairs)]) + (define change? (force-add-binary-Clause! rwtree C)) + (or any-change? (and change? #true))))) + +;; Performs several steps of confluence until no more change happens. +;; Returns whether any change has been made. +;; Warning: if bounded? is #false, this may loop forever. +;; If it does halt however, the system is confluent, but may not be minimal; +;; call re-add-rules! to remove unnecessary rules and simplify rhs of rules +;; (this should help make rewriting faster). +;; It is advised to call re-add-rules! once before and once after rewrite-tree-confluence!. +(define (rewrite-tree-confluence! rwtree #:? bounded? #:? [max-steps (*confluence-max-steps*)]) + (let loop ([step 1] [any-change? #false]) + (define changed? (rewrite-tree-confluence-step! rwtree #:bounded? bounded?)) + (cond [(or (>= step max-steps) + (not changed?)) + any-change?] + [else (loop (+ step 1) #true)]))) + +;================; +;=== Printing ===; +;================; + +(define (rule->list rl) + (cons (Clause-idx (rule-Clause rl)) + (Vars->symbols (list (rule-from-literal rl) + (rule-to-literal rl))))) + +(define display-rule<=> + (make-chain<=> boolean<=> rule-static? + boolean<=> unit-rule? + boolean<=> (λ (r) (lnot? (rule-from-literal r))) + number<=> (λ (r) (+ (tree-size (rule-from-literal r)) + (tree-size (rule-to-literal r)))) + number<=> (λ (r) (tree-size (rule-to-literal r))) + length<=> rule-to-fresh)) + +(define (sort-rules rls) + (sort rls (λ (a b) (order>? (display-rule<=> a b))))) + +;; Human-readable output +;; Notice: Since unit rules are asymmetric (only one rule per unit clause), +;; if positive-only is not #false it may not display some unit rules. +(define (rules->string rls #:? [sort? #true] #:? [positive-only? #false] #:? [unit? #true]) + (string-join + (for/list ([rl (in-list (if sort? (sort-rules rls) rls))] + #:unless (or (and (not unit?) (unit-rule? rl)) + (and positive-only? (lnot? (rule-from-literal rl))))) + ; abusing clause->string: + (clause->string (list (if (rule-static? rl) "static " "dynamic") + (map Var (rule-to-fresh rl)) + ': + (rule-from-literal rl) + '→ + (rule-to-literal rl)))) + "\n")) + +(define-wrapper (display-rules (rules->string rls #:? sort? #:? positive-only? #:? unit?)) + #:call-wrapped call + (displayln (call))) diff --git a/satore/saturation.rkt b/satore/saturation.rkt new file mode 100644 index 0000000..280e8d0 --- /dev/null +++ b/satore/saturation.rkt @@ -0,0 +1,895 @@ +#lang racket/base + +;**************************************************************************************; +;**** Saturation Algorithm ****; +;**************************************************************************************; + +(require bazaar/cond-else + bazaar/date + bazaar/debug + bazaar/dict + bazaar/mutation + data/heap/unsafe + data/queue + define2 + global + racket/block + racket/dict + racket/format + racket/list + racket/math + racket/pretty + racket/string + satore/Clause + satore/clause-format + satore/clause + satore/interact + satore/json-output + satore/misc + satore/rewrite-tree + satore/tptp + satore/unification-tree + satore/unification) + +(provide (all-defined-out)) + +;===============; +;=== Globals ===; +;===============; + +(define-global:boolean *quiet-json?* #false + '("JSON output format and silent mode. Deactivates some verbose options.")) + +(define-global *memory-limit* 4096 + "Memory limit in MB, including the Racket VM." + exact-positive-integer? + string->number) + +(define-global:boolean *find-unit-rules-in-candidates?* #false + '("Search for unit rewrite rules in the condidate set?" + "This may speed up the search significantly, or slow it down significantly," + "depending on how many unit rules can be generated.")) + +(define-global:boolean *backward-rw?* #true + '("Use binary-clause rewriting? (aka θ-equivalences)." + "The iterative mode does not use backward rewrites.")) + +(define-global:boolean *dynamic-rules?* #false + "Use dynamic rules? Experimental.") + +(define-global:boolean *proof?* #false + "Display the proof when found?") + +(define-global *age:cost* '(1 9) + "Age:cost ratio. Format: :, e.g., '1:3'" + (λ (p) (and (list? p) (= 2 (length p)) (andmap exact-nonnegative-integer? p))) + (λ (s) (map string->number (string-split s ":")))) + +(define-global:category *cost-type* 'weight-fair + '(weight-fair weight) + "Cost type.") + +(define-global *cost-noise* 0. + "Noise factor to add to costs" + (λ (x) (and (real? x) (>= x 0))) + string->number) + +(define-global:boolean *parent-discard?* #true + "Discard clauses when at least one parent has been discarded?") + +(define-global:boolean *discover-online?* #true + '("Use rewrite rules as soon as they are discovered?" + "The rules will not be made confluence until the next restart")) + +(define-global:boolean *negative-literal-selection?* #true + "When resolving, if a clause has negative literals, only select one of them.") + +(define-global *cpu-limit* +inf.0 + "CPU limit in seconds per problem." + exact-positive-integer? + string->number) + +(define-global *cpu-first-limit* +inf.0 + "CPU limit in seconds per problem." + exact-positive-integer? + string->number) + +(define-global *cpu-limit-factor* 3 + '("Increase of cpu limit of cpu-first-limit once an iteration has failed." + "Set to 0 to avoid restarting." + "Assumes --cpu-limit.") + (λ (x) (and (real? x) (>= x 0))) + string->number) + +(define-global *input-rules* #false + '("File to read rewrite rules from.") + file-exists? + values) + +(define-global *output-rules* #false + '("File to write rewrite rules to. If 'auto', a unique name is chosen automatically.") + (λ (x) #true) + (λ (str) + (if (string=? str "auto") + (build-path "rules" (string-append "rules-" (date-iso-file) ".txt")) + str))) + +;===============; +;=== Helpers ===; +;===============; + +(define (current-inexact-seconds) + (* 0.001 (current-inexact-milliseconds))) + +;==============; +;=== Clause ===; +;==============; + +(define (Candidate<= C1 C2) + (<= (Clause-cost C1) (Clause-cost C2))) + +;======================; +;=== Rule discovery ===; +;======================; + +;; Finds new binary equivalences between C and the clauses of utree, +;; and adds and returns the set of resulting new rules that can be added to rwtree. +(define (discover-new-rules! rwtree-out C utree) + (cond/else + [(not rwtree-out) '()] + + ;; FIND UNIT REWRITE RULES + ;; Unit rewrite using the binary rewrite tree + [(unit-Clause? C) + (when-debug>= steps (displayln "Found unit clause")) + ;; Add the new unit clause to the set of unit rewrite rules + (rewrite-tree-add-unit-Clause! rwtree-out C #:rewrite? #false)] + + [(not (binary-Clause? C)) + '()] + + ;; FIND BINARY REWRITE RULES + #:else + (when-debug>= steps (displayln "Found binary clause")) + + ;; We search for the converse implication in the active set. + ;; This takes care of clauses that have converse clauses but not the converse. + ;; Ex: C1 = p(X) | q(X) ; C2 = ~p(a) | ~q(a) + ;; C2 has a converse clause, but not C1. Hence C2 can be added as a binary rewrite rule + ;; but not C1. + (define Conv (make-converse-Clause C)) + (define self-conv? (Clause<=>-subsumes C Conv)) + #:cond + [self-conv? + ; Self-converse Clause, so only one Clause to add (but will lead to 2 rules). + (when-debug>= steps (displayln "Self-converse")) + (rewrite-tree-add-binary-Clause! rwtree-out C C #:rewrite? #false)] + #:else + (define Subs (utree-find/any utree Conv (λ (a Conv) (and (binary-Clause? a) + (Clause<=>-subsumes a Conv))))) + #:cond + [Subs + ; We found a converse Clause in the active set, or a Clause that subsumes the + ; converse Clause, so we can add selected-Clause as a rule and also its + ; converse Clause. + ; We can't add Subs, since Subs may not itself have a converse + ; clause in the active set. Ex: + ; selected-Clause = p(a) | q(a), so Conv = ~p(a) | ~q(a) and Subs = ~p(X) | ~q(X) + ; Subs cannot be added as a rule because (supposedly) we haven't found a converse + ; clause yet, but we can still add Conv as a rule. + ; If Subs is aleardy a rule, Conv will be rewritten to a tautology and discarded. + (when-debug>= steps (printf "Found converse subsuming clause: ~a\n" + (Clause->string Subs))) + ; Since C has already been rewritten, there is no need to do it again. + (rewrite-tree-add-binary-Clause! rwtree-out C Subs #:rewrite? #false)] + #:else + ; Asymmetric rules. + ; Even when selected-Clause is not a rule (yet?), it may still enable + ; other more specific Clauses of the active set to be added as rules too. + ; Eg, selected-Clause = p(X) | q(X) and some other active clause is ~p(a) | ~q(a). + (define Subsd (utree-find/all utree Conv (λ (a Conv) (and (binary-Clause? a) + (Clause<=>-subsumes Conv a))))) + #:cond + [(not (empty? Subsd)) + (when-debug>= steps + (displayln "Found converse subsumed clauses:") + (print-Clauses Subsd)) + ; rewrite=#true is ok here because Clause->rules already considers both directions + ; of the implication. Hence if a potential rule is rewritten to a tautology, + ; we know it's already redundant anyway. + ;; TODO: Rename this to add-asymmetric-rules ? + (rewrite-tree-add-binary-Clauses! rwtree-out Subsd C #:rewrite? #true)] + #:else '())) + +;=================; +;=== Cost/loss ===; +;=================; + +(define (Clauses-calculate-cost! Cs cost-type parent) + (case cost-type + ;; Very simple cost function that uses the weight of the Clause. May not be fair. + [(weight) + (for ([C (in-list Cs)]) + (set-Clause-cost! C + (if (empty? (Clause-clause C)) + -inf.0 ; empty clause should always be top of the list + (Clause-size C))))] + + ;; Very simple cost function that is fair + [(weight-fair) + (for ([C (in-list Cs)]) + (set-Clause-cost! C + (if (empty? (Clause-clause C)) + -inf.0 ; empty clause should always be top of the list + (+ (* (Clause-depth C) 1.5) + (Clause-size C)))))]) + + ;; Add noise to the cost so as to potentially solve more later. + ;; To combine with a slowly increasing step-limit-factor in iterative saturation + (unless (zero? (*cost-noise*)) + (define ε (*cost-noise*)) + (for ([C (in-list Cs)]) + (set-Clause-cost! C + (* (+ (- 1. ε) (* ε (random))) + (Clause-cost C)))))) + +;==================; +;=== Saturation ===; +;==================; + +(define statuses '(refuted saturated time memory steps running)) + +(define (check-status res status) + (define res-status (dict-ref res 'status #false)) + + ; To avoid silent typo bugs. + (assert (memq status statuses) status) + (assert (memq res-status statuses) res-status) + + (eq? status res-status)) + +(define (saturation input-clauses + #:? [step-limit +inf.0] + #:? [memory-limit (*memory-limit*)] ; in MB + #:? [cpu-limit +inf.0] ; in seconds + ; The rewrite tree holding the binary rules. + ; Set it to #false to deactivate it. + #:? [rwtree (make-rewrite-tree #:atom<=> (get-atom<=>) + #:dynamic-ok? (*dynamic-rules?*) + #:rules-file (*input-rules*))] + ; rewrite-tree where new rules found during saturation are stored. + ; If rwtree-out is different from rwtree, new rules are not used but only stored, + ; and backward rewriting is deactivated. + #:? [rwtree-out rwtree] ; or #false if don't care + ; Only effective if (eq? rwtree rwtree-out) + #:? [backward-rewrite? (*backward-rw?*)] + #:? [parent-discard? (*parent-discard?*)] + #:? [age:cost (*age:cost*)] ; chooses age if (< (modulo t (+ age cost)) age) + #:? [cost-type (*cost-type*)] + #:? [disp-proof? (*proof?*)] + #:? [L-resolvent-pruning? (*L-resolvent-pruning?*)] + #:? [find-unit-rules-in-candidates? (*find-unit-rules-in-candidates?*)] + #:? [negative-literal-selection? (*negative-literal-selection?*)]) + ;; Do NOT reset the clause-index, in particular if rwtree is kept over several calls to saturation. + #;(reset-clause-index!) + + ;; Tree containing the active Clauses + (define utree (make-unification-tree)) + ;; Clauses are pulled from priority first, unless empty. + ;; INVARIANT: active-Clauses U priority is (should be!) equisatisfiable with input-Clauses. + ;; In other words, if priority is empty, then the set of active-Clauses + ;; is equisatisfiable with the input-Clauses. + ;; Some active clauses may be removed from utree and pushed back into priority for further + ;; processing like 'backward' rewriting. In that case, the active Clauses (utree) is not + ;; 'complete'. + (define priority (make-queue)) + + ;; Both heaps contain the candidate clauses (there may be duplicates between the two, + ;; but this is checked when extracting Clauses from either heap). + (define candidates (make-heap Candidate<=)) + (define age-queue (make-heap Clause-age<=)) + ;; Frequency of extracting Clauses from either heap. + (define age-freq (first age:cost)) + (define cost-freq (second age:cost)) + (define age+cost-freq (+ age-freq cost-freq)) + + ;; Add the Clauses Cs to the priority queue for priority processing. + (define (add-priority-Clauses! Cs) + (for ([C (in-list Cs)]) + ; Need to set candidate? to #true otherwise it may be skipped. + ; (or maybe we should not skip clauses loaded from `priority`?) + (set-Clause-candidate?! C #true) + (enqueue! priority C))) + + (define (add-candidates! parent Cs) + ;; Calculate costs and add to candidate heap. + (unless (empty? Cs) + (Clauses-calculate-cost! Cs cost-type parent) + + (for ([C (in-list Cs)]) + (set-Clause-candidate?! C #true)) + + (unless (= 0 cost-freq) (heap-add-all! candidates Cs)) + (unless (= 0 age-freq) (heap-add-all! age-queue Cs)) + (when-debug>= steps + (printf "#new candidates: ~a #candidates: ~a\n" + (length Cs) + (heap-count candidates))))) + + (define input-Clauses + (map (λ (c) (make-Clause c '() #:type 'in)) input-clauses)) + + ;; This maintains the invariant: If priority is empty, then the set of active-Clauses + ;; is equisatisfiable with the input-Clauses. + ;; In other words active-Clauses U priority is (should be!) equisatisfiable with input-Clauses. + (add-priority-Clauses! input-Clauses) + + ;; We add the Clauses of the binary rules as candidates, so as to not cluter the active set + ;; in case there are many rules. + ;; Another option is to add them to the priority queue because they can be seen as possibly + ;; useful lemmas. + (when rwtree + ; A mock root clause parent of all input rules + (define C0rules (make-Clause (list ltrue) '() #:type 'rules-root)) + ; rewrite=#false should not be necessary (since rewriting checks if a clause is from the original + (add-candidates! C0rules (rewrite-tree-original-Clauses rwtree))) + + (define step 0) + (reset-n-tautologies!) + (define n-parent-pruning 0) + (define n-forward-subsumed 0) + (define n-backward-subsumed 0) + (reset-n-binary-rewrites!) + (reset-n-rule-added!) + (reset-subsumes-stats!) + (reset-n-L-resolvent-pruning!) + (define start-time (current-milliseconds)) + + ;; TODO: Some calls are slow... + (define (make-return-dict status [other '()]) + (assert (memq status statuses) status) + (define stop-time (current-milliseconds)) + `((status . ,status) + (steps . ,step) + (generated . ,clause-index) ; includes all input clauses and rules and intermediate steps + (actives . ,(length (unification-tree-Clauses utree))) + (candidates . ,(heap-count candidates)) + (priority-remaining . ,(queue-length priority)) + (tautologies . ,n-tautologies) ; counted in generated, (mostly) not in candidates + ,@(rewrite-tree-stats rwtree) + (binary-rewrites . ,n-binary-rewrites) + (forward-subsumed . ,n-forward-subsumed) + (backward-subsumed . ,n-backward-subsumed) + (subsumes-checks . ,n-subsumes-checks) + (subsumes-steps . ,n-subsumes-steps) + (subsumes-breaks . ,n-subsumes-breaks) + (parent-pruning . ,n-parent-pruning) + (L-resolvent-pruning . ,n-L-resolvent-pruning) + (memory . ,(current-memory-use)) ; doesn't account for GC---this would take too much time + (time . ,(- stop-time start-time)) + . ,other)) + + (define (make-refuted-dict C) + (define proof (Clause-ancestor-graph C)) ; no duplicates + (define flat-proof (flatten proof)) + (define type-occs (occurrences flat-proof #:key Clause-type)) + (when disp-proof? + (displayln "#| begin-proof") + (display-Clause-ancestor-graph C #:tab " ") + (displayln "end-proof |#")) + (make-return-dict 'refuted + `((proof-length . ,(length flat-proof)) ; doesn't account for compound rewrites + (proof-steps . ,(for/sum ([C2 (in-list flat-proof)]) + (define n (length (Clause-parents C2))) + (if (< n 2) n (- n 1)))) + (proof-inferences . ,(count (λ (C2) (not (empty? (Clause-parents C2)))) + flat-proof)) + ,@(for/list ([(t o) (in-dict type-occs)]) + (cons (string->symbol (format "proof-type:~a" t)) o))))) + + ;:::::::::::::::::::::; + ;:: Saturation Loop ::; + ;:::::::::::::::::::::; + + (define result + (let loop () + (++ step) + (define time-passed (- (current-milliseconds) start-time)) ; this is fast + (define mem (current-memory-use-MB)) ; mflatt says it's fast + + (when-debug>= steps + (printf "\nstep: ~a generated: ~a processed/s: ~a generated/s: ~a\n" + step + clause-index + (quotient (* 1000 step) (+ 1 time-passed)) + (quotient (* 1000 clause-index) (+ 1 time-passed)))) + (cond/else + [(and (= 0 (heap-count candidates)) + (= 0 (heap-count age-queue)) + (= 0 (queue-length priority))) + (when-debug>= steps (displayln "Saturated")) + (make-return-dict 'saturated)] + [(> step step-limit) (make-return-dict 'steps)] + [(> time-passed (* 1000 cpu-limit)) (make-return-dict 'time)] + [(and (> mem memory-limit) + (block + (define pre (current-milliseconds)) + ;; Memory is full, but try to collect garbage first. + (unless (*quiet-json?*) + (printf "; before GC: memory-limit: ~a memory-use: ~a\n" memory-limit mem)) + (collect-garbage) + (collect-garbage) + (define mem2 (current-memory-use-MB)) + (define post (current-milliseconds)) + (unless (*quiet-json?*) + (printf "; after GC: memory-limit: ~a memory-use: ~a gc-time: ~a\n" + memory-limit mem2 (* 0.001 (- post pre)))) + (> mem2 memory-limit))) + ; mem is full even after GC, so exit + (make-return-dict 'memory)] + #:else + ;; Choose a queue/heap to extract the selected-Clause from. + (define queue + (cond [(> (queue-length priority) 0) + ; Always has priority. + priority] + [(or (= 0 (heap-count candidates)) + (and (> (heap-count age-queue) 0) + (< (modulo step age+cost-freq) age-freq))) + ; Warning: This is somewhat defeated by the `priority` queue. + age-queue] + [else candidates])) + (when-debug>= steps + (printf "Selected queue: ~a\n" (cond [(eq? queue priority) "priority"] + [(eq? queue candidates) "candidates"] + [else "age queue"]))) + (define selected-Clause + (if (heap? queue) + (begin0 (heap-min queue) + (heap-remove-min! queue)) + (dequeue! queue))) + + #:cond + ;; ALREADY PROCESSED + [(not (Clause-candidate? selected-Clause)) + (when-debug>= steps (displayln "Clause already processed. Skipping.")) + (-- step) ; don't count this as a step + (loop)] + ;; ONE PARENT DISCARDED + [(and parent-discard? (ormap Clause-discarded? (Clause-parents selected-Clause))) + (when-debug>= steps (displayln "At least one parent has been discarded. Discard too.")) + (discard-Clause! selected-Clause) + (++ n-parent-pruning) + (loop)] + #:else + (set-Clause-candidate?! selected-Clause #false) + + ;; FORWARD REWRITE + ;; BINARY CLAUSE REWRITE OF SELECTED + ;; NOTICE: We do binary rewrites first because if we did unit then binary + ;; we would need to attempt a second unit-rewrite after that. + ;; (This may lead to unnecessary binary rewrites, but it's cleaner this way.) + (define selected-Clause-brw + (if rwtree + (binary-rewrite-Clause rwtree selected-Clause) + selected-Clause)) + + (when-debug>= steps + (printf "|\nstep ~a: selected: ~a\n" + step (Clause->string/alone selected-Clause 'all)) + (define binary-rewritten? (not (eq? selected-Clause-brw selected-Clause))) + (when binary-rewritten? + (displayln "Binary rewritten:") + (display-Clause-ancestor-graph selected-Clause-brw #:depth 1)) + (unless (eq? selected-Clause-brw selected-Clause-brw) + (displayln "Unit rewritten:") + (display-Clause-ancestor-graph selected-Clause-brw #:depth 1)) + (when-debug>= interact + (interact-saturation + (priority utree rwtree selected-Clause make-return-dict) + selected-Clause-brw selected-Clause-brw))) + + (set! selected-Clause selected-Clause-brw) + ;;; From now on, only selected-Clause should be used + + (define selected-clause (Clause-clause selected-Clause)) + #:cond + ;; REFUTED? + [(empty-clause? selected-clause) + (make-refuted-dict selected-Clause)] + ;; TAUTOLOGY? + [(clause-tautology? selected-clause) + (when-debug>= steps (displayln "Tautology.")) + (discard-Clause! selected-Clause) + (loop)] ; skip clause + ;; FORWARD SUBSUMPTION + [(utree-find/any utree selected-Clause Clause<=-subsumes) + ;; TODO: TESTS + => + (λ (C2) + (++ n-forward-subsumed) + (when-debug>= steps (printf "Subsumed by ~a\n" (Clause->string C2 'all))) + (discard-Clause! selected-Clause) + (loop))] ; skip clause + #:else + ;; Clause is being processed. + + ;; BACKWARD SUBSUMPTION + (define removed (utree-inverse-find/remove! utree selected-Clause Clause<=-subsumes)) + (for-each discard-Clause! removed) + (+= n-backward-subsumed (length removed)) + + (when-debug>= steps + (define n-removed (length removed)) + (when (> n-removed 0) + (printf "#backward subsumed: ~a\n" n-removed) + (when-debug>= interact + (print-Clauses removed 'all)))) + + ;; FIND NEW REWRITE RULES + (define clause-index-before-discover clause-index) + (define new-rules (discover-new-rules! rwtree-out selected-Clause utree)) + (define new-rule-Clauses (rules-original-Clauses new-rules)) + ;; NOTICE: We MUST add Clauses that are newly generated to the set of active rules + ;; (via priority) otherwise we may miss some resolutions. + ;; Only the Clauses that have been created during the discovery process need to be added. + ;; Notice: To prevent the clauses from which the rules have originated to be rewritten to + ;; tautologies, a test is performed in binary-rewrite-literal. + ;; But this applies *only* to the `eq?`-Clause of the rule, hence beware of copies or + ;; rewrites. + (add-priority-Clauses! + (filter (λ (C) (> (Clause-idx C) clause-index-before-discover)) + new-rule-Clauses)) + + ;; BACKWARD BINARY REWRITING + ;; We don't need to backward rewrite if the new rules are not stored in rwtree, + ;; as this means the set of used rules does not change during the whole saturation. + (when (and backward-rewrite? + rwtree + (eq? rwtree rwtree-out) ; not storing new rules in a different rwtree + (not (empty? new-rules))) + ; Remove active Clauses that can be rewritten, and push them into priority. + ; We must check whether the clauses we remove will be rewritten, + ; otherwise we might add all the same candidates again when the removed Clause + ; is popped from priority. + (define removed-active-Clauses + ;; TODO: This is inefficient. We should modify utree-inverse-find/remove! + ;; to handle multiple rule-C so as to take advantage of its hash/cache. + (remove-duplicates + (flatten + (for/list ([rule-C (in-list new-rule-Clauses)]) + (utree-inverse-find/remove! utree rule-C + (λ (_rule-C C2) + (binary-rewrite-Clause? rwtree C2))))) + eq?)) + (unless (empty? removed-active-Clauses) + (when-debug>= steps + (displayln "Some active Clauses can be backward binary rewritten:") + (print-Clauses removed-active-Clauses)) + (add-priority-Clauses! removed-active-Clauses))) + ;; Note that backward-rewritable Clauses are not yet discarded. They may be discarded + ;; when they are pulled from priority and deemed discardable. + + ;;; Even if the selected Clause is a unit/binary rewrite rule, we must continue processing it + ;;; and generate resolutions (because rewriting is only left-unification, not full unification) + + ;;; NEW CANDIDATES + + (define L-resolvent-pruning-allowed? + (and L-resolvent-pruning? + ; As per the invariant, if no Clause is in the priority queue, + ; then the set of active Clauses of utree is equisatisfiable with the input clauses. + (= 0 (queue-length priority)))) + + (define new-Candidates + (if negative-literal-selection? + (utree-resolve+unsafe-factors/select utree selected-Clause + #:rewriter (λ (C) (binary-rewrite-Clause rwtree C))) + (utree-resolve+unsafe-factors utree selected-Clause + #:rewriter (λ (C) (binary-rewrite-Clause rwtree C)) + #:L-resolvent-pruning? L-resolvent-pruning-allowed?))) + + ;; If a clause has no resolvent with the active set (when complete) + ;; then it will never resolve with anything and can thus be discarded. + #:cond + [(and L-resolvent-pruning-allowed? + (empty? new-Candidates)) + (discard-Clause! selected-Clause) + (when-debug>= steps + (printf "No resolvent (L-resolvent-pruning?=~a). Clause discarded. \n" + L-resolvent-pruning?)) + (loop)] + #:else + ;; ADD CLAUSE TO ACTIVES + ;; Rewrite the candidates with unit and binary rules, filter out tautologies, + ;; calculate their costs and add them to the queues. + (add-candidates! selected-Clause new-Candidates) + + ;; UNIT RULE DISCOVERY IN CANDIDATES + ;; Look for unit rewrite rules in the candidate set. + ;; (Looking for binary rules would be too costly here) + (when find-unit-rules-in-candidates? + (when rwtree-out + (for ([C (in-list new-Candidates)]) + (when (unit-Clause? C) + ;; WARNING: Should be calling/merged with discover-rules! to avoid inconsistencies + (rewrite-tree-add-unit-Clause! rwtree-out C #:rewrite? #false))))) + + (add-Clause! utree selected-Clause) + (when-debug>= steps + (displayln "Adding clause.") + (print-active-Clauses utree #false)) + + (loop)))) + + (when-debug>= interact + (displayln "Saturation loop finished.") + (pretty-print result) + (define selected-Clause #false) ; mock up + (interact-saturation + (priority utree rwtree selected-Clause make-return-dict))) + result) + +;========================; +;=== User interaction ===; +;========================; + +(define interact-commands '()) + +(define-namespace-anchor ns-anchor) +(define-syntax-rule (interact-saturation + (priority utree rwtree selected-Clause make-return-dict) + more ...) + (begin + (define what '(idx parents clause-pretty)) + (interact + #:command (and (not (empty? interact-commands)) + (begin0 (first interact-commands) + (rest! interact-commands))) + #:variables (priority utree rwtree what more ...) + #:namespace-anchor ns-anchor + #:readline? #true + [(list 'steps (? number? n)) + "skips n steps" + (when (> n 0) + (cons! "" interact-commands) + (cons! (format "steps ~a" (- n 1)) interact-commands))] + [(list (or 'ancestors 'ancestor-graph 'graph)) + "display the ancestor graph of the selected Clause." + (display-Clause-ancestor-graph selected-Clause)] + [(list (or 'ancestors 'ancestor-graph 'graph) (? number? depth)) + "display the ancestor graph of the selected Clause down to the given depth." + (display-Clause-ancestor-graph selected-Clause #:depth depth)] + [(list 'what-fields) + (string-append + "Prints which fields are available for 'what,\n" + "which is used for printing clause information.") + (displayln Clause->string-all-fields)] + [(list 'selected) + "Selected clause" + (print-Clauses (list selected-Clause) what)] + [(list 'active) + "Active clauses" + (print-active-Clauses utree #true what)] + [(list (or 'binary 'rules)) + "Found binary rules" + (print-binary-rules rwtree #true)] + [(list 'stats) + "Return-dictionary-like stats" + (pretty-print (make-return-dict 'running))] + [(list 'save-rules) + "Save the binary rules from the default rules-file" + (save-rules! rwtree)]))) + +(define (print-active-Clauses utree long? [what 'all]) + (define actives (unification-tree-Clauses utree)) + (printf "#active clauses: ~a\n" (length actives)) + (when long? + (displayln "Active clauses:") + (print-Clauses (sort actives < #:key Clause-idx) what))) + +(define (print-binary-rules rwtree long?) + (define rules (rewrite-tree-rules rwtree)) + (printf "#binary rules: ~a #original clauses: ~a\n" + (length rules) + (length (remove-duplicates (map rule-Clause rules) eq?))) + (when long? + (display-rules (rewrite-tree-rules rwtree)))) + +;============================; +;=== Iterative saturation ===; +;============================; + +(struct problem (file name clauses [time-used #:mutable] [last-time #:mutable])) + +(define (make-problem file name clauses) + (problem file name clauses 0 0)) + +;; Returns the same values as body ... but evaluates time-body ... before returning. +;; The result of time-body ... is discarded. +(define-syntax-rule (with-time-result [(cpu real gc) time-body ...] body ...) + (let-values ([(res cpu real gc) (time-apply (λ () body ...) '())]) + time-body ... + (apply values res))) + +;; Calls saturation for a set of problems in a loop. +;; Tries again each unsolved problem after multiplying the step-limit by step-limit-factor +;; and so on untill all problems are solved. +;; Loading time from files is *not* taken into account. +(define (iterative-saturation/problem-set problems + saturate + #:! memory-limit + #:! cpu-first-limit ; in seconds + #:! cpu-limit ; in second + #:! cpu-limit-factor) ; in seconds + (define n-problems (length problems)) + (define n-attempted 0) + (define n-solved 0) + (with-time-result [(cpu real gc) + (unless (*quiet-json?*) + (printf "; Total time: cpu: ~a real: ~a gc: ~a\n" cpu real gc))] + (let loop ([problems problems] [iter 0]) + (define n-unsolved (length problems)) + (define n-solved-iter 0) + (define n-attempted-iter 0) + (define new-unsolved + (for/fold ([unsolved '()] + [cumu-time 0] + #:result (reverse unsolved)) + ([prob (in-list problems)]) + (define input-clauses (problem-clauses prob)) + (when-debug>= init (for-each (compose displayln clause->string) input-clauses)) + + ;; Collecting garbage can take time even when there's nothing to collect, + ;; and can take a significant proportion of the time when solving is fast, + ;; hence it's better to trigger GC only if needed. + (when (>= (current-memory-use-MB) (* 0.8 memory-limit)) + (collect-garbage) + (collect-garbage)) + + ;; Main call + (define cpu-limit-problem (min (max cpu-first-limit + (* cpu-limit-factor (problem-last-time prob))) + (- cpu-limit (problem-time-used prob)))) + (define res (saturate input-clauses cpu-limit-problem)) + + (set! res (append `((name . ,(problem-name prob)) + (file . ,(problem-file prob))) + res)) + (++ n-attempted-iter) + (when (= 0 iter) (++ n-attempted)) + (define solved? (or (check-status res 'refuted) + (check-status res 'saturated))) + (when solved? + (++ n-solved-iter) + (++ n-solved)) + + (define last-time (* 0.001 (dict-ref res 'time))) + (set-problem-last-time! prob last-time) + (set-problem-time-used! prob (+ (problem-time-used prob) last-time)) + (set! res (dict-set res 'cumulative-time (exact-ceiling (* 1000 (problem-time-used prob))))) + + (define remove-problem? + (or solved? + (check-status res 'memory) ; more time won't help if status=memory + (>= (problem-time-used prob) cpu-limit))) ; cpu exhausted for this problem + + ; Don't pretty-print to keep it on a single line which is simpler for parsing. + ; Only print the last iteration of a problem for borg. + (cond + [(*quiet-json?*) + (when remove-problem? (displayln (saturation-result->json res)))] + [else + (pretty-write res) + (printf "; ~a/~a solved (iter: ~a/~a/~a success: ~a% avg-time: ~as ETA: ~as)\n" + n-solved n-attempted + n-solved-iter n-attempted-iter n-unsolved + (~r (* 100 (/ n-solved-iter n-attempted-iter)) #:precision '(= 1)) + (~r (/ cumu-time n-attempted-iter 1000.) #:precision '(= 3)) + (~r (* (/ cumu-time n-attempted-iter 1000.) + (- n-unsolved n-attempted-iter)) #:precision '(= 2)))]) + (flush-output) + + (values + (if remove-problem? + unsolved + (cons prob unsolved)) + (+ cumu-time last-time)))) + (unless (or (empty? new-unsolved) + (= cpu-limit-factor 0)) + (loop new-unsolved (+ iter 1)))))) + +;; Calls saturate on a single set of clauses, first with a time limit of cpu-first-limit, +;; then restarts and doubles it until the cumulative time reaches cpu-limit. +;; Loading time is taken into account. +;; During a call to saturate, the new rewrite rules are saved in a separate tree, +;; which means that no new rule is introduced until the next restart—and thus the first +;; call to saturate uses no rewrite rule. +;; +;; NOTICE: In this mode the unit rewrites are gathered only for the next round, but this is +;; likely not necessary! +(define (iterative-saturation saturate + #:! tptp-program ; string? + #:! rwtree-in + #:? [discover-online? (*discover-online?*)] + #:? [cpu-limit (*cpu-limit*)] + #:? [cpu-first-limit (*cpu-first-limit*)] + #:? [cpu-limit-factor (*cpu-limit-factor*)]) + (define cpu-start (current-inexact-seconds)) + ; Don't make new Clauses here, they need to be created at each `saturation` call. + (define clauses (tptp-prog->clauses tptp-program)) + (define quiet? (*quiet-json?*)) + + (let loop ([iter 1] [uncapped-current-cpu-limit cpu-first-limit] [rwtree-in rwtree-in]) + (define remaining-cpu (- cpu-limit (- (current-inexact-seconds) cpu-start))) + (define current-cpu-limit (min remaining-cpu uncapped-current-cpu-limit)) + (unless quiet? + (printf "; iter: ~a remaining-cpu: ~a current-cpu-limit: ~a\n" + iter + remaining-cpu + current-cpu-limit)) + + ; Simplify the set of rules (only once) + (begin ; unless (= 1 iter) ; don't do this if no restarting + ; Note that these steps destroy the Clause ancestry, and proofs will be incomplete. + (unless quiet? + (printf "; Rules stats: ~v\n" (rewrite-tree-stats rwtree-in)) + (displayln "; Simplifying the rules via re-add-rules!")) + + ;; Rewrite lhs and rhs of rules, remove subsumed and tautologies. + (re-add-rules! rwtree-in) + (unless quiet? + (printf "; Rules stats: ~v\n" (rewrite-tree-stats rwtree-in)) + (printf "; Confluence! bounded? = ~a\n" (*bounded-confluence?*))) + + ;; Unify rhs of rules to produce new rules. + (rewrite-tree-confluence! rwtree-in) + (unless quiet? + (printf "; Rules stats: ~v\n" (rewrite-tree-stats rwtree-in)) + (displayln "; Simplifying the rules via re-add-rules! (again)")) + + ;; Rewrite and simplify again. + (re-add-rules! rwtree-in) + (unless quiet? (printf "; Rules stats: ~v\n" (rewrite-tree-stats rwtree-in)))) + (flush-output) + + (define rwtree-out (if discover-online? rwtree-in (rewrite-tree-shallow-copy rwtree-in))) + + (define res (saturate #:clauses clauses + #:cpu-limit current-cpu-limit + #:rwtree-in rwtree-in + #:rwtree-out rwtree-out)) + + (define new-cumulative-cpu (- (current-inexact-seconds) cpu-start)) + (set! res (dict-set res 'cumulative-time (exact-ceiling (* 1000. new-cumulative-cpu)))) ; ms + (set! res (dict-set res 'saturation-iter iter)) + + (define solved? (or (check-status res 'refuted) + (check-status res 'saturated))) + + ;; We exit also if memory limit has been reached, but we could instead restart + ;; if new rules have been found. + (define finished? (or solved? + (check-status res 'memory) + (> new-cumulative-cpu cpu-limit))) + + (cond + [(*quiet-json?*) + (when finished? (displayln (saturation-result->json res)))] + [else + (pretty-write res)]) + (flush-output) + + (cond + [finished? + (when (*output-rules*) + (unless quiet? + (printf "Saving rules to ~a\n" + (if (string? (*output-rules*)) + (*output-rules*) + (path->string (*output-rules*))))) + (save-rules! rwtree-out #:rules-file (*output-rules*)))] + [else + (loop (+ iter 1) + (* uncapped-current-cpu-limit cpu-limit-factor) + rwtree-out)]))) diff --git a/satore/scribblings/satore.scrbl b/satore/scribblings/satore.scrbl new file mode 100644 index 0000000..7e26fcc --- /dev/null +++ b/satore/scribblings/satore.scrbl @@ -0,0 +1,5 @@ +#lang scribble/manual + +@title{First-order logic saturation with atomic rewriting} + +See the @hyperlink["https://link-to-readme"]{readme}. diff --git a/satore/tests/Clause.rkt b/satore/tests/Clause.rkt new file mode 100644 index 0000000..4989605 --- /dev/null +++ b/satore/tests/Clause.rkt @@ -0,0 +1,12 @@ +#lang racket/base + +(require rackunit + "../Clause.rkt" + (submod "../Clause.rkt" test)) + +;; Polarity should not count for the 'weight' cost function because otherwise it will be harder +;; to prove ~A | ~B than A | B. +(check-equal? (Clause-size (make-Clause '[p q])) + (Clause-size (make-Clause '[(not p) (not q)]))) + +;; TODO: test (check-Clause-set-equivalent? Cs1 Cs2) diff --git a/satore/tests/clause.rkt b/satore/tests/clause.rkt new file mode 100644 index 0000000..8cc8558 --- /dev/null +++ b/satore/tests/clause.rkt @@ -0,0 +1,197 @@ +#lang racket/base + +(require global + racket/dict + rackunit + racket/list + "../clause.rkt" + "../misc.rkt" + "../unification.rkt") + +(*subsumes-iter-limit* 0) + +(begin + (define-simple-check (check-tautology cl res) + (check-equal? (clause-tautology? (sort-clause (Varify cl))) res)) + + (check-tautology '[] #false) + (check-tautology `[,ltrue] #true) + (check-tautology `[,(lnot lfalse)] #true) + (check-tautology '[a] #false) + (check-tautology '[a a] #false) + (check-tautology '[a (not a)] #true) + (check-tautology '[a b (not c)] #false) + (check-tautology '[a b (not a)] #true) + (check-tautology '[a (not (a a)) (a b) (not (a (not a)))] #false) + (check-tautology '[a (a a) b c (not (a a))] #true) + (check-tautology `[(a b) b (not (b a)) (not (b b)) (not (a c)) (not (a ,(Var 'b)))] #false) + ) + +(begin + (define-simple-check (check-remove-duplicate-literals cl res) + (check-equal? (remove-duplicate-literals (sort-clause (Varify cl))) + (sort-clause (Varify res)))) + + (check-remove-duplicate-literals '(a (p X) (q X) (p X) (p Y) a (p a) a b) + '(a b (p a) (p X) (p Y) (q X)))) + + + +(begin + ;; NOTICE: symbol-tree->clause first performs some simplications (which themselves call + ;; clause-implies/1pass) + ;; Equivalences + (for ([(A B) (in-dict '(([] . [] ) ; if empty clause #true, everything is #true + ([p] . [p] ) + ([(p X)] . [(p X)] ) + ([(p X)] . [(p Y)] ) + ([(not (p X))] . [(not (p X))] ) + ([(p X) (q X)] . [(p X) (q X) (q Y)] ) + ))]) + (define cl1 (sort-clause (Varify A))) + (define cl2 (sort-clause (fresh (Varify B)))) + (check-not-false (clause-subsumes cl1 cl2) + (format "cl1: ~a\ncl2: ~a" cl1 cl2)) + (check-not-false (clause-subsumes cl2 cl1) + (format "cl1: ~a\ncl2: ~a" cl1 cl2)) + ) + + ;; One-way implication (not equivalence) + (for ([(A B) (in-dict '(([] . [p] ) ; if empty clause #true, everything is #true + ([p] . [p q] ) + ([(p X)] . [(p c)] ) + ([(p X) (p X) (p Y)] . [(p c)] ) + ([(p X)] . [(p X) (q X)] ) + ([(p X)] . [(p X) (q Y)] ) + ([(p X Y)] . [(p X X)] ) + ([(p X) (q Y)] . [(p X) (p Y) (q Y)] ) + ([(p X) (p Y) (q Y)] . [(p Y) (q Y) c] ) + ([(p X Y) (p Y X)] . [(p X X)] ) + ([(q X X) (q X Y) (q Y Z)] . [(q a a) (q b b)]) + ([(f (q X)) (p X)] . [(p c) (f (q c))]) + ; A θ-subsumes B, but does not θ-subsume it 'strictly' + ([(p X Y) (p Y X)] . [(p X X) (r)]) + ))]) + (define cl1 (sort-clause (Varify A))) + (define cl2 (sort-clause (fresh (Varify B)))) + (check-not-false (clause-subsumes cl1 cl2)) + (check-false (clause-subsumes cl2 cl1))) + + ; Not implications, both ways. Actually, this is independence + (for ([(A B) (in-dict '(([p] . [q]) + ([(p X)] . [(q X)]) + ([p] . [(not p)]) + ([(p X c)] . [(p d Y)]) + ([(p X) (q X)] . [(p c)]) + ([(p X) (f (q X))] . [(p c)]) + ([(eq X X)] . [(eq (mul X0 X1) (mul X2 X3)) + (not (eq X0 X2)) (not (eq X1 X3))]) + ; A implies B, but there is no θ-subsumption + ; https://www.doc.ic.ac.uk/~kb/MACTHINGS/SLIDES/2013Notes/6LSub4up13.pdf + ([(p (f X)) (not (p X))] . [(p (f (f Y))) (not (p Y))]) + ))]) + (define cl1 (sort-clause (Varify A))) + (define cl2 (sort-clause (fresh (Varify B)))) + (check-false (clause-subsumes cl1 cl2) + (list (list 'A= A) (list 'B= B))) + (check-false (clause-subsumes cl2 cl1) + (list A B))) + + (let* () + (define-Vars X Y Z) + (define cl + `((not (incident ,X ,Y)) + (not (incident ab ,Y)) + (not (incident ab ,Z)) + (not (incident ab ,Z)) + (not (incident ac ,Y)) + (not (incident ac ,Z)) + (not (incident ac ,Z)) + (not (incident bc a1b1)) + (not (line_equal ,Z ,Z)) + (not (point_equal bc ,X)))) + (define cl2 + (sort-clause (fresh (left-substitute cl (hasheq (Var-name X) 'bc + (Var-name Y) 'a1b1))))) + (check-not-false (clause-subsumes cl cl2))) + ) + +#; +(begin + ; This case SHOULD pass, according to the standard definition of clause subsumption based on + ; multisets, but our current definition of subsumption is more general (not necessarily in a + ; good way.) + ; Our definition is based on sets, with a constraint on the number of literals (in + ; Clause<=-subsumes). + ; This makes it more general, but also not well-founded (though I'm not sure yet whether this is + ; really bad). + (check-false (clause-subsumes (clausify '[(p A A) (q X Y) (q Y Z)]) + (clausify '[(p a a) (p b b) (q C C)]))) + ) + + +(begin + + (*debug-level* (debug-level->number 'steps)) + + (define-simple-check (check-safe-factoring cl res) + (define got (safe-factoring (sort-clause (Varify cl)))) + (set! res (sort-clause (Varify res))) + ; Check equivalence + (check-not-false (clause-subsumes res got)) + (check-not-false (clause-subsumes got res))) + + (check-safe-factoring '[(p a b) (p A B)] + '[(p a b)]) ; Note that [(p a b) (p A B)] ≠> (p A B) + (check-safe-factoring '[(p X) (p Y)] + '[(p Y)]) + (check-safe-factoring '[(p Y) (p Y)] + '[(p Y)]) + (check-safe-factoring '[(p X) (q X) (p Y) (q Y)] + '[(p Y) (q Y)]) + (check-safe-factoring '[(p X Y) (p A X)] + '[(p X Y) (p A X)]) + (check-safe-factoring '[(p X Y) (p X X)] + '[(p X X)]) ; is a subset of above, so necessarily no less general + (check-safe-factoring '[(p X Y) (p A X) (p Y A)] + '[(p X Y) (p A X) (p Y A)]) ; cannot be safely factored? + (check-safe-factoring '[(p X) (p Y) (q X Y)] + '[(p X) (p Y) (q X Y)]) ; Cannot be safely factored (proven) + (check-safe-factoring '[(leq B A) (leq A B) (not (def B)) (not (def A))] + '[(leq B A) (leq A B) (not (def B)) (not (def A))]) ; no safe factor + (check-safe-factoring '[(p X) (p (f X))] + '[(p X) (p (f X))]) + + (check-safe-factoring + (fresh '((not (incident #s(Var 5343) #s(Var 5344))) + (not (incident ab #s(Var 5344))) + (not (incident ab #s(Var 5345))) + (not (incident ab #s(Var 5345))) + (not (incident ac #s(Var 5344))) + (not (incident ac #s(Var 5345))) + (not (incident ac #s(Var 5345))) + (not (incident bc a1b1)) + (not (line_equal #s(Var 5345) #s(Var 5345))) + (not (point_equal bc #s(Var 5343))))) + (fresh + '((not (incident #s(Var 148) #s(Var 149))) + (not (incident ab #s(Var 149))) + (not (incident ab #s(Var 150))) + (not (incident ac #s(Var 149))) + (not (incident ac #s(Var 150))) + (not (incident bc a1b1)) + (not (line_equal #s(Var 150) #s(Var 150))) + (not (point_equal bc #s(Var 148)))))) + + (check-not-exn (λ () (safe-factoring + (fresh '((not (incident #s(Var 5343) #s(Var 5344))) + (not (incident ab #s(Var 5344))) + (not (incident ab #s(Var 5345))) + (not (incident ab #s(Var 5345))) + (not (incident ac #s(Var 5344))) + (not (incident ac #s(Var 5345))) + (not (incident ac #s(Var 5345))) + (not (incident bc a1b1)) + (not (line_equal #s(Var 5345) #s(Var 5345))) + (not (point_equal bc #s(Var 5343)))))))) + ) diff --git a/satore/tests/confluence.rkt b/satore/tests/confluence.rkt new file mode 100644 index 0000000..501a24c --- /dev/null +++ b/satore/tests/confluence.rkt @@ -0,0 +1,118 @@ +#lang racket/base + +(require (for-syntax racket/base + syntax/parse) + bazaar/debug + define2 + define2/define-wrapper + global + racket/list + racket/pretty + rackunit + "../Clause.rkt" + "../clause.rkt" + "../clause-format.rkt" + "../rewrite-tree.rkt" + "../unification.rkt" + (submod "../Clause.rkt" test)) + +(define-global:boolean *dynamic-ok?* #true + "Use dynamic rules?") + +(define (take-at-most l n) + (take l (min (length l) n))) + +(define (display-rwtree rwtree #:? [n-max 100]) + (define rules (rewrite-tree-rules rwtree)) + (define-values (statics dyns) + (partition rule-static? + (filter-not (λ (rl) (lnot? (rule-from-literal rl))) + rules))) + (display-rules (take-at-most (reverse (sort-rules statics)) n-max)) + (display-rules (take-at-most (reverse (sort-rules dyns)) n-max)) + (when (or (> (length statics) n-max) (> (length dyns) n-max)) + (displayln "(output truncated because there are too many rules)")) + (pretty-write (rewrite-tree-stats rwtree))) + +;; Adds an equivalence as rules. +;; For testing purposes. +(define (add-equiv! rwtree equiv) + (define C (make-Clause (clausify (list (lnot (first equiv)) (second equiv))))) + (force-add-binary-Clause! rwtree C)) + +(define (rewrite-literal rwt lit) + (define-values (new-lit rls) (binary-rewrite-literal rwt lit #false)) + new-lit) + +;; Given a set of implications, generate equivalence +(define (equivs->rwtree equivs + #:? [dynamic-ok? (*dynamic-ok?*)] + #:? [atom<=> (get-atom<=>)]) + (define rwt (make-rewrite-tree #:atom<=> atom<=> #:dynamic-ok? dynamic-ok?)) + (for ([equiv (in-list equivs)]) + (add-equiv! rwt equiv) + (add-equiv! rwt (map lnot equiv))) + rwt) + +(define-syntax (test-confluence stx) + (syntax-parse stx + [(_ equivs expected-stats #:with rwt body ...) + #'(let () + (define rwt (equivs->rwtree equivs)) + (rewrite-tree-confluence! rwt) + (define stats (rewrite-tree-stats rwt)) + (unless (equal? stats expected-stats) + (display-rwtree rwt)) + (check-equal? stats expected-stats) + body ...)] + [(_ equivs expected-stats) + #'(test-confluence equivs expected-stats #:with _rwt)])) + + +(with-globals ([*bounded-confluence?* #true] + [*dynamic-ok?* #false]) + ;; This induction does work and is not subsumed. + ;; This is possibly the minimal induction scheme (that doesn't lead to subsumed rules). + (test-confluence + '([(p A (f B)) (p A B)] + [(p C C) d]) ; not left linear + ; Should not produce longer rules than the parents! + '((rules . 6) + (unit-rules . 0) + (binary-rules . 6) + (binary-rules-static . 6) + (binary-rules-dynamic . 0))) + + (test-confluence + '([(p (f (f (f z))) (f (f (f z)))) (g (g (g b)))] ; should -> b + [(p (f (f (f z))) (f (f (f X)))) b] + [(p (f (f z)) (f (f X))) c] + [(p (f z) (f X)) d] + [(p X X) (q X)]) + '((rules . 18) ; 16 also ok + (unit-rules . 0) + (binary-rules . 18) + (binary-rules-static . 18) + (binary-rules-dynamic . 0)) + #:with rwt + (check-equal? (rewrite-literal rwt '(p z z)) '(q z)) + (check-equal? (rewrite-literal rwt '(p (f (f (f z))) (f (f (f a))))) 'b) + (check-equal? (rewrite-literal rwt '(p (f (f (f z))) (f (f (f z))))) 'b)) + + (test-confluence + '([(p a X) q] + [(p X a) f] + [(p a a) (g b)]) + '((rules . 8) + (unit-rules . 0) + (binary-rules . 8) + (binary-rules-static . 8) + (binary-rules-dynamic . 0)) + #:with rwt + (check-equal? (rewrite-literal rwt '(p a a)) 'f) + (check-equal? (rewrite-literal rwt '(p a b)) 'f) + (check-equal? (rewrite-literal rwt '(g b)) 'f) + (check-equal? (rewrite-literal rwt 'q) 'f)) + ) + + diff --git a/satore/tests/interact.rkt b/satore/tests/interact.rkt new file mode 100644 index 0000000..d51091d --- /dev/null +++ b/satore/tests/interact.rkt @@ -0,0 +1,34 @@ +#lang racket/base + +(require racket/list + racket/port + rackunit + "../interact.rkt") + +(define-syntax-rule (check-interact in out args ...) + (check-equal? + (with-output-to-string + (λ () + (with-input-from-string (string-append in "\n\n") ; ensure no read loop + (λ () (interact args ...))))) + out)) + +(define-namespace-anchor ns-anchor) ; optional, to use the eval command + +(let ([x 2] [y 'a]) + (check-interact + "x\ny\nx 3\nx" + "2\n'a\n3\n" + #:prompt "" + #:variables (x y))) + +(let ([x 3] [y 'a]) + (check-interact + "yo\nyo 4\nx\nx 2\nx" + "yo\n(yo yo yo yo)\n3\n2\n" + #:prompt "" + #:namespace-anchor ns-anchor + #:variables (x y) + ;; All patterns must be of the form (list ....) + [(list 'yo) "prints yo" (displayln "yo")] + [(list 'yo (? number? n)) "prints multiple yos" (displayln (make-list n 'yo))])) diff --git a/satore/tests/misc.rkt b/satore/tests/misc.rkt new file mode 100644 index 0000000..7b86736 --- /dev/null +++ b/satore/tests/misc.rkt @@ -0,0 +1,5 @@ +#lang racket/base + +(require "../misc.rkt" + rackunit) + diff --git a/satore/tests/rewrite-tree.rkt b/satore/tests/rewrite-tree.rkt new file mode 100644 index 0000000..dd22490 --- /dev/null +++ b/satore/tests/rewrite-tree.rkt @@ -0,0 +1,250 @@ +#lang racket/base + +(require bazaar/debug + (except-in bazaar/order atom<=>) + racket/list + racket/file + racket/pretty + racket/random + rackunit + "../Clause.rkt" + "../clause.rkt" + "../misc.rkt" + "../rewrite-tree.rkt" + "../unification.rkt" ; for atom1<=> + (submod "../Clause.rkt" test)) + +(*debug-level* 0) + +(define-check (check-rewrite rwtree c crw) + (define C (Clausify c)) + (define Crw (binary-rewrite-Clause rwtree C)) + (define crw-sorted (sort-clause crw)) + (unless (equal? (Clause-clause Crw) crw-sorted) + (eprintf "c-sorted : ~a\ncrw-sorted: ~a\n" (Clause-clause C) crw-sorted) + (eprintf (Clause-ancestor-graph-string Crw)) + (fail-check))) + +(define-simple-check (check-not-rewrite rwtree c) + (check-rewrite rwtree c c)) + +;;; Self-equivalence +(let () + (define rwtree (make-rewrite-tree #:atom<=> atom1<=>)) + + (define C1 (make-Clause (clausify '[(not (eq A B)) (eq B A)]))) + (define rls1 (Clause->rules C1 C1 #:atom<=> atom1<=>)) + (rewrite-tree-add-binary-Clause! rwtree C1 C1) + (check-equal? (rewrite-tree-count rwtree) 2) + ; Rewrite clause in lexicographical order + (check-rewrite rwtree '[(eq b a)] '[(eq a b)])) + +;;; Adding two converse implications +(let () + (define rwtree (make-rewrite-tree #:atom<=> atom1<=>)) + + (define C1 (make-Clause (clausify '[(not (p A A)) (q A)]))) + (define C2 (make-Clause (clausify '[(not (q A)) (p A A)]))) + (define rls1 (Clause->rules C1 C2 #:atom<=> atom1<=>)) + (rewrite-tree-add-binary-Clause! rwtree C1 C2) + ; This is not needed because both polarities are considered by Clause->rules: + (rewrite-tree-add-binary-Clauses! rwtree (list C2) C1 #:rewrite? #true) + (check-equal? (rewrite-tree-count rwtree) 2) + (check-rewrite rwtree '[(p a a) (z c)] '[(q a) (z c)]) + (check-rewrite rwtree '[(not (p a a)) (z c)] '[(not (q a)) (z c)])) + +;;; Adding rules where the converse implication is more general +(let () + (define rwtree (make-rewrite-tree #:atom<=> atom1<=>)) + + (define Crules + (map (compose make-Clause clausify) + '([(not (p A A)) (q A)] + [(not (q a)) (p a a)] + [(not (q b)) (p b b)]))) + (for ([C (in-list (rest Crules))]) + (rewrite-tree-add-binary-Clause! rwtree C (first Crules))) + (check-equal? (rewrite-tree-count rwtree) 4) + (check-rewrite rwtree '[(p a a) (z c)] '[(q a) (z c)]) + (check-rewrite rwtree '[(not (p a a)) (z c)] '[(not (q a)) (z c)]) + (check-rewrite rwtree '[(p b b) (z c)] '[(q b) (z c)]) + (check-rewrite rwtree '[(not (p b b)) (z c)] '[(not (q b)) (z c)]) + (check-not-rewrite rwtree '[(p x x) (z c)])) +;;; The same with add-binary-Clauses +(let () + (define rwtree (make-rewrite-tree #:atom<=> atom1<=>)) + + (define Crules + (map (compose make-Clause clausify) + '([(not (p A A)) (q A)] + [(not (q a)) (p a a)] + [(not (q b)) (p b b)]))) + (rewrite-tree-add-binary-Clauses! rwtree (rest Crules) (first Crules)) + (check-equal? (rewrite-tree-count rwtree) 4) + (check-rewrite rwtree '[(p a a) (z c)] '[(q a) (z c)]) + (check-rewrite rwtree '[(not (p a a)) (z c)] '[(not (q a)) (z c)]) + (check-not-rewrite rwtree '[(p x x) (z c)])) + +;;; Dynamic, non-self-converse Clauses, leading to 4 rules +(let () + (define rwtree (make-rewrite-tree #:atom<=> atom1<=>)) + + (define C1 (make-Clause (clausify '[(not (p A B C)) (p C A B)]))) + (define C2 (make-converse-Clause C1)) + (define rls1 (Clause->rules C1 C2 #:atom<=> atom1<=>)) + (rewrite-tree-add-binary-Clause! rwtree C1 C2) + (check-equal? (rewrite-tree-count rwtree) 4) + (check-rewrite rwtree '[(p a b c)] '[(p a b c)]) + (check-rewrite rwtree '[(p c a b)] '[(p a b c)]) + (check-rewrite rwtree '[(p b c a)] '[(p a b c)]) + (check-rewrite rwtree '[(p b a c)] '[(p a c b)])) + +;;; Some random testing to make sure atom<=> has the Groundedness property. + +(define (random-atom) + (define syms '(aaa a p q r z zzz)) + (define choices (append syms syms '(NV OV L L))) ; reduce proba of NV and OV + (define vars '()) + (let loop () + (define r (random-ref choices)) + (case r + [(NV) ; new var + (define v (new-Var)) + (set! vars (cons v vars)) + v] + [(OV) (if (empty? vars) (loop) (random-ref vars))] ; old vars + [(L) (cons (random-ref syms) ; first element must be a symbol + (build-list (random 4) (λ (i) (loop))))] + [else r]))) + +(define random-atom-bank + (remove-duplicates (build-list 1000 (λ _ (random-atom))))) +(debug-vars (length random-atom-bank)) + +(define (check-groundedness atom<=> lita litb) + (define from<=>to (atom<=> lita litb)) + ; no point in testing groundedness if we don't have from literal< to + (assert (orderto) lita litb from<=>to) + (define vs (vars (list lita litb))) + (define s (make-subst)) + (for ([v (in-list vs)]) + (subst-set!/name s v (random-ref random-atom-bank))) + (define lita2 (substitute lita s)) + (define litb2 (substitute litb s)) + (check-equal? (atom<=> lita2 litb2) '<)) + +(for ([i 10000]) + (apply check-groundedness atom1<=> (Varify '[(eq A B) (eq A (mul B a))])) + (apply check-groundedness atom1<=> (Varify '[(eq A B a) (eq A (mul B a))]))) + +; IMPORTANT CASE: Check circularity of the rules +; Imagine we have two clauses: +; c1 = p | q +; c2 = ~p | ~q +; They are converse implications. +; From c1 we can generate the rules: +; r1 = ~p → q +; r2 = ~q → p +; and from c2 we can generate: +; r3 = p → ~q +; r4 = q → ~p +; If we choose {r1, r4} or {r2, r3} we run in circles! +; Hence the valid choices are {r2, r4} and {r1, r2} +; {r2, r4} is justified by removing negations and considering 'p < 'q. +; {r1, r2} is justified by considering that the negated atoms 'weigh' more. +; +; Now if the two clauses are: +; c3 = ~p | q with rules p → q and ~q → ~p +; c4 = p | ~q with rules ~p → ~q and q → p +; Now we should choose q → p and ~q → ~p to avoid running in circles. +(for* ([lits (in-list '( (p q) ; + ((not p) (not q)) + (p (not q)) + ((distinct_points A B) (equal_points A B)) + ((distinct_points A B) (not (equal_points A B))) + ))] + [r1 (in-list + (Clause->rules (Clausify lits) #false #:atom<=> atom1<=>))] + [r2 (in-list + (Clause->rules (Clausify (map lnot lits)) #false #:atom<=> atom1<=>))]) + ; The rules should NOT be circular! + (check-not-equal? + (Vars->symbols (list (rule-from-literal r1) (rule-to-literal r1))) + (Vars->symbols (list (rule-to-literal r2) (rule-from-literal r2))))) + +;; Saving and loading rules, especially with asymmetric rules. +(let () + (define rwtree (make-rewrite-tree #:atom<=> atom1<=>)) + (define rwtree2 (make-rewrite-tree #:atom<=> atom1<=>)) + + ;; Asymmetric rules + (let ([Conv (Clausify '[(not (p A A)) (q A)])]) + (rewrite-tree-add-binary-Clauses! rwtree + (map Clausify + '([(not (q a)) (p a a)] + [(not (q b)) (p b b)] + [(not (q c)) (p c c)])) + Conv)) + ; Self-converse + (let ([C (Clausify '[(not (eq A B)) (eq B A)])]) + (rewrite-tree-add-binary-Clause! rwtree C C)) + ; Symmetric + (rewrite-tree-add-binary-Clause! rwtree + (Clausify '[(not (pp A A)) (qq A)]) + (Clausify '[(pp A A) (not (qq A))])) + + (define Crules (rewrite-tree-original-Clauses rwtree)) + (define f (make-temporary-file)) + (save-rules! rwtree #:rules-file f) + (load-rules! rwtree2 #:rules-file f) + (define Crules2 (rewrite-tree-original-Clauses rwtree2)) + (check-equal? (length Crules2) (length Crules)) + ;; not efficient + (for ([C (in-list Crules)]) + (define cl (Clause-clause C)) + (check-not-false (for/or ([C2 (in-list Crules2)]) + (Clause-equivalence? C C2)) + cl))) + +;; Tautology reduction +(let () + (define rwtree (make-rewrite-tree #:atom<=> atom1<=>)) + (rewrite-tree-add-binary-Clause! rwtree + (make-Clause (clausify '[(not (p (p X))) (p X)])) + (make-Clause (clausify '[(p (p X)) (not (p X))]))) + (check-equal? (rewrite-tree-stats rwtree) + '((rules . 2) + (unit-rules . 0) + (binary-rules . 2) + (binary-rules-static . 2) + (binary-rules-dynamic . 0))) + ; These should be reduced to tautologies and thus not added + (rewrite-tree-add-binary-Clause! rwtree + (make-Clause (clausify '[(not (p (p (p X)))) (p X)])) + (make-Clause (clausify '[(p (p (p X))) (not (p X))]))) + (check-equal? (rewrite-tree-stats rwtree) + '((rules . 2) + (unit-rules . 0) + (binary-rules . 2) + (binary-rules-static . 2) + (binary-rules-dynamic . 0)))) + +;; Tautology reduction by dynamic rule +;; Currently fails +#; +(let () + (define rwtree (make-rewrite-tree #:atom<=> atom1<=>)) + (define Cp (Clausify '[(not (p A B)) (p B A)])) + (rewrite-tree-add-binary-Clause! rwtree Cp Cp) + ; What should we do? + ; The dynamic rule *can* reduce this to a tautology, but doesn't because + ; it can't be ground-oriented. + (check Clause-equivalence? + (binary-rewrite-Clause rwtree (Clausify '[(p A B) (p B A) q])) + (Clausify '[(p A B) q])) + ; Same, but after a rewrite + (rewrite-tree-add-binary-Clause! rwtree + (Clausify '[(not (p (f A) B)) (p A B)]) + (Clausify '[(p (f A) B) (not (p A B))])) + (check Clause-equivalence? + (binary-rewrite-Clause rwtree (Clausify '[(p (f A) B) (p B A) q])) + (Clausify '[(p A B) q]))) diff --git a/satore/tests/saturation.rkt b/satore/tests/saturation.rkt new file mode 100644 index 0000000..a922bc2 --- /dev/null +++ b/satore/tests/saturation.rkt @@ -0,0 +1,348 @@ +#lang racket/base + +(require (for-syntax syntax/parse + racket/base) + define2 + define2/define-wrapper + global + rackunit + racket/dict + racket/pretty + syntax/parse/define + "../clause.rkt" + "../misc.rkt" ; for easy access to *debug-level* + "../rewrite-tree.rkt" + (prefix-in sat: "../saturation.rkt") + "../unification.rkt") + +(define-global *cpu-limit* 10 + "Time limit in seconds for tests" + number? + string->number) + +(define (Vars+clausify-list l) + (map clausify + (symbol-variables->Vars l))) + +(define current-saturation-args #false) + +(define-syntax (for-in-list* stx) + (syntax-parse stx + [(_ ([var x ...] ... clauses ...) body ...) + #:with (name ...) (generate-temporaries #'(var ...)) + #'(for ((~@ [var (in-list (list x ...))] + [name (in-list '(x ...))] + #:when #true) + ...) + (set! current-saturation-args (list (cons 'var name) ...)) + body ...)])) + +;; Print additional information +(define old-check-handler (current-check-handler)) +(current-check-handler + (λ (e) + (eprintf (pretty-format current-saturation-args)) + (eprintf "\n") + (old-check-handler e))) + +;; USE THIS FOR DEBUGGING +(define-simple-macro (replay-on-failure body ...) + (let ([old-check-handler (current-check-handler)]) + (parameterize ([current-check-handler + (λ (e) + (old-check-handler e) + (eprintf + "Some checks have failed. Replaying in interactive mode for debugging.\n") + (*debug-level* 3) + (*cpu-limit* +inf.0) + (let () body ...))]) + ; encapsulated to avoid collisions + (let () body ...)))) + +(for-in-list* ([l-res-pruning? #true #false] + [neg-lit-select? #true #false] + [atom<=> KBO1lex<=> atom1<=>] + [dynamic-ok? #true #false] + [rwtree-in=out? #true #false] ; false means no search for new rules + ;#:unless (and l-res-pruning? neg-lit-select?) ; can't have both at the same time + ) + + (define-wrapper (saturation + (sat:saturation input-clauses + #:? [step-limit 200] + #:? [memory-limit 4096] ; in MB + #:? [cpu-limit (*cpu-limit*)] ; in seconds + #:? [rwtree (make-rewrite-tree #:atom<=> atom<=> + #:dynamic-ok? dynamic-ok?)] + #:? [rwtree-out (and rwtree-in=out? rwtree)] + #:? backward-rewrite? + #:? age:cost + #:? cost-type + #:? [disp-proof? #false] + #:? [L-resolvent-pruning? l-res-pruning?] + #:? [negative-literal-selection? neg-lit-select?])) + #:call-wrapped call + (define res (call)) + (unless l-res-pruning? + (check-equal? (dict-ref res 'L-resolvent-pruning) 0)) + (unless dynamic-ok? + (check-equal? (dict-ref res 'binary-rules-dynamic) 0)) + (unless rwtree-in=out? + (check-equal? (dict-ref res 'binary-rules) 0) + (check-true (= (dict-ref res 'binary-rewrites) 0))) + res) + + + ;; Some refutation tests + (check-equal? + (dict-ref (saturation (Vars+clausify-list '( [] ))) + 'status) + 'refuted) + (check-equal? + (dict-ref (saturation (Vars+clausify-list '( [p] ))) + 'status) + 'saturated) + (check-equal? + (dict-ref (saturation (Vars+clausify-list '( [p] + [(not p)]))) + 'status) + 'refuted) + (check-equal? + (dict-ref (saturation (Vars+clausify-list '( [p] + [(not q)]))) + 'status) + 'saturated) + + ;; WARNING (TODO): If L-resolvents-pruning applied to input clauses too, + ;; it would discard the 2nd clause immediately and would saturate! + (replay-on-failure + (check-equal? + (dict-ref (saturation (Vars+clausify-list '( [(p z)] + [(not (p X)) (p (s X))] + [(not q)]))) + 'status) + 'steps)) + + + + ;; Russell's 'paradox', requires factoring: + (check-equal? + (dict-ref (saturation (Vars+clausify-list + '( [(s X X) (s b X)] + [(not (s X X)) (not (s b X))]))) + 'status) + 'refuted) + + ;; Second version + (check-equal? + (dict-ref (saturation (Vars+clausify-list + '( [(s X b) (s b X)] + [(not (s X b)) (not (s b X))]))) + 'status) + 'refuted) + + + + ; TPTP 100k idx = 348 + (check-equal? + (dict-ref (saturation (Vars+clausify-list + '( [(big_f T0_0 T0_1) (big_g T0_0 T0_2)] + [(big_f T1_0 T1_1) (not (big_g T1_0 T1_0))] + [(big_g T2_0 T2_1) (not (big_f T2_0 T2_2))] + [(not (big_f T3_0 T3_1)) (not (big_g T3_0 (esk1_1 T3_0)))]))) + 'status) + 'refuted) + + + ; TPTP 100k idx = 784 + (check-equal? + (dict-ref (saturation (Vars+clausify-list '( [p1 p2] + [p1 (not p2)] + [p2 (not p1)] + [(not p1) (not p2)]))) + 'status) + 'refuted) + + + ; TPTP 100k idx = 117 + (check-equal? + (dict-ref (saturation + (Vars+clausify-list + '( [(big_f T0_0 T0_1 (esk3_2 T0_0 T0_1))] + [(big_f esk1_0 esk2_0 esk2_0) (not (big_f esk1_0 esk1_0 esk2_0))] + [(big_f esk1_0 esk1_0 esk2_0) + (big_f esk1_0 esk2_0 esk2_0) + (not (big_f esk2_0 esk2_0 T2_0))] + [(big_f esk1_0 esk1_0 esk2_0) + (big_f esk2_0 T3_0 T3_1) + (not (big_f esk1_0 esk2_0 esk2_0))] + [(not (big_f esk1_0 esk1_0 esk2_0)) + (not (big_f esk1_0 esk2_0 esk2_0)) + (not (big_f esk2_0 esk2_0 T4_0))] + [(big_f esk1_0 esk2_0 esk2_0) + (not (big_f T5_0 T5_1 (esk3_2 T5_1 T5_0))) + (not (big_f esk1_0 esk1_0 esk2_0))] + [(big_f esk1_0 esk1_0 esk2_0) + (not (big_f T6_0 (esk3_2 T6_0 T6_1) (esk3_2 T6_0 T6_1))) + (not (big_f esk1_0 esk2_0 esk2_0))] ))) + 'status) + 'refuted) + + (check-equal? + (dict-ref + (saturation + (Vars+clausify-list + '([(p X) (not (p (p X)))] + [(not (p a))] + [(not (q a))] + [(q X) (not (q (q (q X))))] + [(q (q (q (q (q (q (q (q (q (q (q (q (q (q (q a)))))))))))))))]))) + 'status) + 'refuted) + ;; This problem shows there may be some loops with implication-removal and factoring! + (check-equal? + (dict-ref + (saturation + (Vars+clausify-list + '([(not (p X Y)) (p X Z) (p Z Y)] + [(p x x)] + [(not (q a a a a b b b b c c c c))] + [(q A A A A B B B B C C C C) (not (q (q A A A A) (q B B B B) (q C C C C)))] + [(q (q a a a a) (q b b b b) (q c c c c))]))) + 'status) + 'refuted) + + ;; Binary rewrite + ;; This example shows that *not* backward rewriting rules can be a problem: + ;; Around step 19, there should be immediate resolution to '() with an active clause. + ;; But because [(not (p a A))] has not been rewritten to [(notp a A)], + ;; it cannot unify to '() immediately, and must wait for a *resolution* between + ;; the rule and the clause to pop up from the queue. + (replay-on-failure + (define res + (saturation + (map clausify + '(((notp A B) (p A B)) ; axiom, binary clause + ((not (notp A B)) (not (p A B))) ; axiom, converse binary clause + ((p a A) (q b B) (r c C) (s d D)) ; these two clauses should resolve to '() immediately + ((not (p A a))) ; Note that 'a A' is to prevent unit-clause rewrites + ((not (q B b))) + ((not (r C c))) + ((not (s D d))) + )))) + (check-equal? (dict-ref res 'status) 'refuted) + (when rwtree-in=out? + (check > (dict-ref res 'unit-rules) 0) + (check-equal? (dict-ref res 'binary-rules) 2) + (check > (dict-ref res 'binary-rewrites) 0))) + + ;; 'Asymmetric' rules + (replay-on-failure + (define res + (saturation + (map clausify + '([(not (p A A)) (q A)] ; Not a rule in itself (too general), but enables the next ones + [(p a a) (not (q a))] ; rule (p a a) <-> (q a) + [(p b b) (not (q b))] ; rule (p b b) <-> (q b) + [(p a a) (p b b) (p c c)] + [(not (q a)) (remove-me x Y)] + [(not (q b)) (remove-me x Y)] + [(not (p c c)) (remove-me x Y)] + [(not (remove-me X y))] ; defeats urw + )))) + (check-equal? (dict-ref res 'status) 'refuted) + (when rwtree-in=out? + (check-equal? (dict-ref res 'binary-rules) 4) + (check-true (> (dict-ref res 'binary-rewrites) 0)))) + ;; Same but with rules loaded from a file + ;; TODO + #; + (replay-on-failure + (define res + (saturation + (map clausify + '([(not (p A A)) (q A)] ; Not a rule in itself (too general), but enables the next ones + [(p a a) (not (q a))] ; rule (p a a) <-> (q a) + [(p b b) (not (q b))] ; rule (p b b) <-> (q b) + [(p a a) (p b b) (p c c)] + [(not (q a)) (remove-me x Y)] + [(not (q b)) (remove-me x Y)] + [(not (p c c)) (remove-me x Y)] + [(not (remove-me X y))] ; defeats urw + )))) + (check-equal? (dict-ref res 'status) 'refuted) + (when rwtree-in=out? + (check-equal? (dict-ref res 'binary-rules) 4) + (check-true (> (dict-ref res 'binary-rewrites) 0)))) + + ;; Greedy selection of binary rewrites can lead to failure + (replay-on-failure + (define res + (saturation + (map clausify + '(; equivalences + [(not (q A B C D)) (p A B C)] ; (q A B C D) <=> (p A B C) + [(q A B C D) (not (p A B C))] + [(not (p A b C)) (t a)] ; (p A b C) <=> (t a) + [(p A b C) (not (t a))] + [(not (q A B c D)) (s b c)] ; (q A b c D) <=> (s b c) + [(q A B c D) (not (s b c))] + ; inputs + ; may be rewritten to (s b c) + [(q a b c d) (remove-me x Y) (remove-me y Y) (remove-me z Y)] + [(not (t a)) (remove-me x Y) (remove-me y Y) (remove-me z Y)] + ; + [(not (remove-me X y))] ; defeats urw + )))) + (check-equal? (dict-ref res 'status) 'refuted) + (when rwtree-in=out? + (check-equal? (dict-ref res 'binary-rules) 6) + (check-true (> (dict-ref res 'binary-rewrites) 0)))) + + ;; Overlapping rewrites can lead to failures (but not without rewrites) + (replay-on-failure + (define res + (saturation + (map clausify + '(; equivalences + [(not (q A B C D)) (p A B C)] ; (q A B C D) <=> (p A B C) + [(q A B C D) (not(p A B C))] + [(not (p A b C)) (t a)] ; (p A b C) <=> (t a) + [(p A b C) (not (t a))] + [(not (q A b c D)) (s b c)] ; (q A b c D) <=> (s b c) + [(q A b c D) (not (s b c))] + ; inputs + [(s b c) (remove-me x Y) (remove-me y Y) (remove-me z Y)] + [(not (t a)) (remove-me x Y) (remove-me y Y) (remove-me z Y)] + ; + [(not (remove-me X y))] ; defeats urw + )))) + (check-equal? (dict-ref res 'status) 'refuted) + (when rwtree-in=out? + (check-equal? (dict-ref res 'binary-rules) 6) + (check-true (> (dict-ref res 'binary-rewrites) 0)))) + + ;; Greedy selection of overlapping rewrites can lead to failures + (replay-on-failure + (define res + (saturation + (map clausify + '(; equivalences + [(not (q A B C D)) (p A B C)] ; (q A B C D) <=> (p A B C) + [(q A B C D) (not(p A B C))] + [(not (p A b C)) (r A C)] ; (p A b C) <=> (r A C) + [(p A b C) (not (r A C))] + [(not (r A c)) (t a)] ; (r A c) <=> (t a) + [(r A c) (not (t a))] + [(not (q A b c D)) (s b c)] ; (q A b c D) <=> (s b c) + [(q A b c D) (not (s b c))] + ; inputs + [(s b c) (remove-me x Y) (remove-me y Y) (remove-me z Y)] + [(not (t a)) (remove-me x Y) (remove-me y Y) (remove-me z Y)] + ; + [(not (remove-me X y))] ; defeats urw + )))) + (check-equal? (dict-ref res 'status) 'refuted) + (when rwtree-in=out? + (check-equal? (dict-ref res 'binary-rules) 8) + (check-true (> (dict-ref res 'binary-rewrites) 0))))) diff --git a/satore/tests/stress-test1.rkt b/satore/tests/stress-test1.rkt new file mode 100644 index 0000000..d8b7b02 --- /dev/null +++ b/satore/tests/stress-test1.rkt @@ -0,0 +1,34 @@ +#lang racket/base + +(require "../clause.rkt" + "../unification.rkt") + +(define cms current-milliseconds) + +;;; Stress test. +;;; There's only one predicate of two arguments. +;;; This takes basically exponential time with n. +;;; All the time is taken by clausify (safe-factoring, which includes subsumption check) +(define (stress n) + (define pre (cms)) + (define cl1 + (time + (clausify + (fresh ; ensures the names are adequate variable names + (for/list ([i n]) + `(eq #s(Var ,i) #s(Var ,(+ i 1)))))))) + (define cl2 + (time + (clausify + (fresh + (for/list ([i (+ n 1)]) + `(eq #s(Var ,i) #s(Var ,(+ i 1)))))))) + (void (time (clause-subsumes cl1 cl2))) + (void (time (clause-subsumes cl2 cl1))) + (- (cms) pre)) + +;; Takes about 10s on my desktop machine for n=40 (subsumes-iter-limit=0). + +(for/list ([n (in-list '(10 20 30 40))]) + (printf "n = ~a\n" n) + (stress n)) diff --git a/satore/tests/timeplus.rkt b/satore/tests/timeplus.rkt new file mode 100644 index 0000000..1efc6a7 --- /dev/null +++ b/satore/tests/timeplus.rkt @@ -0,0 +1,13 @@ +#lang racket/base + +(require "../timeplus.rkt" + rackunit) + +(check-equal? (string-drop-common-prefix '("auiebépo" "auiensrt" "au")) + '("iebépo" "iensrt" "")) +(check-equal? (string-drop-common-prefix '("auiebépo" "auiensrt" )) + '("bépo" "nsrt")) +(check-equal? (string-drop-common-prefix '("auiebépo" )) + '("")) +(check-equal? (string-drop-common-prefix '("" )) + '("")) diff --git a/satore/tests/trie.rkt b/satore/tests/trie.rkt new file mode 100644 index 0000000..dc780dd --- /dev/null +++ b/satore/tests/trie.rkt @@ -0,0 +1,81 @@ +#lang racket/base + +(require "../trie.rkt" + rackunit + (only-in "../unification.rkt" symbol-variable?) + racket/pretty) + +(let ([atrie (make-trie #:variable? symbol-variable?)]) + (trie-set! atrie + '(a X (f Y) c) + 'A) + (trie-set! atrie + '(a b (f Y) c) + 'B) + (trie-set! atrie + '(a b (f Y) E) + 'C) + (check-equal? + (sort (trie-ref atrie '(a b (f (g e)) c)) symbol-subsumes)) + +(define (make-utree1) + (define utree (make-unification-tree)) + (for-each + (λ (cl) (add-Clause! utree (make-Clause (clausify cl)))) + '([(p A) (not (q B))] + [(q A) (r B)] + [(p c) (r b)])) + utree) + +(let () + (define utree (make-utree1)) + (define removed (utree-remove-subsumed! utree (clausify '[(q X)]))) + (check-equal? (length removed) 1) + (check-equal? (length (utree-remove-subsumed! utree (clausify '[(not (q X))]))) 1) + (check-equal? (length (utree-remove-subsumed! utree (clausify '[(r X)]))) 1) + (check-equal? (append* (trie-values utree)) '())) + +(let () + (define utree (make-utree1)) + (define removed (utree-remove-subsumed! utree (clausify '[(p d)]))) + (check-equal? (length removed) 0) + (define removed2 (utree-remove-subsumed! utree (clausify '[(p c)]))) + (check-equal? (length removed2) 1)) + +(let () + (define utree (make-utree1)) + (define removed (utree-remove-subsumed! utree (clausify '[(p X)]))) + (check-equal? (length removed) 2)) + diff --git a/satore/tests/unification.rkt b/satore/tests/unification.rkt new file mode 100644 index 0000000..c05568e --- /dev/null +++ b/satore/tests/unification.rkt @@ -0,0 +1,381 @@ +#lang racket/base + +(require (submod bazaar/order test) + racket/match + rackunit + "../unification.rkt") + +(check-eq? (Var-name->symbol (symbol->Var-name 'C)) 'C) +(check-eq? (Var-name->symbol (symbol->Var-name 'X0)) 'X0) +(check-eq? (Var-name->symbol (symbol->Var-name 'X1353)) 'X1353) + + +(check-equal? + (find-var-names (Varify '(p D C A B))) + (map Var-name (Varify '(D C A B)))) +(check-equal? + (find-var-names (Varify '(p (q D E) C A B E D D A))) + (map Var-name (Varify '(D E C A B)))) + +(let () + (define-check (check/fail-var-occs<=> p q c) + (let ([res (var-occs<=> p q)]) + (unless (eq? res c) + (fail-check (format "Params: ~a ~a \nExpected: ~a\nGot: ~a\n" p q c res))))) + (define (check-var-occs<=> p q c) + (let ([p (Varify p)] [q (Varify q)]) + (check/fail-var-occs<=> p q c) + (case c + [(<) (check/fail-var-occs<=> q p '>)] + [(>) (check/fail-var-occs<=> q p '<)] + [(= #false) (check/fail-var-occs<=> q p c)]))) + + (check-var-occs<=> '(p) '(q) '=) + (check-var-occs<=> '(p X) '(q) '>) + (check-var-occs<=> '(p X) '(q X) '=) + (check-var-occs<=> '(p X X) '(q X) '>) + (check-var-occs<=> '(p X Y) '(q X) '>) + (check-var-occs<=> '(p X Y) '(q X Z) #false) + (check-var-occs<=> '(p X X Y) '(q X Z) #false) + (check-var-occs<=> '(p X X Y) '(q X Y) '>) + (check-var-occs<=> '(p X X Y) '(q X Y Y) #false)) + +(let () + (check equal? (lnot 'auie) `(not auie)) + (check equal? (lnot (lnot 'auie)) 'auie) + (check equal? (lnot lfalse) ltrue) + (check equal? (lnot `(not ,lfalse)) lfalse) ; to fix non-reduced values + (check equal? (lnot `(not ,ltrue)) ltrue) ; to fix non-reduced values + (check equal? (lnot ltrue) lfalse) + (check equal? (lnot (lnot ltrue)) ltrue) + (check equal? (lnot (lnot lfalse)) lfalse) + (check<=> polarity<=> 'a '(not a) '<)) + + +(let () + (define-simple-check (check-atom1<=> a b res) + (check<=> atom1<=> (Varify a) (Varify b) res)) + + (check-atom1<=> lfalse 'a '<) + (check-atom1<=> lfalse lfalse '=) + (check-atom1<=> '() '() '=) + (check-atom1<=> '(eq b a) '(eq a b) '>) ; lexicographical order + (check-atom1<=> '(p X Y) '(p Y X) '=) ; no lex order between variables + (check-atom1<=> '(p a X) '(p X a) '=) ; no lex order between variable and symbol + (check-atom1<=> '(p A (q B)) + '(p (q A) B) + '=) ; no lex order when variable is involved + (check-atom1<=> '(p A (q b)) + '(p (q A) b) + '=) ; ???? + (check-atom1<=> '(not (eq X0 X1 X1)) ; var-occs= + '(not (eq X0 X1 X1)) + '=) + + (check-atom1<=> '(eq X0 X1 X1) + '(not (eq X0 X1 X1)) + '=) ; negation should NOT count + ;;; This is very important, otherwise the following problem can end with 'saturated: + ;;; ((notp A B) (p A B)) ; axiom, binary clause + ;;; ((not (notp A B)) (not (p A B))) ; axiom, converse binary clause + ;;; ((p a A)) ; these two clauses should resolve to '() immediately + ;;; ((not (p A a))) ; Note that 'a A' is to prevent unit-clause rewrites + + + (check-atom1<=> 'p 'q '<) + (check-atom1<=> '(not p) '(not q) '<) + + (check-atom1<=> '(not (eq X0 X1 X1)) + '(not (eq X1 X0)) + '>) + (check-atom1<=> '(p X Y Z) + '(p X Y one) + '>) + (check-atom1<=> '(p X A one) + '(p X Y one) + '#false) + (check-atom1<=> '(p X one one) + '(p X one) + '>) + (check-atom1<=> '(p X one (q one)) + '(p X one one) + '>) + + + ) + + +;; Tests for KBO +(let () + (define-simple-check (check-KBO1lex<=> a b res) + (check<=> KBO1lex<=> (Varify a) (Varify b) res)) + + + (check-KBO1lex<=> lfalse 'a '<) + (check-KBO1lex<=> lfalse lfalse '=) + + + ;(check-KBO1lex<=> '() '() '=) ; not a term + (check-KBO1lex<=> '(eq b a) '(eq a b) '>) ; lexicographical order + (check-KBO1lex<=> '(p X Y) '(p Y X) #false) ; commutativity cannot be oriented + (check-KBO1lex<=> '(p a X) '(p X a) #false) ; left->right order: a <=> X -> #false + (check-KBO1lex<=> '(p A (q B)) + '(p (q A) B) + '<) ; left->right order: A < (q A) + (check-KBO1lex<=> '(p A (q b)) + '(p (q A) b) + '<) ; left->right order: A < (q A) + (check-KBO1lex<=> '(not (eq X0 X1 X1)) ; var-occs= + '(not (eq X0 X1 X1)) + '=) + + (check-KBO1lex<=> '(eq X0 X1 X1) + '(not (eq X0 X1 X1)) + '=) ; negation should NOT count + ;;; This is very important, otherwise the following problem can end with 'saturated: + ;;; ((notp A B) (p A B)) ; axiom, binary clause + ;;; ((not (notp A B)) (not (p A B))) ; axiom, converse binary clause + ;;; ((p a A)) ; these two clauses should resolve to '() immediately + ;;; ((not (p A a))) ; Note that 'a A' is to prevent unit-clause rewrites + + + (check-KBO1lex<=> 'p 'q '<) ; lex + (check-KBO1lex<=> '(not p) '(not q) '<) ; lex + + (check-KBO1lex<=> '(not (eq X0 X1 X1)) + '(not (eq X1 X0)) + '>) ; by var-occs and weight + (check-KBO1lex<=> '(p X Y Z) + '(p X Y one) + #false) ; var-occs incomparable + (check-KBO1lex<=> '(p X Y (f Z)) + '(p X (f Y) one) + #false) ; var-occs incomparable + (check-KBO1lex<=> '(p X Y (f Z)) + '(p X (f Y) Z) + '<) ; same weight, Y < (f Y) + (check-KBO1lex<=> '(p X A one) + '(p X Y one) + #false) + (check-KBO1lex<=> '(p X one one) + '(p X one) + '>) + (check-KBO1lex<=> '(p X one (q one)) + '(p X one one) + '>) + + (check-KBO1lex<=> '(p A (p B C)) + '(p (p A B) C) + '<) ; associativity ok: A < (p A B) + ) + +(let () + (check-equal? (term-lex2<=> '(p a) '(p b)) '<)) + +(let () + (define-simple-check (check-term-lex<=> a b res) + (let-values ([(a b) (apply values (fresh (Varify (list a b))))]) + (check<=> term-lex<=> (Varify a) (Varify b) res))) + (check-term-lex<=> 'a (Var 'X) '>) + (check-term-lex<=> (Var 'X) (Var 'X) '=) + (check-term-lex<=> 'a 'a '=) + (check-term-lex<=> 'a 'b '<) + + (define-simple-check (check-literal<=> a b res) + (let-values ([(a b) (apply values (fresh (Varify (list a b))))]) + (check<=> literal<=> (Varify a) (Varify b) res))) + (check-literal<=> 'a '(not a) '<) + (check-literal<=> 'a 'b '<) + (check-literal<=> 'z '(not a) '<) + (check-literal<=> '(z b) '(not a) '<) + (check-literal<=> 'a 'a '=) + (check-literal<=> 'z '(a a) '>) + (check-literal<=> '(z z) '(z (a a)) '<)) + +(let () + (check-true (literal==? 'a 'a)) + (check-true (literal==? (Var 'X) (Var 'X))) + (check-true (literal==? (Var 'X) #s(Var X))) ; prefab + (check-false (literal==? (Var 'X) (Var 'Y))) + (check-false (literal==? (fresh (Var 'X)) (Var 'X))) + (check-false (literal==? 'X (Var 'X))) ; not considered the same?? + (check-true (literal==? `(p (f ,(Var 'X) ,(Var 'X)) y) `(p (f ,(Var 'X) ,(Var 'X)) y)))) + + +(let () + (define-check (test-unify t1 t2 subst) + (let ([t1 (Varify t1)] [t2 (Varify t2)]) + (set! subst (subst/#false->imsubst subst)) + (define sh (unify t1 t2)) + (define sl (subst/#false->imsubst + (and sh + (for/list ([(k v) (in-subst sh)]) + (cons (Var k) + (if (already-substed? v) + (already-substed-term v) + v)))))) + (unless (equal? sl subst) + (fail-check (format "Expected ~a. Got: ~a\nt1 = ~a\nt2 = ~a\n" + subst sl + t1 t2))) + (when sh + (define r1 (substitute t1 sh)) + (define r2 (substitute t2 sh)) + (unless (equal? r1 r2) + (fail-check "r1≠r2" sh r1 r2))))) + + (test-unify '(p X) + '(p X) + '()) + (test-unify '(p (f X) X) + '(p (f a) a) + '((X . a))) + (test-unify '(p (f c) (g X)) + '(p Y Y) + #false) + (test-unify '(p X (f X)) + '(p a Y) + '((X . a) (Y . (f a)))) + (test-unify '(p (f X Y) (f Y Z)) + '(p (f (f a) (f b)) (f (f b) c)) + '((X . (f a)) (Y . (f b)) (Z . c))) + (test-unify '(p X (p X) a) + '(p Y (p (p Z)) Z) + (if reduce-mgu? + '((Z . a) (X . (p a)) (Y . (p a))) + '((X . Y) (Y . (p Z)) (Z . a)))) + (test-unify '(p X (p X) (p (p X))) + '(p a Y Z) + '((X . a) (Y . (p a)) (Z . (p (p a))))) + (test-unify '(p X (p X) (p (p X))) + '(p a (p Y) (p (p Z))) + '((X . a) (Y . a) (Z . a))) + (test-unify '(p (p X) (p X) a) + '(p Y (p (p Z)) Z) + (if reduce-mgu? + '((Z . a) (X . (p a)) (Y . (p (p a)))) + '((Y . (p X)) (X . (p Z)) (Z . a)))) + (test-unify '(p X X) + '(p a Y) + '((X . a) (Y . a))) + (test-unify '(p X X) + '(p (f Y) Z) + '((X . (f Y)) (Z . (f Y)))) + (test-unify '(p X X) '(p (f Y) Y) #false) + (test-unify '(p (f X Y) (g Z Z)) + '(p (f (f W U) V) W) + (if reduce-mgu? + '((W . (g Z Z)) (Y . V) (X . (f (g Z Z) U))) + '((X . (f W U)) (Y . V) (W . (g Z Z))))) + + (test-unify '(eq X30 (mul X31 (mul X32 (inv (mul X31 X32))))) + '(eq (mul X25 one) X26) + `((X26 . (mul X31 (mul X32 (inv (mul X31 X32))))) + (X30 . (mul X25 one)))) + (test-unify '(p A B) + '(p B A) + '((A . B))) + ) + +(let () + (define (test-suite-left-unify left-unify) + (define-simple-check (test-left-unify t1 t2 subst) + (let ([t1 (Varify t1)] [t2 (Varify t2)]) + (set! subst (subst/#false->imsubst subst)) + (define sh (left-unify t1 t2)) + (define sl (subst/#false->imsubst sh)) + (check-equal? sl subst + (format "Expected ~a. Got: ~at1 = ~a\nt2 = ~a\n" + subst sl + t1 t2)) + (when sh + (define r1 (left-substitute t1 sh)) + (check-equal? r1 t2 (format "r1≠t2\nsh=~a\nr1=~a\nt2=~a\n" sh r1 t2))))) + + (test-left-unify '(p (f X) X) + '(p (f a) a) + '((X . a))) + (test-left-unify '(p (f c) (g X)) + '(p Y Y) + #false) + (test-left-unify '(p X (f X)) '(p a Y) #false) + (test-left-unify '(p (f X Y) (f Y Z)) + '(p (f (f a) (f b)) (f (f b) c)) + '((Z . c) (Y . (f b)) (X . (f a)))) + (test-left-unify '(p X X) '(p a Y) #false) + (test-left-unify '(p X X) '(p (f Y) Z) #false) + (test-left-unify '(p X X) '(p (f Y) Y) #false) + (test-left-unify '(p (f X Y) (g Z Z)) + '(p (f (f W U) V) W) + #false) + (test-left-unify '(p X X) + '(p A B) + #false) + ; This MUST return false because of the circularity. + ; The found substitution must be specializing, that is C2[σ] = C2 (and C1[σ] = C2), + ; otherwise safe factoring can fail, in particular. + ; Hence we must ensure that vars(C2) ∩ dom(σ) = ø. + (test-left-unify '(p A B) + '(p B A) + #false) + (test-left-unify '(p B A) + '(p A B) + #false) + (test-left-unify '(p A A) + '(p B B) + '((A . B))) + (test-left-unify '(p A) + '(p A) + '()) + (test-left-unify '(p a) + '(p a) + '()) + (test-left-unify '(p A X) ;; WARNING + '(p X Y) + #false)) + + (test-suite-left-unify left-unify) + (test-suite-left-unify (λ (t1 t2) (define subst-assoc (left-unify/assoc t1 t2)) + (and subst-assoc (make-subst subst-assoc))))) + + +(let ([pat '(_not_ (_not_ #s(Var A)))] + [t (fresh (Varify '(q (p (_not_ (_not_ (f A B)))))))]) + (define s + (left-unify-anywhere pat t)) + (check-equal? (left-substitute pat s) + (cadadr t))) + +(let ([t '(q (p (_not_ (_not_ (f A B)))))]) + (check-equal? + (match-anywhere (match-lambda [`(_not_ (_not_ ,x)) `([x . ,x])] [else #false]) + t) + '([x . (f A B)]))) + +;; Stress test for unification +;; This should take 0ms +;; See https://en.wikipedia.org/wiki/Unification_(computer_science) +;; #Examples_of_syntactic_unification_of_first-order_terms +(let () + (define last-var? #true) + (define (stress-unify n) + (define A + (let left ([d 1]) + (if (>= d n) + (list '* (Var d) (if last-var? (Var (+ d 1)) 'a)) + (list '* (left (+ d 1)) (Var d))))) + (define B + (let right ([d 1]) + (if (>= d n) + (list '* (if last-var? (Var (+ d 1)) 'a) (Var d)) + (list '* (Var d) (right (+ d 1)))))) + (define subst (time (unify A B))) + ; Verify that there's only 1 variable in the each rhs + (when (and reduce-mgu? last-var?) + (check-equal? (length (Vars (map cdr (subst->list subst)))) + 1 + subst)) + (time (substitute A subst))) + (for ([n (in-range 30 50)]) + (printf "~a: " n) + (stress-unify n))) diff --git a/satore/tptp.rkt b/satore/tptp.rkt new file mode 100644 index 0000000..52f1b9a --- /dev/null +++ b/satore/tptp.rkt @@ -0,0 +1,218 @@ +#lang racket/base + +;**************************************************************************************; +;**** Tptp Input/Output Format ****; +;**************************************************************************************; + +(require bazaar/debug + bazaar/string + global + racket/dict + racket/file + racket/format + racket/list + racket/match + racket/port + racket/string + satore/clause + satore/unification) + +(provide (all-defined-out)) + +(define-global:boolean *tptp-out?* #false + "Output is in TPTP format?") + +#| +File formats: + .rktd: Racket data, one Racket clause per line. + .p: Prolog format, with Prolog clauses that contain tptp (FOL) clauses. + .tptp: only the tptp clauses, one per line. + +|# + + +(define (tptp-program-file->clauses program-file) + ; Not efficient: Loads the whole program as a string then parses it. + ; It would be more efficient to read it as a stream with an actual parser. + ; Another possibility is to read it line by line and parse each line as a cnf(…) + ; but that will file if the cnf(…) is multiline. + (tptp-prog->clauses (file->string program-file))) + +(define (tptp-pre-clauses->clauses pre-clauses) + (define clauses + (for/list ([cl (in-list pre-clauses)]) + (let loop ([t cl]) + (match t + [(? symbol? x) x] + [(? string? x) + (string->symbol (string-append "_str_" x))] ; to avoid being interpreted as a variable + ['() '()] + [(list '~ (? symbol? pred) (list a ...) r ...) + (cons (list 'not (cons (loop pred) (loop a))) + (loop r))] + [(list (? symbol? pred) (list a ...) r ...) + (cons (cons (loop pred) (loop a)) + (loop r))] + [(list '~ x r ...) + (cons (list 'not (loop x)) + (loop r))] + [(list x a ...) + (cons (loop x) (loop a))] + [else (error "Unrecognized token: " t)])))) + (map (compose clausify symbol-variables->Vars) clauses)) + +;; Prolog .p program to rkt format +(define (tptp-prog->clauses str) + + ; hardly tested and not strict enough + ; It should be mostly robust to line breaking though. + ; Doesn't parse strings properly (will remove lines that look like comments in multiline strings) + (define l + (filter + (λ (x) + (if (list? x) + x + (begin + (assert (memq x '(cnf end_cnf)) + x) + #false))) + ; Ensure operators are surrounded with spaces + ; turn racket special symbols (| and ,) into normal symbols. + ; then use racket's reader to parse it like an s-expression + (string->data + (regexp-replaces + str + (list* + '[#px"(?:^|\n)\\s*[%#][^\n]*" "\n"] ; prolog and shell/python/eprover full-line comments + '[#px"\\bnot\\b" "_not_"] ;; WARNING!!! replace lnot with $not instead (as in TPTP) + (map (λ (p) (list (regexp-quote (first p)) + (string-append " " (regexp-replace-quote (second p)) " "))) + '(["|" "" ] + ["&" "" ] + ["," "" ] + ["$false" ""] ; empty literal + ["~" "~"] + ["." "end_cnf"] + ["'" "\""]))))))) + ; first is name, second is type, third is clause, rest is comments(?) + (define pre-clauses (map third l)) + (tptp-pre-clauses->clauses pre-clauses)) + + +;; Simple parser for the proposer output into s-exp clauses. +;; The format is expected to be in cnf. +(define (tptp-string->clauses str) + ; TODO: Optimize. This can be veeeery slow for large conjectures. + (define pre-clauses + (append* + ; split first to avoid regenerating the whole string after each substitution? + (for/list ([str (in-list (string-split str #px"&|\n"))]) ; & and \n play the same role + (with-handlers ([exn? (λ (e) (displayln str) (raise e))]) + (string->data + ; Ensure operators are surrounded with spaces + ; turn racket special symbols (| and ,) into normal symbols + (regexp-replaces + str + (list* + '[#px"\\bnot\\b" "_not_"] ;; WARNING!!! Instead: replace lnot with $not (as TPTP) + (map (λ (p) (list (regexp-quote (first p)) + (string-append " " (regexp-replace-quote (second p)) " "))) + '(["|" ""] + ["," ""] + ["~" "~"] + ["'" "\""]))))))))) + (tptp-pre-clauses->clauses pre-clauses)) + + +(define (literal->tptp-string lit) + (cond + [(lnot? lit) + (string-append "~ " (literal->tptp-string (second lit)))] + [(empty? lit) + "$false"] + [(list? lit) + (string-append (literal->tptp-string (first lit)) + "(" + (string-join (map literal->tptp-string (rest lit)) ", ") + ")")] + [(Var? lit) (symbol->string (Var-name->symbol lit))] + [else (format "~a" lit)])) + +(define (clause->tptp-string cl) + (string-join + (map literal->tptp-string (Vars->symbols cl)) + " | ")) + +(define (clauses->tptp-string cls) + (string-join (map clause->tptp-string cls) "\n")) + +;; String replacement of tptp names with shorter ones to improve readability +(define (tptp-shortener str) + (define substs + (sort + (map (λ (p) (cons (~a (car p)) (~a (cdr p)))) + ; fld_1 + (append + '((multiplicative_identity . _1) + (additive_identity . _0) + (less_or_equal . ≤) + (additive_inverse . –) + (multiplicative_inverse . /) + (equalish . ≃) + (multiply . ×) + (product . ×=) + (inverse . /) + (add . +) + ) + ;grp_5 + '((equalish . ≃) + (multiply . ×) + (product . ×=) + (inverse . /) + (identity . _1) + ) + ; geo + '((convergent_lines . /\\) + (unorthogonal_lines . ¬⊥) + (orthogonal_through_point . ⊥_thru_pt) + (parallel_through_point . //_thru_pt) + (distinct_lines . ≠_ln) + (apart_point_and_line . ≠_pt_ln) + (orthogonal_lines . ⊥) + (distinct_points . ≠_pt) + (parallel_lines . //) + (equal_lines . =_ln) + (equal_points . =_pt))) + ) + ; forces prefixes to appear later to match longer strings first: + > #:key (compose string-length car))) + + + (string-join + (for/list ([line (in-lines (open-input-string str))]) + (for/fold ([line line]) + ([(from to) (in-dict substs)]) + (string-replace line from to #:all? #true))) + "\n")) + +(define-syntax-rule (with-tptp-shortener body ...) + (let ([str (with-output-to-string (λ () body ...))]) + (displayln (tptp-shortener str)))) + +;============; +;=== Main ===; +;============; + +(module+ main + (require global + racket/file) + + (define-global *rktd-file* #false + "file in rktd format to output in tptp format" + file-exists? + values) + + (void (globals->command-line)) + + (when (*rktd-file*) + (displayln (clauses->tptp-string (file->list (*rktd-file*)))))) diff --git a/satore/trie.rkt b/satore/trie.rkt new file mode 100644 index 0000000..d958b01 --- /dev/null +++ b/satore/trie.rkt @@ -0,0 +1,220 @@ +#lang racket/base + +;***************************************************************************************; +;**** Trie: Imperfect Discrimination Tree ****; +;***************************************************************************************; + +;;; A key is a tree (a list of lists of ...), which is flattened to a list +;;; where parenthesis are replaced with symbols. +;;; Variables are considered to be unnamed and there is no unification/matching. +;;; The only dependency on first-order logic specifics is `variable?`. + +(require bazaar/cond-else + racket/list + racket/match + satore/misc) + +(provide (except-out (all-defined-out) no-value) + (rename-out [no-value trie-no-value])) + +;; Default value at the leaves. Should not be visible to the user. +(define no-value (string->uninterned-symbol "no-value")) +; Tokens used in the keys of the tree +(define anyvar (string->uninterned-symbol "¿")) +(define sublist-begin (string->uninterned-symbol "<<")) +(define sublist-end (string->uninterned-symbol ">>")) + +;; edges: hasheq(key . node?) +(struct trie-node (edges value) + #:transparent + #:mutable) +(define (make-node) + (trie-node (make-hasheq) no-value)) + +;; Trie structure with variables. +(struct trie (root variable?)) + +(define (make-trie #:constructor [constructor trie] + #:variable? [variable? (λ (x) #false)] + . other-args) + (apply constructor (make-node) variable? other-args)) + +;; Updates the value of the node for the given key (or add one if none exists). +;; atrie: trie? +;; key: list? +;; val: any/c +(define (trie-update! atrie key update default-val/proc) + (match-define (trie root variable?) atrie) + ; The key is `list`ed because we need a list, and this allows the given key to not be a list. + (let node-insert! ([nd root] [key (list key)]) + (cond/else + [(empty? key) + ; Stop here. + (define old-value (trie-node-value nd)) + (set-trie-node-value! nd (update (if (eq? old-value no-value) + (if (thunk? default-val/proc) + (default-val/proc) + default-val/proc) + old-value)))] + #:else ; key is a list + (define k (car key)) + (define edges (trie-node-edges nd)) + #:cond + [(pair? k) + ; Linearize the tree structure of the key. + (define key2 (cons sublist-begin (append k (cons sublist-end (cdr key))))) + (node-insert! nd key2)] + #:else ; nil, atom, variable + (let ([k (if (variable? k) anyvar k)]) + (define nd2 (hash-ref! edges k make-node)) + (node-insert! nd2 (cdr key)))))) + +;; Keep a list of values at the leaves. +;; If `trie-insert!` is used, any use of `trie-update!` should be consistent with values being lists. +(define (trie-insert! atrie key val) + (trie-update! atrie key (λ (old) (cons val old)) '())) + +;; Replacing the current value (if any) for key with val. +(define (trie-set! atrie key val) + (trie-update! atrie key (λ _ val) #false)) + +;; Applies on-leaf at each node that match with key. +;; The matching keys of the trie are necessarily no less general than the given key. +(define (trie-find atrie key on-leaf) + (define variable? (trie-variable? atrie)) + (let node-ref ([nd (trie-root atrie)] [key (list key)]) + (cond/else + [(empty? key) + ; Leaf found. + (unless (eq? no-value (trie-node-value nd)) + (on-leaf nd))] + #:else + (define k (car key)) + (define var-nd (hash-ref (trie-node-edges nd) anyvar #false)) + #:cond + [(variable? k) + (when var-nd + ; both the key and the node are variables + (node-ref var-nd (cdr key)))] + #:else + (when var-nd + ; If a variable matches, consider the two paths. + (node-ref var-nd (cdr key))) + #:cond + [(pair? k) + ; Linearize the tree structure of the key. + (define key2 (cons sublist-begin (append k (cons sublist-end (cdr key))))) + (node-ref nd key2)] + #:else + (define nd2 (hash-ref (trie-node-edges nd) k #false)) + (when nd2 + (node-ref nd2 (cdr key)))))) + +;; Applies the procedure `on-leaf` to any node for which the key is matched by the given key. +;; The matching keys of the trie are necessarily no more general than the given key. +;; TODO: We could easily maintain a substitution over the branches since there's only one match. +;; on-leaf: (-> node? any/c) +(define (trie-inverse-find atrie key on-leaf) + (define variable? (trie-variable? atrie)) + (let node-find ([nd (trie-root atrie)] [key (list key)] [depth 0]) + (define edges (trie-node-edges nd)) + (cond/else + [(> depth 0) + ; If the depth is positive, that means we are currently matching a variable. + ; We need to continue through every branch and decrease the depth only if we encounter + ; a sublist-end, and increase the counter if we encounter a sublist-begin. + ; Note that key can be empty while depth > 0. + (for([(k2 nd2) (in-hash edges)]) + (node-find nd2 key + (cond [(eq? k2 sublist-begin) (+ depth 1)] + [(eq? k2 sublist-end) (- depth 1)] + [else depth])))] + [(empty? key) + ; Leaf found. + (unless (eq? no-value (trie-node-value nd)) + (on-leaf nd))] + #:else + (define k (car key)) + #:cond + [(variable? k) + ;; Anything matches. For sublist we need to keep track of the depth. + ;; Note that variables in the tree can only be matched if k is a variable. + (for ([(k2 nd2) (in-hash edges)]) + (node-find nd2 (cdr key) (if (eq? k2 sublist-begin) 1 0)))] + [(pair? k) + ; Linearize the tree structure of the key. + (define key2 (cons sublist-begin (append k (cons sublist-end (cdr key))))) + (node-find nd key2 0)] + #:else + (define nd2 (hash-ref edges k #false)) + (when nd2 + (node-find nd2 (cdr key) 0))))) + +;; Both find and inverse-find at the same time. +;; Useful when (full) unification must be performed afterwards. +;; WARNING: A LOT OF CODE DUPLICATION WITH THE ABOVE 2 FUNCTIONS. +(define (trie-both-find atrie key on-leaf) + (define variable? (trie-variable? atrie)) + (let node-find ([nd (trie-root atrie)] [key (list key)] [depth 0]) + (define edges (trie-node-edges nd)) + (cond/else + [(> depth 0) + ; If the depth is positive, that means we are currently matching a variable. + ; Consume everything until we find a sublist-end at depth 1. + ; We need to continue through every branch and decrease the depth only if we encounter + ; a sublist-end, and increase the counter if we encounter a sublist-begin. + ; Note that key can be empty while depth > 0. + (for([(k2 nd2) (in-hash edges)]) + (node-find nd2 key + (cond [(eq? k2 sublist-begin) (+ depth 1)] + [(eq? k2 sublist-end) (- depth 1)] + [else depth])))] + [(empty? key) + ; Leaf found. + (unless (eq? no-value (trie-node-value nd)) + (on-leaf nd))] + #:else + (define k (car key)) + (define var-nd (hash-ref (trie-node-edges nd) anyvar #false)) + #:cond + [(variable? k) + ;; Anything matches. For sublist we need to keep track of the depth. + ;; Note that variables in the tree can only be matched if k is a variable. + (for ([(k2 nd2) (in-hash edges)]) + (node-find nd2 (cdr key) (if (eq? k2 sublist-begin) 1 0)))] + #:else + (when var-nd + ; The node contains a variable, which thus matches the key. + (node-find var-nd (cdr key) 0)) + #:cond + [(pair? k) + ; Linearize the tree structure of the key. + (define key2 (cons sublist-begin (append k (cons sublist-end (cdr key))))) + (node-find nd key2 0)] + #:else + (define nd2 (hash-ref edges k #false)) + (when nd2 + (node-find nd2 (cdr key) 0))))) + + +(define ((make-proc-tree-ref proc) atrie key) + (define res '()) + (proc atrie + key + (λ (nd) (set! res (cons (trie-node-value nd) res)))) + res) + +;; Returns a list of values which keys are matched by the given key. +;; The matching keys of the trie are necessarily no more general than the given key. +;; TODO: We could easily maintain a substitution over the branches since there's only one mach +(define trie-inverse-ref (make-proc-tree-ref trie-inverse-find)) +(define trie-ref (make-proc-tree-ref trie-find)) +(define trie-both-ref (make-proc-tree-ref trie-both-find)) + +(define (trie-values atrie) + (let loop ([nd (trie-root atrie)] [res '()]) + (define edges (trie-node-edges nd)) + (define val (trie-node-value nd)) + (for/fold ([res (if (eq? val no-value) res (cons val res))]) + ([(key nd2) (in-hash edges)]) + (loop nd2 res)))) diff --git a/satore/unification-tree.rkt b/satore/unification-tree.rkt new file mode 100644 index 0000000..7f5509f --- /dev/null +++ b/satore/unification-tree.rkt @@ -0,0 +1,346 @@ +#lang racket/base + +;**************************************************************************************; +;**** Unification Tree ****; +;**************************************************************************************; + +;;; A trie specialized for unifying literals. +;;; This is *different* from "substitution trees" +;;; (https://link.springer.com/chapter/10.1007%2F3-540-59200-8_52) + +;;; TODO: This should be probably named a Clause-trie instead, since the +;;; major difference with the trie is that we are dealing with Clauses, which +;;; are lists of literals, and the same Clause can appear in different leaves +;;; of the trie. Unification is only one of the operations performed on Clauses. + +;;; * A literal A unifies with a literal B iff there exists a substitution σ s.t. Aσ = Bσ. +;;; * A literal A left-unifies with a literal B iff there exists a substitution σ s.t. +;;; Aσ = B and Bσ = B +;;; The last requirement ensures that left-unifies => unifies. +;;; * We call 'sub-varing' a set of literals As the process of replacing each variable occurrence in +;;; the As with a fresh variable. Hence, if B=subvar(A) then the variables in B occur only once +;;; each in B. + +(require bazaar/cond-else + bazaar/debug + bazaar/list + bazaar/loop + bazaar/mutation + (except-in bazaar/order atom<=>) + define2 + global + racket/list + satore/Clause + satore/clause + satore/misc + satore/trie + satore/unification) + +(provide (all-defined-out) + (all-from-out satore/trie)) + +(module+ test + (require rackunit)) + +;; WARNING: This cannot be applied to input clauses. +;; WARNING: To pass Russell's problem, we must +;; do 1-to-N resolution (non-binary resolution), OR, maybe, +;; binary resolution + unsafe factoring, but the 'resolutions' +;; for factoring must be taken into account too. +(define-global:boolean *L-resolvent-pruning?* #false + '("Discard clauses for which a literal leads to 0 resolvents." + "Currently doesn't apply to input clauses.")) + +(define-counter n-L-resolvent-pruning 0) + +;========================; +;=== Unification Tree ===; +;========================; + +;; TODO: Fix naming convention on operations on unification-tree. (utree-?) + +;; Clause-clause: Clause? -> clause ; extract the clause from the Clause object. +;; This module does not need to know what a Clause? is, it only needs to be given this extraction +;; function. It is however assumed that the Clause is an immutable struct object (or the mutation +;; does not concern Clause-clause). +(struct unification-tree trie () #:transparent) + +;; Several leaves may have the same clause-idx but different clauses——well, the same clauses +;; but ordered differently. It's named `uclause` to make it clear it's not a well-formed clause +;; (stands for unordered-clause). +(struct utree-leaf (Clause uclause) #:transparent) + + +(define (make-unification-tree #:constructor [constructor unification-tree] + . other-args) + (apply make-trie + #:constructor constructor + #:variable? Var? + other-args)) + +;; Each literal of the clause cl is added to the tree, and the leaf value at each literal lite is the +;; clause, but where the first literal is lit. +;; /!\ Thus the clause is *not* sorted according to `sort-clause`. +;; Note: We could also keep the clause unchanged and cons the index of the literal, +;; that would avoid using up new cons cells, while keeping the clause intact. +(define (add-Clause! utree C) + (define cl (Clause-clause C)) + (zip-loop ([(left lit right) cl]) + ;; *****WARNING***** + ;; The key must be a list! what if the literal is a mere symbol?? + (define reordered-clause (cons lit (rev-append left right))) + (trie-insert! utree lit (utree-leaf C reordered-clause)))) + +(define (unification-tree-Clauses utree) + (remove-duplicates (map utree-leaf-Clause (append* (trie-values utree))) eq?)) + +;; Calls on-unified for each literal of each clause of utree that unifies with lit. +;; If a clause cl has n literals that unify with lit, then `on-unified` is called n times. +;; on-unified : utree-leaf? subst lit1 lit2 other-lit2s -> void? +(define (find-unifiers utree lit on-unified) + (trie-both-find utree lit + (λ (nd) + (define val (trie-node-value nd)) + (when (list? val) + (for ([lf (in-list val)]) + (define cl (utree-leaf-uclause lf)) + ; Unify only with the first literal, assuming clauses in node-values + ; are so that the first literal corresponds to the key + ; (the path from the root) + (define lit2 (first cl)) + (define subst (unify lit2 lit)) + (when subst + (on-unified lf subst lit lit2 (rest cl)))))))) + +;; Returns the set of Clauses that *may* left-unify with lit. +;; The returned clauses are sorted according to `sort-clause` and duplicate clauses are removed. +(define (unification-tree-ref utree lit) + ; Node values are lists of rules, and trie-ref returns a list of node-values, + ; hence the append*. + (remove-duplicates (append* (map utree-leaf-Clause (trie-ref utree lit))) eq?)) + +;; Helper for the resolve/factors functions below. +;; Defines a new set of Clauses, and a helper function that creates new Clauses, +;; rewrites them, checks for tautologies and add them to the new-Clauses. +(define-syntax-rule (define-add-Clause! C new-Clauses add-Clause! rewriter) + (begin + (define new-Clauses '()) + (define (add-Clause! lits subst type parents) + (define cl (clause-normalize (substitute lits subst))) + (define new-C (make-Clause cl (cons C parents) #:type type)) + ; Rewrite + (let ([new-C (rewriter new-C)]) + (unless (Clause-tautology? new-C) + (cons! new-C new-Clauses)))))) + + +(define (utree-resolve/select-literal utree C + #:? [rewriter (λ (C) C)] + #:? [literal-cost literal-size]) + + (define cl (Clause-clause C)) + ;; Choose the costliest negative literal if any (for elimination) + (define selected-idx + (for/fold ([best-idx #false] + [best-cost -inf.0] + #:result best-idx) + ([lit (in-list cl)] + [idx (in-naturals)] + #:when (lnot? lit)) ; negative literals only + (define c (literal-cost lit)) + (if (> c best-cost) + (values idx c) + (values best-idx best-cost)))) + + (zip-loop ([(left lit right) cl] + [resolvents '()] + [lit-idx 0] + #:result (or resolvents '())) + (cond + [(or (not selected-idx) + (= lit-idx selected-idx)) + + (define-add-Clause! C new-Clauses add-Clause! rewriter) + + ; Find resolvents + (find-unifiers utree + (lnot lit) + (λ (lf subst nlit lit2 rcl2) + (add-Clause! (rev-append left (rev-append right rcl2)) + subst + 'res + (list (utree-leaf-Clause lf))))) + (values (rev-append new-Clauses resolvents) + (+ 1 lit-idx))] + [else + (values resolvents + (+ 1 lit-idx))]))) + +(define (unsafe-factors C #:? [rewriter (λ (C) C)]) + (define-add-Clause! C factors add-Clause! rewriter) + (define cl (Clause-clause C)) + + (zip-loop ([(left lit1 right) cl]) + (define pax (predicate.arity lit1)) + (zip-loop ([(left2 lit2 right2) right] + ; Literals are sorted, so no need to go further. + #:break (not (equal? pax (predicate.arity lit2)))) + (define subst (unify lit1 lit2)) + ; We could do left-unify instead, but then we need to do both sides, + ; at the risk of generating twice as many clauses, so may not be worth it. + (when subst + (add-Clause! (rev-append left right) ; remove lit1 + subst + 'fac + '())))) + factors) + +(define (utree-resolve+unsafe-factors/select utree C #:? rewriter #:? literal-cost) + (rev-append + (unsafe-factors C #:rewriter rewriter) + (utree-resolve/select-literal utree C + #:rewriter rewriter + #:literal-cost literal-cost))) + +;; TODO: Deactivate rewriting inside add-candidates! +;; Returns the set of Clauses from resolutions between cl and the clauses in utree, +;; as well as the factors +(define (utree-resolve+unsafe-factors utree C + #:? [rewriter (λ (C) C)] + #:! L-resolvent-pruning?) + ;; Used to prevent pruning by L-resolvent-discard. + ;; This is used to mark the second literals in unsafe factors. + (define lit-marks (make-vector (Clause-n-literals C) #false)) + (define (mark-literal! idx) (vector-set! lit-marks idx #true)) + (define (literal-marked? idx) (vector-ref lit-marks idx)) + + + (zip-loop ([(left lit right) (Clause-clause C)] + [resolvents+factors '()] + [lit-idx 0] + #:break (not resolvents+factors) ; shortcut + #:result (or resolvents+factors '())) + + (define-add-Clause! C new-Clauses add-Clause! rewriter) + + ;; Resolutions + (find-unifiers utree + (lnot lit) + (λ (lf subst nlit lit2 rcl2) + (add-Clause! (rev-append left (rev-append right rcl2)) + subst + 'res + (list (utree-leaf-Clause lf))))) + ;; Unsafe binary factors + ;; Somewhat efficient implementation since the literals are sorted by predicate.arity. + (define pax (predicate.arity lit)) + (zip-loop ([(left2 lit2 right2) right] + [lit2-idx (+ 1 lit-idx)] + #:break (not (equal? pax (predicate.arity lit2)))) + (define subst (unify lit lit2)) + (when subst + (mark-literal! lit2-idx) ; prevents pruning + (add-Clause! (rev-append left right) ; remove lit + subst + 'fac + '())) + (+ 1 lit2-idx)) + + ;; L-resolvent 'pruning' + ;; See the principle of implication modulo resolution: + ;; "A unifying principle for clause elimination in first-order logic", CADE 26. + ;; which contains other techniques and short proofs of their soundness. + ;; We return the empty set of resolution, meaning that the selected clause + ;; can (must) be discarded, i.e., not added to the active set. + (cond [(and L-resolvent-pruning? + (empty? new-Clauses) + (not (literal-marked? lit-idx))) + (++n-L-resolvent-pruning) + (values #false (+ 1 lit-idx))] + [else + (values (rev-append new-Clauses resolvents+factors) + (+ 1 lit-idx))]))) + +;; Returns the first (in any order) Clause C2 such that +;; there is a literal of C2 that left-subunifies on a literal of C, +;; and (pred C C2). +(define (utree-find/any utree C2 pred) + (define tested (make-hasheq)) ; don't test the same C2 twice + (define cl2 (Clause-clause C2)) + (let/ec return + (for ([lit (in-list cl2)]) + (trie-find utree lit + (λ (nd) + (define val (trie-node-value nd)) + (when (list? val) + (for ([lf (in-list val)]) + (define C (utree-leaf-Clause lf)) + (hash-ref! tested + C + (λ () + (when (pred C C2) + (return C)) + #true))))))) + #false)) + +;; Return all Clauses C that left-subunify on at least one literal and for which (pred C C2). +(define (utree-find/all utree C2 pred) + (define tested (make-hasheq)) ; don't test the same C2 twice + (define cl2 (Clause-clause C2)) + (define res '()) + (for ([lit (in-list cl2)]) + (trie-find utree lit + (λ (nd) + (define val (trie-node-value nd)) + (when (list? val) + (for ([lf (in-list val)]) + (define C (utree-leaf-Clause lf)) + (hash-ref! tested + C + (λ () + (when (pred C C2) + (set! res (cons C res))) + #true))))))) + res) + +;; Removes the Clause C from the utree. +(define (utree-remove-Clause! utree C) + (define cl (Clause-clause C)) + (for ([lit (in-list cl)]) + (trie-find utree lit + (λ (nd) + (define val (trie-node-value nd)) + (when (list? val) + (set-trie-node-value! nd + (filter-not (λ (lf2) (eq? C (utree-leaf-Clause lf2))) + val))))))) + +;; Finds the leaves for which C loosely left-unifies on some literal and remove those which clause C2 +;; where (pred C C2). +;; Returns the set of Clauses that have been removed. +;; pred: Clause? Clause? -> boolean +(define (utree-inverse-find/remove! utree C pred) + ; Since the same Clause may match multiple times, + ; We use a hash to remember which clauses have already been tested (and if the result + ; was #true or #false). + ; Then remove all the leaves of each clause to remove. + (define tested (make-hasheq)) + (define Clauses-to-remove '()) + (define cl (Clause-clause C)) + (for ([lit (in-list cl)]) + (trie-inverse-find utree lit + (λ (nd) + (define val (trie-node-value nd)) + (when (list? val) + (for ([lf (in-list (trie-node-value nd))]) + (define C2 (utree-leaf-Clause lf)) + (hash-ref! tested + C2 + (λ () + (cond [(pred C C2) + (cons! C2 Clauses-to-remove) + #true] + [else #false])))))))) + (for ([C2 (in-list Clauses-to-remove)]) + (utree-remove-Clause! utree C2)) + Clauses-to-remove) diff --git a/satore/unification.rkt b/satore/unification.rkt new file mode 100644 index 0000000..489de88 --- /dev/null +++ b/satore/unification.rkt @@ -0,0 +1,705 @@ +#lang racket/base + +;***************************************************************************************; +;**** Operations On Literals: Unification And Friends ****; +;***************************************************************************************; + +(require bazaar/cond-else + bazaar/debug + bazaar/list + bazaar/mutation + (except-in bazaar/order atom<=>) + define2 + global + racket/dict + racket/list + racket/match + (submod racket/performance-hint begin-encourage-inline) + satore/misc) + +(provide (all-defined-out)) + +;===============; +;=== Globals ===; +;===============; + +(define-global:category *atom-order* 'atom1 + '(atom1 KBO1lex) + "Atom comparison function for rewrite rules.") + +(define (get-atom<=> #:? [atom-order (*atom-order*)]) + (case atom-order + [(KBO1lex) KBO1lex<=>] + [(atom1) atom1<=>] + [else (error "Unknown atom order: ~a" (*atom-order*))])) + +;=================; +;=== Variables ===; +;=================; + +(struct Var (name) + #:prefab) + +(begin-encourage-inline + (define Var-name number<=>) + + (define (Var=? v1 v2) (Var-name=? (Var-name v1) (Var-name v2))) + (define (Var v1 v2) (Var-name<=> (Var-name v1) (Var-name v2))) +; (order=? (Var<=> v1 v2)) = (Vars=? v1 v2) + +;:::::::::::::::::::::::::::::::::::; +;:: Basic operations on Variables ::; +;:::::::::::::::::::::::::::::::::::; + +;; All symbols starting with a capitale letter are considered as variables. +(define (symbol-variable? t) + (and (symbol? t) + (char<=? #\A (string-ref (symbol->string t) 0) #\Z))) + +;; The same symbol is always mapped to the same Var-name, globally. +(define (symbol->Var-name s) + (define str (symbol->string s)) + (cond [(regexp-match #px"^X(\\d+)$" str) + => (λ (m) (+ 26 (string->number (second m))))] + [(regexp-match #px"^[A-Z]$" str) + => (λ (m) (- (char->integer (string-ref str 0)) + (char->integer #\A)))] + [else + (error 'Varify "Unknown variable format: ~a" s)])) + +;; The same Var-name is always mapped to the same symbol, globally. +(define (Var-name->symbol n) + (cond [(symbol-variable? n) n] + [(number? n) + (if (< n 26) + (string->symbol (string (integer->char (+ (char->integer #\A) n)))) + (string->symbol (format "X~a" (- n 26))))] + [else (error 'Var-name->symbol "Don't know what to do with ~a" n)])) + +;; Returns a new atom like t where all symbol-variables have been turned into `Var?`s. +(define (Varify t) + (cond [(pair? t) + ; Works also in assocs + (cons (Varify (car t)) + (Varify (cdr t)))] + [(symbol-variable? t) + (Var (symbol->Var-name t))] + [else t])) + +;; Returns a new atom like t where all `Var`s are replaced with a symbol. +(define (unVarify t) + (cond [(pair? t) + ; Works also in assocs + (cons (unVarify (car t)) + (unVarify (cdr t)))] + [(Var? t) + (Var-name->symbol (Var-name t))] + [else t])) + +(define (rule->string rule) + (format "~a -> ~a" (first rule) (second rule))) + + +;====================================; +;=== Substitutions data structure ===; +;====================================; + +(define (make-make-hash =?) + (cond [(eq? =? eq?) make-hasheq] + [(or (eq? =? =) (eq? =? eqv?)) make-hasheqv] + [(eq? =? equal?) make-hash] + [else (error 'make-make-hash "Unknown hash type: ~a" =?)])) + +(begin-encourage-inline + (define make-subst (make-make-hash Var-name=?)) + (define subst? hash?) + (define in-subst in-hash) + (define subst-count hash-count) + (define subst-ref/name hash-ref) ; for when the name is retrieved from the subst + (define subst-set!/name hash-set!) + (define subst-copy hash-copy) + + (define (subst-set! subst var t) + (hash-set! subst (Var-name var) t) + subst) ; return the substitution to mimick the immutable update behaviour + + (define (subst-ref subst var [default #false]) + (hash-ref subst (Var-name var) default)) + + (define (subst-ref! subst var default) + (hash-ref! subst (Var-name var) default)) + + (define (subst-update! subst var update default) + (hash-update! subst (Var-name var) update default) + subst) + + (define (subst->list s) + (sort (hash->list s) Var-nameVars t) + (define h (make-hasheq)) + (let loop ([t t]) + (cond [(pair? t) + (cons (loop (car t)) (loop (cdr t)))] + [(symbol-variable? t) + (hash-ref! h t new-Var)] + [else t]))) + +;; Variables are replaced with symbols by order of appearence. Mostly for ease of reading by humans. +(define (Vars->symbols t) + (define h (make-subst)) + (define idx -1) + (let loop ([t t]) + (cond [(pair? t) + (cons (loop (car t)) (loop (cdr t)))] + [(Var? t) + (subst-ref! h t (λ () (++ idx) (Var-name->symbol idx)))] + [else t]))) + +;; Returns a subst of the number of occurrences of the variables *names* in the term t. +;; (-> term? subst?) +(define (var-occs t) + (define h (make-subst)) + (let loop ([t t]) + (cond [(pair? t) + (loop (car t)) + (loop (cdr t))] + [(Var? t) + (subst-update! h t add1 0)])) + h) + +;; Returns the variable names of the term t. +(define (vars t) + (map car (subst->list (var-occs t)))) + +;; Returns the variables of the term t. +(define (Vars t) + (map Var (vars t))) + +;; Useful for debugging that two literals have different fresh variables. +(define (common-variables t1 t2) + (let ([h (var-occs t1)]) + (for/list ([(v n) (in-hash (var-occs t2))] + #:when (hash-has-key? h v)) + v))) + +;; Returns the set of variables *names* that appear in t1 but not in t2. +(define (variables-minus t1 t2) + (define h2 (var-occs t2)) + (for/list ([(v n) (in-hash (var-occs t1))] + #:unless (hash-has-key? h2 v)) + v)) + +;; Returns the lexicographical index of each occurrence of the variables, with a depth-first search. +(define (find-var-names t) + (define h (make-subst)) + (let loop ([t t] [idx 0]) + (cond [(pair? t) + (loop (cdr t) (loop (car t) idx))] + [(Var? t) + (subst-update! h t min idx) + (+ idx 1)] + [else idx])) + (map car (sort (subst->list h) < #:key cdr))) + +;; Returns '< if each variable of t1 appears no more times in t1 +;; than the same variable in t2, +;; and at least one variable appears strictly fewer times. +;; Returns '= if the occurrences are equal. +;; Returns #false otherwise. +;; This can be seen as a kind of Pareto dominance. +;; This is used for KBO in particular. +;; Note: (var-occs<=> t1 t2) == (var-occs<=> t2 t1) +;; Note: t1 and t2 may have variables in common if they are two subterms of the same clause. +(define (var-occs<=> t1 t2) + (define h1 (var-occs t1)) ; assumes does not contain 0s + (define h2 (var-occs t2)) ; assumes does not contain 0s + (define n-common 0) + (define cmp + (for/fold ([cmp '=]) + ([(v1 n1) (in-subst h1)]) + (define n2 (subst-ref/name h2 v1 0)) + (cond + [(> n2 0) + (++ n-common) + (define c (number<=> n1 n2)) + (cond [(eq? cmp '=) c] + [(eq? c '=) cmp] + [(eq? cmp c) c] + [else #false])] ; incomparable + [else cmp]))) + + (define n1 (subst-count h1)) + (define n2 (subst-count h2)) + (cond [(and (< n-common n1) + (< n-common n2)) + #false] + [(< n-common n2) + (case cmp [(< =) '<] [else #false])] + [(< n-common n1) + (case cmp [(> =) '>] [else #false])] + [else cmp])) + +;=====================; +;=== Boolean logic ===; +;=====================; + +(begin-encourage-inline + ;; Logical false + (define lfalse '$false) + (define (lfalse? x) (eq? lfalse x)) + ;; lfalse must be the bottom element for the various atom orders. + (define (lfalse<=> a b) + (define afalse? (lfalse? a)) + (define bfalse? (lfalse? b)) + (cond [(and afalse? bfalse?) '=] + [afalse? '<] + [bfalse? '>] + [else #false])) + + (define ltrue '$true) + (define (ltrue? x) (eq? x ltrue)) + + (define (lnot? lit) + (and (pair? lit) + (eq? 'not (car lit)))) + + ;; Inverses the polarity of the atom. + ;; NOTICE: Always use `lnot`, do not construct negated atoms yourself. + (define (lnot x) + (cond [(lnot? x) (cadr x)] + [(lfalse? x) ltrue] + [(ltrue? x) lfalse] + [else (list 'not x)])) + + (define (polarity<=> lit1 lit2) + (boolean<=> (lnot? lit1) (lnot? lit2))) + + ) + +;; Converse implication clause. Invert polarities if binary. +(define (converse cl) + (case (length cl) + [(1) ltrue] ; If A is a fact, then true => A, and thus converse is A => true == true + [(2) (map lnot cl)] + [else (error "Undefined converse for ~v" cl)])) + +;=================================; +;=== Literals, atoms, terms, … ===; +;=================================; + +#| +literal = atom | (not atom) +atom = constant | (predicate term ...) +term = (funtion term ...) | variable | constant +predicate = symbol? +function = symbol? +constant = symbol? +variable = (Var number?) + +For simplicity, we sometimes use 'term' to mean 'atom or term', or even +'literal, atom or tem'. +|# + +;; Returns the number of nodes in the tree representing the term t (or literal, atom). +(define (tree-size t) + (let loop ([t t] [s 0]) + (cond [(Var? t) (+ s 1)] + [(pair? t) + (loop (cdr t) (loop (car t) s))] + [else (+ s 1)]))) + +;; The literals are depolarized first, because negation should not count. +(define (literal-size lit) + (tree-size (depolarize lit))) + +;; In particular, it should be as easy to prove A | B as ~A | ~B, otherwise finding equivalences +;; can be more difficult. +(define (clause-size cl) + (for/sum ([lit (in-list cl)]) + (literal-size lit))) + +;; Returns < if for every substitution α, (atom1<=> t1α t2α) returns <. +;; (Can this be calculated given a base atom1<=> ?) +;; - Rk: variables of t2 that don't appear in t1 are not a problem since they are not instanciated +;; in t2α. +;; - Equality is loose and is based only on *some* properties of the atoms. +;; - This is a good first comparator, but not good enough (e.g., does not associativity) +;; Notice: (order=? (atom<=> t1 t2)) does NOT necessarily mean that t1 and t2 are syntactically equal. +(define (atom1<=> t1 t2) + (let ([t1 (depolarize t1)] + [t2 (depolarize t2)]) + (cond/else + [(lfalse<=> t1 t2)] ; continue if neither is lfalse + #:else + (define size (number<=> (tree-size t1) (tree-size t2))) + (define vs (var-occs<=> t1 t2)) + #:cond + [(and (order=? vs) (order=? size)) (or (term-lex2<=> t1 t2) '=)] ; for commutativity + [(and (order≤? vs) (order≤? size)) '<] ; one is necessarily '< + [(and (order≥? vs) (order≥? size)) '>] + #:else #false))) + +;; For KBO +;; fun-weight is also for constants, hence it's more like symbol-weight +;; (but the name 'function' is commonly used for constants too). +(define (term-weight t #:? [var-weight 1] #:? [fun-weight (λ (f) 1)]) + (let loop ([t t]) + (cond [(Var? t) var-weight] + [(symbol? t) (fun-weight t)] + [(list? t) (for/sum ([s (in-list t)]) (loop s))] + [else (error "Unknown term ~a" t)]))) + +;; Knuth-Bendix Ordering, naive version. +;; See "Things to know when implementing KB", Löchner, 2006. +;; var-weight MUST be ≤ to all fun-weights of constants. +;; Simple version for clarity and proximity to the specifications. +;; TODO: Implement a faster version +(define (make-KBO<=> #:? var-weight #:? fun-weight #:? [fun<=> symbol<=>]) + (define (weight t) + (term-weight t #:var-weight var-weight #:fun-weight fun-weight)) + + (define (KBO<=> t1 t2) + (cond + [(and (Var? t1) (Var? t2)) (and (Var=? t1 t2) '=)] ; not specified, but surely right? + [(Var? t1) (and (occurs? t1 t2) '<)] + [(Var? t2) (and (occurs? t2 t1) '>)] + [else ; both are fun apps or constants + (define v (var-occs<=> t1 t2)) + (and v + (let ([t-cmp (sub-KBO<=> (if (list? t1) t1 (list t1)) ; turn constants into fun apps. + (if (list? t2) t2 (list t2)))]) + (case v + [(<) (and (order<=? t-cmp) t-cmp)] + [(>) (and (order>=? t-cmp) t-cmp)] + [(=) t-cmp])))])) + + ;; t1 and t2 MUST be lists. + (define (sub-KBO<=> t1 t2) + (chain-comparisons + (number<=> (weight t1) (weight t2)) + (fun<=> (first t1) (first t2)) + ;; Chain on subterms. + (<=>map KBO<=> (rest t1) (rest t2)))) + + (λ (t1 t2) + (let ([t1 (depolarize t1)] + [t2 (depolarize t2)]) + (or (lfalse<=> t1 t2) + (KBO<=> t1 t2))))) + +(define KBO1lex<=> (make-KBO<=>)) + +;; Returns a literal like lit, but without negation if lit was negative. +(define (depolarize lit) + (match lit + [`(not ,x) x] + [else lit])) + +;; Returns the number of arguments of the predicate of the literal lit, after depolarizing it. +(define (literal-arity lit) + (let ([lit (depolarize lit)]) + (if (list? lit) + (length lit) + 0))) + +;; Returns the name of the predicate (or constant) of the literal. +(define (literal-symbol lit) + (match lit + [`(not (,p . ,r)) p] + [`(not ,a) a] + [`(,p . ,r) p] + [else lit])) + +;; Lexicographical comparison. +;; Guarantees: (order=? (term-lex<=> t1 t2)) = (term==? t1 t2) (but maybe a slightly slower?) +;; Warning: Doesn't handle variables that are not Var? properly +(define (term-lex<=> t1 t2) + (cond [(eq? t1 t2) '=] ; takes care of '() + [(and (pair? t1) (pair? t2)) + (chain-comparisons (term-lex<=> (car t1) (car t2)) + (term-lex<=> (cdr t1) (cdr t2)))] + [(pair? t1) '>] + [(pair? t2) '<] + [(and (Var? t1) (Var? t2)) + (Var<=> t1 t2)] + [(Var? t1) '<] + [(Var? t2) '>] + [(and (symbol? t1) (symbol? t2)) + (symbol<=> t1 t2)] + [else + (error 'term-lex<=> "Unknown term kind for: ~a, ~a" t1 t2)])) + +;; Can't compare vars with symbols, or vars with vars. Can only compare ground symbols: +;; A binary rule can't be oriented with variables +(define (term-lex2<=> t1 t2) + (cond [(eq? t1 t2) '=] ; takes care of '() + [(and (Var? t1) (Var? t2) (Var=? t1 t2)) '=] + [(or (Var? t1) (Var? t2)) #false] ; incomparable, cannot be oriented + [(and (pair? t1) (pair? t2)) + (chain-comparisons (term-lex2<=> (car t1) (car t2)) + (term-lex2<=> (cdr t1) (cdr t2)))] + [(pair? t1) '>] + [(pair? t2) '<] + [(and (symbol? t1) (symbol? t2)) + (symbol<=> t1 t2)] + [else + (error 'term-lex2<=> "Unknown term kind for: ~a, ~a" t1 t2)])) + +;; Depth-first lexicographical order (df-lex) +;; Guarantees: (order=? (literal<=> lit1 lit2)) = (literal==? lit1 lit2). (or it's a bug) +(define (literal<=> lit1 lit2) + (chain-comparisons + (polarity<=> lit1 lit2) + (symbol<=> (literal-symbol lit1) (literal-symbol lit2)) ; A literal cannot be a variable + (cond [(and (list? lit1) (list? lit2)) + ; this also checks arity + (<=>map term-lex<=> (rest lit1) (rest lit2))] + [(list? lit2) '<] + [(list? lit1) '>] + [else '=]))) + +(define (literal lit1 lit2))) + +;; This works because variables are transparent (prefab), hence equal? traverses the struct too. +;; We use `==` to denote syntactic equivalence. +(define term==? equal?) +(define literal==? equal?) + +;==================================; +;=== Substitution / Unification ===; +;==================================; + +;; Notice: Setting this to #true forces the mgu substitutions to ensure +;; dom(σ)\cap vran(σ) = ø +;; but can be exponentially slow in some rare cases. +;; Also, it's not necessary. +(define reduce-mgu? #false) + +(struct already-substed (term) #:prefab) + +;; Returns a term where the substitution s is applied to the term t. +(define (substitute t s) + (define t-orig t) + (let loop ([t t]) + (cond + [(null? t) t] + [(pair? t) + (cons (loop (car t)) + (loop (cdr t)))] + [(and (Var? t) + (subst-ref s t #false)) + ; Recur into the substitution. + ; This avoids recurring many times inside the same substitution. + => + (λ (rhs) + (cond [(already-substed? rhs) + ; No need to loop inside the new term. + (already-substed-term rhs)] + [else + (define new-rhs (loop rhs)) + (subst-set! s t (already-substed new-rhs)) + new-rhs]))] + [else t]))) + +;; v : variable name (symbol) +;; t : term +(define (occurs? V t) + (cond [(Var? t) (Var=? V t)] + [(pair? t) + (or (occurs? V (car t)) + (occurs? V (cdr t)))] + [else #false])) + +(define (occurs?/extend var t2 subst) + (define t2c (substitute t2 subst)) + (if (occurs? var t2c) + #false + (begin + (subst-set! subst var t2c) + subst))) + +;; Returns one most general unifier α such that t1α = t2α. +;; Assumes that the variables of t1 and t2 are disjoint, +;; so that occur-check is not needed. (really?) +;; TODO: In case left-unification is possible, does this return a left-unifier? +;; Can we also return a boolean saying whether this is the case? +(define (unify t1 t2 [subst (make-subst)]) + (define success? + (let loop ([t1 t1] [t2 t2]) + (cond/else + [(eq? t1 t2) ; takes care of both null? + subst] + [(and (pair? t1) (pair? t2)) + (and (loop (car t1) (car t2)) + (loop (cdr t1) (cdr t2)))] + #:else + (define v1? (Var? t1)) + (define v2? (Var? t2)) + #:cond + [(and (not v1?) (not v2?)) ; since they are not `eq?` + #false] + [(and v1? v2? (Var=? t1 t2)) ; since at least one is a Var + ; Same variable, no need to substitute, and should not fail occurs?/extend. + subst] + #:else + (define t1b (and v1? (subst-ref subst t1 #false))) + (define t2b (and v2? (subst-ref subst t2 #false))) + #:cond + [(or t1b t2b) + ; rec + (loop (or t1b t1) (or t2b t2))] + [v1? ; t2 may also be a variable + (occurs?/extend t1 t2 subst)] + [v2? ; v2? but not v1? + (occurs?/extend t2 t1 subst)] + #:else (void)))) + ; Make sure we return a most general unifier + ; NOTICE: This can take a lot of time (see strest tests), but may prevent issues too. + (and success? + (if reduce-mgu? + (let ([s2 (make-subst)]) + (for ([(k v) (in-subst subst)]) + (subst-set!/name s2 k (substitute v subst))) + s2) + subst))) + +(define (subst/#false->imsubst s) + (cond [(subst? s) + (subst->list s)] + [(list? s) + (sort (map (λ (p) (cons (Var-name (Varify (car p))) + (Varify (cdr p)))) + s) + Var-name