CVC3::SearchSatCoreSatAPI Class Reference

Inheritance diagram for CVC3::SearchSatCoreSatAPI:

[legend]

Collaboration diagram for CVC3::SearchSatCoreSatAPI:

[legend]

List of all members.

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.
  

Private Attributes

• SearchSat * d_ss

---

Detailed Description

Definition at line 46 of file search_sat.cpp.

---

Constructor & Destructor Documentation

CVC3::SearchSatCoreSatAPI::SearchSatCoreSatAPI

(

SearchSat *

ss

)

[inline]

Definition at line 49 of file search_sat.cpp.

CVC3::SearchSatCoreSatAPI::~SearchSatCoreSatAPI

(

)

[inline]

Definition at line 50 of file search_sat.cpp.

---

Member Function Documentation

void CVC3::SearchSatCoreSatAPI::addLemma	(	const Theorem &	thm,
		int	priority,
		bool	atBottomScope
	)			[inline, virtual]

Add a new lemma derived by theory core.

Implements CVC3::TheoryCore::TheoryCore::CoreSatAPI.

Definition at line 51 of file search_sat.cpp.

References CVC3::SearchSat::addLemma(), and d_ss.

Theorem CVC3::SearchSatCoreSatAPI::addAssumption

(

const Expr &

assump

)

[inline, virtual]

Add an assumption to the set of assumptions in the current context.

Assumptions have the form e |- e

Implements CVC3::TheoryCore::TheoryCore::CoreSatAPI.

Definition at line 53 of file search_sat.cpp.

References d_ss, and CVC3::SearchSat::newUserAssumption().

void CVC3::SearchSatCoreSatAPI::addSplitter	(	const Expr &	e,
		int	priority
	)			[inline, 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.

Implements CVC3::TheoryCore::TheoryCore::CoreSatAPI.

Definition at line 55 of file search_sat.cpp.

References CVC3::SearchSat::addSplitter(), and d_ss.

bool CVC3::SearchSatCoreSatAPI::check

(

const Expr &

e

)

[virtual]

Check the validity of e in the current context.

Implements CVC3::TheoryCore::TheoryCore::CoreSatAPI.

Definition at line 62 of file search_sat.cpp.

References CVC3::SearchSat::check(), d_ss, CVC3::SearchSat::pop(), CVC3::SearchSat::push(), and CVC3::VALID.

---

Member Data Documentation

SearchSat* CVC3::SearchSatCoreSatAPI::d_ss [private]

Definition at line 47 of file search_sat.cpp.

Referenced by addAssumption(), addLemma(), addSplitter(), and check().

---

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

• search_sat.cpp