From 040c3a7a345f6e76f410793da4c376d225b62162 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 29 Jul 2021 09:43:30 -0700 Subject: [PATCH] Python quick start example (#6939) This is a translation of quickstart.cpp to python. --- examples/api/python/quickstart.py | 152 ++++++++++++++++++++++++++++++ 1 file changed, 152 insertions(+) create mode 100644 examples/api/python/quickstart.py 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) -- 2.30.2