# Tutorials¶

This page is under-construction. For now, it contains a copy of the files within the examples/ folder of the pySMT repository and a basic tutorial on Boolean logic.

If you are interested in helping us create better tutorials, please let us know at info@pysmt.org .

## Boolean Logic in PySMT¶

An introductory basic example on how to use pySMT for Booean satisfiability: Boolean Logic with PySMT.

## First example¶

# Checking satisfiability of a formula.
#
# This example shows:
#  1. How to build a formula
#  2. How to perform substitution
#  3. Printing
#  4. Satisfiability checking
from pysmt.shortcuts import Symbol, And, Not, is_sat

varA = Symbol("A") # Default type is Boolean
varB = Symbol("B")
f = And([varA, Not(varB)])
g = f.substitute({varB:varA})

res = is_sat(f)
assert res # SAT
print("f := %s is SAT? %s" % (f, res))

res = is_sat(g)
print("g := %s is SAT? %s" % (g, res))
assert not res # UNSAT


## Hello World word puzzle¶

# This is the tutorial example of pySMT.
#
# This example shows how to:
# 1. Deal with Theory atoms
# 2. Specify a solver in the shortcuts (get_model, is_sat etc.)
# 3. Obtain an print a model
#
#
# The goal of the puzzle is to assign a value from 1 to 10 to each letter s.t.
#    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")


## Hello World word puzzle using infix-notation¶

# This is a different take on the puzzle.py example
#
# This examples shows how to:
# 1. Enable and use infix notation
# 2. Use a solver context
#
from pysmt.shortcuts import Symbol, And, Plus, Int
from pysmt.shortcuts import Solver
from pysmt.typing import INT

# Infix-Notation is automatically enabled whenever you import pysmt.shortcuts.
#
# To enable it without using shortcuts, do:
#
#   from pysmt.environment import get_env
#   get_env().enable_infix_notation = True
#
# Similarly, you can disable infix_notation to prevent its accidental use.
#

hello = [Symbol(s, INT) for s in "hello"]
world = [Symbol(s, INT) for s in "world"]
letters = set(hello+world)

# operator. For boolean connectors, we use e.g., x.And(y) This
# increases readability without running into problems of operator
# precedence.
#
# Note how you can mix prefix and infix notation.
domains = And([(Int(1) <= l).And(Int(10) >= l) for l in letters])

sum_hello = Plus(hello) # n-ary operators can take lists
sum_world = Plus(world) # as arguments
problem = (sum_hello.Equals(sum_world)).And(sum_hello.Equals(Int(25)))
formula = domains.And(problem)

print("Serialization of the formula:")
print(formula)

# A context (with-statment) lets python take care of creating and
# destroying the solver.
with Solver() as solver:
if solver.solve():
for l in letters:
print("%s = %s" %(l, solver.get_value(l)))
else:
print("No solution found")


## Combine multiple solvers¶

# This example requires Z3 and MathSAT to be installed (but you can
#  replace MathSAT with any other solver for QF_LRA)
#
# This examples shows how to:
# 1. Define Real valued constants using floats and fractions
# 2. Perform quantifier elimination
# 3. Pass results from one solver to another
#
from pysmt.shortcuts import Symbol, Or, ForAll, GE, LT, Real, Plus
from pysmt.shortcuts import qelim, is_sat
from pysmt.typing import REAL

x, y, z = [Symbol(s, REAL) for s in "xyz"]

f = ForAll([x], Or(LT(x, Real(5.0)),
GE(Plus(x, y, z), Real((17,2))))) # (17,2) ~> 17/2
print("f := %s" % f)
#f := (forall x . ((x < 5.0) | (17/2 <= (x + y + z))))

qf_f = qelim(f, solver_name="z3")
print("Quantifier-Free equivalent: %s" % qf_f)
#Quantifier-Free equivalent: (7/2 <= (z + y))

res = is_sat(qf_f, solver_name="msat")
print("SAT check using MathSAT: %s" % res)
#SAT check using MathSAT: True


## Model-Checking an infinite state system (BMC+K-Induction) in ~150 lines¶

# This example shows a more advance use of pySMT.
#
# It provides a simple implementation of Bounded Model Checking 
# with K-Induction , and PDR [3,4], and applies it on a simple
# transition system.
#
#  Biere, Cimatti, Clarke, Zhu,
#     "Symbolic Model Checking without BDDs",
#     TACAS 1999
#
#  Sheeran, Singh,  Stalmarck,
#     "Checking  safety  properties  using  induction  and  a SAT-solver",
#
#     "SAT-Based Model Checking without Unrolling",
#     VMCAI 2011
#
#  Een, Mischenko, Brayton
#     "Efficient implementation of property directed reachability",
#
from six.moves import xrange

