CVC3
2.4.1
|
#include <expr_transform.h>
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.
Definition at line 72 of file expr_transform.h.
ExprTransform::ExprTransform | ( | TheoryCore * | core | ) |
Definition at line 34 of file expr_transform.cpp.
References d_commonRules, d_core, CVC3::Theory::getCommonRules(), d_rules, and CVC3::TheoryCore::getCoreRules().
CVC3::ExprTransform::~ExprTransform | ( | ) | [inline] |
Definition at line 51 of file expr_transform.h.
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 | ||
) |
Definition at line 110 of file bryant.cpp.
References CVC3::Expr::getOpExpr(), CVC3::Expr::arity(), CVC3::Expr::eqExpr(), CVC3::Expr::isNull(), CVC3::Expr::andExpr(), and CVC3::Expr::iteExpr().
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 | ||
) |
Definition at line 55 of file bryant.cpp.
References CVC3::Expr::isApply(), CVC3::Expr::getOpKind(), UFUNC, CVC3::Expr::isTerm(), CVC3::Expr::getOpExpr(), CVC3::Expr::eqExpr(), CVC3::Expr::notExpr(), and CVC3::Expr::arity().
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::eqExpr(), CVC3::Expr::notExpr(), and CVC3::Expr::andExpr().
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::isApply(), CVC3::Expr::getOpKind(), 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::isEq(), CVC3::Expr::isNot(), and CVC3::Expr::arity().
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 | ||
) |
Definition at line 401 of file bryant.cpp.
References CVC3::Expr::isEq(), CVC3::Expr::eqExpr(), CVC3::Expr::notExpr(), and CVC3::Expr::arity().
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::isApply(), CVC3::Expr::getOpKind(), UFUNC, CVC3::Expr::getOpExpr(), CVC3::Expr::getType(), CVC3::Expr::isTerm(), CVC3::Expr::arity(), and CVC3::Expr::isVar().
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.
Definition at line 573 of file bryant.cpp.
References CVC3::Expr::notExpr(), LIMIT, CVC3::Expr::substExpr(), CVC3::Expr::impExpr(), and CVC3::Expr::iffExpr().
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 | ||
) |
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 DebugAssert, CVC3::ExprMap::find(), CVC3::ExprMap::end(), CVC3::Expr::hasFind(), CVC3::Expr::validSimpCache(), CVC3::Expr::arity(), d_core, and CVC3::TheoryCore::simplify().
Referenced by preprocess().
Definition at line 79 of file expr_transform.cpp.
References d_core, CVC3::Theory::getEM(), CVC3::ExprManager::invalidateSimpCache(), CVC3::TheoryCore::setInPP(), d_commonRules, CVC3::CommonProofRules::reflexivityRule(), CVC3::TheoryCore::getFlags(), pushNegation(), CVC3::CommonProofRules::transitivityRule(), smartSimplify(), CVC3::Theorem::getRHS(), dobryant(), simplifyWithCare(), d_budgetLimit, newPP(), CVC3::Theorem::isRefl(), CVC3::TheoryCore::callTheoryPreprocess(), and CVC3::TheoryCore::clearInPP().
Referenced by preprocess(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchSimple::checkValidInternal(), CVC3::TheoryCore::getAssignment(), and CVC3::TheoryCore::getValue().
Definition at line 120 of file expr_transform.cpp.
References d_commonRules, CVC3::CommonProofRules::iffMP(), preprocess(), and CVC3::Theorem::getExpr().
Push all negations down to the leaves.
Definition at line 127 of file expr_transform.cpp.
References CVC3::Expr::isTerm(), d_commonRules, CVC3::CommonProofRules::reflexivityRule(), pushNegationRec(), d_pushNegCache, and CVC3::ExprMap::clear().
Referenced by preprocess().
Auxiliary recursive function for pushNegation().
Definition at line 141 of file expr_transform.cpp.
References TRACE, DebugAssert, CVC3::Expr::isTerm(), CVC3::Expr::toString(), d_pushNegCache, CVC3::ExprMap::find(), CVC3::ExprMap::end(), d_core, CVC3::Theory::reflexivityRule(), TRUE_EXPR, d_commonRules, CVC3::CommonProofRules::rewriteNotTrue(), FALSE_EXPR, CVC3::CommonProofRules::rewriteNotFalse(), NOT, CVC3::CommonProofRules::rewriteNotNot(), AND, d_rules, CVC3::CoreProofRules::rewriteNotAnd(), OR, CVC3::CoreProofRules::rewriteNotOr(), IMPLIES, CVC3::CoreProofRules::rewriteImplies(), CVC3::CommonProofRules::substitutivityRule(), ITE, CVC3::CoreProofRules::rewriteNotIte(), LETDECL, CVC3::CoreProofRules::rewriteLetDecl(), CVC3::CommonProofRules::reflexivityRule(), and IFF.
Referenced by pushNegation(), and pushNegationRec().
Its version for transitivity.
Definition at line 225 of file expr_transform.cpp.
References DebugAssert, CVC3::Theorem::isRewrite(), CVC3::Theorem::toString(), CVC3::Theorem::getRHS(), d_commonRules, CVC3::CommonProofRules::transitivityRule(), and pushNegationRec().
Push negation one level down. Takes 'e' which is 'NOT e[0]'.
Definition at line 239 of file expr_transform.cpp.
References TRACE, DebugAssert, CVC3::Expr::isNot(), CVC3::Expr::toString(), TRUE_EXPR, d_commonRules, CVC3::CommonProofRules::rewriteNotTrue(), FALSE_EXPR, CVC3::CommonProofRules::rewriteNotFalse(), NOT, CVC3::CommonProofRules::rewriteNotNot(), AND, d_rules, CVC3::CoreProofRules::rewriteNotAnd(), OR, CVC3::CoreProofRules::rewriteNotOr(), IMPLIES, CVC3::CoreProofRules::rewriteImplies(), CVC3::CommonProofRules::substitutivityRule(), CVC3::Expr::getOp(), CVC3::CommonProofRules::transitivityRule(), ITE, CVC3::CoreProofRules::rewriteNotIte(), LETDECL, CVC3::CoreProofRules::rewriteLetDecl(), and CVC3::CommonProofRules::reflexivityRule().
Theorem ExprTransform::specialSimplify | ( | const Expr & | e, |
ExprHashMap< Theorem > & | cache | ||
) |
Helper for newPP.
Definition at line 296 of file expr_transform.cpp.
References CVC3::Expr::isAtomic(), d_commonRules, CVC3::CommonProofRules::reflexivityRule(), CVC3::ExprHashMap::find(), CVC3::ExprHashMap::end(), CVC3::Expr::getType(), CVC3::Type::isBool(), d_core, CVC3::TheoryCore::simplify(), CVC3::Expr::arity(), CVC3::Theorem::isRefl(), and CVC3::CommonProofRules::substitutivityRule().
new preprocessing code
Definition at line 282 of file expr_transform.cpp.
References CVC3::Expr::getType(), CVC3::Type::isBool(), d_commonRules, CVC3::CommonProofRules::reflexivityRule(), d_newPPCache, CVC3::ExprMap::clear(), newPPrec(), d_budgetLimit, CVC3::Theorem::getRHS(), and CVC3::Expr::getSize().
Referenced by preprocess().
main new preprocessing code
Definition at line 334 of file expr_transform.cpp.
References DebugAssert, CVC3::Expr::getType(), CVC3::Type::isBool(), d_commonRules, CVC3::CommonProofRules::reflexivityRule(), CVC3::Expr::containsTermITE(), d_newPPCache, CVC3::ExprMap::find(), CVC3::ExprMap::end(), d_budgetLimit, CVC3::Expr::isPropAtom(), CVC3::Expr::arity(), CVC3::Theorem::isRefl(), CVC3::CommonProofRules::transitivityRule(), CVC3::CommonProofRules::substitutivityRule(), CVC3::Theorem::getRHS(), CVC3::CommonProofRules::liftOneITE(), d_core, CVC3::TheoryCore::getCM(), CVC3::ContextManager::push(), CVC3::TheoryCore::addFact(), CVC3::CommonProofRules::assumpRule(), CVC3::TheoryCore::simplify(), d_rules, CVC3::CoreProofRules::rewriteIteThen(), CVC3::ContextManager::pop(), CVC3::Expr::negate(), and CVC3::CoreProofRules::rewriteIteElse().
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::isAtomic(), d_commonRules, CVC3::CommonProofRules::reflexivityRule(), CVC3::ExprHashMap::find(), CVC3::ExprHashMap::end(), CVC3::CommonProofRules::transitivityRule(), CVC3::Expr::arity(), CVC3::Theorem::isRefl(), and CVC3::CommonProofRules::substitutivityRule().
Referenced by simplifyWithCare().
ITE simplification from Burch paper.
Definition at line 476 of file expr_transform.cpp.
References updateQueue(), CVC3::ExprMap::empty(), CVC3::ExprMap::end(), CVC3::ExprMap::erase(), CVC3::Expr::isAtomic(), CVC3::Expr::isAtomicFormula(), CVC3::Expr::isPropAtom(), d_core, CVC3::Theory::theoryOf(), d_theoryArith, CVC3::TheoryArith::leavesAreNumConst(), d_commonRules, CVC3::CommonProofRules::reflexivityRule(), CVC3::Expr::containsTermITE(), CVC3::CommonProofRules::transitivityRule(), CVC3::CommonProofRules::liftOneITE(), DebugAssert, CVC3::Theorem::isRefl(), d_rules, CVC3::CoreProofRules::rewriteIteCond(), CVC3::TheoryCore::simplify(), CVC3::Expr::getKind(), ITE, CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::iffExpr(), CVC3::Expr::eqExpr(), CVC3::CoreProofRules::dummyTheorem(), AND, CVC3::Expr::arity(), CVC3::Theory::getEM(), CVC3::ExprManager::falseExpr(), OR, CVC3::ExprManager::trueExpr(), and substitute().
Referenced by preprocess().
TheoryCore* CVC3::ExprTransform::d_core [private] |
Definition at line 37 of file expr_transform.h.
Referenced by ExprTransform(), smartSimplify(), preprocess(), pushNegationRec(), specialSimplify(), newPPrec(), and simplifyWithCare().
TheoryArith* CVC3::ExprTransform::d_theoryArith [private] |
Definition at line 38 of file expr_transform.h.
Referenced by simplifyWithCare(), and setTheoryArith().
Definition at line 39 of file expr_transform.h.
Referenced by ExprTransform(), preprocess(), pushNegation(), pushNegationRec(), pushNegation1(), newPP(), specialSimplify(), newPPrec(), substitute(), and simplifyWithCare().
CoreProofRules* CVC3::ExprTransform::d_rules [private] |
Definition at line 40 of file expr_transform.h.
Referenced by ExprTransform(), pushNegationRec(), pushNegation1(), newPPrec(), 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 preprocess(), newPP(), and newPPrec().