emina / rosette

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

Minimization causes read-solution: unrecognized solver output: (error line 262 column 10: maximization suspended) #249

Closed pmatos closed 1 year ago

pmatos commented 1 year ago

I am playing with a minimization example and getting the following error:

../../.local/share/racket/8.7/pkgs/rosette/rosette/query/form.rkt:76:5: read-solution: unrecognized solver output: (error line 262 column 10: maximization suspended)

Code is as follows:

#lang rosette/safe

(define-symbolic B W integer?)

(define-symbolic c d e f g a b integer?)
(define-symbolic Bc2 Bd1 Bd2 Be1 Bf2 Bg1 Bg2 Ba1 Ba2 Bb1 integer?)
(define keys (list c d e f g a b))
(define black-partial (list Bc2 Bd1 Bd2 Be1 Bf2 Bg1 Bg2 Ba1 Ba2 Bb1))

(assert (= (* 7 W) 5880))
(assert (= W (+ c Bc2)))
(assert (= W (+ d Bd1 Bd2)))
(assert (= W (+ e Be1)))
(assert (= W (+ f Bf2)))
(assert (= W (+ g Bg1 Bg2)))
(assert (= W (+ a Ba1 Ba2)))
(assert (= W (+ b Bb1)))

(assert (= B (+ Bc2 Bd1)))
(assert (= B (+ Bd2 Be1)))
(assert (= B (+ Bf2 Bg1)))
(assert (= B (+ Bg2 Ba1)))
(assert (= B (+ Ba2 Bb1)))

(define (combinations-2 x)
  (cond
    [(< (length x) 2) '()]
    [else
     (append (map (lambda (k) (list (car x) k)) (cdr x))
             (combinations-2 (cdr x)))]))

(define-symbolic max-diff real?)

(assert
 (= max-diff
    (foldl
     (lambda (p r)
       (max (abs (- (car p) (cadr p))) r))
     0
     (combinations-2 (cons B keys)))))

(define (buckets n)
  (length (remove-duplicates n)))

(for-each (lambda (k) (assert (> k B))) keys)
(for-each (lambda (k) (assert (> k 0))) black-partial)

(assert (= (* W 3) (+ c d e (* 2 B))))
(assert (= (* W 4) (+ f g a b (* 3 B))))

(assert (= d g 490))

; Reduce variability
(define-symbolic variability real?)
(define (square x) (* x x))
(set! variability
      (/ (apply +
             (cons (* 5 (square (- B 490)))
                   (map (lambda (k)
                          (square (- k 490)))
                        keys)))
         12))

(define sol (optimize #:minimize (list max-diff variability) #:guarantee #true))
sol
(when (sat? sol)
  (printf "Variability: ~a~n" (/ (evaluate variability sol) 12.0))
  (printf "best is B / ~a~n" (* (evaluate max-diff sol) (evaluate B sol))))
sorawee commented 1 year ago

What version of Z3 are you using? This looks like a Z3 bug. Here's what I found from a quick search: https://github.com/Z3Prover/z3/issues/5212.