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::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_batchedAssertionsCVC3::VCL [private]
d_batchedAssertionsIdxCVC3::VCL [private]
d_cmCVC3::VCL [private]
d_dumpCVC3::VCL [private]
d_emCVC3::VCL [private]
d_flagsCVC3::VCL [private]
d_lastClosureCVC3::VCL [private]
d_lastQueryCVC3::VCL [private]
d_lastQueryTCCCVC3::VCL [private]
d_modelStackPushedCVC3::VCL [private]
d_nextIdxCVC3::VCL [private]
d_seCVC3::VCL [private]
d_stackLevelCVC3::VCL [private]
d_statisticsCVC3::VCL [private]
d_theoriesCVC3::VCL [private]
d_theoryArithCVC3::VCL [private]
d_theoryArrayCVC3::VCL [private]
d_theoryBitvectorCVC3::VCL [private]
d_theoryCoreCVC3::VCL [private]
d_theoryDatatypeCVC3::VCL [private]
d_theoryQuantCVC3::VCL [private]
d_theoryRecordsCVC3::VCL [private]
d_theorySimulateCVC3::VCL [private]
d_theoryUFCVC3::VCL [private]
d_tmCVC3::VCL [private]
d_translatorCVC3::VCL [private]
d_userAssertionsCVC3::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 [inline, virtual]
getFlags() const CVC3::VCL [inline, virtual]
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 [inline, virtual]
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 [inline, virtual]
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 [inline, virtual]
~VCL()CVC3::VCL
Generated on Thu Sep 1 2011 19:35:15 for CVC3 by  doxygen 1.7.3