Added objectives extraction that works only for optimizing constants (not expressions).

rosette/solver/smt/cmd.rkt

@@ -4,7 +4,7 @@
                   check-sat get-model get-unsat-core
                   read-solution true false)
          "env.rkt" "enc.rkt"
-         (only-in "../../base/core/term.rkt" constant? term-type solvable-default)
+         (only-in "../../base/core/term.rkt" constant? term-type solvable-default type-of)
          (only-in "../../base/core/function.rkt" fv function? function-domain function-range)
          (only-in "../../base/core/bool.rkt" @boolean?)
          (only-in "../../base/core/bitvector.rkt" bitvector? bv)
@@ -62,7 +62,7 @@
 ; declared or defined in P is bound in (decls env) or (defs env), respectively.
 (define (decode env)
   (match (read-solution)
-    [(? hash? sol) 
+    [(cons (? hash? sol) (? hash? objs))
      (sat (for/hash ([(decl id) (in-dict (decls env))])
             (let ([t (term-type decl)])
               (values decl
@@ -70,7 +70,13 @@
                           (if (function? t)
                               (decode-function t (hash-ref sol id))
                               (decode-value t (hash-ref sol id)))
-                          (solvable-default t))))))]
+                          (solvable-default t)))))
+          (if (hash-empty? objs)
+              (hash)
+              (for/hash ([(obj id) (in-sequences (in-dict (decls env)) (in-dict (defs env)))]
+                         #:when (hash-has-key? objs id))
+                (values obj
+                        (decode-objective (type-of obj) (hash-ref objs id))))))]                
     [(? list? names)
      (unsat (let ([core (apply set (map name->id names))])
               (for/list ([(bool id) (in-sequences (in-dict (decls env)) (in-dict (defs env)))]
@@ -78,6 +84,7 @@
                  bool)))]
     [#f (unsat)]))
 
+
 (define (to-exact-int a) (if (integer? a) (inexact->exact a) a))
 
 (define (decode-value type val)
@@ -132,7 +139,51 @@
         (or (and (equal? p x) y)
             (and (equal? p y) x))]))))
   
