CVCL::TheoryArith::VarOrderGraph Class Reference

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

---

Member Function Documentation

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

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

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

Definition at line 1465 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 1475 of file theory_arith.cpp. References CVCL::ExprMap< Data >::clear(), d_cache, and dfs(). Referenced by selectLargest(), and selectSmallest().

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

Definition at line 1529 of file theory_arith.cpp. References lessThan(), and CVCL::ExprMap< Data >::size(). Referenced by CVCL::TheoryArith::pickMonomial().

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

Definition at line 1501 of file theory_arith.cpp. References lessThan(), and CVCL::ExprMap< Data >::size(). Referenced by CVCL::TheoryArith::assignVariables().

---

Member Data Documentation

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

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

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

Definition at line 170 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

---