fix: make printer for query generation more efficient

We should avoid building the resulting query string with `format`
repeatedly, because `format` creates an entirely new string in
each invocation. When the query is big, the cost is
prohibitively expensive.

This commit instead builds the query string by writing to a
string port directly (similar to the StringBuilder idiom in languages
like Java). As the fix needs to be done on Z3, cvc4, and cvc5, I also
take an opportunity to refactor them to reduce code redundancy.

picus/algorithms/dpvl.rkt

@@ -118,9 +118,7 @@
                       (r1cs:rassert (r1cs:rneq (r1cs:rvar (vector-ref :varvec sid)) (r1cs:rvar (vector-ref :alt-varvec sid))))
                       (r1cs:rsolve))))))
   ; perform optimization
-  (define final-str (string-join (:interpret-r1cs
-                                  (r1cs:rcmds-append :opts final-cmds))
-                                 "\n"))
+  (define final-str (:interpret-r1cs (r1cs:rcmds-append :opts final-cmds)))
   (define res (:solve final-str :arg-timeout #:output-smt? #f))
   (define solved? (cond
                     [(equal? 'unsat (car res))

picus/r1cs/common.rkt

@@ -0,0 +1,69 @@
+#lang racket/base
+
+(provide interp
+         format-op
+         emit)
+
+(require racket/match
+         syntax/parse/define
+         (prefix-in tokamak: "../tokamak.rkt")
+         (prefix-in r1cs: "./r1cs-grammar.rkt")
+         (for-syntax racket/base))
+
+(define (format-op op proc args)
+  (match args
+    ['() (tokamak:exit "empty operation: ~a" op)]
+    [(list x) (proc x)]
+    [(cons x xs)
+     (display "(")
+     (display op)
+     (display " ")
+     (proc x)
+     (display " ")
+     (format-op op proc xs)
+     (display ")")]))
+
+(begin-for-syntax
+  (define-syntax-class item
+    (pattern x:string #:with gen #'(display x))
+    (pattern x #:with gen #'x)))
+
+;; (emit X ...) prints in order, where an element could be either
+;; a string literal or a function call to do further printing.
+(define-syntax-parse-rule (emit xs:item ...)
+  (begin xs.gen ...))
+
+(define (interp arg-r1cs prnt)
+  (define p (open-output-string))
+  (parameterize ([current-output-port p])
+    (let loop ([arg-r1cs arg-r1cs])
+      (prnt
+       arg-r1cs
+       (λ (arg-r1cs)
+         (match arg-r1cs
+
+           ; command level
+           [(r1cs:rcmds vs)
+            (for ([v vs])
+              (loop v)
+              (newline))]
+
+           [(r1cs:rraw v) (display v)]
+           [(r1cs:rlogic v) (printf "(set-logic ~a)" v)]
+           [(r1cs:rdef v t) (emit "(declare-const " (loop v) " " (loop t) ")")]
+           [(r1cs:rassert v) (emit "(assert " (loop v) ")")]
+           [(r1cs:rcmt v) (printf "; ~a" v)]
+           [(r1cs:rsolve ) (display "(check-sat)\n(get-model)")]
+
+           ; sub-command level
+           [(r1cs:req lhs rhs) (emit "(= " (loop lhs) " " (loop rhs) ")")]
+           [(r1cs:rneq lhs rhs) (emit "(not (= " (loop lhs) " " (loop rhs) "))")]
+
+           [(r1cs:rand vs) (format-op "and" loop vs)]
+           [(r1cs:ror vs) (format-op "or" loop vs)]
+           [(r1cs:rimp lhs rhs) (emit "(=> " (loop lhs) " " (loop rhs) ")")]
+
+           [(r1cs:rvar v) (display v)]
+           [(r1cs:rtype v) (display v)]
+           [_ (tokamak:exit "not supported: ~a" arg-r1cs)])))))
+  (get-output-string p))

picus/r1cs/r1cs-cvc4-interpreter.rkt

@@ -1,65 +1,27 @@
 #lang racket
-; this interprets r1cs commands into z3 constraints
-(require
-    (prefix-in tokamak: "../tokamak.rkt")
-    (prefix-in utils: "../utils.rkt")
-    (prefix-in config: "../config.rkt")
-    (prefix-in r1cs: "./r1cs-grammar.rkt")
-)
-(provide (rename-out
-    [interpret-r1cs interpret-r1cs]
-))
+; this interprets r1cs commands into cvc4 constraints
+(require (prefix-in r1cs: "./r1cs-grammar.rkt")
+         "common.rkt")
 
-(define (make-format-op op)
-    (define (format-op x y)
-        (cond
-            ; [(and (null? x) (null? y)) (tokamak:exit "x and y can't both be null")]
-            [(and (null? x) (null? y)) ""]
-            [(null? x) y]
-            [(null? y) x]
-            [else (format "(~a ~a ~a)" op x y)]
-        )
-    )
-    ; return a function
-    format-op
-)
+(provide interpret-r1cs)
 
 (define (interpret-r1cs arg-r1cs)
-    (match arg-r1cs
+  (interp
+   arg-r1cs
+   (λ (arg-r1cs fallback)
+     (let loop ([arg-r1cs arg-r1cs])
+       (match arg-r1cs
+         [(r1cs:rleq lhs rhs) (emit "(<= " (loop lhs) " " (loop rhs) ")")]
+         [(r1cs:rlt lhs rhs) (emit "(< " (loop lhs) " " (loop rhs) ")")]
+         [(r1cs:rgeq lhs rhs) (emit "(>= " (loop lhs) " " (loop rhs) ")")]
+         [(r1cs:rgt lhs rhs) (emit "(> " (loop lhs) " " (loop rhs) ")")]
 
-        ; command level
-        [(r1cs:rcmds vs) (for/list ([v vs]) (interpret-r1cs v))]
+         [(r1cs:rint v) (display v)]
 
-        [(r1cs:rraw v) (format "~a" v)]
-        [(r1cs:rlogic v) (format "(set-logic ~a)" v)]
-        [(r1cs:rdef v t) (format "(declare-const ~a ~a)" (interpret-r1cs v) (interpret-r1cs t))]
-        [(r1cs:rassert v) (format "(assert ~a)" (interpret-r1cs v))]
-        [(r1cs:rcmt v) (format "; ~a" v)]
-        [(r1cs:rsolve ) "(check-sat)\n(get-model)"]
-
-        ; sub-command level
-        [(r1cs:req lhs rhs) (format "(= ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rneq lhs rhs) (format "(not (= ~a ~a))" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rleq lhs rhs) (format "(<= ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rlt lhs rhs) (format "(< ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rgeq lhs rhs) (format "(>= ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rgt lhs rhs) (format "(> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-
-        [(r1cs:rand vs) (foldr (make-format-op "and") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:ror vs) (foldr (make-format-op "or") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rimp lhs rhs) (format "(=> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-
-        [(r1cs:rint v) (format "~a" v)]
-        [(r1cs:rvar v) (format "~a" v)]
-        [(r1cs:rtype v) (format "~a" v)]
-
-        [(r1cs:radd vs) (foldr (make-format-op "+") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rsub vs) (foldr (make-format-op "-") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rmul vs) (foldr (make-format-op "*") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rneg v) (format "(- ~a)" (interpret-r1cs v))]
-        ; use mod for cvc4 since there's no rem
-        [(r1cs:rmod v mod) (format "(mod ~a ~a)" (interpret-r1cs v) (interpret-r1cs mod))]
-
-        [else (tokamak:exit "not supported: ~a" arg-r1cs)]
-    )
-)
+         [(r1cs:radd vs) (format-op "+" loop vs)]
+         [(r1cs:rsub vs) (format-op "-" loop vs)]
+         [(r1cs:rmul vs) (format-op "*" loop vs)]
+         [(r1cs:rneg v) (emit "(- " (loop v) ")")]
+         ; use mod for cvc4 since there's no rem
+         [(r1cs:rmod v mod) (emit "(mod " (loop v) " " (loop mod) ")")]
+         [_ (fallback arg-r1cs)])))))

picus/r1cs/r1cs-cvc5-interpreter.rkt

@@ -1,58 +1,17 @@
 #lang racket
-; this interprets r1cs commands into z3 constraints
-(require
-    (prefix-in tokamak: "../tokamak.rkt")
-    (prefix-in utils: "../utils.rkt")
-    (prefix-in config: "../config.rkt")
-    (prefix-in r1cs: "./r1cs-grammar.rkt")
-)
-(provide (rename-out
-    [interpret-r1cs interpret-r1cs]
-))
-
-(define (make-format-op op)
-    (define (format-op x y)
-        (cond
-            ; [(and (null? x) (null? y)) (tokamak:exit "x and y can't both be null")]
-            [(and (null? x) (null? y)) ""]
-            [(null? x) y]
-            [(null? y) x]
-            [else (format "(~a ~a ~a)" op x y)]
-        )
-    )
-    ; return a function
-    format-op
-)
+; this interprets r1cs commands into cvc5 constraints
+(require (prefix-in config: "../config.rkt")
+         (prefix-in r1cs: "./r1cs-grammar.rkt")
+         "common.rkt")
+(provide interpret-r1cs)
 
 (define (interpret-r1cs arg-r1cs)
-    (match arg-r1cs
-
-        ; command level
-        [(r1cs:rcmds vs) (for/list ([v vs]) (interpret-r1cs v))]
-
-        [(r1cs:rraw v) (format "~a" v)]
-        [(r1cs:rlogic v) (format "(set-logic ~a)" v)]
-        [(r1cs:rdef v t) (format "(declare-const ~a ~a)" (interpret-r1cs v) (interpret-r1cs t))]
-        [(r1cs:rassert v) (format "(assert ~a)" (interpret-r1cs v))]
-        [(r1cs:rcmt v) (format "; ~a" v)]
-        [(r1cs:rsolve ) "(check-sat)\n(get-model)"]
-
-        ; sub-command level
-        [(r1cs:req lhs rhs) (format "(= ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rneq lhs rhs) (format "(not (= ~a ~a))" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-
-        [(r1cs:rand vs) (foldr (make-format-op "and") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:ror vs) (foldr (make-format-op "or") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rimp lhs rhs) (format "(=> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-
-        [(r1cs:rint v) (format "#f~am~a" v config:p)]
-        [(r1cs:rvar v) (format "~a" v)]
-        [(r1cs:rtype v) (format "~a" v)]
-
-        [(r1cs:radd vs) (foldr (make-format-op "ff.add") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rmul vs) (foldr (make-format-op "ff.mul") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rmod v mod) (tokamak:exit "cvc5 doesn't support mod")]
-
-        [else (tokamak:exit "not supported: ~a" arg-r1cs)]
-    )
-)
+  (interp
+   arg-r1cs
+   (λ (arg-r1cs fallback)
+     (let loop ([arg-r1cs arg-r1cs])
+       (match arg-r1cs
+         [(r1cs:rint v) (printf "#f~am~a" v config:p)]
+         [(r1cs:radd vs) (format-op "ff.add" loop vs)]
+         [(r1cs:rmul vs) (format-op "ff.mul" loop vs)]
+         [_ (fallback arg-r1cs)])))))

picus/r1cs/r1cs-z3-interpreter.rkt

@@ -1,64 +1,26 @@
 #lang racket
 ; this interprets r1cs commands into z3 constraints
-(require
-    (prefix-in tokamak: "../tokamak.rkt")
-    (prefix-in utils: "../utils.rkt")
-    (prefix-in config: "../config.rkt")
-    (prefix-in r1cs: "./r1cs-grammar.rkt")
-)
-(provide (rename-out
-    [interpret-r1cs interpret-r1cs]
-))
+(require (prefix-in r1cs: "./r1cs-grammar.rkt")
+         "common.rkt")
 
-(define (make-format-op op)
-    (define (format-op x y)
-        (cond
-            ; [(and (null? x) (null? y)) (tokamak:exit "x and y can't both be null")]
-            [(and (null? x) (null? y)) ""]
-            [(null? x) y]
-            [(null? y) x]
-            [else (format "(~a ~a ~a)" op x y)]
-        )
-    )
-    ; return a function
-    format-op
-)
+(provide interpret-r1cs)
 
 (define (interpret-r1cs arg-r1cs)
-    (match arg-r1cs
+  (interp
+   arg-r1cs
+   (λ (arg-r1cs fallback)
+     (let loop ([arg-r1cs arg-r1cs])
+       (match arg-r1cs
+         [(r1cs:rleq lhs rhs) (emit "(<= " (loop lhs) " " (loop rhs) ")")]
+         [(r1cs:rlt lhs rhs) (emit "(< " (loop lhs) " " (loop rhs) ")")]
+         [(r1cs:rgeq lhs rhs) (emit "(>= " (loop lhs) " " (loop rhs) ")")]
+         [(r1cs:rgt lhs rhs) (emit "(> " (loop lhs) " " (loop rhs) ")")]
 
-        ; command level
-        [(r1cs:rcmds vs) (for/list ([v vs]) (interpret-r1cs v))]
+         [(r1cs:rint v) (display v)]
 
-        [(r1cs:rraw v) (format "~a" v)]
-        [(r1cs:rlogic v) (format "(set-logic ~a)" v)]
-        [(r1cs:rdef v t) (format "(declare-const ~a ~a)" (interpret-r1cs v) (interpret-r1cs t))]
-        [(r1cs:rassert v) (format "(assert ~a)" (interpret-r1cs v))]
-        [(r1cs:rcmt v) (format "; ~a" v)]
-        [(r1cs:rsolve ) "(check-sat)\n(get-model)"]
-
-        ; sub-command level
-        [(r1cs:req lhs rhs) (format "(= ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rneq lhs rhs) (format "(not (= ~a ~a))" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rleq lhs rhs) (format "(<= ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rlt lhs rhs) (format "(< ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rgeq lhs rhs) (format "(>= ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-        [(r1cs:rgt lhs rhs) (format "(> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-
-        [(r1cs:rand vs) (foldr (make-format-op "and") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:ror vs) (foldr (make-format-op "or") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rimp lhs rhs) (format "(=> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
-
-        [(r1cs:rint v) (format "~a" v)]
-        [(r1cs:rvar v) (format "~a" v)]
-        [(r1cs:rtype v) (format "~a" v)]
-
-        [(r1cs:radd vs) (foldr (make-format-op "+") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rsub vs) (foldr (make-format-op "-") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rmul vs) (foldr (make-format-op "*") null (for/list ([v vs]) (interpret-r1cs v)))]
-        [(r1cs:rneg v) (format "(- ~a)" (interpret-r1cs v))]
-        [(r1cs:rmod v mod) (format "(rem ~a ~a)" (interpret-r1cs v) (interpret-r1cs mod))]
-
-        [else (tokamak:exit "not supported: ~a" arg-r1cs)]
-    )
-)
+         [(r1cs:radd vs) (format-op "+" loop vs)]
+         [(r1cs:rsub vs) (format-op "-" loop vs)]
+         [(r1cs:rmul vs) (format-op "*" loop vs)]
+         [(r1cs:rneg v) (emit "(- " (loop v) ")")]
+         [(r1cs:rmod v mod) (emit "(rem " (loop v) " " (loop mod) ")")]
+         [_ (fallback arg-r1cs)])))))

picus/tokamak.rkt

@@ -19,7 +19,7 @@
 
 ; used for forced break out of the execution
 (define (println-and-exit msg . fmts)
-    (printf (format "[tokamak:exit] ~a\n" (apply format (cons msg fmts))))
+    (eprintf (format "[tokamak:exit] ~a\n" (apply format (cons msg fmts))))
     (exit 0)
 )
 
@@ -32,7 +32,7 @@
 
 (define (println-and-log msg . fmts)
     ;; TODO/fixme
-    (printf (format "[tokamak:log] ~a\n" (apply format (cons msg fmts))))
+    (eprintf (format "[tokamak:log] ~a\n" (apply format (cons msg fmts))))
 )
 
 ; usually for debugging, asserting obj is one of types, otherwise print and exit
@@ -110,4 +110,4 @@
         ; not symbolic, so not decomposable
         #f
     )
-)
+)