From 6c608754e8058098e410e208d0b6cc0f586b79ca Mon Sep 17 00:00:00 2001 From: makaimann Date: Thu, 4 Jun 2020 15:18:35 -0700 Subject: [PATCH] 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. --- examples/api/python/bitvectors.py | 2 +- examples/api/python/floating_point.py | 82 ++++++++++++++++++++ src/api/python/cvc4.pxd | 5 +- src/api/python/cvc4.pxi | 103 +++++++++++--------------- 4 files changed, 129 insertions(+), 63 deletions(-) create mode 100755 examples/api/python/floating_point.py 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)) diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 2ca4b3645..1e0b9893b 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -86,13 +86,16 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass Result: - # Note: don't even need constructor + Result() except+ + bint isNull() except + bint isSat() except + bint isUnsat() except + bint isSatUnknown() except + bint isEntailed() except + bint isNotEntailed() except + bint isEntailmentUnknown() except + + bint operator==(const Result& r) except + + bint operator!=(const Result& r) except + string getUnknownExplanation() except + string toString() except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index e742e0061..827c53ef4 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -52,7 +52,6 @@ def expand_list_arg(num_req_args=0): ### can omit spaces between unrelated oneliners ### always use c++ default arguments #### only use default args of None at python level -#### Result class can have default because it's pure python ## Objects for hashing @@ -231,54 +230,47 @@ cdef class Op: return indices -class Result: - def __init__(self, name, explanation=""): - name = name.lower() - incomplete = False - if "(incomplete)" in name: - incomplete = True - name = name.replace("(incomplete)", "").strip() - assert name in {"sat", "unsat", "valid", "invalid", "unknown"}, \ - "can't interpret result = {}".format(name) - - self._name = name - self._explanation = explanation - self._incomplete = incomplete - - def __bool__(self): - if self._name in {"sat", "valid"}: - return True - elif self._name in {"unsat", "invalid"}: - return False - elif self._name == "unknown": - raise RuntimeError("Cannot interpret 'unknown' result as a Boolean") - else: - assert False, "Unhandled result=%s"%self._name +cdef class Result: + cdef c_Result cr + def __cinit__(self): + # gets populated by solver + self.cr = c_Result() - def __eq__(self, other): - if not isinstance(other, Result): - return False + def isNull(self): + return self.cr.isNull() - return self._name == other._name + def isSat(self): + return self.cr.isSat() - def __ne__(self, other): - return not self.__eq__(other) + def isUnsat(self): + return self.cr.isUnsat() - def __str__(self): - return self._name + def isSatUnknown(self): + return self.cr.isSatUnknown() - def __repr__(self): - return self._name + def isEntailed(self): + return self.cr.isEntailed() - def isUnknown(self): - return self._name == "unknown" + def isNotEntailed(self): + return self.cr.isNotEntailed() - def isIncomplete(self): - return self._incomplete + def isEntailmentUnknown(self): + return self.cr.isEntailmentUnknown() - @property - def explanation(self): - return self._explanation + def __eq__(self, Result other): + return self.cr == other.cr + + def __ne__(self, Result other): + return self.cr != other.cr + + def getUnknownExplanation(self): + return self.cr.getUnknownExplanation().decode() + + def __str__(self): + return self.cr.toString().decode() + + def __repr__(self): + return self.cr.toString().decode() cdef class RoundingMode: @@ -735,12 +727,9 @@ cdef class Solver: self.csolver.assertFormula(term.cterm) def checkSat(self): - cdef c_Result r = self.csolver.checkSat() - name = r.toString().decode() - explanation = "" - if r.isSatUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) + cdef Result r = Result() + r.cr = self.csolver.checkSat() + return r @expand_list_arg(num_req_args=0) def checkSatAssuming(self, *assumptions): @@ -751,17 +740,13 @@ cdef class Solver: where assumptions can also be comma-separated arguments of type (boolean) Term ''' - cdef c_Result r + cdef Result r = Result() # used if assumptions is a list of terms cdef vector[c_Term] v for a in assumptions: v.push_back(( a).cterm) - r = self.csolver.checkSatAssuming( v) - name = r.toString().decode() - explanation = "" - if r.isSatUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) + r.cr = self.csolver.checkSatAssuming( v) + return r @expand_list_arg(num_req_args=0) def checkEntailed(self, *assumptions): @@ -772,17 +757,13 @@ cdef class Solver: where assumptions can also be comma-separated arguments of type (boolean) Term ''' - cdef c_Result r + cdef Result r = Result() # used if assumptions is a list of terms cdef vector[c_Term] v for a in assumptions: v.push_back(( a).cterm) - r = self.csolver.checkEntailed( v) - name = r.toString().decode() - explanation = "" - if r.isEntailmentUnknown(): - explanation = r.getUnknownExplanation().decode() - return Result(name, explanation) + r.cr = self.csolver.checkEntailed( v) + return r @expand_list_arg(num_req_args=1) def declareDatatype(self, str symbol, *ctors): -- 2.30.2