CVC3
2.4.1
|
Interface class for callbacks to SAT from Core. More...
#include <theory_core.h>
Public Member Functions | |
CoreSatAPI () | |
virtual | ~CoreSatAPI () |
virtual void | addLemma (const Theorem &thm, int priority=0, bool atBottomScope=false)=0 |
Add a new lemma derived by theory core. | |
virtual Theorem | addAssumption (const Expr &assump)=0 |
Add an assumption to the set of assumptions in the current context. | |
virtual void | addSplitter (const Expr &e, int priority)=0 |
Suggest a splitter to the Sat engine. | |
virtual bool | check (const Expr &e)=0 |
Check the validity of e in the current context. |
Interface class for callbacks to SAT from Core.
Author: Clark Barrett
Created: Mon Dec 5 18:42:15 2005
Definition at line 219 of file theory_core.h.
|
inline |
Definition at line 221 of file theory_core.h.
|
inlinevirtual |
Definition at line 222 of file theory_core.h.
|
pure virtual |
Add a new lemma derived by theory core.
Implemented in CVC3::SearchSatCoreSatAPI, and CVC3::CoreSatAPI_implBase.
Referenced by CVC3::Theory::addGlobalLemma().
Add an assumption to the set of assumptions in the current context.
Assumptions have the form e |- e
Implemented in CVC3::SearchSatCoreSatAPI, and CVC3::CoreSatAPI_implBase.
Referenced by CVC3::TheoryCore::assignValue().
|
pure 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. |
Implemented in CVC3::SearchSatCoreSatAPI, and CVC3::CoreSatAPI_implBase.
Referenced by CVC3::Theory::addSplitter().
|
pure virtual |
Check the validity of e in the current context.
Implemented in CVC3::SearchSatCoreSatAPI, and CVC3::CoreSatAPI_implBase.
Referenced by CVC3::Theory::newSubtypeExpr().