diff options
author | makaimann <makaim@stanford.edu> | 2020-02-19 13:54:17 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-19 15:54:17 -0600 |
commit | c82720479efcf922136f0919f6fc26a502b2515a (patch) | |
tree | f9007e124cfc07490e914ae1e1e05747e1e1ee11 /src/api | |
parent | c6a9ab9da205df7cbf192edc142ee151404dcb1b (diff) |
Add Python bindings using Cython -- see below for more details (#2879)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 25 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 20 | ||||
-rw-r--r-- | src/api/python/CMakeLists.txt | 42 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 274 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 1181 | ||||
-rwxr-xr-x | src/api/python/genkinds.py | 255 | ||||
-rw-r--r-- | src/api/python/pycvc4.pyx | 2 |
7 files changed, 1798 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f4ca1147f..7bdc5008b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1755,27 +1755,40 @@ DatatypeDecl::DatatypeDecl(const Solver* s, new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype)); } +bool DatatypeDecl::isNullHelper() const { return !d_dtype; } + +DatatypeDecl::DatatypeDecl() {} + DatatypeDecl::~DatatypeDecl() {} void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) { + CVC4_API_CHECK_NOT_NULL; d_dtype->addConstructor(*ctor.d_ctor); } size_t DatatypeDecl::getNumConstructors() const { + CVC4_API_CHECK_NOT_NULL; return d_dtype->getNumConstructors(); } -bool DatatypeDecl::isParametric() const { return d_dtype->isParametric(); } +bool DatatypeDecl::isParametric() const +{ + CVC4_API_CHECK_NOT_NULL; + return d_dtype->isParametric(); +} std::string DatatypeDecl::toString() const { + CVC4_API_CHECK_NOT_NULL; std::stringstream ss; ss << *d_dtype; return ss.str(); } +bool DatatypeDecl::isNull() const { return isNullHelper(); } + // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! const CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } @@ -1895,6 +1908,9 @@ DatatypeConstructor::const_iterator::const_iterator( d_idx = begin ? 0 : sels->size(); } +// Nullary constructor for Cython +DatatypeConstructor::const_iterator::const_iterator() {} + DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator:: operator=(const DatatypeConstructor::const_iterator& it) { @@ -1969,6 +1985,9 @@ Datatype::Datatype(const CVC4::Datatype& dtype) { } +// Nullary constructor for Cython +Datatype::Datatype() {} + Datatype::~Datatype() {} DatatypeConstructor Datatype::operator[](size_t idx) const @@ -2007,6 +2026,8 @@ size_t Datatype::getNumConstructors() const bool Datatype::isParametric() const { return d_dtype->isParametric(); } +std::string Datatype::toString() const { return d_dtype->getName(); } + Datatype::const_iterator Datatype::begin() const { return Datatype::const_iterator(*d_dtype, true); @@ -2035,6 +2056,8 @@ Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, d_idx = begin ? 0 : cons->size(); } +Datatype::const_iterator::const_iterator() {} + Datatype::const_iterator& Datatype::const_iterator::operator=( const Datatype::const_iterator& it) { diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index f7f16832a..79c02c031 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1096,6 +1096,11 @@ class CVC4_PUBLIC DatatypeDecl friend class Solver; public: /** + * Nullary constructor for Cython + */ + DatatypeDecl(); + + /** * Destructor. */ ~DatatypeDecl(); @@ -1112,6 +1117,8 @@ class CVC4_PUBLIC DatatypeDecl /** Is this Datatype declaration parametric? */ bool isParametric() const; + bool isNull() const; + /** * @return a string representation of this datatype declaration */ @@ -1158,6 +1165,10 @@ class CVC4_PUBLIC DatatypeDecl const std::string& name, const std::vector<Sort>& params, bool isCoDatatype = false); + + // helper for isNull() to avoid calling API functions from other API functions + bool isNullHelper() const; + /* The internal (intermediate) datatype wrapped by this datatype * declaration * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -1295,6 +1306,9 @@ class CVC4_PUBLIC DatatypeConstructor friend class DatatypeConstructor; // to access constructor public: + /** Nullary constructor (required for Cython). */ + const_iterator(); + /** * Assignment operator. * @param it the iterator to assign to @@ -1398,6 +1412,9 @@ class CVC4_PUBLIC Datatype */ Datatype(const CVC4::Datatype& dtype); + // Nullary constructor for Cython + Datatype(); + /** * Destructor. */ @@ -1447,6 +1464,9 @@ class CVC4_PUBLIC Datatype friend class Datatype; // to access constructor public: + /** Nullary constructor (required for Cython). */ + const_iterator(); + /** * Assignment operator. * @param it the iterator to assign to diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt new file mode 100644 index 000000000..166a728de --- /dev/null +++ b/src/api/python/CMakeLists.txt @@ -0,0 +1,42 @@ +if(POLICY CMP0057) + # For cmake >= 3.3 this policy changed the behavior of IN_LIST + # if the policy exists, we use the NEW behavior + cmake_policy(SET CMP0057 NEW) +endif() + +find_package(PythonExtensions REQUIRED) +find_package(Cython 0.29 REQUIRED) + +include_directories(${PYTHON_INCLUDE_DIRS}) +include_directories(${CMAKE_CURRENT_LIST_DIR}) # cvc4kinds.pxd +include_directories(${PROJECT_SOURCE_DIR}/src) +include_directories(${PROJECT_SOURCE_DIR}/src/include) +include_directories(${CMAKE_CURRENT_BINARY_DIR}) +# TEMP: Only needed while expr/kind.h is public in the C++ api +include_directories("${CMAKE_BINARY_DIR}/src/") + +# Generate cvc4kinds.{pxd,pyx} +add_custom_target( + gen-pycvc4-kinds + ALL + COMMAND + "${PYTHON_EXECUTABLE}" + "${CMAKE_CURRENT_LIST_DIR}/genkinds.py" + --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cvc4cppkind.h" + --kinds-file-prefix "cvc4kinds" + DEPENDS + genkinds.py + COMMENT + "Generate cvc4kinds.{pxd,pyx}" +) + +add_cython_target(pycvc4 CXX) + +add_library(pycvc4 + MODULE + ${pycvc4}) + +target_link_libraries(pycvc4 cvc4 ${PYTHON_LIBRARIES}) + +python_extension_module(pycvc4) +install(TARGETS pycvc4 DESTINATION lib) diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd new file mode 100644 index 000000000..b8bf009af --- /dev/null +++ b/src/api/python/cvc4.pxd @@ -0,0 +1,274 @@ +# import dereference and increment operators +from cython.operator cimport dereference as deref, preincrement as inc +from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t +from libcpp.string cimport string +from libcpp.vector cimport vector +from libcpp.pair cimport pair +from cvc4kinds cimport Kind + + +cdef extern from "<iostream>" namespace "std": + cdef cppclass ostream: + pass + ostream cout + + +cdef extern from "api/cvc4cpp.h" namespace "CVC4": + cdef cppclass Options: + pass + + +cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": + cdef cppclass Datatype: + Datatype() except + + DatatypeConstructor operator[](const string& name) except + + DatatypeConstructor getConstructor(const string& name) except + + Term getConstructorTerm(const string& name) except + + size_t getNumConstructors() except + + bint isParametric() except + + string toString() except + + cppclass const_iterator: + const_iterator() except + + bint operator==(const const_iterator& it) except + + bint operator!=(const const_iterator& it) except + + const_iterator& operator++(); + const DatatypeConstructor& operator*() except + + const_iterator begin() except + + const_iterator end() except + + + + cdef cppclass DatatypeConstructor: + DatatypeConstructor() except + + DatatypeSelector operator[](const string& name) except + + DatatypeSelector getSelector(const string& name) except + + Term getSelectorTerm(const string& name) except + + string toString() except + + cppclass const_iterator: + const_iterator() except + + bint operator==(const const_iterator& it) except + + bint operator!=(const const_iterator& it) except + + const_iterator& operator++(); + const DatatypeSelector& operator*() except + + const_iterator begin() except + + const_iterator end() except + + + + cdef cppclass DatatypeConstructorDecl: + DatatypeConstructorDecl(const string& name) except + + void addSelector(const DatatypeSelectorDecl& stor) except + + string toString() except + + + + cdef cppclass DatatypeDecl: + void addConstructor(const DatatypeConstructorDecl& ctor) except + + bint isParametric() except + + string toString() except + + + + cdef cppclass DatatypeDeclSelfSort: + DatatypeDeclSelfSort() except + + + + cdef cppclass DatatypeSelector: + DatatypeSelector() except + + string toString() except + + + + cdef cppclass DatatypeSelectorDecl: + DatatypeSelectorDecl(const string& name, Sort sort) except + + DatatypeSelectorDecl(const string& name, DatatypeDeclSelfSort sort) except + + string toString() except + + + + cdef cppclass Op: + Op() except + + bint operator==(const Op&) except + + bint operator!=(const Op&) except + + Kind getKind() except + + Sort getSort() except + + bint isNull() except + + T getIndices[T]() except + + string toString() except + + + + cdef cppclass Result: + # Note: don't even need constructor + bint isSat() except + + bint isUnsat() except + + bint isSatUnknown() except + + bint isValid() except + + bint isInvalid() except + + bint isValidUnknown() except + + string getUnknownExplanation() except + + string toString() except + + + + cdef cppclass RoundingMode: + pass + + + cdef cppclass Solver: + Solver(Options*) except + + Sort getBooleanSort() except + + Sort getIntegerSort() except + + Sort getRealSort() except + + Sort getRegExpSort() except + + Sort getRoundingmodeSort() except + + Sort getStringSort() except + + Sort mkArraySort(Sort indexSort, Sort elemSort) except + + Sort mkBitVectorSort(uint32_t size) except + + Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) except + + Sort mkDatatypeSort(DatatypeDecl dtypedecl) except + + Sort mkFunctionSort(Sort domain, Sort codomain) except + + Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except + + Sort mkParamSort(const string& symbol) except + + Sort mkPredicateSort(const vector[Sort]& sorts) except + + Sort mkRecordSort(const vector[pair[string, Sort]]& fields) except + + Sort mkSetSort(Sort elemSort) except + + Sort mkUninterpretedSort(const string& symbol) except + + Sort mkSortConstructorSort(const string& symbol, size_t arity) except + + Sort mkTupleSort(const vector[Sort]& sorts) except + + Term mkTerm(Op op) except + + Term mkTerm(Op op, const vector[Term]& children) except + + Op mkOp(Kind kind) except + + Op mkOp(Kind kind, Kind k) except + + Op mkOp(Kind kind, const string& arg) except + + Op mkOp(Kind kind, uint32_t arg) except + + Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except + + Term mkTrue() except + + Term mkFalse() except + + Term mkBoolean(bint val) except + + Term mkPi() except + + Term mkReal(const string& s) except + + Term mkRegexpEmpty() except + + Term mkRegexpSigma() except + + Term mkEmptySet(Sort s) except + + Term mkSepNil(Sort sort) except + + Term mkString(const string& s) except + + Term mkString(const vector[unsigned]& s) except + + Term mkUniverseSet(Sort sort) except + + Term mkBitVector(uint32_t size) except + + Term mkBitVector(uint32_t size, uint64_t val) except + + Term mkBitVector(const string& s) except + + Term mkBitVector(const string& s, uint32_t base) except + + Term mkConstArray(Sort sort, Term val) except + + Term mkPosInf(uint32_t exp, uint32_t sig) except + + Term mkNegInf(uint32_t exp, uint32_t sig) except + + Term mkNaN(uint32_t exp, uint32_t sig) except + + Term mkPosZero(uint32_t exp, uint32_t sig) except + + Term mkNegZero(uint32_t exp, uint32_t sig) except + + Term mkRoundingMode(RoundingMode rm) except + + Term mkUninterpretedConst(Sort sort, int32_t index) except + + Term mkAbstractValue(const string& index) except + + Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except + + Term mkConst(Sort sort, const string& symbol) except + + # default value for symbol defined in cvc4cpp.h + Term mkConst(Sort sort) except + + Term mkVar(Sort sort, const string& symbol) except + + DatatypeDecl mkDatatypeDecl(const string& name) except + + DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except + + DatatypeDecl mkDatatypeDecl(const string& name, Sort param) except + + DatatypeDecl mkDatatypeDecl(const string& name, Sort param, bint isCoDatatype) except + + DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params) except + + DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params, bint isCoDatatype) except + + # default value for symbol defined in cvc4cpp.h + Term mkVar(Sort sort) except + + Term simplify(const Term& t) except + + void assertFormula(Term term) except + + Result checkSat() except + + Result checkSatAssuming(const vector[Term]& assumptions) except + + Result checkValid() except + + Result checkValidAssuming(const vector[Term]& assumptions) except + + Sort declareDatatype(const string& symbol, const vector[DatatypeConstructorDecl]& ctors) + Term declareFun(const string& symbol, Sort sort) except + + Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except + + Sort declareSort(const string& symbol, uint32_t arity) except + + Term defineFun(const string& symbol, const vector[Term]& bound_vars, + Sort sort, Term term) except + + Term defineFun(Term fun, const vector[Term]& bound_vars, Term term) except + + Term defineFunRec(const string& symbol, const vector[Term]& bound_vars, + Sort sort, Term term) except + + Term defineFunRec(Term fun, const vector[Term]& bound_vars, + Term term) except + + Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars, + vector[Term]& terms) except + + vector[Term] getAssertions() except + + vector[pair[Term, Term]] getAssignment() except + + string getInfo(const string& flag) except + + string getOption(string& option) except + + vector[Term] getUnsatAssumptions() except + + vector[Term] getUnsatCore() except + + Term getValue(Term term) except + + vector[Term] getValue(const vector[Term]& terms) except + + void pop(uint32_t nscopes) except + + void printModel(ostream& out) + void push(uint32_t nscopes) except + + void reset() except + + void resetAssertions() except + + void setInfo(string& keyword, const string& value) except + + void setLogic(const string& logic) except + + void setOption(const string& option, const string& value) except + + + + cdef cppclass Sort: + Sort() except + + bint operator==(const Sort&) except + + bint operator!=(const Sort&) except + + bint isBoolean() except + + bint isInteger() except + + bint isReal() except + + bint isString() except + + bint isRegExp() except + + bint isRoundingMode() except + + bint isBitVector() except + + bint isFloatingPoint() except + + bint isDatatype() except + + bint isParametricDatatype() except + + bint isFunction() except + + bint isPredicate() except + + bint isTuple() except + + bint isRecord() except + + bint isArray() except + + bint isSet() except + + bint isUninterpretedSort() except + + bint isSortConstructor() except + + bint isFirstClass() except + + bint isFunctionLike() except + + Datatype getDatatype() except + + Sort instantiate(const vector[Sort]& params) except + + bint isUninterpretedSortParameterized() except + + string toString() except + + + cdef cppclass Term: + Term() + bint operator==(const Term&) except + + bint operator!=(const Term&) except + + Kind getKind() except + + Sort getSort() except + + bint hasOp() except + + Op getOp() except + + bint isNull() except + + Term notTerm() except + + Term andTerm(const Term& t) except + + Term orTerm(const Term& t) except + + Term xorTerm(const Term& t) except + + Term eqTerm(const Term& t) except + + Term impTerm(const Term& t) except + + Term iteTerm(const Term& then_t, const Term& else_t) except + + string toString() except + + cppclass const_iterator: + const_iterator() except + + bint operator==(const const_iterator& it) except + + bint operator!=(const const_iterator& it) except + + const_iterator& operator++(); + Term operator*() except + + const_iterator begin() except + + const_iterator end() except + + + +cdef extern from "api/cvc4cpp.h" namespace "CVC4::api::RoundingMode": + cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN, + cdef RoundingMode ROUND_TOWARD_POSITIVE, + cdef RoundingMode ROUND_TOWARD_NEGATIVE, + cdef RoundingMode ROUND_TOWARD_ZERO, + cdef RoundingMode ROUND_NEAREST_TIES_TO_AWAY diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi new file mode 100644 index 000000000..39d9d4686 --- /dev/null +++ b/src/api/python/cvc4.pxi @@ -0,0 +1,1181 @@ +import sys + +from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t + +from libcpp.pair cimport pair +from libcpp.string cimport string +from libcpp.vector cimport vector + +from cvc4 cimport cout +from cvc4 cimport Datatype as c_Datatype +from cvc4 cimport DatatypeConstructor as c_DatatypeConstructor +from cvc4 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl +from cvc4 cimport DatatypeDecl as c_DatatypeDecl +from cvc4 cimport DatatypeDeclSelfSort as c_DatatypeDeclSelfSort +from cvc4 cimport DatatypeSelector as c_DatatypeSelector +from cvc4 cimport DatatypeSelectorDecl as c_DatatypeSelectorDecl +from cvc4 cimport Result as c_Result +from cvc4 cimport RoundingMode as c_RoundingMode +from cvc4 cimport Op as c_Op +from cvc4 cimport Solver as c_Solver +from cvc4 cimport Sort as c_Sort +from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE +from cvc4 cimport ROUND_TOWARD_ZERO, ROUND_NEAREST_TIES_TO_AWAY +from cvc4 cimport Term as c_Term + +from cvc4kinds cimport Kind as c_Kind + +################################## DECORATORS ################################# +def expand_list_arg(num_req_args=0): + ''' + Creates a decorator that looks at index num_req_args of the args, + if it's a list, it expands it before calling the function. + ''' + def decorator(func): + def wrapper(owner, *args): + if len(args) == num_req_args + 1 and \ + isinstance(args[num_req_args], list): + args = list(args[:num_req_args]) + args[num_req_args] + return func(owner, *args) + return wrapper + return decorator +############################################################################### + +# Style Guidelines +### Using PEP-8 spacing recommendations +### Limit linewidth to 79 characters +### Break before binary operators +### surround top level functions and classes with two spaces +### separate methods by one space +### use spaces in functions sparingly to separate logical blocks +### 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 + + +cdef class Datatype: + cdef c_Datatype cd + def __cinit__(self): + pass + + def __getitem__(self, str name): + cdef DatatypeConstructor dc = DatatypeConstructor() + dc.cdc = self.cd[name.encode()] + return dc + + def getConstructor(self, str name): + cdef DatatypeConstructor dc = DatatypeConstructor() + dc.cdc = self.cd.getConstructor(name.encode()) + return dc + + def getConstructorTerm(self, str name): + cdef Term term = Term() + term.cterm = self.cd.getConstructorTerm(name.encode()) + return term + + def getNumConstructors(self): + return self.cd.getNumConstructors() + + def isParametric(self): + return self.cd.isParametric() + + def __str__(self): + return self.cd.toString().decode() + + def __repr__(self): + return self.cd.toString().decode() + + def __iter__(self): + for ci in self.cd: + dc = DatatypeConstructor() + dc.cdc = ci + yield dc + + +cdef class DatatypeConstructor: + cdef c_DatatypeConstructor cdc + def __cinit__(self): + self.cdc = c_DatatypeConstructor() + + def __getitem__(self, str name): + cdef DatatypeSelector ds = DatatypeSelector() + ds.cds = self.cdc[name.encode()] + return ds + + def getSelector(self, str name): + cdef DatatypeSelector ds = DatatypeSelector() + ds.cds = self.cdc.getSelector(name.encode()) + return ds + + def getSelectorTerm(self, str name): + cdef Term term = Term() + term.cterm = self.cdc.getSelectorTerm(name.encode()) + return term + + def __str__(self): + return self.cdc.toString().decode() + + def __repr__(self): + return self.cdc.toString().decode() + + def __iter__(self): + for ci in self.cdc: + ds = DatatypeSelector() + ds.cds = ci + yield ds + + +cdef class DatatypeConstructorDecl: + cdef c_DatatypeConstructorDecl* cddc + def __cinit__(self, str name): + self.cddc = new c_DatatypeConstructorDecl(name.encode()) + + def addSelector(self, DatatypeSelectorDecl stor): + self.cddc.addSelector(stor.cdsd[0]) + + def __str__(self): + return self.cddc.toString().decode() + + def __repr__(self): + return self.cddc.toString().decode() + + +cdef class DatatypeDecl: + cdef c_DatatypeDecl cdd + def __cinit__(self): + pass + + def addConstructor(self, DatatypeConstructorDecl ctor): + self.cdd.addConstructor(ctor.cddc[0]) + + def isParametric(self): + return self.cdd.isParametric() + + def __str__(self): + return self.cdd.toString().decode() + + def __repr__(self): + return self.cdd.toString().decode() + + +cdef class DatatypeDeclSelfSort: + cdef c_DatatypeDeclSelfSort cddss + def __cinit__(self): + self.cddss = c_DatatypeDeclSelfSort() + + +cdef class DatatypeSelector: + cdef c_DatatypeSelector cds + def __cinit__(self): + self.cds = c_DatatypeSelector() + + def __str__(self): + return self.cds.toString().decode() + + def __repr__(self): + return self.cds.toString().decode() + + +cdef class DatatypeSelectorDecl: + cdef c_DatatypeSelectorDecl* cdsd + def __cinit__(self, str name, sort): + if isinstance(sort, Sort): + self.cdsd = new c_DatatypeSelectorDecl( + <const string &> name.encode(), (<Sort?> sort).csort) + elif isinstance(sort, DatatypeDeclSelfSort): + self.cdsd = new c_DatatypeSelectorDecl( + <const string &> name.encode(), + (<DatatypeDeclSelfSort?> sort).cddss) + + def __str__(self): + return self.cdsd.toString().decode() + + def __repr__(self): + return self.cdsd.toString().decode() + + +cdef class Op: + cdef c_Op cop + def __cinit__(self): + self.cop = c_Op() + + def __eq__(self, Op other): + return self.cop == other.cop + + def __ne__(self, Op other): + return self.cop != other.cop + + def __str__(self): + return self.cop.toString().decode() + + def __repr__(self): + return self.cop.toString().decode() + + def getKind(self): + return kind(<int> self.cop.getKind()) + + def getSort(self): + cdef Sort sort = Sort() + sort.csort = self.cop.getSort() + return sort + + def isNull(self): + return self.cop.isNull() + + def getIndices(self): + indices = None + try: + indices = self.cop.getIndices[string]() + except: + pass + + try: + indices = kind(<int> self.cop.getIndices[c_Kind]()) + except: + pass + + try: + indices = self.cop.getIndices[uint32_t]() + except: + pass + + try: + indices = self.cop.getIndices[pair[uint32_t, uint32_t]]() + except: + pass + + if indices is None: + raise RuntimeError("Unable to retrieve indices from {}".format(self)) + + 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 + + def __eq__(self, other): + if not isinstance(other, Result): + return False + + return self._name == other._name + + def __ne__(self, other): + return not self.__eq__(other) + + def __str__(self): + return self._name + + def __repr__(self): + return self._name + + def isUnknown(self): + return self._name == "unknown" + + def isIncomplete(self): + return self._incomplete + + @property + def explanation(self): + return self._explanation + + +cdef class RoundingMode: + cdef c_RoundingMode crm + cdef str name + def __cinit__(self, int rm): + # crm always assigned externally + self.crm = <c_RoundingMode> rm + self.name = __rounding_modes[rm] + + def __eq__(self, RoundingMode other): + return (<int> self.crm) == (<int> other.crm) + + def __ne__(self, RoundingMode other): + return not self.__eq__(other) + + def __hash__(self): + return hash((<int> self.crm, self.name)) + + def __str__(self): + return self.name + + def __repr__(self): + return self.name + + +cdef class Solver: + cdef c_Solver* csolver + + def __cinit__(self): + self.csolver = new c_Solver(NULL) + + def getBooleanSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getBooleanSort() + return sort + + def getIntegerSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getIntegerSort() + return sort + + def getRealSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getRealSort() + return sort + + def getRegExpSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getRegExpSort() + return sort + + def getRoundingmodeSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getRoundingmodeSort() + return sort + + def getStringSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getStringSort() + return sort + + def mkArraySort(self, Sort indexSort, Sort elemSort): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort) + return sort + + def mkBitVectorSort(self, uint32_t size): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkBitVectorSort(size) + return sort + + def mkFloatingPointSort(self, uint32_t exp, uint32_t sig): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkFloatingPointSort(exp, sig) + return sort + + def mkDatatypeSort(self, DatatypeDecl dtypedecl): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd) + return sort + + def mkFunctionSort(self, sorts, Sort codomain): + + cdef Sort sort = Sort() + # populate a vector with dereferenced c_Sorts + cdef vector[c_Sort] v + + if isinstance(sorts, Sort): + sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort, + codomain.csort) + elif isinstance(sorts, list): + for s in sorts: + v.push_back((<Sort?>s).csort) + + sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v, + codomain.csort) + return sort + + def mkParamSort(self, symbolname): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkParamSort(symbolname.encode()) + return sort + + @expand_list_arg(num_req_args=0) + def mkPredicateSort(self, *sorts): + ''' + Supports the following arguments: + Sort mkPredicateSort(List[Sort] sorts) + + where sorts can also be comma-separated arguments of + type Sort + ''' + cdef Sort sort = Sort() + cdef vector[c_Sort] v + for s in sorts: + v.push_back((<Sort?> s).csort) + sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v) + return sort + + @expand_list_arg(num_req_args=0) + def mkRecordSort(self, *fields): + ''' + Supports the following arguments: + Sort mkRecordSort(List[Tuple[str, Sort]] fields) + + where fields can also be comma-separated arguments of + type Tuple[str, Sort] + ''' + cdef Sort sort = Sort() + cdef vector[pair[string, c_Sort]] v + cdef pair[string, c_Sort] p + for f in fields: + name, sortarg = f + name = name.encode() + p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort) + v.push_back(p) + sort.csort = self.csolver.mkRecordSort( + <const vector[pair[string, c_Sort]] &> v) + return sort + + def mkSetSort(self, Sort elemSort): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkSetSort(elemSort.csort) + return sort + + def mkUninterpretedSort(self, str name): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkUninterpretedSort(name.encode()) + return sort + + def mkSortConstructorSort(self, str symbol, size_t arity): + cdef Sort sort = Sort() + sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity) + return sort + + @expand_list_arg(num_req_args=0) + def mkTupleSort(self, *sorts): + ''' + Supports the following arguments: + Sort mkTupleSort(List[Sort] sorts) + + where sorts can also be comma-separated arguments of + type Sort + ''' + cdef Sort sort = Sort() + cdef vector[c_Sort] v + for s in sorts: + v.push_back((<Sort?> s).csort) + sort.csort = self.csolver.mkTupleSort(v) + return sort + + @expand_list_arg(num_req_args=1) + def mkTerm(self, kind_or_op, *args): + ''' + Supports the following arguments: + Term mkTerm(Kind kind) + Term mkTerm(Kind kind, Op child1, List[Term] children) + Term mkTerm(Kind kind, List[Term] children) + + where List[Term] can also be comma-separated arguments + ''' + cdef Term term = Term() + cdef vector[c_Term] v + + op = kind_or_op + if isinstance(kind_or_op, kind): + op = self.mkOp(kind_or_op) + + if len(args) == 0: + term.cterm = self.csolver.mkTerm((<Op?> op).cop) + else: + for a in args: + v.push_back((<Term?> a).cterm) + term.cterm = self.csolver.mkTerm((<Op?> op).cop, v) + return term + + def mkOp(self, kind k, arg0=None, arg1 = None): + ''' + Supports the following uses: + Op mkOp(Kind kind) + Op mkOp(Kind kind, Kind k) + Op mkOp(Kind kind, const string& arg) + Op mkOp(Kind kind, uint32_t arg) + Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1) + ''' + cdef Op op = Op() + + if arg0 is None: + op.cop = self.csolver.mkOp(k.k) + elif arg1 is None: + if isinstance(arg0, kind): + op.cop = self.csolver.mkOp(k.k, (<kind?> arg0).k) + elif isinstance(arg0, str): + op.cop = self.csolver.mkOp(k.k, + <const string &> + arg0.encode()) + elif isinstance(arg0, int): + op.cop = self.csolver.mkOp(k.k, <int?> arg0) + else: + raise ValueError("Unsupported signature" + " mkOp: {}".format(" X ".join([k, arg0]))) + else: + if isinstance(arg0, int) and isinstance(arg1, int): + op.cop = self.csolver.mkOp(k.k, <int> arg0, + <int> arg1) + else: + raise ValueError("Unsupported signature" + " mkOp: {}".format(" X ".join([k, arg0, arg1]))) + return op + + def mkTrue(self): + cdef Term term = Term() + term.cterm = self.csolver.mkTrue() + return term + + def mkFalse(self): + cdef Term term = Term() + term.cterm = self.csolver.mkFalse() + return term + + def mkBoolean(self, bint val): + cdef Term term = Term() + term.cterm = self.csolver.mkBoolean(val) + return term + + def mkPi(self): + cdef Term term = Term() + term.cterm = self.csolver.mkPi() + return term + + def mkReal(self, val, den=None): + cdef Term term = Term() + if den is None: + try: + term.cterm = self.csolver.mkReal(str(val).encode()) + except Exception as e: + raise ValueError("Expecting a number" + " or a string representing a number" + " but got: {}".format(val)) + else: + if not isinstance(val, int) or not isinstance(den, int): + raise ValueError("Expecting integers when" + " constructing a rational" + " but got: {}".format((val, den))) + term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode()) + return term + + def mkRegexpEmpty(self): + cdef Term term = Term() + term.cterm = self.csolver.mkRegexpEmpty() + return term + + def mkRegexpSigma(self): + cdef Term term = Term() + term.cterm = self.csolver.mkRegexpSigma() + return term + + def mkEmptySet(self, Sort s): + cdef Term term = Term() + term.cterm = self.csolver.mkEmptySet(s.csort) + return term + + def mkSepNil(self, Sort sort): + cdef Term term = Term() + term.cterm = self.csolver.mkSepNil(sort.csort) + return term + + def mkString(self, str_or_vec): + cdef Term term = Term() + cdef vector[unsigned] v + if isinstance(str_or_vec, str): + term.cterm = self.csolver.mkString(<string &> str_or_vec.encode()) + elif isinstance(str_or_vec, list): + for u in str_or_vec: + if not isinstance(u, int): + raise ValueError("List should contain ints but got: {}" + .format(str_or_vec)) + v.push_back(<unsigned> u) + term.cterm = self.csolver.mkString(<const vector[unsigned]&> v) + else: + raise ValueError("Expected string or vector of ASCII codes" + " but got: {}".format(str_or_vec)) + return term + + def mkUniverseSet(self, Sort sort): + cdef Term term = Term() + term.cterm = self.csolver.mkUniverseSet(sort.csort) + return term + + def mkBitVector(self, size_or_str, val = None): + cdef Term term = Term() + if isinstance(size_or_str, int): + if val is None: + term.cterm = self.csolver.mkBitVector(<int> size_or_str) + else: + term.cterm = self.csolver.mkBitVector(<int> size_or_str, + <int> val) + elif isinstance(size_or_str, str): + # handle default value + if val is None: + term.cterm = self.csolver.mkBitVector( + <const string &> size_or_str.encode()) + else: + term.cterm = self.csolver.mkBitVector( + <const string &> size_or_str.encode(), <int> val) + else: + raise ValueError("Unexpected inputs {} to" + " mkBitVector".format((size_or_str, val))) + return term + + def mkConstArray(self, Sort sort, Term val): + cdef Term term = Term() + term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm) + return term + + def mkPosInf(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkPosInf(exp, sig) + return term + + def mkNegInf(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkNegInf(exp, sig) + return term + + def mkNaN(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkNaN(exp, sig) + return term + + def mkPosZero(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkPosZero(exp, sig) + return term + + def mkNegZero(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkNegZero(exp, sig) + return term + + def mkRoundingMode(self, RoundingMode rm): + cdef Term term = Term() + term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm) + return term + + def mkUninterpretedConst(self, Sort sort, int index): + cdef Term term = Term() + term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index) + return term + + def mkAbstractValue(self, index): + cdef Term term = Term() + try: + term.cterm = self.csolver.mkAbstractValue(str(index).encode()) + except: + raise ValueError("mkAbstractValue expects a str representing a number" + " or an int, but got{}".format(index)) + return term + + def mkFloatingPoint(self, int exp, int sig, Term val): + cdef Term term = Term() + term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm) + return term + + def mkConst(self, Sort sort, symbol=None): + cdef Term term = Term() + if symbol is None: + term.cterm = self.csolver.mkConst(sort.csort) + else: + term.cterm = self.csolver.mkConst(sort.csort, + (<str?> symbol).encode()) + return term + + def mkVar(self, Sort sort, symbol=None): + cdef Term term = Term() + if symbol is None: + term.cterm = self.csolver.mkVar(sort.csort) + else: + term.cterm = self.csolver.mkVar(sort.csort, + (<str?> symbol).encode()) + return term + + def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None): + cdef DatatypeDecl dd = DatatypeDecl() + cdef vector[c_Sort] v + + # argument cases + if sorts_or_bool is None and isCoDatatype is None: + dd.cdd = self.csolver.mkDatatypeDecl(name.encode()) + elif sorts_or_bool is not None and isCoDatatype is None: + if isinstance(sorts_or_bool, bool): + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + <bint> sorts_or_bool) + elif isinstance(sorts_or_bool, Sort): + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + (<Sort> sorts_or_bool).csort) + elif isinstance(sorts_or_bool, list): + for s in sorts_or_bool: + v.push_back((<Sort?> s).csort) + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + <const vector[c_Sort]&> v) + else: + raise ValueError("Unhandled second argument type {}" + .format(type(sorts_or_bool))) + elif sorts_or_bool is not None and isCoDatatype is not None: + if isinstance(sorts_or_bool, Sort): + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + (<Sort> sorts_or_bool).csort, + <bint> isCoDatatype) + elif isinstance(sorts_or_bool, list): + for s in sorts_or_bool: + v.push_back((<Sort?> s).csort) + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + <const vector[c_Sort]&> v, + <bint> isCoDatatype) + else: + raise ValueError("Unhandled second argument type {}" + .format(type(sorts_or_bool))) + else: + raise ValueError("Can't create DatatypeDecl with {}".format([type(a) + for a in [name, + sorts_or_bool, + isCoDatatype]])) + + return dd + + def simplify(self, Term t): + cdef Term term = Term() + term.cterm = self.csolver.simplify(t.cterm) + return term + + def assertFormula(self, Term term): + 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) + + @expand_list_arg(num_req_args=0) + def checkSatAssuming(self, *assumptions): + ''' + Supports the following arguments: + Result checkSatAssuming(List[Term] assumptions) + + where assumptions can also be comma-separated arguments of + type (boolean) Term + ''' + cdef c_Result r + # 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) + + def checkValid(self): + cdef c_Result r = self.csolver.checkValid() + name = r.toString().decode() + explanation = "" + if r.isValidUnknown(): + explanation = r.getUnknownExplanation().decode() + return Result(name, explanation) + + @expand_list_arg(num_req_args=0) + def checkValidAssuming(self, *assumptions): + ''' + Supports the following arguments: + Result checkValidAssuming(List[Term] assumptions) + + where assumptions can also be comma-separated arguments of + type (boolean) Term + ''' + cdef c_Result r + # 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.checkValidAssuming(<const vector[c_Term]&> v) + name = r.toString().decode() + explanation = "" + if r.isValidUnknown(): + explanation = r.getUnknownExplanation().decode() + return Result(name, explanation) + + @expand_list_arg(num_req_args=1) + def declareDatatype(self, str symbol, *ctors): + ''' + Supports the following arguments: + Sort declareDatatype(str symbol, List[Term] ctors) + + where ctors can also be comma-separated arguments of + type DatatypeConstructorDecl + ''' + cdef Sort sort = Sort() + cdef vector[c_DatatypeConstructorDecl] v + + for c in ctors: + v.push_back((<DatatypeConstructorDecl?> c).cddc[0]) + sort.csort = self.csolver.declareDatatype(symbol.encode(), v) + return sort + + def declareFun(self, str symbol, list sorts, Sort sort): + cdef Term term = Term() + cdef vector[c_Sort] v + for s in sorts: + v.push_back((<Sort?> s).csort) + term.cterm = self.csolver.declareFun(symbol.encode(), + <const vector[c_Sort]&> v, + sort.csort) + return term + + def declareSort(self, str symbol, int arity): + cdef Sort sort = Sort() + sort.csort = self.csolver.declareSort(symbol.encode(), arity) + return sort + + def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None): + ''' + Supports two uses: + Term defineFun(str symbol, List[Term] bound_vars, + Sort sort, Term term) + Term defineFun(Term fun, List[Term] bound_vars, + Term term) + ''' + cdef Term term = Term() + cdef vector[c_Term] v + for bv in bound_vars: + v.push_back((<Term?> bv).cterm) + + if t is not None: + term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(), + <const vector[c_Term] &> v, + (<Sort?> sort_or_term).csort, + (<Term?> t).cterm) + else: + term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm, + <const vector[c_Term]&> v, + (<Term?> sort_or_term).cterm) + + return term + + def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None): + ''' + Supports two uses: + Term defineFunRec(str symbol, List[Term] bound_vars, + Sort sort, Term term) + Term defineFunRec(Term fun, List[Term] bound_vars, + Term term) + ''' + cdef Term term = Term() + cdef vector[c_Term] v + for bv in bound_vars: + v.push_back((<Term?> bv).cterm) + + if t is not None: + term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(), + <const vector[c_Term] &> v, + (<Sort?> sort_or_term).csort, + (<Term?> t).cterm) + else: + term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm, + <const vector[c_Term]&> v, + (<Term?> sort_or_term).cterm) + + return term + + def defineFunsRec(self, funs, bound_vars, terms): + cdef vector[c_Term] vf + cdef vector[vector[c_Term]] vbv + cdef vector[c_Term] vt + + for f in funs: + vf.push_back((<Term?> f).cterm) + + cdef vector[c_Term] temp + for v in bound_vars: + for t in v: + temp.push_back((<Term?> t).cterm) + vbv.push_back(temp) + temp.clear() + + for t in terms: + vf.push_back((<Term?> t).cterm) + + def getAssertions(self): + assertions = [] + for a in self.csolver.getAssertions(): + term = Term() + term.cterm = a + assertions.append(term) + return assertions + + def getAssignment(self): + ''' + Gives the assignment of *named* formulas as a dictionary. + ''' + assignments = {} + for a in self.csolver.getAssignment(): + varterm = Term() + valterm = Term() + varterm.cterm = a.first + valterm.cterm = a.second + assignments[varterm] = valterm + return assignments + + def getInfo(self, str flag): + return self.csolver.getInfo(flag.encode()) + + def getOption(self, str option): + return self.csolver.getOption(option.encode()) + + def getUnsatAssumptions(self): + assumptions = [] + for a in self.csolver.getUnsatAssumptions(): + term = Term() + term.cterm = a + assumptions.append(term) + return assumptions + + def getUnsatCore(self): + core = [] + for a in self.csolver.getUnsatCore(): + term = Term() + term.cterm = a + core.append(term) + return core + + def getValue(self, Term t): + cdef Term term = Term() + term.cterm = self.csolver.getValue(t.cterm) + return term + + def pop(self, nscopes=1): + self.csolver.pop(nscopes) + + def printModel(self): + self.csolver.printModel(cout) + + def push(self, nscopes=1): + self.csolver.push(nscopes) + + def reset(self): + self.csolver.reset() + + def resetAssertions(self): + self.csolver.resetAssertions() + + def setInfo(self, str keyword, str value): + self.csolver.setInfo(keyword.encode(), value.encode()) + + def setLogic(self, str logic): + self.csolver.setLogic(logic.encode()) + + def setOption(self, str option, str value): + self.csolver.setOption(option.encode(), value.encode()) + + +cdef class Sort: + cdef c_Sort csort + def __cinit__(self): + # csort always set by Solver + pass + + def __eq__(self, Sort other): + return self.csort == other.csort + + def __ne__(self, Sort other): + return self.csort != other.csort + + def __str__(self): + return self.csort.toString().decode() + + def __repr__(self): + return self.csort.toString().decode() + + def isBoolean(self): + return self.csort.isBoolean() + + def isInteger(self): + return self.csort.isInteger() + + def isReal(self): + return self.csort.isReal() + + def isString(self): + return self.csort.isString() + + def isRegExp(self): + return self.csort.isRegExp() + + def isRoundingMode(self): + return self.csort.isRoundingMode() + + def isBitVector(self): + return self.csort.isBitVector() + + def isFloatingPoint(self): + return self.csort.isFloatingPoint() + + def isDatatype(self): + return self.csort.isDatatype() + + def isParametricDatatype(self): + return self.csort.isParametricDatatype() + + def isFunction(self): + return self.csort.isFunction() + + def isPredicate(self): + return self.csort.isPredicate() + + def isTuple(self): + return self.csort.isTuple() + + def isRecord(self): + return self.csort.isRecord() + + def isArray(self): + return self.csort.isArray() + + def isSet(self): + return self.csort.isSet() + + def isUninterpretedSort(self): + return self.csort.isUninterpretedSort() + + def isSortConstructor(self): + return self.csort.isSortConstructor() + + def isFirstClass(self): + return self.csort.isFirstClass() + + def isFunctionLike(self): + return self.csort.isFunctionLike() + + def getDatatype(self): + cdef Datatype d = Datatype() + d.cd = self.csort.getDatatype() + return d + + def instantiate(self, params): + cdef Sort sort = Sort() + cdef vector[c_Sort] v + for s in params: + v.push_back((<Sort?> s).csort) + sort.csort = self.csort.instantiate(v) + return sort + + def isUninterpretedSortParameterized(self): + return self.csort.isUninterpretedSortParameterized() + + +cdef class Term: + cdef c_Term cterm + def __cinit__(self): + # cterm always set in the Solver object + pass + + def __eq__(self, Term other): + return self.cterm == other.cterm + + def __ne__(self, Term other): + return self.cterm != other.cterm + + def __str__(self): + return self.cterm.toString().decode() + + def __repr__(self): + return self.cterm.toString().decode() + + def __iter__(self): + for ci in self.cterm: + term = Term() + term.cterm = ci + yield term + + def getKind(self): + return kind(<int> self.cterm.getKind()) + + def getSort(self): + cdef Sort sort = Sort() + sort.csort = self.cterm.getSort() + return sort + + def hasOp(self): + return self.cterm.hasOp() + + def getOp(self): + cdef Op op = Op() + op.cop = self.cterm.getOp() + return op + + def isNull(self): + return self.cterm.isNull() + + def notTerm(self): + cdef Term term = Term() + term.cterm = self.cterm.notTerm() + return term + + def andTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.andTerm((<Term> t).cterm) + return term + + def orTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.orTerm(t.cterm) + return term + + def xorTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.xorTerm(t.cterm) + return term + + def eqTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.eqTerm(t.cterm) + return term + + def impTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.impTerm(t.cterm) + return term + + def iteTerm(self, Term then_t, Term else_t): + cdef Term term = Term() + term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm) + return term + + +# Generate rounding modes +cdef __rounding_modes = { + <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven", + <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive", + <int> ROUND_TOWARD_ZERO: "RoundTowardZero", + <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway" +} + +mod_ref = sys.modules[__name__] +for rm_int, name in __rounding_modes.items(): + r = RoundingMode(rm_int) + + if name in dir(mod_ref): + raise RuntimeError("Redefinition of Python RoundingMode %s."%name) + + setattr(mod_ref, name, r) + +del r +del rm_int +del name diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py new file mode 100755 index 000000000..1e22875e7 --- /dev/null +++ b/src/api/python/genkinds.py @@ -0,0 +1,255 @@ +#!/usr/bin/env python +""" +This script reads CVC4/src/api/cvc4cppkind.h and generates +.pxd and .pxi files which declare all the CVC4 kinds and +implement a Python wrapper for kinds, respectively. The +default names are kinds.pxd / kinds.pxi, but the name is +configurable from the command line with --kinds-file-prefix. + +The script is aware of the '#if 0' pattern and will ignore +kinds declared between '#if 0' and '#endif'. It can also +handle nested '#if 0' pairs. +""" + +import argparse +from collections import OrderedDict + +#################### Default Filenames ################ +DEFAULT_HEADER = 'cvc4cppkind.h' +DEFAULT_PREFIX = 'kinds' + +##################### Useful Constants ################ +OCB = '{' +CCB = '}' +SC = ';' +EQ = '=' +C = ',' +US = '_' +NL = '\n' + +#################### Enum Declarations ################ +ENUM_START = 'enum CVC4_PUBLIC Kind' +ENUM_END = CCB+SC + +################ Comments and Macro Tokens ############ +PYCOMMENT = '#' +COMMENT = '//' +BLOCK_COMMENT_BEGIN = '/*' +BLOCK_COMMENT_END = '*/' +MACRO_BLOCK_BEGIN = '#if 0' +MACRO_BLOCK_END = '#endif' + +#################### Format Kind Names ################ +# special cases for format_name +_IS = '_IS' +# replacements after some preprocessing +replacements = { + 'Bitvector' : 'BV', + 'Floatingpoint': 'FP' +} + +####################### Code Blocks ################### +CDEF_KIND = " cdef Kind " + +KINDS_PXD_TOP = \ +r"""cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api": + cdef cppclass Kind: + pass + + +# Kind declarations: See cvc4cppkind.h for additional information +cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api::Kind": +""" + +KINDS_PXI_TOP = \ +r"""# distutils: language = c++ +# distutils: extra_compile_args = -std=c++11 + +from cvc4kinds cimport * +import sys +from types import ModuleType + +cdef class kind: + cdef Kind k + cdef str name + def __cinit__(self, str name): + self.name = name + + def __eq__(self, kind other): + return (<int> self.k) == (<int> other.k) + + def __ne__(self, kind other): + return (<int> self.k) != (<int> other.k) + + def __hash__(self): + return hash((<int> self.k, self.name)) + + def __str__(self): + return self.name + + def __repr__(self): + return self.name + + def as_int(self): + return <int> self.k + +# create a kinds submodule +kinds = ModuleType('kinds') +# fake a submodule for dotted imports, e.g. from pycvc4.kinds import * +sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds +kinds.__file__ = kinds.__name__ + ".py" +""" + +KINDS_ATTR_TEMPLATE = \ +r""" +cdef kind {name} = kind("{name}") +{name}.k = {kind} +setattr(kinds, "{name}", {name}) +""" + +class KindsParser: + tokenmap = { + BLOCK_COMMENT_BEGIN : BLOCK_COMMENT_END, + MACRO_BLOCK_BEGIN : MACRO_BLOCK_END + } + + def __init__(self): + self.kinds = OrderedDict() + self.endtoken = None + self.endtoken_stack = [] + self.in_kinds = False + + def format_name(self, name): + ''' + In the Python API, each Kind name is reformatted for easier use + + The naming scheme is: + 1. capitalize the first letter of each word (delimited by underscores) + 2. make the rest of the letters lowercase + 3. replace Floatingpoint with FP + 4. replace Bitvector with BV + + There is one exception: + FLOATINGPOINT_ISNAN --> FPIsNan + + For every "_IS" in the name, there's an underscore added before step 1, + so that the word after "Is" is capitalized + + Examples: + BITVECTOR_PLUS --> BVPlus + APPLY_SELECTOR --> ApplySelector + FLOATINGPOINT_ISNAN --> FPIsNan + SETMINUS --> Setminus + + See the generated .pxi file for an explicit mapping + ''' + name = name.replace(_IS, _IS+US) + words = [w.capitalize() for w in name.lower().split(US)] + name = "".join(words) + + for og, new in replacements.items(): + name = name.replace(og, new) + + return name + + def ignore_block(self, line): + ''' + Returns a boolean telling self.parse whether to ignore a line or not. + It also updates all the necessary state to track comments and macro + blocks + ''' + + # check if entering block comment or macro block + for token in self.tokenmap: + if token in line: + if self.tokenmap[token] not in line: + if self.endtoken is not None: + self.endtoken_stack.append(self.endtoken) + self.endtoken = self.tokenmap[token] + return True + + # check if currently in block comment or macro block + if self.endtoken is not None: + # check if reached the end of block comment or macro block + if self.endtoken in line: + if self.endtoken_stack: + self.endtoken = self.endtoken_stack.pop() + else: + self.endtoken =None + return True + + return False + + def parse(self, filename): + f = open(filename, "r") + + for line in f.read().split(NL): + line = line.strip() + if COMMENT in line: + line = line[:line.find(COMMENT)] + if not line: + continue + + if self.ignore_block(line): + continue + + if ENUM_END in line: + self.in_kinds = False + break + elif self.in_kinds: + if line == OCB: + continue + if EQ in line: + line = line[:line.find(EQ)].strip() + elif C in line: + line = line[:line.find(C)].strip() + self.kinds[line] = self.format_name(line) + elif ENUM_START in line: + self.in_kinds = True + continue + + f.close() + + def gen_pxd(self, filename): + f = open(filename, "w") + f.write(KINDS_PXD_TOP) + # include the format_name docstring in the generated file + # could be helpful for users to see the formatting rules + for line in self.format_name.__doc__.split(NL): + f.write(PYCOMMENT) + if not line.isspace(): + f.write(line) + f.write(NL) + for kind in self.kinds: + f.write(CDEF_KIND + kind + NL) + f.close() + + def gen_pxi(self, filename): + f = open(filename, "w") + pxi = KINDS_PXI_TOP + for kind, name in self.kinds.items(): + pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) + f.write(pxi) + f.close() + + +if __name__ == "__main__": + parser = argparse.ArgumentParser('Read a kinds header file and generate a ' + 'corresponding pxd file, with simplified kind names.') + parser.add_argument('--kinds-header', metavar='<KINDS_HEADER>', + help='The header file to read kinds from', + default=DEFAULT_HEADER) + parser.add_argument('--kinds-file-prefix', metavar='<KIND_FILE_PREFIX>', + help='The prefix for the .pxd and .pxi files to write ' + 'the Cython declarations to.', + default=DEFAULT_PREFIX) + + args = parser.parse_args() + kinds_header = args.kinds_header + kinds_file_prefix = args.kinds_file_prefix + + kp = KindsParser() + kp.parse(kinds_header) + + kp.gen_pxd(kinds_file_prefix + ".pxd") + kp.gen_pxi(kinds_file_prefix + ".pxi") diff --git a/src/api/python/pycvc4.pyx b/src/api/python/pycvc4.pyx new file mode 100644 index 000000000..40766341a --- /dev/null +++ b/src/api/python/pycvc4.pyx @@ -0,0 +1,2 @@ +include "cvc4kinds.pxi" +include "cvc4.pxi" |