Solvers & Results

Simple Solving

cvc5.pythonic.solve(*args, **kwargs)

Solve the constraints *args.

This is a simple function for creating demonstrations. It creates a solver, configure it using the options in kwargs, adds the constraints in args, and invokes check.

>>> a = Int('a')
>>> solve(a > 0, a < 2)
[a = 1]
>>> solve(a > 0, a < 2, show=True)
Problem:
[a > 0, a < 2]
Solution:
[a = 1]

cvc5.pythonic.solve_using(s, *args, **kwargs)

Solve the constraints *args using solver s.

This is a simple function for creating demonstrations. It is similar to solve, but it uses the given solver s. It configures solver s using the options in kwargs, adds the constraints in args, and invokes check.

>>> a = Int('a')
>>> s = Solver()
>>> solve_using(s, a > 0, a < 2)
[a = 1]
>>> solve_using(s, a != 1, show=True)
Problem:
[a > 0, a < 2, a != 1]
no solution

cvc5.pythonic.prove(claim, **keywords)

Try to prove the given claim.

This is a simple function for creating demonstrations. It tries to prove claim by showing the negation is unsatisfiable.

>>> p, q = Bools('p q')
>>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
proved
>>> prove(p == True)
counterexample
[p = False]
>>> prove(p == True, show=True)
[Not(p == True)]
counterexample
[p = False]

cvc5.pythonic.is_tautology(taut)

Return whether these constraints hold for all assignments.

Prints nothing.

>>> p, q = Bools('p q')
>>> is_tautology(Not(And(p, q)) == Or(Not(p), Not(q)))
True

The Solver Class

cvc5.pythonic.SolverFor(logic, ctx=None, logFile=None)

Create a solver customized for the given logic.

The parameter logic is a string. It should be the name of an SMT-LIB logic. See https://smtlib.cs.uiowa.edu/ for the name of all available logics.

cvc5.pythonic.SimpleSolver(ctx=None, logFile=None)

Return a simple general purpose solver.

>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat

class cvc5.pythonic.Solver(logic=None, ctx=None, logFile=None)

Solver API provides methods for implementing the main SMT 2.0 commands:

• push,

• pop,

• check,

• get-model,

• etc.

__iadd__(fml)

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s += x > 0
>>> s += x < 2
>>> s
[x > 0, x < 2]

__init__(logic=None, ctx=None, logFile=None)

__repr__()

Return a formatted string with all added constraints.

__weakref__

list of weak references to the object (if defined)

add(*args)

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s
[x > 0, x < 2]

append(*args)

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.append(x > 0, x < 2)
>>> s
[x > 0, x < 2]

assert_exprs(*args)

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.assert_exprs(x > 0, x < 2)
>>> s
[x > 0, x < 2]

assertions()

Return an AST vector containing all added constraints.

>>> s = Solver()
>>> s.assertions()
[]
>>> a = Int('a')
>>> s.add(a > 0)
>>> s.add(a < 10)
>>> s.assertions()
[a > 0, a < 10]

check(*assumptions)

Check whether the assertions in the given solver plus the optional assumptions are consistent or not.

>>> x = Int('x')
>>> s = Solver()
>>> s.check()
sat
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> s.model().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.resetAssertions()

getOption(name)

Get the current value of an option from the solver. The value is returned as a string. For type-safe querying use getOptionInfo().

>>> s = Solver()
>>> s.setOption(incremental=True)
>>> s.getOption("incremental")
'true'

getOptionInfo(name)

Get the current value of an option from the solver. The value is returned as a string. For type-safe querying use getOptionInfo().

>>> s = Solver()
>>> s.setOption(incremental=False)
>>> s.getOptionInfo("incremental")
{'name': 'incremental', 'aliases': [], 'setByUser': True, 'type': <class 'bool'>, 'current': False, 'default': True}

getOptionNames()

Get all option names that can be used with getOption(), setOption() and getOptionInfo().

>>> s = Solver()
>>> s.getOptionNames()[:2]
['abstract-values', 'ackermann']

initFromLogic()

Create the base-API solver from the logic

insert(*args)

Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.insert(x > 0, x < 2)
>>> s
[x > 0, x < 2]

model()

Return a model for the last check().

This function raises an exception if a model is not available (e.g., last check() returned unsat).

>>> s = Solver()
>>> a = Int('a')
>>> s.add(a + 2 == 0)
>>> s.check()
sat
>>> s.model()
[a = -2]

num_scopes()

Return the current number of backtracking points.

>>> s = Solver()
>>> s.num_scopes()
0
>>> s.push()
>>> s.num_scopes()
1
>>> s.push()
>>> s.num_scopes()
2
>>> s.pop()
>>> s.num_scopes()
1

pop(num=1)

Backtrack num backtracking points.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

proof()

Return a proof for the last check().

This function raises an exception if a proof is not available (e.g., last check() does not return unsat).

>>> s = Solver()
>>> s.set('produce-proofs','true')
>>> a = Int('a')
>>> s.add(a + 2 == 0)
>>> s.check()
sat
>>> try:
...   s.proof()
... except RuntimeError:
...   print("failed to get proof (last `check()` must have returned unsat)")
failed to get proof (last `check()` must have returned unsat)
>>> s.add(a == 0)
>>> s.check()
unsat
>>> s.proof()
(SCOPE: Not(And(a + 2 == 0, a == 0)),
 (SCOPE: Not(And(a + 2 == 0, a == 0)),
  [a + 2 == 0, a == 0],
  (EQ_RESOLVE: False,
   (ASSUME: a == 0, [a == 0]),
   (MACRO_SR_EQ_INTRO: (a == 0) == False,
    [a == 0, 7, 12],
    (EQ_RESOLVE: a == -2,
     (ASSUME: a + 2 == 0, [a + 2 == 0]),
     (MACRO_SR_EQ_INTRO: (a + 2 == 0) == (a == -2),
      [a + 2 == 0, 7, 12]))))))

push()

Create a backtracking point.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]

reason_unknown()

Return a string describing why the last check() returned unknown.

>>> x = Int('x')
>>> s = SimpleSolver()

reset()

Fully reset the solver. This actually destroys the solver object in the context and recreates this. This invalidates all objects created within this context and using them will most likely crash.

>>> s = Solver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
>>> s.reset()
>>> s.setOption(incremental=True)

resetAssertions()

Remove all asserted constraints and backtracking points created using push().

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.resetAssertions()
>>> s
[]

set(*args, **kwargs)

Set an option on the solver. Wraps setOption().

>>> s = Solver()
>>> s.set(incremental=True)
>>> s.set('incremental', 'true')

setOption(name=None, value=None, **kwargs)

Set options on the solver. Options can either be set via the name and value arguments in the form setOption('foo', 'bar'), or as keyword arguments using the syntax setOption(foo='bar'). The option value is passed as a string internally. Boolean values are properly converted manually, all other types are convertes using str().

>>> s = Solver()
>>> s.setOption('incremental', True)
>>> s.setOption(incremental='true')

sexpr()

Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> r = s.sexpr()

statistics()

Return the statistics of this solver.

>>> c = Context()
>>> s = Solver(ctx=c)
>>> a = Int('a', c)
>>> s.add(a == 0)
>>> s.check()
sat
>>> stats = s.statistics()
>>> stats['cvc5::CONSTANT']
{'default': True, 'internal': False, 'value': {}}
>>> len(stats.get()) < 10
True
>>> len(stats.get(True, True)) > 30
True

unsat_core()

Return a subset (as a list of Bool expressions) of the assertions and assumptions provided to the last check().

To enable this, set the option “produce-unsat-cores” to true.

>>> a,b,c = Bools('a b c')
>>> s = Solver()
>>> s.set('produce-unsat-cores','true')
>>> s.add(Or(a,b),Or(b,c),Not(c))
>>> s.check(a,b,c)
unsat
>>> core = s.unsat_core()
>>> a in core
False
>>> b in core
False
>>> c in core
True
>>> s.check(a,b)
sat

Results & Models

cvc5.pythonic.unsat

An UNSAT result.

cvc5.pythonic.sat

A SAT result.

cvc5.pythonic.unknown

The satisfiability could not be determined.

class cvc5.pythonic.CheckSatResult(r)

Represents the result of a satisfiability check: sat, unsat, unknown.

>>> s = Solver()
>>> s.check()
sat
>>> r = s.check()
>>> isinstance(r, CheckSatResult)
True

__eq__(other)

Return self==value.

__hash__ = None

__init__(r)

__ne__(other)

Return self!=value.

__repr__()

Return repr(self).

__weakref__

list of weak references to the object (if defined)

class cvc5.pythonic.ModelRef(solver)

Model/Solution of a satisfiability problem (aka system of constraints).

__getitem__(idx)

If idx is an integer, then the declaration at position idx in the model self is returned. If idx is a declaration, then the actual interpretation is returned.

The elements can be retrieved using position or the actual declaration.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2, f(x) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m.decls()
[f, x]
>>> len(m)
2
>>> m[0]
f
>>> m[1]
x
>>> m[x]
1

__init__(solver)

__len__()

Return the number of constant and function declarations in the model self.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, f(x) != x)
>>> s.check()
sat
>>> m = s.model()
>>> len(m)
2

__repr__()

Return repr(self).

__weakref__

list of weak references to the object (if defined)

decls()

Return a list with all symbols that have an interpretation in the model self.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2, f(x) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m.decls()
[f, x]

eval(t, model_completion=False)

Evaluate the expression t in the model self. If model_completion is enabled, then a default interpretation is automatically added for symbols that do not have an interpretation in the model self.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> m = s.model()
>>> m.eval(x + 1)
2
>>> m.eval(x == 1)
True

evaluate(t, model_completion=False)

Alias for eval.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> m = s.model()
>>> m.evaluate(x + 1)
2
>>> m.evaluate(x == 1)
True

vars()

Returns the free constants in an assertion, as terms

Utilities

cvc5.pythonic.evaluate(t)

Evaluates the given term (assuming it is constant!)

cvc5.pythonic.simplify(a)

Simplify the expression a.

>>> x = Int('x')
>>> y = Int('y')
>>> simplify(x + 1 + y + x + 1)
2 + 2*x + y

cvc5.pythonic.substitute(t, *m)

Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to.

>>> x = Int('x')
>>> y = Int('y')
>>> f = Function('f', IntSort(), IntSort())
>>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
1 + 1

cvc5.pythonic.Sum(*args)

Create the sum of the SMT expressions.

>>> a, b, c = Ints('a b c')
>>> Sum(a, b, c)
a + b + c
>>> Sum([a, b, c])
a + b + c
>>> A = IntVector('a', 5)
>>> Sum(A)
a__0 + a__1 + a__2 + a__3 + a__4
>>> Sum()
0

cvc5.pythonic.Product(*args)

Create the product of the SMT expressions.

>>> a, b, c = Ints('a b c')
>>> Product(a, b, c)
a*b*c
>>> Product([a, b, c])
a*b*c
>>> A = IntVector('a', 5)
>>> Product(A)
a__0*a__1*a__2*a__3*a__4
>>> Product()
1