Rename vc-clear! -> clear-vc!.

emina · Feb 13, 2021 · 6281fa8 · 6281fa8
1 parent ac0fb55
commit 6281fa8
Show file tree

Hide file tree

Showing 30 changed files with 167 additions and 167 deletions.
diff --git a/rosette/base/base.rkt b/rosette/base/base.rkt
@@ -16,7 +16,7 @@
   (filtered-out drop@ 
     (combine-out
      ; core/bool.rkt
-     vc with-vc vc-clear! vc? vc-true? vc-true vc-assumes vc-asserts
+     vc with-vc clear-vc! vc? vc-true? vc-true vc-assumes vc-asserts
      @assert @assume
      @boolean? @false? @! @&& @=> @<=> @forall @exists
      ; core/real.rkt

diff --git a/rosette/base/core/bool.rkt b/rosette/base/core/bool.rkt
@@ -9,7 +9,7 @@
  and-&& or-|| instance-of? T*->boolean?
  ;; ---- VC generation ---- ;;       
  @assert @assume $assert $assume
- (rename-out [vc-get vc]) vc-clear! vc-merge! with-vc 
+ (rename-out [vc-get vc]) clear-vc! vc-merge! with-vc 
  vc? vc-assumes vc-asserts
  vc-true vc-true?)
 
@@ -318,7 +318,7 @@
 (define (vc-get) (current-vc))
 
 ; Clears the current vc by setting it to the true spec.
-(define (vc-clear!) (current-vc vc-true))
+(define (clear-vc!) (current-vc vc-true))
 
 ; Returns #t if x && (g => y) is equivalent to x according to the embedded
 ; rewrite rules. Otherwise returns #f.

diff --git a/rosette/guide/scribble/datatypes/bitvectors.scrbl b/rosette/guide/scribble/datatypes/bitvectors.scrbl
@@ -89,7 +89,7 @@ into a programming language.
    (bv? (if b (bv 3 6) #t))]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @section{Comparison Operators}
 
@@ -118,7 +118,7 @@ equality (@racket[bveq]) and signed / unsigned versions of
 (code:line (vc)                        (code:comment "so Rosette emits a corresponding assertion."))]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @section{Bitwise Operators}
 
@@ -134,7 +134,7 @@ equality (@racket[bveq]) and signed / unsigned versions of
  (code:line (vc)                      (code:comment "so Rosette emits a corresponding assertion."))]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(bvand [x (bitvector n)] ...+) (bitvector n)]
            [(bvor  [x (bitvector n)] ...+) (bitvector n)]
@@ -155,7 +155,7 @@ Returns the bitwise "and", "or", "xor" of one or more bitvector values of the sa
 }
 
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 @defproc*[([(bvshl  [x (bitvector n)] [y (bitvector n)]) (bitvector n)]
            [(bvlshr [x (bitvector n)] [y (bitvector n)]) (bitvector n)]
            [(bvashr [x (bitvector n)] [y (bitvector n)]) (bitvector n)])]{
@@ -186,7 +186,7 @@ Returns the left, logical right, or arithmetic right shift of @racket[x]  by
  (bvneg z)]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 @(rosette-eval '(clear-terms!))
 
 @defproc*[([(bvadd [x (bitvector n)] ...+) (bitvector n)]
@@ -204,7 +204,7 @@ Returns the sum, difference, or product of one or more bitvector values of the s
  (vc)]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(bvsdiv [x (bitvector n)] [y (bitvector n)]) (bitvector n)]
            [(bvudiv [x (bitvector n)] [y (bitvector n)]) (bitvector n)]
@@ -224,7 +224,7 @@ All five operations are defined even when the second argument is zero.
  (vc)]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @section{Conversion Operators}
 
