Definition at line 47 of file search_sat.cpp.
CVC3::SearchSatCoreSatAPI::SearchSatCoreSatAPI | ( | SearchSat * | ss | ) | [inline] |
Definition at line 50 of file search_sat.cpp.
CVC3::SearchSatCoreSatAPI::~SearchSatCoreSatAPI | ( | ) | [inline] |
Definition at line 51 of file search_sat.cpp.
void CVC3::SearchSatCoreSatAPI::addLemma | ( | const Theorem & | thm | ) | [inline, virtual] |
Add a new lemma derived by theory core.
Implements CVC3::TheoryCore::CoreSatAPI.
Definition at line 52 of file search_sat.cpp.
References CVC3::SearchSat::addLemma(), and d_ss.
Add an assumption to the set of assumptions in the current context.
Assumptions have the form e |- e
Implements CVC3::TheoryCore::CoreSatAPI.
Definition at line 53 of file search_sat.cpp.
References d_ss, and CVC3::SearchSat::newUserAssumption().
void CVC3::SearchSatCoreSatAPI::addSplitter | ( | const Expr & | e, | |
int | priority | |||
) | [inline, virtual] |
Suggest a splitter to the Sat engine.
e | is a literal. | |
priority | is between -10 and 10. A priority above 0 indicates that the splitter should be favored. A priority below 0 indicates that the splitter should be delayed. |
Implements CVC3::TheoryCore::CoreSatAPI.
Definition at line 55 of file search_sat.cpp.
References CVC3::SearchSat::addSplitter(), and d_ss.
bool CVC3::SearchSatCoreSatAPI::check | ( | const Expr & | e | ) | [virtual] |
Check the validity of e in the current context.
Implements CVC3::TheoryCore::CoreSatAPI.
Definition at line 61 of file search_sat.cpp.
References CVC3::SearchSat::check(), d_ss, CVC3::SearchSat::pop(), CVC3::SearchSat::push(), and CVC3::VALID.
SearchSat* CVC3::SearchSatCoreSatAPI::d_ss [private] |
Definition at line 48 of file search_sat.cpp.
Referenced by addAssumption(), addLemma(), addSplitter(), and check().