From 5dd348906d8bafacef6354c2e5e75a67be0bec66 Mon Sep 17 00:00:00 2001
From: sorawee <sorawee.pwase@gmail.com>
Date: Thu, 10 Aug 2023 18:38:48 -0700
Subject: [PATCH] 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 | 23 +++++++++++++----------
 rosette/solver/smt/z3.rkt          |  4 ++--
 test/all-rosette-tests.rkt         |  1 +
 test/base/optimize-order.rkt       | 27 +++++++++++++++++++++++++++
 4 files changed, 43 insertions(+), 12 deletions(-)
 create mode 100644 test/base/optimize-order.rkt

diff --git a/rosette/solver/smt/base-solver.rkt b/rosette/solver/smt/base-solver.rkt
index d3a1bd8c..e20a022a 100644
--- a/rosette/solver/smt/base-solver.rkt
+++ b/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
diff --git a/rosette/solver/smt/z3.rkt b/rosette/solver/smt/z3.rkt
index 974ea66e..d86f7097 100644
--- a/rosette/solver/smt/z3.rkt
+++ b/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)
diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt
index 88bfc197..8013dae9 100644
--- a/test/all-rosette-tests.rkt
+++ b/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"
diff --git a/test/base/optimize-order.rkt b/test/base/optimize-order.rkt
new file mode 100644
index 00000000..a9266a7e
--- /dev/null
+++ b/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)))