A python layer to interface with several SMTLIBv2 enabled SMT solvers
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
test
.gitignore
README.md
setup.py
smtlib.py

README.md

pysmtlib

A python layer to interface with several SMTlIBv2 enabled SMT solvers

Features

  • Serializable.
  • You can to save, replicate and send the solver state over the network
  • Python native integer operations. Operation on native python types are translates to smtlib transparently
  • Multiple solvers supported (Z3, YICES, CVC4)

#Example

        import pickle
        s = Solver()
        #make array of 32->8 bits
        array = s.mkArray(32)
        #make free 32bit bitvector 
        key = s.mkBitVec(32)

        #assert that the array is 'A' at key position
        array[key] = 'A'
        #lets restrict key to be greater than 1000
        s.add(key.ugt(1000))
        s = pickle.loads(pickle.dumps(s))
        self.assertEqual(s.check(), 'sat')
        self.checkLeak(s)

Tests

pysmtlib $ python -m unittest discover
........
----------------------------------------------------------------------
Ran 8 tests in 0.619s

OK