package smbc

  1. Overview
  2. Docs
Experimental model finder/SMT solver for functional programming

Install

Dune Dependency

Authors

Maintainers

Sources

0.6.tar.gz
md5=4ee7e4ae0796195da18ac4783bc8e2a8
sha512=6bd90c14a8a31d4d02ebeaa77c99e3722c751a75885b44d0d48ec43e987b503dc06e65c92519c0af3f17e536782e2c7a28fdf1e6d64eb959eec048fff8dbfb0a

Description

Tags

logic narrowing model smt

Published: 03 Jun 2019

README

SMBC

Experimental model finder/SMT solver for functional programming.

The underlying algorithm is described in a 2016 paper.

The code is under the BSD license.

Use

  • run on a problem (timeout 30s)

    smbc examples/regex_2.smt2 -t 30
    
  • get a list of options:

    smbc --help
    
  • verbose mode:

    smbc examples/regex_0.smt2 --debug 2
    
  • specify depth/depth-step:

    smbc examples/regex_0.smt2 --depth-step 3 --max-depth 200
    

Build

The recommended way is to use opam

opam pin 'https://github.com/c-cube/smbc.git#master'
opam install smbc

Or manually, using

opam install msat containers iter tip-parser
make

A Few Examples

We show a few example input files for smbc, along with the result.

examples/append.smt2

A wrong conjecture stating that append l1 l2 = append l2 l1 holds for every lists l1 and l2.

(declare-datatypes ()
 ((nat (s (select_s_0 nat)) (z))))
(declare-datatypes
   ()
   ((list (cons (select_cons_0 nat) (select_cons_1 list))
          (nil))))
(define-funs-rec
   ((append ((x list) (y list)) list))
   ((match x (case (cons n tail) (cons n (append tail y)))
             (case nil y))))
(assert-not
 (forall ((l1 list) (l2 list)) (= (append l1 l2) (append l2 l1))))

(check-sat)

Running smbc gives us a counter-example, the lists l1 = [s _] and l2 = [0]. Note that l1 is not fully defined, the ?nat_8 object is an unknown that can take any value of type nat. Whatever its value is, the counter-example holds because append l1 l2 != append l2 l1.

$ smbc examples/append.smt2
(result SAT :model ((val l2 (cons z nil))
                    (val l1 (cons (s ?nat_8) nil))))

examples/pigeon4.smt2

An instance of the classic pigeon-hole problem with 4 holes and 5 pigeons

(declare-sort hole 0)
(declare-fun h1 () hole)
(declare-fun h2 () hole)
(declare-fun h3 () hole)
(declare-fun h4 () hole)
(declare-fun p1 () hole)
(declare-fun p2 () hole)
(declare-fun p3 () hole)
(declare-fun p4 () hole)
(declare-fun p5 () hole)
(assert
 (and
  (not (= h1 h2)) (not (= h1 h3)) (not (= h1 h4))
  (not (= h2 h3)) (not (= h2 h4)) (not (= h3 h4))))
(assert
 (and
  (not (= p1 p2)) (not (= p1 p3)) (not (= p1 p4))
  (not (= p1 p5))
  (not (= p2 p3))
  (not (= p2 p4))
  (not (= p2 p5))
  (not (= p3 p4))
  (not (= p3 p5))
  (not (= p4 p5))))
(assert
  (forall ((p hole)) (or (= p h1) (= p h2) (= p h3) (= p h4))))
(check-sat)

We obtain (result UNSAT) since there is no way of satisfying the constraints.

Why the name?

"Sat Modulo Bounded Checking"

(and a reference to the awesome webcomics)

Note: Memory Profiling

opam sw 4.04.0+spacetime
make
OCAML_SPACETIME_INTERVAL=100 ./smbc.native --debug 1 --check examples/ty_infer.lisp
prof_spacetime serve spacetime-<PID> -e smbc.native

Dependencies (7)

  1. ocaml >= "4.03"
  2. tip-parser >= "0.6" & < "0.7"
  3. msat >= "0.8" & < "0.9"
  4. iter >= "1.0"
  5. containers >= "1.0" & < "2.7"
  6. base-bytes
  7. dune

Dev Dependencies

None

Used by

None

Conflicts

None