CVC3::TheoryDatatypeLazy Class Reference
[Theories]

This theory handles datatypes. More...

#include <theory_datatype_lazy.h>

Inheritance diagram for CVC3::TheoryDatatypeLazy:

[legend]Collaboration diagram for CVC3::TheoryDatatypeLazy:

[legend]List of all members.

Public Member Functions

TheoryDatatypeLazy (TheoryCore *theoryCore)
~TheoryDatatypeLazy ()
void checkSat (bool fullEffort)
Check for satisfiability in the theory.
void setup (const Expr &e)
Set up the term e for call-backs when e or its children change.
void update (const Theorem &e, const Expr &d)
Notify a theory of a new equality.

Private Types

enum ProcessKinds { MERGE1 = 0, MERGE2, ENQUEUE }

Private Member Functions

void instantiate (const Expr &e, const bigunsigned &u)
void initializeLabels (const Expr &e, const Type &t)
void mergeLabels (const Theorem &thm, const Expr &e1, const Expr &e2)
void mergeLabels (const Theorem &thm, const Expr &e, unsigned position, bool positive)

Private Attributes

CDList< Theorem > d_processQueue
CDList< ProcessKinds > d_processQueueKind
CDO< unsigned > d_processIndex
CDO< bool > d_typeComplete

Detailed Description

This theory handles datatypes.

Author: Clark Barrett

Created: Wed Dec 1 22:27:12 2004

Definition at line 42 of file theory_datatype_lazy.h.

Member Enumeration Documentation

enum CVC3::TheoryDatatypeLazy::ProcessKinds [private]

Enumerator:

MERGE1
MERGE2
ENQUEUE

Definition at line 44 of file theory_datatype_lazy.h.

Constructor & Destructor Documentation

TheoryDatatypeLazy::TheoryDatatypeLazy ( TheoryCore * theoryCore )

Definition at line 41 of file theory_datatype_lazy.cpp.

CVC3::TheoryDatatypeLazy::~TheoryDatatypeLazy ( ) [inline]

Definition at line 64 of file theory_datatype_lazy.h.

Member Function Documentation

void TheoryDatatypeLazy::instantiate	(	const Expr &	e,
		const bigunsigned &	u
	)			`[private]`

void TheoryDatatypeLazy::initializeLabels	(	const Expr &	e,
		const Type &	t
	)			`[private, virtual]`

Reimplemented from CVC3::TheoryDatatype.

Definition at line 90 of file theory_datatype_lazy.cpp.

References CVC3::TheoryDatatype::d_datatypes, CVC3::TheoryDatatype::d_labels, CVC3::TheoryDatatype::d_splitters, d_typeComplete, DebugAssert, CVC3::Theory::findExpr(), CVC3::getConstructor(), CVC3::Type::getExpr(), instantiate(), CVC3::isConstructor(), CVC3::Theory::theoryCore(), and CVC3::Expr::toString().

Referenced by setup().

void TheoryDatatypeLazy::mergeLabels	(	const Theorem &	thm,
		const Expr &	e1,
		const Expr &	e2
	)			`[private, virtual]`

Reimplemented from CVC3::TheoryDatatype.

Definition at line 123 of file theory_datatype_lazy.cpp.

References CVC3::TheoryDatatype::d_facts, CVC3::TheoryDatatype::d_labels, CVC3::TheoryDatatype::d_rules, DebugAssert, CVC3::DatatypeProofRules::dummyTheorem(), CVC3::Theory::falseExpr(), CVC3::Theory::find(), CVC3::Expr::getType(), CVC3::Expr::hasFind(), instantiate(), CVC3::Theorem::isNull(), and CVC3::Theory::setInconsistent().

Referenced by checkSat().

void TheoryDatatypeLazy::mergeLabels	(	const Theorem &	thm,
		const Expr &	e,
		unsigned	position,
		bool	positive
	)			`[private, virtual]`

Reimplemented from CVC3::TheoryDatatype.

Definition at line 151 of file theory_datatype_lazy.cpp.

References CVC3::TheoryDatatype::d_facts, CVC3::TheoryDatatype::d_labels, CVC3::TheoryDatatype::d_rules, DebugAssert, CVC3::DatatypeProofRules::dummyTheorem(), CVC3::Theory::falseExpr(), CVC3::Theory::find(), CVC3::Expr::hasFind(), instantiate(), and CVC3::Theory::setInconsistent().

void TheoryDatatypeLazy::checkSat ( bool fullEffort ) [virtual]

Check for satisfiability in the theory.

Parameters:

fullEffort

when it is false, checkSat can do as much or as little work as it likes, though simple inferences and checks for consistency should be done to increase efficiency. If fullEffort is true, checkSat must check whether the set of facts given by assertFact together with the arrangement of shared terms (provided by addSharedTerm) induced by the global find database equivalence relation are satisfiable. If satisfiable, checkSat does nothing.

If satisfiability can be acheived by merging some of the shared terms, a new fact must be enqueued using enqueueFact (this fact need not be a literal). If there is no way to make things satisfiable, setInconsistent must be called.

Reimplemented from CVC3::TheoryDatatype.

Definition at line 178 of file theory_datatype_lazy.cpp.

References CVC3::Theory::addSplitter(), CVC3::TheoryDatatype::d_datatypes, CVC3::TheoryDatatype::d_facts, CVC3::TheoryDatatype::d_labels, d_processIndex, d_processQueue, d_processQueueKind, CVC3::TheoryDatatype::d_splitterAsserted, CVC3::TheoryDatatype::d_splitters, CVC3::TheoryDatatype::d_splittersIndex, d_typeComplete, CVC3::TheoryDatatype::datatypeTestExpr(), DebugAssert, ENQUEUE, CVC3::Theory::enqueueFact(), CVC3::Theory::findExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::isSelected(), MERGE1, MERGE2, mergeLabels(), and CVC3::Expr::setSelected().

void TheoryDatatypeLazy::setup ( const Expr & e ) [virtual]

Set up the term e for call-backs when e or its children change.

setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update.

See also:: update

Reimplemented from CVC3::TheoryDatatype.

Definition at line 246 of file theory_datatype_lazy.cpp.

References CVC3::Expr::addToNotify(), CVC3::APPLY, CVC3::TheoryDatatype::d_labels, d_processQueue, d_processQueueKind, CVC3::TheoryDatatype::d_rules, CVC3::DATATYPE, ENQUEUE, CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getType(), initializeLabels(), CVC3::isConstructor(), CVC3::isSelector(), MERGE2, CVC3::DatatypeProofRules::noCycle(), CVC3::Theory::reflexivityRule(), and CVC3::Theory::setupCC().

void TheoryDatatypeLazy::update	(	const Theorem &	e,
		const Expr &	d
	)			`[virtual]`

Notify a theory of a new equality.

update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2.

To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup.