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.

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.

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.

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  ) 

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 
)

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 
)

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 
)

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 
)

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  ) 

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  ) 

Theorem ExprTransform::preprocess ( const Theorem thm  ) 

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 
)

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

Theorem ExprTransform::pushNegation1 ( const Expr e  ) 

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

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

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

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]

Theorem ExprTransform::simplifyWithCare ( const Expr e  ) 


Member Data Documentation

Definition at line 38 of file expr_transform.h.

Referenced by setTheoryArith(), and simplifyWithCare().

Cache for pushNegation().

Definition at line 43 of file expr_transform.h.

Referenced by pushNegation(), and pushNegationRec().

Cache for newPP.

Definition at line 45 of file expr_transform.h.

Referenced by newPP(), and newPPrec().

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