I thought I should start learning about type systems and I came across a term I didn’t > Certain languages, for example https://en.wikipedia.org/wiki/Clojure\|Clojure, <https://en.wikipedia.org/wiki/Common_Lisp|Common Lisp>, or https://en.wikipedia.org/wiki/Cython\|Cython are dynamically type checked by default, but allow programs to opt into static type checking by providing optional annotations. One reason to use such hints would be to optimize the performance of critical sections of a program. This is formalized by <https://en.wikipedia.org/wiki/Type_system#Gradual_typing|gradual typing>. This is formalized by <https://en.wikipedia.org/wiki/Type_system#Gradual_typing|gradual typing>. The programming environment _https://en.wikipedia.org/wiki/DrRacket\|DrRacket_, a pedagogic environment based on Lisp, and a precursor of the language https://en.wikipedia.org/wiki/Racket_(programming_language)#Development\|Racket is also soft-typed. https://en.wikipedia.org/wiki/Type_system#Combining_static_and_dynamic_type_checking

Any idea what ‘*soft-typed*’ is? - it is not defined or mentioned elsewhere in the page.

It’s an older term/idea. From “Practical Soft Typing” by Andrew K. Wright.

https://www.cs.rice.edu/CS/PLT/Publications/Scheme/thesis-wright.ps.gz

thanks!

Another rosette question. (require rosette/solver/smt/z3 rosette/query/debug) (define s (z3 #:options (hash ':produce-unsat-cores 'true ':smt.relevancy 2 ':smt.mbqi.max_iterations 10000000))) (define-symbolic i (bitvector 32)) (current-solver s) (define c (solve (assert (and (bveq (bv 0 32) i) (bveq (bv 1 32) i))))) (unsat? c) > #t (core c) > #f ==== Using the solver directly seems to work (solver-assert s (list (bveq (bv 0 32) i) (bveq (bv 1 32) i))) (solver-debug s) > (core (bveq (bv #x00000000 32) i) (bveq (bv #x00000001 32) i)) I assume I’m not configuring the solver correctly to get the unsat core, but I couldnt find anything in the source/docs to help point me at the correct instantiation

You can’t use solve to get an unsat core

I also tried debug but it only respected the provided expr and not any of the other asserts previously made.

Is there a function I’m missing?

(assert (bveq (bv 0 32) i)) (assert (bveq (bv 1 32) i)) (debug i) code in case that’s helpful

I guess the question I need to ask is, what are you trying to do? Are you using Rosette for its symbolic evaluation? Or simply as an interface to an SMT solver?

For the latter, your second approach is the right one (just use the solver directly)

For symbolic evaluation. I just tried to distill the core problem to focus the discussion

Ah, OK. I think the short answer is that there’s no good way to do that, simply because the information unsat cores provided usually is not useful much (according to Emina), so we don’t really support it.

If you are OK with hacking Rosette internals, you can create a new solver

https://github.com/emina/rosette/blob/master/rosette/solver/smt/z3.rkt

Just copy this file, and change solver-check: https://github.com/emina/rosette/blob/master/rosette/solver/smt/z3.rkt#L76

Ha! while we were having this discussion I did exactly that and I’m slowly discovering that the information unsat core is producing isnt that helpful :stuck_out_tongue:

“exactly” ~= quickly hacking it in the repl, not a robust solution

As always thank you @sorawee

you are welcome!