CVC3
2.4.1
|
Public Member Functions | |
CoreSatAPI_implBase (SearchImplBase *se) | |
virtual | ~CoreSatAPI_implBase () |
virtual void | addLemma (const Theorem &thm, int priority, bool atBottomScope) |
Add a new lemma derived by theory core. More... | |
virtual Theorem | addAssumption (const Expr &assump) |
Add an assumption to the set of assumptions in the current context. More... | |
virtual void | addSplitter (const Expr &e, int priority) |
Suggest a splitter to the Sat engine. More... | |
virtual bool | check (const Expr &e) |
Check the validity of e in the current context. More... | |
![]() | |
CoreSatAPI () | |
virtual | ~CoreSatAPI () |
Private Attributes | |
SearchImplBase * | d_se |
Definition at line 40 of file search_impl_base.cpp.
|
inline |
Definition at line 43 of file search_impl_base.cpp.
|
inlinevirtual |
Definition at line 44 of file search_impl_base.cpp.
|
inlinevirtual |
Add a new lemma derived by theory core.
Implements CVC3::TheoryCore::CoreSatAPI.
Definition at line 45 of file search_impl_base.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 47 of file search_impl_base.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 49 of file search_impl_base.cpp.
|
virtual |
Check the validity of e in the current context.
Implements CVC3::TheoryCore::CoreSatAPI.
Definition at line 54 of file search_impl_base.cpp.
References CVC3::VALID.
|
private |
Definition at line 41 of file search_impl_base.cpp.