diff --git a/satore/Clause.rkt b/satore/Clause.rkt index 41e3de8..3a4abf2 100644 --- a/satore/Clause.rkt +++ b/satore/Clause.rkt @@ -23,14 +23,23 @@ ;==============; ;; TODO: A lot of space is wasted in Clause (boolean flags?) -;; What's the best way to gain space without losing time or readability? +;; TODO: What's the best way to gain space without losing time or readability? +;; idx : exact-nonnegative-integer? ; unique id of the Clause. ;; 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. +;; clause : clause? ; the list of literals. +;; type : symbol? ; How the Clause was generated (loaded from file, input clause, rewrite, resolution, +;; factor, etc.) +;; binary-rewrite-rule? : boolean? ; Initially #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). +;; candidate? : boolean? ; Whether the clause is currently a candidate (see `saturation` in +;; saturation.rkt). +;; discarded? : boolean? ; whether the Clause has been discarded (see `saturation` in saturation.rkt). +;; n-literals : exact-nonnegative-integer? ; number of literals in the clause. +;; size : number? ; tree-size of the clause. +;; depth : exact-nonnegative-integer? : Number of parents up to the input clauses, when following +;; resolutions and factorings. +;; cost : number? ; Used to sort Clauses in `saturation` (in saturation.rkt). (struct Clause (idx parents clause @@ -41,19 +50,26 @@ n-literals size depth - [cost #:mutable] - [g-cost #:mutable]) + [cost #:mutable]) #:prefab) +;; Unique clause index. No two Clauses should have the same index. (define-counter clause-index 0) +;; Clause constructor. See the struct Clause for more information. +;; +;; parents : (listof Clause?) +;; candidate? : boolean? +;; n-literals : exact-nonnegative-integer? +;; size : number? +;; depth : exact-nonnegative-integer? (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))))]) + #:? [type '?] + #:? [candidate? #false] + #:? [n-literals (length cl)] + #:? [size (clause-size cl)] + #:? [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 @@ -76,27 +92,38 @@ size depth ; depth (C0 is of depth 0, axioms are of depth 1) 0. ; cost - 0. ; g-cost )) +;; Sets the Clause as discarded. Used in `saturation`. +;; +;; Clause? -> void? (define (discard-Clause! C) (set-Clause-discarded?! C #true)) +;; A tautological clause used for as parent of the converse of a unit Clause. (define true-Clause (make-Clause (list ltrue))) -;; For temporary converse Clauses for binary clauses. -(define (make-converse-Clause C #:candidate? [candidate? #false]) +;; Returns a converse Clause of a unit or binary Clause. +;; These are meant to be temporary. +;; +;; C : Clause? +;; candidate? : boolean? +;; -> Clause? +(define (make-converse-Clause C #:? [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? - ))) + #:candidate? candidate?))) +;; List of possible fields for output formatting. (define Clause->string-all-fields '(idx parents clause type binary-rw? depth size cost)) +;; Returns a tree representation of the Clause, for human reading. ;; If what is a list, each element is printed (possibly multiple times). ;; If what is 'all, all fields are printed. +;; +;; Clause? (or/c 'all (listof symbol?)) -> list? (define (Clause->list C [what '(idx parents clause)]) (when (eq? what 'all) (set! what Clause->string-all-fields)) @@ -112,9 +139,15 @@ [(size) (~r (Clause-size C))] [(cost) (~r2 (Clause-cost C))]))) +;; Returns a string representation of a Clause. +;; +;; Clause? (or/c 'all (listof symbol?)) -> string? (define (Clause->string C [what '(idx parents clause)]) (string-join (Clause->list C what) " ")) +;; Returns a string representation of a Clause, for displaying a single Clause. +;; +;; Clause? (listof symbol?) -> string? (define (Clause->string/alone C [what '(idx parents clause)]) (when (eq? what 'all) (set! what Clause->string-all-fields)) @@ -123,6 +156,9 @@ what) " ")) +;; Outputs the Clauses `Cs` in a table for human reading. +;; +;; (listof Clause?) (or/c 'all (listof symbol?)) -> void? (define (print-Clauses Cs [what '(idx parents clause)]) (when (eq? what 'all) (set! what Clause->string-all-fields)) @@ -130,44 +166,60 @@ (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))) +;; Returns a substitution if C1 subsumes C2 and the number of literals of C1 is no larger +;; than that of C2, #false otherwise. +;; Indeed, even when the clauses are safely factored, there can still be issues, for example, +;; this prevents cases infinite chains such as: +;; p(A, A) subsumed by p(A, B) | p(B, A) subsumed by p(A, B) | p(B, C) | p(C, A) subsumed by… +;; Notice: This is an approximation of the correct subsumption based on multisets. +;; +;; Clause? Clause? -> (or/c #false subst?) +(define (Clause-subsumes C1 C2) + (and (<= (Clause-n-literals C1) (Clause-n-literals 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))) +;; Like Clause-subsumes but first takes the converse of C1. +;; Useful for rewrite rules. +;; +;; Clause? Clause? -> (or/c #false subst?) +(define (Clause-converse-subsumes C1 C2) + (and (<= (Clause-n-literals C1) (Clause-n-literals C2)) + (clause-subsumes (clause-converse (Clause-clause C1)) + (Clause-clause C2)))) +;; Clause? -> boolean? (define (unit-Clause? C) (= 1 (Clause-n-literals C))) +;; Clause? -> boolean? (define (binary-Clause? C) (= 2 (Clause-n-literals C))) +;; Clause? -> boolean? (define (Clause-tautology? C) (clause-tautology? (Clause-clause C))) +;; Returns whether C1 and C2 are α-equivalences, that is, +;; if there exists a renaming substitution α such that C1α = C2 +;; and C2α⁻¹ = C1. +;; +;; Clause? Clause? -> boolean? +(define (Clause-equivalence? C1 C2) + (and (Clause-subsumes C1 C2) + (Clause-subsumes C2 C1))) + +;================; +;=== Printing ===; +;================; + ;; 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. +;; +;; C : Clause? +;; dmax : number? +;; -> (treeof Clause?) (define (Clause-ancestor-graph C #:depth [dmax +inf.0]) (define h (make-hasheq)) (let loop ([C C] [depth 0]) @@ -180,6 +232,13 @@ (cons C (filter-map (λ (C2) (loop C2 (+ depth 1))) (Clause-parents C)))]))) +;; Like `Clause-ancestor-graph` but represented as a string for printing. +;; +;; C : Clause? +;; prefix : string? ; a prefix before each line +;; tab : string? ; tabulation string to show the tree-like structure +;; what : (or/c 'all (listof symbol?)) ; see `Clause->string` +;; -> string? (define (Clause-ancestor-graph-string C #:? [depth +inf.0] #:? [prefix ""] @@ -200,29 +259,51 @@ (loop P (+ d 1))))) str-out) +;; Like `Clause-ancestor-graph-string` but directly outputs it. (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) +;; Returns #true if C1 was generated before C2 +;; +;; Clause? Clause? -> boolean? +(define (Clause-age>= C1 C2) (<= (Clause-idx C1) (Clause-idx C2))) + +;=================; +;=== Save/load ===; +;=================; + +;; Saves the Clauses `Cs` to the file `f`. +;; +;; Cs : (listof Clause?) +;; f : file? +;; exists : symbol? ; see `with-output-to-file` +;; -> void? (define (save-Clauses! Cs f #:? exists) (save-clauses! (map Clause-clause Cs) f #:exists exists)) +;; Loads Clauses from a file. If `sort?` is not #false, Clauses are sorted by Clause-size. +;; The type defaults to `'load` and can be changed with `type`. +;; +;; f : file? +;; sort? : boolean? +;; type : symbol? +;; -> (listof Clause?) (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<=) + (sort Cs <= #:key Clause-size) Cs)) -(define (Clause-equivalence? C1 C2) - (and (Clause<=>-subsumes C1 C2) - (Clause<=>-subsumes C2 C1))) +;======================; +;=== Test utilities ===; +;======================; -;; Provides testing utilities. Use with `(require (submod "Clause.rkt" test))`. +;; Provides testing utilities. Use with `(require (submod satore/Clause test))`. (module+ test (require rackunit) (provide Clausify @@ -230,6 +311,9 @@ (define Clausify (compose make-Clause clausify)) + ;; Returns whether for every clause of Cs1 there is an α-equivalent clause in Cs2. + ;; + ;; (listof Clause?) (listof Clause?) -> any/c (define-check (check-Clause-set-equivalent? Cs1 Cs2) (unless (= (length Cs1) (length Cs2)) (fail-check "not =")) diff --git a/satore/clause-format.rkt b/satore/clause-format.rkt index 30cd2ef..eca1f32 100644 --- a/satore/clause-format.rkt +++ b/satore/clause-format.rkt @@ -6,7 +6,8 @@ ;;; In a separate file because of cyclic dependencies with "tptp.rkt" if in "clause.rkt" -(require racket/format +(require define2 + racket/format racket/list racket/pretty satore/clause @@ -16,19 +17,30 @@ (provide (all-defined-out)) +;; Returns a string representation of the clause. +;; +;; clause? -> string? (define (clause->string cl) ((if (*tptp-out?*) clause->tptp-string ~a) (Vars->symbols cl))) +;; Same as clause->string but pretty prints the result for better reading. +;; +;; clause? -> string? (define (clause->string/pretty cl) (pretty-format (Vars->symbols cl))) +;; clause? -> void? (define (print-clause cl) (displayln (clause->string cl))) -(define (print-clauses cls #:sort? [sort? #false]) +;; Prints the list of clauses in a table, possibly sothing them first. +;; +;; cls : (listof clause?) +;; sort? : boolean? +(define (print-clauses cls #:? [sort? #false]) (unless (empty? cls) (print-table (for/list ([cl (in-list (if sort? diff --git a/satore/clause.rkt b/satore/clause.rkt index f67b0a6..1a27b0b 100644 --- a/satore/clause.rkt +++ b/satore/clause.rkt @@ -33,25 +33,37 @@ (define-counter n-tautologies 0) +;; Returns a new clause where the literals have been sorted according to `literal (listof literal?) (define (sort-clause cl) (sort cl literal (listof literal?) (define (clause-normalize cl) ; fresh the variables just to make sure (fresh (safe-factoring (sort-clause cl)))) +;; Takes a tree of symbols and returns a clause, after turning symbol variables into `Var`s. ;; Used to turn human-readable clauses into computer-friendly clauses. -(define (clausify cl) - (clause-normalize (Varify cl))) +;; +;; tree? -> clause? +(define (clausify l) + (clause-normalize (Varify l))) +;; clause? -> boolean? (define (empty-clause? cl) (empty? cl)) -;; Definition of tautology: -;; cl is a tautology if all ground instances of cl contain an atom and its negation. +;; Returns whether the clause `cl` is a tautologie. +;; cl is a tautology if it contains the literals `l` and `(not l)`. ;; Assumes that the clause cl is sorted according to `sort-clause`. +;; +;; clause? -> boolean? (define (clause-tautology? cl) (define-values (neg pos) (partition lnot? cl)) (define pneg (map lnot neg)) @@ -73,26 +85,22 @@ #:else (error "uh?")))) (begin (++n-tautologies) #true))) -;; NOTICE: This does *not* rename the variables. +;; Returns the converse clause of `cl`. +;; Notice: This does *not* rename the variables. +;; +;; clause? -> clause? (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)))) - +;; Returns the pair of (predicate-symbol . arity) of the literal. +;; +;; literal? -> (cons/c symbol? exact-nonnegative-integer?) (define (predicate.arity lit) - (cond [(list? lit) (cons (first lit) (length lit))] - [else (cons lit 0)])) - + (let ([lit (depolarize lit)]) + (cond [(list? lit) (cons (first lit) (length lit))] + [else (cons lit 0)]))) +;; Several counters to keep track of statistics. (define-counter n-subsumes-checks 0) (define-counter n-subsumes-steps 0) (define-counter n-subsumes-breaks 0) @@ -102,20 +110,17 @@ (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). +;; θ-subsumption. Returns a (unreduced) most-general unifier θ such that caθ ⊆ cb, in the sense +;; of set inclusion. ;; Assumes vars(ca) ∩ vars(cb) = ∅. - +;; Note that this function does not check for multiset inclusion. A length check is performed in +;; Clause-subsumes?. +;; +;; clause? clause? -> subst? (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 + ; such that we can extend β to β' so that la β' = lb. (define cbtrie (make-trie #:variable? Var?)) (for ([litb (in-list cb)]) @@ -133,13 +138,13 @@ < #: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) + ; Abort when we have reached the step limit (when (= n-iter n-iter-max) ; if n-iter-max = 0 then no limit (++n-subsumes-breaks) (return #false)) @@ -147,17 +152,23 @@ (cond [(empty? groups) subst] [else - (define-values (lita litbs) (car+cdr (first groups))) + (define gp (first groups)) + (define lita (car gp)) + (define litbs (cdr gp)) (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)))])))) +;; Returns the shortest clause `cl2` such that `cl2` subsumes `cl`. +;; Since `cl` subsumes each of its factors (safe or unsafe, and in the sense of +;; non-multiset subsumption above), this means that `cl2` is equivalent to `cl` +;; (hence no information is lost in `cl2`, it's a 'safe' factor). ;; 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. +;; +;; clause? -> clause? (define (safe-factoring cl) (let/ec return (zip-loop ([(l x r) cl]) @@ -181,17 +192,29 @@ (attempt y x))) cl)) -(define (clause-equivalence? A B) - (and (clause-subsumes A B) - (clause-subsumes B A))) +;; Returns whether the two clauses subsume each other, +;; in the sense of (non-multiset) subsumption above. +;; +;; clause? clause? -> boolean? +(define (clause-equivalence? cl1 cl2) + (and (clause-subsumes cl1 cl2) + (clause-subsumes cl2 cl1))) -;==============; -;=== Saving ===; -;==============; +;=================; +;=== Save/load ===; +;=================; +;; Save the clauses `cls` to the file `f`. +;; +;; cls : (listof clause?) +;; f : file? +;; exists : symbol? ; See `with-output-to-file`. (define (save-clauses! cls f #:? [exists 'replace]) (with-output-to-file f #:exists exists (λ () (for-each writeln cls)))) +;; Returns the list of clauses loaded from the file `f`. +;; +;; file? -> (listof clause?) (define (load-clauses f) (map clausify (file->list f))) diff --git a/satore/interact.rkt b/satore/interact.rkt index 87cd02b..d3e038f 100644 --- a/satore/interact.rkt +++ b/satore/interact.rkt @@ -18,7 +18,7 @@ ;; 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) +;; TODO: variables one must use ! (where the second argument is evaled) (define-syntax (interact stx) (syntax-parse stx #:literals (list) @@ -83,6 +83,7 @@ [else (printf "Unknown command: ~a\n" cmd) (loop)]))))))])) +;; For manual testing in DrRacket (module+ drracket (define-namespace-anchor ns-anchor) ; optional, to use the eval command diff --git a/satore/json-output.rkt b/satore/json-output.rkt index 12cbf44..48d0794 100644 --- a/satore/json-output.rkt +++ b/satore/json-output.rkt @@ -10,6 +10,7 @@ (provide (all-defined-out)) +;; Correspondance with Eprover output values (define status-dict '((running . UNSPECIFIED_PROOF_STATUS) (refuted . REFUTATION_FOUND) @@ -18,6 +19,9 @@ (steps . STEP_LIMIT_REACHED) (saturated . COUNTER_SATISFIABLE))) +;; Take a result dictionary from `saturation` and returns a JSON string representation of it. +;; +;; dict? -> string? (define (saturation-result->json res) (define d (let* ([res (dict-remove res 'name)] @@ -32,6 +36,7 @@ ",\n " #:after-last "\n}")) +;; Simple visual test. (module+ drracket (define res '((name . "GEO170+1.p") diff --git a/satore/log.rkt b/satore/log.rkt index 4bd0457..1f61da1 100644 --- a/satore/log.rkt +++ b/satore/log.rkt @@ -23,15 +23,27 @@ (define-global:boolean *git?* #false "Commit to git if needed and include the last git commit hash in the globals.") +;; Calls thunk. Outputs to a log file if `log?` is not #false. +;; When `git?` is not #false, also commits to git to ensure consistency of the code base +;; with the experiment, and adds the git commit number to the global variables. +;; +;; thunk : thunk? +;; dir : path-string? +;; filename : string? +;; filepath : path-string? +;; log? : boolean? +;; git? : boolean? +;; quiet? : boolean? (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*)] + #:? [git? (*git?*)] #:? [quiet? #false]) - (when (*git?*) + (when git? (define cmd "git commit -am \".\" ") (displayln cmd) (system cmd)) @@ -41,7 +53,7 @@ ; Also write the last commit hash for easy retrieval. (pretty-write (list* `(cmd-line . ,(current-command-line-arguments)) - `(git-commit . ,(and (*git?*) + `(git-commit . ,(and git? (string-normalize-spaces (with-output-to-string (λ () (system "git rev-parse HEAD")))))) (globals->assoc))) diff --git a/satore/main.rkt b/satore/main.rkt index a2b404b..d649fe5 100755 --- a/satore/main.rkt +++ b/satore/main.rkt @@ -5,6 +5,10 @@ ;**** Satore ****; ;**************************************************************************************; +;;; Try: +;;; racket -l- satore --help +;;; to see all the available flags. + (module+ main (require global racket/file diff --git a/satore/misc.rkt b/satore/misc.rkt index 23bdd56..39b53c1 100644 --- a/satore/misc.rkt +++ b/satore/misc.rkt @@ -17,6 +17,7 @@ (provide (all-defined-out)) +;; Prints #true and #false (print-boolean-long-form #true) (define-syntax-rule (begin-for-both e) @@ -25,6 +26,7 @@ (begin-for-syntax e))) (begin-for-both + ;; (or/c string? symbol? number?) -> number? (define (debug-level->number lev) (cond [(number? lev) lev] @@ -43,10 +45,11 @@ debug-level->number '("--debug")) +;; ;; (or/c string? symbol? number?) -> boolean? (define (debug>= lev) (>= (*debug-level*) (debug-level->number lev))) -;; TODO: Make faster +;; Do a sequence of actions only when debug-level is greater than a given level. (define-syntax (when-debug>= stx) (syntax-case stx () [(_ lev body ...) @@ -54,11 +57,12 @@ #'(when (>= (*debug-level*) levv) body ...))])) +;; any/c -> boolean? (define (thunk? p) (and (procedure? p) (procedure-arity-includes? p 0))) -;; Defines a counter with a reset function and an increment function +;; Defines a counter with a reset function and an increment function. ;; Ex: ;; (define-counter num 0) ;; (++num) @@ -76,15 +80,19 @@ (define (++ [n 1]) (set! name (+ name n)))))])) +;; -> number? +(define (current-inexact-seconds) + (* 0.001 (current-inexact-milliseconds))) +;; -> exact-nonnegative-integere? (define (current-memory-use-MB) (arithmetic-shift (current-memory-use) -20)) -(define (car+cdr p) - (values (car p) (cdr p))) - +;; Prints `x` with a given precision if it is a rational, otherwise formants it with `~a`. +;; +;; x : any/c +;; precision : (or/c exact-nonnegative-integer? (list/c '= exact-nonnegative-integer?)) (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 index 036ecad..0e58ed4 100644 --- a/satore/rewrite-tree.rkt +++ b/satore/rewrite-tree.rkt @@ -44,10 +44,18 @@ ;====================; ;; atom<=> : comparator? -;; dynamic-ok? : whether we keep dynamic rules -;; rules-file : if not #false, loads rules from the given file +;; dynamic-ok? : boolean? ; whether we keep dynamic rules +;; rules-file : file? ; if not #false, loads rules from the given file (struct rewrite-tree trie (atom<=> dynamic?)) +;; rewrite-tree constructor. +;; +;; constructor: procedure? +;; atom<=> : comparator? +;; dynamic-ok? : boolean? +;; rules-file : file? +;; other-args : list? +;; -> rewrite-tree? (define (make-rewrite-tree #:? [constructor rewrite-tree] #:! atom<=> #:? [dynamic-ok? #true] @@ -67,6 +75,9 @@ ;; 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. +;; +;; rwtree : rewrite-tree? +;; -> rewrite-tree? (define (rewrite-tree-shallow-copy rwtree) (define new-rwtree (make-rewrite-tree #:atom<=> (rewrite-tree-atom<=> rwtree) #:dynamic-ok? (rewrite-tree-dynamic? rwtree))) @@ -74,6 +85,11 @@ (add-rule! new-rwtree rl)) new-rwtree) +;; Returns the list of values that match the literal t. +;; +;; rwtree : rewrite-tree? +;; t : any/c +;; -> list? (define (rewrite-tree-ref rwtree t) ; Node values are lists of rules, and trie-ref returns a list of node-values, ; hence the append*. @@ -85,6 +101,13 @@ ;; to-literal : light side ;; to-fresh : variables of to-literal not in from-literal that need to be freshed ;; after applying the rule +;; +;; Clause : Clause? +;; rule-group : rule-group? +;; from-literal? : literal? +;; to-literal? : literal? +;; to-fresh : unused +;; static? : boolean? (struct rule (Clause rule-group from-literal to-literal to-fresh static?) #:prefab) @@ -94,24 +117,55 @@ ;; 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. +;; +;; Clause : (or/c false/c Clause?) +;; Converse : Clause? +;; rules: (listof rule?) (struct rule-group (Clause Converse [rules #:mutable]) #:prefab) - +;; Rule constructor. +;; +;; C : Clause? +;; rule-gp : rule-group? +;; from : literal? +;; to : literal? +;; static? : boolean? +;; -> rule? (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?)) +;; Returns whether rule is a unit rule, that is, if the `to` literal +;; is either ltrue or lfalse. +;; +;; rl : rule? +;; -> any/c (define (unit-rule? rl) (memq (rule-to-literal rl) (list lfalse ltrue))) +;; Returns whether rl is a 'tautology', that is, if its `to` and `from` +;; literals are syntactically equal. +;; +;; rl : rule? +;; -> boolean? (define (rule-tautology? rl) (equal? (rule-from-literal rl) (rule-to-literal rl))) +;; Returns whether the rule is left linear, that is, if each variable +;; occurs at most once in the `from` literal. +;; +;; rl : rule? +;; -> boolean? (define (left-linear? rl) (define occs (var-occs (rule-from-literal rl))) (for/and ([(v n) (in-hash occs)]) (<= n 1))) +;; Returns whether rl1 subsumes rl2. +;; +;; rl1 : rule? +;; rl2 : rule? +;; -> any/c (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))) @@ -131,6 +185,12 @@ ;; 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. +;; +;; C : Clause? +;; Conv : Clause? +;; atom<=> : comparator? +;; dynamic-ok? : boolean? +;; -> (listof rule?) (define (Clause->rules C Conv #:! atom<=> #:? [dynamic-ok? #true]) (define cl (Clause-clause C)) (define unit? (unit-Clause? C)) @@ -155,7 +215,8 @@ #: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. @@ -165,6 +226,9 @@ rules) ;; a is left-unify< to b if a left-unifies with b. +;; +;; comparator? +;; literal? literal? -> (one-of '< '> '= #false) (define left-unify<=> (make<=> left-unify) ; left-unify is <=? ; equivalent to: #;(if (left-unify c1 c2) @@ -184,24 +248,32 @@ ;; 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. +;; +;; rl1 : rule? +;; rl2 : rule? +;; atom<=> : comparator? +;; -> (one-of '< '> '= #false) (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))) - +;; Returns a rule of rwtree that subsumes rl if any. +;; +;; rwtree : rewrite-tree? +;; rl : rule? +;; -> (or/c #false rule?) (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, +;; 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. +;; +;; rl : rule? +;; lit : literal? +;; -> literal? (define (rule-rewrite-literal rl lit) (define subst (left-unify (rule-from-literal rl) lit)) (cond [subst @@ -221,6 +293,10 @@ ;; (may contain duplicate rules). ;; lit: literal? ;; C: The Clause containing the literal lit. Used to avoid backward rewriting C to a tautology. +;; +;; rwtree : rewrite-tree? +;; lit : literal? +;; C : Clause? (define (binary-rewrite-literal rwtree lit C) (define atom<=> (rewrite-tree-atom<=> rwtree)) (let loop ([lit lit] [rules '()]) @@ -249,6 +325,10 @@ ;; 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. +;; +;; rwtree : rewrite-tree? +;; cl : clause? +;; C : Clause? (define (binary-rewrite-clause rwtree cl C) (let/ec return (for/fold ([lits '()] @@ -264,12 +344,17 @@ (define Clause-type-rw 'rw) +;; Clause? -> boolean? (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. +;; +;; rwtree : rewrite-tree? +;; C : Clause? +;; -> Clause? (define (binary-rewrite-Clause rwtree C) (define-values (new-cl rules) (binary-rewrite-clause rwtree (Clause-clause C) C)) (cond [(empty? rules) @@ -281,6 +366,11 @@ #:type Clause-type-rw)])) ;; Returns whether the clause cl would be rewritten. Does not perform the rewriting. +;; +;; rwtree : rewrite-tree? +;; cl : clause? +;; C : Clause? +;; -> boolean? (define (binary-rewrite-clause? rwtree cl C) (for/or ([lit (in-list cl)]) ; We need to perform the literal rewriting anyway, because @@ -289,11 +379,19 @@ (not (empty? new-rules)))) ;; Returns whether the Clause C would be rewritten. Does not perform the rewriting. +;; +;; rwtree : rewrite-tree? +;; C : Clause? +;; -> boolean? (define (binary-rewrite-Clause? rwtree C) (binary-rewrite-clause? rwtree (Clause-clause C) C)) ;; Unconditionally adds the rule rl to the rewrite-tree rwtree, ;; and removes from rwtree the rules that are subsumed by rl +;; +;; rwtree : rewrite-tree? +;; rl : rule? +;; -> void? (define (add-rule! rwtree rl) (define atom<=> (rewrite-tree-atom<=> rwtree)) (unless (or (rule-tautology? rl) @@ -309,8 +407,7 @@ #: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?) + ;; TODO: 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. @@ -327,18 +424,25 @@ ;; Unconditionally removes a single (oriented) rule from the tree. ;; Use with caution and see instead remove-rule-group!. +;; +;; rwtree : rewrite-tree? +;; rl : rule? +;; -> void? (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?) + ;; TODO: 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!). +;; +;; rwtree : rewrite-tree? +;; gp : rule-group? +;; -> void? (define (remove-rule-group! rwtree gp) (for ([rl (in-list (rule-group-rules gp))]) (remove-rule! rwtree rl))) @@ -349,6 +453,11 @@ ;; 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). +;; +;; rwtree : rewrite-tree? +;; C : Clause? +;; rewrite? : boolean? +;; -> void? (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?)) @@ -356,6 +465,12 @@ ;; 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). +;; +;; rwtree : rewrite-tree? +;; C : Clause? +;; Conv : Clause? +;; rewrite? : boolean? +;; -> void? (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? @@ -392,7 +507,7 @@ (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. + ; TODO: at the next saturation iteration. '()] [else (define atom<=> (rewrite-tree-atom<=> rwtree)) @@ -407,7 +522,7 @@ ; 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. + ; TODO: of conv. (set-Clause-binary-rewrite-rule?! C #true) rls]))])) @@ -419,35 +534,68 @@ ;; 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. +;; +;; rwtree : rewrite-tree? +;; Cs : (listof Clause?) +;; Conv : Clause? +;; rewrite? : boolean? +;; -> void? (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))) +;; Returns the list of rules (without duplicates) of rwtree. +;; +;; rwtree : rewrite-tree? +;; -> (listof rule?) (define (rewrite-tree-rules rwtree) (remove-duplicates (append* (trie-values rwtree)) eq?)) +;; Returns the list of rule groups (without duplicates) of rwtree. +;; +;; rwtree : rewrite-tree? +;; -> (listof rule-group?) (define (rewrite-tree-rule-groups rwtree) (remove-duplicates (map rule-rule-group (append* (trie-values rwtree))) eq?)) +;; Returns the list of unique Clauses that have been used to create the rules +;; held by the given rule groups. +;; +;; groups : (listof rule-group?) +;; -> (listof Clause?) (define (rule-groups-original-Clauses groups) (remove-duplicates (append (map rule-group-Clause groups) (map rule-group-Converse groups)) eq?)) +;; Returns the list of unique Clauses that have been used to create the rules. +;; +;; rules : (listof rule?) +;; -> (listof Clause?) (define (rules-original-Clauses rules) (rule-groups-original-Clauses (map rule-rule-group rules))) +;; Returns the list of unique Clauses that have been used to create the rules +;; of the rewrite tree. +;; +;; rwtree : rewrite-tree? +;; -> (listof Clause?) (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))) - +;; Returns the number of rules in the rewrite tree. +;; +;; rwtree : rewrite-tree? +;; -> exact-nonnegative-integer? (define (rewrite-tree-count rwtree) (length (rewrite-tree-rules rwtree))) ; not efficient +;; Returns a dictionary of statistics about the rewrite tree. +;; +;; rwtree : rewrite-tree? +;; -> list? (define (rewrite-tree-stats rwtree) (define rules (rewrite-tree-rules rwtree)) (define n-rules (length rules)) @@ -460,12 +608,14 @@ (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 +;; Notice: 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. +;; +;; rwtree : rewrite-tree? +;; -> void? (define (re-add-rules! rwtree) (define groups (rewrite-tree-rule-groups rwtree)) (for ([gp (in-list groups)]) @@ -479,6 +629,11 @@ ;===================; ;; Save the rules to file f (as clauses). +;; +;; rwtree : rewrite-tree? +;; rules-file : file? +;; exists : symbol? ; see `display-to-file`. +;; -> void? (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 @@ -503,6 +658,9 @@ (get-clause Conv)))))))) ;; Private. +;; +;; rules-file : file? +;; -> (listof Clause?) (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 @@ -521,7 +679,13 @@ (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. +;; Optionally: rewrites the rules before adding them +;; Returns the set of new rules. +;; +;; rwtree : rewrite-tree? +;; rules-file : file? +;; rewrite? : boolean? +;; -> (listof rule?) (define (load-rules! rwtree #:! rules-file #:? [rewrite? #true]) (define Crules (load-rule-Clause-lists #:rules-file rules-file)) (for/fold ([rules '()]) @@ -539,6 +703,10 @@ ;=======================; ;; Returns a new rwtree containing only the filtered rules +;; +;; rwtree : rewrite-tree? +;; proc : rule-group? -> boolean? +;; -> rewrite-tree? (define (filter-rule-groups rwtree proc) (define rwtree2 (make-rewrite-tree #:atom<=> (rewrite-tree-atom<=> rwtree) #:dynamic-ok? (rewrite-tree-dynamic? rwtree))) @@ -560,6 +728,11 @@ ;; 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. +;; +;; rwtree : rewrite-tree? +;; rl : rule? +;; bounded? : boolean? +;; -> (listof Clause?) (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)) @@ -591,6 +764,10 @@ ;; 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. +;; +;; rwtree : rewrite-tree? +;; C : Clause? +;; -> void? (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))) @@ -600,6 +777,10 @@ ;; 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. +;; +;; rwtree : rewrite-tree? +;; bounded? : boolean? +;; -> boolean? (define (rewrite-tree-confluence-step! rwtree #:? bounded?) (define rules (rewrite-tree-rules rwtree)) (for/fold ([any-change? #false]) @@ -612,11 +793,16 @@ ;; 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. +;; Notice: 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!. +;; +;; rwtree : rewrite-tree? +;; bounded? : boolean? +;; max-steps : exact-nonnegative-integer? +;; -> boolean? (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?)) @@ -629,11 +815,15 @@ ;=== Printing ===; ;================; +;; Returns a list representing the rule. +;; +;; rule? -> list? (define (rule->list rl) (cons (Clause-idx (rule-Clause rl)) (Vars->symbols (list (rule-from-literal rl) (rule-to-literal rl))))) +;; A comparator to sort the rules for printing (define display-rule<=> (make-chain<=> boolean<=> rule-static? boolean<=> unit-rule? @@ -643,12 +833,18 @@ number<=> (λ (r) (tree-size (rule-to-literal r))) length<=> rule-to-fresh)) +;; (listof rule?) -> (listof rule?) (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. +;; +;; rls : (listof rule?) +;; sort? : boolean? +;; positive-only? : boolean? +;; unit? : boolean? (define (rules->string rls #:? [sort? #true] #:? [positive-only? #false] #:? [unit? #true]) (string-join (for/list ([rl (in-list (if sort? (sort-rules rls) rls))] @@ -663,6 +859,12 @@ (rule-to-literal rl)))) "\n")) +;; Like rules->string but directly displays the result. +;; +;; rls : (listof rule?) +;; sort? : boolean? +;; positive-only? : boolean? +;; unit? : boolean? (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 index 280e8d0..41c25ba 100644 --- a/satore/saturation.rkt +++ b/satore/saturation.rkt @@ -114,26 +114,16 @@ (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. +;; 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`. +;; +;; rwtree-out : rewrite-tree? +;; C : Clause? +;; utree : unification-tree? (define (discover-new-rules! rwtree-out C utree) (cond/else [(not rwtree-out) '()] @@ -158,7 +148,7 @@ ;; 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)) + (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). @@ -166,7 +156,7 @@ (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))))) + (Clause-subsumes a Conv))))) #:cond [Subs ; We found a converse Clause in the active set, or a Clause that subsumes the @@ -188,7 +178,7 @@ ; 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))))) + (Clause-subsumes Conv a))))) #:cond [(not (empty? Subsd)) (when-debug>= steps @@ -197,14 +187,27 @@ ; 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 ? + ; TODO: Rename this to add-asymmetric-rules ? (rewrite-tree-add-binary-Clauses! rwtree-out Subsd C #:rewrite? #true)] #:else '())) -;=================; -;=== Cost/loss ===; -;=================; +;====================; +;=== Clause costs ===; +;====================; +;; Clause comparison for the cost queue. +;; +;; Clause? Clause? -> boolean? +(define (Candidate<= C1 C2) + (<= (Clause-cost C1) (Clause-cost C2))) + +;; Sets the cost of a list of Clauses that all have the same parent `parent`. +;; Some noise can be added to the cost via *cost-noise*. +;; +;; Cs : (listof Clause?) +;; cost-type: symbol? +;; parent : Clause? +;; -> void? (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. @@ -237,8 +240,13 @@ ;=== Saturation ===; ;==================; +;; List of possible status values. Used to prevent mistakes. (define statuses '(refuted saturated time memory steps running)) +;; Returns whether the result dictionary `res` has the status `status`. +;; +;; res : dict? +;; status : symbol? (define (check-status res status) (define res-status (dict-ref res 'status #false)) @@ -248,6 +256,25 @@ (eq? status res-status)) +;; The main algorithm. Saturates the formula given by the input clauses +;; by adding new clauses (either resolutions or factors) until either +;; the empty clause is produced, or a resource limit is reached (steps, time, memory). +;; +;; input-clauses : (listof clause?) +;; step-limit : number? +;; memory-limit : number? +;; cpu-limit : number? +;; rwtree : (or/c #false rewrite-tree?) +;; rwtree-out : (or/c #false rewrite-tree?) +;; backward-rewrite? : boolean? +;; parent-discard? : boolean? +;; age:cost : (list/c exact-nonnegative-integer? exact-nonnegative-integer?) +;; cost-type : symbol? +;; disp-proof? : boolean? +;; L-resolvent-pruning : boolean? +;; find-unit-rules-in-candidates? : boolean? +;; negative-literal-selection? : boolean? +;; -> dict? (define (saturation input-clauses #:? [step-limit +inf.0] #:? [memory-limit (*memory-limit*)] ; in MB @@ -287,7 +314,7 @@ ;; 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<=)) + (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)) @@ -345,7 +372,7 @@ (reset-n-L-resolvent-pruning!) (define start-time (current-milliseconds)) - ;; TODO: Some calls are slow... + ;; TODO: Some calls are very slow... (define (make-return-dict status [other '()]) (assert (memq status statuses) status) (define stop-time (current-milliseconds)) @@ -436,7 +463,7 @@ [(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. + ; TODO: This is somewhat defeated by the `priority` queue. age-queue] [else candidates])) (when-debug>= steps @@ -503,8 +530,8 @@ (discard-Clause! selected-Clause) (loop)] ; skip clause ;; FORWARD SUBSUMPTION - [(utree-find/any utree selected-Clause Clause<=-subsumes) - ;; TODO: TESTS + [(utree-find/any utree selected-Clause Clause-subsumes) + ;; TODO: Tests => (λ (C2) (++ n-forward-subsumed) @@ -515,7 +542,7 @@ ;; Clause is being processed. ;; BACKWARD SUBSUMPTION - (define removed (utree-inverse-find/remove! utree selected-Clause Clause<=-subsumes)) + (define removed (utree-inverse-find/remove! utree selected-Clause Clause-subsumes)) (for-each discard-Clause! removed) (+= n-backward-subsumed (length removed)) @@ -554,7 +581,7 @@ ; 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. + ;; TODO: 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)]) @@ -612,7 +639,7 @@ (when rwtree-out (for ([C (in-list new-Candidates)]) (when (unit-Clause? C) - ;; WARNING: Should be calling/merged with discover-rules! to avoid inconsistencies + ;; TODO: 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) @@ -634,6 +661,8 @@ ;=== User interaction ===; ;========================; +;; Some commands to use with '--debug interact'. Type 'help' for information. + (define interact-commands '()) (define-namespace-anchor ns-anchor) @@ -681,6 +710,12 @@ "Save the binary rules from the default rules-file" (save-rules! rwtree)]))) +;; Prints the set of active Clauses (held in utree). +;; +;; utree : unification-tree? +;; long? : boolean? +;; what : (or/c 'all (listof symbol?)) +;; -> void? (define (print-active-Clauses utree long? [what 'all]) (define actives (unification-tree-Clauses utree)) (printf "#active clauses: ~a\n" (length actives)) @@ -688,6 +723,9 @@ (displayln "Active clauses:") (print-Clauses (sort actives < #:key Clause-idx) what))) +;; Prints the set of binary rules. +;; +;; rewrite-tree? boolean? -> void? (define (print-binary-rules rwtree long?) (define rules (rewrite-tree-rules rwtree)) (printf "#binary rules: ~a #original clauses: ~a\n" @@ -700,8 +738,10 @@ ;=== Iterative saturation ===; ;============================; +;; A struct holding information about a given input formula. (struct problem (file name clauses [time-used #:mutable] [last-time #:mutable])) +;; file? (or/ #false string?) (listof clause?) -> problem? (define (make-problem file name clauses) (problem file name clauses 0 0)) @@ -716,11 +756,19 @@ ;; 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. +;; +;; problems : (listof problem?) +;; saturate : procedure? +;; memory-limit : number? +;; cpu-limit : number? +;; cpu-first-limit : number? +;; cpu-limit-factor? : number? +;; -> void? (define (iterative-saturation/problem-set problems saturate #:! memory-limit - #:! cpu-first-limit ; in seconds #:! cpu-limit ; in second + #:! cpu-first-limit ; in seconds #:! cpu-limit-factor) ; in seconds (define n-problems (length problems)) (define n-attempted 0) @@ -808,8 +856,17 @@ ;; ;; NOTICE: In this mode the unit rewrites are gathered only for the next round, but this is ;; likely not necessary! +;; +;; saturate : procedure? +;; tptp-program : string? +;; rwtree-in : rewrite-tree? +;; discover-online? : boolean? +;; cpu-limit : number? +;; cpu-first-limit : number? +;; cpu-limit-factor? : number? +;; -> void? (define (iterative-saturation saturate - #:! tptp-program ; string? + #:! tptp-program #:! rwtree-in #:? [discover-online? (*discover-online?*)] #:? [cpu-limit (*cpu-limit*)] diff --git a/satore/tests/Clause.rkt b/satore/tests/Clause.rkt index 4989605..44e50b0 100644 --- a/satore/tests/Clause.rkt +++ b/satore/tests/Clause.rkt @@ -1,12 +1,22 @@ #lang racket/base -(require rackunit - "../Clause.rkt" - (submod "../Clause.rkt" test)) +(require racket/list + rackunit + (submod satore/Clause test) + satore/Clause + satore/unification) ;; 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)]))) +(check-equal? (Clause-size (make-Clause '[p q])) + (Clause-size (make-Clause '[(not p) q]))) -;; TODO: test (check-Clause-set-equivalent? Cs1 Cs2) +(let () + (define Cs1 (map Clausify '([(p A B) (p B C) (p D E)] + [(q A B C) (q B A C)] + [(r X Y)]))) + (define Cs2 (shuffle (map (λ (C) (make-Clause (fresh (Clause-clause C)))) Cs1))) + (check-Clause-set-equivalent? Cs1 Cs2) + (check-Clause-set-equivalent? Cs2 Cs1)) diff --git a/satore/tests/clause.rkt b/satore/tests/clause.rkt index 8cc8558..821c280 100644 --- a/satore/tests/clause.rkt +++ b/satore/tests/clause.rkt @@ -2,11 +2,11 @@ (require global racket/dict - rackunit racket/list - "../clause.rkt" - "../misc.rkt" - "../unification.rkt") + rackunit + satore/clause + satore/misc + satore/unification) (*subsumes-iter-limit* 0) @@ -28,18 +28,6 @@ ) (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] ) @@ -98,23 +86,22 @@ (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)))) + (Varify + `((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))) - ) + (sort-clause (fresh (left-substitute cl (hasheq (symbol->Var-name 'X) 'bc + (symbol->Var-name 'Y) 'a1b1))))) + (check-not-false (clause-subsumes cl cl2)))) #; (begin @@ -122,12 +109,11 @@ ; 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). + ; 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)]))) - ) + (clausify '[(p a a) (p b b) (q C C)])))) (begin diff --git a/satore/tests/confluence.rkt b/satore/tests/confluence.rkt index 501a24c..ed1384b 100644 --- a/satore/tests/confluence.rkt +++ b/satore/tests/confluence.rkt @@ -1,7 +1,6 @@ #lang racket/base -(require (for-syntax racket/base - syntax/parse) +(require (for-syntax racket/base syntax/parse) bazaar/debug define2 define2/define-wrapper @@ -9,12 +8,12 @@ racket/list racket/pretty rackunit - "../Clause.rkt" - "../clause.rkt" - "../clause-format.rkt" - "../rewrite-tree.rkt" - "../unification.rkt" - (submod "../Clause.rkt" test)) + (submod satore/Clause test) + satore/Clause + satore/clause + satore/clause-format + satore/rewrite-tree + satore/unification) (define-global:boolean *dynamic-ok?* #true "Use dynamic rules?") diff --git a/satore/tests/interact.rkt b/satore/tests/interact.rkt index d51091d..a607150 100644 --- a/satore/tests/interact.rkt +++ b/satore/tests/interact.rkt @@ -3,7 +3,7 @@ (require racket/list racket/port rackunit - "../interact.rkt") + satore/interact) (define-syntax-rule (check-interact in out args ...) (check-equal? diff --git a/satore/tests/misc.rkt b/satore/tests/misc.rkt index 7b86736..6131965 100644 --- a/satore/tests/misc.rkt +++ b/satore/tests/misc.rkt @@ -1,5 +1,13 @@ #lang racket/base -(require "../misc.rkt" - rackunit) +(require rackunit + satore/misc) +(define-counter num 0) +(check-equal? num 0) +(++num) +(check-equal? num 1) +(++num 3) +(check-equal? num 4) +(reset-num!) +(check-equal? num 0) diff --git a/satore/tests/rewrite-tree.rkt b/satore/tests/rewrite-tree.rkt index dd22490..f19592d 100644 --- a/satore/tests/rewrite-tree.rkt +++ b/satore/tests/rewrite-tree.rkt @@ -2,17 +2,17 @@ (require bazaar/debug (except-in bazaar/order atom<=>) - racket/list racket/file + racket/list racket/pretty racket/random rackunit - "../Clause.rkt" - "../clause.rkt" - "../misc.rkt" - "../rewrite-tree.rkt" - "../unification.rkt" ; for atom1<=> - (submod "../Clause.rkt" test)) + (submod satore/Clause test) + satore/Clause + satore/clause + satore/misc + satore/rewrite-tree + satore/unification) (*debug-level* 0) diff --git a/satore/tests/saturation.rkt b/satore/tests/saturation.rkt index a922bc2..d33b264 100644 --- a/satore/tests/saturation.rkt +++ b/satore/tests/saturation.rkt @@ -1,19 +1,18 @@ #lang racket/base -(require (for-syntax syntax/parse - racket/base) +(require (for-syntax racket/base syntax/parse) 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") + rackunit + (prefix-in sat: satore/saturation) + satore/clause + satore/misc + satore/rewrite-tree + satore/unification + syntax/parse/define) (define-global *cpu-limit* 10 "Time limit in seconds for tests" @@ -113,8 +112,8 @@ 'status) 'saturated) - ;; WARNING (TODO): If L-resolvents-pruning applied to input clauses too, - ;; it would discard the 2nd clause immediately and would saturate! + ;; To do: 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)] @@ -254,26 +253,7 @@ (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)))) + ;; TODO: Same test but with rules loaded from a file ;; Greedy selection of binary rewrites can lead to failure (replay-on-failure diff --git a/satore/tests/stress-test1.rkt b/satore/tests/stress-test1.rkt index d8b7b02..ed9b3b9 100644 --- a/satore/tests/stress-test1.rkt +++ b/satore/tests/stress-test1.rkt @@ -1,7 +1,7 @@ #lang racket/base -(require "../clause.rkt" - "../unification.rkt") +(require satore/clause + satore/unification) (define cms current-milliseconds) diff --git a/satore/tests/trie.rkt b/satore/tests/trie.rkt index dc780dd..6508bf3 100644 --- a/satore/tests/trie.rkt +++ b/satore/tests/trie.rkt @@ -1,9 +1,9 @@ #lang racket/base -(require "../trie.rkt" +(require racket/pretty rackunit - (only-in "../unification.rkt" symbol-variable?) - racket/pretty) + satore/trie + (only-in satore/unification symbol-variable?)) (let ([atrie (make-trie #:variable? symbol-variable?)]) (trie-set! atrie @@ -28,8 +28,7 @@ '(C)) (check-equal? (trie-ref atrie '(a (f (g Y)) (f Y) c)) '(A)) - #;(pretty-print (trie-root atrie)) - #;(displayln (trie-values atrie)) + (check-equal? (sort (trie-values atrie) symbol-subsumes)) + (utree-inverse-find/remove! utree C Clause-subsumes)) (define (make-utree1) (define utree (make-unification-tree)) diff --git a/satore/tests/unification.rkt b/satore/tests/unification.rkt index c05568e..b606b64 100644 --- a/satore/tests/unification.rkt +++ b/satore/tests/unification.rkt @@ -3,7 +3,18 @@ (require (submod bazaar/order test) racket/match rackunit - "../unification.rkt") + satore/unification) + +(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-namesymbol (symbol->Var-name 'C)) 'C) (check-eq? (Var-name->symbol (symbol->Var-name 'X0)) 'X0) @@ -312,7 +323,7 @@ '(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), + ; 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) @@ -330,7 +341,7 @@ (test-left-unify '(p a) '(p a) '()) - (test-left-unify '(p A X) ;; WARNING + (test-left-unify '(p A X) '(p X Y) #false)) diff --git a/satore/tptp.rkt b/satore/tptp.rkt index 52f1b9a..46f53a6 100644 --- a/satore/tptp.rkt +++ b/satore/tptp.rkt @@ -30,7 +30,10 @@ File formats: |# - +;; Reads a .p file and returns a list of clauses. +;; +;; program-file : file? +;; -> (listof clause?) (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. @@ -38,6 +41,7 @@ File formats: ; but that will file if the cnf(…) is multiline. (tptp-prog->clauses (file->string program-file))) +;; Helper function (define (tptp-pre-clauses->clauses pre-clauses) (define clauses (for/list ([cl (in-list pre-clauses)]) @@ -61,7 +65,10 @@ File formats: [else (error "Unrecognized token: " t)])))) (map (compose clausify symbol-variables->Vars) clauses)) -;; Prolog .p program to rkt format +;; Reads the .p program given as a string and returns a list of clauses. +;; +;; str : string? +;; -> (listof clause?) (define (tptp-prog->clauses str) ; hardly tested and not strict enough @@ -84,7 +91,7 @@ File formats: 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) + '[#px"\\bnot\\b" "_not_"] ;; To do: Use $not for `lnot` instead? (as in TPTP) (map (λ (p) (list (regexp-quote (first p)) (string-append " " (regexp-replace-quote (second p)) " "))) '(["|" "" ] @@ -101,8 +108,11 @@ File formats: ;; Simple parser for the proposer output into s-exp clauses. ;; The format is expected to be in cnf. +;; +;; str : string? +;; -> (listof clause?) (define (tptp-string->clauses str) - ; TODO: Optimize. This can be veeeery slow for large conjectures. + ; To do: Optimize. This can be very slow for large conjectures. (define pre-clauses (append* ; split first to avoid regenerating the whole string after each substitution? @@ -114,7 +124,7 @@ File formats: (regexp-replaces str (list* - '[#px"\\bnot\\b" "_not_"] ;; WARNING!!! Instead: replace lnot with $not (as TPTP) + '[#px"\\bnot\\b" "_not_"] ;; To do: use $not for `lnot` instead? (as TPTP) (map (λ (p) (list (regexp-quote (first p)) (string-append " " (regexp-replace-quote (second p)) " "))) '(["|" ""] @@ -123,7 +133,10 @@ File formats: ["'" "\""]))))))))) (tptp-pre-clauses->clauses pre-clauses)) - +;; Returns a string representing the literal lit. +;; +;; lit : literal? +;; -> string? (define (literal->tptp-string lit) (cond [(lnot? lit) @@ -138,15 +151,26 @@ File formats: [(Var? lit) (symbol->string (Var-name->symbol lit))] [else (format "~a" lit)])) +;; Returns a string representing the clause cl. +;; +;; cl : clause? +;; ->string? (define (clause->tptp-string cl) (string-join (map literal->tptp-string (Vars->symbols cl)) " | ")) +;; Returns a string representing the clauses cls. +;; +;; cls : (listof clause?) +;; -> string? (define (clauses->tptp-string cls) (string-join (map clause->tptp-string cls) "\n")) ;; String replacement of tptp names with shorter ones to improve readability +;; +;; str : string? +;; -> string? (define (tptp-shortener str) (define substs (sort @@ -195,6 +219,8 @@ File formats: (string-replace line from to #:all? #true))) "\n")) +;; Helper: Surround any printing operation with this macro +;; to automatically replace the output with shortened names. (define-syntax-rule (with-tptp-shortener body ...) (let ([str (with-output-to-string (λ () body ...))]) (displayln (tptp-shortener str)))) diff --git a/satore/trie.rkt b/satore/trie.rkt index d958b01..3a896f9 100644 --- a/satore/trie.rkt +++ b/satore/trie.rkt @@ -4,12 +4,23 @@ ;**** Trie: Imperfect Discrimination Tree ****; ;***************************************************************************************; -;;; A key is a tree (a list of lists of ...), which is flattened to a list +;;; A discrimination tree is like a hashtable where the key is a list of elements. +;;; The keys are organized in a tree structure so that to retrieving an object +;;; takes at most O(A×l) steps, where l is the length of the key and A is the size of +;;; the alphabet. In practice it will be closer to O(l) since a hash table is used +;;; at each node to store the branches. +;;; +;;; A key is a actually 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?`. +;;; +;;; An imperfect discrimination tree does not differentiate variable names. +;;; Hence p(X Y) is stored in the same node as p(A A). An additional tests +;;; is required to tell them apart. (require bazaar/cond-else + define2 racket/list racket/match satore/misc) @@ -24,7 +35,8 @@ (define sublist-begin (string->uninterned-symbol "<<")) (define sublist-end (string->uninterned-symbol ">>")) -;; edges: hasheq(key . node?) +;; edges : hasheq(key . node?) +;; value : any/c (struct trie-node (edges value) #:transparent #:mutable) @@ -32,17 +44,32 @@ (trie-node (make-hasheq) no-value)) ;; Trie structure with variables. +;; +;; root : trie-node? +;; variable? : any/c -> boolean? (struct trie (root variable?)) -(define (make-trie #:constructor [constructor trie] - #:variable? [variable? (λ (x) #false)] +;; Trie constructor. +;; +;; constructor : procedure? +;; variable? : any/c -> boolean? +;; other-args : (listof any/c) +;; -> trie? +(define (make-trie #:? [constructor trie] + #:? [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 +;; Updates the value of the node for the given key (or sets one if none exists). +;; If default-val/proc is a procedure of arity 0, then it is applied to produce the +;; default value when requested, otherwise default-val/proc is used itself as the +;; default value. +;; +;; atrie : trie? +;; key : any/c +;; update : any/c -> any/c +;; default-val/proc : (or/c thunk? any/c) +;; -> void? (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. @@ -69,17 +96,32 @@ (define nd2 (hash-ref! edges k make-node)) (node-insert! nd2 (cdr key)))))) -;; Keep a list of values at the leaves. +;; Keeps a list of values at the leaves. ;; If `trie-insert!` is used, any use of `trie-update!` should be consistent with values being lists. +;; +;; atrie : trie? +;; key : any/c +;; val : any/c +;; -> void? (define (trie-insert! atrie key val) (trie-update! atrie key (λ (old) (cons val old)) '())) ;; Replacing the current value (if any) for key with val. +;; +;; atrie : trie? +;; key : any/c +;; val : any/C (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. +;; `on-leaf` may be effectful. +;; +;; atrie : trie? +;; key : any/c +;; on-leaf : trie-node? -> any +;; -> void? (define (trie-find atrie key on-leaf) (define variable? (trie-variable? atrie)) (let node-ref ([nd (trie-root atrie)] [key (list key)]) @@ -112,8 +154,12 @@ ;; 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) +;; `on-leaf` may be effectful. +;; +;; atrie : trie? +;; key : any/c +;; on-leaf : trie-node -> any/c +;; -> void? (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]) @@ -152,7 +198,12 @@ ;; 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. +;; `on-leaf` may be effectful. +;; +;; atrie : trie? +;; key : any/c +;; on-leaf : trie-node? -> any +;; -> void? (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]) @@ -196,7 +247,7 @@ (when nd2 (node-find nd2 (cdr key) 0))))) - +;; Helper function (define ((make-proc-tree-ref proc) atrie key) (define res '()) (proc atrie @@ -206,11 +257,20 @@ ;; 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 +;; These functions do not have side effects. +;; +;; Each function takes as input: +;; atrie : trie? +;; key : any/c +;; -> list? (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)) +;; Returns the list of all values in all nodes. +;; +;; atrie : trie? +;; -> list? (define (trie-values atrie) (let loop ([nd (trie-root atrie)] [res '()]) (define edges (trie-node-edges nd)) diff --git a/satore/unification-tree.rkt b/satore/unification-tree.rkt index 7f5509f..c9f7a74 100644 --- a/satore/unification-tree.rkt +++ b/satore/unification-tree.rkt @@ -7,19 +7,10 @@ ;;; 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. +;;; TODO: major difference with the trie is that we are dealing with Clauses, which +;;; TODO: are lists of literals, and the same Clause can appear in different leaves +;;; TODO: of the trie. Unification is only one of the operations performed on Clauses. (require bazaar/cond-else bazaar/debug @@ -42,8 +33,12 @@ (module+ test (require rackunit)) -;; WARNING: This cannot be applied to input clauses. -;; WARNING: To pass Russell's problem, we must +;; Experimental. +;; Based on "A Unifying Principle for Clause Elimination in First-Order Logic", +;; by Kiesl, Benjamin and Suda, Martin, CADE 26, 2017. +;; +;; Notice: This cannot be applied to input clauses. +;; Notice: 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. @@ -57,20 +52,21 @@ ;=== 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). +;; A unification tree is simply a discrimination tree where trie-node-values +;; are lists of `utree-leaf`. (struct unification-tree trie () #:transparent) +;; A leaf value. ;; 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) - +;; Returns a new unification tree (or a substruct). +;; +;; constructor : procedure? +;; other-args : list? +;; -> unification-tree? (define (make-unification-tree #:constructor [constructor unification-tree] . other-args) (apply make-trie @@ -78,25 +74,33 @@ #:variable? Var? other-args)) +;; Inserts a Clause into the unification tree. ;; 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`. +;; Notice: 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. +;; +;; unification-tree? Clause? -> void? (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)))) +;; Returns the list of unique Clauses present in the utree. +;; +;; unification-tree? -> (listof 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. +;; 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. +;; +;; utree : unification-tree? +;; lit : literal? ;; on-unified : utree-leaf? subst lit1 lit2 other-lit2s -> void? +;; -> void? (define (find-unifiers utree lit on-unified) (trie-both-find utree lit (λ (nd) @@ -114,6 +118,8 @@ ;; 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. +;; +;; unification-tree? literal? -> (listof Clause?) (define (unification-tree-ref utree lit) ; Node values are lists of rules, and trie-ref returns a list of node-values, ; hence the append*. @@ -133,7 +139,17 @@ (unless (Clause-tautology? new-C) (cons! new-C new-Clauses)))))) - +;; Resolves the Clause `C` with all the Clauses in `utree` and returns the list of resolvents. +;; Uses negative literal selection based on `literal-cost`: +;; If `C` has at least one negative literal, the costliest one is selected using `literal-cost`, +;; and only this literal is used for resolution with other Clauses. +;; The resolvents are immediately rewritten with `rewriter`. +;; +;; utree : unification-tree? +;; C : Clause? +;; rewriter : Clause? -> Clause? +;; literal-cost : literal? -> number? +;; -> (listof Clause?) (define (utree-resolve/select-literal utree C #:? [rewriter (λ (C) C)] #:? [literal-cost literal-size]) @@ -176,6 +192,12 @@ (values resolvents (+ 1 lit-idx))]))) +;; Returns the list of unsafe factors of `C`. +;; Factors are immediately rewritten with `rewriter`. +;; +;; C : Clause? +;; rewriter : Clause? -> Clause? +;; -> (listof Clause?) (define (unsafe-factors C #:? [rewriter (λ (C) C)]) (define-add-Clause! C factors add-Clause! rewriter) (define cl (Clause-clause C)) @@ -195,6 +217,13 @@ '())))) factors) +;; Appends and returns the results of `unsafe-factors` and `utree-resolve/select-literal`. +;; +;; utree : unification-tree? +;; C : Clause? +;; rewriter : Clause? -> Clause? +;; literal-cost : literal? -> number? +;; -> (listof Clause?) (define (utree-resolve+unsafe-factors/select utree C #:? rewriter #:? literal-cost) (rev-append (unsafe-factors C #:rewriter rewriter) @@ -202,9 +231,17 @@ #:rewriter rewriter #:literal-cost literal-cost))) -;; TODO: Deactivate rewriting inside add-candidates! +;; Like `utree-resolve+unsafe-factors/select` but without negative literal selection, +;; and with L-resolvent pruning. ;; Returns the set of Clauses from resolutions between cl and the clauses in utree, -;; as well as the factors +;; as well as the factors. +;; Clauses are immediately rewritten with `rewriter`. +;; +;; utree : unification-tree? +;; C : Clause? +;; rewriter : Clause? -> Clause? +;; L-resolvent-pruning? : boolean? +;; -> (listof Clause?) (define (utree-resolve+unsafe-factors utree C #:? [rewriter (λ (C) C)] #:! L-resolvent-pruning?) @@ -262,8 +299,12 @@ (+ 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, +;; there is a literal of C2 that imperfectly matches a literal of C, ;; and (pred C C2). +;; +;; utree : unification-tree? +;; C2 : Clause? +;; pred : Clause? Clause? -> boolean? (define (utree-find/any utree C2 pred) (define tested (make-hasheq)) ; don't test the same C2 twice (define cl2 (Clause-clause C2)) @@ -284,6 +325,10 @@ #false)) ;; Return all Clauses C that left-subunify on at least one literal and for which (pred C C2). +;; +;; utree : unification-tree? +;; C2 : Clause? +;; pred : Clause? Clause? -> boolean? (define (utree-find/all utree C2 pred) (define tested (make-hasheq)) ; don't test the same C2 twice (define cl2 (Clause-clause C2)) @@ -304,6 +349,9 @@ res) ;; Removes the Clause C from the utree. +;; +;; utree : unification-tree? +;; C : Clause? (define (utree-remove-Clause! utree C) (define cl (Clause-clause C)) (for ([lit (in-list cl)]) @@ -318,6 +366,9 @@ ;; 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. +;; +;; utree : unification-tree? +;; C2 : Clause? ;; pred: Clause? Clause? -> boolean (define (utree-inverse-find/remove! utree C pred) ; Since the same Clause may match multiple times, diff --git a/satore/unification.rkt b/satore/unification.rkt index 489de88..1feeae4 100644 --- a/satore/unification.rkt +++ b/satore/unification.rkt @@ -4,8 +4,12 @@ ;**** Operations On Literals: Unification And Friends ****; ;***************************************************************************************; +;;; * A literal A unifies with a literal B iff there exists a substitution σ s.t. Aσ = Bσ. +;;; * A literal A left-unifies (= matches) with a literal B iff there exists a substitution +;;; σ s.t. Aσ = B. +;;; Note that left-unifies => unifies. + (require bazaar/cond-else - bazaar/debug bazaar/list bazaar/mutation (except-in bazaar/order atom<=>) @@ -37,9 +41,11 @@ ;=== Variables ===; ;=================; +;; The name of a variable is a number. (struct Var (name) #:prefab) +;; Comparisons between variables (begin-encourage-inline (define Var-name v1 v2) (Var-name<=> (Var-name v1) (Var-name v2))) -; (order=? (Var<=> v1 v2)) = (Vars=? v1 v2) +; Ensures: (order=? (Var<=> v1 v2)) = (Vars=? v1 v2) ;:::::::::::::::::::::::::::::::::::; ;:: Basic operations on Variables ::; ;:::::::::::::::::::::::::::::::::::; ;; All symbols starting with a capitale letter are considered as variables. +;; +;; any/c -> boolean? (define (symbol-variable? t) (and (symbol? t) (char<=? #\A (string-ref (symbol->string t) 0) #\Z))) +;; Returns a variable 'name' corresponding to the given symbol. +;; Currently accepts only symbols like X1, X2, … and A, B, C, … ;; The same symbol is always mapped to the same Var-name, globally. +;; +;; symbol? -> exact-nonnegative-integer? (define (symbol->Var-name s) (define str (symbol->string s)) (cond [(regexp-match #px"^X(\\d+)$" str) @@ -70,7 +82,10 @@ [else (error 'Varify "Unknown variable format: ~a" s)])) +;; Inverse operation of symbol->Var-name. ;; The same Var-name is always mapped to the same symbol, globally. +;; +;; exact-nonnegative-integer? -> symbol? (define (Var-name->symbol n) (cond [(symbol-variable? n) n] [(number? n) @@ -80,6 +95,9 @@ [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. +;; Notice: Does *not* ensure unicity of the variables across clauses. +;; +;; tree? -> atom? (define (Varify t) (cond [(pair? t) ; Works also in assocs @@ -89,32 +107,15 @@ (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" =?)])) - +;; Basic substitution operations. +;; Simply put, a substitution is a `hasheqv`, where the keys are variables names, +;; and the values are terms. (begin-encourage-inline - (define make-subst (make-make-hash Var-name=?)) + (define make-subst make-hasheqv) (define subst? hash?) (define in-subst in-hash) (define subst-count hash-count) @@ -122,48 +123,80 @@ (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) + ;; Modifies the substitution to bind `t` to `var`. + ;; Returns the substitution to mimick the immutable update behaviour. + ;; + ;; subst? Var? term? -> subst? + (define (subst-set! subst V t) + (hash-set! subst (Var-name V) t) subst) + ;; Returns the binding for the variable `V` in `subst`, or `default` if it doesn't exist. + ;; + ;; susbt? Var? term? -> term? + (define (subst-ref subst V [default #false]) + (hash-ref subst (Var-name V) default)) + + ;; Returns the binding for the variable `V` in `susbt` if it exists, + ;; otherwise sets it to `default` and returns `default`. + ;; + ;; subst? Var? term? -> term? + (define (subst-ref! subst V default) + (hash-ref! subst (Var-name V) default)) + + ;; Updates the binding for the variable `V` with `update` + ;; Returns the modified substitution + ;; + ;; subst : subst? + ;; V : Var? + ;; update : term? -> term? + ;; default : term + (define (subst-update! subst V update default) + (hash-update! subst (Var-name V) update default) + subst) + + ;; Returns the substitution as an association list sorted by `Var-name list? (define (subst->list s) - (sort (hash->list s) Var-namelist s) Var-name list? (define (make-imsubst [pairs '()]) pairs) - (define (imsubst-ref subst var default) - (define p (assoc (Var-name var) subst Var-name=?)) - (if p (cdr p) default)) - ) + ;; Like subst-ref for immutable substitutions. + ;; + ;; imsubst? Var? term? -> term? + (define (imsubst-ref subst V default) + (define p (assoc (Var-name V) subst Var-name=?)) + (if p (cdr p) default))) -;; like dict-set, but possibly faster and with fewer checks -(define (imsubst-set subst var val) - (define name (Var-name var)) +;; like subst-set!, but does not modify the substitution and returns a new substitution. +;; +;; subst : imsubst? +;; V : var? +;; t : term? +(define (imsubst-set subst V t) + (define name (Var-name V)) (let loop ([s subst] [left '()]) (cond/else [(empty? s) - (cons (cons name val) subst)] + (cons (cons name t) subst)] #:else (define p (car s)) #:cond [(Var-name=? (car p) name) - (rev-append left (cons (cons name val) (cdr s)))] + (rev-append left (cons (cons name t) (cdr s)))] #:else (loop (cdr s) (cons p left))))) @@ -171,18 +204,22 @@ ;=== Operations on Variables ===; ;===============================; +;; Global index to ensure unicity of variable names. (define fresh-idx 0) + +;; Returns a fresh variable with a unique name. +;; +;; -> Var? (define (new-Var) (++ fresh-idx) (Var fresh-idx)) -(define-syntax-rule (define-Vars v ...) - (begin (define v (new-Var)) ...)) - ;; Renames all variables with fresh names to avoid collisions. -(define (fresh C) +;; +;; term? -> term? +(define (fresh t) (define h (make-subst)) - (let loop ([t C]) + (let loop ([t t]) (cond [(pair? t) (cons (loop (car t)) (loop (cdr t)))] [(Var? t) @@ -193,6 +230,8 @@ ;; and this mapping is guaranteed to be consistent only locally to the term t. ;; Used mostly to turn human-readable expressions into terms, without needing to worry about ;; the actual names of the variables. +;; +;; tree? -> term? (define (symbol-variables->Vars t) (define h (make-hasheq)) (let loop ([t t]) @@ -203,6 +242,8 @@ [else t]))) ;; Variables are replaced with symbols by order of appearence. Mostly for ease of reading by humans. +;; +;; term? -> tree? (define (Vars->symbols t) (define h (make-subst)) (define idx -1) @@ -213,8 +254,9 @@ (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?) +;; 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]) @@ -225,29 +267,31 @@ (subst-update! h t add1 0)])) h) -;; Returns the variable names of the term t. +;; Returns the variable names of the term `t`. +;; +;; term? -> list? (define (vars t) (map car (subst->list (var-occs t)))) -;; Returns the variables of the term t. +;; Returns the variables of the term `t`. +;; +;; term? -> (listof Var?) (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. +;; Returns the set of variables *names* that appear in `t1` but not in `t2`. +;; +;; term? term? -> list? (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. +;; Returns the lexicographical index of each occurrence of the variable names of `t`, +;; in depth-first order. +;; +;; term? -> list? (define (find-var-names t) (define h (make-subst)) (let loop ([t t] [idx 0]) @@ -268,6 +312,8 @@ ;; 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. +;; +;; term? term? -> (or/c '< '> '= #false) (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 @@ -304,8 +350,12 @@ (begin-encourage-inline ;; Logical false (define lfalse '$false) + ;; any/c -> boolean (define (lfalse? x) (eq? lfalse x)) + ;; lfalse must be the bottom element for the various atom orders. + ;; + ;; any/c any/c -> (or/c '< '> '= #false) (define (lfalse<=> a b) (define afalse? (lfalse? a)) (define bfalse? (lfalse? b)) @@ -315,31 +365,32 @@ [else #false])) (define ltrue '$true) + ;; any/c -> boolean? (define (ltrue? x) (eq? x ltrue)) + ;; Returns whether the literal `lit` has negative polarity. + ;; + ;; literal? -> boolean? (define (lnot? lit) (and (pair? lit) (eq? 'not (car lit)))) - ;; Inverses the polarity of the atom. + ;; Inverses the polarity of the literal. ;; NOTICE: Always use `lnot`, do not construct negated atoms yourself. + ;; + ;; literal? -> literal? (define (lnot x) (cond [(lnot? x) (cadr x)] [(lfalse? x) ltrue] [(ltrue? x) lfalse] [else (list 'not x)])) + ;; Compares the polarities of the two literals. + ;; (polarity<=> 'a '(not a)) returns '< + ;; + ;; literal? literal? -> (or/c '< '> '= #false) (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)])) + (boolean<=> (lnot? lit1) (lnot? lit2)))) ;=================================; ;=== Literals, atoms, terms, … ===; @@ -355,10 +406,12 @@ constant = symbol? variable = (Var number?) For simplicity, we sometimes use 'term' to mean 'atom or term', or even -'literal, atom or tem'. +'literal, atom or term'. |# -;; Returns the number of nodes in the tree representing the term t (or literal, atom). +;; Returns the number of nodes in the tree representing the term `t` (or literal, atom). +;; +;; term? -> exact-nonnegative-integer? (define (tree-size t) (let loop ([t t] [s 0]) (cond [(Var? t) (+ s 1)] @@ -367,15 +420,20 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even [else (+ s 1)]))) ;; The literals are depolarized first, because negation should not count. +;; +;; literal? -> exact-nonnegative-integer? (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. +;; +;; clause? -> exact-nonnegative-integer? (define (clause-size cl) (for/sum ([lit (in-list cl)]) (literal-size lit))) +;; Comparison of atoms (or literals) for atom rewriting. ;; 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 @@ -383,9 +441,11 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even ;; - 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)]) +;; +;; literal? literal? -> (or/c '< '> '= #false) +(define (atom1<=> lit1 lit2) + (let ([t1 (depolarize lit1)] + [t2 (depolarize lit2)]) (cond/else [(lfalse<=> t1 t2)] ; continue if neither is lfalse #:else @@ -397,9 +457,14 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even [(and (order≥? vs) (order≥? size)) '>] #:else #false))) -;; For KBO +;; 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). +;; +;; t : term? +;; var-weight : number? +;; fun-weight : symbol? -> number? +;; -> number? (define (term-weight t #:? [var-weight 1] #:? [fun-weight (λ (f) 1)]) (let loop ([t t]) (cond [(Var? t) var-weight] @@ -408,10 +473,16 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even [else (error "Unknown term ~a" t)]))) ;; Knuth-Bendix Ordering, naive version. +;; Can be used for atom rewriting. +;; To do: Implement a faster 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 +;; +;; var-weight : number? +;; fun-weight : symbol? -> number? +;; fun<=> : symbol? symbol? -> (or/c '< '> '= #false) +;; -> (term? term? -> (or/c '< '> '= #false)) (define (make-KBO<=> #:? var-weight #:? fun-weight #:? [fun<=> symbol<=>]) (define (weight t) (term-weight t #:var-weight var-weight #:fun-weight fun-weight)) @@ -445,15 +516,22 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even (or (lfalse<=> t1 t2) (KBO<=> t1 t2))))) +;; Default KBO comparator. +;; +;; term? term? -> (or/c '< '> '= #false) (define KBO1lex<=> (make-KBO<=>)) -;; Returns a literal like lit, but without negation if lit was negative. +;; Returns the atom of the literal. +;; +;; literal? -> atom? (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. +;; +;; literal? -> exact-nonnegative-integer? (define (literal-arity lit) (let ([lit (depolarize lit)]) (if (list? lit) @@ -461,6 +539,8 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even 0))) ;; Returns the name of the predicate (or constant) of the literal. +;; +;; literal? -> symbol? (define (literal-symbol lit) (match lit [`(not (,p . ,r)) p] @@ -469,8 +549,10 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even [else lit])) ;; Lexicographical comparison. +;; Used in literal<=> to sort literals within a clause. NOT used for rewriting. ;; Guarantees: (order=? (term-lex<=> t1 t2)) = (term==? t1 t2) (but maybe a slightly slower?) -;; Warning: Doesn't handle variables that are not Var? properly +;; +;; term? term? -> (or/c '< '> '= #false) (define (term-lex<=> t1 t2) (cond [(eq? t1 t2) '=] ; takes care of '() [(and (pair? t1) (pair? t2)) @@ -487,8 +569,11 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even [else (error 'term-lex<=> "Unknown term kind for: ~a, ~a" t1 t2)])) +;; Comparator for terms used in atom1<=> for atom rewriting. ;; Can't compare vars with symbols, or vars with vars. Can only compare ground symbols: ;; A binary rule can't be oriented with variables +;; +;; term? term? -> (or/c '< '> '= #false) (define (term-lex2<=> t1 t2) (cond [(eq? t1 t2) '=] ; takes care of '() [(and (Var? t1) (Var? t2) (Var=? t1 t2)) '=] @@ -504,7 +589,10 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even (error 'term-lex2<=> "Unknown term kind for: ~a, ~a" t1 t2)])) ;; Depth-first lexicographical order (df-lex) +;; Used for literal ordering in clauses. Not used for atom rewriting. ;; Guarantees: (order=? (literal<=> lit1 lit2)) = (literal==? lit1 lit2). (or it's a bug) +;; +;; literal? literal? -> (or/c '< '> '= #false) (define (literal<=> lit1 lit2) (chain-comparisons (polarity<=> lit1 lit2) @@ -516,12 +604,19 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even [(list? lit1) '>] [else '=]))) +;; Used to sort literals in a clause. +;; +;; literal? literal? -> boolean? (define (literal lit1 lit2))) -;; This works because variables are transparent (prefab), hence equal? traverses the struct too. +;; Syntactic comparison of terms and literals. +;; This works because variables are transparent (prefab), hence equal? traverses the Var struct too. ;; We use `==` to denote syntactic equivalence. +;; +;; term? term? -> boolean? (define term==? equal?) +;; literal? literal? -> boolean? (define literal==? equal?) ;==================================; @@ -534,9 +629,18 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even ;; Also, it's not necessary. (define reduce-mgu? #false) +;; A simple box to signify that there is no need to attempt to substitute +;; inside `term` as this has already been done. (struct already-substed (term) #:prefab) ;; Returns a term where the substitution s is applied to the term t. +;; The substitution `s` may not be 'reduced' in the sense that variables +;; of the domain may appear in the range. +;; Such substitutions are performed 'on-demand', if needed. +;; Once a substitution has been applied recursively to a rhs, the resulting +;; term is marked with `already-substed` to avoid attempting it again. +;; +;; term? subst? -> term? (define (substitute t s) (define t-orig t) (let loop ([t t]) @@ -560,8 +664,9 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even new-rhs]))] [else t]))) -;; v : variable name (symbol) -;; t : term +;; Checks whether the variable `V` occurs un `t`. +;; +;; Var? term? -> boolean? (define (occurs? V t) (cond [(Var? t) (Var=? V t)] [(pair? t) @@ -569,19 +674,20 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even (occurs? V (cdr t)))] [else #false])) -(define (occurs?/extend var t2 subst) +;; Returns #false if `V` occurs in `t2`, otherwise binds `t2` to `V` in `subst` and returns `subst`. +;; +;; Var? term? subst? -> (or/c #false subst?) +(define (occurs?/extend V t2 subst) (define t2c (substitute t2 subst)) - (if (occurs? var t2c) + (if (occurs? V t2c) #false (begin - (subst-set! subst var t2c) + (subst-set! subst V 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? +;; +;; term? term? subst? -> subst? (define (unify t1 t2 [subst (make-subst)]) (define success? (let loop ([t1 t1] [t2 t2]) @@ -622,16 +728,6 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even 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 term? (define (left-substitute t s) (let loop ([t t]) (cond @@ -657,9 +753,10 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even [(and (Var? t) (subst-ref s t #false))] [else t]))) - ;; t1: term? - ;; t2: term? - ;; subst: subst? + + ;; Returns a substitution α such that t1α = t2, if it exists, #false otherwise. + ;; + ;; term? term? subst? -> (or/c #false subst?) (define (left-unify t1 t2 [subst (make-subst)]) (cond/else [(eq? t1 t2) ; takes care of both null? @@ -668,7 +765,7 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even (define new-subst (left-unify (car t1) (car t2) subst)) (and new-subst (left-unify (cdr t1) (cdr t2) new-subst))] - [(term==? t1 t2) subst] ; *** WARNING: This is costly + [(term==? t1 t2) subst] ; To do: This is costly [(not (Var? t1)) #false] #:else (define t1b (subst-ref subst t1 #false)) @@ -685,21 +782,25 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even #:else (subst-set subst t1 t2))))) - +;; Mutable substitutions (define-left-subst+unify left-substitute left-unify make-subst subst-ref subst-set!) ;; Immutable substitutions (define-left-subst+unify left-substitute/assoc left-unify/assoc make-imsubst imsubst-ref imsubst-set) -;; Like traditional pattern matching, but using left-unify +;; Returns #true if `pat` left-unifies with any subterm of `t`. +;; +;; term? term? -> (or/c #false term?) (define (left-unify-anywhere pat t) (let loop ([t t]) (cond [(left-unify pat t)] [(list? t) (ormap loop t)] [else #false]))) -; Could also use match: -(define (match-anywhere filt term) - (let loop ([t term]) +;; Returns #true if `(filt tt)` is true for any subterm `tt` of `t`. +;; +;; (term? -> boolean?) term? -> boolean? +(define (match-anywhere filt t) + (let loop ([t t]) (cond [(filt t)] [(list? t) (ormap loop (rest t))] [else #false])))