add: include options in SMT-lib, not command line, where applicable

tnelson · Sep 29, 2024 · 0c23720 · 0c23720
1 parent fe8d3e0
commit 0c23720
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 4 deletions.
diff --git a/forge/solver-specific/cvc5-server.rkt b/forge/solver-specific/cvc5-server.rkt
@@ -38,10 +38,11 @@
     ; Omitting:
     ;  "--finite-model-find": use finite model finding heuristic for quantifier instantiation
     ;  we should not have any quantifiers remaining, save perhaps Int quantifiers.
-
+
+    ; Options like these are now added in the SMT-lib output, for better debugging from file.
+    ; "--force-logic=ALL" "--finite-model-find" "--nl-cov" "--produce-models" "--sets-ext"
     (define cmdline-options
-      (list "--incremental" "--interactive" "--sets-ext" "--force-logic=ALL"
-            "--produce-models" "--finite-model-find" "--nl-cov"))
+      (list "--incremental" "--interactive"))
     (printf "system type: ~a cvc5 path: ~a~ncommand-line options: ~a~n" (system-type) cvc5 cmdline-options)
     ; --sets-ext to use "extended set" operators, which help reconcile sets/relations
     (apply subprocess #f #f #f cvc5 cmdline-options)))

diff --git a/forge/solver-specific/cvc5-tor.rkt b/forge/solver-specific/cvc5-tor.rkt
@@ -259,7 +259,17 @@
      `(declare-fun univInt () (Relation IntAtom))
      ; IntAtom, because those are what appear in sets. Just Int could end up empty.
      `(assert (= univInt (as set.universe (Relation IntAtom))))))
-  (define preamble-str (append (list `(reset) `(declare-sort Atom 0) `(declare-sort IntAtom 0) `(declare-fun IntAtom-to-Int (IntAtom) Int)) defined-funs))
+  (define preamble-str (append (list `(reset)
+                                     `(set-logic ALL)
+                                     `(set-option :sets-ext true)
+                                     `(set-option :produce-models true)
+                                     `(set-option :finite-model-find true)
+                                     `(set-option :nl-cov true)
+                                     `(set-option :finite-model-find true)
+                                     `(declare-sort Atom 0)
+                                     `(declare-sort IntAtom 0)
+                                     `(declare-fun IntAtom-to-Int (IntAtom) Int))
+                               defined-funs))
   (define bounds-str (apply append (map (lambda (b) (declare-sigs b)) total-bounds)))
   (define bounds-constraint-strs (apply append (filter-map (lambda (b) 
                                                 (let ([result (child-constraint new-fake-run b)])