CVC3
CVC3::ValidityChecker Member List

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

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