CVCL::ExprTransform Class Reference

#include <expr_transform.h>

Collaboration diagram for CVCL::ExprTransform:

[legend]List of all members.

Public Member Functions

• ExprTransform (TheoryCore *core)
• ~ExprTransform ()

Preprocessor methods

FIXME: please document these functions

• Theorem preprocess (const Expr &e)
• Theorem preprocess (const Theorem &thm)
• Theorem pushNegation (const Expr &e)

  Push all negations down to the leaves.
  

• Theorem pushNegationRec (const Expr &e, bool neg)

  Auxiliary recursive function for pushNegation().
  

• Theorem pushNegationRec (const Theorem &e, bool neg)

  Its version for transitivity.
  

• Theorem pushNegation1 (const Expr &e)

  Push negation one level down. Takes 'e' which is 'NOT e[0]'.
  

• Theorem substitute (Expr e, ExprMap< Theorem > *init_st=NULL)
• Theorem ite_simplify (Expr e)
• Theorem ite_convert (const Expr &e)
• Expr ite_reorder (const Expr &e)
• Expr getNeg (const Expr &e)

Private Attributes

• TheoryCore * d_core
• CommonProofRules * d_commonRules
• CoreProofRules * d_rules
• ExprMap< Theorem > d_pushNegCache

  Cache for pushNegation().
  

---

Detailed Description

Definition at line 42 of file expr_transform.h.

---

Constructor & Destructor Documentation

ExprTransform::ExprTransform (  TheoryCore *  core  )

Definition at line 42 of file expr_transform.cpp. References d_commonRules, d_core, d_rules, CVCL::Theory::getCommonRules(), and CVCL::TheoryCore::getCoreRules().

CVCL::ExprTransform::~ExprTransform (   )  [inline]

Definition at line 53 of file expr_transform.h.

---

Member Function Documentation

Theorem ExprTransform::preprocess (  const Expr &  e  )

