CVCL::ValidityChecker Member List

This is the complete list of members for CVCL::ValidityChecker, including all inherited members.

andExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
andExpr(const std::vector< Expr > &children)=0CVCL::ValidityChecker [pure virtual]
arrayType(const Type &typeIndex, const Type &typeData)=0CVCL::ValidityChecker [pure virtual]
assertFormula(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
boolType()=0CVCL::ValidityChecker [pure virtual]
boundVarExpr(const std::string &name, const std::string &uid, const Type &type)=0CVCL::ValidityChecker [pure virtual]
checkContinue()=0CVCL::ValidityChecker [pure virtual]
checkUnsat(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
create(const CLFlags &flags)CVCL::ValidityChecker [static]
create()CVCL::ValidityChecker [static]
createFlags()CVCL::ValidityChecker [static]
createOp(const std::string &name, const Type &type)=0CVCL::ValidityChecker [pure virtual]
createOp(const std::string &name, const Type &type, const Expr &def)=0CVCL::ValidityChecker [pure virtual]
createType(const std::string &typeName)=0CVCL::ValidityChecker [pure virtual]
createType(const std::string &typeName, const Type &def)=0CVCL::ValidityChecker [pure virtual]
dataType(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types)=0CVCL::ValidityChecker [pure 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)=0CVCL::ValidityChecker [pure 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)=0CVCL::ValidityChecker [pure virtual]
datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args)=0CVCL::ValidityChecker [pure virtual]
datatypeSelExpr(const std::string &selector, const Expr &arg)=0CVCL::ValidityChecker [pure virtual]
datatypeTestExpr(const std::string &constructor, const Expr &arg)=0CVCL::ValidityChecker [pure virtual]
divideExpr(const Expr &numerator, const Expr &denominator)=0CVCL::ValidityChecker [pure virtual]
eqExpr(const Expr &child0, const Expr &child1)=0CVCL::ValidityChecker [pure virtual]
existsExpr(const std::vector< Expr > &vars, const Expr &body)=0CVCL::ValidityChecker [pure virtual]
falseExpr()=0CVCL::ValidityChecker [pure virtual]
forallExpr(const std::vector< Expr > &vars, const Expr &body)=0CVCL::ValidityChecker [pure virtual]
funExpr(const Op &op, const Expr &child)=0CVCL::ValidityChecker [pure virtual]
funExpr(const Op &op, const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
funExpr(const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)=0CVCL::ValidityChecker [pure virtual]
funExpr(const Op &op, const std::vector< Expr > &children)=0CVCL::ValidityChecker [pure virtual]
funType(const Type &typeDom, const Type &typeRan)=0CVCL::ValidityChecker [pure virtual]
funType(const std::vector< Type > &typeDom, const Type &typeRan)=0CVCL::ValidityChecker [pure virtual]
geExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
getAssumptions(std::vector< Expr > &assumptions)=0CVCL::ValidityChecker [pure virtual]
getAssumptionsTCC(std::vector< Expr > &assumptions)=0CVCL::ValidityChecker [pure virtual]
getAssumptionsUsed(std::vector< Expr > &assumptions)=0CVCL::ValidityChecker [pure virtual]
getBaseType(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
getBaseType(const Type &t)=0CVCL::ValidityChecker [pure virtual]
getClosure()=0CVCL::ValidityChecker [pure virtual]
getConcreteModel(ExprMap< Expr > &m)=0CVCL::ValidityChecker [pure virtual]
getCounterExample(std::vector< Expr > &assumptions, bool inOrder=true)=0CVCL::ValidityChecker [pure virtual]
getCurrentContext()=0CVCL::ValidityChecker [pure virtual]
getEM()=0CVCL::ValidityChecker [pure virtual]
getFlags() const =0CVCL::ValidityChecker [pure virtual]
getImpliedLiteral()=0CVCL::ValidityChecker [pure virtual]
getInternalAssumptions(std::vector< Expr > &assumptions)=0CVCL::ValidityChecker [pure virtual]
getProof()=0CVCL::ValidityChecker [pure virtual]
getProofClosure()=0CVCL::ValidityChecker [pure virtual]
getProofTCC()=0CVCL::ValidityChecker [pure virtual]
getStatistics()=0CVCL::ValidityChecker [pure virtual]
getTCC()=0CVCL::ValidityChecker [pure virtual]
getType(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
getTypePred(const Type &t, const Expr &e)=0CVCL::ValidityChecker [pure virtual]
getUserAssumptions(std::vector< Expr > &assumptions)=0CVCL::ValidityChecker [pure virtual]
gtExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
idExpr(const std::string &name)=0CVCL::ValidityChecker [pure virtual]
iffExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
impliesExpr(const Expr &hyp, const Expr &conc)=0CVCL::ValidityChecker [pure virtual]
importExpr(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
importType(const Type &t)=0CVCL::ValidityChecker [pure virtual]
incomplete()=0CVCL::ValidityChecker [pure virtual]
incomplete(std::vector< std::string > &reasons)=0CVCL::ValidityChecker [pure virtual]
inconsistent(std::vector< Expr > &assumptions)=0CVCL::ValidityChecker [pure virtual]
intType()=0CVCL::ValidityChecker [pure virtual]
iteExpr(const Expr &ifpart, const Expr &thenpart, const Expr &elsepart)=0CVCL::ValidityChecker [pure virtual]
lambdaExpr(const std::vector< Expr > &vars, const Expr &body)=0CVCL::ValidityChecker [pure virtual]
leExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
listExpr(const std::vector< Expr > &kids)=0CVCL::ValidityChecker [pure virtual]
listExpr(const Expr &e1)=0CVCL::ValidityChecker [pure virtual]
listExpr(const Expr &e1, const Expr &e2)=0CVCL::ValidityChecker [pure virtual]
listExpr(const Expr &e1, const Expr &e2, const Expr &e3)=0CVCL::ValidityChecker [pure virtual]
listExpr(const std::string &op, const std::vector< Expr > &kids)=0CVCL::ValidityChecker [pure virtual]
listExpr(const std::string &op, const Expr &e1)=0CVCL::ValidityChecker [pure virtual]
listExpr(const std::string &op, const Expr &e1, const Expr &e2)=0CVCL::ValidityChecker [pure virtual]
listExpr(const std::string &op, const Expr &e1, const Expr &e2, const Expr &e3)=0CVCL::ValidityChecker [pure virtual]
loadFile(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)=0CVCL::ValidityChecker [pure virtual]
loadFile(std::istream &is, InputLanguage lang=PRESENTATION_LANG, bool interactive=false)=0CVCL::ValidityChecker [pure virtual]
lookupType(const std::string &typeName)=0CVCL::ValidityChecker [pure virtual]
lookupVar(const std::string &name, Type *type)=0CVCL::ValidityChecker [pure virtual]
ltExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
minusExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
multExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
notExpr(const Expr &child)=0CVCL::ValidityChecker [pure virtual]
orExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
orExpr(const std::vector< Expr > &children)=0CVCL::ValidityChecker [pure virtual]
parseExpr(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
parseType(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
plusExpr(const Expr &left, const Expr &right)=0CVCL::ValidityChecker [pure virtual]
pop()=0CVCL::ValidityChecker [pure virtual]
popScope()=0CVCL::ValidityChecker [pure virtual]
popto(int stackLevel)=0CVCL::ValidityChecker [pure virtual]
poptoScope(int scopeLevel)=0CVCL::ValidityChecker [pure virtual]
powExpr(const Expr &x, const Expr &n)=0CVCL::ValidityChecker [pure virtual]
printExpr(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
printExpr(const Expr &e, std::ostream &os)=0CVCL::ValidityChecker [pure virtual]
printStatistics()=0CVCL::ValidityChecker [pure virtual]
printV(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
push()=0CVCL::ValidityChecker [pure virtual]
pushScope()=0CVCL::ValidityChecker [pure virtual]
query(const Expr &e, bool tcc=false)=0CVCL::ValidityChecker [pure virtual]
ratExpr(int n, int d=1)=0CVCL::ValidityChecker [pure virtual]
ratExpr(const std::string &n, const std::string &d, int base)=0CVCL::ValidityChecker [pure virtual]
ratExpr(const std::string &n, int base=10)=0CVCL::ValidityChecker [pure virtual]
readExpr(const Expr &array, const Expr &index)=0CVCL::ValidityChecker [pure virtual]
realType()=0CVCL::ValidityChecker [pure virtual]
recordExpr(const std::string &field, const Expr &expr)=0CVCL::ValidityChecker [pure virtual]
recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1)=0CVCL::ValidityChecker [pure virtual]
recordExpr(const std::string &field0, const Expr &expr0, const std::string &field1, const Expr &expr1, const std::string &field2, const Expr &expr2)=0CVCL::ValidityChecker [pure virtual]
recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &exprs)=0CVCL::ValidityChecker [pure virtual]
recordType(const std::string &field, const Type &type)=0CVCL::ValidityChecker [pure virtual]
recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1)=0CVCL::ValidityChecker [pure virtual]
recordType(const std::string &field0, const Type &type0, const std::string &field1, const Type &type1, const std::string &field2, const Type &type2)=0CVCL::ValidityChecker [pure virtual]
recordType(const std::vector< std::string > &fields, const std::vector< Type > &types)=0CVCL::ValidityChecker [pure virtual]
recSelectExpr(const Expr &record, const std::string &field)=0CVCL::ValidityChecker [pure virtual]
recUpdateExpr(const Expr &record, const std::string &field, const Expr &newValue)=0CVCL::ValidityChecker [pure virtual]
registerAtom(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
reprocessFlags()=0CVCL::ValidityChecker [pure virtual]
restart(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
returnFromCheck()=0CVCL::ValidityChecker [pure virtual]
scopeLevel()=0CVCL::ValidityChecker [pure virtual]
setResourceLimit(unsigned limit)=0CVCL::ValidityChecker [pure virtual]
simplify(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
simplifyThm(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
simplifyThm2(const Expr &e)=0CVCL::ValidityChecker [pure virtual]
simulateExpr(const Expr &f, const Expr &s0, const std::vector< Expr > &inputs, const Expr &n)=0CVCL::ValidityChecker [pure virtual]
stackLevel()=0CVCL::ValidityChecker [pure virtual]
stringExpr(const std::string &str)=0CVCL::ValidityChecker [pure virtual]
subrangeType(const Expr &l, const Expr &r)=0CVCL::ValidityChecker [pure virtual]
subtypeType(const Expr &pred)=0CVCL::ValidityChecker [pure virtual]
trueExpr()=0CVCL::ValidityChecker [pure virtual]
tupleExpr(const std::vector< Expr > &exprs)=0CVCL::ValidityChecker [pure virtual]
tupleSelectExpr(const Expr &tuple, int index)=0CVCL::ValidityChecker [pure virtual]
tupleType(const Type &type0, const Type &type1)=0CVCL::ValidityChecker [pure virtual]
tupleType(const Type &type0, const Type &type1, const Type &type2)=0CVCL::ValidityChecker [pure virtual]
tupleType(const std::vector< Type > &types)=0CVCL::ValidityChecker [pure virtual]
tupleUpdateExpr(const Expr &tuple, int index, const Expr &newValue)=0CVCL::ValidityChecker [pure virtual]
uminusExpr(const Expr &child)=0CVCL::ValidityChecker [pure virtual]
ValidityChecker()CVCL::ValidityChecker [inline]
varExpr(const std::string &name, const Type &type)=0CVCL::ValidityChecker [pure virtual]
varExpr(const std::string &name, const Type &type, const Expr &def)=0CVCL::ValidityChecker [pure virtual]
writeExpr(const Expr &array, const Expr &index, const Expr &newValue)=0CVCL::ValidityChecker [pure virtual]
~ValidityChecker()CVCL::ValidityChecker [inline, virtual]


Generated on Thu Apr 13 16:57:45 2006 for CVC Lite by  doxygen 1.4.4