Next: Introduction, Previous: (dir), Up: (dir) [Contents][Index]
This is the cl-smt-lib Reference Manual, version 1.0.0, generated automatically by Declt version 3.0 "Montgomery Scott" on Sun May 15 04:11:08 2022 GMT+0.
| • Introduction | What cl-smt-lib is all about | |
| • Systems | The systems documentation | |
| • Files | The files documentation | |
| • Packages | The packages documentation | |
| • Definitions | The symbols documentation | |
| • Indexes | Concepts, functions, variables and data types |
CL-SMT-LIB is a minimal package providing an SMT object encapsulating any SMT solver process supporting SMT-LIB with input and output streams. CL-SMT-LIB provides a reader macro to support reading case sensitive SMT-LIB forms into lisp and writing these forms to an SMT solver process.
The make-smt function takes a program name and command line
arguments and returns an smt object holding the process and the input
and output streams. This process may be read from and written to like
any other stream.
The #! reader macro, defined in the :cl-smt-lib read table using
the NAMED-READTABLES
package, enables case-sensitive reading of forms into common lisp.
The write-to-smt function facilitates writing case-sensitive forms
to the solver.
The following example demonstrates the use of CL-SMT-LIB to launch a solver process, write a query to the solver, and read back the results.
CL-SMT-LIB> (in-readtable :cl-smt-lib)
T
CL-SMT-LIB> (defparameter smt (make-smt "z3" "-in" "-smt2"))
SMT
CL-SMT-LIB> smt
#<SMT
:PROCESS #<SB-IMPL::PROCESS 24691 :RUNNING>
:INPUT-STREAM #<SB-SYS:FD-STREAM for "descriptor 10" {1002F3AB13}>
:OUTPUT-STREAM #<SB-SYS:FD-STREAM for "descriptor 9" {1002F3A713}>>
CL-SMT-LIB> (write-to-smt smt
(let ((range 8))
#!`((set-option :produce-models true)
(set-logic QF_BV)
(define-fun hamming-weight ((bv (_ BitVec ,RANGE)))
(_ BitVec ,RANGE)
,(REDUCE (LAMBDA (ACC N)
`(bvadd ,ACC ((_ zero_extend ,(1- RANGE))
((_ extract ,N ,N) bv))))
(LOOP :FOR I :UPFROM 1 :BELOW (1- RANGE) :COLLECT I)
:INITIAL-VALUE
`((_ zero_extend ,(1- RANGE)) ((_ extract 0 0) bv))))
(declare-const example1 (_ BitVec ,RANGE))
(declare-const example2 (_ BitVec ,RANGE))
(assert (= (_ bv3 ,RANGE) (hamming-weight example1)))
(assert (= (_ bv3 ,RANGE) (hamming-weight example2)))
(assert (distinct example1 example2))
(check-sat)
(get-model))))
NIL
CL-SMT-LIB> (read smt)
SAT
CL-SMT-LIB> (read smt)
(MODEL (DEFINE-FUN EXAMPLE2 NIL (_ BITVEC 8) 44)
(DEFINE-FUN EXAMPLE1 NIL (_ BITVEC 8) 97))
Since write-to-smt takes any stream as its first argument you can
preview the text sent to the smt solver by passing t as the first
argument.
CL-SMT-LIB> (write-to-smt t
(let ((range 8))
#!`((set-option :produce-models true)
(set-logic QF_BV)
(define-fun hamming-weight ((bv (_ BitVec ,RANGE)))
(_ BitVec ,RANGE)
,(REDUCE (LAMBDA (ACC N)
`(bvadd ,ACC ((_ zero_extend ,(1- RANGE))
((_ extract ,N ,N) bv))))
(LOOP :FOR I :UPFROM 1 :BELOW (1- RANGE) :COLLECT I)
:INITIAL-VALUE
`((_ zero_extend ,(1- RANGE)) ((_ extract 0 0) bv))))
(declare-const example1 (_ BitVec ,RANGE))
(declare-const example2 (_ BitVec ,RANGE))
(assert (= (_ bv3 ,RANGE) (hamming-weight example1)))
(assert (= (_ bv3 ,RANGE) (hamming-weight example2)))
(assert (distinct example1 example2))
(check-sat)
(get-model))))
(set-option :produce-models true)
(set-logic QF_BV)
(define-fun hamming-weight ((bv (_ BitVec 8))) (_ BitVec 8)
(bvadd
(bvadd
(bvadd
(bvadd
(bvadd
(bvadd ((_ zero_extend 7) ((_ extract 0 0) bv))
((_ zero_extend 7) ((_ extract 1 1) bv)))
((_ zero_extend 7) ((_ extract 2 2) bv)))
((_ zero_extend 7) ((_ extract 3 3) bv)))
((_ zero_extend 7) ((_ extract 4 4) bv)))
((_ zero_extend 7) ((_ extract 5 5) bv)))
((_ zero_extend 7) ((_ extract 6 6) bv))))
(declare-const example1 (_ BitVec 8))
(declare-const example2 (_ BitVec 8))
(assert (= (_ bv3 8) (hamming-weight example1)))
(assert (= (_ bv3 8) (hamming-weight example2)))
(assert (distinct example1 example2))
(check-sat)
(get-model)
NIL
CL-SMT-LIB>
The special variable *smt-debug* may be used to copy smt input and
output to a stream for debugging. Set *smt-debug* to t to echo
all input and output to STDOUT.
The following options should work to define smt objects for popular SMT solvers.
Z3
: (make-smt "z3" '("-in" "-smt2"))
CVC4
: (make-smt "cvc4" '("--lang=smt2"))
The project or effort depicted was sponsored by the Air Force Research Laboratory (AFRL) and the Defense Advanced Research Projects Agency (DARPA) under contract no. FA8750-15-C-0113. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of AFRL or DARPA.
Next: Files, Previous: Introduction, Up: Top [Contents][Index]
The main system appears first, followed by any subsystem dependency.
| • The cl-smt-lib system | ||
| • The cl-smt-lib/cl-smt-lib system | ||
| • The cl-smt-lib/process-two-way-stream system | ||
| • The cl-smt-lib/fundamental-two-way-stream system |
Next: The cl-smt-lib/cl-smt-lib system, Previous: Systems, Up: Systems [Contents][Index]
Eric Schulte <eschulte@grammatech.com>
BSD-3-Clause
SMT object supporting SMT-LIB communication over input and output streams
1.0.0
asdf-package-system
cl-smt-lib/cl-smt-lib (system)
cl-smt-lib.asd (file)
Next: The cl-smt-lib/process-two-way-stream system, Previous: The cl-smt-lib system, Up: Systems [Contents][Index]
Eric Schulte <eschulte@grammatech.com>
BSD-3-Clause
cl-smt-lib.asd (file)
file-type.lisp (file)
Next: The cl-smt-lib/fundamental-two-way-stream system, Previous: The cl-smt-lib/cl-smt-lib system, Up: Systems [Contents][Index]
Eric Schulte <eschulte@grammatech.com>
BSD-3-Clause
cl-smt-lib.asd (file)
file-type.lisp (file)
Previous: The cl-smt-lib/process-two-way-stream system, Up: Systems [Contents][Index]
Eric Schulte <eschulte@grammatech.com>
BSD-3-Clause
trivial-gray-streams
cl-smt-lib.asd (file)
file-type.lisp (file)
Files are sorted by type and then listed depth-first from the systems components trees.
| • Lisp files |
| • The cl-smt-lib.asd file | ||
| • The cl-smt-lib/cl-smt-lib/file-type.lisp file | ||
| • The cl-smt-lib/process-two-way-stream/file-type.lisp file | ||
| • The cl-smt-lib/fundamental-two-way-stream/file-type.lisp file |
Next: The cl-smt-lib/cl-smt-lib/file-type․lisp file, Previous: Lisp files, Up: Lisp files [Contents][Index]
cl-smt-lib.asd
Next: The cl-smt-lib/process-two-way-stream/file-type․lisp file, Previous: The cl-smt-lib․asd file, Up: Lisp files [Contents][Index]
cl-smt-lib/cl-smt-lib (system)
cl-smt-lib.lisp
Next: The cl-smt-lib/fundamental-two-way-stream/file-type․lisp file, Previous: The cl-smt-lib/cl-smt-lib/file-type․lisp file, Up: Lisp files [Contents][Index]
cl-smt-lib/process-two-way-stream (system)
process-two-way-stream.lisp
Previous: The cl-smt-lib/process-two-way-stream/file-type․lisp file, Up: Lisp files [Contents][Index]
fundamental-two-way-stream.lisp
Next: Definitions, Previous: Files, Up: Top [Contents][Index]
Packages are listed by definition order.
| • The cl-smt-lib/cl-smt-lib package | ||
| • The cl-smt-lib/process-two-way-stream package | ||
| • The cl-smt-lib/fundamental-two-way-stream package |
Next: The cl-smt-lib/process-two-way-stream package, Previous: Packages, Up: Packages [Contents][Index]
file-type.lisp (file)
cl-smt-lib
Next: The cl-smt-lib/fundamental-two-way-stream package, Previous: The cl-smt-lib/cl-smt-lib package, Up: Packages [Contents][Index]
file-type.lisp (file)
Previous: The cl-smt-lib/process-two-way-stream package, Up: Packages [Contents][Index]
file-type.lisp (file)
Definitions are sorted by export status, category, package, and then by lexicographic order.
| • Exported definitions | ||
| • Internal definitions |
Next: Internal definitions, Previous: Definitions, Up: Definitions [Contents][Index]
| • Exported special variables | ||
| • Exported macros | ||
| • Exported functions | ||
| • Exported generic functions | ||
| • Exported conditions | ||
| • Exported classes |
Next: Exported macros, Previous: Exported definitions, Up: Exported definitions [Contents][Index]
Set to a stream to duplicate smt input and output to the *SMT-DEBUG*.
file-type.lisp (file)
Next: Exported functions, Previous: Exported special variables, Up: Exported definitions [Contents][Index]
file-type.lisp (file)
Next: Exported generic functions, Previous: Exported macros, Up: Exported definitions [Contents][Index]
Wrap PROCESS in an PROCESS-TWO-WAY-STREAM object.
file-type.lisp (file)
Wrap PROCESS in an SMT object.
file-type.lisp (file)
Write FORMS to the process in SMT over it’s STDIN.
Sets READTABLE-CASE to :PRESERVE to ensure printing in valid
case-sensitive smt libv2 format.
file-type.lisp (file)
Write FORMS to the process in SMT over it’s STDIN.
Sets READTABLE-CASE to :PRESERVE to ensure printing in valid
case-sensitive smt libv2 format.
file-type.lisp (file)
Next: Exported conditions, Previous: Exported functions, Up: Exported definitions [Contents][Index]
automatically generated reader method
file-type.lisp (file)
automatically generated writer method
file-type.lisp (file)
automatically generated reader method
file-type.lisp (file)
automatically generated writer method
file-type.lisp (file)
automatically generated reader method
file-type.lisp (file)
Next: Exported classes, Previous: Exported generic functions, Up: Exported definitions [Contents][Index]
file-type.lisp (file)
error (condition)
:text
(quote nil)
text (generic function)
:smt
(quote nil)
smt (generic function)
Previous: Exported conditions, Up: Exported definitions [Contents][Index]
A two-way stream composed of fundamental-{input,output}-streams.
file-type.lisp (file)
process-two-way-stream (class)
:input
input (generic function)
(setf input) (generic function)
:output
output (generic function)
(setf output) (generic function)
A fundamental-two-way-stream wrapping a single process’ input and output.
file-type.lisp (file)
fundamental-two-way-stream (class)
smt (class)
process (method)
:process
(error "process argument is required")
process (generic function)
Previous: Exported definitions, Up: Definitions [Contents][Index]
| • Internal special variables | ||
| • Internal functions | ||
| • Internal generic functions | ||
| • Internal classes |
Next: Internal functions, Previous: Internal definitions, Up: Internal definitions [Contents][Index]
When bound to non-nil print NIL as the empty list.
file-type.lisp (file)
Next: Internal generic functions, Previous: Internal special variables, Up: Internal definitions [Contents][Index]
file-type.lisp (file)
Next: Internal classes, Previous: Internal functions, Up: Internal definitions [Contents][Index]
file-type.lisp (file)
file-type.lisp (file)
Previous: Internal generic functions, Up: Internal definitions [Contents][Index]
An SMT process with input and output streams.
file-type.lisp (file)
process-two-way-stream (class)
Previous: Definitions, Up: Top [Contents][Index]
| • Concept index | ||
| • Function index | ||
| • Variable index | ||
| • Data type index |
Next: Function index, Previous: Indexes, Up: Indexes [Contents][Index]
| Jump to: | C F L |
|---|
| Jump to: | C F L |
|---|
Next: Variable index, Previous: Concept index, Up: Indexes [Contents][Index]
| Jump to: | (
F G I M O P R S T W |
|---|
| Jump to: | (
F G I M O P R S T W |
|---|
Next: Data type index, Previous: Function index, Up: Indexes [Contents][Index]
| Jump to: | *
I O P S T |
|---|
| Jump to: | *
I O P S T |
|---|
Previous: Variable index, Up: Indexes [Contents][Index]
| Jump to: | C F P S |
|---|
| Jump to: | C F P S |
|---|