from pysmt.shortcuts import Symbol, Not, And, Or, EqualsOrIff, Implies
from pysmt.shortcuts import is_sat, is_unsat, Solver, TRUE
from pysmt.typing import BOOL

def next_var(v):
"""Returns the 'next' of the given variable"""
return Symbol("next(%s)" % v.symbol_name(), v.symbol_type())

def at_time(v, t):
"""Builds an SMT variable representing v at time t"""
return Symbol("%s@%d" % (v.symbol_name(), t), v.symbol_type())

class TransitionSystem(object):
"""Trivial representation of a Transition System."""

def __init__(self, variables, init, trans):
self.variables = variables
self.init = init
self.trans = trans

# EOC TransitionSystem

class PDR(object):
def __init__(self, system):
self.system = system
self.frames = [system.init]
self.solver = Solver()
self.prime_map = dict([(v, next_var(v)) for v in self.system.variables])

def check_property(self, prop):
"""Property Directed Reachability approach without optimizations."""
print("Checking property %s..." % prop)

while True:
if cube is not None:
# Blocking phase of a bad state
if self.recursive_block(cube):
print("--> Bug found at step %d" % (len(self.frames)))
break
else:
print("   [PDR] Cube blocked '%s'" % str(cube))
else:
# Checking if the last two frames are equivalent i.e., are inductive
if self.inductive():
print("--> The system is safe!")
break
else:
print("   [PDR] Adding frame %d..." % (len(self.frames)))
self.frames.append(TRUE())

"""Extracts a reachable state that intersects the negation
of the property and the last current frame"""
return self.solve(And(self.frames[-1], Not(prop)))

def solve(self, formula):
"""Provides a satisfiable assignment to the state variables that are consistent with the input formula"""
if self.solver.solve([formula]):
return And([EqualsOrIff(v, self.solver.get_value(v)) for v in self.system.variables])
return None

def recursive_block(self, cube):
"""Blocks the cube at each frame, if possible.

Returns True if the cube cannot be blocked.
"""
for i in range(len(self.frames)-1, 0, -1):
cubeprime = cube.substitute(dict([(v, next_var(v)) for v in self.system.variables]))
cubepre = self.solve(And(self.frames[i-1], self.system.trans, Not(cube), cubeprime))
if cubepre is None:
for j in range(1, i+1):
self.frames[j] = And(self.frames[j], Not(cube))
return False
cube = cubepre
return True

def inductive(self):
"""Checks if last two frames are equivalent """
if len(self.frames) > 1 and \
self.solve(Not(EqualsOrIff(self.frames[-1], self.frames[-2]))) is None:
return True
return False

class BMCInduction(object):

def __init__(self, system):
self.system = system

def get_subs(self, i):
"""Builds a map from x to x@i and from x' to x@(i+1), for all x in system."""
subs_i = {}
for v in self.system.variables:
subs_i[v] = at_time(v, i)
subs_i[next_var(v)] = at_time(v, i+1)
return subs_i

def get_unrolling(self, k):
"""Unrolling of the transition relation from 0 to k:

E.g. T(0,1) & T(1,2) & ... & T(k-1,k)
"""
res = []
for i in xrange(k+1):
subs_i = self.get_subs(i)
res.append(self.system.trans.substitute(subs_i))
return And(res)

def get_simple_path(self, k):
"""Simple path constraint for k-induction:
each time encodes a different state
"""
res = []
for i in xrange(k+1):
subs_i = self.get_subs(i)
for j in xrange(i+1, k+1):
state = []
subs_j = self.get_subs(j)
for v in self.system.variables:
v_i = v.substitute(subs_i)
v_j = v.substitute(subs_j)
state.append(Not(EqualsOrIff(v_i, v_j)))
res.append(Or(state))
return And(res)

def get_k_hypothesis(self, prop, k):
"""Hypothesis for k-induction: each state up to k-1 fulfills the property"""
res = []
for i in xrange(k):
subs_i = self.get_subs(i)
res.append(prop.substitute(subs_i))
return And(res)

def get_bmc(self, prop, k):
"""Returns the BMC encoding at step k"""
init_0 = self.system.init.substitute(self.get_subs(0))
prop_k = prop.substitute(self.get_subs(k))
return And(self.get_unrolling(k), init_0, Not(prop_k))

def get_k_induction(self, prop, k):
"""Returns the K-Induction encoding at step K"""
subs_k = self.get_subs(k)
prop_k = prop.substitute(subs_k)
return And(self.get_unrolling(k),
self.get_k_hypothesis(prop, k),
self.get_simple_path(k),
Not(prop_k))

