CVCL::TheoryArith::VarOrderGraph Class Reference

Collaboration diagram for CVCL::TheoryArith::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)

Private Member Functions

• bool dfs (const Expr &e1, const Expr &e2)

Private Attributes

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

---

Detailed Description

Definition at line 166 of file theory_arith.h.

---

Member Function Documentation

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

Definition at line 1508 of file theory_arith.cpp. References CVCL::ExprMap< Data >::begin(), CVCL::ExprMap< Data >::count(), d_cache, and d_edges. Referenced by lessThan().

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

Definition at line 1490 of file theory_arith.cpp. References d_edges, CVCL::Expr::toString(), and CVCL::TRACE. Referenced by CVCL::TheoryArith::pickMonomial().

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

Definition at line 1500 of file theory_arith.cpp. References CVCL::ExprMap< Data >::clear(), d_cache, and dfs().

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

Referenced by CVCL::TheoryArith::pickMonomial().

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

Referenced by CVCL::TheoryArith::assignVariables().

---

Member Data Documentation

ExprMap<std::vector<Expr> > CVCL::TheoryArith::VarOrderGraph::d_edges [private]

Definition at line 167 of file theory_arith.h. Referenced by addEdge(), and dfs().

ExprMap<bool> CVCL::TheoryArith::VarOrderGraph::d_cache [private]

Definition at line 168 of file theory_arith.h. Referenced by dfs(), and lessThan().

---

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

• theory_arith.h
• theory_arith.cpp

---