Definition at line 49 of file expr_transform.cpp. References d_commonRules, d_core, CVCL::TheoryCore::getFlags(), CVCL::Theorem::getRHS(), ite_convert(), ite_simplify(), pushNegation(), CVCL::CommonProofRules::reflexivityRule(), CVCL::TheoryCore::simplify(), and CVCL::CommonProofRules::transitivityRule(). Referenced by CVCL::SearchSat::check(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchImplBase::newUserAssumption(), and preprocess().

Theorem ExprTransform::preprocess (  const Theorem &  thm  )

Definition at line 65 of file expr_transform.cpp. References d_commonRules, CVCL::Theorem::getExpr(), CVCL::CommonProofRules::iffMP(), and preprocess().

Theorem ExprTransform::pushNegation (  const Expr &  e  )

Push all negations down to the leaves. Definition at line 72 of file expr_transform.cpp. References CVCL::ExprMap< Data >::clear(), d_commonRules, d_pushNegCache, CVCL::Expr::isTerm(), pushNegationRec(), and CVCL::CommonProofRules::reflexivityRule(). Referenced by preprocess().

Theorem ExprTransform::pushNegationRec (  const Expr &  e, bool  neg )

Auxiliary recursive function for pushNegation(). Definition at line 86 of file expr_transform.cpp. References CVCL::AND, CVCL::ExprMap< Data >::begin(), CVCL::CONSTDEF, d_commonRules, d_core, d_pushNegCache, d_rules, CVCL::ExprMap< Data >::end(), CVCL::FALSE, CVCL::ExprMap< Data >::find(), CVCL::IFF, CVCL::IMPLIES, CVCL::Expr::isTerm(), CVCL::ITE, CVCL::LETDECL, CVCL::NOT, CVCL::OR, CVCL::CommonProofRules::reflexivityRule(), CVCL::Theory::reflexivityRule(), CVCL::CoreProofRules::rewriteConstDef(), CVCL::CoreProofRules::rewriteImplies(), CVCL::CoreProofRules::rewriteLetDecl(), CVCL::CoreProofRules::rewriteNotAnd(), CVCL::CommonProofRules::rewriteNotFalse(), CVCL::CoreProofRules::rewriteNotIte(), CVCL::CommonProofRules::rewriteNotNot(), CVCL::CoreProofRules::rewriteNotOr(), CVCL::CommonProofRules::rewriteNotTrue(), CVCL::CommonProofRules::substitutivityRule(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::TRUE. Referenced by pushNegation(), and pushNegationRec().

Theorem ExprTransform::pushNegationRec (  const Theorem &  e, bool  neg )

Its version for transitivity. Definition at line 181 of file expr_transform.cpp. References d_commonRules, CVCL::Theorem::getRHS(), CVCL::Expr::isNot(), CVCL::Theorem::isRewrite(), pushNegationRec(), CVCL::Theorem::toString(), and CVCL::CommonProofRules::transitivityRule().

Theorem ExprTransform::pushNegation1 (  const Expr &  e  )

Push negation one level down. Takes 'e' which is 'NOT e[0]'. Definition at line 195 of file expr_transform.cpp. References CVCL::AND, CVCL::CONSTDEF, d_commonRules, d_rules, CVCL::FALSE, CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Expr::getOp(), CVCL::Theorem::getRHS(), CVCL::IMPLIES, CVCL::Expr::isNot(), CVCL::ITE, CVCL::LETDECL, CVCL::NOT, CVCL::OR, CVCL::CommonProofRules::reflexivityRule(), CVCL::CoreProofRules::rewriteConstDef(), CVCL::CoreProofRules::rewriteImplies(), CVCL::CoreProofRules::rewriteLetDecl(), CVCL::CoreProofRules::rewriteNotAnd(), CVCL::CommonProofRules::rewriteNotFalse(), CVCL::CoreProofRules::rewriteNotIte(), CVCL::CommonProofRules::rewriteNotNot(), CVCL::CoreProofRules::rewriteNotOr(), CVCL::CommonProofRules::rewriteNotTrue(), CVCL::CommonProofRules::substitutivityRule(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::CommonProofRules::transitivityRule(), and CVCL::TRUE. Referenced by TheoryCore::simplifyOp().

Theorem CVCL::ExprTransform::substitute (  Expr  e, ExprMap< Theorem > *  init_st = NULL )

Referenced by ite_simplify().

Theorem ExprTransform::ite_simplify (  Expr  e  )

Definition at line 341 of file expr_transform.cpp. References CVCL::CommonProofRules::assumpRule(), cf(), d_commonRules, d_core, d_rules, CVCL::FALSE, CVCL::Theory::falseExpr(), CVCL::Hash_Table< _Key, _Data >::Fetch(), CVCL::Expr::getKind(), CVCL::Theorem::getRHS(), hf(), CVCL::CommonProofRules::iffTrue(), CVCL::Hash_Table< _Key, _Data >::Insert(), CVCL::Dict< _Key, _Data >::Insert(), CVCL::Expr::isApply(), CVCL::Expr::isBoolConst(), CVCL::Expr::isNull(), CVCL::Expr::isRational(), CVCL::Expr::isString(), CVCL::Expr::isVar(), CVCL::ITE, mf(), CVCL::CoreProofRules::rewriteIteFalse(), CVCL::CoreProofRules::rewriteIteTrue(), substitute(), CVCL::CommonProofRules::substitutivityRule(), CVCL::CommonProofRules::transitivityRule(), CVCL::TRUE, CVCL::Theory::trueExpr(), and update_queue(). Referenced by preprocess().

Theorem ExprTransform::ite_convert (  const Expr &  e  )

Definition at line 420 of file expr_transform.cpp. References CVCL::AND, CVCL::CoreProofRules::AndToIte(), CVCL::Expr::arity(), d_commonRules, d_rules, CVCL::FALSE, CVCL::Expr::getKids(), CVCL::Expr::getKind(), CVCL::Expr::getOp(), CVCL::Theorem::getRHS(), CVCL::IFF, CVCL::CoreProofRules::IffToIte(), CVCL::IMPLIES, CVCL::CoreProofRules::ImpToIte(), CVCL::ITE, CVCL::NOT, CVCL::CoreProofRules::NotToIte(), CVCL::OR, CVCL::CoreProofRules::OrToIte(), CVCL::CommonProofRules::reflexivityRule(), CVCL::CommonProofRules::substitutivityRule(), CVCL::CommonProofRules::transitivityRule(), and CVCL::TRUE. Referenced by preprocess().

Expr ExprTransform::ite_reorder (  const Expr &  e  )

Definition at line 497 of file expr_transform.cpp. References CVCL::FALSE, CVCL::Expr::getKind(), getNeg(), CVCL::Expr::isFalse(), CVCL::Expr::isTrue(), CVCL::ITE, CVCL::Expr::iteExpr(), and CVCL::TRUE.

Expr ExprTransform::getNeg (  const Expr &  e  )

Definition at line 560 of file expr_transform.cpp. References d_core, CVCL::FALSE, CVCL::Theory::falseExpr(), CVCL::Expr::getKind(), CVCL::Expr::isFalse(), CVCL::Expr::isTrue(), CVCL::ITE, CVCL::Expr::iteExpr(), CVCL::TRUE, and CVCL::Theory::trueExpr(). Referenced by ite_reorder().

---

Member Data Documentation

TheoryCore* CVCL::ExprTransform::d_core [private]

Definition at line 44 of file expr_transform.h. Referenced by ExprTransform(), getNeg(), ite_simplify(), preprocess(), and pushNegationRec().

CommonProofRules* CVCL::ExprTransform::d_commonRules [private]

Definition at line 45 of file expr_transform.h. Referenced by ExprTransform(), ite_convert(), ite_simplify(), preprocess(), pushNegation(), pushNegation1(), and pushNegationRec().

CoreProofRules* CVCL::ExprTransform::d_rules [private]

Definition at line 46 of file expr_transform.h. Referenced by ExprTransform(), ite_convert(), ite_simplify(), pushNegation1(), and pushNegationRec().

ExprMap<Theorem> CVCL::ExprTransform::d_pushNegCache [private]

Cache for pushNegation(). Definition at line 49 of file expr_transform.h. Referenced by pushNegation(), and pushNegationRec().

---

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

• expr_transform.h
• expr_transform.cpp
• preprocess.cpp

---