CVC3
|
Inherits CVC3::TheoryCore::CoreSatAPI.
Public Member Functions | |
SearchSatCoreSatAPI (SearchSat *ss) | |
~SearchSatCoreSatAPI () | |
void | addLemma (const Theorem &thm, int priority, bool atBottomScope) |
Add a new lemma derived by theory core. | |
Theorem | addAssumption (const Expr &assump) |
Add an assumption to the set of assumptions in the current context. | |
void | addSplitter (const Expr &e, int priority) |
Suggest a splitter to the Sat engine. | |
bool | check (const Expr &e) |
Check the validity of e in the current context. | |
![]() | |
CoreSatAPI () | |
virtual | ~CoreSatAPI () |
Private Attributes | |
SearchSat * | d_ss |
Definition at line 46 of file search_sat.cpp.
|
inline |
Definition at line 49 of file search_sat.cpp.
|
inline |
Definition at line 50 of file search_sat.cpp.
|
inlinevirtual |
Add a new lemma derived by theory core.
Implements CVC3::TheoryCore::CoreSatAPI.
Definition at line 51 of file search_sat.cpp.
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.
|
inlinevirtual |
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.
|
virtual |
Check the validity of e in the current context.
Implements CVC3::TheoryCore::CoreSatAPI.
Definition at line 62 of file search_sat.cpp.
References CVC3::VALID.
|
private |
Definition at line 47 of file search_sat.cpp.