CVC3::ExprTransform Class Reference

#include <expr_transform.h>

Collaboration diagram for CVC3::ExprTransform:

[legend]List of all members.

Public Types

• typedef std::map< std::pair<
  Expr, ExprTransform::CParameter >,
  Expr > T_name_map
• typedef std::map< Expr, std::set<
  ExprTransform::CParameter > * > T_ack_map
• typedef std::map< Expr, Type > T_type_map
• typedef std::map< std::pair<
  Expr, Expr >, Expr > B_name_map
• typedef std::map< Expr, Type > B_type_map
• typedef std::map< Expr, std::set<
  Expr > * > T_generator_map
• typedef std::map< Expr, std::vector<
  Expr > * > B_Term_map
• typedef std::map< Expr, Expr > T_ITE_map
• typedef std::map< Expr, int > B_formula_map
• typedef std::map< Expr, std::set<
  int > * > NEW_formula_map
• typedef std::vector< Expr > T_ITE_vec

Public Member Functions

• ExprTransform (TheoryCore *core)
• ~ExprTransform ()
• void setTheoryArith (TheoryArith *arith)
• std::string NewBryantVar (const int a, const int b)
• std::string NewVar (const int a, const int b)
• B_name_map BryantNames (T_generator_map &generator_map, B_type_map &type_map)
• Expr ITE_generator (Expr &Orig, Expr &Value, B_Term_map &Creation_map, B_name_map &name_map, T_ITE_map &ITE_map)
• void Get_ITEs (B_formula_map &instance_map, std::set< Expr > &Not_replaced_set, B_Term_map &P_term_map, T_ITE_vec &ITE_vec, B_Term_map &Creation_map, B_name_map &name_map, T_ITE_map &ITE_map)
• void PredConstrainTester (std::set< Expr > &Not_replaced_set, const Expr &e, B_name_map &name_map, std::vector< Expr > &Pred_vec, std::set< Expr > &Constrained_set, std::set< Expr > &P_constrained_set, T_generator_map &Constrained_map)
• void PredConstrainer (std::set< Expr > &Not_replaced_set, const Expr &e, const Expr &Pred, int location, B_name_map &name_map, std::set< Expr > &SeenBefore, std::set< Expr > &Constrained_set, T_generator_map &Constrained_map, std::set< Expr > &P_constrained_set)
• Expr ConstrainedConstraints (std::set< Expr > &Not_replaced_set, T_generator_map &Constrained_map, B_name_map &name_map, B_Term_map &Creation_map, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, std::set< Expr > &P_constrained_set)
• void RemoveFunctionApps (const Expr &orig, std::set< Expr > &Not_replaced_set, std::vector< Expr > &Old, std::vector< Expr > &New, T_ITE_map &ITE_map, std::set< Expr > &SeenBefore)
• void GetSortedOpVec (B_Term_map &X_generator_map, B_Term_map &X_term_map, B_Term_map &P_term_map, std::set< Expr > &P_terms, std::set< Expr > &G_terms, std::set< Expr > &X_terms, std::vector< Expr > &sortedOps, std::set< Expr > &SeenBefore)
• void GetFormulaMap (const Expr &e, std::set< Expr > &formula_map, std::set< Expr > &G_terms, int &size, int negations)
• void GetGTerms2 (std::set< Expr > &formula_map, std::set< Expr > &G_terms)
• void GetSub_vec (T_ITE_vec &ITE_vec, const Expr &e, std::set< Expr > &ITE_Added)
• void GetOrderedTerms (B_formula_map &instance_map, B_name_map &name_map, B_Term_map &X_term_map, T_ITE_vec &ITE_vec, std::set< Expr > &G_terms, std::set< Expr > &X_terms, std::vector< Expr > &Pred_vec, std::vector< Expr > &sortedOps, std::vector< Expr > &Constrained_vec, std::vector< Expr > &UnConstrained_vec, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, B_Term_map &G_term_map, B_Term_map &P_term_map, std::set< Expr > &SeenBefore, std::set< Expr > &ITE_Added)
• void GetPEqs (const Expr &e, B_name_map &name_map, std::set< Expr > &P_constrained_set, std::set< Expr > &Constrained_set, T_generator_map &Constrained_map, std::set< Expr > &SeenBefore)
• Expr ConstrainedConstraints (T_generator_map &Constrained_map, B_name_map &name_map, B_Term_map &Creation_map, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, std::set< Expr > &P_constrained_set)
• void BuildBryantMaps (const Expr &e, T_generator_map &generator_map, B_Term_map &X_generator_map, B_type_map &type_map, std::vector< Expr > &Pred_vec, std::set< Expr > &P_terms, std::set< Expr > &G_terms, B_Term_map &P_term_map, B_Term_map &G_term_map, std::set< Expr > &SeenBefore, std::set< Expr > &ITE_Added)
• int CountSubTerms (const Expr &e, int &counter)
• void GetOrdering (B_Term_map &X_generator_map, B_Term_map &G_term_map, B_Term_map &P_Term_map)
• void B_Term_Map_Deleter (B_Term_map &Map)
• void T_generator_Map_Deleter (T_generator_map &Map)
• Theorem dobryant (const Expr &T)
• T_name_map ANNames (T_ack_map &ack_map, T_type_map &type_map)
• Expr AckConstraints (T_ack_map &ack_map, T_name_map &name_map)
• void GetAckSwap (const Expr &orig, std::vector< Expr > &OldAck, std::vector< Expr > &NewAck, T_name_map &name_map, T_ack_map &ack_map, std::set< Expr > &SeenBefore)
• void BuildMap (const Expr &e, T_ack_map &ack_map, T_type_map &type_map, std::set< Expr > &SeenBefore)
• Theorem doackermann (const Expr &T)
• 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]'.
  

