Rosette returns integer? but the symbol is real?.

[chansey97]

For example,

(define-symbolic a real?)
(let ((sol (solve (assert (= a 2.0)))))
  (evaluate a sol))
;; 2

I defined a real? a and = with an inexact number 2.0, the expected result should also be inexact 2.0 instead of exact 2. So the current rosette's result is not very natural.

Also, SMT-LIB return 2.0 instead of 2.

(set-option :auto-config true)
(set-option :produce-unsat-cores false)
(set-option :smt.mbqi.max_iterations 10000000)
(set-option :smt.relevancy 2)
(declare-fun c0 () Real)
(define-fun e1 () Bool (= 2 c0))
(assert e1)
(check-sat)
(get-model)
sat
(
  (define-fun c0 () Real
    2.0)
  (define-fun e1 () Bool
    (= 2.0 c0))
)

It is better to keep the SMT result type.

This patch fix the problem.

(define-symbolic a real?)
(let ((sol (solve (assert (= a 2.0)))))
  (evaluate a sol))
;; 2.0

I also tried a with integer?, it is no problem.

(define-symbolic a integer?)
(let ((sol (solve (assert (= a 2.0)))))
  (evaluate a sol))
;; 2

P.s. The current dec code of rosette seems to ignore SMT type. It is better to infer values' type based on symbol definition, but that is another story.

[emina]

Thank you for reporting this issue!

Rosette follows Racket conventions, so this isn't a bug in the sense that 2 is both a real? and an integer?.

But I agree that it's preferable to pass on the literals returned by the solver. I've pushed a fix that has the preferred behavior.