Compare commits
No commits in common. "xenia/patches" and "4.1" have entirely different histories.
xenia/patc
...
4.1
|
|
@ -14,11 +14,11 @@ jobs:
|
||||||
|
|
||||||
steps:
|
steps:
|
||||||
- name: Clone Repository
|
- name: Clone Repository
|
||||||
uses: actions/checkout@v4
|
uses: actions/checkout@v3
|
||||||
|
|
||||||
- name: Configure Docker Metadata
|
- name: Configure Docker Metadata
|
||||||
id: meta
|
id: meta
|
||||||
uses: docker/metadata-action@v5
|
uses: docker/metadata-action@v3
|
||||||
with:
|
with:
|
||||||
images: ghcr.io/${{ github.repository }}
|
images: ghcr.io/${{ github.repository }}
|
||||||
tags: |
|
tags: |
|
||||||
|
|
@ -29,7 +29,7 @@ jobs:
|
||||||
type=semver,pattern={{major}}.{{minor}}
|
type=semver,pattern={{major}}.{{minor}}
|
||||||
|
|
||||||
- name: Authenticate to Package Registry
|
- name: Authenticate to Package Registry
|
||||||
uses: docker/login-action@v3
|
uses: docker/login-action@v1
|
||||||
if: ${{ github.event_name != 'pull_request' }}
|
if: ${{ github.event_name != 'pull_request' }}
|
||||||
with:
|
with:
|
||||||
registry: ghcr.io
|
registry: ghcr.io
|
||||||
|
|
@ -37,10 +37,10 @@ jobs:
|
||||||
password: ${{ secrets.GITHUB_TOKEN }}
|
password: ${{ secrets.GITHUB_TOKEN }}
|
||||||
|
|
||||||
- name: Set up Docker Buildx
|
- name: Set up Docker Buildx
|
||||||
uses: docker/setup-buildx-action@v3
|
uses: docker/setup-buildx-action@v1
|
||||||
|
|
||||||
- name: Build and Publish Rosette Image
|
- name: Build and Publish Rosette Image
|
||||||
uses: docker/build-push-action@v6
|
uses: docker/build-push-action@v2
|
||||||
with:
|
with:
|
||||||
context: .
|
context: .
|
||||||
push: ${{ github.event_name != 'pull_request' }}
|
push: ${{ github.event_name != 'pull_request' }}
|
||||||
|
|
|
||||||
|
|
@ -5,10 +5,6 @@ on: [push, pull_request]
|
||||||
env:
|
env:
|
||||||
CVC4_URL: "http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.8-x86_64-linux-opt"
|
CVC4_URL: "http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.8-x86_64-linux-opt"
|
||||||
BOOLECTOR_URL: "https://github.com/Boolector/boolector/archive/3.2.1.tar.gz"
|
BOOLECTOR_URL: "https://github.com/Boolector/boolector/archive/3.2.1.tar.gz"
|
||||||
CVC5_URL: "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.7/cvc5-Linux"
|
|
||||||
BITWUZLA_URL: "https://github.com/bitwuzla/bitwuzla/archive/93a3d930f622b4cef0063215e63b7c3bd10bd663.tar.gz"
|
|
||||||
STP_URL: "https://github.com/stp/stp/archive/d70085462f07c8a5a2f1225f727cda3ef505b141.tar.gz"
|
|
||||||
YICES2_URL: "https://github.com/SRI-CSL/yices2/archive/e27cf308cffb0ecc6cc7165c10e81ca65bc303b3.tar.gz"
|
|
||||||
|
|
||||||
jobs:
|
jobs:
|
||||||
test:
|
test:
|
||||||
|
|
@ -23,14 +19,12 @@ jobs:
|
||||||
steps:
|
steps:
|
||||||
- uses: actions/checkout@master
|
- uses: actions/checkout@master
|
||||||
- name: Setup Racket
|
- name: Setup Racket
|
||||||
uses: Bogdanp/setup-racket@v1.14
|
uses: Bogdanp/setup-racket@v1.7
|
||||||
with:
|
with:
|
||||||
architecture: x64
|
architecture: x64
|
||||||
version: ${{ matrix.racket-version }}
|
version: ${{ matrix.racket-version }}
|
||||||
variant: ${{ matrix.racket-variant }}
|
variant: ${{ matrix.racket-variant }}
|
||||||
- name: Install solvers
|
- name: Install solvers
|
||||||
# Note that setting LD_LIBRARY_PATH can be removed once this bug is
|
|
||||||
# fixed: https://github.com/stp/stp/issues/485
|
|
||||||
run: |
|
run: |
|
||||||
mkdir bin &&
|
mkdir bin &&
|
||||||
wget $CVC4_URL -nv -O bin/cvc4 &&
|
wget $CVC4_URL -nv -O bin/cvc4 &&
|
||||||
|
|
@ -46,50 +40,7 @@ jobs:
|
||||||
make &&
|
make &&
|
||||||
popd &&
|
popd &&
|
||||||
cp boolector/build/bin/boolector bin/ &&
|
cp boolector/build/bin/boolector bin/ &&
|
||||||
rm -rf boolector* &&
|
rm -rf boolector*
|
||||||
wget $CVC5_URL -nv -O bin/cvc5 &&
|
|
||||||
chmod +x bin/cvc5 &&
|
|
||||||
sudo apt-get update &&
|
|
||||||
sudo apt-get install -y ninja-build &&
|
|
||||||
pip3 install meson &&
|
|
||||||
wget $BITWUZLA_URL -nv -O bitwuzla.tar.gz &&
|
|
||||||
mkdir bitwuzla &&
|
|
||||||
tar xzf bitwuzla.tar.gz -C bitwuzla --strip-components=1 &&
|
|
||||||
pushd bitwuzla &&
|
|
||||||
./configure.py &&
|
|
||||||
pushd build &&
|
|
||||||
ninja &&
|
|
||||||
popd &&
|
|
||||||
popd &&
|
|
||||||
cp bitwuzla/build/src/main/bitwuzla bin/ &&
|
|
||||||
sudo apt-get install -y build-essential git cmake bison flex libboost-all-dev libtinfo-dev python3 perl &&
|
|
||||||
wget $STP_URL -nv -O stp.tar.gz &&
|
|
||||||
mkdir stp &&
|
|
||||||
tar xzf stp.tar.gz -C stp --strip-components=1 &&
|
|
||||||
pushd stp &&
|
|
||||||
echo "LD_LIBRARY_PATH=$PWD/deps/cadical/build:$PWD/deps/cadiback/:$LD_LIBRARY_PATH" >> $GITHUB_ENV &&
|
|
||||||
./scripts/deps/setup-gtest.sh &&
|
|
||||||
./scripts/deps/setup-outputcheck.sh &&
|
|
||||||
./scripts/deps/setup-cms.sh &&
|
|
||||||
./scripts/deps/setup-minisat.sh &&
|
|
||||||
mkdir build &&
|
|
||||||
pushd build &&
|
|
||||||
cmake .. &&
|
|
||||||
cmake --build . &&
|
|
||||||
popd &&
|
|
||||||
popd &&
|
|
||||||
ln -s stp/build/stp bin/stp &&
|
|
||||||
sudo apt-get install -y gperf &&
|
|
||||||
wget $YICES2_URL -nv -O yices2.tar.gz &&
|
|
||||||
mkdir yices2 &&
|
|
||||||
tar xvf yices2.tar.gz -C yices2 --strip-components=1 &&
|
|
||||||
pushd yices2 &&
|
|
||||||
autoconf &&
|
|
||||||
./configure --prefix=$PWD/out/ &&
|
|
||||||
make &&
|
|
||||||
make install &&
|
|
||||||
popd &&
|
|
||||||
cp yices2/out/bin/yices-smt2 bin/yices-smt2
|
|
||||||
- name: Install Rosette
|
- name: Install Rosette
|
||||||
run: raco pkg install --auto --name rosette
|
run: raco pkg install --auto --name rosette
|
||||||
- name: Compile Rosette tests
|
- name: Compile Rosette tests
|
||||||
|
|
|
||||||
|
|
@ -33,7 +33,6 @@
|
||||||
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
||||||
@bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
@bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
||||||
@concat @extract @sign-extend @zero-extend
|
@concat @extract @sign-extend @zero-extend
|
||||||
@z3_ext_rotate_left @z3_ext_rotate_right
|
|
||||||
@integer->bitvector @bitvector->integer @bitvector->natural
|
@integer->bitvector @bitvector->integer @bitvector->natural
|
||||||
; core/bvlib.rkt
|
; core/bvlib.rkt
|
||||||
bit lsb msb bvzero? bvadd1 bvsub1
|
bit lsb msb bvzero? bvadd1 bvsub1
|
||||||
|
|
|
||||||
|
|
@ -14,7 +14,6 @@
|
||||||
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
||||||
@bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
@bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
||||||
@concat @extract @sign-extend @zero-extend
|
@concat @extract @sign-extend @zero-extend
|
||||||
@z3_ext_rotate_left @z3_ext_rotate_right
|
|
||||||
@integer->bitvector @bitvector->integer @bitvector->natural)
|
@integer->bitvector @bitvector->integer @bitvector->natural)
|
||||||
|
|
||||||
;; ----------------- Bitvector Types ----------------- ;;
|
;; ----------------- Bitvector Types ----------------- ;;
|
||||||
|
|
@ -339,13 +338,6 @@
|
||||||
(ite (bveq (bv 0 t) (bvand x (bv (bvsmin t) t))) (bv 0 t) (bv -1 t))]
|
(ite (bveq (bv 0 t) (bvand x (bv (bvsmin t) t))) (bv 0 t) (bv -1 t))]
|
||||||
[(_ _) (expression @bvashr x y)]))
|
[(_ _) (expression @bvashr x y)]))
|
||||||
|
|
||||||
|
|
||||||
(define (z3_ext_rotate_left x y)
|
|
||||||
(expression @z3_ext_rotate_left x y))
|
|
||||||
|
|
||||||
(define (z3_ext_rotate_right x y)
|
|
||||||
(expression @z3_ext_rotate_right x y))
|
|
||||||
|
|
||||||
(define-lifted-operator @bvnot bvnot T*->T)
|
(define-lifted-operator @bvnot bvnot T*->T)
|
||||||
(define-lifted-operator @bvand bvand T*->T)
|
(define-lifted-operator @bvand bvand T*->T)
|
||||||
(define-lifted-operator @bvor bvor T*->T)
|
(define-lifted-operator @bvor bvor T*->T)
|
||||||
|
|
@ -353,8 +345,6 @@
|
||||||
(define-lifted-operator @bvshl bvshl T*->T)
|
(define-lifted-operator @bvshl bvshl T*->T)
|
||||||
(define-lifted-operator @bvlshr bvlshr T*->T)
|
(define-lifted-operator @bvlshr bvlshr T*->T)
|
||||||
(define-lifted-operator @bvashr bvashr T*->T)
|
(define-lifted-operator @bvashr bvashr T*->T)
|
||||||
(define-lifted-operator @z3_ext_rotate_left z3_ext_rotate_left T*->T)
|
|
||||||
(define-lifted-operator @z3_ext_rotate_right z3_ext_rotate_right T*->T)
|
|
||||||
|
|
||||||
;; ----------------- Simplification ruules for bitwise operators ----------------- ;;
|
;; ----------------- Simplification ruules for bitwise operators ----------------- ;;
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -19,12 +19,7 @@
|
||||||
; These IDs are never reused, and they are used to impose an ordering on the children
|
; These IDs are never reused, and they are used to impose an ordering on the children
|
||||||
; of expressions with commutative operators.
|
; of expressions with commutative operators.
|
||||||
#|-----------------------------------------------------------------------------------|#
|
#|-----------------------------------------------------------------------------------|#
|
||||||
|
(define current-terms (make-parameter (make-hash)))
|
||||||
;; Initialize with #f so that the hash table cooperates with garbage collector.
|
|
||||||
;; See #247
|
|
||||||
(define current-terms (make-parameter #f))
|
|
||||||
(current-terms (make-hash))
|
|
||||||
|
|
||||||
(define current-index (make-parameter 0))
|
(define current-index (make-parameter 0))
|
||||||
|
|
||||||
; Clears the entire term cache if invoked with #f (default), or
|
; Clears the entire term cache if invoked with #f (default), or
|
||||||
|
|
@ -82,23 +77,17 @@
|
||||||
; restores (terms) to its old value. If terms-expr is not given, it defaults to
|
; restores (terms) to its old value. If terms-expr is not given, it defaults to
|
||||||
; (terms), so (with-terms expr) is equivalent to (with-terms (terms) expr).
|
; (terms), so (with-terms expr) is equivalent to (with-terms (terms) expr).
|
||||||
(define-syntax (with-terms stx)
|
(define-syntax (with-terms stx)
|
||||||
;; Parameterize with #f so that the hash table cooperates with garbage collector.
|
|
||||||
;; See #247
|
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ expr)
|
[(_ expr)
|
||||||
#'(let ([orig-terms (current-terms)])
|
#'(parameterize ([current-terms (hash-copy (current-terms))])
|
||||||
(parameterize ([current-terms #f])
|
expr)]
|
||||||
(current-terms (hash-copy orig-terms))
|
|
||||||
expr))]
|
|
||||||
[(_ terms-expr expr)
|
[(_ terms-expr expr)
|
||||||
#'(let ([orig-terms (current-terms)])
|
#'(parameterize ([current-terms (hash-copy-clear (current-terms))])
|
||||||
(parameterize ([current-terms #f])
|
|
||||||
(current-terms (hash-copy-clear orig-terms))
|
|
||||||
(let ([ts terms-expr]
|
(let ([ts terms-expr]
|
||||||
[cache (current-terms)])
|
[cache (current-terms)])
|
||||||
(for ([t ts])
|
(for ([t ts])
|
||||||
(hash-set! cache (term-val t) t))
|
(hash-set! cache (term-val t) t))
|
||||||
expr)))]))
|
expr))]))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -132,21 +121,14 @@
|
||||||
(define (term<? s1 s2) (< (term-ord s1) (term-ord s2)))
|
(define (term<? s1 s2) (< (term-ord s1) (term-ord s2)))
|
||||||
|
|
||||||
(define-syntax-rule (make-term term-constructor args type rest ...)
|
(define-syntax-rule (make-term term-constructor args type rest ...)
|
||||||
(let ([val args]
|
(let ([val args])
|
||||||
[ty type])
|
(or (hash-ref (current-terms) val #f)
|
||||||
(define cached (hash-ref (current-terms) val #f))
|
(let* ([ord (current-index)]
|
||||||
(cond
|
[out (term-constructor val type ord rest ...)])
|
||||||
[cached
|
|
||||||
(unless (equal? (term-type cached) ty)
|
|
||||||
(error 'define-symbolic "type should remain unchanged"))
|
|
||||||
cached]
|
|
||||||
[else
|
|
||||||
(define ord (current-index))
|
|
||||||
(define out (term-constructor val ty ord rest ...))
|
|
||||||
(current-index (add1 ord))
|
(current-index (add1 ord))
|
||||||
((current-reporter) 'new-term out)
|
((current-reporter) 'new-term out)
|
||||||
(hash-set! (current-terms) val out)
|
(hash-set! (current-terms) val out)
|
||||||
out])))
|
out))))
|
||||||
|
|
||||||
(define (make-const id t)
|
(define (make-const id t)
|
||||||
(unless (and (type? t) (solvable? t))
|
(unless (and (type? t) (solvable? t))
|
||||||
|
|
|
||||||
|
|
@ -43,8 +43,8 @@
|
||||||
[type-cast type val [caller]] ; (-> type? any/c symbol? any/c)
|
[type-cast type val [caller]] ; (-> type? any/c symbol? any/c)
|
||||||
[type-name type] ; (-> type? symbol?)
|
[type-name type] ; (-> type? symbol?)
|
||||||
[type-applicable? type] ; (-> type? boolean?)
|
[type-applicable? type] ; (-> type? boolean?)
|
||||||
[type-eq? type u v] ; (-> type? any/c any/c @boolean?)
|
[type-eq? type u v] ; (-> type? (-> any/c any/c @boolean?)))
|
||||||
[type-equal? type u v] ; (-> type? any/c any/c @boolean?)
|
[type-equal? type u v] ; (-> type? (-> any/c any/c @boolean?)))
|
||||||
[type-compress type force? ps] ; (-> type? (listof (cons @boolean? any/c)) (listof (cons @boolean? any/c)))
|
[type-compress type force? ps] ; (-> type? (listof (cons @boolean? any/c)) (listof (cons @boolean? any/c)))
|
||||||
[type-construct type vals] ; (-> type? (listof any/c) any/c)
|
[type-construct type vals] ; (-> type? (listof any/c) any/c)
|
||||||
[type-deconstruct type val]) ; (-> type? any/c (listof any/c))
|
[type-deconstruct type val]) ; (-> type? any/c (listof any/c))
|
||||||
|
|
|
||||||
|
|
@ -434,7 +434,7 @@ leads to faster solving times.
|
||||||
|
|
||||||
@(rosette-eval '(clear-vc!))
|
@(rosette-eval '(clear-vc!))
|
||||||
|
|
||||||
@defproc[(bitvector->bits [x (bitvector n)]) (listof (bitvector 1))]{
|
@defproc[(bitvector->bits [x (bitvector n)]) (listof (bitvector n))]{
|
||||||
|
|
||||||
Returns the bits of @racket[x] as a list, i.e., @racket[(list (bit 0 x) ... (bit (- n 1) x))].
|
Returns the bits of @racket[x] as a list, i.e., @racket[(list (bit 0 x) ... (bit (- n 1) x))].
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -4,10 +4,6 @@
|
||||||
rosette/solver/solver rosette/solver/solution
|
rosette/solver/solver rosette/solver/solution
|
||||||
rosette/solver/smt/z3 rosette/solver/smt/cvc4
|
rosette/solver/smt/z3 rosette/solver/smt/cvc4
|
||||||
rosette/solver/smt/boolector
|
rosette/solver/smt/boolector
|
||||||
rosette/solver/smt/bitwuzla
|
|
||||||
rosette/solver/smt/cvc5
|
|
||||||
rosette/solver/smt/stp
|
|
||||||
rosette/solver/smt/yices
|
|
||||||
rosette/base/form/define rosette/query/query
|
rosette/base/form/define rosette/query/query
|
||||||
rosette/base/core/term (only-in rosette/base/base bv?)
|
rosette/base/core/term (only-in rosette/base/base bv?)
|
||||||
(only-in rosette/base/base assert)
|
(only-in rosette/base/base assert)
|
||||||
|
|
@ -26,10 +22,6 @@
|
||||||
rosette/solver/smt/z3
|
rosette/solver/smt/z3
|
||||||
rosette/solver/smt/cvc4
|
rosette/solver/smt/cvc4
|
||||||
rosette/solver/smt/boolector
|
rosette/solver/smt/boolector
|
||||||
rosette/solver/smt/bitwuzla
|
|
||||||
rosette/solver/smt/cvc5
|
|
||||||
rosette/solver/smt/stp
|
|
||||||
rosette/solver/smt/yices
|
|
||||||
#:use-sources
|
#:use-sources
|
||||||
(rosette/query/finitize
|
(rosette/query/finitize
|
||||||
rosette/query/query
|
rosette/query/query
|
||||||
|
|
@ -37,11 +29,7 @@
|
||||||
rosette/solver/solution
|
rosette/solver/solution
|
||||||
rosette/solver/smt/z3
|
rosette/solver/smt/z3
|
||||||
rosette/solver/smt/cvc4
|
rosette/solver/smt/cvc4
|
||||||
rosette/solver/smt/boolector
|
rosette/solver/smt/boolector)]
|
||||||
rosette/solver/smt/bitwuzla
|
|
||||||
rosette/solver/smt/cvc5
|
|
||||||
rosette/solver/smt/stp
|
|
||||||
rosette/solver/smt/yices)]
|
|
||||||
|
|
||||||
A @deftech{solver} is an automatic reasoning engine, used to answer
|
A @deftech{solver} is an automatic reasoning engine, used to answer
|
||||||
@seclink["sec:queries"]{queries} about Rosette programs. The result of
|
@seclink["sec:queries"]{queries} about Rosette programs. The result of
|
||||||
|
|
@ -291,146 +279,6 @@ Returns true if the Boolector solver is available for use (i.e., Rosette can loc
|
||||||
If this returns @racket[#f], @racket[(boolector)] will not succeed
|
If this returns @racket[#f], @racket[(boolector)] will not succeed
|
||||||
without its optional @racket[path] argument.}
|
without its optional @racket[path] argument.}
|
||||||
|
|
||||||
@subsection{Bitwuzla}
|
|
||||||
|
|
||||||
@defmodule[rosette/solver/smt/bitwuzla #:no-declare]
|
|
||||||
|
|
||||||
@defproc*[([(bitwuzla [#:path path (or/c path-string? #f) #f]
|
|
||||||
[#:logic logic (or/c symbol? #f) #f]
|
|
||||||
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
|
|
||||||
[(bitwuzla? [v any/c]) boolean?])]{
|
|
||||||
|
|
||||||
Returns a @racket[solver?] wrapper for the @hyperlink["https://bitwuzla.github.io/"]{Bitwuzla} solver.
|
|
||||||
|
|
||||||
To use this solver, download prebuilt Bitwuzla or build it yourself,
|
|
||||||
and ensure the executable is on your @tt{PATH} or pass the path to the
|
|
||||||
executable as the optional @racket[path] argument.
|
|
||||||
Rosette currently tests Bitwuzla at commit
|
|
||||||
@tt{93a3d930f622b4cef0063215e63b7c3bd10bd663}.
|
|
||||||
|
|
||||||
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
|
|
||||||
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
|
|
||||||
emitted constraints fall within the chosen logic. The default is @racket[#f],
|
|
||||||
which uses Bitwuzla's default logic.
|
|
||||||
|
|
||||||
The @racket[options] argument provides additional options that are sent to Bitwuzla
|
|
||||||
via the @tt{set-option} SMT command.
|
|
||||||
For example, setting @racket[options] to @racket[(hash ':seed 5)]
|
|
||||||
will send the command @tt{(set-option :seed 5)} to Bitwuzla prior to solving.
|
|
||||||
}
|
|
||||||
|
|
||||||
@defproc[(bitwuzla-available?) boolean?]{
|
|
||||||
Returns true if the Bitwuzla solver is available for use (i.e., Rosette can locate a @tt{bitwuzla} binary).
|
|
||||||
If this returns @racket[#f], @racket[(bitwuzla)] will not succeed
|
|
||||||
without its optional @racket[path] argument.}
|
|
||||||
|
|
||||||
@subsection{CVC5}
|
|
||||||
|
|
||||||
@defmodule[rosette/solver/smt/cvc5 #:no-declare]
|
|
||||||
|
|
||||||
@defproc*[([(cvc5 [#:path path (or/c path-string? #f) #f]
|
|
||||||
[#:logic logic (or/c symbol? #f) #f]
|
|
||||||
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
|
|
||||||
[(cvc5? [v any/c]) boolean?])]{
|
|
||||||
|
|
||||||
Returns a @racket[solver?] wrapper for the @hyperlink["https://cvc5.github.io/"]{CVC5} solver.
|
|
||||||
|
|
||||||
To use this solver, download prebuilt CVC5 or build it yourself,
|
|
||||||
and ensure the executable is on your @tt{PATH} or pass the path to the
|
|
||||||
executable as the optional @racket[path] argument.
|
|
||||||
Rosette currently tests CVC5 at version 1.0.7.
|
|
||||||
|
|
||||||
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
|
|
||||||
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
|
|
||||||
emitted constraints fall within the chosen logic. The default is @racket[#f],
|
|
||||||
which uses CVC5's default logic.
|
|
||||||
|
|
||||||
The @racket[options] argument provides additional options that are sent to CVC5
|
|
||||||
via the @tt{set-option} SMT command.
|
|
||||||
For example, setting @racket[options] to @racket[(hash ':seed 5)]
|
|
||||||
will send the command @tt{(set-option :seed 5)} to CVC5 prior to solving.
|
|
||||||
}
|
|
||||||
|
|
||||||
@defproc[(cvc5-available?) boolean?]{
|
|
||||||
Returns true if the CVC5 solver is available for use (i.e., Rosette can locate a @tt{cvc5} binary).
|
|
||||||
If this returns @racket[#f], @racket[(cvc5)] will not succeed
|
|
||||||
without its optional @racket[path] argument.}
|
|
||||||
|
|
||||||
@subsection{STP}
|
|
||||||
|
|
||||||
@defmodule[rosette/solver/smt/stp #:no-declare]
|
|
||||||
|
|
||||||
@defproc*[([(stp [#:path path (or/c path-string? #f) #f]
|
|
||||||
[#:logic logic (or/c symbol? #f) #f]
|
|
||||||
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
|
|
||||||
[(stp? [v any/c]) boolean?])]{
|
|
||||||
|
|
||||||
Returns a @racket[solver?] wrapper for the @hyperlink["https://stp.github.io/"]{STP} solver.
|
|
||||||
|
|
||||||
To use this solver, download prebuilt STP or build it yourself,
|
|
||||||
and ensure the executable is on your @tt{PATH} or pass the path to the
|
|
||||||
executable as the optional @racket[path] argument.
|
|
||||||
Rosette currently tests STP at commit
|
|
||||||
@tt{0510509a85b6823278211891cbb274022340fa5c}.
|
|
||||||
Note that as of December 2023, the STP version on Mac Homebrew is too old to be
|
|
||||||
supported by Rosette.
|
|
||||||
|
|
||||||
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
|
|
||||||
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
|
|
||||||
emitted constraints fall within the chosen logic. The default is @racket[#f],
|
|
||||||
which uses STP's default logic.
|
|
||||||
|
|
||||||
The @racket[options] argument provides additional options that are sent to STP
|
|
||||||
via the @tt{set-option} SMT command.
|
|
||||||
For example, setting @racket[options] to @racket[(hash ':seed 5)]
|
|
||||||
will send the command @tt{(set-option :seed 5)} to STP prior to solving.
|
|
||||||
}
|
|
||||||
|
|
||||||
@defproc[(stp-available?) boolean?]{
|
|
||||||
Returns true if the STP solver is available for use (i.e., Rosette can locate a @tt{stp} binary).
|
|
||||||
If this returns @racket[#f], @racket[(stp)] will not succeed
|
|
||||||
without its optional @racket[path] argument.}
|
|
||||||
|
|
||||||
@subsection{Yices2}
|
|
||||||
|
|
||||||
@defmodule[rosette/solver/smt/yices #:no-declare]
|
|
||||||
|
|
||||||
@defproc*[([(yices [#:path path (or/c path-string? #f) #f]
|
|
||||||
[#:logic logic (or/c symbol? #f) 'QF_BV]
|
|
||||||
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
|
|
||||||
[(yices? [v any/c]) boolean?])]{
|
|
||||||
|
|
||||||
Returns a @racket[solver?] wrapper for the @hyperlink["https://yices.csl.sri.com/"]{Yices2} solver.
|
|
||||||
|
|
||||||
To use this solver, download prebuilt Yices2 or build it yourself,
|
|
||||||
and ensure the executable is on your @tt{PATH} or pass the path to the
|
|
||||||
executable as the optional @racket[path] argument.
|
|
||||||
Rosette specifically uses the @tt{yices-smt2} executable, which is the Yices2
|
|
||||||
solver with its SMTLIB2 frontend enabled.
|
|
||||||
Note that just building (without installing) Yices2 will produce an executable
|
|
||||||
named @tt{yices_smt2}. Running the installation step produces an executable
|
|
||||||
with the correct name. However, it is safe to skip the installation step and
|
|
||||||
simply rename or symlink the @tt{yices_smt2} executable to @tt{yices-smt2}.
|
|
||||||
Rosette currently tests Yices2 at commit
|
|
||||||
@tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}.
|
|
||||||
|
|
||||||
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
|
|
||||||
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
|
|
||||||
emitted constraints fall within the chosen logic. Yices2 expects a logic to be
|
|
||||||
set; Rosette defaults to @racket['QF_BV].
|
|
||||||
|
|
||||||
The @racket[options] argument provides additional options that are sent to Yices2
|
|
||||||
via the @tt{set-option} SMT command.
|
|
||||||
For example, setting @racket[options] to @racket[(hash ':seed 5)]
|
|
||||||
will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving.
|
|
||||||
}
|
|
||||||
|
|
||||||
@defproc[(yices-available?) boolean?]{
|
|
||||||
Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary).
|
|
||||||
If this returns @racket[#f], @racket[(yices)] will not succeed
|
|
||||||
without its optional @racket[path] argument.}
|
|
||||||
|
|
||||||
|
|
||||||
@section{Solutions}
|
@section{Solutions}
|
||||||
|
|
||||||
A solution to a set of formulas may be satisfiable (@racket[sat?]), unsatisfiable (@racket[unsat?]),
|
A solution to a set of formulas may be satisfiable (@racket[sat?]), unsatisfiable (@racket[unsat?]),
|
||||||
|
|
|
||||||
|
|
@ -9,28 +9,21 @@
|
||||||
|
|
||||||
@(define rosette:onward13
|
@(define rosette:onward13
|
||||||
(make-bib
|
(make-bib
|
||||||
#:title @hyperlink["http://dl.acm.org/citation.cfm?id=2509586"]{Growing Solver-Aided Languages with Rosette}
|
#:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.onward13.pdf"]{Growing Solver-Aided Languages with Rosette}
|
||||||
#:author (authors "Emina Torlak" "Rastislav Bodik")
|
#:author (authors "Emina Torlak" "Rastislav Bodik")
|
||||||
#:date 2013
|
#:date 2013
|
||||||
#:location "New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)"))
|
#:location "New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)"))
|
||||||
|
|
||||||
@(define rosette:pldi14
|
@(define rosette:pldi14
|
||||||
(make-bib
|
(make-bib
|
||||||
#:title @hyperlink["http://dl.acm.org/citation.cfm?id=2594340"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
|
#:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.pldi14.pdf"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
|
||||||
#:author (authors "Emina Torlak" "Rastislav Bodik")
|
#:author (authors "Emina Torlak" "Rastislav Bodik")
|
||||||
#:date 2014
|
#:date 2014
|
||||||
#:location "Programming Language Design and Implementation (PLDI)"))
|
#:location "Programming Language Design and Implementation (PLDI)"))
|
||||||
|
|
||||||
@(define sympro:oopsla18
|
@(define sympro:oopsla18
|
||||||
(make-bib
|
(make-bib
|
||||||
#:title @hyperlink["https://dl.acm.org/citation.cfm?id=3276519"]{Finding Code That Explodes Under Symbolic Evaluation}
|
#:title @hyperlink["https://unsat.cs.washington.edu/papers/bornholt-sympro.pdf"]{Finding Code That Explodes Under Symbolic Evaluation}
|
||||||
#:author (authors "James Bornholt" "Emina Torlak")
|
#:author (authors "James Bornholt" "Emina Torlak")
|
||||||
#:date 2018
|
#:date 2018
|
||||||
#:location "Object Oriented Programming, Systems, Languages, and Applications (OOPSLA)"))
|
#:location "Object Oriented Programming, Systems, Languages, and Applications (OOPSLA)"))
|
||||||
|
|
||||||
@(define rosette:popl22
|
|
||||||
(make-bib
|
|
||||||
#:title @hyperlink["https://doi.org/10.1145/3498709"]{A Formal Foundation for Symbolic Evaluation with Merging}
|
|
||||||
#:author (authors "Sorawee Porncharoenwase" "Luke Nelson" "Xi Wang" "Emina Torlak")
|
|
||||||
#:date 2022
|
|
||||||
#:location "Principles of Programming Languages (POPL)"))
|
|
||||||
|
|
@ -4,7 +4,7 @@
|
||||||
@(require (for-label rosette/base/form/define rosette/query/query rosette/solver/solution
|
@(require (for-label rosette/base/form/define rosette/query/query rosette/solver/solution
|
||||||
(only-in rosette/base/base assert vc-true? vc) )
|
(only-in rosette/base/base assert vc-true? vc) )
|
||||||
racket/runtime-path racket/sandbox)
|
racket/runtime-path racket/sandbox)
|
||||||
@(require (only-in "../refs.scrbl" ~cite rosette:pldi14 rosette:popl22))
|
@(require (only-in "../refs.scrbl" ~cite rosette:pldi14))
|
||||||
@(require "../util/lifted.rkt")
|
@(require "../util/lifted.rkt")
|
||||||
|
|
||||||
@(define-runtime-path root ".")
|
@(define-runtime-path root ".")
|
||||||
|
|
@ -19,7 +19,7 @@ functionality}. In this chapter, we briefly discuss the @racketmodname[rosette]
|
||||||
dialect of the language, which exports all of Racket.
|
dialect of the language, which exports all of Racket.
|
||||||
|
|
||||||
Safe use of the full @racketmodname[rosette] language requires a basic understanding
|
Safe use of the full @racketmodname[rosette] language requires a basic understanding
|
||||||
of how Rosette's Symbolic Virtual Machine (SVM) works @~cite[rosette:pldi14 rosette:popl22].
|
of how Rosette's Symbolic Virtual Machine (SVM) works @~cite[rosette:pldi14].
|
||||||
Briefly, the SVM hijacks the normal Racket execution for all procedures and
|
Briefly, the SVM hijacks the normal Racket execution for all procedures and
|
||||||
constructs that are exported by @racketmodname[rosette/safe]. Any programs that are
|
constructs that are exported by @racketmodname[rosette/safe]. Any programs that are
|
||||||
implemented exclusively in the @racketmodname[rosette/safe] language are therefore
|
implemented exclusively in the @racketmodname[rosette/safe] language are therefore
|
||||||
|
|
|
||||||
|
|
@ -14,7 +14,10 @@
|
||||||
(experimental))))
|
(experimental))))
|
||||||
;; Documentation category. On Racket 6.3+ this can be any string.
|
;; Documentation category. On Racket 6.3+ this can be any string.
|
||||||
|
|
||||||
(define compile-omit-files '("lib/trace/report/node_modules"))
|
;; Runs the code in `private/install.rkt` before installing this collection.
|
||||||
|
(define pre-install-collection "private/install.rkt")
|
||||||
|
(define compile-omit-files '("private/install.rkt"
|
||||||
|
"lib/trace/report/node_modules"))
|
||||||
|
|
||||||
(define raco-commands
|
(define raco-commands
|
||||||
'(("symprofile"
|
'(("symprofile"
|
||||||
|
|
|
||||||
|
|
@ -48,11 +48,10 @@
|
||||||
|
|
||||||
(define-simple-macro (destruct val [pat:clause-pattern e:expr ...+] ...)
|
(define-simple-macro (destruct val [pat:clause-pattern e:expr ...+] ...)
|
||||||
#:do [(for-each check-duplicate-identifier! (attribute pat.id-set))]
|
#:do [(for-each check-duplicate-identifier! (attribute pat.id-set))]
|
||||||
#:with match-expr (syntax/loc this-syntax (match var [pat (begin e ...)] ...))
|
|
||||||
#:with result
|
#:with result
|
||||||
(syntax/loc this-syntax
|
(syntax/loc this-syntax
|
||||||
(for/all ([var val]);(guarded-values val)])
|
(for/all ([var val]);(guarded-values val)])
|
||||||
match-expr))
|
(match var [pat (begin e ...)] ...)))
|
||||||
result)
|
result)
|
||||||
|
|
||||||
(define-simple-macro (destruct* (val ...) [(pat:clause-pattern ...) e:expr ...+] ...)
|
(define-simple-macro (destruct* (val ...) [(pat:clause-pattern ...) e:expr ...+] ...)
|
||||||
|
|
|
||||||
|
|
@ -40,7 +40,7 @@
|
||||||
"Only install the compile handler; do not run the profiler"
|
"Only install the compile handler; do not run the profiler"
|
||||||
(run-profiler? #f)]
|
(run-profiler? #f)]
|
||||||
[("-m" "--module") name
|
[("-m" "--module") name
|
||||||
"Run submodule <name> (defaults to 'main')"
|
"Run submodule <name> (defaults to 'main)"
|
||||||
(module-name (string->symbol name))]
|
(module-name (string->symbol name))]
|
||||||
[("-r" "--racket")
|
[("-r" "--racket")
|
||||||
"Instrument code in any language, not just `#lang rosette`"
|
"Instrument code in any language, not just `#lang rosette`"
|
||||||
|
|
|
||||||
|
|
@ -29,7 +29,7 @@
|
||||||
|
|
||||||
;; SymPro options
|
;; SymPro options
|
||||||
[("-m" "--module") name
|
[("-m" "--module") name
|
||||||
"Run submodule <name> (defaults to 'main')"
|
"Run submodule <name> (defaults to 'main)"
|
||||||
(module-name (string->symbol name))]
|
(module-name (string->symbol name))]
|
||||||
[("-r" "--racket")
|
[("-r" "--racket")
|
||||||
"Instrument code in any language, not just `#lang rosette`"
|
"Instrument code in any language, not just `#lang rosette`"
|
||||||
|
|
|
||||||
|
|
@ -21,8 +21,6 @@
|
||||||
(string-prefix? (path->string (resolve-path a))
|
(string-prefix? (path->string (resolve-path a))
|
||||||
(path->string (resolve-path b))))
|
(path->string (resolve-path b))))
|
||||||
|
|
||||||
(define pkg-cache (make-hash))
|
|
||||||
|
|
||||||
(define (make-rosette-load/use-compiled pkgs-to-instrument)
|
(define (make-rosette-load/use-compiled pkgs-to-instrument)
|
||||||
(make-custom-load/use-compiled
|
(make-custom-load/use-compiled
|
||||||
#:blacklist
|
#:blacklist
|
||||||
|
|
@ -30,6 +28,6 @@
|
||||||
(cond
|
(cond
|
||||||
[(path-prefix? path (find-collects-dir)) #f]
|
[(path-prefix? path (find-collects-dir)) #f]
|
||||||
[else
|
[else
|
||||||
(match (path->pkg path #:cache pkg-cache)
|
(match (path->pkg path)
|
||||||
[#f #t]
|
[#f #t]
|
||||||
[pkg-name (member pkg-name pkgs-to-instrument)])]))))
|
[pkg-name (member pkg-name pkgs-to-instrument)])]))))
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,107 @@
|
||||||
|
#lang racket/base
|
||||||
|
|
||||||
|
;; Check whether z3 is installed during package setup.
|
||||||
|
;; If missing, builds & links a z3 binary.
|
||||||
|
|
||||||
|
|
||||||
|
(provide pre-installer)
|
||||||
|
|
||||||
|
(require racket/match
|
||||||
|
racket/file
|
||||||
|
racket/port
|
||||||
|
net/url
|
||||||
|
file/unzip)
|
||||||
|
|
||||||
|
(define (print-failure path msg)
|
||||||
|
(printf "\n\n********** Failed to install Z3 **********\n\n")
|
||||||
|
(printf "You'll need to manually install a Z3 binary\n")
|
||||||
|
(printf "to this location: ~a\n\n" path)
|
||||||
|
(printf "The problem was:\n~a\n\n" msg)
|
||||||
|
(printf "*********\n\n\n"))
|
||||||
|
|
||||||
|
(define (pre-installer collections-top-path racl-path)
|
||||||
|
(define bin-path (simplify-path (build-path racl-path ".." "bin")))
|
||||||
|
(define z3-path (build-path bin-path "z3"))
|
||||||
|
(with-handlers ([exn:fail? (lambda (e) (print-failure z3-path (exn-message e)))])
|
||||||
|
(unless (custom-z3-symlink? z3-path)
|
||||||
|
(define-values (z3-url z3-path-in-zip) (get-z3-url))
|
||||||
|
(define z3-port (get-pure-port (string->url z3-url) #:redirections 10))
|
||||||
|
(make-directory* bin-path) ;; Ensure that `bin-path` exists
|
||||||
|
(delete-directory/files z3-path #:must-exist? #f) ;; Delete old version of Z3, if any
|
||||||
|
(parameterize ([current-directory bin-path])
|
||||||
|
(call-with-unzip z3-port
|
||||||
|
(λ (dir)
|
||||||
|
(copy-directory/files (build-path dir z3-path-in-zip) z3-path)))
|
||||||
|
;; Unzipping loses file permissions, so we reset the z3 binary here
|
||||||
|
(file-or-directory-permissions
|
||||||
|
z3-path
|
||||||
|
(if (equal? (system-type) 'windows) #o777 #o755))))))
|
||||||
|
|
||||||
|
(define (custom-z3-symlink? z3-path)
|
||||||
|
(and (file-exists? z3-path)
|
||||||
|
(let ([p (simplify-path z3-path)])
|
||||||
|
(not (equal? (resolve-path p) p)))))
|
||||||
|
|
||||||
|
(define (get-z3-url)
|
||||||
|
(define site "https://github.com/Z3Prover/z3/releases/download")
|
||||||
|
(define version "z3-4.8.8")
|
||||||
|
(define-values (os exe)
|
||||||
|
(match (list (system-type) (system-type 'word))
|
||||||
|
['(unix 64) (values "x64-ubuntu-16.04" "z3")]
|
||||||
|
[`(macosx ,_) (values "x64-osx-10.14.6" "z3")]
|
||||||
|
['(windows 64) (values "x64-win" "z3.exe")]
|
||||||
|
[any (raise-user-error 'get-z3-url "Unknown system type '~a'" any)]))
|
||||||
|
(define name (format "~a-~a" version os))
|
||||||
|
(values
|
||||||
|
(format "~a/~a/~a.zip" site version name)
|
||||||
|
(format "~a/bin/~a" name exe)))
|
||||||
|
|
||||||
|
|
||||||
|
;; A copy of net/url's get-pure-port/headers, except with the Location header
|
||||||
|
;; for redirects made case-insensitive, fixing https://github.com/racket/racket/pull/3057
|
||||||
|
(require net/http-client net/url-connect)
|
||||||
|
(define (get-pure-port url #:redirections [redirections 0])
|
||||||
|
(let redirection-loop ([redirections redirections] [url url])
|
||||||
|
(define hc (http-conn-open (url-host url)
|
||||||
|
#:ssl? (if (equal? "https" (url-scheme url))
|
||||||
|
(current-https-protocol)
|
||||||
|
#f)))
|
||||||
|
(define access-string
|
||||||
|
(url->string
|
||||||
|
;; RFCs 1945 and 2616 say:
|
||||||
|
;; Note that the absolute path cannot be empty; if none is present in
|
||||||
|
;; the original URI, it must be given as "/" (the server root).
|
||||||
|
(let-values ([(abs? path)
|
||||||
|
(if (null? (url-path url))
|
||||||
|
(values #t (list (make-path/param "" '())))
|
||||||
|
(values (url-path-absolute? url) (url-path url)))])
|
||||||
|
(make-url #f #f #f #f abs? path (url-query url) (url-fragment url)))))
|
||||||
|
(http-conn-send! hc access-string #:method #"GET" #:content-decode '())
|
||||||
|
(define-values (status headers response-port)
|
||||||
|
(http-conn-recv! hc #:method #"GET" #:close? #t #:content-decode '()))
|
||||||
|
|
||||||
|
(define new-url
|
||||||
|
(ormap (λ (h)
|
||||||
|
(match (regexp-match #rx#"^[Ll]ocation: (.*)$" h)
|
||||||
|
[#f #f]
|
||||||
|
[(list _ m1b)
|
||||||
|
(define m1 (bytes->string/utf-8 m1b))
|
||||||
|
(with-handlers ((exn:fail? (λ (x) #f)))
|
||||||
|
(define next-url (string->url m1))
|
||||||
|
(make-url
|
||||||
|
(or (url-scheme next-url) (url-scheme url))
|
||||||
|
(or (url-user next-url) (url-user url))
|
||||||
|
(or (url-host next-url) (url-host url))
|
||||||
|
(or (url-port next-url) (url-port url))
|
||||||
|
(url-path-absolute? next-url)
|
||||||
|
(url-path next-url)
|
||||||
|
(url-query next-url)
|
||||||
|
(url-fragment next-url)))]))
|
||||||
|
headers))
|
||||||
|
(define redirection-status-line?
|
||||||
|
(regexp-match #rx#"^HTTP/[0-9]+[.][0-9]+ 3[0-9][0-9]" status))
|
||||||
|
(cond
|
||||||
|
[(and redirection-status-line? new-url (not (zero? redirections)))
|
||||||
|
(redirection-loop (- redirections 1) new-url)]
|
||||||
|
[else
|
||||||
|
response-port])))
|
||||||
|
|
@ -47,10 +47,7 @@
|
||||||
[(cons x y)
|
[(cons x y)
|
||||||
(cons (eval-rec x sol cache) (eval-rec y sol cache))]
|
(cons (eval-rec x sol cache) (eval-rec y sol cache))]
|
||||||
[(? vector?)
|
[(? vector?)
|
||||||
(let ([v (for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))])
|
(for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))]
|
||||||
(if (immutable? expr)
|
|
||||||
(vector->immutable-vector v)
|
|
||||||
v))]
|
|
||||||
[(? box?)
|
[(? box?)
|
||||||
((if (immutable? expr) box-immutable box) (eval-rec (unbox expr) sol cache))]
|
((if (immutable? expr) box-immutable box) (eval-rec (unbox expr) sol cache))]
|
||||||
[(? typed?)
|
[(? typed?)
|
||||||
|
|
|
||||||
|
|
@ -12,8 +12,6 @@
|
||||||
|
|
||||||
(provide (all-defined-out))
|
(provide (all-defined-out))
|
||||||
|
|
||||||
(define (unique/reverse xs)
|
|
||||||
(reverse (unique xs)))
|
|
||||||
|
|
||||||
(define (find-solver binary base-path [user-path #f])
|
(define (find-solver binary base-path [user-path #f])
|
||||||
(cond
|
(cond
|
||||||
|
|
@ -44,15 +42,14 @@
|
||||||
(unless (list? bools)
|
(unless (list? bools)
|
||||||
(raise-argument-error 'solver-assert "(listof boolean?)" bools))
|
(raise-argument-error 'solver-assert "(listof boolean?)" bools))
|
||||||
(define wfcheck-cache (mutable-set))
|
(define wfcheck-cache (mutable-set))
|
||||||
(set-solver-asserts!
|
(set-solver-asserts! self
|
||||||
self
|
(append (solver-asserts self)
|
||||||
(append (for/list ([b bools] #:unless (equal? b #t))
|
(for/list ([b bools] #:unless (equal? b #t))
|
||||||
(unless (or (boolean? b) (and (term? b) (equal? @boolean? (term-type b))))
|
(unless (or (boolean? b) (and (term? b) (equal? @boolean? (term-type b))))
|
||||||
(error 'assert "expected a boolean value, given ~s" b))
|
(error 'assert "expected a boolean value, given ~s" b))
|
||||||
(when wfcheck
|
(when wfcheck
|
||||||
(wfcheck b wfcheck-cache))
|
(wfcheck b wfcheck-cache))
|
||||||
b)
|
b))))
|
||||||
(solver-asserts self))))
|
|
||||||
|
|
||||||
(define (solver-minimize self nums)
|
(define (solver-minimize self nums)
|
||||||
(unless (null? nums)
|
(unless (null? nums)
|
||||||
|
|
@ -71,7 +68,7 @@
|
||||||
(server-shutdown (solver-server self)))
|
(server-shutdown (solver-server self)))
|
||||||
|
|
||||||
(define (solver-push self)
|
(define (solver-push self)
|
||||||
(match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env level) self)
|
(match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env level) self)
|
||||||
(server-write
|
(server-write
|
||||||
server
|
server
|
||||||
(begin
|
(begin
|
||||||
|
|
@ -93,7 +90,7 @@
|
||||||
(set-solver-level! self (drop level k)))
|
(set-solver-level! self (drop level k)))
|
||||||
|
|
||||||
(define (solver-check self [read-solution read-solution])
|
(define (solver-check self [read-solution read-solution])
|
||||||
(match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env _) self)
|
(match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env _) self)
|
||||||
(cond [(ormap false? asserts) (unsat)]
|
(cond [(ormap false? asserts) (unsat)]
|
||||||
[else (server-write
|
[else (server-write
|
||||||
server
|
server
|
||||||
|
|
@ -134,9 +131,7 @@
|
||||||
; core was extracted); #f (if the solution is
|
; core was extracted); #f (if the solution is
|
||||||
; 'unsat and no core was extracted); or 'unknown otherwise.
|
; 'unsat and no core was extracted); or 'unknown otherwise.
|
||||||
(define (read-solution server env #:unsat-core? [unsat-core? #f])
|
(define (read-solution server env #:unsat-core? [unsat-core? #f])
|
||||||
(decode (parse-solution server #:unsat-core? unsat-core?) env))
|
(decode
|
||||||
|
|
||||||
(define (parse-solution server #:unsat-core? [unsat-core? #f])
|
|
||||||
(parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
|
(parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
|
||||||
(match (server-read server (read))
|
(match (server-read server (read))
|
||||||
[(== 'sat)
|
[(== 'sat)
|
||||||
|
|
@ -144,11 +139,7 @@
|
||||||
(let loop ()
|
(let loop ()
|
||||||
(match (server-read server (read))
|
(match (server-read server (read))
|
||||||
[(list (== 'objectives) _ ...) (loop)]
|
[(list (== 'objectives) _ ...) (loop)]
|
||||||
; The SMT-LIB spec says that a model should be just a list of
|
[(list (== 'model) def ...)
|
||||||
; `define-fun`s, but many SMT solvers used to prefix that list
|
|
||||||
; with `model`, so let's support both versions.
|
|
||||||
; https://groups.google.com/g/smt-lib/c/5xpcIxdQ8-A/m/X4uQ7dIgAwAJ
|
|
||||||
[(or (list (== 'model) def ...) (list def ...))
|
|
||||||
(for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun)))
|
(for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun)))
|
||||||
(values (cadr d) d))]
|
(values (cadr d) d))]
|
||||||
[other (error 'read-solution "expected model, given ~a" other)]))]
|
[other (error 'read-solution "expected model, given ~a" other)]))]
|
||||||
|
|
@ -161,4 +152,5 @@
|
||||||
[other (error 'read-solution "expected unsat core, given ~a" other)]))
|
[other (error 'read-solution "expected unsat core, given ~a" other)]))
|
||||||
'unsat)]
|
'unsat)]
|
||||||
[(== 'unknown) 'unknown]
|
[(== 'unknown) 'unknown]
|
||||||
[other (error 'read-solution "unrecognized solver output: ~a" other)])))
|
[other (error 'read-solution "unrecognized solver output: ~a" other)]))
|
||||||
|
env))
|
||||||
|
|
|
||||||
|
|
@ -1,106 +0,0 @@
|
||||||
;;; Requires Bitwuzla 0.1.0 or later.
|
|
||||||
#lang racket
|
|
||||||
|
|
||||||
(require racket/runtime-path
|
|
||||||
"server.rkt" "cmd.rkt" "env.rkt"
|
|
||||||
"../solver.rkt" "../solution.rkt"
|
|
||||||
(prefix-in base/ "base-solver.rkt")
|
|
||||||
(only-in "../../base/core/term.rkt" term term? term-type constant? expression constant with-terms)
|
|
||||||
(only-in "../../base/core/bool.rkt" @boolean? @forall @exists)
|
|
||||||
(only-in "../../base/core/bitvector.rkt" bitvector bitvector? bv? bv bv-value @extract @sign-extend @zero-extend @bveq)
|
|
||||||
(only-in "../../base/core/function.rkt" function-domain function-range function? function fv)
|
|
||||||
(only-in "../../base/core/type.rkt" type-of)
|
|
||||||
(only-in "../../base/form/control.rkt" @if))
|
|
||||||
|
|
||||||
(provide (rename-out [make-bitwuzla bitwuzla]) bitwuzla? bitwuzla-available?)
|
|
||||||
|
|
||||||
(define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "bitwuzla"))
|
|
||||||
(define bitwuzla-opts '("-m"))
|
|
||||||
|
|
||||||
(define (bitwuzla-available?)
|
|
||||||
(not (false? (base/find-solver "bitwuzla" bitwuzla-path #f))))
|
|
||||||
|
|
||||||
(define (make-bitwuzla [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
|
|
||||||
(define config
|
|
||||||
(cond
|
|
||||||
[(bitwuzla? solver)
|
|
||||||
(base/solver-config solver)]
|
|
||||||
[else
|
|
||||||
(define real-bitwuzla-path (base/find-solver "bitwuzla" bitwuzla-path path))
|
|
||||||
(when (and (false? real-bitwuzla-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
|
||||||
(error 'bitwuzla "bitwuzla binary is not available (expected to be at ~a); try passing the #:path argument to (bitwuzla)" (path->string (simplify-path bitwuzla-path))))
|
|
||||||
(base/config options real-bitwuzla-path logic)]))
|
|
||||||
(bitwuzla (server (base/config-path config) bitwuzla-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
|
||||||
|
|
||||||
(struct bitwuzla base/solver ()
|
|
||||||
#:property prop:solver-constructor make-bitwuzla
|
|
||||||
#:methods gen:custom-write
|
|
||||||
[(define (write-proc self port mode) (fprintf port "#<bitwuzla>"))]
|
|
||||||
#:methods gen:solver
|
|
||||||
[
|
|
||||||
(define (solver-features self)
|
|
||||||
'(qf_bv))
|
|
||||||
|
|
||||||
(define (solver-options self)
|
|
||||||
(base/solver-options self))
|
|
||||||
|
|
||||||
(define (solver-assert self bools)
|
|
||||||
(base/solver-assert self bools bitwuzla-wfcheck))
|
|
||||||
|
|
||||||
(define (solver-minimize self nums)
|
|
||||||
(base/solver-minimize self nums))
|
|
||||||
|
|
||||||
(define (solver-maximize self nums)
|
|
||||||
(base/solver-maximize self nums))
|
|
||||||
|
|
||||||
(define (solver-clear self)
|
|
||||||
(base/solver-clear self))
|
|
||||||
|
|
||||||
(define (solver-shutdown self)
|
|
||||||
(base/solver-shutdown self))
|
|
||||||
|
|
||||||
(define (solver-push self)
|
|
||||||
(base/solver-push self))
|
|
||||||
|
|
||||||
(define (solver-pop self [k 1])
|
|
||||||
(base/solver-pop self k))
|
|
||||||
|
|
||||||
(define (solver-check self [read-solution base/read-solution])
|
|
||||||
(base/solver-check self read-solution))
|
|
||||||
|
|
||||||
(define (solver-debug self)
|
|
||||||
(base/solver-debug self))])
|
|
||||||
|
|
||||||
(define (set-default-options server)
|
|
||||||
void)
|
|
||||||
|
|
||||||
|
|
||||||
(define (valid-type? t)
|
|
||||||
(or (equal? t @boolean?)
|
|
||||||
(bitvector? t)
|
|
||||||
(and (function? t)
|
|
||||||
(for/and ([d (in-list (function-domain t))]) (valid-type? d))
|
|
||||||
(valid-type? (function-range t)))))
|
|
||||||
; Check whether a term v is well-formed for bitwuzla -- it must not mention
|
|
||||||
; types other than bitvectors, booleans, and uninterpreted functions over those
|
|
||||||
; types. If not, raise an exception.
|
|
||||||
(define (bitwuzla-wfcheck v [cache (mutable-set)])
|
|
||||||
(unless (set-member? cache v)
|
|
||||||
(set-add! cache v)
|
|
||||||
(cond
|
|
||||||
[(term? v)
|
|
||||||
(unless (valid-type? (type-of v))
|
|
||||||
(error 'bitwuzla "bitwuzla does not support values of type ~v (value: ~v)" (type-of v) v))
|
|
||||||
(match v
|
|
||||||
[(expression (or (== @forall) (== @exists)) vars body)
|
|
||||||
(error 'bitwuzla "bitwuzla does not support quantified formulas (value: ~v)" v)]
|
|
||||||
[(expression (== @extract) i j e)
|
|
||||||
(bitwuzla-wfcheck e cache)]
|
|
||||||
[(expression (or (== @sign-extend) (== @zero-extend)) v t)
|
|
||||||
(bitwuzla-wfcheck v cache)]
|
|
||||||
[(expression op es ...)
|
|
||||||
(for ([e es]) (bitwuzla-wfcheck e cache))]
|
|
||||||
[_ #t])]
|
|
||||||
[else
|
|
||||||
(unless (or (boolean? v) (bv? v))
|
|
||||||
(error 'bitwuzla "bitwuzla does not support value (expected boolean? or bv?): ~v" v))])))
|
|
||||||
|
|
@ -107,10 +107,27 @@
|
||||||
|
|
||||||
|
|
||||||
; Reads the SMT solution from the server.
|
; Reads the SMT solution from the server.
|
||||||
; This is the same as `base/read-solution` except that it applies some fixups
|
; The solution consists of 'sat or 'unsat, followed by
|
||||||
; for quirks in how various versions of Boolector have emitted models.
|
; followed by a suitably formatted s-expression. The
|
||||||
|
; output of this procedure is a hashtable from constant
|
||||||
|
; identifiers to their SMTLib values (if the solution is 'sat);
|
||||||
|
; a non-empty list of assertion identifiers that form an
|
||||||
|
; unsatisfiable core (if the solution is 'unsat and a
|
||||||
|
; core was extracted); #f (if the solution is
|
||||||
|
; 'unsat and no core was extracted); or 'unknown otherwise.
|
||||||
(define (boolector-read-solution server env)
|
(define (boolector-read-solution server env)
|
||||||
(define raw-model (base/parse-solution server))
|
(define raw-model
|
||||||
|
(parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
|
||||||
|
(match (server-read server (read))
|
||||||
|
[(== 'sat)
|
||||||
|
(server-write server (get-model))
|
||||||
|
(match (server-read server (read))
|
||||||
|
[(list (== 'model) ... (and def (list (== 'define-fun) _ ...)) ...)
|
||||||
|
(for/hash ([d def]) (values (cadr d) d))]
|
||||||
|
[other (error 'read-solution "expected model, given ~a" other)])]
|
||||||
|
[(== 'unsat) 'unsat]
|
||||||
|
[(== 'unknown) 'unknown]
|
||||||
|
[other (error 'read-solution "unrecognized solver output: ~a" other)])))
|
||||||
; First, we need to fix up the model's shadowing of incremental variables
|
; First, we need to fix up the model's shadowing of incremental variables
|
||||||
(define stripped-raw-model (if (hash? raw-model) (fixup-incremental-names raw-model) raw-model))
|
(define stripped-raw-model (if (hash? raw-model) (fixup-incremental-names raw-model) raw-model))
|
||||||
; Now decode in an environment with fake types for UFs
|
; Now decode in an environment with fake types for UFs
|
||||||
|
|
|
||||||
|
|
@ -1,68 +0,0 @@
|
||||||
#lang racket
|
|
||||||
|
|
||||||
(require racket/runtime-path
|
|
||||||
"server.rkt" "env.rkt"
|
|
||||||
"../solver.rkt"
|
|
||||||
(prefix-in base/ "base-solver.rkt"))
|
|
||||||
|
|
||||||
(provide (rename-out [make-cvc5 cvc5]) cvc5? cvc5-available?)
|
|
||||||
|
|
||||||
(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "cvc5"))
|
|
||||||
(define cvc5-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols"))
|
|
||||||
|
|
||||||
(define (cvc5-available?)
|
|
||||||
(not (false? (base/find-solver "cvc5" cvc5-path #f))))
|
|
||||||
|
|
||||||
(define (make-cvc5 [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
|
|
||||||
(define config
|
|
||||||
(cond
|
|
||||||
[(cvc5? solver)
|
|
||||||
(base/solver-config solver)]
|
|
||||||
[else
|
|
||||||
(define real-cvc5-path (base/find-solver "cvc5" cvc5-path path))
|
|
||||||
(when (and (false? real-cvc5-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
|
||||||
(error 'cvc5 "cvc5 binary is not available (expected to be at ~a); try passing the #:path argument to (cvc5)" (path->string (simplify-path cvc5-path))))
|
|
||||||
(base/config options real-cvc5-path logic)]))
|
|
||||||
(cvc5 (server (base/config-path config) cvc5-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
|
||||||
|
|
||||||
(struct cvc5 base/solver ()
|
|
||||||
#:property prop:solver-constructor make-cvc5
|
|
||||||
#:methods gen:custom-write
|
|
||||||
[(define (write-proc self port mode) (fprintf port "#<cvc5>"))]
|
|
||||||
#:methods gen:solver
|
|
||||||
[
|
|
||||||
(define (solver-features self)
|
|
||||||
'(qf_bv))
|
|
||||||
|
|
||||||
(define (solver-options self)
|
|
||||||
(base/solver-options self))
|
|
||||||
|
|
||||||
(define (solver-assert self bools)
|
|
||||||
(base/solver-assert self bools))
|
|
||||||
|
|
||||||
(define (solver-minimize self nums)
|
|
||||||
(base/solver-minimize self nums))
|
|
||||||
|
|
||||||
(define (solver-maximize self nums)
|
|
||||||
(base/solver-maximize self nums))
|
|
||||||
|
|
||||||
(define (solver-clear self)
|
|
||||||
(base/solver-clear self))
|
|
||||||
|
|
||||||
(define (solver-shutdown self)
|
|
||||||
(base/solver-shutdown self))
|
|
||||||
|
|
||||||
(define (solver-push self)
|
|
||||||
(base/solver-push self))
|
|
||||||
|
|
||||||
(define (solver-pop self [k 1])
|
|
||||||
(base/solver-pop self k))
|
|
||||||
|
|
||||||
(define (solver-check self)
|
|
||||||
(base/solver-check self))
|
|
||||||
|
|
||||||
(define (solver-debug self)
|
|
||||||
(base/solver-debug self))])
|
|
||||||
|
|
||||||
(define (set-default-options server)
|
|
||||||
void)
|
|
||||||
|
|
@ -14,8 +14,7 @@
|
||||||
@bvslt @bvsle @bvult @bvule
|
@bvslt @bvsle @bvult @bvule
|
||||||
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
||||||
@bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
@bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
||||||
@z3_ext_rotate_left @z3_ext_rotate_right
|
@concat @extract))
|
||||||
@concat @extract @sign-extend @zero-extend))
|
|
||||||
|
|
||||||
|
|
||||||
(provide decode-model)
|
(provide decode-model)
|
||||||
|
|
@ -117,6 +116,7 @@
|
||||||
(hash-ref ~env id)]
|
(hash-ref ~env id)]
|
||||||
[(== true) #t]
|
[(== true) #t]
|
||||||
[(== false) #f]
|
[(== false) #f]
|
||||||
|
[(? integer?) (inexact->exact expr)]
|
||||||
[(? real?) expr]
|
[(? real?) expr]
|
||||||
[(? symbol?)
|
[(? symbol?)
|
||||||
(cond
|
(cond
|
||||||
|
|
@ -132,10 +132,6 @@
|
||||||
(bv n (bitvector len))]
|
(bv n (bitvector len))]
|
||||||
[(list (list (== '_) (== 'extract) i j) s)
|
[(list (list (== '_) (== 'extract) i j) s)
|
||||||
`(, @extract ,(inline i sol ~env) ,(inline j sol ~env) ,(inline s sol ~env))]
|
`(, @extract ,(inline i sol ~env) ,(inline j sol ~env) ,(inline s sol ~env))]
|
||||||
[(list (list (== '_) (== 'sign_extend) i) s)
|
|
||||||
`(, @sign-extend ,(inline i sol ~env) ,(inline s sol ~env))]
|
|
||||||
[(list (list (== '_) (== 'zero_extend) i) s)
|
|
||||||
`(, @zero-extend ,(inline i sol ~env) ,(inline s sol ~env))]
|
|
||||||
[(list (== 'let) binds body)
|
[(list (== 'let) binds body)
|
||||||
(substitute (inline body sol ~env)
|
(substitute (inline body sol ~env)
|
||||||
(for/hash ([id:expr binds])
|
(for/hash ([id:expr binds])
|
||||||
|
|
@ -166,7 +162,6 @@
|
||||||
'bvslt @bvslt 'bvsle @bvsle 'bvult @bvult 'bvule @bvule
|
'bvslt @bvslt 'bvsle @bvsle 'bvult @bvult 'bvule @bvule
|
||||||
'bvnot @bvnot 'bvor @bvor 'bvand @bvand 'bvxor @bvxor
|
'bvnot @bvnot 'bvor @bvor 'bvand @bvand 'bvxor @bvxor
|
||||||
'bvshl @bvshl 'bvlshr @bvlshr 'bvashr @bvashr
|
'bvshl @bvshl 'bvlshr @bvlshr 'bvashr @bvashr
|
||||||
'ext_rotate_left @z3_ext_rotate_left 'ext_rotate_right @z3_ext_rotate_right
|
|
||||||
'bvneg @bvneg 'bvadd @bvadd 'bvmul @bvmul
|
'bvneg @bvneg 'bvadd @bvadd 'bvmul @bvmul
|
||||||
'bvudiv @bvudiv 'bvsdiv @bvsdiv
|
'bvudiv @bvudiv 'bvsdiv @bvsdiv
|
||||||
'bvurem @bvurem 'bvsrem @bvsrem
|
'bvurem @bvurem 'bvsrem @bvsrem
|
||||||
|
|
|
||||||
|
|
@ -16,7 +16,6 @@
|
||||||
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
||||||
@bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
@bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
||||||
@concat @extract @zero-extend @sign-extend
|
@concat @extract @zero-extend @sign-extend
|
||||||
@z3_ext_rotate_left @z3_ext_rotate_right
|
|
||||||
@integer->bitvector @bitvector->integer @bitvector->natural))
|
@integer->bitvector @bitvector->integer @bitvector->natural))
|
||||||
|
|
||||||
(provide enc)
|
(provide enc)
|
||||||
|
|
@ -109,7 +108,6 @@
|
||||||
[@bveq $=] [@bvslt $bvslt] [@bvsle $bvsle] [@bvult $bvult] [@bvule $bvule]
|
[@bveq $=] [@bvslt $bvslt] [@bvsle $bvsle] [@bvult $bvult] [@bvule $bvule]
|
||||||
[@bvnot $bvnot] [@bvor $bvor] [@bvand $bvand] [@bvxor $bvxor]
|
[@bvnot $bvnot] [@bvor $bvor] [@bvand $bvand] [@bvxor $bvxor]
|
||||||
[@bvshl $bvshl] [@bvlshr $bvlshr] [@bvashr $bvashr]
|
[@bvshl $bvshl] [@bvlshr $bvlshr] [@bvashr $bvashr]
|
||||||
[@z3_ext_rotate_left $ext_rotate_left] [@z3_ext_rotate_right $ext_rotate_right]
|
|
||||||
[@bvneg $bvneg] [@bvadd $bvadd] [@bvmul $bvmul] [@bvudiv $bvudiv] [@bvsdiv $bvsdiv]
|
[@bvneg $bvneg] [@bvadd $bvadd] [@bvmul $bvmul] [@bvudiv $bvudiv] [@bvsdiv $bvsdiv]
|
||||||
[@bvurem $bvurem] [@bvsrem $bvsrem] [@bvsmod $bvsmod] [@concat $concat])
|
[@bvurem $bvurem] [@bvsrem $bvsrem] [@bvsmod $bvsmod] [@concat $concat])
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -68,8 +68,7 @@
|
||||||
bvnot bvand bvor bvxor
|
bvnot bvand bvor bvxor
|
||||||
bvule bvult bvuge bvugt bvsle bvslt bvsge bvsgt
|
bvule bvult bvuge bvugt bvsle bvslt bvsge bvsgt
|
||||||
bvneg bvadd bvsub bvmul bvsdiv bvudiv bvurem bvsrem bvsmod
|
bvneg bvadd bvsub bvmul bvsdiv bvudiv bvurem bvsrem bvsmod
|
||||||
bvshl bvlshr bvashr concat
|
bvshl bvlshr bvashr concat)
|
||||||
ext_rotate_left ext_rotate_right)
|
|
||||||
|
|
||||||
(define (extract i j s)
|
(define (extract i j s)
|
||||||
`((_ extract ,i ,j) ,s))
|
`((_ extract ,i ,j) ,s))
|
||||||
|
|
|
||||||
|
|
@ -1,69 +0,0 @@
|
||||||
#lang racket
|
|
||||||
|
|
||||||
(require racket/runtime-path
|
|
||||||
"server.rkt" "env.rkt"
|
|
||||||
"../solver.rkt"
|
|
||||||
(prefix-in base/ "base-solver.rkt"))
|
|
||||||
|
|
||||||
(provide (rename-out [make-stp stp]) stp? stp-available?)
|
|
||||||
|
|
||||||
(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
|
|
||||||
(define stp-opts '("--SMTLIB2"))
|
|
||||||
|
|
||||||
(define (stp-available?)
|
|
||||||
(not (false? (base/find-solver "stp" stp-path #f))))
|
|
||||||
|
|
||||||
(define (make-stp [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
|
|
||||||
(define config
|
|
||||||
(cond
|
|
||||||
[(stp? solver)
|
|
||||||
(base/solver-config solver)]
|
|
||||||
[else
|
|
||||||
(define real-stp-path (base/find-solver "stp" stp-path path))
|
|
||||||
(when (and (false? real-stp-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
|
||||||
(error 'stp "stp binary is not available (expected to be at ~a); try passing the #:path argument to (stp)" (path->string (simplify-path stp-path))))
|
|
||||||
(base/config options real-stp-path logic)]))
|
|
||||||
(stp (server (base/config-path config) stp-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
|
||||||
|
|
||||||
(struct stp base/solver ()
|
|
||||||
#:property prop:solver-constructor make-stp
|
|
||||||
#:methods gen:custom-write
|
|
||||||
[(define (write-proc self port mode) (fprintf port "#<stp>"))]
|
|
||||||
#:methods gen:solver
|
|
||||||
[
|
|
||||||
(define (solver-features self)
|
|
||||||
'(qf_bv))
|
|
||||||
|
|
||||||
(define (solver-options self)
|
|
||||||
(base/solver-options self))
|
|
||||||
|
|
||||||
(define (solver-assert self bools)
|
|
||||||
(base/solver-assert self bools))
|
|
||||||
|
|
||||||
(define (solver-minimize self nums)
|
|
||||||
(base/solver-minimize self nums))
|
|
||||||
|
|
||||||
(define (solver-maximize self nums)
|
|
||||||
(base/solver-maximize self nums))
|
|
||||||
|
|
||||||
(define (solver-clear self)
|
|
||||||
(base/solver-clear self))
|
|
||||||
|
|
||||||
(define (solver-shutdown self)
|
|
||||||
(base/solver-shutdown self))
|
|
||||||
|
|
||||||
(define (solver-push self)
|
|
||||||
(base/solver-push self))
|
|
||||||
|
|
||||||
(define (solver-pop self [k 1])
|
|
||||||
(base/solver-pop self k))
|
|
||||||
|
|
||||||
(define (solver-check self)
|
|
||||||
(base/solver-check self))
|
|
||||||
|
|
||||||
(define (solver-debug self)
|
|
||||||
(base/solver-debug self))])
|
|
||||||
|
|
||||||
(define (set-default-options server)
|
|
||||||
void)
|
|
||||||
|
|
||||||
|
|
@ -1,69 +0,0 @@
|
||||||
#lang racket
|
|
||||||
|
|
||||||
(require racket/runtime-path
|
|
||||||
"server.rkt" "env.rkt"
|
|
||||||
"../solver.rkt"
|
|
||||||
(prefix-in base/ "base-solver.rkt"))
|
|
||||||
|
|
||||||
(provide (rename-out [make-yices yices]) yices? yices-available?)
|
|
||||||
|
|
||||||
(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2"))
|
|
||||||
(define yices-opts '("--incremental"))
|
|
||||||
|
|
||||||
(define (yices-available?)
|
|
||||||
(not (false? (base/find-solver "yices-smt2" yices-path #f))))
|
|
||||||
(define default-logic 'QF_BV) ;; Yices2 needs a default logic set otherwise it will error
|
|
||||||
(define (make-yices [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f])
|
|
||||||
(define config
|
|
||||||
(cond
|
|
||||||
[(yices? solver)
|
|
||||||
(base/solver-config solver)]
|
|
||||||
[else
|
|
||||||
(define real-yices-path (base/find-solver "yices-smt2" yices-path path))
|
|
||||||
(when (and (false? real-yices-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
|
||||||
(error 'yices "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path))))
|
|
||||||
(base/config options real-yices-path logic)]))
|
|
||||||
(yices (server (base/config-path config) yices-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
|
||||||
|
|
||||||
(struct yices base/solver ()
|
|
||||||
#:property prop:solver-constructor make-yices
|
|
||||||
#:methods gen:custom-write
|
|
||||||
[(define (write-proc self port mode) (fprintf port "#<yices>"))]
|
|
||||||
#:methods gen:solver
|
|
||||||
[
|
|
||||||
(define (solver-features self)
|
|
||||||
'(qf_bv))
|
|
||||||
|
|
||||||
(define (solver-options self)
|
|
||||||
(base/solver-options self))
|
|
||||||
|
|
||||||
(define (solver-assert self bools)
|
|
||||||
(base/solver-assert self bools))
|
|
||||||
|
|
||||||
(define (solver-minimize self nums)
|
|
||||||
(base/solver-minimize self nums))
|
|
||||||
|
|
||||||
(define (solver-maximize self nums)
|
|
||||||
(base/solver-maximize self nums))
|
|
||||||
|
|
||||||
(define (solver-clear self)
|
|
||||||
(base/solver-clear self))
|
|
||||||
|
|
||||||
(define (solver-shutdown self)
|
|
||||||
(base/solver-shutdown self))
|
|
||||||
|
|
||||||
(define (solver-push self)
|
|
||||||
(base/solver-push self))
|
|
||||||
|
|
||||||
(define (solver-pop self [k 1])
|
|
||||||
(base/solver-pop self k))
|
|
||||||
|
|
||||||
(define (solver-check self)
|
|
||||||
(base/solver-check self))
|
|
||||||
|
|
||||||
(define (solver-debug self)
|
|
||||||
(base/solver-debug self))])
|
|
||||||
|
|
||||||
(define (set-default-options server)
|
|
||||||
void)
|
|
||||||
|
|
||||||
|
|
@ -30,9 +30,7 @@
|
||||||
[else
|
[else
|
||||||
(define real-z3-path (base/find-solver "z3" z3-path path))
|
(define real-z3-path (base/find-solver "z3" z3-path path))
|
||||||
(when (and (false? real-z3-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
(when (and (false? real-z3-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
||||||
(fprintf (current-error-port)
|
(printf "warning: could not find z3 executable at ~a\n" (path->string (simplify-path z3-path))))
|
||||||
"warning: could not find z3 executable at ~a\n"
|
|
||||||
(path->string (simplify-path z3-path))))
|
|
||||||
(define opts (hash-union default-options options #:combine (lambda (a b) b)))
|
(define opts (hash-union default-options options #:combine (lambda (a b) b)))
|
||||||
(base/config opts real-z3-path logic)]))
|
(base/config opts real-z3-path logic)]))
|
||||||
(z3 (server (base/config-path config) z3-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
(z3 (server (base/config-path config) z3-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
||||||
|
|
@ -54,10 +52,10 @@
|
||||||
(base/solver-assert self bools))
|
(base/solver-assert self bools))
|
||||||
|
|
||||||
(define (solver-minimize self nums)
|
(define (solver-minimize self nums)
|
||||||
(base/set-solver-mins! self (append (reverse (numeric-terms nums 'solver-minimize)) (base/solver-mins self))))
|
(base/set-solver-mins! self (append (base/solver-mins self) (numeric-terms nums 'solver-minimize))))
|
||||||
|
|
||||||
(define (solver-maximize self nums)
|
(define (solver-maximize self nums)
|
||||||
(base/set-solver-maxs! self (append (reverse (numeric-terms nums 'solver-maximize)) (base/solver-maxs self))))
|
(base/set-solver-maxs! self (append (base/solver-maxs self) (numeric-terms nums 'solver-maximize))))
|
||||||
|
|
||||||
(define (solver-clear self)
|
(define (solver-clear self)
|
||||||
(base/solver-clear-stacks! self)
|
(base/solver-clear-stacks! self)
|
||||||
|
|
|
||||||
|
|
@ -4,10 +4,6 @@
|
||||||
rosette/lib/roseunit
|
rosette/lib/roseunit
|
||||||
rosette/solver/smt/z3 rosette/solver/smt/cvc4
|
rosette/solver/smt/z3 rosette/solver/smt/cvc4
|
||||||
rosette/solver/smt/boolector
|
rosette/solver/smt/boolector
|
||||||
rosette/solver/smt/cvc5
|
|
||||||
rosette/solver/smt/bitwuzla
|
|
||||||
rosette/solver/smt/stp
|
|
||||||
rosette/solver/smt/yices
|
|
||||||
"config.rkt")
|
"config.rkt")
|
||||||
|
|
||||||
(error-print-width default-error-print-width)
|
(error-print-width default-error-print-width)
|
||||||
|
|
@ -42,7 +38,6 @@
|
||||||
"base/distinct.rkt"
|
"base/distinct.rkt"
|
||||||
"base/generics.rkt"
|
"base/generics.rkt"
|
||||||
"base/push-pop.rkt"
|
"base/push-pop.rkt"
|
||||||
"base/optimize-order.rkt"
|
|
||||||
"base/reflect.rkt"
|
"base/reflect.rkt"
|
||||||
"base/decode.rkt"
|
"base/decode.rkt"
|
||||||
"query/solve.rkt"
|
"query/solve.rkt"
|
||||||
|
|
@ -85,22 +80,6 @@
|
||||||
(when (boolector-available?)
|
(when (boolector-available?)
|
||||||
(printf "===== Running Boolector tests =====\n")
|
(printf "===== Running Boolector tests =====\n")
|
||||||
(run-tests-with-solver boolector))
|
(run-tests-with-solver boolector))
|
||||||
|
|
||||||
(when (cvc5-available?)
|
|
||||||
(printf "===== Running cvc5 tests =====\n")
|
|
||||||
(run-tests-with-solver cvc5))
|
|
||||||
|
|
||||||
(when (bitwuzla-available?)
|
|
||||||
(printf "===== Running bitwuzla tests =====\n")
|
|
||||||
(run-tests-with-solver bitwuzla))
|
|
||||||
|
|
||||||
(when (stp-available?)
|
|
||||||
(printf "===== Running stp tests =====\n")
|
|
||||||
(run-tests-with-solver stp))
|
|
||||||
|
|
||||||
(when (yices-available?)
|
|
||||||
(printf "===== Running Yices2 tests =====\n")
|
|
||||||
(run-tests-with-solver yices))
|
|
||||||
)
|
)
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
|
|
|
||||||
|
|
@ -1,27 +0,0 @@
|
||||||
#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)))
|
|
||||||
|
|
@ -14,10 +14,6 @@
|
||||||
(define-symbolic b @boolean?)
|
(define-symbolic b @boolean?)
|
||||||
(define-symbolic c @boolean?)
|
(define-symbolic c @boolean?)
|
||||||
|
|
||||||
(define (f type)
|
|
||||||
(define-symbolic x type)
|
|
||||||
x)
|
|
||||||
|
|
||||||
(define (check-ordered v1 v2)
|
(define (check-ordered v1 v2)
|
||||||
(check-true (and (or (term<? v1 v2) (term<? v2 v1))
|
(check-true (and (or (term<? v1 v2) (term<? v2 v1))
|
||||||
(not (and (term<? v1 v2) (term<? v2 v1))))))
|
(not (and (term<? v1 v2) (term<? v2 v1))))))
|
||||||
|
|
@ -53,47 +49,7 @@
|
||||||
(check-cached @/ x y)
|
(check-cached @/ x y)
|
||||||
(check-cached @remainder x y)
|
(check-cached @remainder x y)
|
||||||
(check-cached @= x y)
|
(check-cached @= x y)
|
||||||
(check-cached @< x y)
|
(check-cached @< x y)))
|
||||||
|
|
||||||
(f @integer?)
|
|
||||||
(check-exn #px"type should remain unchanged" (lambda () (f @boolean?)))))
|
|
||||||
|
|
||||||
(define clear-terms!+gc-terms!-tests
|
|
||||||
(test-suite+
|
|
||||||
"Tests for clear-terms! and gc-terms!"
|
|
||||||
|
|
||||||
(with-terms '()
|
|
||||||
(let ()
|
|
||||||
(define-symbolic x y z @integer?)
|
|
||||||
(define a (@+ x 1))
|
|
||||||
(define b (@+ y 2))
|
|
||||||
(define c (@+ z 3))
|
|
||||||
(check-equal? (length (terms)) 6)
|
|
||||||
|
|
||||||
;; this should evict z and c
|
|
||||||
(clear-terms! (list z))
|
|
||||||
|
|
||||||
(check-equal? (length (terms)) 4)
|
|
||||||
|
|
||||||
;; this doesn't affect strongly-held values
|
|
||||||
(set! b #f)
|
|
||||||
|
|
||||||
(check-equal? (length (terms)) 4)
|
|
||||||
|
|
||||||
(gc-terms!) ; change the representation
|
|
||||||
(collect-garbage)
|
|
||||||
|
|
||||||
(check-equal? (length (terms)) 3)
|
|
||||||
|
|
||||||
(clear-terms! (list x))
|
|
||||||
(collect-garbage)
|
|
||||||
|
|
||||||
(check-equal? (length (terms)) 1)
|
|
||||||
|
|
||||||
;; this is a dummy check to reference a, b, and c so that
|
|
||||||
;; they are not garbage-collected earlier
|
|
||||||
(check-equal? (length (list a b c)) 3)))))
|
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
(time (run-tests value-tests))
|
(time (run-tests value-tests)))
|
||||||
(time (run-tests clear-terms!+gc-terms!-tests)))
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue