diff options
author | makaimann <makaim@stanford.edu> | 2020-06-04 15:18:35 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-04 15:18:35 -0700 |
commit | 6c608754e8058098e410e208d0b6cc0f586b79ca (patch) | |
tree | 6e1f58c09e6dd08eab04ec43acebd796d7cf8c99 /examples | |
parent | f0169b253759632aee0d21db916fe68702c66116 (diff) |
Wrap Result in Python API (#4473)
This PR would change the Python API to wrap the C++ Result class instead of translating it to a pure Python class. This is more convenient because there are several possibilities other than sat/unsat/unknown. Furthermore, this PR updates the bitvectors.py example which had an incorrect function name "checkEntailment" and adds a floating point example contributed by Eva Darulova.
Diffstat (limited to 'examples')
-rwxr-xr-x | examples/api/python/bitvectors.py | 2 | ||||
-rwxr-xr-x | examples/api/python/floating_point.py | 82 |
2 files changed, 83 insertions, 1 deletions
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index 8e4e1b682..f12e79541 100755 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -84,7 +84,7 @@ if __name__ == "__main__": print("Checking entailment assuming:", new_x_eq_new_x_) print("Expect ENTAILED.") - print("CVC4:", slv.checkEntailment(new_x_eq_new_x_)) + print("CVC4:", slv.checkEntailed(new_x_eq_new_x_)) print("Popping context.") slv.pop() diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py new file mode 100755 index 000000000..c92666c0b --- /dev/null +++ b/examples/api/python/floating_point.py @@ -0,0 +1,82 @@ +#!/usr/bin/env python + +##################### +#! \file floating_point.py + ## \verbatim + ## Top contributors (to current version): + ## Eva Darulova, Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 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.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## floating point solver through the Python API contributed by Eva + ## Darulova. This requires building CVC4 with symfpu. + +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setOption("produce-models", "true") + slv.setLogic("FP") + + # single 32-bit precision + fp32 = slv.mkFloatingPointSort(8, 24) + + # the standard rounding mode + rm = slv.mkRoundingMode(pycvc4.RoundNearestTiesToEven) + + # create a few single-precision variables + x = slv.mkConst(fp32, 'x') + y = slv.mkConst(fp32, 'y') + z = slv.mkConst(fp32, 'z') + + # check floating-point arithmetic is commutative, i.e. x + y == y + x + commutative = slv.mkTerm(kinds.FPEq, slv.mkTerm(kinds.FPPlus, rm, x, y), slv.mkTerm(kinds.FPPlus, rm, y, x)) + + slv.push() + slv.assertFormula(slv.mkTerm(kinds.Not, commutative)) + print("Checking floating-point commutativity") + print("Expect SAT (property does not hold for NaN and Infinities).") + print("CVC4:", slv.checkSat()) + print("Model for x:", slv.getValue(x)) + print("Model for y:", slv.getValue(y)) + + # disallow NaNs and Infinities + slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsNan, x))) + slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsInf, x))) + slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsNan, y))) + slv.assertFormula(slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPIsInf, y))) + + print("Checking floating-point commutativity assuming x and y are not NaN or Infinity") + print("Expect UNSAT.") + print("CVC4:", slv.checkSat()) + + # check floating-point arithmetic is not associative + slv.pop() + + # constrain x, y, z between -3.14 and 3.14 (also disallows NaN and infinity) + a = slv.mkFloatingPoint(8, 24, slv.mkBitVector("11000000010010001111010111000011", 2)) # -3.14 + b = slv.mkFloatingPoint(8, 24, slv.mkBitVector("01000000010010001111010111000011", 2)) # 3.14 + + bounds_x = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, x), slv.mkTerm(kinds.FPLeq, x, b)) + bounds_y = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, y), slv.mkTerm(kinds.FPLeq, y, b)) + bounds_z = slv.mkTerm(kinds.And, slv.mkTerm(kinds.FPLeq, a, z), slv.mkTerm(kinds.FPLeq, z, b)) + slv.assertFormula(slv.mkTerm(kinds.And, slv.mkTerm(kinds.And, bounds_x, bounds_y), bounds_z)) + + # (x + y) + z == x + (y + z) + lhs = slv.mkTerm(kinds.FPPlus, rm, slv.mkTerm(kinds.FPPlus, rm, x, y), z) + rhs = slv.mkTerm(kinds.FPPlus, rm, x, slv.mkTerm(kinds.FPPlus, rm, y, z)) + associative = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPEq, lhs, rhs)) + + slv.assertFormula(associative) + + print("Checking floating-point associativity") + print("Expect SAT.") + print("CVC4:", slv.checkSat()) + print("Model for x:", slv.getValue(x)) + print("Model for y:", slv.getValue(y)) + print("Model for z:", slv.getValue(z)) |