Rename solver-add to solver-assert.

sorawee · Feb 27, 2016 · 4cf85e2 · 4cf85e2
1 parent 46749fe
commit 4cf85e2
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 27 deletions.
diff --git a/rosette/query/core.rkt b/rosette/query/core.rkt
@@ -11,7 +11,7 @@
   (only-in "../base/struct/enum.rkt" enum? enum-first)
   (only-in "../base/core/finitize.rkt" finitize current-bitwidth)
   (only-in "../base/util/log.rkt" log-info)
-  (only-in "../solver/solver.rkt" solver? solver-shutdown solver-clear solver-add solver-check solver-localize)
+  (only-in "../solver/solver.rkt" solver? solver-shutdown solver-clear solver-assert solver-check solver-localize)
   (only-in "../solver/solution.rkt" model core sat unsat sat? unsat? default-binding)
   (only-in "../solver/smt/z3.rkt" z3))
 
@@ -92,16 +92,16 @@
         [bw 
          (parameterize ([term-cache (hash-copy (term-cache))])
            (define fmap (finitize φs bw))
-           (solver-add solver (for/list ([φ φs]) (hash-ref fmap φ)))
+           (solver-assert solver (for/list ([φ φs]) (hash-ref fmap φ)))
            (let loop ()
              (define fsol (complete (solver-check solver) fmap))
              (define sol (unfinitize fsol fmap)) 
              (cond 
                [(or (unsat? sol) (all-true? φs sol)) sol]
-               [else (solver-add solver (list (apply || (for/list ([(c v) (model fsol)]) (! (@equal? c v))))))
+               [else (solver-assert solver (list (apply || (for/list ([(c v) (model fsol)]) (! (@equal? c v))))))
                      (loop)])))]
         [else 
-         (solver-add solver φs)
+         (solver-assert solver φs)
          (solver-check solver)]))
     (solver-clear solver)))
 
@@ -123,7 +123,7 @@
          (let outer ([δs ψs])
            (with-handlers ([exn? handler])
              (finitize δs bw fmap)
-             (solver-add solver (for/list ([δ δs]) (hash-ref fmap δ)))
+             (solver-assert solver (for/list ([δ δs]) (hash-ref fmap δ)))
              (set! φs (append δs φs)) 
              (let inner ()
                (define fsol (complete (solver-check solver) fmap))
@@ -136,12 +136,12 @@
                       sol]
                      [(all-true? φs sol) (outer (yield sol))]
                      [else  
-                      (solver-add solver (list (apply || (for/list ([(c v) (model fsol)]) (! (@equal? c v))))))
+                      (solver-assert solver (list (apply || (for/list ([(c v) (model fsol)]) (! (@equal? c v))))))
                       (inner)]))))))                      
       (generator (φs)
        (let loop ([φs φs])
          (with-handlers ([exn? handler])
-           (solver-add solver φs)
+           (solver-assert solver φs)
            (define sol (solver-check solver))
            (cond [(unsat? sol) (solver-shutdown solver) (custodian-shutdown-all cust) sol]
                  [else (loop (yield sol))]))))))
@@ -161,10 +161,10 @@
         [bw 
          (parameterize ([term-cache (hash-copy (term-cache))])
            (define fmap (finitize φs bw))
-           (solver-add solver (for/list ([φ φs]) (hash-ref fmap φ)))
+           (solver-assert solver (for/list ([φ φs]) (hash-ref fmap φ)))
            (unfinitize (solver-localize solver) fmap))]
         [else 
-         (solver-add solver φs)
+         (solver-assert solver φs)
          (solver-localize solver)]))
     (solver-clear solver)))
 
