summaryrefslogtreecommitdiff
path: root/src/api/python/cvc4.pxd
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/python/cvc4.pxd')
-rw-r--r--src/api/python/cvc4.pxd73
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback