CVC3::TheoryCore::CoreSatAPI Class Reference

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

#include <theory_core.h>

Inherited by CVC3::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.

List of all members.

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.
  

---

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

(

)

[inline, virtual]

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::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.

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::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.

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:

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::CoreSatAPI_implBase, and CVC3::SearchSatCoreSatAPI.

virtual bool CVC3::TheoryCore::CoreSatAPI::check

(

const Expr &

e

)

[pure virtual]

Check the validity of e in the current context.

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

---

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

• theory_core.h