The cl-smt-lib Reference Manual

Table of Contents

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 Mon Dec 02 09:48:28 2019 GMT+0.

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 it's 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.

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

Dependency

named-readtables

Source

cl-smt-lib.asd (file)

Component

cl-smt-lib.lisp (file)

3 Files

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

3.1 Lisp

3.1.1 cl-smt-lib.asd

Location

cl-smt-lib.asd

Systems

cl-smt-lib (system)

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

Parent

cl-smt-lib (system)

Location

cl-smt-lib.lisp

Packages

cl-smt-lib

Exported Definitions

• *smt-debug* (special variable)
• make-smt (function)
• read-from-smt (function)
• smt-error (condition)
• smt-input-stream (function)
• smt-output-stream (function)
• smt-process (function)
• with-smt (macro)
• write-to-smt (function)

Internal Definitions

• %make-smt (function)
• read-preserving-case (function)
• smt (method)
• smt (structure)
• smt-bin (function)
• (setf smt-bin) (function)
• smt-bout (function)
• (setf smt-bout) (function)
• smt-cin-buffer (function)
• (setf smt-cin-buffer) (function)
• smt-in (function)
• (setf smt-in) (function)
• smt-in-buffer (function)
• (setf smt-in-buffer) (function)
• smt-in-index (function)
• (setf smt-in-index) (function)
• smt-input-char-pos (function)
• (setf smt-input-char-pos) (function)
• smt-misc (function)
• (setf smt-misc) (function)
• smt-n-bin (function)
• (setf smt-n-bin) (function)
• smt-out (function)
• (setf smt-out) (function)
• smt-sout (function)
• (setf smt-sout) (function)
• text (method)

4 Packages

Packages are listed by definition order.

4.1 cl-smt-lib

Source

cl-smt-lib.lisp (file)

Use List

• editor-hints.named-readtables
• common-lisp

Exported Definitions

• *smt-debug* (special variable)
• make-smt (function)
• read-from-smt (function)
• smt-error (condition)
• smt-input-stream (function)
• smt-output-stream (function)
• smt-process (function)
• with-smt (macro)
• write-to-smt (function)

Internal Definitions

• %make-smt (function)
• read-preserving-case (function)
• smt (generic function)
• smt (method)
• smt (structure)
• smt-bin (function)
• (setf smt-bin) (function)
• smt-bout (function)
• (setf smt-bout) (function)
• smt-cin-buffer (function)
• (setf smt-cin-buffer) (function)
• smt-in (function)
• (setf smt-in) (function)
• smt-in-buffer (function)
• (setf smt-in-buffer) (function)
• smt-in-index (function)
• (setf smt-in-index) (function)
• smt-input-char-pos (function)
• (setf smt-input-char-pos) (function)
• smt-misc (function)
• (setf smt-misc) (function)
• smt-n-bin (function)
• (setf smt-n-bin) (function)
• smt-out (function)
• (setf smt-out) (function)
• smt-sout (function)
• (setf smt-sout) (function)
• text (generic function)
• text (method)

5 Definitions

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

5.1 Exported definitions

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

Source

cl-smt-lib.lisp (file)

5.1.2 Macros

Macro: with-smt (SMT (PROGRAM &optional ARGS) &optional PRESERVE-CASE-P) &body BODY

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

5.1.3 Functions

Function: make-smt PROGRAM &optional ARGS

Wrap PROCESS in an SMT object

Package

cl-smt-lib

Source

cl-smt-lib.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

Source

cl-smt-lib.lisp (file)

Function: smt-input-stream INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-output-stream INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-process INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.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

Source

cl-smt-lib.lisp (file)

5.1.4 Conditions

Condition: smt-error ()

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Direct superclasses

error (condition)

Direct methods

• smt (method)
• text (method)

Direct slots

Slot: text

Initargs

:text

Initform

(quote nil)

Readers

text (generic function)

Slot: smt

Initargs

:smt

Initform

(quote nil)

Readers

smt (generic function)

5.2 Internal definitions

5.2.1 Functions

Function: %make-smt INPUT-STREAM OUTPUT-STREAM PROCESS

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: read-preserving-case STREAM CHAR N

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-bin INSTANCE

Function: (setf smt-bin) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-bout INSTANCE

Function: (setf smt-bout) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-cin-buffer INSTANCE

Function: (setf smt-cin-buffer) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-in INSTANCE

Function: (setf smt-in) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-in-buffer INSTANCE

Function: (setf smt-in-buffer) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-in-index INSTANCE

Function: (setf smt-in-index) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-input-char-pos INSTANCE

Function: (setf smt-input-char-pos) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-misc INSTANCE

Function: (setf smt-misc) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-n-bin INSTANCE

Function: (setf smt-n-bin) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-out INSTANCE

Function: (setf smt-out) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Function: smt-sout INSTANCE

Function: (setf smt-sout) VALUE INSTANCE

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

5.2.2 Generic functions

Generic Function: smt CONDITION

Package

cl-smt-lib

Methods

Method: smt (CONDITION smt-error)

Source

cl-smt-lib.lisp (file)

Generic Function: text CONDITION

Package

cl-smt-lib

Methods

Method: text (CONDITION smt-error)

Source

cl-smt-lib.lisp (file)

5.2.3 Structures

Structure: smt ()

Package

cl-smt-lib

Source

cl-smt-lib.lisp (file)

Direct superclasses

two-way-stream (structure)

Direct methods

print-object (method)

Direct slots

Slot: process

Initform

(sb-int:missing-arg)

Readers

smt-process (function)

Writers

(setf smt-process) (function)

Appendix A Indexes

A.1 Concepts

A.2 Functions

A.3 Variables

A.4 Data types