Python quick start example (#6939)

This is a translation of quickstart.cpp to python.

1 files changed, 152 insertions, 0 deletions

diff --git a/examples/api/python/quickstart.py b/examples/api/python/quickstart.py
new file mode 100644
index 000000000..389e08be1
--- /dev/null
+++ b/examples/api/python/quickstart.py
@@ -0,0 +1,152 @@
+#!/usr/bin/env python
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# A simple demonstration of the api capabilities of cvc5, adapted from quickstart.cpp
+##
+
+import pycvc5
+from pycvc5 import kinds
+
+if __name__ == "__main__":
+  # Create a solver
+  solver = pycvc5.Solver()
+
+  # We will ask the solver to produce models and unsat cores,
+  # hence these options should be turned on.
+  solver.setOption("produce-models", "true");
+  solver.setOption("produce-unsat-cores", "true");
+
+  # The simplest way to set a logic for the solver is to choose "ALL".
+  # This enables all logics in the solver.
+  # Alternatively, "QF_ALL" enables all logics without quantifiers.
+  # To optimize the solver's behavior for a more specific logic,
+  # use the logic name, e.g. "QF_BV" or "QF_AUFBV".
+
+  # Set the logic
+  solver.setLogic("ALL");
+
+  # In this example, we will define constraints over reals and integers.
+  # Hence, we first obtain the corresponding sorts.
+  realSort = solver.getRealSort();
+  intSort = solver.getIntegerSort();
+
+  # x and y will be real variables, while a and b will be integer variables.
+  # Formally, their python type is Term,
+  # and they are called "constants" in SMT jargon:
+  x = solver.mkConst(realSort, "x");
+  y = solver.mkConst(realSort, "y");
+  a = solver.mkConst(intSort, "a");
+  b = solver.mkConst(intSort, "b");
+
+  # Our constraints regarding x and y will be:
+  #
+  #   (1)  0 < x
+  #   (2)  0 < y
+  #   (3)  x + y < 1
+  #   (4)  x <= y
+  #
+
+  # Formally, constraints are also terms. Their sort is Boolean.
+  # We will construct these constraints gradually,
+  # by defining each of their components.
+  # We start with the constant numerals 0 and 1:
+  zero = solver.mkReal(0);
+  one = solver.mkReal(1);
+
+  # Next, we construct the term x + y
+  xPlusY = solver.mkTerm(kinds.Plus, x, y);
+
+  # Now we can define the constraints.
+  # They use the operators +, <=, and <.
+  # In the API, these are denoted by Plus, Leq, and Lt.
+  constraint1 = solver.mkTerm(kinds.Lt, zero, x);
+  constraint2 = solver.mkTerm(kinds.Lt, zero, y);
+  constraint3 = solver.mkTerm(kinds.Lt, xPlusY, one);
+  constraint4 = solver.mkTerm(kinds.Leq, x, y);
+
+  # Now we assert the constraints to the solver.
+  solver.assertFormula(constraint1);
+  solver.assertFormula(constraint2);
+  solver.assertFormula(constraint3);
+  solver.assertFormula(constraint4);
+
+  # Check if the formula is satisfiable, that is,
+  # are there real values for x and y that satisfy all the constraints?
+  r1 = solver.checkSat();
+
+  # The result is either SAT, UNSAT, or UNKNOWN.
+  # In this case, it is SAT.
+  print("expected: sat")
+  print("result: ", r1)
+
+  # We can get the values for x and y that satisfy the constraints.
+  xVal = solver.getValue(x);
+  yVal = solver.getValue(y);
+
+  # It is also possible to get values for compound terms,
+  # even if those did not appear in the original formula.
+  xMinusY = solver.mkTerm(kinds.Minus, x, y);
+  xMinusYVal = solver.getValue(xMinusY);
+  
+  # We can now obtain the values as python values
+  xPy = xVal.getRealValue();
+  yPy = yVal.getRealValue();
+  xMinusYPy = xMinusYVal.getRealValue();
+
+  print("value for x: ", xPy)
+  print("value for y: ", yPy)
+  print("value for x - y: ", xMinusYPy)
+
+  # Another way to independently compute the value of x - y would be
+  # to use the python minus operator instead of asking the solver.
+  # However, for more complex terms,
+  # it is easier to let the solver do the evaluation.
+  xMinusYComputed = xPy - yPy;
+  if xMinusYComputed == xMinusYPy:
+    print("computed correctly") 
+  else:
+    print("computed incorrectly")
+
+  # Further, we can convert the values to strings
+  xStr = str(xPy);
+  yStr = str(yPy);
+  xMinusYStr = str(xMinusYPy);
+
+
+  # Next, we will check satisfiability of the same formula,
+  # only this time over integer variables a and b.
+
+  # We start by resetting assertions added to the solver.
+  solver.resetAssertions();
+
+  # Next, we assert the same assertions above with integers.
+  # This time, we inline the construction of terms
+  # to the assertion command.
+  solver.assertFormula(solver.mkTerm(kinds.Lt, solver.mkInteger(0), a));
+  solver.assertFormula(solver.mkTerm(kinds.Lt, solver.mkInteger(0), b));
+  solver.assertFormula(
+      solver.mkTerm(kinds.Lt, solver.mkTerm(kinds.Plus, a, b), solver.mkInteger(1)));
+  solver.assertFormula(solver.mkTerm(kinds.Leq, a, b));
+
+  # We check whether the revised assertion is satisfiable.
+  r2 = solver.checkSat();
+
+  # This time the formula is unsatisfiable
+  print("expected: unsat")
+  print("result:", r2)
+
+  # We can query the solver for an unsatisfiable core, i.e., a subset
+  # of the assertions that is already unsatisfiable.
+  unsatCore = solver.getUnsatCore();
+  print("unsat core size:", len(unsatCore))
+  print("unsat core:", unsatCore)