Skip to content
Permalink
Browse files

Examples: Print loggin info in portfolio.py

  • Loading branch information...
marcogario committed Jul 29, 2018
1 parent cf77bbf commit 73c553f6052be20d931a0f60710a60f932481ae0
Showing with 13 additions and 2 deletions.
  1. +1 −0 examples/README.rst
  2. +12 −2 examples/portfolio.py
@@ -19,3 +19,4 @@ This directory contains examples to get you started using pySMT. Suggested order
14. `xor.py </examples/xor.py>`_ : Equivalence checking of XOR rewriting using BitVectors
15. `qe.py </examples/qe.py>`_ : Quantifier Elimination of an LRA formula
16. `theory_combination.py </examples/theory_combination.py>`_ : Combine multiple theories (Array, BitVectors, Integer, and Reals) in the same formula
17. `portfolio.py </examples/portfolio.py>`_ : Portfolio solving
@@ -15,10 +15,16 @@
#
from pysmt.shortcuts import is_sat

# We enable logging to see what is going on behind the scenes:
import logging
_info = logging.getLogger(__name__).info
logging.basicConfig(level=logging.DEBUG)

# A solver set is an iterable of solver names or pairs of
# solvers+options (See next example)

solvers_set = ["z3", "yices"]
_info("Example 1: is_sat")
solvers_set = ["z3", "yices", "msat"]
res = is_sat(f, portfolio=solvers_set)
assert res is True

@@ -34,6 +40,8 @@

# The options given to the Portfolio will be passed to all solvers, in
# particular, we are enabling incrementality and model generation.

_info("Example 2: Portfolio()")
with Portfolio(solvers_set,
logic=QF_UFLIRA,
incremental=True,
@@ -56,9 +64,11 @@
# documentation. This is an area of pySMT that could use additional
# feedback and help!

_info("Example 3: Portfolio w options")
with Portfolio([("msat", {"random_seed": 1}),
("msat", {"random_seed": 17}),
("msat", {"random_seed": 42})],
("msat", {"random_seed": 42}),
"cvc4", "yices"],
logic=QF_UFLIRA,
incremental=False,
generate_models=False) as s:

0 comments on commit 73c553f

Please sign in to comment.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.