diff options
Diffstat (limited to 'src/api/python')
| -rw-r--r-- | src/api/python/CMakeLists.txt | 16 | ||||
| -rw-r--r-- | src/api/python/cvc5.pxd | 7 | ||||
| -rw-r--r-- | src/api/python/cvc5.pxi | 45 |
3 files changed, 33 insertions, 35 deletions
diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 74d1d84fc..96fcd67a0 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -95,13 +95,25 @@ target_include_directories(pycvc5 target_link_libraries(pycvc5 cvc5-shared) # Disable -Werror and other warnings for code generated by Cython. +set(PY_SRC_FLAGS "") +check_cxx_compiler_flag("-Werror" HAVE_CXX_FLAGWerror) +if(HAVE_CXX_FLAGWerror) + set(PY_SRC_FLAGS "${PY_SRC_FLAGS} -Wno-error") +endif() +check_cxx_compiler_flag("-Wshadow" HAVE_CXX_FLAGWshadow) +if(HAVE_CXX_FLAGWshadow) + set(PY_SRC_FLAGS "${PY_SRC_FLAGS} -Wno-shadow") +endif() +check_cxx_compiler_flag("-Wimplicit-fallthrough" HAVE_CXX_FLAGWimplicit_fallthrough) +if(HAVE_CXX_FLAGWimplicit_fallthrough) + set(PY_SRC_FLAGS "${PY_SRC_FLAGS} -Wno-implicit-fallthrough") +endif() # Note: Visibility is reset to default here since otherwise the PyInit_... # function will not be exported correctly # (https://github.com/cython/cython/issues/3380). set_target_properties(pycvc5 PROPERTIES - COMPILE_FLAGS - "-Wno-error -Wno-shadow -Wno-implicit-fallthrough" + COMPILE_FLAGS "${PY_SRC_FLAGS}" CXX_VISIBILITY_PRESET default VISIBILITY_INLINES_HIDDEN 0 LIBRARY_OUTPUT_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/pycvc5") diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 42aee08b0..a2c238985 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -266,7 +266,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort declareSort(const string& symbol, uint32_t arity) except + Term defineFun(const string& symbol, const vector[Term]& bound_vars, Sort sort, Term term, bint glbl) except + - Term defineFun(Term fun, const vector[Term]& bound_vars, Term term, bint glbl) except + Term defineFunRec(const string& symbol, const vector[Term]& bound_vars, Sort sort, Term term, bint glbl) except + Term defineFunRec(Term fun, const vector[Term]& bound_vars, @@ -282,9 +281,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": vector[Term] getValue(const vector[Term]& terms) except + vector[Term] getModelDomainElements(Sort sort) except + bint isModelCoreSymbol(Term v) except + - void declareSeparationHeap(Sort locSort, Sort dataSort) except + - Term getSeparationHeap() except + - Term getSeparationNilTerm() except + + void declareSepHeap(Sort locSort, Sort dataSort) except + + Term getValueSepHeap() except + + Term getValueSepNil() except + Term declarePool(const string& name, Sort sort, vector[Term]& initValue) except + void pop(uint32_t nscopes) except + void push(uint32_t nscopes) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 3367bf47b..05138e9bc 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1811,14 +1811,8 @@ cdef class Solver: sort.csort = self.csolver.declareSort(symbol.encode(), arity) return sort - def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False): - """ - Define n-ary function. - Supports two uses: - - - ``Term defineFun(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)`` - - ``Term defineFun(Term fun, List[Term] bound_vars, Term term, bool glbl)`` - + def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False): + """Define n-ary function. SMT-LIB: @@ -1830,27 +1824,20 @@ cdef class Solver: :param bound_vars: the parameters to this function :param sort: the sort of the return value of this function :param term: the function body - :param global: determines whether this definition is global (i.e. persists when popping the context) + :param glbl: determines whether this definition is global (i.e. persists when popping the context) :return: the function """ - cdef Term term = Term(self) + cdef Term fun = Term(self) 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, - <bint> glbl) - else: - term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm, - <const vector[c_Term]&> v, - (<Term?> sort_or_term).cterm, - <bint> glbl) - - return term + fun.cterm = self.csolver.defineFun(symbol.encode(), + <const vector[c_Term] &> v, + sort.csort, + term.cterm, + <bint> glbl) + return fun def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False): """Define recursive functions. @@ -2060,25 +2047,25 @@ cdef class Solver: """ return self.csolver.isModelCoreSymbol(v.cterm) - def getSeparationHeap(self): + def getValueSepHeap(self): """When using separation logic, obtain the term for the heap. :return: The term for the heap """ cdef Term term = Term(self) - term.cterm = self.csolver.getSeparationHeap() + term.cterm = self.csolver.getValueSepHeap() return term - def getSeparationNilTerm(self): + def getValueSepNil(self): """When using separation logic, obtain the term for nil. :return: The term for nil """ cdef Term term = Term(self) - term.cterm = self.csolver.getSeparationNilTerm() + term.cterm = self.csolver.getValueSepNil() return term - def declareSeparationHeap(self, Sort locType, Sort dataType): + def declareSepHeap(self, Sort locType, Sort dataType): """ When using separation logic, this sets the location sort and the datatype sort to the given ones. This method should be invoked exactly @@ -2087,7 +2074,7 @@ cdef class Solver: :param locSort: The location sort of the heap :param dataSort: The data sort of the heap """ - self.csolver.declareSeparationHeap(locType.csort, dataType.csort) + self.csolver.declareSepHeap(locType.csort, dataType.csort) def declarePool(self, str symbol, Sort sort, initValue): """Declare a symbolic pool of terms with the given initial value. |