68 void vc_setFlags(VC vc, char c, int /*param_value*/)  in vc_setFlags()
74 void vc_setFlag(VC vc, char c)  in vc_setFlag()
79 void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value)  in vc_setInterfaceFlags()
147 void vc_printExpr(VC vc, Expr e)  in vc_printExpr()
156 char* vc_printSMTLIB(VC vc, Expr e)  in vc_printSMTLIB()
169 void vc_printExprCCode(VC vc, Expr e)  in vc_printExprCCode()
203 void vc_printExprFile(VC vc, Expr e, int fd)  in vc_printExprFile()
214 static void vc_printVarDeclsToStream(VC vc, ostream& os)  in vc_printVarDeclsToStream()
246 void vc_printVarDecls(VC vc)  in vc_printVarDecls()
251 void vc_clearDecls(VC vc)  in vc_clearDecls()
258 static void vc_printAssertsToStream(VC vc, ostream& os, int simplify_print)  in vc_printAssertsToStream()
277 void vc_printAsserts(VC vc, int simplify_print)  in vc_printAsserts()
282 void vc_printQueryStateToBuffer(VC vc, Expr e, char** buf, unsigned long* len,  in vc_printQueryStateToBuffer()
325 void vc_printCounterExampleToBuffer(VC vc, char** buf, unsigned long* len)  in vc_printCounterExampleToBuffer()
359 void vc_printExprToBuffer(VC vc, Expr e, char** buf, unsigned long* len)  in vc_printExprToBuffer()
375 void vc_printQuery(VC vc)  in vc_printQuery()
387 stp::ASTNode* persistNode(VC vc, stp::ASTNode n)  in persistNode()
402 Type vc_arrayType(VC vc, Type typeIndex, Type typeData)  in vc_arrayType()
427 Expr vc_readExpr(VC vc, Expr array, Expr index)  in vc_readExpr()
445 Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue)  in vc_writeExpr()
470 void vc_assertFormula(VC vc, Expr e)  in vc_assertFormula()
496 int vc_query(VC vc, Expr e)  in vc_query()
501 int vc_query_with_timeout(VC vc, Expr e, int timeout_ms)  in vc_query_with_timeout()
566 void vc_push(VC vc)  in vc_push()
575 void vc_pop(VC vc)  in vc_pop()
582 void vc_printCounterExample(VC vc)  in vc_printCounterExample()
605 Expr vc_getCounterExample(VC vc, Expr e)  in vc_getCounterExample()
616 void vc_getCounterExampleArray(VC vc, Expr e, Expr** indices, Expr** values,  in vc_getCounterExampleArray()
646 int vc_counterexample_size(VC vc)  in vc_counterexample_size()
654 WholeCounterExample vc_getWholeCounterExample(VC vc)  in vc_getWholeCounterExample()
699 Expr vc_varExpr1(VC vc, const char* name, int indexwidth, int valuewidth)  in vc_varExpr1()
715 Expr vc_varExpr(VC vc, const char* name, Type type)  in vc_varExpr()
757 Expr vc_eqExpr(VC vc, Expr ccc0, Expr ccc1)  in vc_eqExpr()
773 Expr vc_boolType(VC vc)  in vc_boolType()
787 Expr vc_trueExpr(VC vc)  in vc_trueExpr()
798 Expr vc_falseExpr(VC vc)  in vc_falseExpr()
809 Expr vc_notExpr(VC vc, Expr ccc)  in vc_notExpr()
823 Expr vc_andExpr(VC vc, Expr left, Expr right)  in vc_andExpr()
838 Expr vc_orExpr(VC vc, Expr left, Expr right)  in vc_orExpr()
852 Expr vc_xorExpr(VC vc, Expr left, Expr right)  in vc_xorExpr()
866 Expr vc_andExprN(VC vc, Expr* cc, int n)  in vc_andExprN()
887 Expr vc_orExprN(VC vc, Expr* cc, int n)  in vc_orExprN()
905 Expr vc_bvPlusExprN(VC vc, int n_bits, Expr* cc, int n)  in vc_bvPlusExprN()
923 Expr vc_iteExpr(VC vc, Expr cond, Expr thenpart, Expr elsepart)  in vc_iteExpr()
950 Expr vc_impliesExpr(VC vc, Expr antecedent, Expr consequent)  in vc_impliesExpr()
968 Expr vc_iffExpr(VC vc, Expr e0, Expr e1)  in vc_iffExpr()
986 Expr vc_boolToBVExpr(VC vc, Expr form)  in vc_boolToBVExpr()
1011 Expr vc_paramBoolExpr(VC vc, Expr boolvar, Expr parameter)  in vc_paramBoolExpr()
1032 Type vc_bvType(VC vc, int num_bits)  in vc_bvType()
1049 Type vc_bv32Type(VC vc)  in vc_bv32Type()
1054 Expr vc_bvConstExprFromDecStr(VC vc, int width, const char* decimalInput)  in vc_bvConstExprFromDecStr()
1066 Expr vc_bvConstExprFromStr(VC vc, const char* binary_repr)  in vc_bvConstExprFromStr()
1078 Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value)  in vc_bvConstExprFromInt()
1098 Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value)  in vc_bvConstExprFromLL()
1110 Expr vc_bvConcatExpr(VC vc, Expr left, Expr right)  in vc_bvConcatExpr()
1127 Expr createBinaryTerm(VC vc, int n_bits, Kind k, Expr left, Expr right)  in createBinaryTerm()
1143 Expr vc_bvPlusExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_bvPlusExpr()
1148 Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right)  in vc_bv32PlusExpr()
1153 Expr vc_bvMinusExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_bvMinusExpr()
1158 Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right)  in vc_bv32MinusExpr()
1163 Expr vc_bvMultExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_bvMultExpr()
1168 Expr vc_bvDivExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_bvDivExpr()
1173 Expr vc_bvModExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_bvModExpr()
1178 Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_sbvDivExpr()
1183 Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_sbvModExpr()
1188 Expr vc_sbvRemExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_sbvRemExpr()
1193 Expr vc_bv32MultExpr(VC vc, Expr left, Expr right)  in vc_bv32MultExpr()
1198 Expr createBinaryNode(VC vc, Kind k, Expr left, Expr right)  in createBinaryNode()
1215 Expr vc_bvLtExpr(VC vc, Expr left, Expr right)  in vc_bvLtExpr()
1219 Expr vc_bvLeExpr(VC vc, Expr left, Expr right)  in vc_bvLeExpr()
1223 Expr vc_bvGtExpr(VC vc, Expr left, Expr right)  in vc_bvGtExpr()
1227 Expr vc_bvGeExpr(VC vc, Expr left, Expr right)  in vc_bvGeExpr()
1232 Expr vc_sbvLtExpr(VC vc, Expr left, Expr right)  in vc_sbvLtExpr()
1236 Expr vc_sbvLeExpr(VC vc, Expr left, Expr right)  in vc_sbvLeExpr()
1240 Expr vc_sbvGtExpr(VC vc, Expr left, Expr right)  in vc_sbvGtExpr()
1244 Expr vc_sbvGeExpr(VC vc, Expr left, Expr right)  in vc_sbvGeExpr()
1249 Expr vc_bvLeftShiftExprExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_bvLeftShiftExprExpr()
1254 Expr vc_bvRightShiftExprExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_bvRightShiftExprExpr()
1259 Expr vc_bvSignedRightShiftExprExpr(VC vc, int n_bits, Expr left, Expr right)  in vc_bvSignedRightShiftExprExpr()
1264 Expr vc_bvUMinusExpr(VC vc, Expr ccc)  in vc_bvUMinusExpr()
1282 Expr vc_bvAndExpr(VC vc, Expr left, Expr right)  in vc_bvAndExpr()
1288 Expr vc_bvOrExpr(VC vc, Expr left, Expr right)  in vc_bvOrExpr()
1294 Expr vc_bvXorExpr(VC vc, Expr left, Expr right)  in vc_bvXorExpr()
1300 Expr vc_bvNotExpr(VC vc, Expr ccc)  in vc_bvNotExpr()
1314 Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr ccc)  in vc_bvLeftShiftExpr()
1336 Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr ccc)  in vc_bvRightShiftExpr()
1383 Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child)  in vc_bv32LeftShiftExpr()
1389 Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child)  in vc_bv32RightShiftExpr()
1394 Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child)  in vc_bvVar32LeftShiftExpr()
1425 Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs)  in vc_bvVar32DivByPowOfTwoExpr()
1449 Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child)  in vc_bvVar32RightShiftExpr()
1479 Expr vc_bvExtract(VC vc, Expr ccc, int hi_num, int low_num)  in vc_bvExtract()
1496 Expr vc_bvBoolExtract(VC vc, Expr ccc, int bit_num)  in vc_bvBoolExtract()
1514 Expr vc_bvBoolExtract_Zero(VC vc, Expr ccc, int bit_num)  in vc_bvBoolExtract_Zero()
1532 Expr vc_bvBoolExtract_One(VC vc, Expr ccc, int bit_num)  in vc_bvBoolExtract_One()
1550 Expr vc_bvSignExtend(VC vc, Expr ccc, int nbits)  in vc_bvSignExtend()
1629 Expr vc_simplify(VC vc, Expr e)  in vc_simplify()
1654 Expr vc_bvCreateMemoryArray(VC vc, const char* arrayName)  in vc_bvCreateMemoryArray()
1663 Expr vc_bvReadMemoryArray(VC vc, Expr array, Expr byteIndex, int numOfBytes)  in vc_bvReadMemoryArray()
1687 Expr vc_bvWriteToMemoryArray(VC vc, Expr array, Expr byteIndex, Expr element,  in vc_bvWriteToMemoryArray()
1719 Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value)  in vc_bv32ConstExprFromInt()
1740 Expr vc_parseExpr(VC vc, const char* infile)  in vc_parseExpr()
1839 int vc_getHashQueryStateToBuffer(VC vc, Expr query)  in vc_getHashQueryStateToBuffer()
1852 Type vc_getType(VC vc, Expr ex)  in vc_getType()
1898 void vc_Destroy(VC vc)  in vc_Destroy()
1969 void vc_printCounterExampleFile(VC vc, int fd)  in vc_printCounterExampleFile()
1997 void process_argument(const char ch, VC vc)  in process_argument()
2063 int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts)  in vc_parseMemExpr()
2117 void _vc_useSolver(VC vc, stp::UserDefinedFlags::SATSolvers solver)  in _vc_useSolver()
2125 bool _vc_isUsingSolver(VC vc, stp::UserDefinedFlags::SATSolvers solver)  in _vc_isUsingSolver()
2133 bool vc_supportsMinisat(VC vc)  in vc_supportsMinisat()
2138 bool vc_useMinisat(VC vc)  in vc_useMinisat()
2144 bool vc_isUsingMinisat(VC vc)  in vc_isUsingMinisat()
2149 bool vc_supportsSimplifyingMinisat(VC vc )  in vc_supportsSimplifyingMinisat()
2154 bool vc_useSimplifyingMinisat(VC vc)  in vc_useSimplifyingMinisat()
2160 bool vc_isUsingSimplifyingMinisat(VC vc)  in vc_isUsingSimplifyingMinisat()
2165 bool vc_supportsCryptominisat(VC vc )  in vc_supportsCryptominisat()
2174 bool vc_useCryptominisat(VC vc  in vc_useCryptominisat()
2188 bool vc_isUsingCryptominisat(VC vc  in vc_isUsingCryptominisat()
2201 bool vc_supportsRiss(VC vc )  in vc_supportsRiss()
2210 bool vc_useRiss(VC vc  in vc_useRiss()
2224 bool vc_isUsingRiss(VC vc  in vc_isUsingRiss()