CVC3  2.4.1
Public Member Functions | List of all members
CVC3::TheoryCore::CoreSatAPI Class Referenceabstract

Interface class for callbacks to SAT from Core. More...

#include <theory_core.h>

Inheritance diagram for CVC3::TheoryCore::CoreSatAPI:
CVC3::CoreSatAPI_implBase CVC3::SearchSatCoreSatAPI

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. More...
 
virtual Theorem addAssumption (const Expr &assump)=0
 Add an assumption to the set of assumptions in the current context. More...
 
virtual void addSplitter (const Expr &e, int priority)=0
 Suggest a splitter to the Sat engine. More...
 
virtual bool check (const Expr &e)=0
 Check the validity of e in the current context. More...
 

Detailed Description

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.

Constructor & Destructor Documentation

CVC3::TheoryCore::CoreSatAPI::CoreSatAPI ( )
inline

Definition at line 221 of file theory_core.h.

virtual CVC3::TheoryCore::CoreSatAPI::~CoreSatAPI ( )
inlinevirtual

Definition at line 222 of file theory_core.h.

Member Function Documentation

virtual void CVC3::TheoryCore::CoreSatAPI::addLemma ( const Theorem thm,
int  priority = 0,
bool  atBottomScope = false 
)
pure virtual

Add a new lemma derived by theory core.

Implemented in CVC3::SearchSatCoreSatAPI, and CVC3::CoreSatAPI_implBase.

Referenced by CVC3::Theory::addGlobalLemma().

virtual Theorem CVC3::TheoryCore::CoreSatAPI::addAssumption ( const Expr assump)
pure virtual

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().

virtual void CVC3::TheoryCore::CoreSatAPI::addSplitter ( const Expr e,
int  priority 
)
pure virtual

Suggest a splitter to the Sat engine.

Parameters
eis a literal.
priorityis 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().

virtual bool CVC3::TheoryCore::CoreSatAPI::check ( const Expr e)
pure virtual

Check the validity of e in the current context.

Implemented in CVC3::SearchSatCoreSatAPI, and CVC3::CoreSatAPI_implBase.

Referenced by CVC3::Theory::newSubtypeExpr().


The documentation for this class was generated from the following file: