CVC3
2.4.1
|
This is the complete list of members for CVC3::VCL, including all inherited members.
addPairToArithOrder(const Expr &smaller, const Expr &bigger) | CVC3::VCL | virtual |
andExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
andExpr(const std::vector< Expr > &children) | CVC3::VCL | virtual |
arrayType(const Type &typeIndex, const Type &typeData) | CVC3::VCL | virtual |
assertFormula(const Expr &e) | CVC3::VCL | virtual |
bitvecType(int n) | CVC3::VCL | virtual |
boolType() | CVC3::VCL | virtual |
boundVarExpr(const std::string &name, const std::string &uid, const Type &type) | CVC3::VCL | virtual |
checkContinue() | CVC3::VCL | virtual |
checkTCC(const Expr &tcc) | CVC3::VCL | private |
checkUnsat(const Expr &e) | CVC3::VCL | virtual |
cmdsFromString(const std::string &s, InputLanguage lang) | CVC3::VCL | virtual |
computeBVConst(const Expr &e) | CVC3::VCL | virtual |
core() | CVC3::VCL | |
create(const CLFlags &flags) | CVC3::ValidityChecker | static |
create() | CVC3::ValidityChecker | static |
createFlags() | CVC3::ValidityChecker | static |
createOp(const std::string &name, const Type &type) | CVC3::VCL | virtual |
createOp(const std::string &name, const Type &type, const Expr &def) | CVC3::VCL | virtual |
createType(const std::string &typeName) | CVC3::VCL | virtual |
createType(const std::string &typeName, const Type &def) | CVC3::VCL | virtual |
d_batchedAssertions | CVC3::VCL | private |
d_batchedAssertionsIdx | CVC3::VCL | private |
d_cm | CVC3::VCL | private |
d_dump | CVC3::VCL | private |
d_em | CVC3::VCL | private |
d_flags | CVC3::VCL | private |
d_lastClosure | CVC3::VCL | private |
d_lastQuery | CVC3::VCL | private |
d_lastQueryTCC | CVC3::VCL | private |
d_modelStackPushed | CVC3::VCL | private |
d_nextIdx | CVC3::VCL | private |
d_se | CVC3::VCL | private |
d_stackLevel | CVC3::VCL | private |
d_statistics | CVC3::VCL | private |
d_theories | CVC3::VCL | private |
d_theoryArith | CVC3::VCL | private |
d_theoryArray | CVC3::VCL | private |
d_theoryBitvector | CVC3::VCL | private |
d_theoryCore | CVC3::VCL | private |
d_theoryDatatype | CVC3::VCL | private |
d_theoryQuant | CVC3::VCL | private |
d_theoryRecords | CVC3::VCL | private |
d_theorySimulate | CVC3::VCL | private |
d_theoryUF | CVC3::VCL | private |
d_tm | CVC3::VCL | private |
d_translator | CVC3::VCL | private |
d_userAssertions | CVC3::VCL | private |
dataType(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types) | CVC3::VCL | virtual |
dataType(const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types) | CVC3::VCL | virtual |
dataType(const std::vector< std::string > &names, const std::vector< std::vector< std::string > > &constructors, const std::vector< std::vector< std::vector< std::string > > > &selectors, const std::vector< std::vector< std::vector< Expr > > > &types, std::vector< Type > &returnTypes) | CVC3::VCL | virtual |
datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args) | CVC3::VCL | virtual |
datatypeSelExpr(const std::string &selector, const Expr &arg) | CVC3::VCL | virtual |
datatypeTestExpr(const std::string &constructor, const Expr &arg) | CVC3::VCL | virtual |
deriveClosure(const Theorem3 &thm) | CVC3::VCL | private |
destroy(void) | CVC3::VCL | private |
distinctExpr(const std::vector< Expr > &children) | CVC3::VCL | virtual |
divideExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
eqExpr(const Expr &child0, const Expr &child1) | CVC3::VCL | virtual |
existsExpr(const std::vector< Expr > &vars, const Expr &body) | CVC3::VCL | virtual |
exprFromString(const std::string &s) | CVC3::VCL | virtual |
falseExpr() | CVC3::VCL | virtual |
forallExpr(const std::vector< Expr > &vars, const Expr &body) | CVC3::VCL | virtual |
forallExpr(const std::vector< Expr > &vars, const Expr &body, const Expr &trigger) | CVC3::VCL | virtual |
forallExpr(const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers) | CVC3::VCL | virtual |
forallExpr(const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers) | CVC3::VCL | virtual |
funExpr(const Op &op, const Expr &child) | CVC3::VCL | virtual |
funExpr(const Op &op, const Expr &left, const Expr &right) | CVC3::VCL | virtual |
funExpr(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2) | CVC3::VCL | virtual |
funExpr(const Op &op, const std::vector< Expr > &children) | CVC3::VCL | virtual |
funType(const Type &typeDom, const Type &typeRan) | CVC3::VCL | virtual |
funType(const std::vector< Type > &typeDom, const Type &typeRan) | CVC3::VCL | virtual |
geExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
getAssignment() | CVC3::VCL | virtual |
getAssumptions(const Assumptions &a, std::vector< Expr > &assumptions) | CVC3::VCL | private |
getAssumptions(std::vector< Expr > &assumptions) | CVC3::VCL | virtual |
getAssumptionsRec(const Theorem &thm, std::set< UserAssertion > &assumptions, bool addTCCs) | CVC3::VCL | private |
getAssumptionsTCC(std::vector< Expr > &assumptions) | CVC3::VCL | virtual |
getAssumptionsUsed(std::vector< Expr > &assumptions) | CVC3::VCL | virtual |
getBaseType(const Expr &e) | CVC3::VCL | virtual |
getBaseType(const Type &e) | CVC3::VCL | virtual |
getClosure() | CVC3::VCL | virtual |
getConcreteModel(ExprMap< Expr > &m) | CVC3::VCL | virtual |
getCounterExample(std::vector< Expr > &assumptions, bool inOrder) | CVC3::VCL | virtual |
getCurrentContext() | CVC3::VCL | virtual |
getEM() | CVC3::VCL | inlinevirtual |
getFlags() const | CVC3::VCL | inlinevirtual |
getImpliedLiteral() | CVC3::VCL | virtual |
getInternalAssumptions(std::vector< Expr > &assumptions) | CVC3::VCL | virtual |
getMemory(int verbosity=0) | CVC3::VCL | |
getProof() | CVC3::VCL | virtual |
getProofClosure() | CVC3::VCL | virtual |
getProofQuery() | CVC3::VCL | virtual |
getProofTCC() | CVC3::VCL | virtual |
getStatistics() | CVC3::VCL | inlinevirtual |
getTCC() | CVC3::VCL | virtual |
getType(const Expr &e) | CVC3::VCL | virtual |
getTypePred(const Type &t, const Expr &e) | CVC3::VCL | virtual |
getUserAssumptions(std::vector< Expr > &assumptions) | CVC3::VCL | virtual |
getValue(Expr e) | CVC3::VCL | virtual |
gtExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
idExpr(const std::string &name) | CVC3::VCL | virtual |
iffExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
impliesExpr(const Expr &hyp, const Expr &conc) | CVC3::VCL | virtual |
importExpr(const Expr &e) | CVC3::VCL | virtual |
importType(const Type &t) | CVC3::VCL | virtual |
incomplete() | CVC3::VCL | virtual |
incomplete(std::vector< std::string > &reasons) | CVC3::VCL | virtual |
inconsistent(std::vector< Expr > &assumptions) | CVC3::VCL | virtual |
inconsistent() | CVC3::VCL | virtual |
init(void) | CVC3::VCL | private |
intType() | CVC3::VCL | virtual |
iteExpr(const Expr &ifpart, const Expr &thenpart, const Expr &elsepart) | CVC3::VCL | virtual |
lambdaExpr(const std::vector< Expr > &vars, const Expr &body) | CVC3::VCL | virtual |
leExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
listExpr(const std::vector< Expr > &kids) | CVC3::VCL | virtual |
listExpr(const Expr &e1) | CVC3::VCL | virtual |
listExpr(const Expr &e1, const Expr &e2) | CVC3::VCL | virtual |
listExpr(const Expr &e1, const Expr &e2, const Expr &e3) | CVC3::VCL | virtual |
listExpr(const std::string &op, const std::vector< Expr > &kids) | CVC3::VCL | virtual |
listExpr(const std::string &op, const Expr &e1) | CVC3::VCL | virtual |
listExpr(const std::string &op, const Expr &e1, const Expr &e2) | CVC3::VCL | virtual |
listExpr(const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3) | CVC3::VCL | virtual |
loadFile(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false) | CVC3::VCL | virtual |
loadFile(std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false) | CVC3::VCL | virtual |
logAnnotation(const Expr &annot) | CVC3::VCL | virtual |
lookupOp(const std::string &name, Type *type) | CVC3::VCL | virtual |
lookupType(const std::string &typeName) | CVC3::VCL | virtual |
lookupVar(const std::string &name, Type *type) | CVC3::VCL | virtual |
ltExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
minusExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
multExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
newBVAndExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVAndExpr(const std::vector< Expr > &kids) | CVC3::VCL | virtual |
newBVASHR(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVCompExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVConstExpr(const std::string &s, int base) | CVC3::VCL | virtual |
newBVConstExpr(const std::vector< bool > &bits) | CVC3::VCL | virtual |
newBVConstExpr(const Rational &r, int len) | CVC3::VCL | virtual |
newBVExtractExpr(const Expr &e, int hi, int low) | CVC3::VCL | virtual |
newBVLEExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVLSHR(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVLTExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVMultExpr(int numbits, const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVNandExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVNegExpr(const Expr &t1) | CVC3::VCL | virtual |
newBVNorExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVOrExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVOrExpr(const std::vector< Expr > &kids) | CVC3::VCL | virtual |
newBVPlusExpr(int numbits, const std::vector< Expr > &k) | CVC3::VCL | virtual |
newBVPlusExpr(int numbits, const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVSDivExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVSHL(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVSLEExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVSLTExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVSModExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVSRemExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVSubExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVUDivExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVUminusExpr(const Expr &t1) | CVC3::VCL | virtual |
newBVURemExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVXnorExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVXnorExpr(const std::vector< Expr > &kids) | CVC3::VCL | virtual |
newBVXorExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newBVXorExpr(const std::vector< Expr > &kids) | CVC3::VCL | virtual |
newConcatExpr(const Expr &t1, const Expr &t2) | CVC3::VCL | virtual |
newConcatExpr(const std::vector< Expr > &kids) | CVC3::VCL | virtual |
newFixedConstWidthLeftShiftExpr(const Expr &t1, int r) | CVC3::VCL | virtual |
newFixedLeftShiftExpr(const Expr &t1, int r) | CVC3::VCL | virtual |
newFixedRightShiftExpr(const Expr &t1, int r) | CVC3::VCL | virtual |
newSXExpr(const Expr &t1, int len) | CVC3::VCL | virtual |
notExpr(const Expr &child) | CVC3::VCL | virtual |
orExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
orExpr(const std::vector< Expr > &children) | CVC3::VCL | virtual |
parseExpr(const Expr &e) | CVC3::VCL | virtual |
parseType(const Expr &e) | CVC3::VCL | virtual |
plusExpr(const Expr &left, const Expr &right) | CVC3::VCL | virtual |
plusExpr(const std::vector< Expr > &children) | CVC3::VCL | virtual |
pop() | CVC3::VCL | virtual |
popScope() | CVC3::VCL | virtual |
popto(int stackLevel) | CVC3::VCL | virtual |
poptoScope(int scopeLevel) | CVC3::VCL | virtual |
powExpr(const Expr &x, const Expr &n) | CVC3::VCL | virtual |
printExpr(const Expr &e) | CVC3::VCL | virtual |
printExpr(const Expr &e, std::ostream &os) | CVC3::VCL | virtual |
printStatistics() | CVC3::VCL | inlinevirtual |
push() | CVC3::VCL | virtual |
pushScope() | CVC3::VCL | virtual |
query(const Expr &e) | CVC3::VCL | virtual |
ratExpr(int n, int d) | CVC3::VCL | virtual |
ratExpr(const std::string &n, const std::string &d, int base) | CVC3::VCL | virtual |
ratExpr(const std::string &n, int base) | CVC3::VCL | virtual |
readExpr(const Expr &array, const Expr &index) | CVC3::VCL | virtual |
realType() | CVC3::VCL | virtual |
recordExpr(const std::string &field, const Expr &expr) | CVC3::VCL | virtual |
recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1) | CVC3::VCL | virtual |
recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2) | CVC3::VCL | virtual |
recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &exprs) | CVC3::VCL | virtual |
recordType(const std::string &field, const Type &type) | CVC3::VCL | virtual |
recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1) | CVC3::VCL | virtual |
recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2) | CVC3::VCL | virtual |
recordType(const std::vector< std::string > &fields, const std::vector< Type > &types) | CVC3::VCL | virtual |
recSelectExpr(const Expr &record, const std::string &field) | CVC3::VCL | virtual |
recUpdateExpr(const Expr &record, const std::string &field, const Expr &newValue) | CVC3::VCL | virtual |
registerAtom(const Expr &e) | CVC3::VCL | virtual |
reprocessFlags() | CVC3::VCL | virtual |
reset() | CVC3::VCL | virtual |
restart(const Expr &e) | CVC3::VCL | virtual |
returnFromCheck() | CVC3::VCL | virtual |
scopeLevel() | CVC3::VCL | virtual |
setMultiTrigger(const Expr &e, const std::vector< Expr > &multiTrigger) | CVC3::VCL | virtual |
setResourceLimit(unsigned limit) | CVC3::VCL | virtual |
setTimeLimit(unsigned limit) | CVC3::VCL | virtual |
setTrigger(const Expr &e, const Expr &trigger) | CVC3::VCL | virtual |
setTriggers(const Expr &e, const std::vector< std::vector< Expr > > &triggers) | CVC3::VCL | virtual |
setTriggers(const Expr &e, const std::vector< Expr > &triggers) | CVC3::VCL | virtual |
simplify(const Expr &e) | CVC3::VCL | virtual |
simplifyThm(const Expr &e) | CVC3::VCL | |
simulateExpr(const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n) | CVC3::VCL | virtual |
stackLevel() | CVC3::VCL | virtual |
stringExpr(const std::string &str) | CVC3::VCL | virtual |
subrangeType(const Expr &l, const Expr &r) | CVC3::VCL | virtual |
subtypeType(const Expr &pred, const Expr &witness) | CVC3::VCL | virtual |
transClosure(const Op &op) | CVC3::VCL | virtual |
trueExpr() | CVC3::VCL | virtual |
tryModelGeneration() | CVC3::VCL | virtual |
tupleExpr(const std::vector< Expr > &exprs) | CVC3::VCL | virtual |
tupleSelectExpr(const Expr &tuple, int index) | CVC3::VCL | virtual |
tupleType(const Type &type0, const Type &type1) | CVC3::VCL | virtual |
tupleType(const Type &type0, const Type &type1, const Type &type2) | CVC3::VCL | virtual |
tupleType(const std::vector< Type > &types) | CVC3::VCL | virtual |
tupleUpdateExpr(const Expr &tuple, int index, const Expr &newValue) | CVC3::VCL | virtual |
uminusExpr(const Expr &child) | CVC3::VCL | virtual |
ValidityChecker() | CVC3::ValidityChecker | inline |
value(const Expr &e) | CVC3::VCL | virtual |
varExpr(const std::string &name, const Type &type) | CVC3::VCL | virtual |
varExpr(const std::string &name, const Type &type, const Expr &def) | CVC3::VCL | virtual |
VCL(const CLFlags &flags) | CVC3::VCL | |
writeExpr(const Expr &array, const Expr &index, const Expr &newValue) | CVC3::VCL | virtual |
~ValidityChecker() | CVC3::ValidityChecker | inlinevirtual |
~VCL() | CVC3::VCL |