emina / rosette Goto Github PK

I might be missing something but I don't think this is appropriate behaviour. Still running with example from #72 but with a slight change:

#lang rosette

(define opvec (vector 'foo 'bar 'baz 'tar 'taz))

(define-struct insn
  (op
   args-vec))

(define-symbolic* op integer?)
(define-symbolic* arg1 (bitvector 32))
(define-symbolic* arg2 (bitvector 32))

(define-symbolic* res (bitvector 32))

(define i1
  (insn op
        (vector arg1 arg2)))

(define (inter b)
  (case (vector-ref opvec (insn-op b))
    [(foo)
     (printf "rosette: interpreting foo~n")
     (void)]

    [(baz)
     (printf "rosette: interpreting baz~n")
     (set! res (vector-ref (insn-args-vec b)
                           0))]

    [(tar)
     (printf "rosette: interpreting tar~n")
     (set! res (bvadd (vector-ref (insn-args-vec b) 0)
                       (vector-ref (insn-args-vec b) 1)))]

    [else
     (assert #f "unknown op")])
  res)

(printf "store~n")
(pretty-print (asserts))

(define result
  (inter i1))

(printf "store after inter~n")
(pretty-print (asserts))

(printf "result: ~a~n" result)

The repl shows:

result: (ite (= 0 op$0) res$0 (ite (= 2 op$0) arg1$0 (bvadd arg1$0 arg2$0)))

This is correct. We get a value depending on if we went into the foo, baz or tar case.
However, if we introduce an error on purpose:

#lang rosette

(define opvec (vector 'foo 'bar 'baz 'tar 'taz))

(define-struct insn
  (op
   args-vec))

(define-symbolic* op integer?)
(define-symbolic* arg1 (bitvector 32))
(define-symbolic* arg2 (bitvector 32))

(define-symbolic* res (bitvector 32))

(define i1
  (insn op
        (vector arg1 arg2)))

(define (inter b)
  (case (vector-ref opvec (insn-op b))
    [(foo)
     (printf "rosette: interpreting foo~n")
     (void)]

    [(baz)
     (printf "rosette: interpreting baz~n")
     (set! res (vector-ref (insn-args-vec b)
                           0))]

    [(tar)
     (printf "rosette: interpreting tar~n")
     (set! res (bvadd (vector-ref (insn-args-vec b) 0)
                      (bv ; <- ERROR
                       (vector-ref (insn-args-vec b) 1)
                       (bitvector 32))
           ))]

    [else
     (assert #f "unknown op")])
  res)

(printf "store~n")
(pretty-print (asserts))

(define result
  (inter i1))

(printf "store after inter~n")
(pretty-print (asserts))

(printf "result: ~a~n" result)

The error is in the tar case where we call bv and the vector-ref argument already returns a bitvector. In this case this should cause an error except it doesn't.

We get:

result: (ite (= 0 op$0) res$0 arg1$0)

So it's almost as if since there's an error in the case, this is silently ignored. This makes debugging large rosette programs very, very hard.

When trying one of the basic examples from the docs, I get the following error:

.racket/snapshot/pkgs/rosette/rosette/solver/smt/cmd.rkt:60:0: solution: unrecognized solver output: #<eof>

Here's the program:

#lang rosette/safe

(define (poly x)
 (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))

(define-symbolic x y integer?)
(define sol
    (solve (begin (assert (not (= x y)))
                  (assert (< (abs x) 10))
                  (assert (< (abs y) 10))
                  (assert (not (= (poly x) 0)))
                  (assert (= (poly x) (poly y))))))
(evaluate x sol)
(evaluate y sol)
(evaluate (poly x) sol)
(evaluate (poly y) sol)

I'm using Z3 version 4.4.1, 64-bit version, on the NixOS Linux Distribution.

I tried adding (writeln (port->string (peeking-input-port port))) inside (read-solution) in smtlib2.rkt, and indeed, I get an empty string, but I don't know where to look further.

Is there anything I can do to debug this?

Currently, bitvector is broken because syntax-id-rules is poorly designed (and should not be used):

> (bitvector 1 1)
#<procedure:bitvector-type>
> (bitvector 1 2 3 4 6 #:fskal)
#<procedure:bitvector-type>
> ((bitvector 1 2 3 4 6 #:fskal) 1)
(bitvector 1)
> ((set! bitvector 5) 1)
(bitvector 1)

A better alternative is to (in this code) use make-variable-like-transformer:

(define-match-expander @bitvector
  (syntax-rules ()
    [(_ sz) (bitvector sz)])
  (make-variable-like-transformer #'bitvector-type))

Should we submit a pull request with this change?

For the program:

#lang rosette/safe
(define-symbolic offset integer?)
(define-symbolic a (~> integer? integer?))
(define-symbolic disk (~> integer? integer? integer?))

(current-bitwidth #false)
(solve
 (assert
  (forall
   (list offset)
   (= (a offset) (disk 5 offset)))))

Rosette throws errors from decode-body, one of:

• .../rosette/solver/smt/cmd.rkt:113:2: match: no matching clause for 0
• .../rosette/solver/smt/cmd.rkt:113:2: match: no matching clause for '(c3 5 x!1)

The original undecoded input solution was this hash table:

'#hash((c3 . (define-fun c3 ((x!1 Int) (x!2 Int)) Int 0))
       (c1 . (define-fun c1 ((x!1 Int)) Int (c3 5 x!1))))

The first error case no matching clause for 0 can be solved by adding these two lines to the match in decode-body

    [(? integer? v0)
     (list (decode-value ran v0))]

But the second case with '(c3 5 x!1) will be different.

I get error writing to stream port system error: The pipe is being closed.; errno=232 when trying to eval (define cex (verify (same poly factored i))) with the following set of definitions (and with z3.exe in the bin directory, as per the documentation).

#lang s-exp rosette

(require rosette/solver/smt/z3)
(current-solver (new z3%))

; > (current-solver)
; z3%

; From: http://homes.cs.washington.edu/~emina/rosette/guide/ch_essentials.html
; (as of 2016-01-28)

(define (poly x)
 (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))

(define (factored x)
 (* x (+ x 1) (+ x 2) (+ x 2)))

(define (same p f x)
 (assert (= (p x) (f x))))

; "check zeros; all seems well ..."
; > (same poly factored 0)
; > (same poly factored -1)
; > (same poly factored -2)

; > (define-symbolic i number?)
; > (define cex (verify (same poly factored i)))
;   -- Currently returns:
; error writing to stream port
;   system error: The pipe is being closed.; errno=232

Backtrace seems to finger server.rkt as the culprit (but maybe it's really an issue with flush-output in racket/base? -- see below):

E:\Temp\rosette\rosette\solver\common\server.rkt: 59:4

(define/public (write proc)
  (initialize)
  (begin0 (proc in)
          (flush-output in)))

E:\Temp\rosette\rosette\solver\smt\smt.rkt: 30:4

(define/public (clear)
  (send server write clear-solver)
  (set!-values (asserts env) (values '() (make-env))))

Perhaps this is related to the issue mentioned here (WRT some Python code using Python's multiprocessing module): http://stackoverflow.com/questions/19070638/python-multiprocessing-ioerror-errno-232-the-pipe-is-being-closed ?

I haven't spent much time on this, and this is as far as I've gotten with diagnosing and troubleshooting this issue so far. Time permitting, I'll continue to dig, but any help would be appreciated. FWIW, I'm on Windows 7 Ultimate SP1 64-bit, and I'm currently using DrRacket 6.1 64-bit.

Thanks!

If I have the following module, based on the one in the docs:

#lang s-exp rosette/safe

(require rosette/query/debug
         rosette/lib/tools/render
         rosette/lib/meta/meta)

(define (poly x)
  (* (+ x 1) (+ x 1)))

(define (factor x)
  (+ (* x x) (* 2 x) (??))) ;; XXX: Should be 1

(define (same p f x)
  (assert (= (p x) (f x))))

(define-symbolic i number?)
(define binding
  (synthesize #:forall (list i)
              #:guarantee (same poly factor i)))
(print-forms binding)

I get the following output:

'(define (factor x) (+ (* x x) (* 2 x) 1))

However, if I move those last three lines into the repl, I get the following output:

'(define (factor x) (+ (* x x) (* 2 x) 1))

Is this expected behavior? (If so, can you please help me understand it?)

For code

#lang rosette
(define-symbolic x integer?)
(solve (begin
(define y (* x 2) )
(assert (> x y) )
)) 

It always returns x=-2. Currently, I only come out with one solution to get values other than -2:

#lang rosette
(define-symbolic x integer?)
(solve (begin
(define y (* x 2) )
(assert (> x y) )
(assert (not (eq? x -2)))
))

However, it is not a scalable solution if I want to get multiple values. Is there some racket programming tricks to solve this problem?

Is there a way to output the SMT problem sent to Z3 in smt format?

I can create a fake z3 that gathers the communication between rosette and z3 but if there was a simpler way it would be great.

Not sure yet how I got to this backtrace (it's a very large rosette program), but I end up with:

 $=: expected real? arguments
  arguments: (list input$0)
  context...:
   /home/pmatos/.racket/6.11/pkgs/rosette/rosette/base/core/real.rkt:160:10
   /home/pmatos/.racket/6.11/pkgs/rosette/rosette/base/form/control.rkt:30:25

I am trying to create a small reproducer in the meantime. Posting this before I find one in case you manage to look at the code and figure out straight away what the problem might be.

Is there a reason why the function symbolics is undocumented?

If it's not supposed to be part of the public API, does rosette provide another public function that can be used instead?

I ran the following code which have a race condition with SynthCL, but SynthCL didn't report any race and said "No counterexample found".

;; kernel.rkt
;; A kernel with a race between 0-th and (size - 1)-th threads
(kernel void (test-race [int* arr] [int size])
  (: int x)
  (print "id = " (get_global_id 0) "\n")
  (= x [arr 0])
  (if (== (get_global_id 0) (- size 1))
      { (= [arr 0] (get_global_id 0)) }
))

;; host.rkt
#lang s-exp "./synthcl/lang/main.rkt"

(procedure int* (host [int* src] [int SIZE])
  (: cl_context context)
  (: cl_command_queue command_queue)
  (: cl_program program)
  (: cl_kernel kernel)
  (: cl_mem buffer_src)
  (: int global)

  (= global SIZE)

  (= context (clCreateContext))

  (= command_queue (clCreateCommandQueue context))

  (= buffer_src (clCreateBuffer context CL_MEM_READ_WRITE (* SIZE (sizeof int))))

  (= program (clCreateProgramWithSource context "kernel.rkt"))

  (clEnqueueWriteBuffer command_queue buffer_src 0 SIZE src)

  (= kernel (clCreateKernel program "test-race"))
  (clSetKernelArg kernel 0 buffer_src)
  (clSetKernelArg kernel 1 SIZE)

  (clEnqueueNDRangeKernel command_queue kernel 1 NULL (@ global) NULL)
  (clEnqueueReadBuffer command_queue buffer_src 0 SIZE src) 
  src)

(procedure void (run-test-race)
  (: int* dst)
  (: int size)
  (= size 10)
  (= dst ((int*) (malloc (* size (sizeof int)))))
  (for ([: int i in (range size)]) (= [dst i] 0))
  (host dst size))

(verify #:forall [] #:ensure (run-test-race))

This example:

(list
 (add1 (if b 1 (bv 1 1)))
 (bvnot (if b 1 (bv 1 1))))

evaluates to (list 2 (bv 0 1)) even though it would result in an exception in Racket for any value of b. Is this the intended behavior?

I am trying rosette on a (yes!) rpi. :) This is an arm based cpu with no issues running racket, rosette or z3, however it turns out that there's no entry on private/install.rkt so it can't automatically install z3.

I see you have purpose-built z3 on the releases folder which you download. How can one add a build for (unix 32)?

Unfortunately, right now the Racket automatic pkg-build server for Racket fails to build Rosette, because it doesn't allow it to download Z3. You can see the current error here: https://plt.eecs.northwestern.edu/pkg-build/server/built/fail/rosette.txt

This means that Rosette's documentation doesn't appear on https://docs.racket-lang.org among other issues.

Probably the right fix is to enable the docs to run without actually using z3. I'm happy to help with that if needed.

As opposed to what's said here:
https://docs.racket-lang.org/rosette-guide/sec_solvers-and-solutions.html?q=rosette#%28def._%28%28lib._rosette%2Fsolver%2Fsmt%2Fz3..rkt%29._z3%29%29

Rosette does not recognize z3:

#lang rosette
(define solver-z3 (z3))

Output:

z3: unbound identifier in module in: z3

Hello,

Sometimes when printing formulas I get a ...:

(ite (bveq input$35 (bvadd (bv 2 32) input$35)) ...))) ...)

How can I avoid this and request the whole formula to be printed?

Also, sometimes I get the printed formula as above, other times I see: {4486849377583105866:41}

What does this mean?

If we evaluate a vector of one element, we get a new vector with the result of evaluating the contents. But it doesn't work with box. Bug?

(define-symbolic x number?)
(define bx (box x))
(define v (vector x))
(solve (assert (= x 1)))
(evaluate bx)
(evaluate v)

Hi, Does Rosette have a mailing list? Or is there another channel of communication where one can ask questions about Rosette?

Currently bvs show up as (bv -2069063186 32). This is pretty grim to read if you're dealing with large bitvectors. Easier would be hex notation. Can we have a way to request rosette to print them as bitvectors?

Maybe from a param? (set-printing-bv-as-hex! #t)

Then this code:

  #:methods gen:custom-write
  [(define (write-proc self port mode)
     (fprintf port "(bv ~a ~a)" 
              (bv-value self)
(bitvector-size (bv-type self))))])

Could become (untested):

  #:methods gen:custom-write
  [(define (write-proc self port mode)
(if (set-printing-bv-as-hex!)
     (fprintf port "(bv 0x~x ~a)" 
              (bv-value self)
(bitvector-size (bv-type self)))
     (fprintf port "(bv ~a ~a)" 
              (bv-value self)
(bitvector-size (bv-type self))))])

The documentation for synthesize specifies a list of constants as the #:forall expression, but arbitrary expressions seem to be allowed.

#lang rosette
(define-symbolic x c integer?)
(synthesize #:forall (list 1) ;; should this error?
                   #:guarantee (assert (odd? (+ x c))))

Should the contract in the documentation be enforced?

I've got some Wallingford code that works using this function:

(define (button-pressed)
(if (member symbolic-time button-down-event-times) #t #f))

but not the clean version:

(define (button-pressed)
(member symbolic-time button-down-event-times))

Is this a bug? I distilled out some code to exhibit this, which is in reactive/bug.rkt in the Wallingford repository at https://github.com/alanborning/wallingford.git

If you run the code in the repository it prints out:
button is pressed at time 3
button is pressed at time 8
button is pressed at time 10
advanced time to 100

If you change the button-pressed function it doesn't catch the button pressed events.

Evaluating:

(bvand (bv -1 4) (if b (bv 3 4) (bv 2 4)))

where b is (define-symbolic b boolean?), produces:

(ite b49 (bv 3 4) (bv 2 4))

But evaluating:

(bvshl (bv -1 4) (if b (bv 3 4) (bv 2 4)))

produces:

(bvshl (bv -1 4) (ite b49 (bv 3 4) (bv 2 4)))

Is this the intended behavior, or should the bvshl operation be pushed into the ite branches, as with bvand?

The Rosette docs say that Racket v6.6 is required, but is this still the case? Racket is currently at v6.10.1. Should it be "6.6 or later"?

I just noticed the very useful with-asserts-only cousin or with-asserts. However, the former is not documented. Maybe it should be added to the docs?

When I try to use verify, I get the error:

../../nix/store/8bfa4iwj4g8q77513i0w31wc5aw7br2z-racket-6.10.1/share/racket/collects/racket/private/kw.rkt:1170:47: solution: unrecognized solver output: #<eof>

I investigated a bit, and I suspect this is happening because Rosette is not looking in my PATH for the z3 binary, but instead in ../../../bin/z3. Indeed, when I reproduce this directory structure from the file I have open in DrRacket, I get a different error instead:

../../../../../nix/store/8bfa4iwj4g8q77513i0w31wc5aw7br2z-racket-6.10.1/share/racket/collects/racket/private/kw.rkt:1170:47: error writing to stream port
  system error: Broken pipe; errno=32

I'm not yet sure what that one's about, but at least it confirms the source of the bad behavior.

Hello,

I can see let is lifted but for is not. However, there's no mention if the special let <label> form is lifted that allows recursion. Is it?

What is in general the best way to determine if a specific form is lifted? Is there some test I can run to see if lifting is occurring?

Is there any practical difference when x is a concrete integer value to do (bv x 32) or (integer->bitvector x (bitvector 32))? If not, is one of them faster?

Perhaps this is not worth fixing with Rosette 2 coming out, but it still seems like interesting (or at least unexpected) behavior to me.

Consider the following program that compares an identity function with an almost identity function that gives the wrong value if it is applied with 16:

#lang s-exp rosette/safe

(define (almost-identity x)
  (if (= x 16)
      17
      x))

(define (identity x)
  x)

(define (same id1 id2 x)
  (assert (= (id1 x) (id2 x))))

(define-symbolic i number?)
(define cex (verify (same identity almost-identity i)))

Rosette correctly determines that these are not the same function (and if I 'fix' almost-identity to be an actual identity function it also correctly fails to find a counter example).

However, the counter example it produces does not seem correct:

> cex
(model
 [i -16])

If we change almost-identity to break on 17, the i in the counter example changes to -15, 18 turns to -14 and so on up until 32 turns into 0. After that it seems to wrap between 0 and 32, depending on the value passed into it.

I'm wondering if this is related to the Java portion of the solver, where counter examples are only given a nibble of memory.

For what it's worth though, it does seem to correctly identify when something is wrong, just not why.

I am not able use the (z3) wrapper as described here

sumith1896@yoda:~/uwplse/ml$ racket solver-test.rkt 
solver-test.rkt:6:17: z3: unbound identifier in module
  in: z3
  context...:
   /home/sumith1896/uwplse/rosette/rosette/base/form/module.rkt:16:0
   standard-module-name-resolver

Hi, I'm trying to solving constraints on reals. The following is my code.

(define (close-to? a b) (< (abs (- a b)) 0.1))

(define-symbolic x real?)

(solve (begin
(assert (close-to? x 3))
))

However, it just return unsat. Is there any solution for asserting a real number equals to a certain value?

And another question, could Rosette solve strings? like (define-symbolic x string?)

It seems that Z3 for Linux that Rosette uses (https://github.com/emina/rosette/releases/download/v2.0/z3-d89c39cb-x64-ubuntu-14.04.zip) has some bugs and outdated:

~/.racket/6.8/pkgs/rosette/bin $ cat test.smt2
(declare-const root1i Real)
(declare-const root2i Real)
(assert (forall ((xi Real)) (= (* (+ xi root1i) (+ xi root2i)) (+ (* xi xi) (* -198.0 xi) -39483.0))))
(check-sat)
(get-model)
(exit)
~/.racket/6.8/pkgs/rosette/bin $ ./z3 --version
~/.racket/6.8/pkgs/rosette/bin $ ./z3 -smt2 test.smt2
unknown
(error "line 5 column 10: model is not available")

This works fine on Windows, and on online Z3 (http://rise4fun.com/Z3/) which should give the following output:

sat
(model 
  (define-fun root1i () Real
    (- 321.0))
  (define-fun root2i () Real
    123.0)
)

This is more of a question rather than an issue.

The following example, derived from the example at the beginning of Sec 4.4 of the guide, produces a different result depending on whether the (f 1) is commented or uncommented:

#lang rosette
(define-symbolic f (~> integer? boolean?))
(define-symbolic x integer?)
(f 1) ; the existence of this expression changes the solver output
(define sol
  (solve
   (assert
    (not (equal? (f x) (f 1))))))
(define g (evaluate f sol))
(g x) ; (= 0 x) vs (= 1 x)

I realize that solve may produce any satisfactory result, but I can't figure out how the (f 1) above affects the solver output. Is there some state that is changed? (The assertion store seems to be unchanged.)

This behavior is somewhat problematic for us because it complicates unit testing.

I implemented a threaded solver based on rosette and thought all was fine until I started getting the very strange error:

.racket/6.12/pkgs/rosette/rosette/solver/smt/z3.rkt:104:printf: output port is closed

After digging in rosette code and some attempts to reproduce this I found the issue:

#lang rosette

(current-bitwidth #f)

;; Issues 100 threads
(define thds
  (for/list ([i (in-range 100)])
    (thread
     (thunk
      (define-symbolic* v z integer?)
      (sleep (random))
      (verify
       (assert (and (> v 0)
                    (not (= z 0))
                    (= (* z v) 0))))))))

(for ([thd (in-list thds)])
  (thread-wait thd))

(printf "Done")

This generates a bunch of horrible errors. It turns out rosette is not thread safe. I understand the decision, however I wonder what's the best way to get rosette to behave under several threads.

I can imagine two ways:

1. Implement thread safety into rosette by ensuring that each thread can have a solver instance. Not completely sure how to approach this yet but it's certainly feasible.
2. Implement thread safety at the application level by assuming rosette is not thread safety and creating a lock on rosette usage.

Do you have any thoughts on this?

I wanted to do a simple define-synthax, something like the following:

(define-synthax (??const-or-var var-names ...)
  [choose
   (const (??))
   (var var-names) ...
  ])

Which should correspond to the following non-recursive grammar:

const-or-var ::= (const integer) | (var var-name)
var-name ::= var-names ...

However I get an error:

#%datum: identifier's binding is ambiguous
  at phase: 1
  in: #%datum

With the simple change of adding #:assert #tto the define-synthax, this error goes away and the grammar seems to create the right values. The docs say the assert is optional, and my understanding was that it was for making sure recursive grammars bottomed-out, so for a non-recursive grammar like mine, it shouldn't be needed.

Maybe I'm not understanding that with … the grammar becomes recursive anyway?

Hello.

I think your video where you explain Rosette should be added to Rosette homepage somewhere (http://emina.github.io/rosette/): https://youtu.be/KpDyuMIb_E0

Or perhaps it's already there and I'm not seeing it?

It's an extremely good introduction.

Congrats btw. Your work is very impressive and I think you should be awarded for it.

Cheers!

#lang rosette/safe

(define-symbolic x integer?)

(define (f x)
  (cond
    [(= x 543) 1]
    [else "asd"]))

(solve (assert (integer? (f x))))

results in (unsat). Perhaps integer? is not designed to be used in this way and therefore should be prohibited?

Z3 handles large distinct constraints (> 32 operands) involving uninterpreted functions differently, and Rosette doesn't recognize the changed solution format. I think that the extra output can just be thrown away, as it looks to be an artifact of Z3's internal algorithm for handling these constraints.

Example Rosette code:

Welcome to Racket v6.6.
> 
(define (test n)
  (current-bitwidth #f)
  (define-symbolic f (~> integer? integer?))
  (printf "trying ~a inputs...\n" n)
  (let ([xs (build-list n identity)])
    (solve (assert (apply distinct? (map f xs))))))
> (test 32) ; this succeeds, as expected
(model
 [f (fv (((0) . 32) ((1) . 33) ((2) . 34) ((3) . 35) ((4) . 36) ((5) . 37) ((6) . 38) ((7) . 39) ((8) . 40) ((9) . 41) ((10) . 42) ((11) . 43) ((12) . 44) ((13) . 45) ((14) . 46) ((15) . 47) ((16) . 48) ((17) . 49) ((18) . 50) ((19) . 51) ((20) . 52) ((21) . 53) ((22) . 54) ((23) . 55) ((24) . 56) ((25) . 57) ((26) . 58) ((27) . 59) ((28) . 60) ((29) . 61) ((30) . 62) ((31) . 63)) 32 integer?~>integer?)])
> (test 33) ; this triggers an error
trying 33 inputs...
match: no matching clause for '(declare-fun distinct-elems!0!val!0 () distinct-elems!0)
  context...:
   /Applications/Racket v6.6/collects/racket/match/runtime.rkt:24:0: match:error
   ~/Development/rosette/rosette/solver/smt/smtlib2.rkt:25:10: for-loop
   ~/Development/rosette/rosette/solver/smt/cmd.rkt:60:0: decode
   ~/Development/rosette/rosette/query/core.rkt:58:0: ∃-solve10
   /Applications/Racket v6.6/collects/racket/private/misc.rkt:88:7
> 

You can see the difference in output formats when invoking Z3 manually, as well.

Content of test32.z3:

(declare-fun f (Int) Int)
(assert (distinct (f 0) (f 1) (f 2) (f 3) (f 4) (f 5) (f 6) (f 7) (f 8) (f 9) (f 10) (f 11) (f 12) (f 13) (f 14) (f 15) (f 16) (f 17) (f 18) (f 19) (f 20) (f 21) (f 22) (f 23) (f 24) (f 25) (f 26) (f 27) (f 28) (f 29) (f 30) (f 31)))
(check-sat)
(get-model)

Output of z3 test32.z3:

sat
(model 
  (define-fun f ((x!1 Int)) Int
    (ite (= x!1 0) 32
    (ite (= x!1 1) 33
    (ite (= x!1 2) 34
    (ite (= x!1 3) 35
    (ite (= x!1 4) 36
    (ite (= x!1 5) 37
    (ite (= x!1 6) 38
    (ite (= x!1 7) 39
    (ite (= x!1 8) 40
    (ite (= x!1 9) 41
    (ite (= x!1 10) 42
    (ite (= x!1 11) 43
    (ite (= x!1 12) 44
    (ite (= x!1 13) 45
    (ite (= x!1 14) 46
    (ite (= x!1 15) 47
    (ite (= x!1 16) 48
    (ite (= x!1 17) 49
    (ite (= x!1 18) 50
    (ite (= x!1 19) 51
    (ite (= x!1 20) 52
    (ite (= x!1 21) 53
    (ite (= x!1 22) 54
    (ite (= x!1 23) 55
    (ite (= x!1 24) 56
    (ite (= x!1 25) 57
    (ite (= x!1 26) 58
    (ite (= x!1 27) 59
    (ite (= x!1 28) 60
    (ite (= x!1 29) 61
    (ite (= x!1 30) 62
    (ite (= x!1 31) 63
      32)))))))))))))))))))))))))))))))))
)

Content of test33.z3:

(declare-fun f (Int) Int)
(assert (distinct (f 0) (f 1) (f 2) (f 3) (f 4) (f 5) (f 6) (f 7) (f 8) (f 9) (f 10) (f 11) (f 12) (f 13) (f 14) (f 15) (f 16) (f 17) (f 18) (f 19) (f 20) (f 21) (f 22) (f 23) (f 24) (f 25) (f 26) (f 27) (f 28) (f 29) (f 30) (f 31) (f 32)))
(check-sat)
(get-model)

Output of z3 test33.z3:

sat
(model 
  ;; universe for distinct-elems!0:
  ;;   distinct-elems!0!val!0 distinct-elems!0!val!10 distinct-elems!0!val!18 distinct-elems!0!val!30 distinct-elems!0!val!19 distinct-elems!0!val!32 distinct-elems!0!val!20 distinct-elems!0!val!27 distinct-elems!0!val!3 distinct-elems!0!val!15 distinct-elems!0!val!16 distinct-elems!0!val!1 distinct-elems!0!val!8 distinct-elems!0!val!17 distinct-elems!0!val!24 distinct-elems!0!val!21 distinct-elems!0!val!23 distinct-elems!0!val!12 distinct-elems!0!val!2 distinct-elems!0!val!4 distinct-elems!0!val!31 distinct-elems!0!val!29 distinct-elems!0!val!11 distinct-elems!0!val!13 distinct-elems!0!val!9 distinct-elems!0!val!25 distinct-elems!0!val!28 distinct-elems!0!val!7 distinct-elems!0!val!6 distinct-elems!0!val!5 distinct-elems!0!val!14 distinct-elems!0!val!26 distinct-elems!0!val!22 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun distinct-elems!0!val!0 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!10 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!18 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!30 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!19 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!32 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!20 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!27 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!3 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!15 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!16 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!1 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!8 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!17 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!24 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!21 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!23 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!12 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!2 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!4 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!31 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!29 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!11 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!13 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!9 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!25 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!28 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!7 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!6 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!5 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!14 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!26 () distinct-elems!0)
  (declare-fun distinct-elems!0!val!22 () distinct-elems!0)
  ;; cardinality constraint:
  (forall ((x distinct-elems!0))
          (or (= x distinct-elems!0!val!0)
              (= x distinct-elems!0!val!10)
              (= x distinct-elems!0!val!18)
              (= x distinct-elems!0!val!30)
              (= x distinct-elems!0!val!19)
              (= x distinct-elems!0!val!32)
              (= x distinct-elems!0!val!20)
              (= x distinct-elems!0!val!27)
              (= x distinct-elems!0!val!3)
              (= x distinct-elems!0!val!15)
              (= x distinct-elems!0!val!16)
              (= x distinct-elems!0!val!1)
              (= x distinct-elems!0!val!8)
              (= x distinct-elems!0!val!17)
              (= x distinct-elems!0!val!24)
              (= x distinct-elems!0!val!21)
              (= x distinct-elems!0!val!23)
              (= x distinct-elems!0!val!12)
              (= x distinct-elems!0!val!2)
              (= x distinct-elems!0!val!4)
              (= x distinct-elems!0!val!31)
              (= x distinct-elems!0!val!29)
              (= x distinct-elems!0!val!11)
              (= x distinct-elems!0!val!13)
              (= x distinct-elems!0!val!9)
              (= x distinct-elems!0!val!25)
              (= x distinct-elems!0!val!28)
              (= x distinct-elems!0!val!7)
              (= x distinct-elems!0!val!6)
              (= x distinct-elems!0!val!5)
              (= x distinct-elems!0!val!14)
              (= x distinct-elems!0!val!26)
              (= x distinct-elems!0!val!22)))
  ;; -----------
  (define-fun unique-value!3 () distinct-elems!0
    distinct-elems!0!val!1)
  (define-fun unique-value!6 () distinct-elems!0
    distinct-elems!0!val!4)
  (define-fun unique-value!5 () distinct-elems!0
    distinct-elems!0!val!3)
  (define-fun unique-value!7 () distinct-elems!0
    distinct-elems!0!val!5)
  (define-fun unique-value!12 () distinct-elems!0
    distinct-elems!0!val!10)
  (define-fun unique-value!21 () distinct-elems!0
    distinct-elems!0!val!19)
  (define-fun unique-value!22 () distinct-elems!0
    distinct-elems!0!val!20)
  (define-fun unique-value!17 () distinct-elems!0
    distinct-elems!0!val!15)
  (define-fun unique-value!28 () distinct-elems!0
    distinct-elems!0!val!26)
  (define-fun unique-value!30 () distinct-elems!0
    distinct-elems!0!val!28)
  (define-fun unique-value!16 () distinct-elems!0
    distinct-elems!0!val!14)
  (define-fun unique-value!23 () distinct-elems!0
    distinct-elems!0!val!21)
  (define-fun unique-value!14 () distinct-elems!0
    distinct-elems!0!val!12)
  (define-fun unique-value!9 () distinct-elems!0
    distinct-elems!0!val!7)
  (define-fun unique-value!4 () distinct-elems!0
    distinct-elems!0!val!2)
  (define-fun unique-value!32 () distinct-elems!0
    distinct-elems!0!val!30)
  (define-fun unique-value!33 () distinct-elems!0
    distinct-elems!0!val!31)
  (define-fun unique-value!24 () distinct-elems!0
    distinct-elems!0!val!22)
  (define-fun unique-value!34 () distinct-elems!0
    distinct-elems!0!val!32)
  (define-fun unique-value!20 () distinct-elems!0
    distinct-elems!0!val!18)
  (define-fun unique-value!10 () distinct-elems!0
    distinct-elems!0!val!8)
  (define-fun unique-value!25 () distinct-elems!0
    distinct-elems!0!val!23)
  (define-fun unique-value!29 () distinct-elems!0
    distinct-elems!0!val!27)
  (define-fun unique-value!18 () distinct-elems!0
    distinct-elems!0!val!16)
  (define-fun unique-value!13 () distinct-elems!0
    distinct-elems!0!val!11)
  (define-fun unique-value!2 () distinct-elems!0
    distinct-elems!0!val!0)
  (define-fun unique-value!8 () distinct-elems!0
    distinct-elems!0!val!6)
  (define-fun unique-value!19 () distinct-elems!0
    distinct-elems!0!val!17)
  (define-fun unique-value!15 () distinct-elems!0
    distinct-elems!0!val!13)
  (define-fun unique-value!26 () distinct-elems!0
    distinct-elems!0!val!24)
  (define-fun unique-value!11 () distinct-elems!0
    distinct-elems!0!val!9)
  (define-fun unique-value!31 () distinct-elems!0
    distinct-elems!0!val!29)
  (define-fun unique-value!27 () distinct-elems!0
    distinct-elems!0!val!25)
  (define-fun f ((x!1 Int)) Int
    (ite (= x!1 0) 33
    (ite (= x!1 1) 34
    (ite (= x!1 2) 35
    (ite (= x!1 3) 36
    (ite (= x!1 4) 37
    (ite (= x!1 5) 38
    (ite (= x!1 6) 39
    (ite (= x!1 7) 40
    (ite (= x!1 8) 41
    (ite (= x!1 9) 42
    (ite (= x!1 10) 43
    (ite (= x!1 11) 44
    (ite (= x!1 12) 45
    (ite (= x!1 13) 46
    (ite (= x!1 14) 47
    (ite (= x!1 15) 48
    (ite (= x!1 16) 49
    (ite (= x!1 17) 50
    (ite (= x!1 18) 51
    (ite (= x!1 19) 52
    (ite (= x!1 20) 53
    (ite (= x!1 21) 54
    (ite (= x!1 22) 55
    (ite (= x!1 23) 56
    (ite (= x!1 24) 57
    (ite (= x!1 25) 58
    (ite (= x!1 26) 59
    (ite (= x!1 27) 60
    (ite (= x!1 28) 61
    (ite (= x!1 29) 62
    (ite (= x!1 30) 63
    (ite (= x!1 31) 64
    (ite (= x!1 32) 65
      33))))))))))))))))))))))))))))))))))
  (define-fun distinct-aux-f!!1 ((x!1 Int)) distinct-elems!0
    (ite (= x!1 33) distinct-elems!0!val!0
    (ite (= x!1 34) distinct-elems!0!val!1
    (ite (= x!1 35) distinct-elems!0!val!2
    (ite (= x!1 36) distinct-elems!0!val!3
    (ite (= x!1 37) distinct-elems!0!val!4
    (ite (= x!1 38) distinct-elems!0!val!5
    (ite (= x!1 39) distinct-elems!0!val!6
    (ite (= x!1 40) distinct-elems!0!val!7
    (ite (= x!1 41) distinct-elems!0!val!8
    (ite (= x!1 42) distinct-elems!0!val!9
    (ite (= x!1 43) distinct-elems!0!val!10
    (ite (= x!1 44) distinct-elems!0!val!11
    (ite (= x!1 45) distinct-elems!0!val!12
    (ite (= x!1 46) distinct-elems!0!val!13
    (ite (= x!1 47) distinct-elems!0!val!14
    (ite (= x!1 48) distinct-elems!0!val!15
    (ite (= x!1 49) distinct-elems!0!val!16
    (ite (= x!1 50) distinct-elems!0!val!17
    (ite (= x!1 51) distinct-elems!0!val!18
    (ite (= x!1 52) distinct-elems!0!val!19
    (ite (= x!1 53) distinct-elems!0!val!20
    (ite (= x!1 54) distinct-elems!0!val!21
    (ite (= x!1 55) distinct-elems!0!val!22
    (ite (= x!1 56) distinct-elems!0!val!23
    (ite (= x!1 57) distinct-elems!0!val!24
    (ite (= x!1 58) distinct-elems!0!val!25
    (ite (= x!1 59) distinct-elems!0!val!26
    (ite (= x!1 60) distinct-elems!0!val!27
    (ite (= x!1 61) distinct-elems!0!val!28
    (ite (= x!1 62) distinct-elems!0!val!29
    (ite (= x!1 63) distinct-elems!0!val!30
    (ite (= x!1 64) distinct-elems!0!val!31
    (ite (= x!1 65) distinct-elems!0!val!32
      distinct-elems!0!val!0))))))))))))))))))))))))))))))))))
)

On the bitvector documentation at:
https://docs.racket-lang.org/rosette-guide/sec_bitvectors.html

You can see right at the beginning:

> (bv 4 (bitvector 7))        ; a bitvector literal of size 7
--
warning: could not find z3 executable in '/home/racket/build-pkgs/user/.racket/6.11/pkgs/rosette/bin/z3.exe/'
(bv 4 7)

I assume that warning was not supposed to be there.

Hello,

I am trying to prove that forall bitvector x0...xY F. However, I keep getting unsat. So I did a small experiment whose solution looked pretty obvious:

(current-bitwidth 32)

(define-symbolic x0 (bitvector 32))

(define sol (synthesize #:forall (list x0)
                        #:assume (assert (bvsgt x0 0))
                        #:guarantee (assert (bvsgt (bvmul x0 (integer->bitvector 2 (bitvector 32))) 
                                                                   x0))))

(if (unsat? sol)
    (printf "unsat core: ~a~n" (core sol))
    (printf "solution: ~a~n" sol))

It seems to me that if you assume that x0 is always positive, then 2*x0 should be always larger than x0. However, this returns unsat which I take it to mean that there is an x0 for which this does not hold.

Then I thought, ok, lets try to find a situation where this is not true and added:

(solve (assert (=> (bvsgt x0 0) 
                             (! (bvsgt (bvmul x0 (integer->bitvector 2 (bitvector 32))) x0)))))

So, assume that x0 > 0, for which value 2*x0 is not larger than x0? It turns out I get unsat as well. I am certainly failing to understand what's the problem. It just occurred to me that it might be related to multiplication overflow, but still I would get have expected to find a value for x0 in the solve call that would show it to me.

It seems (but it might be my misunderstanding) that synthesize is returning sat for an unsatisfiable model.

#lang rosette

(define-symbolic input2 input3 (bitvector 32))
(define bv1 (bv 1 (bitvector 32)))

(define formula
  (bveq (bvadd bv1 (bvadd bv1 input3))
        (bvadd input2 (sign-extend (integer->bitvector 16 (bitvector 11))
                                   (bitvector 32)))))

(synthesize
 #:forall '(input2 input3)
 #:guarantee formula)

This return an empty model, which means it's sat. Why?
This as far as I am concerned checks if for all possible values of input2 and input3: input3 + 1+ 1 = input2 + 16 which is obviously not true for all possible values of input2 and input3.

In the lifted forms documentation [1] there is a reference to lifted value let-values and define-values but no reference to values. It seems this is an omission. It doesn't seem to make sense to lift let-values and define-values which are values consumers but not values, the values producer.

Am I correct into thinking, therefore that values is also lifted but not documented?

1. http://docs.racket-lang.org/rosette-guide/ch_syntactic-forms_racket.html?q=rosette

Apologies in advance if this is not the best place for requests/questions.

I have a bitvector and an integer and I need to shift the bitvector by the integer amount. How can I convert the integer to a bitvector if I have no accessor for the integer size. With an accessor bv-size I could do: (bvshl my-bv (bv my-int (bv-size my-bv))).

Can we get a bv-size if it doesn't exist yet?

I think there might be a problem with xor. Is it supposed to allow non-booleans?

> (xor 11 #t)
(! 11)
> (xor 11 #f)
. . rosette/rosette/base/core/term.rkt:67:0: term-ord: contract violation
  expected: term?
  given: 11

If I run a program like this:

#lang rosette/safe
(require rosette/query/debug rosette/lib/render
         (for-syntax syntax/transformer))

(define-syntax add (make-variable-like-transformer #'+))
(define-syntax mult (make-variable-like-transformer #'*))

(define (poly x)
  (add (mult x x x x) (mult 6 x x x) (mult 11 x x) (mult 6 x)))

(define/debug (factored x)
  (mult x (add x 1) (add x 2) (add x 2)))

(define (same p f x)
  (assert (= (p x) (f x))))

(define ucore (debug [integer?] (same poly factored 12)))
(render ucore)

Rosette tries to render something in the definition of make-variable-like-transformer instead of the definition of the factored function in define/debug.

quasiquote can sometimes create symbolic lists that you can't take the length of. This seems to be an issue specifically when the symbolic list is represented as a pair with For example:

(define-symbolic b boolean?)
(define sym-list (if b '(bar) '(bar baz)))
(define thing `(foo ,@sym-list))
(print thing) (newline)
(print (length thing)) (newline)

prints:

'(foo . {[b (bar)] [(! b) (bar baz)]})
length: contract violation
  expected: #
  given: '(foo . {[b (bar)] [(! b) (bar baz)]})
  context...:
   @length
   /.../tmp.rkt: [running body]

While this throws an error, I also have a much larger codebase where it just returns the wrong result (it says the length is definitely 2 when I'm fairly confident it should be either 3 or 4). I haven't been able to create a smaller example showing this behavior.

This code works fine if you replace the quasiquote with (cons 'foo sym-list), producing the output:

{[b '(foo bar)] [(! b) '(foo bar baz)]}
(ite b 2 3)

So it looks like length can only work with symbolic lists which are not represented with dotted-tail notation (that is, as a pair with a symbolic car and symbolic cdr). So far I've only been able to construct such a symbolic list with quasiquote.

I noticed that there's no definition of quasiquote in Rosette, is it not supposed to be used? The docs say that it should work: https://docs.racket-lang.org/rosette-guide/ch_syntactic-forms_racket.html

As far as I understand it rosette supports cond with no exceptions (at least, they are not mentioned in the docs).

However this does not work:

#lang rosette
(define v 3)

(cond [v => identity]
      [else 2])

This returns #<procedure:identity>. In #lang racket returns, as it should 3.

After running in racket 6.11 with latest rosette:

#lang rosette

(define opvec (vector 'foo 'bar 'baz 'tar 'taz))

(define-struct insn
  (op
   args-vec))

(define-symbolic* op integer?)
(define-symbolic* arg1 (bitvector 32))
(define-symbolic* arg2 (bitvector 32))

(define-symbolic* res (bitvector 32))

(define i1
  (insn op
        (vector arg1 arg2)))

(define (inter b)
  (case (vector-ref opvec (insn-op b))
    [(foo)
     (printf "rosette: interpreting foo~n")
     (void)]

    [(baz)
     (printf "rosette: interpreting baz~n")
     (set! res (vector-ref (insn-args-vec b)
                           0))]

    [(tar)
     (printf "rosette: interpreting tar~n")
     (set! res (bvadd (vector-ref (insn-args-vec b) 0)
                      (vector-ref (insn-args-vec b) 1)))]

    [else
     (assert #f "unknown op")]))

(printf "store~n")
(pretty-print (asserts))

(inter i1)

(printf "store after inter~n")
(pretty-print (asserts))

I get:

Welcome to DrRacket, version 6.11 [3m].
Language: rosette, with debugging; memory limit: 2048 MB.
store
'()
rosette: interpreting foo
rosette: interpreting baz
rosette: interpreting tar
store after inter
(list
 (|| (= 3 op$0) (! (&& (! (= 0 op$0)) (! (= 2 op$0)))))
 (|| (= 3 op$0) (! (&& (! (= 0 op$0)) (! (= 2 op$0)))))
 (< op$0 5)
 (<= 0 op$0))

However, (|| (= 3 op$0) (! (&& (! (= 0 op$0)) (! (= 2 op$0))))) and (|| (= 3 op$0) (! (&& (! (= 0 op$0)) (! (= 2 op$0))))) are equivalent. Why are we adding these to the store? Even if the solver discards one of them later, surely it would be better not to add them to start with.

Try
https://emina.github.io/rosette/search/index.html?q=bvshl

Can the output of union-contents contain symbolic unions?

The docs say that it cannot but I'm running into some cases where it does (trying to create a small example).

Would an assert-like form that returns a value be useful to Rosette programmers? It would return the value that the programmer annotates, but with some paths pruned using the additional information.

A hypothetical assert-pred would behave like:

(define-symbolic b1 b2 boolean?)
(define-symbolic i1 i2 integer?)
(assert-pred i1 positive?) ; => i1, with (< 0 i1) added to the assertion store
(assert-pred (if b1 i2 b2) integer?) ; => i2, with b1 added to the assertion store

There are no paths to merge in the first assert-pred, but the second assert-pred eliminates the b2 branch. Essentially, assert-pred allows programmers to help Rosette's path merging (if possible), at a higher point in the tree.

Does Rosette already support something like this? Would Rosette programmers ever want such an optimization?