Stack Overflow
Stack Overflow

Questions tagged [pysmt]

PySMT is a python API for interfacing with a variety of SMT solvers.

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...

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:

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.

pySMT works on both Python 3.5 and Python 2.7.

11 questions
3
votes
1 answer

How to use array in PySMT?

I have a problem with PySMT. I'm new in the field and I have no idea how to use arrays. I've understood that: 1) It's possible to declare an array as: a = Symbol("a", ArrayType(INT, INT)) 2) Then, to store values in the array: k = Store(a, Int(0),…
Nombre
  • 31
  • 1
3
votes
1 answer

Is there way to give input as normal expression to Z3 Solver?

The Z3 input format is an extension of the one defined by SMT-LIB 2.0 standard. The input expressions need to write in prefix form. As for example rise4fun, x + (y * 2) = 20 needs to be given input in the form of " (= (+ x (* 2 y)) 20)) ". Z3…
Rituraj Singh
  • 579
  • 1
  • 5
  • 16
3
votes
2 answers

Use different back-end solvers in Z3

I'm using Z3 Python interface to create formulas for my experiments. I'm then sending that formula to a Z3 solver. If I'm correct Z3 uses its own solver! How to use a different SAT/SMT solver with Z3py? The way I use to do it in CBMC (C bounded…
user2754673
  • 439
  • 3
  • 13
2
votes
2 answers

Using SMT-LIB to count the number of modules using a formula

I am not sure that this is possible using SMT-LIB, if it is not possible does an alternative solver exist that can do it? Consider the equations a < 10 and a > 5 b < 5 and b > 0 b < c < a with a, b and c integers The values for a and b where the…
Johan
  • 575
  • 5
  • 21
1
vote
1 answer

how to duplicate a solver created in pysmt?

in pysmt, assuming that i have created a solver and added many assertions. now, i want to make a copy of the solver instance because i need to add different assertions to the solver. how do i do so? i need to do so in order to improve the…
adrianX
  • 619
  • 7
  • 21
0
votes
1 answer

Representing an SMT formula

Making a Boolean formula in PySMT is simple: from pysmt.shortcuts import * from pysmt.typing import INT x1 = Symbol("x1") x2 = Symbol("x2") formula = Or(x1, x2) model = get_model(formula) print(model) Moreover, an SMT formula has this shape: x1 =…
foobar
  • 571
  • 1
  • 5
  • 20
0
votes
0 answers

arm-linux-gnueabi-g++: .so file not recognized

I would like to compile MathSat on an EV3 Mindstorm with ev3dev as OS. For this, I am using the installer given by PySMT (PySMT is successfully installed): pysmt-install --msat Additionally, I installed some necessary packages: sudo apt-get install…
Steve2Fish
  • 187
  • 4
  • 15
0
votes
1 answer

Print SMTLib constraints to stdout in PySMT

I have some problem encoded using PySMT APIs. PySMT's GitHub page shows an example about using any SMTLib compliant solver with PySMT. It says that PySMT will give the problem to solver in stdin. But I can't find any straightforward way of printing…
Samvid Mistry
  • 783
  • 1
  • 8
  • 14
0
votes
2 answers

pysmt z3 solver crashing?

I am having trouble with the pysmt solvers. I am getting the following error message: AttributeError: 'module' object has no attribute 'Z3_mk_and' whenever I try to both: (1) Instantiate a solver via Solver() and (2) Run pysmt-install --check Here…
HSC
  • 1
  • 1
0
votes
1 answer

How to activate partial mode in Z3py?

I am using Z3's Python bindings and am curious wether partial mode would speed up my model. However there doesn't seem to be a way to do this in Python. (set_param(...) doesn"t seem to have a parameter for it) I considered migrating to pySMT since…
TheHowlingHoaschd
  • 666
  • 7
  • 13
0
votes
1 answer

Which tool is the best to convert clauses in CNF (or even better DIMACS CNF)?

I am automatically generating clauses like this with a C++ program: ((((((condition1#0 and not action1#0 and not action2#0 and TRUE) and (action1#1 and not action2#1 and not condition1#1 and TRUE) and TRUE)) or (not action1#0 and not action2#0 and…
elena
  • 889
  • 2
  • 11
  • 19