Repository files navigation

pySMT makes working withSatisfiability Modulo Theory simple:

• Define formulae in asimple,intuitive, andsolver independent way
• Solve your formulae using one of the native solvers, or by wrappingany SMT-Lib compliant solver,
• Dump your problems in the SMT-Lib format,
• and more...

>>>frompysmt.shortcutsimportSymbol,And,Not,is_sat>>>>>>varA=Symbol("A")# Default type is Boolean>>>varB=Symbol("B")>>>f=And(varA,Not(varB))>>>f(A& (!B))>>>is_sat(f)True>>>g=f.substitute({varB:varA})>>>g(A& (!A))>>>is_sat(g)False

Is there a value for each letter (between 1 and 9) so that H+E+L+L+O = W+O+R+L+D = 25?

frompysmt.shortcutsimportSymbol,And,GE,LT,Plus,Equals,Int,get_modelfrompysmt.typingimportINThello= [Symbol(s,INT)forsin"hello"]world= [Symbol(s,INT)forsin"world"]letters=set(hello+world)domains=And([And(GE(l,Int(1)),LT(l,Int(10)))forlinletters])sum_hello=Plus(hello)# n-ary operators can take listssum_world=Plus(world)# as argumentsproblem=And(Equals(sum_hello,sum_world),Equals(sum_hello,Int(25)))formula=And(domains,problem)print("Serialization of the formula:")print(formula)model=get_model(formula)ifmodel:print(model)else:print("No solution found")

Portfolio solving consists of running multiple solvers inparallel. pySMT provides a simple interface to perform portfoliosolving using multiple solvers and multiple solver configurations.

frompysmt.shortcutsimportPortfolio,Symbol,Notx,y=Symbol("x"),Symbol("y")f=x.Implies(y)withPortfolio(["cvc5","yices",                ("msat", {"random_seed":1}),                ("msat", {"random_seed":17}),                ("msat", {"random_seed":42})],logic="QF_UFLIRA",incremental=False,generate_models=False)ass:s.add_assertion(f)s.push()s.add_assertion(x)res=s.solve()v_y=s.get_value(y)print(v_y)# TRUEs.pop()s.add_assertion(Not(y))res=s.solve()v_x=s.get_value(x)print(v_x)# FALSE

frompysmt.shortcutsimportSymbol,get_env,Solverfrompysmt.logicsimportQF_UFLRAname="mathsat-smtlib"# Note: The API version is called 'msat'# Path to the solver. The solver needs to take the smtlib file from# stdin. This might require creating a tiny shell script to set the# solver options.path= ["/tmp/mathsat"]logics= [QF_UFLRA,]# List of the supported logics# Add the solver to the environmentenv=get_env()env.factory.add_generic_solver(name,path,logics)# The solver name of the SMT-LIB solver can be now used anywhere# where pySMT would accept an API solver namewithSolver(name=name,logic="QF_UFLRA")ass:print(s.is_sat(Symbol("x")))# True

Check out more examples in theexamples/ directory and thedocumentation on ReadTheDocs

pySMT provides methods to define a formula in Linear Real Arithmetic(LRA), Real Difference Logic (RDL), Equalities and UninterpretedFunctions (EUF), Bit-Vectors (BV), Arrays (A), Strings (S) and theircombinations. The following solvers are supported through native APIs:

• MathSAT (http://mathsat.fbk.eu/)
• Z3 (https://github.com/Z3Prover/z3/)
• cvc5 (https://cvc5.github.io/)
• Yices 2 (http://yices.csl.sri.com/)
• CUDD (http://vlsi.colorado.edu/~fabio/CUDD/)
• PicoSAT (http://fmv.jku.at/picosat/)
• Boolector (http://fmv.jku.at/boolector/)

Additionally, you can use any SMT-LIB 2 compliant solver.

PySMT assumes that the python bindings for the SMT Solver areinstalled and accessible from yourPYTHONPATH.

You can install the latest stable release of pySMT from PyPI:

$ pip install pysmt

this will additionally install thepysmt-install command, that canbe used to install the solvers: e.g.,

$ pysmt-install --check

will show you which solvers have been found in yourPYTHONPATH.PySMT does not depend directly on any solver, but if you want toperform solving, you need to have at least one solver installed. Thiscan be used by pySMT via its native API, or passing through an SMT-LIBfile.

The scriptpysmt-install can be used to simplify the installation of the solvers:

$ pysmt-install --msat

will install MathSAT 5.

By default the solvers are downloaded, unpacked and built in your home directoryin the.smt_solvers folder. Compiled libraries and actual solver packages areinstalled in the relevantsite-packages directory (e.g. virtual environment'spackages root or local user-site).pysmt-install has many options tocustomize its behavior. If you have multiple versions of python in your system,we recommend the following syntax to run pysmt-install:python -m pysmt install.

Note: This script does not install requireddependencies for building the solver (e.g., make or gcc) and has beentested mainly on Linux Debian/Ubuntu systems. We suggest that yourefer to the documentation of each solver to understand how to installit with its python bindings.

For Yices, picosat, and CUDD, we use external wrappers:

• yicespy (https://github.com/pysmt/yicespy)
• repycudd (https://github.com/pysmt/repycudd)
• pyPicoSAT (https://github.com/pysmt/pyPicoSAT)

For instruction on how to use any SMT-LIB complaint solver with pySMTseeexamples/generic_smtlib.py

For more information, refer to onlinedocumentation on ReadTheDocs

The following table summarizes the features supported via pySMT foreach of the available solvers.

Solver	pySMT name	Supported Theories	Quantifiers	Quantifier Elimination	Unsat Core	Interpolation
MathSAT	msat	UF, LIA, LRA, BV, AX	No	msat-fm, msat-lw	Yes	Yes
Z3	z3	UF, LIA, LRA, BV, AX, NRA, NIA	Yes	z3	Yes	No
cvc5	cvc5	UF, LIA, LRA, BV, AX, S	Yes	No	No	No
Yices	yices	UF, LIA, LRA, BV	No	No	No	No
Boolector	btor	UF, BV, AX	No	No	No	No
SMT-Lib Interface	<custom>	UF, LIA, LRA, BV, AX	Yes	No	No	No
PicoSAT	picosat	[None]	No	[No]	No	No
BDD (CUDD)	bdd	[None]	Yes	bdd	No	No

pySMT is released under the APACHE 2.0 License.

For further questions, feel free to open an issue, or write topysmt@googlegroups.com (Browse the Archive).

If you use pySMT in your work, please consider citing:

@inproceedings{pysmt2015,  title={PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms},  author={Gario, Marco and Micheli, Andrea},  booktitle={SMT Workshop 2015},  year={2015}}