CVC3::TheoryArithOld::VarOrderGraph Class Reference

Collaboration diagram for CVC3::TheoryArithOld::VarOrderGraph:

[legend]List of all members.

Public Member Functions

• void addEdge (const Expr &e1, const Expr &e2)
• bool lessThan (const Expr &e1, const Expr &e2)
• void selectLargest (const std::vector< Expr > &v1, std::vector< Expr > &v2)
• void selectSmallest (std::vector< Expr > &v1, std::vector< Expr > &v2)
• void getVerticesTopological (std::vector< Expr > &output_list)

Private Member Functions

• bool dfs (const Expr &e1, const Expr &e2)
• void dfs (const Expr &e1, std::vector< Expr > &output_list)

Private Attributes

• ExprMap< std::vector< Expr > > d_edges
• ExprMap< bool > d_cache

---

Detailed Description

Definition at line 136 of file theory_arith_old.h.

---

Member Function Documentation

bool TheoryArithOld::VarOrderGraph::dfs	(	const Expr &	e1,
		const Expr &	e2
	)			[private]

Definition at line 2109 of file theory_arith_old.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::count(), d_cache, and d_edges.

Referenced by dfs(), getVerticesTopological(), and lessThan().

void TheoryArithOld::VarOrderGraph::dfs	(	const Expr &	e1,
		std::vector< Expr > &	output_list
	)			[private]

Definition at line 2126 of file theory_arith_old.cpp.

References CVC3::Expr::begin(), CVC3::ExprMap< Data >::count(), d_cache, d_edges, dfs(), CVC3::Expr::toString(), and CVC3::TRACE.

void TheoryArithOld::VarOrderGraph::addEdge	(	const Expr &	e1,
		const Expr &	e2
	)

Definition at line 2091 of file theory_arith_old.cpp.

References d_edges, DebugAssert, CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by CVC3::TheoryArithOld::addPairToArithOrder(), and CVC3::TheoryArithOld::pickMonomial().

bool TheoryArithOld::VarOrderGraph::lessThan	(	const Expr &	e1,
		const Expr &	e2
	)

Definition at line 2101 of file theory_arith_old.cpp.

References CVC3::ExprMap< Data >::clear(), d_cache, and dfs().

Referenced by CVC3::TheoryArithOld::addPairToArithOrder(), selectLargest(), and selectSmallest().

void TheoryArithOld::VarOrderGraph::selectLargest	(	const std::vector< Expr > &	v1,
		std::vector< Expr > &	v2
	)

Definition at line 2196 of file theory_arith_old.cpp.

References lessThan().

Referenced by CVC3::TheoryArithOld::pickMonomial().

void TheoryArithOld::VarOrderGraph::selectSmallest	(	std::vector< Expr > &	v1,
		std::vector< Expr > &	v2
	)

Definition at line 2168 of file theory_arith_old.cpp.

References lessThan().

Referenced by CVC3::TheoryArithOld::assignVariables().

void TheoryArithOld::VarOrderGraph::getVerticesTopological

(

std::vector< Expr > &

output_list

)

Definition at line 2150 of file theory_arith_old.cpp.

References CVC3::ExprMap< Data >::begin(), CVC3::ExprMap< Data >::clear(), d_cache, d_edges, dfs(), and CVC3::ExprMap< Data >::end().

Referenced by CVC3::TheoryArithOld::computeTermBounds().

---

Member Data Documentation

ExprMap<std::vector<Expr> > CVC3::TheoryArithOld::VarOrderGraph::d_edges [private]

Definition at line 137 of file theory_arith_old.h.

Referenced by addEdge(), dfs(), and getVerticesTopological().

ExprMap<bool> CVC3::TheoryArithOld::VarOrderGraph::d_cache [private]

Definition at line 138 of file theory_arith_old.h.

Referenced by dfs(), getVerticesTopological(), and lessThan().

---

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

• theory_arith_old.h
• theory_arith_old.cpp

---