pysmt/pysmt

pySMT: A library for SMT formulae manipulation and solving

pySMT: a Python API for SMT

pySMT makes working with Satisfiability Modulo Theory simple:

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

Usage

>>> from pysmt.shortcuts import Symbol, 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

A More Complex Example

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

from pysmt.shortcuts import Symbol, And, GE, LT, Plus, Equals, Int, get_model
from pysmt.typing import INT

hello = [Symbol(s, INT) for s in "hello"]
world = [Symbol(s, INT) for s in "world"]
letters = set(hello+world)
domains = And([And(GE(l, Int(1)),
                   LT(l, Int(10))) for l in letters])

sum_hello = Plus(hello) # n-ary operators can take lists
sum_world = Plus(world) # as arguments
problem = 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)
if model:
  print(model)
else:
  print("No solution found")

Portfolio

Portfolio solving consists of running multiple solvers in parallel. pySMT provides a simple interface to perform portfolio solving using multiple solvers and multiple solver configurations.

from pysmt.shortcuts import Portfolio, Symbol, Not

x, y = Symbol("x"), Symbol("y")
f = x.Implies(y)

with Portfolio(["cvc4",
                "yices",
                ("msat", {"random_seed": 1}),
                ("msat", {"random_seed": 17}),
                ("msat", {"random_seed": 42})],
               logic="QF_UFLIRA",
               incremental=False,
               generate_models=False) as s:
  s.add_assertion(f)
  s.push()
  s.add_assertion(x)
  res = s.solve()
  v_y = s.get_value(y)
  print(v_y) # TRUE

  s.pop()
  s.add_assertion(Not(y))
  res = s.solve()
  v_x = s.get_value(x)
  print(v_x) # FALSE

Using other SMT-LIB Solvers

from pysmt.shortcuts import Symbol, get_env, Solver
from pysmt.logics import QF_UFLRA

name = "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 environment
env = 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 name
with Solver(name=name, logic="QF_UFLRA") as s:
  print(s.is_sat(Symbol("x"))) # True

Check out more examples in the examples/ directory and the documentation on ReadTheDocs

Supported Theories and Solvers

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

• MathSAT (http://mathsat.fbk.eu/)
• Z3 (https://github.com/Z3Prover/z3/)
• CVC4 (http://cvc4.cs.nyu.edu/web/)
• 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 are installed and accessible from your PYTHONPATH.

Installation

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

$ pip install pysmt

this will additionally install the pysmt-install command, that can be used to install the solvers: e.g., :

$ pysmt-install --check

will show you which solvers have been found in your PYTHONPATH. PySMT does not depend directly on any solver, but if you want to perform solving, you need to have at least one solver installed. This can be used by pySMT via its native API, or passing through an SMT-LIB file.

The script pysmt-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 directory in the .smt_solvers folder. Compiled libraries and actual solver packages are installed in the relevant site-packages directory (e.g. virtual environment's packages root or local user-site). pysmt-install has many options to customize 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 required dependencies for building the solver (e.g., make or gcc) and has been tested mainly on Linux Debian/Ubuntu systems. We suggest that you refer to the documentation of each solver to understand how to install it 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 pySMT see examples/generic_smtlib.py

For more information, refer to online documentation on ReadTheDocs

Solvers Support

The following table summarizes the features supported via pySMT for each 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
CVC4	cvc4	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

License

pySMT is released under the APACHE 2.0 License.

For further questions, feel free to open an issue, or write to [email protected] (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}
}

pysmt's Issues

OSX: Solver Installation (pysmt-install)

This issue is to keep track of the status of support of OSX.
Each solver should be tested on OSX and, if it works, the installer (pysmt-install) should be able to build the solver and python binding. Finally, the CI should be extended to run the tests for the solver.
See the branch travis/macosx to see how we test for OSX on Travis CI.

Current situation:

• MathSAT: Tested on CI
• Z3: Tested on CI
• CVC4: Works on OSX; Installer needs to be extended
• Picosat: Works on OSX; Installer needs to be extended
• CUDD: Unknown
• Yices: Unknown
• Boolector: Unknown

Steps to go from "Unknown" to "Tested on CI":

• Check on the documentation of the solver, whether it is known to work (or not work) with OSX. If it should work, try to compile it and build the python bindings. Note that there might be a version of the solver available via external tools such as homebrew. If it works, please comment on this issue about the steps needed to get it to work (in some cases this is trivial, in some other cases it requires some tweaking). Please, include a list of the dependencies needed to make the installer work.
• Extend Installer (pysmt-install/ pysmt/cmd/installers/<solver>.py) to work on OSX. Adapt the existing code to work on OSX, and perform the steps described above. Open a PR against master once this is working. This will test that the installer still works on Linux (via Travis CI).
  Note: pysmt-install should not worry about installing dependencies, but please clearly state if there is some crucial dependency to be installed beforehand.
• Setup CI for OSX: Once pysmt-install works, modify .travis.yml in the branch travis/macosx in order to install all the dependencies needed by pysmt-install to work. Open a PR against travis/macosx once this is working.

Provide a deterministic unique id to fnodes at creation time

Solver.get_model should not try to assign a value to each variable in the environment

Implementation of get_model in the solvers using EagerModel, extracts one value for each symbol defined in the environment. This has a few problems:

1. In same cases we are doing much more work than needed
2. We cannot extract "partial models"
3. Symbols of type not supported by the solver (e.g., BV) will cause the solver to fail in the model creation.

Ideally, we should use iteration functions from the native solver API to extract models (if these are available).

Enable test-configuration in CI for Generic Wrapper

feature request: add a few more convenience methods

conjunctive_partition(), disjunctive_partition(), nnf() would be nice to have

Add SMT-LIB in README as Supported Solver

We should:

• Clarify that any SMT-LIB compatible solver can be wrapped
• Add an example of wrapping in the documentation

Failing Yices test (probably due to finite precision representation)

test_solving.py:do_model (added in branch bitvector_support) fails. The reason seems to be that the variables are assigned a value that is not precise enough:

Traceback (most recent call last):
  File "/home/viashino/pySMT/github/pysmt/test/__init__.py", line 88, in wrapper
    return test_fun(*args, **kwargs)
  File "/home/viashino/pySMT/github/pysmt/test/test_solving.py", line 215, in test_model_yices
    self.do_model("yices")
  File "/home/viashino/pySMT/github/pysmt/test/test_solving.py", line 187, in do_model
    self.assertEqual(simp, TRUE(), "%s -- %s" % (f, subs))
AssertionError: (((r + s) = 28/5) & (s < r)) -- {r: 4278419646001971/1125899906842624, s: 2026619832316723/1125899906842624}

The assertion error shows a formula and an assignment. The assignment should make the formula true, but this is not the case. Indeed s+r ~ 5.5998 instead of 28/5.

We can remove the test, but it would be nice to find a proper way of handling this.

Integrate install.py in setup.py and documentation

Now that we have a way to install the solvers we should:

1. Document it in the README
2. Integrate it with the setup.py, so that it can either be run during pip install or we add an alias pysmt_install that can be called by the user.

Extend Yices wrapper to use GMP for infinite precision

As explained in #78 we still have some cases that are not handled by the yices wrapper. We should therefore extend the wrapper to support these special cases, and possibly reimplement the wrapper in order to avoid the dependency from pyices.

scripts pysmt, pysmt-shell, pysmt-install fail with import errors

I did pip install pysmt, but when I run any of the scripts, I get an import error.

On running pysmt or pysmt-shell: ImportError: No module named shell
On running pysmt-install: ImportError: No module named install

Did you guys simply miss including install.py, shell.py while building the pypi package? I'm seeing the following diff between
https://github.com/pysmt/pysmt/archive/v0.2.3.tar.gz and https://pypi.python.org/packages/source/p/pySMT/PySMT-0.2.3.tar.gz:

diff -rq pysmt-0.2.3-github/ pysmt-0.2.3-pypi/

Only in pysmt-0.2.3-github/: .gitignore
Only in pysmt-0.2.3-github/: NOTICE
Only in pysmt-0.2.3-pypi/: PKG-INFO
Only in pysmt-0.2.3-pypi/: PySMT.egg-info
Only in pysmt-0.2.3-github/: SMT-LIB
Files pysmt-0.2.3-github/docs/CHANGES.rst and pysmt-0.2.3-pypi/docs/CHANGES.rst differ
Only in pysmt-0.2.3-github/docs: Makefile
Only in pysmt-0.2.3-github/docs: code_snippets
Only in pysmt-0.2.3-github/docs: conf.py
Only in pysmt-0.2.3-github/: examples
Only in pysmt-0.2.3-github/: health_check.sh
Only in pysmt-0.2.3-github/: install.py
Only in pysmt-0.2.3-github/: make_distrib.sh
Only in pysmt-0.2.3-github/: patches
Only in pysmt-0.2.3-github/pysmt/test: configs
Only in pysmt-0.2.3-github/pysmt/test/smtlib: bin
Only in pysmt-0.2.3-github/pysmt/test/smtlib: small_set
Only in pysmt-0.2.3-github/: run_all_tests.sh
Only in pysmt-0.2.3-github/: run_tests.sh
Only in pysmt-0.2.3-pypi/: setup.cfg
Only in pysmt-0.2.3-github/: shell.py
Only in pysmt-0.2.3-github/: shippable.sh
Only in pysmt-0.2.3-github/: shippable.yml

Update README and CHANGES

IFF node handling MathSAT

The IFF node a <-> b is currently handled in MathSAT by rewriting it to (a -> b) & (b -> a) in pysmt.solvers.msat.py

However, the MathSAT API supports it natively via the msat_make_iff() function. We should use ths function.

issues with infix notation

It seems that the infix notation has still some rough edges.
Some examples:
From the shell.py, using get_env().enable_infix_notation=True

x = Symbol('x', INT)
f = (x > Int(10))

works, but:

f = (x > 10)

raises an exception AttributeError: 'int' object has no attribute 'get_sons'.

Also:

f = (x == Int(10))

does not do what one would expect (i.e. it checks whether x and
Int(10) are equal, instead of building the equality formula).

Provide a definition of the common interface of Converter

All solvers share the same Converter interface. Although we do not have any way to enforce this requirement. We need to add a Converter interface that defines the key methods (convert and back) and a property for the solver to obtain the converter.

Provide support for getting the return type of a node

We shall provide support for a member function that returns the expected type of an FNode (without type-checking):

def get_sort(self):
    if not self.is_term():
        raise Exception("not a term")
    if self.is_bool_op():
        return BOOL
    elif self.is_int_constant():
        return INT
    ...
    elif self.is_symbol():
        return self.symbol_type()
    ...

feature request: support for get_implicant()

It would be nice to have a get_implicant(f) function, that returns an
SMT-level implicant for a satisfiable formula f (aka a T-consistent truth
assignment for the atoms of f, aka a "propositional" model that is
T-consistent).
Alternatively, what's the easiest way of achieving this?

PicoSAT UNSAT Cores

In #68 we add UNSAT cores support for MathSAT and Z3.

Also PicoSAT can produce cores and UNSAT assumptions, so we should extend our wrapper to support cores.

Extend quantifier eliminator interface to support logic specification

Currently, we assume that a quantifier eliminator is capable of quantifying UFLIRA.
A better approach would be to specify the logic as we do for solvers. This would also make it possible to integrate CUDD as Quantifier eliminator for BOOL.

FNode.get_dependencies() should become a walker

FNode.get_dependencies() is implemented recursively within FNode (via compute_dependencies).
This means that:

• The formula TREE is visited
• On deep formulas we have problems of recursion
• It is not extensible when new node types are introduced.

We can either replace compute_dependencies with a call to a proper walker, or we can introduce an additional method (to keep get_dependencies simple and independent from the environment).

Add examples in documentation and ad-hoc directory

Add the examples used in presentations/demos to the documentation, also as more advance tutorials.

Include the source-codes in an examples directory.

IdentityDagWalker lacks BV support

Unsat-cores Support

Add support for unsat cores

SMT-LIB Annotations

SMT-LIB annotations are currently not supported. We should extend the SMTLib script class to include a dictionary of annotations for the terms.

The class for keeping annotations should be designed independently so that it can be reused later inside the solvers (if needed).

(Experimental code for this feature exists)

Pasing options to Solvers / QuantifierEliminators / Interpolator

We should design a clean and simple way of passing options to the Solvers / QuantifierEliminators / Interpolator instances through the factory class

Module operator is missing

Mod operator is missing

Patches in python package

We are currently not distributing the patches in the python package.

After looking better into python packaging, I realized that this is a bit messy. I see two options:

1. Move patches within the package (pysmt/patches). This has the advantage that the patches are stored in a well-known location (within the package) and should be cross-platform. Although I don't like the idea of having the patches in the pkg source code.
2. Embed the patches in install.py during pkg creation (setup.py). This is unorthodox, but has the advantage that the patches are easy to find by install.py (that is also the only file needing them), and we do not pollute the source-tree.

@mikand What do you think? I have a demo for 1. I wanted to get your feedback before trying 2 (that should be easy -> gzip + BaseEncode)

PicoSAT solving under assumptions

Currently we use push/pop to support solving under assumptions in PicoSAT.
The PicoSAT API actually supports solving under assumptions, we should use that feature (similarly to MathSAT and Z3 solver wrappers)

Create Min, Max operators

Add shortcuts.Min as the operator: min{x1, ..., xn} . This should be handled by rewriting it as an ITE, and can be done by successive partitioning of the set: i.e.,

  min(x1, .., xn, xn+1, ... xm) = min( min(x1, ..., xn),  min(xn+1, ..., xm) )

Add explicit argument to install.py to define where to install solvers

install.py installs the solvers in the directory where pysmt has been installed. While this makes sense in most cases, it should be possible to configure it. In particular, if one installs pysmt system-wide, then it needs root access to install the solvers. This does not seem to be a good idea.

My proposal is to add a --target option (better name?) to specify the directory in which to install.

BDD ordering support

We shall consider adding support for static BDD ordering specification as well as dynamic reordering.
@cmattarei could be interested in this feature.

Environment reset and Dynamic Walker Functions

DWFs have been introduced to enable the introduction of new node types from outside pySMT. However, DWF functions are associated with the environment. This opens a bit of a design issue when resetting the environment. Currently, I am taking care of re-defining the DWFs everytime I reset the environment, but this is error-prone.

We should consider whether it makes sense to add an optional parameter to shortcuts.reset_env. More in general, we should define a proper interaction with the environment stack. I.e., what happens if I create a new environment within a context?

Not informative assertion for unsupported operators

The following code raises the exception "NotImplementedError", because the quantifier is not handled by the default logic.
I would excpect a better error reporting, e.g. "Not supported logic"

from pysmt.shortcuts import *
from pysmt.typing import BOOL
solver = Solver()
xs = Symbol("xs",BOOL)
solver.add_assertion(Exists([xs],xs))

Extend BV Support

The current implementation of bitvector could be extended in several directions:

• More solvers should support bitvectors (currently only mathsat's converter is enabled for BVs)
• Some derived operators (e.g., all the signed operators) are not implemented
• No simplification is performed on BV formulas.

Add methods in pysmt.test.TestCase

In many tests, we build a formula and test whether it is sat/unsat/valid. We should make these tests an assertion in the custom pysmt TestCase:

  def assertValid(self, formula, message=None, logic=None)
  def assertSat(self, formula, message=None, logic=None)
  def assertUnsat(self, formula, message=None, logic=None)

Create CONTRIBUTORS file and prepare CLA

make FNodes and walkers easier to use

It seems that FNodes have a lot of hardcoded information, that makes
using them somewhat inconvenient. For instance, I could not understand
how to retrieve the sort of a node in a generic way, without using big
"switch statements" over the node types (which are tedious and will
break as soon as some other node types are added). For symbols, there's
FNode.symbol_type(), but what about other nodes? For example, how do I
know that an AND is of Bool sort without knowing that it is an AND
operator?

Related to this, the use of walkers seems also quite verbose. From what
I understand, one needs to implement the various walk_* functions for
all the different nodes, because examining the node_type() is the only
way of retrieving all the information needed to properly operate on
formulas.

For a concrete example, I was trying to implement a walker to extract
all the atoms in the formula. I was trying to do something like this:

class GetAtomsWalker(pysmt.walkers.dag.DagWalker):
    def __init__(self):
        super(ImplicantWalker, self).__init__()
        for k in self.functions:
            self.functions[k] = self.walk_get_atom
        self.atoms = []

    def walk_get_atom(self, formula, **kwargs):
        if formula.is_quantifier():
            raise NotImplementedError("get_atoms for quantified formulae")

        if formula.symbol_type().is_bool_type():
            if not formula.is_boolean_operator():
                self.atoms.append(formula)

But this does not work, because formula.symbol_type() only works if
formula.is_symbol() is true, otherwise it fails (horribly :-)

Integrate get_logic in Factory

Factory should call get_logic if the logic of formula is not provided, in order to pick a solver for the given logic.

This is the last step for the deprecation of the "quantified" flag in Factory.

Create a table showing solver / capability relationship

We shall add this to the documentation and provide also info if the missing functionality is due to the solver or the wrapper.

Add pip install/pysmt-install target on CI

We need a target on the CI that runs the flow using pip install.

$ pip install pysmt
$ pysmt-install --EVERY-SOLVER

This would highlight issues like #52 and #48 .

Since building the solvers takes a lot of time, we should decouple this from the main testing flow.

MathSat 5.3.4 wrapper is not working

Mathsat 5.3.* introduces some optimization for SMT-LIB parsing, that tries to understand whether it is been run in an interactive mode. This might be breaking our wrapper, that is not able to provide this information.

See io.is_atty().

BitVector Support

Factorize code for solver selection

The method Factory.get_unsat_core_solver duplicates the logic for solver selection from get_solver. Since that is a quite complex flow, we might think about factoring it and dividing it into two parts.

The first part will be responsible for selecting the SolverClass according to the given options (logic, quantified, name etc.). The second part will be responsible for instantiating the solver with adequate options.

Create get_model shortcut

We should add a get_model shortcut that takes care of creating the solver, solving and returning a model (if one is found).
The signature would be similar to is_sat. It should return a Model (Eager or Lazy) or None if the formula is unsat.

Integrate MSatExistElim

Provide interface for msatexistelim

Implement FNode.__len__()

Sometimes we want to get an idea of how big a formula is. Currently, the hackish way I do this is:

  len(str(f))

that tells me the length of the string representation of f . This is not a good approach, since I need to build str(f) first and this could be expensive. We should implement the method FNode.len() to address this issue.

There are multiple metrics that one could consider, but I think the number of nodes of the underlying tree is a trivial one that makes sense.

Wrapper for Boolector

issues installing CVC4 on Mac OS X

I'm wondering if you guys have tried pysmt-install on Mac OS X. I tried installing CVC4, MathSAT, and ran into very obvious issues. Good news is I was able to fix most of these issues. Here's a list of issues/fixes for CVC4. I'll write later about MathSAT.

My environment:

• Mac OS X Yosemite 10.10.2
• Anaconda Python 2.7.9
• Homebrew to install non-python packages

pysmt-install --cvc4 first gave me obvious problems, because I didn't even have autoconf/automake etc.

To fix that I did:

brew install autoconf
brew install automake
brew install libtool
brew install boost
brew install swig
brew install gmp

I installed Java JRE, JDK from Oracle. That's needed for running antlr used by CVC4.

I got a warning about libtoolize & glibtoolize, so I followed the advice by doing:

ln -s /usr/local/bin/glibtoolize /usr/local/bin/libtoolize

GMP could not be found even if it was in /usr/local. So I did:

setenv LDFLAGS /usr/local/lib
setenv CPPFLAGS /usr/local/include

Suggestion: Add the above as manual setup instructions before trying to install CVC4.

---

pysmt-install --cvc4 then gave a error of cvc4_wrapper.patch not found. I just ignored the error, and continued. The rest of the text below is with that situation. Now after doing everything I realize that the patch fixes one of the swig problems (but doesn't seem to fix the problems I list below).

The reason why the patch isn't found is because the patch is missing in the pypi tarball or the installed files. I see it in the github tarball.

Suggestion: make sure to distribute the solver install patches!

---

pysmt-install --cvc4 then went through the steps of get-antlr, configure, make, and then I got a simple error:

mv: rename .libs/CVC4.so.3.0.0 to ./_CVC4.so: No such file or directory

That "mv" command is invoked by install.py, and in my build there was no .libs/CVC4.so.3.0.0, but I had .libs/CVC4.so symlinked to .libs/CVC4.3.so.

So I changed the "mv" command to ln -s .libs/CVC4.so _CVC4.so.

Then the install succeeded, but the resultant CVC4 module didn't work. When I did "import CVC4", I got a swig dlopen import error regarding libcvc4.3.dylib. So I found and symlinked that too.

But, all shared libraries of CVC4 have the install-prefix embedded in them. By default it is /usr/local. That is confirmed by running otool:

[prompt] otool -L builds/src/bindings/python/.libs/CVC4.so
builds/src/bindings/python/.libs/CVC4.so:
    /usr/local/lib/libcvc4.3.dylib (compatibility version 4.0.0, current version 4.0.0)
    /usr/local/lib/libcvc4parser.3.dylib (compatibility version 4.0.0, current version 4.0.0)
    /usr/local/lib/libgmp.10.dylib (compatibility version 13.0.0, current version 13.0.0)
    /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 120.0.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1213.0.0)  

[prompt] otool -L builds/lib/libcvc4.3.dylib
builds/lib/libcvc4.3.dylib:
    /usr/local/lib/libcvc4.3.dylib (compatibility version 4.0.0, current version 4.0.0)
    /usr/local/lib/libgmp.10.dylib (compatibility version 13.0.0, current version 13.0.0)
    /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 120.0.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1213.0.0)

So, even if the .so or .dylib are symlinked in the directory containing CVC4.py, there is still an import error.

Suggestion: please add --prefix when configuring CVC4, and do make; make install. That way, all libs are in the right place. You could have two folders source and install. The former is used to unzip and build the source code, while the latter is used as the install prefix. This way, it's easier to delete the full source/build folder tree, and have just the install folder.

---

After all of the above, I was able to get python -c 'import CVC4' to load all the libs correctly. But then I got an undefined symbol error:

Symbol not found: __ZN4CVC411ExprManager7mkConstINS_12TypeConstantEEENS_4ExprERKT_

Looks like CVC4's swig-generated python interface isn't really completely correct. I was able to fix the above error by commenting out a line in expr_manager.i. Then I got another such error regarding __ZNK4CVC44Expr8getConstINS_12TypeConstantEEERKT_v. So I commented out a line in expr.i.

After that, I was finally able to successfully execute import CVC4 in python. Using it via pysmt worked too!

Add support for returning UNSAT assumptions when Solving under assumptions

We should add this feature as it is part of the new SMT-Lib draft (http://smt-lib.org/papers/smt-lib-reference-v2.5-draft-2.pdf)

Possible race conditions in Continuous Integration

Recently, I noticed that shippable.com has some trouble with our tests.

In configurations where no solvers are available, the tests are failing because a SMT-Lib wrapper solver is not found. This seems to me a sort of race condition or a caching problem in our CI.

E.g. https://app.shippable.com/builds/5548786542da970c000f1c6f

FreeVariablesOracle extensions

A possible improvement to the FreeVariablesOracle could be to have a parameter to control if/how function symbols are added in the resulting cone.

I see three modes:

• Only Variables: meaning that only variables are considered in the cone
• Function Symbols [default and current behavior]: function names are symbols appearing in the cpone, but function applications are discarded
• Function applications: function applications are considered atomic and are retured together with the cones of their parameters.