def check_property(self, prop):
"""Interleaves BMC and K-Ind to verify the property."""
print("Checking property %s..." % prop)
for b in xrange(100):
f = self.get_bmc(prop, b)
print("   [BMC]    Checking bound %d..." % (b+1))
if is_sat(f):
print("--> Bug found at step %d" % (b+1))
return

f = self.get_k_induction(prop, b)
print("   [K-IND]  Checking bound %d..." % (b+1))
if is_unsat(f):
print("--> The system is safe!")
return

def counter(bit_count):
"""Counter example with n bits and reset signal."""

# Example Counter System (SMV-like syntax)
#
# VAR bits: word[bit_count];
#     reset: boolean;
#
# INIT: bits = 0 & reset = FALSE;
#
# TRANS: next(bits) = bits + 1
# TRANS: next(bits = 0) <-> next(reset)

from pysmt.typing import BVType
bits = Symbol("bits", BVType(bit_count))
nbits = next_var(bits)
reset = Symbol("r", BOOL)
nreset = next_var(reset)
variables = [bits, reset]

init = bits.Equals(0) & Not(reset)

trans = nbits.Equals(bits + 1) &\
(nbits.Equals(0)).Iff(nreset)

# A true invariant property: (reset -> bits = 0)
true_prop = reset.Implies(bits.Equals(0))

# A false invariant property: (bits != 2**bit_count-1)
false_prop = bits.NotEquals(2**bit_count -1)

return (TransitionSystem(variables, init, trans), [true_prop, false_prop])

def main():
example = counter(4)

bmcind = BMCInduction(example)
pdr = PDR(example)

for prop in example:
bmcind.check_property(prop)
pdr.check_property(prop)
print("")

if __name__ == "__main__":
main()


## How to access functionalities of solvers not currently wrapped by pySMT¶

# This example requires MathSAT to be installed.
#
# This example shows how to use a solver converter to access
# functionalities of the solver that are not wrapped by pySMT.
#
# Our goal is to call the method msat_all_sat from the MathSAT API.
#
import mathsat
from pysmt.shortcuts import Or, Symbol, Solver, And

def callback(model, converter, result):
"""Callback for msat_all_sat.

This function is called by the MathSAT API everytime a new model
is found. If the function returns 1, the search continues,
otherwise it stops.
"""
# Elements in model are msat_term .
# Converter.back() provides the pySMT representation of a solver term.
py_model = [converter.back(v) for v in model]
result.append(And(py_model))
return 1 # go on

x, y = Symbol("x"), Symbol("y")
f = Or(x, y)

msat = Solver(name="msat")
converter = msat.converter # .converter is a property implemented by all solvers
msat.add_assertion(f) # This is still at pySMT level

result = []
# Directly invoke the mathsat API !!!
# The second term is a list of "important variables"
mathsat.msat_all_sat(msat.msat_env(),
[converter.convert(x)],      # Convert the pySMT term into a MathSAT term
lambda model : callback(model, converter, result))

print("'exists y . %s' is equivalent to '%s'" %(f, Or(result)))
#exists y . (x | y) is equivalent to ((! x) | x)


## How to use any SMT-LIB complaint SMT solver¶

# This example shows how to define a generic SMT-LIB solver, and use
# it within pySMT. The example looks for mathsat in /tmp, you can
#
# Using this process you can experiment with any SMT-LIB 2 compliant
# solver even if it does not have python bindings, or has not been
# integrated with pySMT.
#
# Note: When using the SMT-LIB wrapper, you can only use logics
# supported by pySMT. If the version of pySMT in use does not support
# Arrays, then you cannot represent arrays.
#

# To define a Generic Solver you need to provide:
#
# - A name to associate to the solver
# - The path to the script + Optional arguments
# - The list of logics supported by the solver
#
# It is usually convenient to wrap the solver in a simple shell script.
# See examples for Z3, Mathsat and Yices in pysmt/test/smtlib/bin/*.template
#
from pysmt.logics import QF_UFLRA, QF_UFIDL, QF_LRA, QF_IDL, QF_LIA
from pysmt.shortcuts import get_env, GT, Solver, Symbol
from pysmt.typing import REAL, INT
from pysmt.exceptions import NoSolverAvailableError

name = "mathsat" # Note: The API version is called 'msat'
path = ["/tmp/mathsat"] # Path to the solver
logics = [QF_UFLRA, QF_UFIDL] # Some of the supported logics

env = get_env()

# Add the solver to the environment

r, s = Symbol("r", REAL), Symbol("s", REAL)
p, q = Symbol("p", INT), Symbol("q", INT)

f_lra = GT(r, s)
f_idl = GT(p, q)

# PySMT takes care of recognizing that QF_LRA can be solved by a QF_UFLRA solver.
with Solver(name=name, logic=QF_LRA) as s:
res = s.solve()
assert res, "Was expecting '%s' to be SAT" % f_lra

with Solver(name=name, logic=QF_IDL) as s:
res = s.solve()
assert res, "Was expecting '%s' to be SAT" % f_idl

try:
with Solver(name=name, logic=QF_LIA) as s:
pass
except NoSolverAvailableError:
# If we ask for a logic that is not contained by any of the
# supported logics an exception is thrown
print("%s does not support QF_LIA" % name)


## How to combine two different solvers to solve an Exists Forall problem¶

# EF-SMT solver implementation
#
# This example shows:
#  1. How to combine 2 different solvers
#  2. How to extract information from a model
#
from pysmt.shortcuts import Solver, get_model
from pysmt.shortcuts import Symbol, Bool, Real, Implies, And, Not, Equals
from pysmt.shortcuts import GT, LT, LE, Minus, Times
from pysmt.logics import AUTO, QF_LRA
from pysmt.typing import REAL
from pysmt.exceptions import SolverReturnedUnknownResultError

def efsmt(y, phi, logic=AUTO, maxloops=None,
esolver_name=None, fsolver_name=None,
verbose=False):
"""Solves exists x. forall y. phi(x, y)"""

y = set(y)
x = phi.get_free_variables() - y

with Solver(logic=logic, name=esolver_name) as esolver:

loops = 0
while maxloops is None or loops <= maxloops:
loops += 1

eres = esolver.solve()
if not eres:
return False
else:
tau = {v: esolver.get_value(v) for v in x}
sub_phi = phi.substitute(tau).simplify()
if verbose: print("%d: Tau = %s" % (loops, tau))

fmodel = get_model(Not(sub_phi),
logic=logic, solver_name=fsolver_name)
if fmodel is None:
return tau
else:
sigma = {v: fmodel[v] for v in y}
sub_phi = phi.substitute(sigma).simplify()
if verbose: print("%d: Sigma = %s" % (loops, sigma))

raise SolverReturnedUnknownResultError

def run_test(y, f):
print("Testing " + str(f))
try:
res = efsmt(y, f, logic=QF_LRA, maxloops=20, verbose=True)
if res == False:
print("unsat")
else:
print("sat : %s" % str(res))
except SolverReturnedUnknownResultError:
print("unknown")
print("\n\n")

def main():
x,y = [Symbol(n, REAL) for n in "xy"]
f_sat = Implies(And(GT(y, Real(0)), LT(y, Real(10))),
LT(Minus(y, Times(x, Real(2))), Real(7)))

f_incomplete = And(GT(x, Real(0)), LE(x, Real(10)),
Implies(And(GT(y, Real(0)), LE(y, Real(10)),
Not(Equals(x, y))),
GT(y, x)))

run_test([y], f_sat)
run_test([y], f_incomplete)

if __name__ == "__main__":
main()


## How to detect the logic of a formula and perform model enumeration¶

# Perform ALL-SMT on Theory atoms
#
# This example shows:
#  - How to get the logic of a formula
#  - How to enumerate models
#  - How to extract a partial model
#  - How to use the special operator EqualsOrIff
#
from pysmt.shortcuts import Solver, Not, And, Symbol, Or
from pysmt.shortcuts import LE, GE, Int, Plus, Equals, EqualsOrIff
from pysmt.typing import INT
from pysmt.oracles import get_logic

def all_smt(formula, keys):
target_logic = get_logic(formula)
print("Target Logic: %s" % target_logic)
with Solver(logic=target_logic) as solver:
while solver.solve():
partial_model = [EqualsOrIff(k, solver.get_value(k)) for k in keys]
print(partial_model)

A0 = Symbol("A0", INT)
A1 = Symbol("A1", INT)
A2 = Symbol("A2", INT)

f = And(GE(A0, Int(0)), LE(A0, Int(5)),
GE(A1, Int(0)), LE(A1, Int(5)),
GE(A2, Int(0)), LE(A2, Int(5)),
Equals(Plus(A0, A1, A2), Int(8)))

all_smt(f, [A0, A1, A2])

# By using the operator EqualsOrIff, we can mix theory and bool variables
x = Symbol("x")
y = Symbol("y")
f = And(f, Or(x,y))

all_smt(f, [A0, A1, A2, x])


## Shows how to use multi-processing to perform parallel and asynchronous solving¶

# This example requires Z3
#
# This example shows how to parallelize solving using pySMT, by using
# the multiprocessing library.
#
# All shortcuts (is_sat, is_unsat, get_model, etc.) can be easily
# used. We sho two techniques: map and apply_async.
#
# Map applies a given function to a list of elements, and returns a
# list of results. We show an example using is_sat.
#
# Apply_async provides a way to perform operations in an asynchronous
# way. This allows us to start multiple solving processes in parallel,
# and collect the results whenever they become available.
#
# documentation for the multiprocessing module.
#
#
# NOTE: When running this example, a warning will appear saying:
#   "Contextualizing formula during is_sat"
#
# Each process will inherit a different formula manager, but the
# formulas that we are solving have been all created in the same
# formula manager. pySMT takes care of moving the formula across
# formula managers. This step is called contextualization, and occurs
# only when using multiprocessing.
# To disable the warning see the python module warnings.
#
from multiprocessing import Pool, TimeoutError
from time import sleep

from pysmt.test.examples import get_example_formulae
from pysmt.shortcuts import is_sat, is_valid, is_unsat
from pysmt.shortcuts import And

# Ignore this for now
def check_validity_and_test(args):
"""Checks expression and compare the outcome against a known value."""

expr, expected = args # IMPORTANT: Unpack args !!!
local_res = is_valid(expr)
return local_res == expected

# Create the Pool with 4 workers.
pool = Pool(4)

# We use the examples formula from the test suite.
# This generator iterates over all the expressions
f_gen = (f.expr for f in get_example_formulae())

# Call the functino is_sat on each expression
res = pool.map(is_sat, f_gen)

# The result is a list of True/False, in the same order as the input.
print(res)

sleep(1) # Have some time to look at the result

# Notice that all shortcuts (is_sat, qelim, etc) require only one
# mandatory argument. To pass multiple arguments, we need to pack them
# together.

# Lets create a list of (formula, result), where result is the
# expected result of the is_valid query.
f_gen = (f.expr for f in get_example_formulae())
res_gen = (f.is_valid for f in get_example_formulae())
args_gen = zip(f_gen, res_gen)

# We now define a function that check the formula against the expected
# value of is_valid: See check_validity_and_test(...) above.
# Due to the way multiprocessing works, we need to define the function
# _before_ we create the Pool.

# As before, we call the map on the pool
res = pool.map(check_validity_and_test, args_gen)

# We can also apply a map-reduce strategy, by making sure that all
# results are as expected.
if all(res):
print("Everything is ok!")
else:
print("Ooops, something is wrong!")
print(res)

# A different option is to run solvers in an asynchronous way.  This
# does not provide us with any guarantee on the execution order, but
# it is particular convenient, if we want to perform solving together
# with another long operation (e.g., I/O, network etc.)  or if we want
# to run multiple solvers.

# Create a formula
big_f = And(f.expr for f in get_example_formulae() \
if not f.logic.theory.bit_vectors and \
not f.logic.theory.arrays and \
not f.logic.theory.strings and \
f.logic.theory.linear)

# Create keyword arguments for the function call.
# This is the simplest way to pass multiple arguments to apply_async.
kwargs = {"formula": big_f, "solver_name": "z3"}
future_res_sat = pool.apply_async(is_sat, kwds=kwargs)
future_res_unsat = pool.apply_async(is_unsat, kwds=kwargs)

# In the background, the solving is taking place... We can do other
# stuff in the meanwhile.
print("This is non-blocking...")

# Get the result with a deadline.
# See multiprocessing.pool.AsyncResult for more options
sat_res = future_res_sat.get(10)  # Get result after 10 seconds or kill
try:
unsat_res = future_res_unsat.get(0) # No wait
except TimeoutError:
unsat_res = None
print(sat_res, unsat_res)


## Demonstrates how to perform SMT-LIB parsing, dumping and extension¶

# The last part of the example requires a QF_LIA solver to be installed.
#
#
# This example shows how to interact with files in the SMT-LIB
# format. In particular:
#
# 1. How to read a file in SMT-LIB format
# 2. How to write a file in SMT-LIB format
# 3. Formulas and SMT-LIB script
# 4. How to access annotations from SMT-LIB files
# 5. How to extend the parser with custom commands
#
from six.moves import cStringIO # Py2-Py3 Compatibility

from pysmt.smtlib.parser import SmtLibParser

# To make the example self contained, we store the example SMT-LIB
# script in a string.
DEMO_SMTLIB=\
"""
(set-logic QF_LIA)
(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun x () Bool)
(declare-fun y () Bool)
(define-fun .def_1 () Bool (! (and x y) :cost 1))
(assert (=> x (> p q)))
(check-sat)
(push)
(assert (=> y (> q p)))
(check-sat)
(assert .def_1)
(check-sat)
(pop)
(check-sat)
"""

# We read the SMT-LIB Script by creating a Parser.
# From here we can get the SMT-LIB script.
parser = SmtLibParser()

# The method SmtLibParser.get_script takes a buffer in input. We use
# cStringIO to simulate an open file.
# See SmtLibParser.get_script_fname() if to pass the path of a file.
script = parser.get_script(cStringIO(DEMO_SMTLIB))

# The SmtLibScript provides an iterable representation of the commands
# that are present in the SMT-LIB file.
#
# Printing a summary of the issued commands
for cmd in script:
print(cmd.name)
print("*"*50)

# SmtLibScript provides some utilities to perform common operations: e.g,
#
# - Checking if a command is present
assert script.contains_command("check-sat")
# - Counting the occurrences of a command
assert script.count_command_occurrences("assert") == 3
# - Obtain all commands of a particular type
decls = script.filter_by_command_name("declare-fun")
for d in decls:
print(d)
print("*"*50)

# Most SMT-LIB scripts define a single SAT call. In these cases, the
# result can be obtained by conjoining multiple assertions.  The
# method to do that is SmtLibScript.get_strict_formula() that, raises
# an exception if there are push/pop calls.  To obtain the formula at
# the end of the execution of the Script (accounting for push/pop) we
# use get_last_formula
#
f = script.get_last_formula()
print(f)

# Finally, we serialize the script back into SMT-Lib format.  This can
# be dumped into a file (see SmtLibScript.to_file).  The flag daggify,
# specifies whether the printing is done as a DAG or as a tree.

buf_out = cStringIO()
script.serialize(buf_out, daggify=True)
print(buf_out.getvalue())

print("*"*50)
# Expressions can be annotated in order to provide additional
# information. The semantic of annotations is solver/problem
# dependent. For example, VMT uses annotations to identify two
# expressions as 1) the Transition Relation and 2) Initial Condition
#
# Here we pretend that we make up a ficticious Weighted SMT format
# and label .def1 with cost 1
#
# The class pysmt.smtlib.annotations.Annotations deals with the
# handling of annotations.
#
ann = script.annotations
print(ann.all_annotated_formulae("cost"))

print("*"*50)

# Annotations are part of the SMT-LIB standard, and are the
# recommended way to perform inter-operable operations. However, in
# many cases, we are interested in prototyping some algorithm/idea and
# need to write the input files by hand. In those cases, using an
# extended version of SMT-LIB usually provides a more readable input.
# We provide now an example on how to define a symbolic transition
# system as an extension of SMT-LIB.
# (A more complete version of this example can be found in :
#    pysmt.tests.smtlib.test_parser_extensibility.py)
#
EXT_SMTLIB="""\
(declare-fun A () Bool)
(declare-fun B () Bool)
(init (and A B))
(trans (=> A (next A)))
(exit)
"""

# We define two new commands (init, trans) and a new
# operator (next). In order to parse this file, we need to create a
# sub-class of the SmtLibParser, and add handlers for he new commands
# and operators.
from pysmt.smtlib.script import SmtLibCommand

class TSSmtLibParser(SmtLibParser):
def __init__(self, env=None, interactive=False):
SmtLibParser.__init__(self, env, interactive)

#
# The mapping function takes care of consuming the command
# name from the input stream, e.g., '(init' . Therefore,
# _cmd_init will receive the rest of the stream, in our
# example, '(and A B)) ...'
self.commands["init"] = self._cmd_init
self.commands["trans"] = self._cmd_trans

# Remove unused commands
#
# If some commands are not compatible with the extension, they
# can be removed from the parser. If found, they will cause
# the raising of the exception UnknownSmtLibCommandError
del self.commands["check-sat"]
del self.commands["get-value"]
# ...

#
# New operators can be added similarly as done for commands.
# e.g., 'next'. The helper function _operator_adapter,
# simplifies the writing of such extensions.  In this example,
# we will rewrite the content of the next without the need of
# introducing a new pySMT operator. If you are interested in a
# simple way of handling new operators in pySMT see
# pysmt.test.test_dwf.

def _cmd_init(self, current, tokens):
# This cmd performs the parsing of:
#   <expr> )
# and returns a new SmtLibCommand
expr = self.get_expression(tokens)
self.consume_closing(tokens, current)
return SmtLibCommand(name="init", args=(expr,))

def _cmd_trans(self, current, tokens):
# This performs the same parsing as _cmd_init, but returns a
# different object. The parser is not restricted to return
# SmtLibCommand, but using them makes handling them
# afterwards easier.
expr = self.get_expression(tokens)
self.consume_closing(tokens, current)
return SmtLibCommand(name="trans", args=(expr,))

def _next_var(self, symbol):
# The function is called with the arguments obtained from
# parsing the rest of the SMT-LIB file. In this case, 'next'
# is a unary function, thus we have only 1 argument. 'symbol'
# is an FNode. We require that 'symbol' is _really_ a symbol:
if symbol.is_symbol():
name = symbol.symbol_name()
ty = symbol.symbol_type()
# The return type MUST be an FNode, because this is part
# of an expression.
return self.env.formula_manager.Symbol("next_" + name, ty)
else:
raise ValueError("'next' operator can be applied only to symbols")

def get_ts(self, script):
# New Top-Level command that takes a script stream in input.
# We return a pair (Init, Trans) that defines the symbolic
# transition system.
init = self.env.formula_manager.TRUE()
trans = self.env.formula_manager.TRUE()

for cmd in self.get_command_generator(script):
if cmd.name=="init":
init = cmd.args
elif cmd.name=="trans":
trans = cmd.args
else:
# Ignore other commands
pass

return (init, trans)

# Time to try out the parser !!!
#
# First we check that the standard SMT-Lib parser cannot handle the new format.
from pysmt.exceptions import UnknownSmtLibCommandError

try:
parser.get_script(cStringIO(EXT_SMTLIB))
except UnknownSmtLibCommandError as ex:
print("Unsupported command: %s" % ex)

# The new parser can parse our example, and returns the (init, trans) pair
ts_parser = TSSmtLibParser()
init, trans = ts_parser.get_ts(cStringIO(EXT_SMTLIB))
print("INIT: %s" % init.serialize())
print("TRANS: %s" % trans.serialize())


## Shows the use of UNSAT Core as debugging tools¶

#
# This example requires MathSAT or Z3
#
# In this example, we will encode a more complex puzzle and see:
#
# - Use of UNSAT cores as a debugging tool
# - Conjunctive partitioning
# - Symbol handling delegation to auxiliary functions
#

# This puzzle is known as Einstein Puzzle
#
# There are five houses in five different colours in a row. In each
# house lives a person with a different nationality. The five owners
# drink a certain type of beverage, smoke a certain brand of cigar and
# keep a certain pet.
#
# No owners have the same pet, smoke the same brand of cigar, or drink
# the same beverage.
#
# The Brit lives in the red house.
# The Swede keeps dogs as pets.
# The Dane drinks tea.
# The green house is on the immediate left of the white house.
# The green house owner drinks coffee.
# The owner who smokes Pall Mall rears birds.
# The owner of the yellow house smokes Dunhill.
# The owner living in the center house drinks milk.
# The Norwegian lives in the first house.
# The owner who smokes Blends lives next to the one who keeps cats.
# The owner who keeps the horse lives next to the one who smokes Dunhill.
# The owner who smokes Bluemasters drinks beer.
# The German smokes Prince.
# The Norwegian lives next to the blue house.
# The owner who smokes Blends lives next to the one who drinks water.
#
# The question is: who owns the fish?

from pysmt.shortcuts import (Symbol, ExactlyOne, Or, And, FALSE, TRUE,
Iff, Implies)
from pysmt.shortcuts import get_model, get_unsat_core, is_sat, is_unsat

#
# Lets start by expliciting all values for all dimensions

Color = "white", "yellow", "blue", "red", "green"
Nat = "german", "swedish", "british", "norwegian", "danish"
Pet =  "birds", "cats", "horses", "fish", "dogs"
Drink = "beer", "water", "tea", "milk", "coffee"
Smoke = "blends", "pall_mall", "prince", "bluemasters", "dunhill"
Houses = range(0,5)
#
# We number the houses from 0 to 4, and create the macros to assert
# properties of the i-th house:
#
#  e.g., color(1, "green")  to indicate that the house 1 is Green
#
# This is not strictly necessary, but it is a way of making programs
#
def color(number, name):
assert name in Color
if number in Houses:
return Symbol("%d_color_%s" % (number, name))
return FALSE()

def nat(number, name):
assert name in Nat
if number in Houses:
return Symbol("%d_nat_%s" % (number, name))
return FALSE()

def pet(number, name):
assert name in Pet
if number in Houses:
return Symbol("%d_pet_%s" % (number, name))
return FALSE()

def drink(number, name):
assert name in Drink
if number in Houses:
return Symbol("%d_drink_%s" % (number, name))
return FALSE()

def smoke(number, name):
assert name in Smoke
if number in Houses:
return Symbol("%d_smoke_%s" % (number, name))
return FALSE()

#
# We can encode the facts
#

