The cl-smt-lib Reference Manual

Next: , Previous: , Up: (dir)   [Contents][Index]

The cl-smt-lib Reference Manual

This is the cl-smt-lib Reference Manual, version 1.0.0, generated automatically by Declt version 4.0 beta 2 "William Riker" on Thu Sep 15 04:10:42 2022 GMT+0.

Table of Contents


1 Introduction

CL-SMT-LIB -- Common Lisp SMT-Lib Integration

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"))

Acknowledgment

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.


2 Systems

The main system appears first, followed by any subsystem dependency.


Next: , Previous: , Up: Systems   [Contents][Index]

2.1 cl-smt-lib

SMT object supporting SMT-LIB communication over input and output streams

Author

Eric Schulte <eschulte@grammatech.com>

License

BSD-3-Clause

Version

1.0.0

Defsystem Dependency

asdf-package-system (system).

Dependency

cl-smt-lib/cl-smt-lib (system).

Source

cl-smt-lib.asd.


2.2 cl-smt-lib/cl-smt-lib

Author

Eric Schulte <eschulte@grammatech.com>

License

BSD-3-Clause

Dependencies
Source

cl-smt-lib.asd.


2.3 cl-smt-lib/process-two-way-stream

Author

Eric Schulte <eschulte@grammatech.com>

License

BSD-3-Clause

Dependency

cl-smt-lib/fundamental-two-way-stream (system).

Source

cl-smt-lib.asd.


2.4 cl-smt-lib/fundamental-two-way-stream

Author

Eric Schulte <eschulte@grammatech.com>

License

BSD-3-Clause

Dependency

trivial-gray-streams (system).

Source

cl-smt-lib.asd.


3 Files

Files are sorted by type and then listed depth-first from the systems components trees.


Previous: , Up: Files   [Contents][Index]

3.1 Lisp


3.1.1 cl-smt-lib/cl-smt-lib.asd

Source

cl-smt-lib.asd.

Parent Component

cl-smt-lib (system).

ASDF Systems

3.1.2 cl-smt-lib/cl-smt-lib/file-type.lisp

Source

cl-smt-lib.asd.

Parent Component

cl-smt-lib/cl-smt-lib (system).

Packages

cl-smt-lib/cl-smt-lib.

Public Interface
Internals

3.1.3 cl-smt-lib/process-two-way-stream/file-type.lisp

Source

cl-smt-lib.asd.

Parent Component

cl-smt-lib/process-two-way-stream (system).

Packages

cl-smt-lib/process-two-way-stream.

Public Interface

3.1.4 cl-smt-lib/fundamental-two-way-stream/file-type.lisp

Source

cl-smt-lib.asd.

Parent Component

cl-smt-lib/fundamental-two-way-stream (system).

Packages

cl-smt-lib/fundamental-two-way-stream.

Public Interface

4 Packages

Packages are listed by definition order.


Next: , Previous: , Up: Packages   [Contents][Index]

4.1 cl-smt-lib/fundamental-two-way-stream

Source

file-type.lisp.

Use List
  • common-lisp.
  • trivial-gray-streams.
Used By List

cl-smt-lib/process-two-way-stream.

Public Interface

4.2 cl-smt-lib/cl-smt-lib

Source

file-type.lisp.

Nickname

cl-smt-lib

Use List
Public Interface
Internals

4.3 cl-smt-lib/process-two-way-stream

Source

file-type.lisp.

Use List
Used By List

cl-smt-lib/cl-smt-lib.

Public Interface

5 Definitions

Definitions are sorted by export status, category, package, and then by lexicographic order.


Next: , Previous: , Up: Definitions   [Contents][Index]

5.1 Public Interface


Next: , Previous: , Up: Public Interface   [Contents][Index]

5.1.1 Special variables

Special Variable: *smt-debug*

Set to a stream to duplicate smt input and output to the *SMT-DEBUG*.

Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.


5.1.2 Macros

Macro: with-smt ((smt (program &rest args) &optional preserve-case-p) &body body)
Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.


5.1.3 Ordinary functions

Function: make-process-two-way-stream (program &rest args)

Wrap PROCESS in an PROCESS-TWO-WAY-STREAM object.

Package

cl-smt-lib/process-two-way-stream.

Source

file-type.lisp.

Function: make-smt (program &rest args)

Wrap PROCESS in an SMT object.

Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.

Function: read-from-smt (smt &optional preserve-case-p eof-error-p eof-value)

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.

Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.

Function: write-to-smt (smt forms)

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.

Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.


5.1.4 Generic functions

Generic Reader: input (object)
Package

cl-smt-lib/fundamental-two-way-stream.

Methods
Reader Method: input ((fundamental-two-way-stream fundamental-two-way-stream))

automatically generated reader method

Source

file-type.lisp.

Target Slot

input.

Generic Writer: (setf input) (object)
Package

cl-smt-lib/fundamental-two-way-stream.

Methods
Writer Method: (setf input) ((fundamental-two-way-stream fundamental-two-way-stream))

