CVC3  2.4.1
Public Types | Public Member Functions | Private Member Functions | Private Attributes | List of all members
CVC3::ExprTransform Class Reference

#include <expr_transform.h>

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, TypeT_type_map
 
typedef std::map< std::pair
< Expr, Expr >, Expr
B_name_map
 
typedef std::map< Expr, TypeB_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, ExprT_ITE_map
 
typedef std::map< Expr, int > B_formula_map
 
typedef std::map< Expr,
std::set< int > * > 
NEW_formula_map
 
typedef std::vector< ExprT_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. More...
 
Theorem preprocess (const Expr &e)
 
Theorem preprocess (const Theorem &thm)
 
Theorem pushNegation (const Expr &e)
 Push all negations down to the leaves. More...
 
Theorem pushNegationRec (const Expr &e, bool neg)
 Auxiliary recursive function for pushNegation(). More...
 
Theorem pushNegationRec (const Theorem &e, bool neg)
 Its version for transitivity. More...
 
Theorem pushNegation1 (const Expr &e)
 Push negation one level down. Takes 'e' which is 'NOT e[0]'. More...
 
Theorem specialSimplify (const Expr &e, ExprHashMap< Theorem > &cache)
 Helper for newPP. More...
 
Theorem newPP (const Expr &e, int &budget)
 new preprocessing code More...
 
Theorem newPPrec (const Expr &e, int &budget)
 main new preprocessing code More...
 
Theorem simplifyWithCare (const Expr &e)
 ITE simplification from Burch paper. More...
 

Private Member Functions

void updateQueue (ExprMap< std::set< Expr > * > &queue, const Expr &e, const std::set< Expr > &careSet)
 Helper for simplifyWithCare. More...
 
Theorem substitute (const Expr &e, ExprHashMap< Theorem > &substTable, ExprHashMap< Theorem > &cache)
 Helper for simplifyWithCare. More...
 

Private Attributes

TheoryCored_core
 
TheoryArithd_theoryArith
 
CommonProofRulesd_commonRules
 
CoreProofRulesd_rules
 
ExprMap< Theoremd_pushNegCache
 Cache for pushNegation() More...
 
ExprMap< Theoremd_newPPCache
 Cache for newPP. More...
 
int d_budgetLimit
 Budget limit for newPP. More...
 

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.

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

Definition at line 25 of file bryant.cpp.

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.

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 LIMIT.

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.

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 
)

Definition at line 442 of file bryant.cpp.

References CVC3::Expr::andExpr(), CVC3::Expr::eqExpr(), and CVC3::Expr::notExpr().

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 UFUNC.

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.

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().

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

Definition at line 262 of file bryant.cpp.

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().

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.

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 
)
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().

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.

void ExprTransform::B_Term_Map_Deleter ( B_Term_map Map)

Definition at line 563 of file bryant.cpp.

void ExprTransform::T_generator_Map_Deleter ( T_generator_map Map)

Definition at line 568 of file bryant.cpp.

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 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.

References CVC3::ExprMap< Data >::find().

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

TheoryCore* CVC3::ExprTransform::d_core
private
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
CoreProofRules* CVC3::ExprTransform::d_rules
private
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: