Skip to content

Commit

Permalink
cvc5: minor improvement
Browse files Browse the repository at this point in the history
Add comments to explain regexp and add a check so that we get nice error
messages when cvc5 returns unexpected model.
  • Loading branch information
sorawee committed Aug 22, 2023
1 parent 5934bf3 commit 797cf5d
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion picus/solvers/cvc5-solver.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,8 @@
(make-readtable #f #\f 'dispatch-macro
(λ (_ port src line col pos)
(match (symbol->string (read port))
;; we have already consumed "#f" from the dispatch macro
;; so here, we consume the rest of the token: <value> m <mod-value>
[(pregexp #px"^(\\d+)m\\d+$" (list _ (app string->number val)))
val]))))

Expand Down Expand Up @@ -106,7 +108,8 @@
(define model (make-hash))
(for ([binding (in-list raw-model)])
(match binding
[`(define-fun ,var () #;type ,_ ,val)
;; check that val is a number so that non-number will get reported below.
[`(define-fun ,var () #;type ,_ ,(? number? val))
; update model
(hash-set! model (symbol->string var)
(if (< val 0)
Expand Down

0 comments on commit 797cf5d

Please sign in to comment.