The cl-smt-lib Reference Manual

Table of Contents

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 3.0 "Montgomery Scott" on Wed Oct 13 10:10:10 2021 GMT+0.


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

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.


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

2 Systems

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


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

2.1 cl-smt-lib

Author

Eric Schulte <eschulte@grammatech.com>

License

BSD-3-Clause

Description

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

Version

1.0.0

Defsystem Dependency

asdf-package-system

Dependency

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

Source

cl-smt-lib.asd (file)


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

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

Author

Eric Schulte <eschulte@grammatech.com>

License

BSD-3-Clause

Dependencies
Source

cl-smt-lib.asd (file)

Component

file-type.lisp (file)


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

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 (file)

Component

file-type.lisp (file)


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

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

Author

Eric Schulte <eschulte@grammatech.com>

License

BSD-3-Clause

Dependency

trivial-gray-streams

Source

cl-smt-lib.asd (file)

Component

file-type.lisp (file)


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

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


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.1 cl-smt-lib.asd

Location

cl-smt-lib.asd

Systems

Next: , Previous: , Up: Lisp files   [Contents][Index]

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

Parent

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

Location

cl-smt-lib.lisp

Packages

cl-smt-lib/cl-smt-lib

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

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

Parent

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

Location

process-two-way-stream.lisp

Packages

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

Exported Definitions

Previous: , Up: Lisp files   [Contents][Index]

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

Parent

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

Location

fundamental-two-way-stream.lisp

Packages

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

Exported Definitions

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

4 Packages

Packages are listed by definition order.


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

4.1 cl-smt-lib/cl-smt-lib

Source

file-type.lisp (file)

Nickname

cl-smt-lib

Use List
Exported Definitions
Internal Definitions

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

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

Source

file-type.lisp (file)

Use List
Used By List

cl-smt-lib/cl-smt-lib

Exported Definitions

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

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

Source

file-type.lisp (file)

Use List
Used By List

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

Exported Definitions

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

5 Definitions

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


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

5.1 Exported definitions


Next: , Previous: , Up: Exported definitions   [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 (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

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 (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.3 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 (file)

Function: make-smt PROGRAM &rest ARGS

Wrap PROCESS in an SMT object.

Package

cl-smt-lib/cl-smt-lib

Source

file-type.lisp (file)

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 (file)

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 (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.4 Generic functions

Generic Function: input OBJECT
Generic Function: (setf input) NEW-VALUE OBJECT
Package

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

Methods
Method: input (FUNDAMENTAL-TWO-WAY-STREAM fundamental-two-way-stream)

automatically generated reader method

Source

file-type.lisp (file)

Method: (setf input) NEW-VALUE (FUNDAMENTAL-TWO-WAY-STREAM fundamental-two-way-stream)

automatically generated writer method

Source

file-type.lisp (file)

Generic Function: output OBJECT
Generic Function: (setf output) NEW-VALUE OBJECT
Package

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

Methods
Method: output (FUNDAMENTAL-TWO-WAY-STREAM fundamental-two-way-stream)

automatically generated reader method

Source

file-type.lisp (file)

Method: (setf output) NEW-VALUE (FUNDAMENTAL-TWO-WAY-STREAM fundamental-two-way-stream)

automatically generated writer method

Source

file-type.lisp (file)

Generic Function: process OBJECT
Package

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

Methods
Method: process (PROCESS-TWO-WAY-STREAM process-two-way-stream)

automatically generated reader method

Source

file-type.lisp (file)


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.5 Conditions

Condition: smt-error ()
Package

cl-smt-lib/cl-smt-lib

Source

file-type.lisp (file)

Direct superclasses

error (condition)

Direct methods
Direct slots
Slot: text
Initargs

:text

Initform

(quote nil)

Readers

text (generic function)

Slot: smt
Initargs

:smt

Initform

(quote nil)

Readers

smt (generic function)


Previous: , Up: Exported definitions   [Contents][Index]

5.1.6 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 (file)

Direct superclasses
  • fundamental-output-stream (class)
  • fundamental-input-stream (class)
Direct subclasses

process-two-way-stream (class)

Direct methods
  • stream-finish-output (method)
  • stream-write-string (method)
  • stream-write-sequence (method)
  • stream-write-char (method)
  • stream-line-column (method)
  • stream-unread-char (method)
  • stream-read-sequence (method)
  • stream-read-line (method)
  • stream-read-char-no-hang (method)
  • stream-read-char (method)
  • output (method)
  • output (method)
  • input (method)
  • input (method)
Direct slots
Slot: input
Initargs

:input

Readers

input (generic function)

Writers

(setf input) (generic function)

Slot: output
Initargs

:output

Readers

output (generic function)

Writers

(setf output) (generic function)

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 (file)

Direct superclasses

fundamental-two-way-stream (class)

Direct subclasses

smt (class)

Direct methods

process (method)

Direct slots
Slot: process
Initargs

:process

Initform

(error "process argument is required")

Readers

process (generic function)


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

5.2 Internal definitions


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.1 Functions

Function: read-preserving-case STREAM CHAR N
Package

cl-smt-lib/cl-smt-lib

Source

file-type.lisp (file)


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.2 Generic functions

Generic Function: smt CONDITION
Package

cl-smt-lib/cl-smt-lib

Methods
Method: smt (CONDITION smt-error)
Source

file-type.lisp (file)

Generic Function: text CONDITION
Package

cl-smt-lib/cl-smt-lib

Methods
Method: text (CONDITION smt-error)
Source

file-type.lisp (file)


Previous: , Up: Internal definitions   [Contents][Index]

5.2.3 Classes

Class: smt ()

An SMT process with input and output streams.

Package

cl-smt-lib/cl-smt-lib

Source

file-type.lisp (file)

Direct superclasses

process-two-way-stream (class)


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

Appendix A Indexes


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

A.1 Concepts

Jump to:   C   F   L  
Index Entry  Section

C
cl-smt-lib.asd: The cl-smt-lib․asd file
cl-smt-lib/cl-smt-lib/file-type.lisp: The cl-smt-lib/cl-smt-lib/file-type․lisp file
cl-smt-lib/fundamental-two-way-stream/file-type.lisp: The cl-smt-lib/fundamental-two-way-stream/file-type․lisp file
cl-smt-lib/process-two-way-stream/file-type.lisp: The cl-smt-lib/process-two-way-stream/file-type․lisp file

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

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

Jump to:   C   F   L  

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): Exported generic functions
(setf input): Exported generic functions
(setf output): Exported generic functions
(setf output): Exported generic functions

F
Function, make-process-two-way-stream: Exported functions
Function, make-smt: Exported functions
Function, read-from-smt: Exported functions
Function, read-preserving-case: Internal functions
Function, write-to-smt: Exported functions

G
Generic Function, (setf input): Exported generic functions
Generic Function, (setf output): Exported generic functions
Generic Function, input: Exported generic functions
Generic Function, output: Exported generic functions
Generic Function, process: Exported generic functions
Generic Function, smt: Internal generic functions
Generic Function, text: Internal generic functions

I
input: Exported generic functions
input: Exported generic functions

M
Macro, with-smt: Exported macros
make-process-two-way-stream: Exported functions
make-smt: Exported functions
Method, (setf input): Exported generic functions
Method, (setf output): Exported generic functions
Method, input: Exported generic functions
Method, output: Exported generic functions
Method, process: Exported generic functions
Method, smt: Internal generic functions
Method, text: Internal generic functions

O
output: Exported generic functions
output: Exported generic functions

P
process: Exported generic functions
process: Exported generic functions

R
read-from-smt: Exported functions
read-preserving-case: Internal functions

S
smt: Internal generic functions
smt: Internal generic functions

T
text: Internal generic functions
text: Internal generic functions

W
with-smt: Exported macros
write-to-smt: Exported functions

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

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

A.3 Variables

Jump to:   *  
I   O   P   S   T  
Index Entry  Section

*
*smt-debug*: Exported special variables

I
input: Exported classes

O
output: Exported classes

P
process: Exported classes

S
Slot, input: Exported classes
Slot, output: Exported classes
Slot, process: Exported classes
Slot, smt: Exported conditions
Slot, text: Exported conditions
smt: Exported conditions
Special Variable, *smt-debug*: Exported special variables

T
text: Exported conditions

Jump to:   *  
I   O   P   S   T  

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/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: Exported classes
Class, process-two-way-stream: Exported classes
Class, smt: Internal classes
Condition, smt-error: Exported conditions

F
fundamental-two-way-stream: Exported 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: Exported classes

S
smt: Internal classes
smt-error: Exported 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