automatically generated writer method

Source

file-type.lisp.

Target Slot

input.

Generic Reader: output (object)
Package

cl-smt-lib/fundamental-two-way-stream.

Methods
Reader Method: output ((fundamental-two-way-stream fundamental-two-way-stream))

automatically generated reader method

Source

file-type.lisp.

Target Slot

output.

Generic Writer: (setf output) (object)
Package

cl-smt-lib/fundamental-two-way-stream.

Methods
Writer Method: (setf output) ((fundamental-two-way-stream fundamental-two-way-stream))

automatically generated writer method

Source

file-type.lisp.

Target Slot

output.

Generic Reader: process (object)
Package

cl-smt-lib/process-two-way-stream.

Methods
Reader Method: process ((process-two-way-stream process-two-way-stream))

automatically generated reader method

Source

file-type.lisp.

Target Slot

process.


5.1.5 Standalone methods

Method: stream-finish-output ((stream fundamental-two-way-stream))
Package

sb-gray.

Source

file-type.lisp.

Method: stream-line-column ((stream fundamental-two-way-stream))
Package

sb-gray.

Source

file-type.lisp.

Method: stream-read-char ((stream fundamental-two-way-stream))
Package

sb-gray.

Source

file-type.lisp.

Method: stream-read-char-no-hang ((stream fundamental-two-way-stream))
Package

sb-gray.

Source

file-type.lisp.

Method: stream-read-line ((stream fundamental-two-way-stream))
Package

sb-gray.

Source

file-type.lisp.

Method: stream-read-sequence ((stream fundamental-two-way-stream) sequence start end &key &allow-other-keys)
Package

trivial-gray-streams.

Source

file-type.lisp.

Method: stream-unread-char ((stream fundamental-two-way-stream) character)
Package

sb-gray.

Source

file-type.lisp.

Method: stream-write-char ((stream fundamental-two-way-stream) character)
Package

sb-gray.

Source

file-type.lisp.

Method: stream-write-sequence ((stream fundamental-two-way-stream) sequence start end &key &allow-other-keys)
Package

trivial-gray-streams.

Source

file-type.lisp.

Method: stream-write-string ((stream fundamental-two-way-stream) string &optional start end)
Package

sb-gray.

Source

file-type.lisp.


5.1.6 Conditions

Condition: smt-error
Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.

Direct superclasses

error.

Direct methods
Direct slots
Slot: text
Initform

(quote nil)

Initargs

:text

Readers

text.

Writers

This slot is read-only.

Slot: smt
Initform

(quote nil)

Initargs

:smt

Readers

smt.

Writers

This slot is read-only.


Previous: , Up: Public Interface   [Contents][Index]

5.1.7 Classes

Class: fundamental-two-way-stream

A two-way stream composed of fundamental-{input,output}-streams.

Package

cl-smt-lib/fundamental-two-way-stream.

Source

file-type.lisp.

Direct superclasses
  • fundamental-input-stream.
  • fundamental-output-stream.
Direct subclasses

process-two-way-stream.

Direct methods
Direct slots
Slot: input
Initargs

:input

Readers

input.

Writers

(setf input).

Slot: output
Initargs

:output

Readers

output.

Writers

(setf output).

Class: process-two-way-stream

A fundamental-two-way-stream wrapping a single process’ input and output.

Package

cl-smt-lib/process-two-way-stream.

Source

file-type.lisp.

Direct superclasses

fundamental-two-way-stream.

Direct subclasses

smt.

Direct methods

process.

Direct slots
Slot: process
Initform

(error "process argument is required")

Initargs

:process

Readers

process.

Writers

This slot is read-only.


5.2 Internals


Next: , Previous: , Up: Internals   [Contents][Index]

5.2.1 Special variables

Special Variable: *print-nil-as-list*

When bound to non-nil print NIL as the empty list.

Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.


5.2.2 Ordinary functions

Function: read-preserving-case (stream char n)
Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.


Next: , Previous: , Up: Internals   [Contents][Index]

5.2.3 Generic functions

Generic Reader: smt (condition)
Package

cl-smt-lib/cl-smt-lib.

Methods
Reader Method: smt ((condition smt-error))
Source

file-type.lisp.

Target Slot

smt.

Generic Reader: text (condition)
Package

cl-smt-lib/cl-smt-lib.

Methods
Reader Method: text ((condition smt-error))
Source

file-type.lisp.

Target Slot

text.


Previous: , Up: Internals   [Contents][Index]

5.2.4 Classes

Class: smt

An SMT process with input and output streams.

Package

cl-smt-lib/cl-smt-lib.

Source

file-type.lisp.

Direct superclasses

process-two-way-stream.


Appendix A Indexes


Next: , Previous: , Up: Indexes   [Contents][Index]

A.1 Concepts


Next: , Previous: , Up: Indexes   [Contents][Index]

A.2 Functions

Jump to:   (  
F   G   I   M   O   P   R   S   T   W  
Index Entry  Section

(
(setf input): Public generic functions
(setf input): Public generic functions
(setf output): Public generic functions
(setf output): Public generic functions

F
Function, make-process-two-way-stream: Public ordinary functions
Function, make-smt: Public ordinary functions
Function, read-from-smt: Public ordinary functions
Function, read-preserving-case: Private ordinary functions
Function, write-to-smt: Public ordinary functions

G
Generic Function, (setf input): Public generic functions
Generic Function, (setf output): Public generic functions
Generic Function, input: Public generic functions
Generic Function, output: Public generic functions
Generic Function, process: Public generic functions
Generic Function, smt: Private generic functions
Generic Function, text: Private generic functions

I
input: Public generic functions
input: Public generic functions

M
Macro, with-smt: Public macros
make-process-two-way-stream: Public ordinary functions
make-smt: Public ordinary functions
Method, (setf input): Public generic functions
Method, (setf output): Public generic functions
Method, input: Public generic functions
Method, output: Public generic functions
Method, process: Public generic functions
Method, smt: Private generic functions
Method, stream-finish-output: Public standalone methods
Method, stream-line-column: Public standalone methods
Method, stream-read-char: Public standalone methods
Method, stream-read-char-no-hang: Public standalone methods
Method, stream-read-line: Public standalone methods
Method, stream-read-sequence: Public standalone methods
Method, stream-unread-char: Public standalone methods
Method, stream-write-char: Public standalone methods
Method, stream-write-sequence: Public standalone methods
Method, stream-write-string: Public standalone methods
Method, text: Private generic functions

O
output: Public generic functions
output: Public generic functions

P
process: Public generic functions
process: Public generic functions

R
read-from-smt: Public ordinary functions
read-preserving-case: Private ordinary functions

S
smt: Private generic functions
smt: Private generic functions
stream-finish-output: Public standalone methods
stream-line-column: Public standalone methods
stream-read-char: Public standalone methods
stream-read-char-no-hang: Public standalone methods
stream-read-line: Public standalone methods
stream-read-sequence: Public standalone methods
stream-unread-char: Public standalone methods
stream-write-char: Public standalone methods
stream-write-sequence: Public standalone methods
stream-write-string: Public standalone methods

T
text: Private generic functions
text: Private generic functions

W
with-smt: Public macros
write-to-smt: Public ordinary functions

Jump to:   (  
F   G   I   M   O   P   R   S   T   W  

Previous: , Up: Indexes   [Contents][Index]

A.4 Data types

Jump to:   C   F   P   S  
Index Entry  Section

C
cl-smt-lib: The cl-smt-lib system
cl-smt-lib.asd: The cl-smt-lib/cl-smt-lib․asd file
cl-smt-lib/cl-smt-lib: The cl-smt-lib/cl-smt-lib system
cl-smt-lib/cl-smt-lib: The cl-smt-lib/cl-smt-lib package
cl-smt-lib/fundamental-two-way-stream: The cl-smt-lib/fundamental-two-way-stream system
cl-smt-lib/fundamental-two-way-stream: The cl-smt-lib/fundamental-two-way-stream package
cl-smt-lib/process-two-way-stream: The cl-smt-lib/process-two-way-stream system
cl-smt-lib/process-two-way-stream: The cl-smt-lib/process-two-way-stream package
Class, fundamental-two-way-stream: Public classes
Class, process-two-way-stream: Public classes
Class, smt: Private classes
Condition, smt-error: Public conditions

F
File, cl-smt-lib.asd: The cl-smt-lib/cl-smt-lib․asd file
File, file-type.lisp: The cl-smt-lib/cl-smt-lib/file-type․lisp file
File, file-type.lisp: The cl-smt-lib/process-two-way-stream/file-type․lisp file
File, file-type.lisp: The cl-smt-lib/fundamental-two-way-stream/file-type․lisp file
file-type.lisp: The cl-smt-lib/cl-smt-lib/file-type․lisp file
file-type.lisp: The cl-smt-lib/process-two-way-stream/file-type․lisp file
file-type.lisp: The cl-smt-lib/fundamental-two-way-stream/file-type․lisp file
fundamental-two-way-stream: Public classes

P
Package, cl-smt-lib/cl-smt-lib: The cl-smt-lib/cl-smt-lib package
Package, cl-smt-lib/fundamental-two-way-stream: The cl-smt-lib/fundamental-two-way-stream package
Package, cl-smt-lib/process-two-way-stream: The cl-smt-lib/process-two-way-stream package
process-two-way-stream: Public classes

S
smt: Private classes
smt-error: Public conditions
System, cl-smt-lib: The cl-smt-lib system
System, cl-smt-lib/cl-smt-lib: The cl-smt-lib/cl-smt-lib system
System, cl-smt-lib/fundamental-two-way-stream: The cl-smt-lib/fundamental-two-way-stream system
System, cl-smt-lib/process-two-way-stream: The cl-smt-lib/process-two-way-stream system

Jump to:   C   F   P   S