Searched refs:BVQuickCheck (Results 1 – 6 of 6) sorted by relevance
29 BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv) in BVQuickCheck() function in CVC4::theory::bv::BVQuickCheck43 void BVQuickCheck::setConflict() in setConflict()93 bool BVQuickCheck::addAssertion(TNode assertion) { in addAssertion()105 void BVQuickCheck::push() { in push()109 void BVQuickCheck::pop() { in pop()113 BVQuickCheck::vars_iterator BVQuickCheck::beginVars() { in beginVars()116 BVQuickCheck::vars_iterator BVQuickCheck::endVars() { in endVars()120 Node BVQuickCheck::getVarValue(TNode var, bool fullModel) { in getVarValue()130 void BVQuickCheck::clearSolver() { in clearSolver()135 void BVQuickCheck::popToZero() { in popToZero()[all …]
41 class BVQuickCheck {49 BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv);50 ~BVQuickCheck();123 BVQuickCheck* d_solver;166 QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budged = 10000);
36 class BVQuickCheck; variable64 std::unique_ptr<BVQuickCheck> d_quickCheck;
151 class BVQuickCheck; variable173 std::unique_ptr<BVQuickCheck> d_quickSolver;
50 d_quickCheck.reset(new BVQuickCheck("bb", bv)); in BitblastSolver()
233 d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)), in AlgebraicSolver()