@@ -251,7 +251,7 @@ All five operations are defined even when the second argument is zero.
  (vc)]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(sign-extend [x bv?] [t (or/c bitvector? union?)]) bv?]
            [(zero-extend [x bv?] [t (or/c bitvector? union?)]) bv?])]{
@@ -272,7 +272,7 @@ must not be smaller than the size of @racket[x]'s type.
  (vc)]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(bitvector->integer [x bv?]) integer?]
            [(bitvector->natural [x bv?]) integer?])]{
@@ -288,7 +288,7 @@ Returns the (un)signed integer value of the given bitvector.
  (vc)]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(integer->bitvector [i integer?] [t (or/c bitvector? union?)]) bv?])]{
 
@@ -306,7 +306,7 @@ Note that both @racket[i] and @racket[t] may be symbolic.
 
 @section{Additional Operators}
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc[(bit [i integer?] [x (bitvector n)]) (bitvector 1)]{
 
@@ -322,7 +322,7 @@ Note that both @racket[i] and @racket[t] may be symbolic.
  (vc)]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(lsb [x (bitvector n)]) (bitvector 1)]
            [(msb [x (bitvector n)]) (bitvector 1)])]{
@@ -339,7 +339,7 @@ Note that both @racket[i] and @racket[t] may be symbolic.
   ]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc[(bvzero? [x (bitvector n)]) boolean?]{
 
@@ -355,7 +355,7 @@ Returns @racket[(bveq x (bv 0 n))].
  ]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(bvadd1 [x (bitvector n)]) (bitvector n)]
            [(bvsub1 [x (bitvector n)]) (bitvector n)])]{
@@ -374,7 +374,7 @@ Returns @racket[(bveq x (bv 0 n))].
 }
 
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(bvsmin [x (bitvector n)] ...+) (bitvector n)]
            [(bvumin [x (bitvector n)] ...+) (bitvector n)]
@@ -393,7 +393,7 @@ Returns the (un)signed minimum or maximum of one or more bitvector values of the
  (vc)]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(bvrol [x (bitvector n)] [y (bitvector n)]) (bitvector n)]
            [(bvror [x (bitvector n)] [y (bitvector n)]) (bitvector n)])]{
@@ -412,7 +412,7 @@ Returns the left or right rotation of @racket[x] by @racket[(bvurem y n)] bits,
   (vc)                      (code:comment "so Rosette emits a corresponding assertion."))]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(rotate-left  [i integer?] [x (bitvector n)]) (bitvector n)]
            [(rotate-right [i integer?] [x (bitvector n)]) (bitvector n)])]{
@@ -432,7 +432,7 @@ leads to faster solving times.
  ]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc[(bitvector->bits [x (bitvector n)]) (listof (bitvector n))]{
 
@@ -450,7 +450,7 @@ Returns the bits of @racket[x] as a list, i.e., @racket[(list (bit 0 x) ... (bit
 Returns @racket[(not (bvzero? x))].
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc[(bool->bitvector [b any/c] [t (or/c positive-integer? (bitvector n)) (bitvector 1)]) bv?]{
 

diff --git a/rosette/guide/scribble/datatypes/bools+ints+reals.scrbl b/rosette/guide/scribble/datatypes/bools+ints+reals.scrbl
@@ -61,7 +61,7 @@ logical meaning; e.g., unlike Racket's shortcircuiting
 evaluates all of its arguments before taking their
 conjunction.
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc[(! [v boolean?]) boolean?]{
   Returns the negation of the given boolean value.
@@ -73,7 +73,7 @@ conjunction.
    (code:line (vc)            (code:comment "so Rosette emits a corresponding assertion."))]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(&& [v boolean?] ...) boolean?]
            [(|| [v boolean?] ...) boolean?])]{
@@ -87,7 +87,7 @@ Returns the logical conjunction or disjunction of zero or more boolean values.
  (code:line (vc)               (code:comment "so Rosette emits a corresponding assertion."))]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc*[([(=>  [x boolean?] [y boolean?]) boolean?]
            [(<=> [x boolean?] [y boolean?]) boolean?])]{
@@ -109,7 +109,7 @@ body may have side effects (e.g., generate assertions). When
 there are no side effects, however, these constructs have
 their usual logical meaning.
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 @(rosette-eval '(current-bitwidth #f))
 @defproc*[([(forall [vs (listof constant?)] [body boolean?]) boolean?]
            [(exists [vs (listof constant?)] [body boolean?]) boolean?])]{
@@ -135,7 +135,7 @@ with pure bodies, as shown below.
   (forall (list b x y)
     (= (+ (if b x 'x) 1) y))    (code:comment "Body emits a type assertion."))
  (vc)
- (vc-clear!)
+ (clear-vc!)
  (code:comment "To avoid surprises, capture assertions and assumptions using with-vc,")
  (code:comment "and handle as desired, e.g.:")
  (define out (with-vc (= (+ (if b x 'x) 1) y)))

diff --git a/rosette/guide/scribble/datatypes/bools-log.txt b/rosette/guide/scribble/datatypes/bools-log.txt
@@ -16,7 +16,7 @@
   (c values c (0 (u . "(! b)"))))
  #""
  #"")
-((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
+((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((! #f) ((3) 0 () 0 () () (q values #t)) #"" #"")
 ((! #t) ((3) 0 () 0 () () (q values #f)) #"" #"")
 ((define-symbolic b boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -33,7 +33,7 @@
   (c values c (0 (u . "(vc #t b)"))))
  #""
  #"")
-((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
+((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((&&) ((3) 0 () 0 () () (q values #t)) #"" #"")
 ((||) ((3) 0 () 0 () () (q values #f)) #"" #"")
 ((&& #f (begin (displayln "hello") #t))
@@ -65,7 +65,7 @@
   (c values c (0 (u . "(vc #t b)"))))
  #""
  #"")
-((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
+((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((=> #f (begin (displayln "hello") #f))
  ((3) 0 () 0 () () (q values #t))
  #"hello\n"
@@ -95,7 +95,7 @@
   (c values c (0 (u . "(vc #t b)"))))
  #""
  #"")
-((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
+((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((define-symbolic x y integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -136,7 +136,7 @@
   (c values c (0 (u . "(vc #t b)"))))
  #""
  #"")
-((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
+((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((define out (with-vc (= (+ (if b x 'x) 1) y)))
  ((3) 0 () 0 () () (c values c (void)))
  #""

diff --git a/rosette/guide/scribble/datatypes/equality.scrbl b/rosette/guide/scribble/datatypes/equality.scrbl
@@ -61,7 +61,7 @@ comparisons.  But when applied to symbolic values of a primitive
 @tech[#:key "solvable type"]{solvable} type, @racket[distinct?] will produce a compact
 symbolic value that can be directly solved by the underlying solver.
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 @defproc[(distinct? [v any/c] ...) boolean?]{
   Returns true iff all of the given values @racket[v] are distinct---i.e., pairwise un-@racket[equal?]
   to each other.  If all values @racket[v] are of the same primitive (non-@racket[function?])

diff --git a/rosette/guide/scribble/datatypes/uninterpreted-log.txt b/rosette/guide/scribble/datatypes/uninterpreted-log.txt
@@ -141,7 +141,7 @@
 ((function? (if b t0? t1?)) ((3) 0 () 0 () () (q values #f)) #"" #"")
 ((function? integer?) ((3) 0 () 0 () () (q values #f)) #"" #"")
 ((function? 3) ((3) 0 () 0 () () (q values #f)) #"" #"")
-((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
+((clear-vc!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((define-symbolic f (~> boolean? boolean?))
  ((3) 0 () 0 () () (c values c (void)))
  #""

diff --git a/rosette/guide/scribble/datatypes/uninterpreted.scrbl b/rosette/guide/scribble/datatypes/uninterpreted.scrbl
@@ -5,7 +5,7 @@
            rosette/base/core/term (only-in rosette/query/finitize current-bitwidth)
            (only-in rosette/base/core/union union?)
            (only-in rosette/base/core/function ~> function? fv?)
-           (only-in rosette/base/base bv bitvector assert vc vc-clear!))
+           (only-in rosette/base/base bv bitvector assert vc clear-vc!))
           (for-label racket) racket/runtime-path
           scribble/core scribble/html-properties scribble/examples racket/sandbox
           "../util/lifted.rkt")
@@ -81,7 +81,7 @@ g
   (code:line (function? 3)              (code:comment "Not a type."))]
 }
 
-@(rosette-eval '(vc-clear!))
+@(rosette-eval '(clear-vc!))
 
 @defproc[(fv? [v any/c]) boolean?]{