CVC3::ExprTransform Class Reference

#include <expr_transform.h>

Collaboration diagram for CVC3::ExprTransform:

Collaboration graph
[legend]

List of all members.

Public Types

Public Member Functions

Private Member Functions

Private Attributes

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.

Referenced by CVC3::VCL::init().

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::iffExpr(), 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 CVC3::Expr::arity(), d_commonRules, d_core, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Expr::getType(), CVC3::Expr::isAtomic(), CVC3::Type::isBool(), CVC3::Theorem::isRefl(), 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 ExprTransform::updateQueue ( ExprMap< std::set< Expr > * > &  queue,
const Expr &  e,
const std::set< Expr > &  careSet 
) [private]

Helper for simplifyWithCare.

Definition at line 413 of file expr_transform.cpp.

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 CVC3::Expr::arity(), d_commonRules, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Expr::isAtomic(), CVC3::Theorem::isRefl(), 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(), CVC3::Expr::containsTermITE(), 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::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::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:
Generated on Thu Oct 15 22:18:58 2009 for CVC3 by  doxygen 1.5.8