diff options
Diffstat (limited to 'src/api/python/cvc4.pxd')
-rw-r--r-- | src/api/python/cvc4.pxd | 73 |
1 files changed, 66 insertions, 7 deletions
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index d81d0c0bf..940922052 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -21,6 +21,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4": cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass Datatype: Datatype() except + + DatatypeConstructor operator[](size_t idx) except + DatatypeConstructor operator[](const string& name) except + DatatypeConstructor getConstructor(const string& name) except + Term getConstructorTerm(const string& name) except + @@ -39,7 +40,12 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass DatatypeConstructor: DatatypeConstructor() except + + DatatypeSelector operator[](size_t idx) except + DatatypeSelector operator[](const string& name) except + + string getName() except + + Term getConstructorTerm() except + + Term getTesterTerm() except + + size_t getNumSelectors() except + DatatypeSelector getSelector(const string& name) except + Term getSelectorTerm(const string& name) except + string toString() except + @@ -54,7 +60,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass DatatypeConstructorDecl: - DatatypeConstructorDecl(const string& name) except + void addSelector(const string& name, Sort sort) except + void addSelectorSelf(const string& name) except + string toString() except + @@ -62,12 +67,16 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass DatatypeDecl: void addConstructor(const DatatypeConstructorDecl& ctor) except + + size_t getNumConstructors() except + bint isParametric() except + string toString() except + cdef cppclass DatatypeSelector: DatatypeSelector() except + + string getName() except + + Term getSelectorTerm() except + + Sort getRangeSort() except + string toString() except + @@ -81,15 +90,22 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": T getIndices[T]() except + string toString() except + + cdef cppclass OpHashFunction: + OpHashFunction() except + + size_t operator()(const Op & o) except + + 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 + @@ -156,6 +172,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": # default value for symbol defined in cvc4cpp.h Term mkConst(Sort sort) except + Term mkVar(Sort sort, const string& symbol) except + + DatatypeConstructorDecl mkDatatypeConstructorDecl(const string& name) except + DatatypeDecl mkDatatypeDecl(const string& name) except + DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except + DatatypeDecl mkDatatypeDecl(const string& name, Sort param) except + @@ -174,14 +191,14 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": 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 + + 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) except + + Sort sort, Term term, bint glbl) except + Term defineFunRec(Term fun, const vector[Term]& bound_vars, - Term term) except + + Term term, bint glbl) except + Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars, - vector[Term]& terms) except + + vector[Term]& terms, bint glbl) except + vector[Term] getAssertions() except + vector[pair[Term, Term]] getAssignment() except + string getInfo(const string& flag) except + @@ -190,6 +207,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": vector[Term] getUnsatCore() except + Term getValue(Term term) except + vector[Term] getValue(const vector[Term]& terms) except + + Term getSeparationHeap() except + + Term getSeparationNilTerm() except + void pop(uint32_t nscopes) except + void printModel(ostream& out) void push(uint32_t nscopes) except + @@ -204,6 +223,10 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Sort() except + bint operator==(const Sort&) except + bint operator!=(const Sort&) except + + bint operator<(const Sort&) except + + bint operator>(const Sort&) except + + bint operator<=(const Sort&) except + + bint operator>=(const Sort&) except + bint isBoolean() except + bint isInteger() except + bint isReal() except + @@ -214,6 +237,9 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": bint isFloatingPoint() except + bint isDatatype() except + bint isParametricDatatype() except + + bint isConstructor() except + + bint isSelector() except + + bint isTester() except + bint isFunction() except + bint isPredicate() except + bint isTuple() except + @@ -224,20 +250,49 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": bint isSortConstructor() except + bint isFirstClass() except + bint isFunctionLike() except + + bint isSubsortOf(Sort s) except + + bint isComparableTo(Sort s) except + Datatype getDatatype() except + Sort instantiate(const vector[Sort]& params) except + + size_t getConstructorArity() except + + vector[Sort] getConstructorDomainSorts() except + + Sort getConstructorCodomainSort() except + + size_t getFunctionArity() except + + vector[Sort] getFunctionDomainSorts() except + + Sort getFunctionCodomainSort() except + + Sort getArrayIndexSort() except + + Sort getArrayElementSort() except + + Sort getSetElementSort() except + + string getUninterpretedSortName() except + bint isUninterpretedSortParameterized() except + + vector[Sort] getUninterpretedSortParamSorts() except + + string getSortConstructorName() except + + size_t getSortConstructorArity() except + + uint32_t getBVSize() except + + uint32_t getFPExponentSize() except + + uint32_t getFPSignificandSize() except + + vector[Sort] getDatatypeParamSorts() except + + size_t getDatatypeArity() except + + size_t getTupleLength() except + + vector[Sort] getTupleSorts() except + string toString() except + + cdef cppclass SortHashFunction: + SortHashFunction() except + + size_t operator()(const Sort & s) except + + cdef cppclass Term: Term() bint operator==(const Term&) except + bint operator!=(const Term&) except + Kind getKind() except + Sort getSort() except + + Term substitute(const vector[Term] es, const vector[Term] & reps) except + bint hasOp() except + Op getOp() except + bint isNull() except + + bint isConst() except + + Term getConstArrayBase() except + Term notTerm() except + Term andTerm(const Term& t) except + Term orTerm(const Term& t) except + @@ -255,6 +310,10 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": const_iterator begin() except + const_iterator end() except + + cdef cppclass TermHashFunction: + TermHashFunction() except + + size_t operator()(const Term & t) except + + cdef extern from "api/cvc4cpp.h" namespace "CVC4::api::RoundingMode": cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN, |