+(define (decode-objective type expr)
+  (match expr
+    [(app decode-objective-value (cons val ε))
+     (if (bitvector? type)
+         (interval (bv val type) #t (bv val type) #t)
+         (cond [(zero? ε) (interval val #t val #t)]
+               [(positive? ε) (interval val #f +inf.0 #f)]
+               [else (interval -inf.0 #f val #f)]))]
+    [(list (app decode-objective-value (cons min-val minε))
+           (app decode-objective-value (cons max-val maxε)))
+     (if (bitvector? type)
+         (interval (bv min-val type) #t (bv max-val type) #t)
+         (interval min-val (zero? minε) max-val (zero? maxε)))]))
 
+(define (decode-objective-value expr)
+  (match (normalize-objective-value expr)
+    [(? real? r) (cons r 0)]
+    [(== 'epsilon) (cons 0 1)]
+    [(list (== '*) (? real? r) (== 'epsilon)) (cons 0 r)]
+    [(list (== '+) (? real? r) (== 'epsilon)) (cons r 1)]
+    [(list (== '+) (? real? r) (list (== '*) (? real? s) (== 'epsilon))) (cons r s)]
+    [_ #f]))
+
+(define (normalize-objective-value expr)
+  (match expr
+    [(or (? real?) (== 'epsilon)) expr]
+    [(== 'oo) +inf.0]
+    [(list (== 'to_real) r) r]
+    [(list (== '-) r) (- r)]
+    [(list (== '+) e0 e1)
+     (match* ((normalize-objective-value e0) (normalize-objective-value e1))
+       [((? real? r0) (? real? r1)) (+ r0 r1)]
+       [((? real? r) other) `(+ ,r ,other)]
+       [(other (? real? r)) `(+ ,r ,other)])]
+    [(list (== '*) e0 e1)
+     (match* ((normalize-objective-value e0) (normalize-objective-value e1))
+       [((? real? r0) (? real? r1)) (* r0 r1)]
+       [((? real? r) other) `(* ,r ,other)]
+       [(other (? real? r)) `(* ,r ,other)])]
+    [_ #f]))
+    
+    
+
+  
+     
 
   
 

rosette/solver/smt/smtlib2.rkt

@@ -7,26 +7,34 @@
 
 ; Reads the SMT solution from current-input-port.
 ; The solution consist of 'sat or 'unsat, followed by  
-; followed by a suitably formatted s-expression.  The 
-; output of this procedure is a hashtable from constant 
-; identifiers to their values (if the solution is 'sat);
-; a non-empty list of assertion identifiers that form an
-; unsatisfiable core (if the solution is 'unsat and a 
-; core was extracted); or #f (if the solution is 
-; 'unsat and no core was extracted).
+; followed by a suitably formatted s-expression.
+; If the solution is 'sat, the output of this procedure is a pair of
+; hashtables, where the first table represents the model as a
+; map from constant identifiers to their values, and the second table
+; maps objective terms to values.  If the solution is 'unsat
+; and a core was extracted, the procedure outputs a non-empty 
+; list of assertion identifiers that form an
+; unsatisfiable core.  If the solution is 'unsat and no core was
+; extracted, the output is #f.
 (define (read-solution)
   (define port (current-input-port))
   (match (read port)
     [(== 'sat)
+     (define model (make-hash))
+     (define objectives (make-hash))
      (let loop ()
        (match (read port)
-         [(list (== 'objectives) _ ...) (loop)]
+         [(list (== 'objectives) (list term val) ...)
+          (for ([t term] [v val])
+            (hash-set! objectives t v))
+          (loop)]
          [(list (== 'model) def ...)
-          (for/hash ([d def])
+          (for ([d def])
             (match d
-              [(list (== 'define-fun) c '() _ v) (values c v)]
-              [(list (== 'define-fun) c _ ...) (values c d)]))]
-         [other (error 'solution "expected model, given ~a" other)]))]
+              [(list (== 'define-fun) c '() _ v) (hash-set! model c v)]
+              [(list (== 'define-fun) c _ ...)   (hash-set! model c d)]))]
+         [other (error 'solution "expected model, given ~a" other)]))
+     (cons model objectives)]
     [(== 'unsat) 
      (match (read port) 
        [(list (? symbol? name) ...) name]

rosette/solver/solution.rkt

@@ -1,13 +1,18 @@
 #lang racket
 
 (require "../base/core/term.rkt" 
-         (only-in "../base/core/term.rkt" type-of))
+         (only-in "../base/core/term.rkt" type-of)
+         (only-in "../base/core/bitvector.rkt" bv? @bvsle))
 
-(provide solution? sat? unsat? sat unsat model core)
+(provide solution? sat? unsat? sat unsat model core objectives
+         interval? interval interval-min interval-max
+         interval-includes-min? interval-includes-max?) 
 
 ; Represents the solution to a set of logical constraints.  The solution 
-; has single field, result, which stores either a model of the constraints, 
-; an unsatisfiable core, or #f. 
+; has two fields: result and objectives.  The result field stores either
+; a model of the constraints, an unsatisfiable core, or #f. The objectives
+; field maps optimization objective terms, if any, to intervals indicating the best
+; values those objectives may take in a given solution.  
 ; 
 ; If the constraints are satisfiable, the result is dictionary binding symbolic 
 ; constants to values. In that case, the solution 
@@ -15,20 +20,29 @@
 ; returns a concrete value for that constant, if any, or the constant itself, if the 
 ; model has no binding for that constant.
 ; 
-; If the constraints are unsatisfiable, and no core has been extracted, the result field is #f.
-; If a core has been extracted, the result is a list of constraints (that is @boolean? terms or 
-; values) that do not have a model.
-(struct solution (result)
+; If the constraints are unsatisfiable, and no core has been extracted, the result
+; field is #f.  If a core has been extracted, the result is a list of constraints
+; (that is @boolean? terms or values) that do not have a model. The objectives field
+; is #f in the case of unsatisfiability.
+(struct solution (result objectives)
   #:property prop:procedure 
   (lambda (self arg)
     (match self
-      [(solution (? dict? model))
+      [(solution (? dict? model) _)
        (if (dict-has-key? model arg)
            (dict-ref model arg)
            arg)]
       [else (error 'solution "cannot query an unsat solution: ~s" self)]))
   #:methods gen:custom-write
   [(define (write-proc self port mode)
+     (match (solution-objectives self)
+       [(? dict? objs)
+        (unless (dict-empty? objs)
+          (fprintf port "(objectives")
+          (for ([(k v) (in-dict objs)])
+            (fprintf port "\n [~a ~a]" k v))
+          (fprintf port ")\n"))]
+       [_ (void)])
      (match (solution-result self)
        [(? dict? model) 
         (let ([bindings (sort (dict->list model) term<? #:key car)])
@@ -49,45 +63,54 @@
 
 (define (unsat? sol) (not (sat? sol)))
 
+(define (objectives sol) (solution-objectives sol))
+
 (define (get-model s)
   (match s
-    [(solution (? dict? m)) m]
+    [(solution (? dict? m) _) m]
     [_ (error 'model "expected a sat? solution, given ~a" s)]))
 
 (define (get-core s)
   (match s
-    [(solution #f) #f]
-    [(solution (? list? c)) c]
+    [(solution #f _) #f]
+    [(solution (? list? c) _) c]
     [_ (error 'model "expected an unsat? solution, given ~a" s)]))
 
 (define-match-expander model
   (syntax-rules ()
-    [(model) (solution (? dict? (app dict-count 0)))]
-    [(model pat) (solution (? dict? pat))])
+    [(model) (solution (? dict? (app dict-count 0)) _)]
+    [(model pat) (solution (? dict? pat) _)])
   (syntax-id-rules (set!)
     [(model s) (get-model s)]
     [model get-model]))
 
 (define-match-expander core
   (syntax-rules ()
-    [(core) (solution #f)]
-    [(core #f) (solution #f)]
-    [(core pat) (solution (? list? pat))])
+    [(core) (solution #f #f)]
+    [(core #f) (solution #f #f)]
+    [(core pat) (solution (? list? pat) #f)])
   (syntax-id-rules (set!)
     [(core s) (get-core s)]
     [core get-core]))
 
-(define empty-sat (solution (hash)))
-(define empty-unsat (solution #f)) 
+(define empty-sat (solution (hash) (hash)))
+(define empty-unsat (solution #f #f)) 
 
 ; Creates and returns a satisfiable solution consisting of the given model.  The model
 ; must be an immutable dictionary, with symbolic constants as keys.
 (define sat
   (case-lambda 
     [() empty-sat]
-    [(model) (unless (and (dict? model) (not (dict-mutable? model)))
-               (error 'sat "expected an immutable dictionary, given ~s" model))
-             (solution model)]))
+    [(model)
+     (unless (and (dict? model) (not (dict-mutable? model)))
+       (raise-arguments-error 'sat "expected an immutable dictionary" "model" model))
+     (solution model (hash))]
+    [(model objs) 
+     (unless (and (dict? model) (not (dict-mutable? model))
+                  (dict? objs) (not (dict-mutable? objs)))
+       (raise-arguments-error 'sat "expected immutable dictionaries"
+                              "model" model "objectives" objs))
+     (solution model objs)]))
 
 ; Creates and returns a new unsatisfiable solution that consists of the given core, if any, 
 ; or no core, if called with no arguments.  The must be a list of @boolean? values.
@@ -95,5 +118,25 @@
   (case-lambda [() empty-unsat]
                [(core) (unless (and (list? core) (not (null? core)))
                          (error 'unsat "expected a non-empty list, given ~s" core))
-                       (solution core)]))
+                       (solution core #f)]))
+
+(struct interval (min includes-min? max includes-max?)
+  #:transparent
+  #:guard (lambda (min includes-min? max includes-max? name)
+            (unless (boolean? includes-min?)
+              (raise-arguments-error name "expected a boolean?" "includes-min?" includes-min?))
+            (unless (boolean? includes-max?)
+              (raise-arguments-error name "expected a boolean?" "includes-max?" includes-max?))
+            (unless (or (and (real? min) (real? max) (<= min max))
+                        (and (bv? min) (bv? max) (@bvsle min max)))
+              (raise-arguments-error name "expected two real? or bv? values with min <= max"
+                                     "min" min "max" max))
+            (values min includes-min?  max includes-max?))
+  #:methods gen:custom-write
+  [(define (write-proc self port mode)
+     (match-define (interval min includes-min? max includes-max?) self)
+     (fprintf port (if includes-min? "[" "("))
+     (fprintf port "~a " min)
+     (fprintf port "~a" max)
+     (fprintf port (if includes-max? "]" ")")))])
   

test/query/optimize.rkt

@@ -3,34 +3,67 @@
 (require rackunit rackunit/text-ui rosette/lib/roseunit)
 
 (define (minimize obj . asserts)
-  (optimize #:minimize (list obj)
+  (optimize #:minimize (if (list? obj) obj (list obj))
             #:guarantee (for ([a asserts]) (assert a))))
 
 (define (maximize obj . asserts)
-  (optimize #:maximize (list obj)
+  (optimize #:maximize (if (list? obj) obj (list obj))
             #:guarantee (for ([a asserts]) (assert a))))
 
-(define (check-solution actual expected [test =])
+(define (check-solution actual test expected)
   (check-sat actual)
+  ;(printf "actual: ~a\nexpected: ~a\n" actual expected)
   (define ma (model actual))
   (define me (model expected))
   (check-equal? (dict-keys ma) (dict-keys me))
   (for ([(k v) ma])
-    (check test v (dict-ref me k))))
+    (check test v (dict-ref me k)))
+  (define oa (objectives actual))
+  (define oe (objectives expected))
+  (check-equal? (dict-keys oa) (dict-keys oe))
+  (for ([(k v) oa])
+    (check-equal? v (dict-ref oe k))))
 
 (define basic-tests
   (test-suite+ "Basic optimize tests with no finitization."
     (current-bitwidth #f)
-    (define-symbolic x y integer?)
-    (check-solution (maximize (+ x y) (< x 2) (< (- y x) 1))
-                    (sat (hash x 1 y 1)))
+    (define-symbolic x y z integer?)
+    
+;    (check-solution
+;     (maximize (+ x y) (< x 2) (< (- y x) 1)) =
+;     (sat (hash x 1 y 1) (hash (+ x y) 2)))
+
+    (check-solution
+     (maximize z (< x 2) (< (- y x) 1) (= z (+ x y))) =
+     (sat (hash x 1 y 1 z 2) (hash z (interval 2 #t 2 #t))))
+    
     (check-unsat (maximize (+ x y) (< x 2) (< y 2) (> (+ x y) 4)))
+
     (check-unsat (minimize (+ x y) (< x 2) (< y 2) (> (+ x y) 4)))
-    (check-solution (minimize (+ x y) (< x 4) (< (- y x) 1) (> y 1))
-                    (sat (hash x 2 y 2)))
-    (define-symbolic r q real?)
-    (check-solution (maximize (+ r q) (< r 4) (< q 5))
-                    (sat (hash r 3.0 q 4.0)) >=)
+
+;    (check-solution
+;     (minimize (+ x y) (< x 4) (< (- y x) 1) (> y 1)) =
+;     (sat (hash x 2 y 2) (hash (+ x y) 4)))
+
+;    (check-solution
+;     (maximize (+ x y) (< x 2) (> (- y x) 1)) >=
+;     (sat (hash x 1 y 3) (hash (+ x y) (interval +inf.0 #t +inf.0 #t))))
+
+;    (check-solution
+;     (minimize (+ x y) (< x 4) (< (- y x) 1) (< y 1)) <=
+;     (sat (hash x -1 y -1) (hash (+ x y) (interval -inf.0 #t -inf.0 #t))))
+
+    (check-solution
+     (maximize (list x y) (< x z) (< y z) (< z 5) (! (= x y))) =
+     (sat (hash z 4 y 2 x 3) (hash x (interval 3 #t 3 #t) y (interval 2 #t 2 #t))))
+
+;    (define-symbolic r q real?)
+;
+;    (check-solution
+;     (maximize (+ r q) (< r 4) (< q 5)) >=
+;     (sat (hash r 3.0 q 4.0) (hash (+ r q) (interval -inf.0 #f 9 #f))))
+;
+
     ))
 
 (time (run-tests basic-tests))