search

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
638 stars 74 forks source link

EOF error when using bitwuzla #275

Closed jieqiu0630 closed 8 months ago

jieqiu0630 commented 8 months ago

Hi! When running part2_listbound5_seed1.rkt file in issue.zip, which uses bitwuzla as the solver, I'm seeing an error with the following trace:

read-solution: unrecognized solver output: #<eof>
  context...:
  rosette/rosette/solver/smt/base-solver.rkt:136:0: read-solution
  rosette/rosette/solver/smt/base-solver.rkt:95:0: solver-check
  rosette/rosette/query/core.rkt:157:2: guess
  rosette/rosette/query/core.rkt:151:0: cegis
  rosette/rosette/query/core.rkt:129:6
  body of "part2_listbound5.rkt"
  rosette/rosette/lib/profile/record.rkt:152:6
  rosette/rosette/lib/profile/record.rkt:146:0: run-profile-thunk
  rosette/rosette/lib/profile/tool.rkt:12:0: profile-thunk
  body of "rosette/rosette/lib/profile/raco.rkt"
  /Applications/Racket v8.8/collects/raco/raco.rkt:41:0
  body of "/Applications/Racket v8.8/collects/raco/raco.rkt"
  body of "/Applications/Racket v8.8/collects/raco/main.rkt"

cc: @sahilbhatia17

sorawee commented 8 months ago

Could you provide bounded.rkt and utils.rkt (and any transitive dependencies) as well?

jieqiu0630 commented 8 months ago

Could you provide bounded.rkt and utils.rkt (and any transitive dependencies) as well?

Just zipped everything and uploaded!

sorawee commented 8 months ago

I can reproduce the issue. It appears that the communication with bitwuzla abruptly ended, causing a malformed SMT-LIB encoding.

... 6905602 lines ...
(define-fun e6905601 () (_ BitVec 6) (bvor (ite e4760375 e6905548 (_ bv0 6)) (ite e4760376 e6905516 (_ bv0 6)) (ite e4760377 e6905484 (_ bv0 6)) (ite e4760378 e6905453 (_ bv0 6)) (ite e4760379 e6905422 (_ bv0 6)) (ite e4760380 e6905391 (_ bv0 6)) (ite e4760381 e6905360 (_ bv0 6)) (ite e4760382 e6905331 (_ bv0 6)) (ite e4760383 e6905302 (_ bv0

I will continue to investigate. One possibility is that Bitwuzla couldn't handle this large encoding.

sorawee commented 8 months ago

I think Bitwuzla simply uses too much memory, and got killed as a result:

$ time bitwuzla -v 4 out.smt2
[bzla] Preprocessing 2 assertions
[2]    10001 killed     bitwuzla -v 4 out.smt2
bitwuzla -v 4 out.smt2  595.79s user 243.13s system 91% cpu 15:19.17 total

where out.smt2 is the SMT-LIB encoding that Rosette generates.

Toward the end of the process, Activity Monitor for Mac reports that the Bitwuzla takes ~90GB of memory.

Z3 doesn't seem to suffer the same problem. After ~15 mins, it consumes only ~30 GB (peaking at ~40 GB).

So I don't think this is Rosette's fault. What you can try to do is to modify your Rosette programs to generate simpler constraints, and that will likely help with this problem.

You can also report this issue to Bitwuzla, and I'd be happy to provide the SMT-LIB encoding. It's ~600 MB though, so I do not know if it's reasonable to expect this to work.

Since this is not Rosette's fault, I will close the issue, but feel free to add more comments if you have questions.

jieqiu0630 commented 8 months ago

Thank you @sorawee for the quick and thorough help! 🙏🏼