CVC3
CVC3::VCL Member List

This is the complete list of members for CVC3::VCL, including all inherited members.

addPairToArithOrder(const Expr &smaller, const Expr &bigger)CVC3::VCLvirtual
andExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
andExpr(const std::vector< Expr > &children)CVC3::VCLvirtual
arrayType(const Type &typeIndex, const Type &typeData)CVC3::VCLvirtual
assertFormula(const Expr &e)CVC3::VCLvirtual
bitvecType(int n)CVC3::VCLvirtual
boolType()CVC3::VCLvirtual
boundVarExpr(const std::string &name, const std::string &uid, const Type &type)CVC3::VCLvirtual
checkContinue()CVC3::VCLvirtual
checkTCC(const Expr &tcc)CVC3::VCLprivate
checkUnsat(const Expr &e)CVC3::VCLvirtual
cmdsFromString(const std::string &s, InputLanguage lang)CVC3::VCLvirtual
computeBVConst(const Expr &e)CVC3::VCLvirtual
core()CVC3::VCL
create(const CLFlags &flags)CVC3::ValidityCheckerstatic
create()CVC3::ValidityCheckerstatic
createFlags()CVC3::ValidityCheckerstatic
createOp(const std::string &name, const Type &type)CVC3::VCLvirtual
createOp(const std::string &name, const Type &type, const Expr &def)CVC3::VCLvirtual
createType(const std::string &typeName)CVC3::VCLvirtual
createType(const std::string &typeName, const Type &def)CVC3::VCLvirtual
d_batchedAssertionsCVC3::VCLprivate
d_batchedAssertionsIdxCVC3::VCLprivate
d_cmCVC3::VCLprivate
d_dumpCVC3::VCLprivate
d_emCVC3::VCLprivate
d_flagsCVC3::VCLprivate
d_lastClosureCVC3::VCLprivate
d_lastQueryCVC3::VCLprivate
d_lastQueryTCCCVC3::VCLprivate
d_modelStackPushedCVC3::VCLprivate
d_nextIdxCVC3::VCLprivate
d_seCVC3::VCLprivate
d_stackLevelCVC3::VCLprivate
d_statisticsCVC3::VCLprivate
d_theoriesCVC3::VCLprivate
d_theoryArithCVC3::VCLprivate
d_theoryArrayCVC3::VCLprivate
d_theoryBitvectorCVC3::VCLprivate
d_theoryCoreCVC3::VCLprivate
d_theoryDatatypeCVC3::VCLprivate
d_theoryQuantCVC3::VCLprivate
d_theoryRecordsCVC3::VCLprivate
d_theorySimulateCVC3::VCLprivate
d_theoryUFCVC3::VCLprivate
d_tmCVC3::VCLprivate
d_translatorCVC3::VCLprivate
d_userAssertionsCVC3::VCLprivate
dataType(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types)CVC3::VCLvirtual
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::VCLvirtual
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::VCLvirtual
datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args)CVC3::VCLvirtual
datatypeSelExpr(const std::string &selector, const Expr &arg)CVC3::VCLvirtual
datatypeTestExpr(const std::string &constructor, const Expr &arg)CVC3::VCLvirtual
deriveClosure(const Theorem3 &thm)CVC3::VCLprivate
destroy(void)CVC3::VCLprivate
distinctExpr(const std::vector< Expr > &children)CVC3::VCLvirtual
divideExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
eqExpr(const Expr &child0, const Expr &child1)CVC3::VCLvirtual
existsExpr(const std::vector< Expr > &vars, const Expr &body)CVC3::VCLvirtual
exprFromString(const std::string &s)CVC3::VCLvirtual
falseExpr()CVC3::VCLvirtual
forallExpr(const std::vector< Expr > &vars, const Expr &body)CVC3::VCLvirtual
forallExpr(const std::vector< Expr > &vars, const Expr &body, const Expr &trigger)CVC3::VCLvirtual
forallExpr(const std::vector< Expr > &vars, const Expr &body, const std::vector< Expr > &triggers)CVC3::VCLvirtual
forallExpr(const std::vector< Expr > &vars, const Expr &body, const std::vector< std::vector< Expr > > &triggers)CVC3::VCLvirtual
funExpr(const Op &op, const Expr &child)CVC3::VCLvirtual
funExpr(const Op &op, const Expr &left, const Expr &right)CVC3::VCLvirtual
funExpr(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)CVC3::VCLvirtual
funExpr(const Op &op, const std::vector< Expr > &children)CVC3::VCLvirtual
funType(const Type &typeDom, const Type &typeRan)CVC3::VCLvirtual
funType(const std::vector< Type > &typeDom, const Type &typeRan)CVC3::VCLvirtual
geExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
getAssignment()CVC3::VCLvirtual
getAssumptions(const Assumptions &a, std::vector< Expr > &assumptions)CVC3::VCLprivate
getAssumptions(std::vector< Expr > &assumptions)CVC3::VCLvirtual
getAssumptionsRec(const Theorem &thm, std::set< UserAssertion > &assumptions, bool addTCCs)CVC3::VCLprivate
getAssumptionsTCC(std::vector< Expr > &assumptions)CVC3::VCLvirtual
getAssumptionsUsed(std::vector< Expr > &assumptions)CVC3::VCLvirtual
getBaseType(const Expr &e)CVC3::VCLvirtual
getBaseType(const Type &e)CVC3::VCLvirtual
getClosure()CVC3::VCLvirtual
getConcreteModel(ExprMap< Expr > &m)CVC3::VCLvirtual
getCounterExample(std::vector< Expr > &assumptions, bool inOrder)CVC3::VCLvirtual
getCurrentContext()CVC3::VCLvirtual
getEM()CVC3::VCLinlinevirtual
getFlags() const CVC3::VCLinlinevirtual
getImpliedLiteral()CVC3::VCLvirtual
getInternalAssumptions(std::vector< Expr > &assumptions)CVC3::VCLvirtual
getMemory(int verbosity=0)CVC3::VCL
getProof()CVC3::VCLvirtual
getProofClosure()CVC3::VCLvirtual
getProofQuery()CVC3::VCLvirtual
getProofTCC()CVC3::VCLvirtual
getStatistics()CVC3::VCLinlinevirtual
getTCC()CVC3::VCLvirtual
getType(const Expr &e)CVC3::VCLvirtual
getTypePred(const Type &t, const Expr &e)CVC3::VCLvirtual
getUserAssumptions(std::vector< Expr > &assumptions)CVC3::VCLvirtual
getValue(Expr e)CVC3::VCLvirtual
gtExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
idExpr(const std::string &name)CVC3::VCLvirtual
iffExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
impliesExpr(const Expr &hyp, const Expr &conc)CVC3::VCLvirtual
importExpr(const Expr &e)CVC3::VCLvirtual
importType(const Type &t)CVC3::VCLvirtual
incomplete()CVC3::VCLvirtual
incomplete(std::vector< std::string > &reasons)CVC3::VCLvirtual
inconsistent(std::vector< Expr > &assumptions)CVC3::VCLvirtual
inconsistent()CVC3::VCLvirtual
init(void)CVC3::VCLprivate
intType()CVC3::VCLvirtual
iteExpr(const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)CVC3::VCLvirtual
lambdaExpr(const std::vector< Expr > &vars, const Expr &body)CVC3::VCLvirtual
leExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
listExpr(const std::vector< Expr > &kids)CVC3::VCLvirtual
listExpr(const Expr &e1)CVC3::VCLvirtual
listExpr(const Expr &e1, const Expr &e2)CVC3::VCLvirtual
listExpr(const Expr &e1, const Expr &e2, const Expr &e3)CVC3::VCLvirtual
listExpr(const std::string &op, const std::vector< Expr > &kids)CVC3::VCLvirtual
listExpr(const std::string &op, const Expr &e1)CVC3::VCLvirtual
listExpr(const std::string &op, const Expr &e1, const Expr &e2)CVC3::VCLvirtual
listExpr(const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3)CVC3::VCLvirtual
loadFile(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false)CVC3::VCLvirtual
loadFile(std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)CVC3::VCLvirtual
logAnnotation(const Expr &annot)CVC3::VCLvirtual
lookupOp(const std::string &name, Type *type)CVC3::VCLvirtual
lookupType(const std::string &typeName)CVC3::VCLvirtual
lookupVar(const std::string &name, Type *type)CVC3::VCLvirtual
ltExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
minusExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
multExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
newBVAndExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVAndExpr(const std::vector< Expr > &kids)CVC3::VCLvirtual
newBVASHR(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVCompExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVConstExpr(const std::string &s, int base)CVC3::VCLvirtual
newBVConstExpr(const std::vector< bool > &bits)CVC3::VCLvirtual
newBVConstExpr(const Rational &r, int len)CVC3::VCLvirtual
newBVExtractExpr(const Expr &e, int hi, int low)CVC3::VCLvirtual
newBVLEExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVLSHR(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVLTExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVMultExpr(int numbits, const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVNandExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVNegExpr(const Expr &t1)CVC3::VCLvirtual
newBVNorExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVOrExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVOrExpr(const std::vector< Expr > &kids)CVC3::VCLvirtual
newBVPlusExpr(int numbits, const std::vector< Expr > &k)CVC3::VCLvirtual
newBVPlusExpr(int numbits, const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVSDivExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVSHL(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVSLEExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVSLTExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVSModExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVSRemExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVSubExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVUDivExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVUminusExpr(const Expr &t1)CVC3::VCLvirtual
newBVURemExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVXnorExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVXnorExpr(const std::vector< Expr > &kids)CVC3::VCLvirtual
newBVXorExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newBVXorExpr(const std::vector< Expr > &kids)CVC3::VCLvirtual
newConcatExpr(const Expr &t1, const Expr &t2)CVC3::VCLvirtual
newConcatExpr(const std::vector< Expr > &kids)CVC3::VCLvirtual
newFixedConstWidthLeftShiftExpr(const Expr &t1, int r)CVC3::VCLvirtual
newFixedLeftShiftExpr(const Expr &t1, int r)CVC3::VCLvirtual
newFixedRightShiftExpr(const Expr &t1, int r)CVC3::VCLvirtual
newSXExpr(const Expr &t1, int len)CVC3::VCLvirtual
notExpr(const Expr &child)CVC3::VCLvirtual
orExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
orExpr(const std::vector< Expr > &children)CVC3::VCLvirtual
parseExpr(const Expr &e)CVC3::VCLvirtual
parseType(const Expr &e)CVC3::VCLvirtual
plusExpr(const Expr &left, const Expr &right)CVC3::VCLvirtual
plusExpr(const std::vector< Expr > &children)CVC3::VCLvirtual
pop()CVC3::VCLvirtual
popScope()CVC3::VCLvirtual
popto(int stackLevel)CVC3::VCLvirtual
poptoScope(int scopeLevel)CVC3::VCLvirtual
powExpr(const Expr &x, const Expr &n)CVC3::VCLvirtual
printExpr(const Expr &e)CVC3::VCLvirtual
printExpr(const Expr &e, std::ostream &os)CVC3::VCLvirtual
printStatistics()CVC3::VCLinlinevirtual
push()CVC3::VCLvirtual
pushScope()CVC3::VCLvirtual
query(const Expr &e)CVC3::VCLvirtual
ratExpr(int n, int d)CVC3::VCLvirtual
ratExpr(const std::string &n, const std::string &d, int base)CVC3::VCLvirtual
ratExpr(const std::string &n, int base)CVC3::VCLvirtual
readExpr(const Expr &array, const Expr &index)CVC3::VCLvirtual
realType()CVC3::VCLvirtual
recordExpr(const std::string &field, const Expr &expr)CVC3::VCLvirtual
recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1)CVC3::VCLvirtual
recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2)CVC3::VCLvirtual
recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &exprs)CVC3::VCLvirtual
recordType(const std::string &field, const Type &type)CVC3::VCLvirtual
recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)CVC3::VCLvirtual
recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2)CVC3::VCLvirtual
recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)CVC3::VCLvirtual
recSelectExpr(const Expr &record, const std::string &field)CVC3::VCLvirtual
recUpdateExpr(const Expr &record, const std::string &field, const Expr &newValue)CVC3::VCLvirtual
registerAtom(const Expr &e)CVC3::VCLvirtual
reprocessFlags()CVC3::VCLvirtual
reset()CVC3::VCLvirtual
restart(const Expr &e)CVC3::VCLvirtual
returnFromCheck()CVC3::VCLvirtual
scopeLevel()CVC3::VCLvirtual
setMultiTrigger(const Expr &e, const std::vector< Expr > &multiTrigger)CVC3::VCLvirtual
setResourceLimit(unsigned limit)CVC3::VCLvirtual
setTimeLimit(unsigned limit)CVC3::VCLvirtual
setTrigger(const Expr &e, const Expr &trigger)CVC3::VCLvirtual
setTriggers(const Expr &e, const std::vector< std::vector< Expr > > &triggers)CVC3::VCLvirtual
setTriggers(const Expr &e, const std::vector< Expr > &triggers)CVC3::VCLvirtual
simplify(const Expr &e)CVC3::VCLvirtual
simplifyThm(const Expr &e)CVC3::VCL
simulateExpr(const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)CVC3::VCLvirtual
stackLevel()CVC3::VCLvirtual
stringExpr(const std::string &str)CVC3::VCLvirtual
subrangeType(const Expr &l, const Expr &r)CVC3::VCLvirtual
subtypeType(const Expr &pred, const Expr &witness)CVC3::VCLvirtual
transClosure(const Op &op)CVC3::VCLvirtual
trueExpr()CVC3::VCLvirtual
tryModelGeneration()CVC3::VCLvirtual
tupleExpr(const std::vector< Expr > &exprs)CVC3::VCLvirtual
tupleSelectExpr(const Expr &tuple, int index)CVC3::VCLvirtual
tupleType(const Type &type0, const Type &type1)CVC3::VCLvirtual
tupleType(const Type &type0, const Type &type1, const Type &type2)CVC3::VCLvirtual
tupleType(const std::vector< Type > &types)CVC3::VCLvirtual
tupleUpdateExpr(const Expr &tuple, int index, const Expr &newValue)CVC3::VCLvirtual
uminusExpr(const Expr &child)CVC3::VCLvirtual
ValidityChecker()CVC3::ValidityCheckerinline
value(const Expr &e)CVC3::VCLvirtual
varExpr(const std::string &name, const Type &type)CVC3::VCLvirtual
varExpr(const std::string &name, const Type &type, const Expr &def)CVC3::VCLvirtual
VCL(const CLFlags &flags)CVC3::VCL
writeExpr(const Expr &array, const Expr &index, const Expr &newValue)CVC3::VCLvirtual
~ValidityChecker()CVC3::ValidityCheckerinlinevirtual
~VCL()CVC3::VCL