From becbfab2b7b4f889f5980b25d9545dddb99a7263 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 12 Dec 2023 10:38:37 -0800 Subject: [PATCH 1/3] Skip `ASSERT` lines during `check-sat` for STP --- rosette/solver/smt/stp.rkt | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index 59c54e1e..be90e65e 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -58,8 +58,25 @@ (define (solver-pop self [k 1]) (base/solver-pop self k)) - (define (solver-check self) - (base/solver-check self)) + +(define (solver-check self) + (define (read-solution server env #:unsat-core? [unsat-core? #f]) + ;;; Ignore the ASSERT lines, if present. + (server-read server + ; Peek at the first five characters, which should always be present. They'll either be "unsat" or + ; "ASSER", the latter of which is the first five characters of "ASSERT". + (let loop () + (if (and (not (equal? (peek-string 3 0) "sat")) + (not (equal? (peek-string 5 0) "unsat"))) + (begin + (when (not (string-prefix? (read-line) "ASSERT")) + (error "Expected extra line to start with ASSERT")) + (loop)) + (void)))) + (base/read-solution server env #:unsat-core? unsat-core?)) + + (base/solver-check self read-solution) + ) (define (solver-debug self) (base/solver-debug self))]) From 5d5cfae067e036a270b6b8608eb91d513c923ad7 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 12 Dec 2023 11:00:59 -0800 Subject: [PATCH 2/3] Revert "Skip `ASSERT` lines during `check-sat` for STP" This reverts commit becbfab2b7b4f889f5980b25d9545dddb99a7263. --- rosette/solver/smt/stp.rkt | 21 ++------------------- 1 file changed, 2 insertions(+), 19 deletions(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index be90e65e..59c54e1e 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -58,25 +58,8 @@ (define (solver-pop self [k 1]) (base/solver-pop self k)) - -(define (solver-check self) - (define (read-solution server env #:unsat-core? [unsat-core? #f]) - ;;; Ignore the ASSERT lines, if present. - (server-read server - ; Peek at the first five characters, which should always be present. They'll either be "unsat" or - ; "ASSER", the latter of which is the first five characters of "ASSERT". - (let loop () - (if (and (not (equal? (peek-string 3 0) "sat")) - (not (equal? (peek-string 5 0) "unsat"))) - (begin - (when (not (string-prefix? (read-line) "ASSERT")) - (error "Expected extra line to start with ASSERT")) - (loop)) - (void)))) - (base/read-solution server env #:unsat-core? unsat-core?)) - - (base/solver-check self read-solution) - ) + (define (solver-check self) + (base/solver-check self)) (define (solver-debug self) (base/solver-debug self))]) From f1ad2907e55125120fe1e76a9a4b1ff309043cc6 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 12 Dec 2023 12:49:58 -0800 Subject: [PATCH 3/3] don't need the -p flag With the most up-to-date version of STP, all this flag does is force the printing of the model after (check-sat), which causes a parser error. --- rosette/solver/smt/stp.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rosette/solver/smt/stp.rkt b/rosette/solver/smt/stp.rkt index 59c54e1e..2cb91529 100644 --- a/rosette/solver/smt/stp.rkt +++ b/rosette/solver/smt/stp.rkt @@ -8,7 +8,7 @@ (provide (rename-out [make-stp stp]) stp? stp-available?) (define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp")) -(define stp-opts '("--SMTLIB2" "-p")) +(define stp-opts '("--SMTLIB2")) (define (stp-available?) (not (false? (base/find-solver "stp" stp-path #f))))