Merge pull request #40 from pysmt/examples

Examples

README.rst

@@ -57,28 +57,20 @@ Usage
 
 .. code:: python
 
-  from pysmt.shortcuts import Symbol, And, Not, FALSE, Solver
+  from pysmt.shortcuts import Symbol, And, Not, is_sat
 
-  with Solver() as solver:
+  varA = Symbol("A") # Default type is Boolean
+  varB = Symbol("B")
+  f = And([varA, Not(varB)])
+  g = f.substitute({varB:varA})
 
-      varA = Symbol("A") # Default type is Boolean
-      varB = Symbol("B")
+  res = is_sat(f)
+  assert res # SAT
+  print("f := %s is SAT? %s" % (f, res))
 
-      f = And([varA, Not(varB)])
-
-      print(f)
-
-      g = f.substitute({varB:varA})
-
-      print(g)
-
-      solver.add_assertion(g)
-      res = solver.solve()
-      assert not res
-
-      h = And(g, FALSE())
-      simp_h = h.simplify()
-      print(h, "-->", simp_h)
+  res = is_sat(g)
+  print("g := %s is SAT? %s" % (g, res))
+  assert not res # UNSAT
 
 
 A more complex example is the following:
@@ -91,34 +83,26 @@ The following is the pySMT code for solving this problem:
 
 .. code:: python
 
-  from pysmt.shortcuts import Symbol, LE, GE, Int, And, Equals, Plus, Solver
+  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(LE(Int(1), l),
-                     GE(Int(10), l) ) for l in letters])
+  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)
 
-  # Use context to create and free a solver. Solver are selected by name
-  # and can be used in a uniform way (try name="msat")
-  with Solver(name="z3") as solver:
-      solver.add_assertion(formula)
-      if solver.solve():
-         for l in letters:
-            print("%s = %s" %(l, solver.get_value(l)))
-      else:
-        print("No solution found")
+  model = get_model(formula)
+  if model:
+    print(model)
+  else:
+    print("No solution found")

examples/README.rst

@@ -0,0 +1,14 @@
+Example
+=======
+
+This directory contains examples to get you started using
+pySMT. Suggested order:
+
+1. basic.py : First example of the README
+2. puzzle.py : Hello World word puzzle
+3. infix_notation.py : Hello World word puzzle using infix-notation
+4. combine_solvers.py : Combine multiple solvers to solve the same
+5. model_checking.py : Model-Checking an infinite state system
+   (BMC+K-Induction) in ~150 lines
+6. allsat.py: How to access functionalities of solvers not currently
+   wrapped by pySMT.

examples/allsat.py

@@ -0,0 +1,39 @@
+# 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)

examples/basic.py

@@ -0,0 +1,21 @@
+# 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

examples/combine_solvers.py

@@ -0,0 +1,26 @@
+# 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

examples/infix_notation.py

@@ -0,0 +1,42 @@
+# 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 get_env, Solver
+from pysmt.shortcuts import Symbol, And, Plus, Int
+from pysmt.typing import INT
+
+# Infix-Notation is disable by default
+get_env().enable_infix_notation = True
+
+hello = [Symbol(s, INT) for s in "hello"]
+world = [Symbol(s, INT) for s in "world"]
+letters = set(hello+world)
+
+# Infix notation for Theory atoms does the overloading of python
+# 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:
+    solver.add_assertion(formula)
+    if solver.solve():
+        for l in letters:
+            print("%s = %s" %(l, solver.get_value(l)))
+    else:
+        print("No solution found")