avoid quadratic time processing in solver-(assert,min/maximize) (#261)

* avoid quadratic time processing in solver-(assert,min/maximize)

The time complexity of n calls to solver-assert / solver-minimize /
solver-maximize is currently O(n^2) due to list appending at the tail,
which requires traversal. This PR fixes the problem. The ordering of
solver-minimize and solver-maximize matters, however
(it specifies the lexicographic ordering minimization),
so rearranging them is slightly more complicated.

* Add an optimization order test

* Clear the solver

rosette/solver/smt/base-solver.rkt

@@ -12,6 +12,8 @@
 
 (provide (all-defined-out))
 
+(define (unique/reverse xs)
+  (reverse (unique xs)))
 
 (define (find-solver binary base-path [user-path #f])
   (cond
@@ -42,14 +44,15 @@
   (unless (list? bools)
     (raise-argument-error 'solver-assert "(listof boolean?)" bools))
   (define wfcheck-cache (mutable-set))
-  (set-solver-asserts! self 
-    (append (solver-asserts self)
-            (for/list ([b bools] #:unless (equal? b #t))
-              (unless (or (boolean? b) (and (term? b) (equal? @boolean? (term-type b))))
-                (error 'assert "expected a boolean value, given ~s" b))
-              (when wfcheck
-                (wfcheck b wfcheck-cache))
-              b))))
+  (set-solver-asserts!
+   self
+   (append (for/list ([b bools] #:unless (equal? b #t))
+             (unless (or (boolean? b) (and (term? b) (equal? @boolean? (term-type b))))
+               (error 'assert "expected a boolean value, given ~s" b))
+             (when wfcheck
+               (wfcheck b wfcheck-cache))
+             b)
+           (solver-asserts self))))
 
 (define (solver-minimize self nums)
   (unless (null? nums)
@@ -68,7 +71,7 @@
   (server-shutdown (solver-server self)))
 
 (define (solver-push self)
-  (match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env level) self)
+  (match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env level) self)
   (server-write
    server
    (begin
@@ -90,7 +93,7 @@
   (set-solver-level! self (drop level k)))
 
 (define (solver-check self [read-solution read-solution])
-  (match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env _) self)
+  (match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env _) self)
   (cond [(ormap false? asserts) (unsat)]
         [else (server-write
                server

rosette/solver/smt/z3.rkt

@@ -52,10 +52,10 @@
      (base/solver-assert self bools))
 
    (define (solver-minimize self nums)
-     (base/set-solver-mins! self (append (base/solver-mins self) (numeric-terms nums 'solver-minimize))))
+     (base/set-solver-mins! self (append (reverse (numeric-terms nums 'solver-minimize)) (base/solver-mins self))))
 
    (define (solver-maximize self nums)
-     (base/set-solver-maxs! self (append (base/solver-maxs self) (numeric-terms nums 'solver-maximize))))
+     (base/set-solver-maxs! self (append (reverse (numeric-terms nums 'solver-maximize)) (base/solver-maxs self))))
 
    (define (solver-clear self) 
      (base/solver-clear-stacks! self)

test/all-rosette-tests.rkt

@@ -38,6 +38,7 @@
  "base/distinct.rkt"
  "base/generics.rkt"
  "base/push-pop.rkt"
+ "base/optimize-order.rkt"
  "base/reflect.rkt"
  "base/decode.rkt"
  "query/solve.rkt"

test/base/optimize-order.rkt

@@ -0,0 +1,27 @@
+#lang rosette
+
+;; This test is taken from https://www.philipzucker.com/z3-rise4fun/optimization.html
+
+(require rackunit rackunit/text-ui racket/generator
+         rosette/lib/roseunit)
+
+(current-bitwidth #f)
+(define-symbolic x y z integer?)
+
+(define (check-model sol m)
+  (check-pred sat? sol)
+  (check-equal? (model sol) m))
+
+(define optimization-order-tests
+  (test-suite+ "Tests for the optimization order"
+   #:features '(optimize)
+
+  (define solver (current-solver))
+  (solver-clear solver)
+  (solver-assert solver (list (< x z) (< y z) (< z 5) (not (= x y))))
+  (solver-maximize solver (list x))
+  (solver-maximize solver (list y))
+  (check-model (solver-check solver) (hash x 3 y 2 z 4))))
+
+(module+ test
+  (time (run-tests optimization-order-tests)))