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.
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()
--- /dev/null
+#!/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))
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 +
### 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
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:
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):
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((<Term?> a).cterm)
- r = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
- name = r.toString().decode()
- explanation = ""
- if r.isSatUnknown():
- explanation = r.getUnknownExplanation().decode()
- return Result(name, explanation)
+ r.cr = self.csolver.checkSatAssuming(<const vector[c_Term]&> v)
+ return r
@expand_list_arg(num_req_args=0)
def checkEntailed(self, *assumptions):
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((<Term?> a).cterm)
- r = self.csolver.checkEntailed(<const vector[c_Term]&> v)
- name = r.toString().decode()
- explanation = ""
- if r.isEntailmentUnknown():
- explanation = r.getUnknownExplanation().decode()
- return Result(name, explanation)
+ r.cr = self.csolver.checkEntailed(<const vector[c_Term]&> v)
+ return r
@expand_list_arg(num_req_args=1)
def declareDatatype(self, str symbol, *ctors):
projects / cvc5.git / commitdiff