• Theorem specialSimplify (const Expr &e, ExprHashMap< Theorem > &cache)

  Helper for newPP.
  

• Theorem newPP (const Expr &e, int &budget)

  new preprocessing code
  

• Theorem newPPrec (const Expr &e, int &budget)

  main new preprocessing code
  

• Theorem simplifyWithCare (const Expr &e)

  ITE simplification from Burch paper.
  

Private Member Functions

• void updateQueue (ExprMap< std::set< Expr > * > &queue, const Expr &e, const std::set< Expr > &careSet)

  Helper for simplifyWithCare.
  

• Theorem substitute (const Expr &e, ExprHashMap< Theorem > &substTable, ExprHashMap< Theorem > &cache)

  Helper for simplifyWithCare.
  

Private Attributes

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

  Cache for pushNegation().
  

• ExprMap< Theorem > d_newPPCache

  Cache for newPP.
  

• int d_budgetLimit

  Budget limit for newPP.
  

---

Detailed Description

Definition at line 35 of file expr_transform.h.

---

Member Typedef Documentation

typedef std::map< std::pair< Expr, ExprTransform::CParameter >, Expr > CVC3::ExprTransform::T_name_map

Definition at line 57 of file expr_transform.h.

typedef std::map< Expr, std::set< ExprTransform::CParameter >* > CVC3::ExprTransform::T_ack_map

Definition at line 63 of file expr_transform.h.

typedef std::map< Expr, Type> CVC3::ExprTransform::T_type_map

Definition at line 64 of file expr_transform.h.

typedef std::map< std::pair< Expr, Expr>, Expr > CVC3::ExprTransform::B_name_map

Definition at line 65 of file expr_transform.h.

typedef std::map<Expr, Type> CVC3::ExprTransform::B_type_map

Definition at line 66 of file expr_transform.h.

typedef std::map< Expr, std::set<Expr>*> CVC3::ExprTransform::T_generator_map

Definition at line 67 of file expr_transform.h.

typedef std::map<Expr, std::vector<Expr>*> CVC3::ExprTransform::B_Term_map

Definition at line 68 of file expr_transform.h.

typedef std::map< Expr, Expr> CVC3::ExprTransform::T_ITE_map

Definition at line 69 of file expr_transform.h.

typedef std::map< Expr, int> CVC3::ExprTransform::B_formula_map

Definition at line 70 of file expr_transform.h.

typedef std::map<Expr, std::set<int>*> CVC3::ExprTransform::NEW_formula_map

Definition at line 71 of file expr_transform.h.

typedef std::vector<Expr> CVC3::ExprTransform::T_ITE_vec

Definition at line 72 of file expr_transform.h.

---

Constructor & Destructor Documentation

ExprTransform::ExprTransform

(

TheoryCore *

core

)

Definition at line 34 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 51 of file expr_transform.h.

---

Member Function Documentation

void CVC3::ExprTransform::setTheoryArith

(

TheoryArith *

arith

)

[inline]

Definition at line 53 of file expr_transform.h.

References d_theoryArith.

std::string ExprTransform::NewBryantVar	(	const int	a,
		const int	b
	)

Definition at line 25 of file bryant.cpp.

Referenced by BryantNames().

std::string CVC3::ExprTransform::NewVar	(	const int	a,
		const int	b
	)

ExprTransform::B_name_map ExprTransform::BryantNames	(	T_generator_map &	generator_map,
		B_type_map &	type_map
	)

Definition at line 36 of file bryant.cpp.

References d_core, NewBryantVar(), and CVC3::Theory::newVar().

Referenced by dobryant().

Expr ExprTransform::ITE_generator	(	Expr &	Orig,
		Expr &	Value,
		B_Term_map &	Creation_map,
		B_name_map &	name_map,
		T_ITE_map &	ITE_map
	)

Definition at line 110 of file bryant.cpp.

References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::Expr::eqExpr(), CVC3::Expr::getOpExpr(), CVC3::Expr::isNull(), and CVC3::Expr::iteExpr().

Referenced by Get_ITEs().

void ExprTransform::Get_ITEs	(	B_formula_map &	instance_map,
		std::set< Expr > &	Not_replaced_set,
		B_Term_map &	P_term_map,
		T_ITE_vec &	ITE_vec,
		B_Term_map &	Creation_map,
		B_name_map &	name_map,
		T_ITE_map &	ITE_map
	)

Definition at line 149 of file bryant.cpp.

References ITE_generator(), and LIMIT.

Referenced by dobryant().

void ExprTransform::PredConstrainTester	(	std::set< Expr > &	Not_replaced_set,
		const Expr &	e,
		B_name_map &	name_map,
		std::vector< Expr > &	Pred_vec,
		std::set< Expr > &	Constrained_set,
		std::set< Expr > &	P_constrained_set,
		T_generator_map &	Constrained_map
	)

Definition at line 94 of file bryant.cpp.

References PredConstrainer().

Referenced by dobryant().

void ExprTransform::PredConstrainer	(	std::set< Expr > &	Not_replaced_set,
		const Expr &	e,
		const Expr &	Pred,
		int	location,
		B_name_map &	name_map,
		std::set< Expr > &	SeenBefore,
		std::set< Expr > &	Constrained_set,
		T_generator_map &	Constrained_map,
		std::set< Expr > &	P_constrained_set
	)

Definition at line 55 of file bryant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::end(), CVC3::Expr::eqExpr(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), CVC3::Expr::isTerm(), CVC3::Expr::notExpr(), and CVC3::UFUNC.

Referenced by PredConstrainTester().

Expr ExprTransform::ConstrainedConstraints	(	std::set< Expr > &	Not_replaced_set,
		T_generator_map &	Constrained_map,
		B_name_map &	name_map,
		B_Term_map &	Creation_map,
		std::set< Expr > &	Constrained_set,
		std::set< Expr > &	UnConstrained_set,
		std::set< Expr > &	P_constrained_set
	)

Definition at line 442 of file bryant.cpp.

References CVC3::Expr::andExpr(), CVC3::Expr::begin(), d_core, CVC3::Expr::eqExpr(), CVC3::Expr::notExpr(), and CVC3::Theory::trueExpr().

Referenced by dobryant().

void ExprTransform::RemoveFunctionApps	(	const Expr &	orig,
		std::set< Expr > &	Not_replaced_set,
		std::vector< Expr > &	Old,
		std::vector< Expr > &	New,
		T_ITE_map &	ITE_map,
		std::set< Expr > &	SeenBefore
	)

Definition at line 185 of file bryant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), and CVC3::UFUNC.

Referenced by dobryant().

void ExprTransform::GetSortedOpVec	(	B_Term_map &	X_generator_map,
		B_Term_map &	X_term_map,
		B_Term_map &	P_term_map,
		std::set< Expr > &	P_terms,
		std::set< Expr > &	G_terms,
		std::set< Expr > &	X_terms,
		std::vector< Expr > &	sortedOps,
		std::set< Expr > &	SeenBefore
	)

Definition at line 199 of file bryant.cpp.

Referenced by dobryant().

void ExprTransform::GetFormulaMap	(	const Expr &	e,
		std::set< Expr > &	formula_map,
		std::set< Expr > &	G_terms,
		int &	size,
		int	negations
	)

Definition at line 252 of file bryant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::isEq(), and CVC3::Expr::isNot().

Referenced by dobryant().

void ExprTransform::GetGTerms2	(	std::set< Expr > &	formula_map,
		std::set< Expr > &	G_terms
	)

Definition at line 262 of file bryant.cpp.

Referenced by dobryant().

void ExprTransform::GetSub_vec	(	T_ITE_vec &	ITE_vec,
		const Expr &	e,
		std::set< Expr > &	ITE_Added
	)

Definition at line 271 of file bryant.cpp.

References CVC3::Expr::arity(), and CVC3::Expr::isTerm().

Referenced by GetOrderedTerms().

void ExprTransform::GetOrderedTerms	(	B_formula_map &	instance_map,
		B_name_map &	name_map,
		B_Term_map &	X_term_map,
		T_ITE_vec &	ITE_vec,
		std::set< Expr > &	G_terms,
		std::set< Expr > &	X_terms,
		std::vector< Expr > &	Pred_vec,
		std::vector< Expr > &	sortedOps,
		std::vector< Expr > &	Constrained_vec,
		std::vector< Expr > &	UnConstrained_vec,
		std::set< Expr > &	Constrained_set,
		std::set< Expr > &	UnConstrained_set,
		B_Term_map &	G_term_map,
		B_Term_map &	P_term_map,
		std::set< Expr > &	SeenBefore,
		std::set< Expr > &	ITE_Added
	)

Definition at line 281 of file bryant.cpp.

References GetSub_vec().

Referenced by dobryant().

void ExprTransform::GetPEqs	(	const Expr &	e,
		B_name_map &	name_map,
		std::set< Expr > &	P_constrained_set,
		std::set< Expr > &	Constrained_set,
		T_generator_map &	Constrained_map,
		std::set< Expr > &	SeenBefore
	)

Definition at line 401 of file bryant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::eqExpr(), CVC3::Expr::isEq(), and CVC3::Expr::notExpr().

Referenced by dobryant().

Expr CVC3::ExprTransform::ConstrainedConstraints	(	T_generator_map &	Constrained_map,
		B_name_map &	name_map,
		B_Term_map &	Creation_map,
		std::set< Expr > &	Constrained_set,
		std::set< Expr > &	UnConstrained_set,
		std::set< Expr > &	P_constrained_set
	)

void ExprTransform::BuildBryantMaps	(	const Expr &	e,
		T_generator_map &	generator_map,
		B_Term_map &	X_generator_map,
		B_type_map &	type_map,
		std::vector< Expr > &	Pred_vec,
		std::set< Expr > &	P_terms,
		std::set< Expr > &	G_terms,
		B_Term_map &	P_term_map,
		B_Term_map &	G_term_map,
		std::set< Expr > &	SeenBefore,
		std::set< Expr > &	ITE_Added
	)

Definition at line 342 of file bryant.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Expr::isApply(), CVC3::Expr::isTerm(), CVC3::Expr::isVar(), and CVC3::UFUNC.

Referenced by dobryant().

int ExprTransform::CountSubTerms	(	const Expr &	e,
		int &	counter
	)

Definition at line 14 of file bryant.cpp.

References CVC3::Expr::arity().

Referenced by GetOrdering().

void ExprTransform::GetOrdering	(	B_Term_map &	X_generator_map,
		B_Term_map &	G_term_map,
		B_Term_map &	P_Term_map
	)

Definition at line 493 of file bryant.cpp.

References CountSubTerms().

Referenced by dobryant().

void ExprTransform::B_Term_Map_Deleter

(

B_Term_map &

Map

)

Definition at line 563 of file bryant.cpp.

Referenced by dobryant().

void ExprTransform::T_generator_Map_Deleter

(

T_generator_map &

Map

)

Definition at line 568 of file bryant.cpp.

Referenced by dobryant().

Theorem ExprTransform::dobryant

(

const Expr &

T

)

Definition at line 573 of file bryant.cpp.

References B_Term_Map_Deleter(), BryantNames(), BuildBryantMaps(), ConstrainedConstraints(), d_core, d_rules, CVC3::CoreProofRules::dummyTheorem(), Get_ITEs(), GetFormulaMap(), GetGTerms2(), GetOrderedTerms(), GetOrdering(), GetPEqs(), GetSortedOpVec(), CVC3::Expr::impExpr(), LIMIT, CVC3::Expr::notExpr(), PredConstrainTester(), CVC3::Theory::reflexivityRule(), RemoveFunctionApps(), CVC3::Expr::substExpr(), and T_generator_Map_Deleter().

Referenced by preprocess().

T_name_map CVC3::ExprTransform::ANNames	(	T_ack_map &	ack_map,
		T_type_map &	type_map
	)

Expr CVC3::ExprTransform::AckConstraints	(	T_ack_map &	ack_map,
		T_name_map &	name_map
	)

void CVC3::ExprTransform::GetAckSwap	(	const Expr &	orig,
		std::vector< Expr > &	OldAck,
		std::vector< Expr > &	NewAck,
		T_name_map &	name_map,
		T_ack_map &	ack_map,
		std::set< Expr > &	SeenBefore
	)

void CVC3::ExprTransform::BuildMap	(	const Expr &	e,
		T_ack_map &	ack_map,
		T_type_map &	type_map,
		std::set< Expr > &	SeenBefore
	)

Theorem CVC3::ExprTransform::doackermann

(

const Expr &

T

)

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 42 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 79 of file expr_transform.cpp.

References CVC3::TheoryCore::callTheoryPreprocess(), CVC3::TheoryCore::clearInPP(), d_budgetLimit, d_commonRules, d_core, dobryant(), CVC3::Theory::getEM(), CVC3::TheoryCore::getFlags(), CVC3::Theorem::getRHS(), CVC3::ExprManager::invalidateSimpCache(), CVC3::Theorem::isRefl(), newPP(), pushNegation(), CVC3::CommonProofRules::reflexivityRule(), CVC3::TheoryCore::setInPP(), simplifyWithCare(), smartSimplify(), and CVC3::CommonProofRules::transitivityRule().

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

Theorem ExprTransform::preprocess

(

const Theorem &

thm

)

Definition at line 120 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 127 of file expr_transform.cpp.

References CVC3::ExprMap< Data >::clear(), 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 141 of file expr_transform.cpp.

References CVC3::AND, d_commonRules, d_core, d_pushNegCache, d_rules, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::FALSE_EXPR, CVC3::ExprMap< Data >::find(), 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 225 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 239 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.

Theorem ExprTransform::specialSimplify	(	const Expr &	e,
		ExprHashMap< Theorem > &	cache
	)

Helper for newPP.

Definition at line 296 of file expr_transform.cpp.

References d_commonRules, d_core, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Expr::isAtomic(), CVC3::CommonProofRules::reflexivityRule(), CVC3::TheoryCore::simplify(), and CVC3::CommonProofRules::substitutivityRule().

Theorem ExprTransform::newPP	(	const Expr &	e,
		int &	budget
	)

new preprocessing code

Definition at line 282 of file expr_transform.cpp.

References CVC3::ExprMap< Data >::clear(), d_budgetLimit, d_commonRules, d_newPPCache, CVC3::Theorem::getRHS(), CVC3::Expr::getSize(), CVC3::Expr::getType(), CVC3::Type::isBool(), newPPrec(), and CVC3::CommonProofRules::reflexivityRule().

Referenced by preprocess().

Theorem ExprTransform::newPPrec	(	const Expr &	e,
		int &	budget
	)

main new preprocessing code

Definition at line 334 of file expr_transform.cpp.

