CVC3::ExprTransform Class Reference

#include <expr_transform.h>

Collaboration diagram for CVC3::ExprTransform:

[legend]List of all members.

Public Member Functions

• ExprTransform (TheoryCore *core)
• ~ExprTransform ()
• Theorem smartSimplify (const Expr &e, ExprMap< bool > &cache)

  Simplification that avoids stack overflow.
  

• 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]'.
  

Private Attributes

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

  Cache for pushNegation().
  

---

Detailed Description

Definition at line 34 of file expr_transform.h.

---

Constructor & Destructor Documentation

ExprTransform::ExprTransform

(

TheoryCore *

core

)

Definition at line 32 of file expr_transform.cpp.

References d_commonRules, d_core, d_rules, CVC3::Theory::getCommonRules(), and CVC3::TheoryCore::getCoreRules().

CVC3::ExprTransform::~ExprTransform

(

)

[inline]

Definition at line 45 of file expr_transform.h.

---

Member Function Documentation

Theorem ExprTransform::smartSimplify	(	const Expr &	e,
		ExprMap< bool > &	cache
	)

Simplification that avoids stack overflow.

Stack overflow is avoided by traversing the expression to depths that are multiples of 5000 until the bottom is reached. Then, simplification is done bottom-up.

Definition at line 39 of file expr_transform.cpp.

References CVC3::Expr::arity(), d_core, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::hasFind(), CVC3::TheoryCore::simplify(), and CVC3::Expr::validSimpCache().

Referenced by preprocess().

Theorem ExprTransform::preprocess

(

const Expr &

e

)

Definition at line 76 of file expr_transform.cpp.

References d_commonRules, d_core, CVC3::TheoryCore::getFlags(), CVC3::Theorem::getRHS(), pushNegation(), CVC3::CommonProofRules::reflexivityRule(), smartSimplify(), and CVC3::CommonProofRules::transitivityRule().

Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSat::newUserAssumptionInt(), and preprocess().

Theorem ExprTransform::preprocess

(

const Theorem &

thm

)

Definition at line 89 of file expr_transform.cpp.

References d_commonRules, CVC3::Theorem::getExpr(), CVC3::CommonProofRules::iffMP(), and preprocess().

Theorem ExprTransform::pushNegation

(

const Expr &

e

)

Push all negations down to the leaves.

Definition at line 96 of file expr_transform.cpp.

References d_commonRules, d_pushNegCache, CVC3::Expr::isTerm(), pushNegationRec(), and CVC3::CommonProofRules::reflexivityRule().

Referenced by preprocess().

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

Auxiliary recursive function for pushNegation().

Definition at line 110 of file expr_transform.cpp.

References CVC3::AND, d_commonRules, d_core, d_pushNegCache, d_rules, DebugAssert, CVC3::FALSE_EXPR, CVC3::IFF, CVC3::IMPLIES, CVC3::Expr::isTerm(), CVC3::ITE, CVC3::LETDECL, CVC3::NOT, CVC3::OR, CVC3::CommonProofRules::reflexivityRule(), CVC3::Theory::reflexivityRule(), CVC3::CoreProofRules::rewriteImplies(), CVC3::CoreProofRules::rewriteLetDecl(), CVC3::CoreProofRules::rewriteNotAnd(), CVC3::CommonProofRules::rewriteNotFalse(), CVC3::CoreProofRules::rewriteNotIte(), CVC3::CommonProofRules::rewriteNotNot(), CVC3::CoreProofRules::rewriteNotOr(), CVC3::CommonProofRules::rewriteNotTrue(), CVC3::CommonProofRules::substitutivityRule(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TRUE_EXPR.

Referenced by pushNegation(), and pushNegationRec().

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

Its version for transitivity.

Definition at line 194 of file expr_transform.cpp.

References d_commonRules, DebugAssert, CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), pushNegationRec(), CVC3::Theorem::toString(), and CVC3::CommonProofRules::transitivityRule().

Theorem ExprTransform::pushNegation1

(

const Expr &

e

)

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

Definition at line 208 of file expr_transform.cpp.

References CVC3::AND, d_commonRules, d_rules, DebugAssert, CVC3::FALSE_EXPR, CVC3::Expr::getOp(), CVC3::IMPLIES, CVC3::Expr::isNot(), CVC3::ITE, CVC3::LETDECL, CVC3::NOT, CVC3::OR, CVC3::CommonProofRules::reflexivityRule(), CVC3::CoreProofRules::rewriteImplies(), CVC3::CoreProofRules::rewriteLetDecl(), CVC3::CoreProofRules::rewriteNotAnd(), CVC3::CommonProofRules::rewriteNotFalse(), CVC3::CoreProofRules::rewriteNotIte(), CVC3::CommonProofRules::rewriteNotNot(), CVC3::CoreProofRules::rewriteNotOr(), CVC3::CommonProofRules::rewriteNotTrue(), CVC3::CommonProofRules::substitutivityRule(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::CommonProofRules::transitivityRule(), and CVC3::TRUE_EXPR.

---

Member Data Documentation

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

Definition at line 36 of file expr_transform.h.

Referenced by ExprTransform(), preprocess(), pushNegationRec(), and smartSimplify().

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

Definition at line 37 of file expr_transform.h.

Referenced by ExprTransform(), preprocess(), pushNegation(), pushNegation1(), and pushNegationRec().

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

Definition at line 38 of file expr_transform.h.

Referenced by ExprTransform(), pushNegation1(), and pushNegationRec().

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

Cache for pushNegation().

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

---