CVCL::Translator Class Reference

#include <translator.h>

Collaboration diagram for CVCL::Translator:

[legend]List of all members.

Public Member Functions

• Translator::Translator (TheoryArith *theoryarith, bool convertToDiff, bool iteLiftArith)
• Expr preprocess (const Expr &e)
• virtual ~Translator ()

Private Member Functions

• Expr preprocessRec (const Expr &e, ExprMap< Expr > &cache)

Private Attributes

• TheoryArith * d_theoryArith
• bool d_convertToDiff
• bool d_iteLiftArith

---

Detailed Description

Definition at line 40 of file translator.h.

---

Constructor & Destructor Documentation

virtual CVCL::Translator::~Translator (   )  [inline, virtual]

Definition at line 57 of file translator.h.

---

Member Function Documentation

Expr CVCL::Translator::preprocessRec (  const Expr &  e, ExprMap< Expr > &  cache )  [private]

Definition at line 42 of file translator.cpp. References CVCL::Expr::arity(), CVCL::CONSTDEF, d_convertToDiff, d_iteLiftArith, d_theoryArith, CVCL::DIVIDE, CVCL::ExprMap< Data >::end(), CVCL::EQ, CVCL::ExprMap< Data >::find(), CVCL::GE, CVCL::Theory::getBaseType(), CVCL::Expr::getKind(), CVCL::Expr::getOp(), CVCL::GT, CVCL::INTDIV, CVCL::TheoryArith::isAtomicArithFormula(), CVCL::ITE, CVCL::Expr::iteExpr(), CVCL::LE, CVCL::LT, CVCL::MINUS, CVCL::MOD, CVCL::MULT, CVCL::PLUS, CVCL::POW, CVCL::TheoryArith::realType(), CVCL::TheoryArith::rewriteToDiff(), and CVCL::UMINUS. Referenced by preprocess().

CVCL::Translator::Translator::Translator (  TheoryArith *  theoryarith, bool  convertToDiff, bool  iteLiftArith )  [inline]

Definition at line 49 of file translator.h. References Translator::Translator(). Referenced by Translator::Translator().

Expr CVCL::Translator::preprocess (  const Expr &  e  )

Definition at line 129 of file translator.cpp. References preprocessRec(). Referenced by CVCL::VCL::query().

---

Member Data Documentation

TheoryArith* CVCL::Translator::d_theoryArith [private]

Definition at line 41 of file translator.h. Referenced by preprocessRec().

bool CVCL::Translator::d_convertToDiff [private]

Definition at line 42 of file translator.h. Referenced by preprocessRec().

bool CVCL::Translator::d_iteLiftArith [private]

Definition at line 43 of file translator.h. Referenced by preprocessRec().

---

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

• translator.h
• translator.cpp

---