References CVC3::TheoryCore::addFact(), CVC3::Expr::arity(), CVC3::CommonProofRules::assumpRule(), CVC3::Expr::containsTermITE(), d_budgetLimit, d_commonRules, d_core, d_newPPCache, d_rules, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::TheoryCore::getCM(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isPropAtom(), CVC3::Theorem::isRefl(), CVC3::CommonProofRules::liftOneITE(), CVC3::Expr::negate(), CVC3::ContextManager::pop(), CVC3::ContextManager::push(), CVC3::CommonProofRules::reflexivityRule(), CVC3::CoreProofRules::rewriteIteElse(), CVC3::CoreProofRules::rewriteIteThen(), CVC3::TheoryCore::simplify(), CVC3::CommonProofRules::substitutivityRule(), and CVC3::CommonProofRules::transitivityRule().

Referenced by newPP().

void CVC3::ExprTransform::updateQueue	(	ExprMap< std::set< Expr > * > &	queue,
		const Expr &	e,
		const std::set< Expr > &	careSet
	)			[private]

Helper for simplifyWithCare.

Referenced by simplifyWithCare().

Theorem ExprTransform::substitute	(	const Expr &	e,
		ExprHashMap< Theorem > &	substTable,
		ExprHashMap< Theorem > &	cache
	)			[private]

Helper for simplifyWithCare.

Definition at line 434 of file expr_transform.cpp.

References d_commonRules, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Expr::isAtomic(), CVC3::CommonProofRules::reflexivityRule(), CVC3::CommonProofRules::substitutivityRule(), and CVC3::CommonProofRules::transitivityRule().

Referenced by simplifyWithCare().

Theorem ExprTransform::simplifyWithCare

(

const Expr &

e

)

ITE simplification from Burch paper.

Definition at line 476 of file expr_transform.cpp.

References CVC3::AND, CVC3::Expr::arity(), d_commonRules, d_core, d_rules, d_theoryArith, DebugAssert, CVC3::CoreProofRules::dummyTheorem(), CVC3::ExprMap< Data >::empty(), CVC3::ExprMap< Data >::end(), CVC3::Expr::eqExpr(), CVC3::ExprMap< Data >::erase(), CVC3::ExprManager::falseExpr(), CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Expr::isAtomic(), CVC3::Expr::isAtomicFormula(), CVC3::Type::isBool(), CVC3::Expr::isPropAtom(), CVC3::Theorem::isRefl(), CVC3::ITE, CVC3::TheoryArith::leavesAreNumConst(), CVC3::CommonProofRules::liftOneITE(), CVC3::Expr::negate(), CVC3::OR, CVC3::CommonProofRules::reflexivityRule(), CVC3::CoreProofRules::rewriteIteCond(), CVC3::TheoryCore::simplify(), substitute(), CVC3::Theory::theoryOf(), CVC3::CommonProofRules::transitivityRule(), CVC3::ExprManager::trueExpr(), and updateQueue().

Referenced by preprocess().

---

Member Data Documentation

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

Definition at line 37 of file expr_transform.h.

Referenced by BryantNames(), ConstrainedConstraints(), dobryant(), ExprTransform(), newPPrec(), preprocess(), pushNegationRec(), simplifyWithCare(), smartSimplify(), and specialSimplify().

TheoryArith* CVC3::ExprTransform::d_theoryArith [private]

Definition at line 38 of file expr_transform.h.

Referenced by setTheoryArith(), and simplifyWithCare().

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

Definition at line 39 of file expr_transform.h.

Referenced by ExprTransform(), newPP(), newPPrec(), preprocess(), pushNegation(), pushNegation1(), pushNegationRec(), simplifyWithCare(), specialSimplify(), and substitute().

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

Definition at line 40 of file expr_transform.h.

Referenced by dobryant(), ExprTransform(), newPPrec(), pushNegation1(), pushNegationRec(), and simplifyWithCare().

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

Cache for pushNegation().

Definition at line 43 of file expr_transform.h.

Referenced by pushNegation(), and pushNegationRec().

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

Cache for newPP.

Definition at line 45 of file expr_transform.h.

Referenced by newPP(), and newPPrec().

int CVC3::ExprTransform::d_budgetLimit [private]

Budget limit for newPP.

Definition at line 47 of file expr_transform.h.

Referenced by newPP(), newPPrec(), and preprocess().

---

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

• expr_transform.h
• bryant.cpp
• expr_transform.cpp

---