Skip to content

A python layer to interface with several SMTLIBv2 enabled SMT solvers

Notifications You must be signed in to change notification settings

feliam/pysmtlib

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

34 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

A python layer to interface with several SMTLIBv2 enabled SMT solvers

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages