expr_transform.cpp File Reference

Go to the source code of this file.

Typedefs

• typedef Hash_Table< Expr,
  Expr > CareSet
• typedef Hash_Ptr< Expr, Expr > CareSetPtr
• typedef Dict< Expr, CareSet * > Queue
• typedef Dict_Ptr< Expr, CareSet * > QueuePtr
• typedef ExprMap< Theorem > Table

Functions

• static int cf (Expr x, Expr y)
• static size_t hf (const Expr x)
• static size_t mf (const Expr x, const Expr y)
• static void update_queue (Queue *q, Expr e, CareSet *cs_prime)

---

Detailed Description

Author: Ying Hu, Clark Barrett

Created: Jun 05 2003

---

Copyright (C) 2003 by the Board of Trustees of Leland Stanford Junior University and by New York University.

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution. In particular:

• The above copyright notice and this permission notice must appear in all copies of the software and related documentation.

• THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK.

---

Definition in file expr_transform.cpp.

---

Typedef Documentation

typedef Hash_Table<Expr, Expr> CareSet

Definition at line 245 of file expr_transform.cpp.

typedef Hash_Ptr<Expr, Expr> CareSetPtr

Definition at line 246 of file expr_transform.cpp.

typedef Dict<Expr, CareSet*> Queue

Definition at line 247 of file expr_transform.cpp.

typedef Dict_Ptr<Expr, CareSet*> QueuePtr

Definition at line 248 of file expr_transform.cpp.

typedef ExprMap<Theorem> Table

Definition at line 250 of file expr_transform.cpp.

---

Function Documentation

static int cf (  Expr  x, Expr  y )  [static]

Definition at line 252 of file expr_transform.cpp. References CVCL::Expr::getIndex(). Referenced by CVCL::ExprTransform::ite_simplify().

static size_t hf (  const Expr  x  )  [static]

Definition at line 254 of file expr_transform.cpp. References CVCL::Expr::getEM(), and CVCL::ExprManager::hash(). Referenced by CVCL::ExprTransform::ite_simplify().

static size_t mf (  const Expr  x, const Expr  y )  [static]

Definition at line 256 of file expr_transform.cpp. Referenced by CVCL::ExprTransform::ite_simplify().

static void update_queue (  Queue *  q, Expr  e, CareSet *  cs_prime )  [static]

Definition at line 258 of file expr_transform.cpp. References CVCL::Hash_Table< _Key, _Data >::Fetch(), CVCL::Dict< _Key, _Data >::Fetch(), and CVCL::Dict< _Key, _Data >::Insert(). Referenced by CVCL::ExprTransform::ite_simplify().

---