facts = TRUE()
for i in Houses:
facts = (facts &
# The Brit lives in the red house.
nat(i, "british").Iff(color(i, "red")) &

# The Swede keeps dogs as pets.
nat(i, "swedish").Iff(pet(i, "dogs")) &

# The Dane drinks tea.
nat(i, "danish").Iff(drink(i, "tea")) &

# The green house is on the immediate left of the white house.
color(i, "green").Iff(color(i+1, "white")) &

# The green house owner drinks coffee.
color(i, "green").Iff(drink(i, "coffee")) &

# The owner who smokes Pall Mall rears birds.
smoke(i, "pall_mall").Iff(pet(i, "birds")) &

# The owner of the yellow house smokes Dunhill.
color(i, "yellow").Iff(smoke(i, "dunhill")) &

# The owner who smokes Bluemasters drinks beer.
smoke(i, "bluemasters").Iff(drink(i, "beer")) &

# The German smokes Prince.
nat(i, "german").Iff(smoke(i, "prince")) &

# The owner who smokes Blends lives next to the one who keeps cats.
smoke(i, "blends").Implies(pet(i-1, "cats") | pet(i+1, "cats")) &

# The owner who keeps the horse lives next to the one who smokes Dunhill.
pet(i, "horses").Implies(smoke(i-1, "dunhill") | smoke(i+1, "dunhill")) &

# The Norwegian lives next to the blue house.
# Carefull with this one!
nat(i, "norwegian").Iff(color(i-1, "blue") | color(i+1, "blue")) &

# The owner who smokes Blends lives next to the one who drinks water.
smoke(i, "blends").Implies(drink(i-1, "water") | drink(i+1, "water"))
)

facts = And(facts,
# The owner living in the center house drinks milk.
drink(2, "milk"),

# The Norwegian lives in the first house.
nat(0, "norwegian")
)

domain = And(
And(ExactlyOne(color(i, c) for i in Houses) for c in Color),
And(ExactlyOne(nat(i, c) for i in Houses) for c in Nat),
And(ExactlyOne(pet(i, c) for i in Houses) for c in Pet),
And(ExactlyOne(drink(i, c) for i in Houses) for c in Drink),
And(ExactlyOne(smoke(i, c) for i in Houses) for c in Smoke),
#
And(ExactlyOne(color(i, c) for c in Color) for i in Houses),
And(ExactlyOne(nat(i, c) for c in Nat) for i in Houses),
And(ExactlyOne(pet(i, c) for c in Pet) for i in Houses),
And(ExactlyOne(drink(i, c) for c in Drink) for i in Houses),
And(ExactlyOne(smoke(i, c) for c in Smoke) for i in Houses),
)

problem = domain.And(facts)

model = get_model(problem)

if model is None:
print("UNSAT")
# We first check whether the constraints on the domain and problem
# are satisfiable in isolation.
assert is_sat(facts)
assert is_sat(domain)
assert is_unsat(problem)

# In isolation they are both fine, rules from both are probably
# interacting.
#
# The problem is given by a nesting of And().
# conjunctive_partition can be used to obtain a "flat"
# structure, i.e., a list of conjuncts.
#
from pysmt.rewritings import conjunctive_partition
conj = conjunctive_partition(problem)
ucore = get_unsat_core(conj)
print("UNSAT-Core size '%d'" % len(ucore))
for f in ucore:
print(f.serialize())

# The exact version of the UNSAT-Core depends on the solver in
# use.  Nevertheless, this represents a starting point for your
# debugging.  A possible way to approach the result is to look for
# clauses of size 1 (i.e., unit clauses). In the facts list there
# is only 1 fact:
#   0_nat_norwegian
#
# The clause ("1_color_blue" <-> "0_nat_norwegian")
# Implies that "1_color_blue"
# But (("3_color_blue" | "1_color_blue") <-> "2_nat_norwegian")
# Requires "2_nat_norwegian"
# The ExactlyOne constraint forbids that both 0 and 2 are nowegian
# thus, we have a better idea of where the problem might be.
#
# Please go back to the comment '# Careful with this!!!' in the
# facts list, and change the Iff with an Implies.
#
# Done?
#
# Good, you should be getting a model, now!
else:
for h in Houses:
# Extract the relevants bits to get some pretty-printing
c = [x for x in Color if model[color(h, x)].is_true()]
n = [x for x in Nat if model[nat(h, x)].is_true()]
p = [x for x in Pet if model[pet(h, x)].is_true()]
d = [x for x in Drink if model[drink(h, x)].is_true()]
s = [x for x in Smoke if model[smoke(h, x)].is_true()]
print(h, c, n, p, d, s)
if p == "fish":
sol = "The '%s' owns the fish!" % n
print(sol)