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