change: send-to-kodkod -> send-to-solver

forge/amalgam.rkt

@@ -4,7 +4,7 @@
 
 (require forge/amalgam/desugar/desugar)
 (require forge/amalgam/lift-bounds/lift-bounds)
-(require forge/send-to-kodkod)
+(require forge/send-to-solver)
 
 (require (only-in racket/contract define/contract ->i and/c or/c listof))
 (require (only-in racket cartesian-product first second rest empty?
@@ -55,7 +55,7 @@
   ; which means we have its Run-spec
   ; which is post-processing by the run macro
   (define modified-run-spec (struct-copy Run-spec (Run-run-spec orig-run) [scope scope] [bounds bounds]))
-  (define-values (run-result atoms server-ports kodkod-currents kodkod-bounds) (send-to-kodkod modified-run-spec (Run-command orig-run)))        
+  (define-values (run-result atoms server-ports kodkod-currents kodkod-bounds) (send-to-solver modified-run-spec (Run-command orig-run)))        
   (Run (Run-name orig-run) (Run-command orig-run) modified-run-spec run-result server-ports atoms kodkod-currents kodkod-bounds))
 
 ; takes a hash-table representation of an instance and a tuple and flips the truth of

forge/send-to-kodkod.rkt → forge/send-to-solver.rkt

@@ -23,7 +23,7 @@
 ; Disable DrRacket GUI extension/tool
 ;(require "drracket-gui.rkt")
 
-(provide send-to-kodkod)
+(provide send-to-solver)
 
 (define no-version-printed-yet #t)
 
@@ -37,12 +37,12 @@
 ; and throw a friendlier error if one is re-used. 
 (define run-name-history (box (list)))
 
-; send-to-kodkod :: Run-spec -> Stream<model>, List<Symbol>
+; send-to-solver :: Run-spec -> Stream<model>, List<Symbol>
 ; Given a Run-spec structure, processes the data and communicates it to KodKod-CLI;
 ; then produces a stream to produce instances generated by KodKod, 
 ; along with a list of all of the atom names for sig atoms.
-(define (send-to-kodkod run-spec run-command #:run-name [run-name (gensym)])
-  (do-time "send-to-kodkod")
+(define (send-to-solver run-spec run-command #:run-name [run-name (gensym)])
+  (do-time "send-to-solver")
 
   ; In case of error, highlight an AST node if able. Otherwise, focus on the offending run command.
   (define (raise-run-error message [node #f])
@@ -152,7 +152,7 @@
       [(and (unbox server-state) ((Server-ports-is-running? (unbox server-state))))
        (define sstate (unbox server-state))
        (when (@> (get-verbosity) VERBOSITY_LOW)
-        (printf "Pardinus solver process already running. Preparing to start new run with id ~a.~n" run-name))
+        (printf "~a solver process already running. Preparing to start new run with id ~a.~n" backend run-name))
        (values (Server-ports-stdin sstate) (Server-ports-stdout sstate) 
                (Server-ports-stderr sstate) (Server-ports-shutdown sstate)
                (Server-ports-is-running? sstate))]
@@ -797,7 +797,7 @@ Please declare a sufficient scope for ~a."
       ;(define upper (set->list (set-intersect (get-bound-upper relation) (list->set (apply cartesian-product sig-atoms)))))
       ;(printf "~a: refined upper : ~a~n" relation upper)
 
-      ; Piecewise lower bounds were handled in sigs-functional, before send-to-kodkod is called.
+      ; Piecewise lower bounds were handled in sigs-functional, before send-to-solver is called.
       (define lower                   
         (let ([bound-lower (get-bound-lower relation)])
             (if bound-lower

forge/sigs-functional.rkt

@@ -26,7 +26,7 @@
 (require forge/shared
          forge/sigs-structs
          forge/evaluator
-         forge/send-to-kodkod)
+         forge/send-to-solver)
 
 (require (only-in forge/lang/alloy-syntax/parser [parse forge-lang:parse])
          (only-in forge/lang/alloy-syntax/tokenizer [make-tokenizer forge-lang:make-tokenizer]))
@@ -601,7 +601,7 @@
   ; piecewise (incomplete), it cannot be bound complete. E.g., we cannot mix "`Alice.father = ..."
   ; and "father = " ...
   ; However, we cannot actually convert 'in/'= piecewise bounds to complete upper bounds until
-  ; send-to-kodkod, when we have created the universe of atoms and can "fill in" missing upper bounds.
+  ; send-to-solver, when we have created the universe of atoms and can "fill in" missing upper bounds.
   ; (Piecewise 'ni bounds should be fine to convert here.)
   (for/list ([rel (hash-keys (Bound-piecewise bounds))])
     (when (or (hash-has-key? (Bound-tbindings bounds) rel)
@@ -614,10 +614,10 @@
       (define pwb (hash-ref (Bound-piecewise bounds) rel))
       (define tups (PiecewiseBound-tuples pwb))
       (cond [(equal? '= (PiecewiseBound-operator pwb))
-             ; update only lower bound, not upper (handled in send-to-kodkod)
+             ; update only lower bound, not upper (handled in send-to-solver)
              (update-bindings bs rel tups #f #:node #f)] 
             [(equal? 'in (PiecewiseBound-operator pwb))
-             ; do nothing (upper bound handled in send-to-kodkod)
+             ; do nothing (upper bound handled in send-to-solver)
              bs]
             [(equal? 'ni (PiecewiseBound-operator pwb))
              ; update lower-bound
@@ -633,7 +633,7 @@
 
   (define spec (Run-spec state preds scope bounds-with-piecewise-lower target))        
   (define-values (result atoms server-ports kodkod-currents kodkod-bounds) 
-                 (send-to-kodkod spec command #:run-name name))
+                 (send-to-solver spec command #:run-name name))
 
   (Run name command spec result server-ports atoms kodkod-currents kodkod-bounds (box #f)))
 
@@ -911,7 +911,7 @@
                          [target new-target]
                          [state new-state]))
           (define-values (run-result atom-rels server-ports kodkod-currents kodkod-bounds) 
-                         (send-to-kodkod contrast-run-spec))
+                         (send-to-solver contrast-run-spec))
           (define contrast-run 
             (struct-copy Run run
                          [name (string->symbol (format "~a-contrast" (Run-name run)))]

forge/sigs-structs.rkt

@@ -85,7 +85,7 @@
 
 ; NOTE WELL:
 ; The structs below define an intermediate representation; the Kodkod bounds (produced in
-; forge/send-to-kodkod) are what is actually sent to the solver.
+; forge/send-to-solver) are what is actually sent to the solver.
 
 ; ALSO: be aware that the "bounds", "sbounds" etc. structs defined elsewhere are distinct from
 ; the Bounds struct defined here. At some point, we can perhaps condense these into a single IR.

forge/sigs.rkt

@@ -24,7 +24,7 @@
          forge/sigs-structs
          forge/evaluator
          (prefix-in tree: forge/lazy-tree)
-         forge/send-to-kodkod)
+         forge/send-to-solver)
 (require (only-in forge/lang/alloy-syntax/parser [parse forge-lang:parse])
          (only-in forge/lang/alloy-syntax/tokenizer [make-tokenizer forge-lang:make-tokenizer]))
 (require (only-in forge/sigs-functional
@@ -876,7 +876,7 @@
                          [target new-target]
                          [state new-state]))
           (define-values (run-result atom-rels server-ports kodkod-currents kodkod-bounds)
-                         (send-to-kodkod contrast-run-spec))
+                         (send-to-solver contrast-run-spec))
           (define contrast-run 
             (struct-copy Run run
                          [name (string->symbol (format "~a-contrast" (Run-name run)))]