@@ -214,15 +214,15 @@
 
   (define (guess sol)
     (log-cegis-info [trial] "searching for a candidate: ~s" (map sol inputs))
-    (solver-add guesser (evaluate φ sol))
+    (solver-assert guesser (evaluate φ sol))
     (match (solver-check guesser)
       [(model m) (sat (for/hash ([(c v) m] #:unless (member c inputs)) (values c v)))]
       [other other]))
 
   (define (check sol)
     (log-cegis-info [trial] "verifying the candidate solution ...")
     (solver-clear checker)
-    (solver-add checker (evaluate ¬φ sol))
+    (solver-assert checker (evaluate ¬φ sol))
     (match (solver-check checker)
       [(? sat? m) (sat (for/hash ([i inputs]) (values i (value-for (m i)))))]
       [other other]))
@@ -249,4 +249,4 @@
         [(? enum? t) (enum-first t)])
       v))
 
-
+
diff --git a/rosette/solver/smt/z3.rkt b/rosette/solver/smt/z3.rkt
@@ -21,7 +21,7 @@
 (struct z3 (server [asserts #:mutable] [mins #:mutable] [maxs #:mutable] [env #:mutable])
   #:methods gen:solver
   [
-   (define (solver-add self bools)
+   (define (solver-assert self bools)
      (set-z3-asserts! self 
       (append (z3-asserts self)
               (for/list ([b bools] #:unless (equal? b #t))
@@ -84,4 +84,4 @@
   (for/list ([t ts] #:unless (or (real? t) (bv? t)))
     (match t
       [(term _ (or (== @integer?) (== @real?) (? bitvector?))) t]
-      [_ (error caller "expected a numeric term, given ~s" t)])))
+      [_ (error caller "expected a numeric term, given ~s" t)])))
diff --git a/rosette/solver/solver.rkt b/rosette/solver/solver.rkt
@@ -3,17 +3,17 @@
 (require racket/generic)
 
 (provide gen:solver solver? 
-         solver-add solver-clear
+         solver-assert solver-clear
          solver-minimize solver-maximize
          solver-check solver-localize 
          solver-shutdown)
 
 ; The generic solver interface specifies the set of procedures that 
 ; should be provided by a Rosette solver. These include 
-; solver-add, solver-clear, solver-minimize, solver-maximize,
+; solver-assert, solver-clear, solver-minimize, solver-maximize,
 ; solver-check, solver-localize, and solver-shutdown. 
 ;
-; The solver-add procedure takes as input zero or more @boolean? 
+; The solver-assert procedure takes as input zero or more @boolean? 
 ; values and adds them to the current state of the solver. 
 ; The solver-clear procedure clears all constraints from the current 
 ; state of the solver.
@@ -37,7 +37,7 @@
 ; with this solver instance.  The solver must be able to reacquire these resources 
 ; if needed.  That is, the solver should behave as specified above after a shutdown call.
 (define-generics solver
-  [solver-add solver bools]
+  [solver-assert solver bools]
   [solver-clear solver]
   [solver-minimize solver nums]
   [solver-maximize solver nums]

diff --git a/sdsl/bv/lang/core.rkt b/sdsl/bv/lang/core.rkt
@@ -11,7 +11,7 @@
   (only-in rosette/base/util/log log-info)
   (only-in rosette/solver/solution model sat sat? unsat? unsat)
   (only-in rosette/solver/smt/z3 z3)
-  (only-in rosette/solver/solver solver-add solver-check solver-clear))
+  (only-in rosette/solver/solver solver-assert solver-check solver-clear))
 
 (provide ∃∀-solve)
 
@@ -35,7 +35,7 @@
              (parameterize ([term-cache (hash-copy (term-cache))]
                             [BV (bitvector maxbw)])
                (solver-clear checker)
-               (solver-add checker (φ_verify (evaluate (trace* impl) sol) spec))
+               (solver-assert checker (φ_verify (evaluate (trace* impl) sol) spec))
                (unsat? (solver-check checker)))))
       (let loop ([bw (min (max 1 minbw) maxbw)])
         (define candidate 
@@ -63,24 +63,24 @@
 
   (define (init)
     (solver-clear guesser)
-    (solver-add guesser (φ_wfp impl))
-    (solver-add guesser (φ_synth t0 spec))
+    (solver-assert guesser (φ_wfp impl))
+    (solver-assert guesser (φ_synth t0 spec))
     (log-solver-info [trial] "searching for an initial candidate at ~a" (BV))
     (begin0
       (solution->candidate (solver-check guesser))
       (solver-clear guesser)
-      (solver-add guesser (φ_wfp impl))))
+      (solver-assert guesser (φ_wfp impl))))
 
   (define (guess sol)
     (set! trial (add1 trial))
     (define sample (map sol inputs))
     (log-solver-info [trial] "searching for a candidate: ~s" sample)
-    (solver-add guesser (φ_synth (trace* impl sample) spec))
+    (solver-assert guesser (φ_synth (trace* impl sample) spec))
     (solution->candidate (solver-check guesser)))
 
   (define (check sol)
     (solver-clear checker)
-    (solver-add checker (φ_verify (evaluate t0 sol) spec))
+    (solver-assert checker (φ_verify (evaluate t0 sol) spec))
     (solution->sample (solver-check checker) inputs))
 
   (let loop ([candidate (init)])
@@ -130,4 +130,4 @@
 ;(current-log-handler (log-handler #:info any/c))
 (define impl (prog* 1 (list (op #'identity identity))))
 (∃∀-solve impl identity 4)
-|#
+|#
diff --git a/test/base/solver.rkt b/test/base/solver.rkt
@@ -7,7 +7,7 @@
 (define solver (make-parameter (z3)))
 
 (define (solve  . asserts)
-  (solver-add (solver) asserts)
+  (solver-assert (solver) asserts)
   (begin0
     (solver-check (solver))
     (solver-clear (solver))))