CVC3
2.4.1
|
#include <LFSCConvert.h>
virtual LFSCConvert::~LFSCConvert | ( | ) | [inline, private, virtual] |
Definition at line 45 of file LFSCConvert.h.
LFSCConvert::LFSCConvert | ( | int | lfscm | ) |
Definition at line 9 of file LFSCConvert.cpp.
References nodeCount, nodeCountTh, unodeCount, unodeCountTh, ignore_theory_lemmas, and LFSCObj::lfsc_mode.
bool LFSCConvert::isTrivialTheoryAxiom | ( | const Expr & | expr, |
bool | checkBody = false |
||
) | [private] |
Definition at line 57 of file LFSCConvert.cpp.
References LFSCObj::d_plus_predicate_str, LFSCObj::d_right_minus_left_str, LFSCObj::d_minus_to_plus_str, LFSCObj::d_mult_ineqn_str, LFSCObj::d_canon_mult_str, LFSCObj::d_canon_plus_str, LFSCObj::d_flip_inequality_str, LFSCObj::d_negated_inequality_str, LFSCObj::d_rewrite_eq_symm_str, LFSCObj::d_refl_str, LFSCObj::d_mult_eqn_str, LFSCObj::d_canon_invert_divide_str, LFSCObj::d_rewrite_eq_refl_str, LFSCObj::d_uminus_to_mult_str, LFSCObj::d_rewrite_not_true_str, LFSCObj::d_rewrite_not_false_str, LFSCObj::d_int_const_eq_str, LFSCObj::what_is_proven(), and LFSCObj::getY().
Referenced by cvc3_to_lfsc().
bool LFSCConvert::isTrivialBooleanAxiom | ( | const Expr & | expr | ) | [private] |
Definition at line 79 of file LFSCConvert.cpp.
References LFSCObj::d_rewrite_not_not_str.
Referenced by cvc3_to_lfsc().
bool LFSCConvert::isIgnoredRule | ( | const Expr & | expr | ) | [private] |
Definition at line 86 of file LFSCConvert.cpp.
References LFSCObj::d_iff_not_false_str, LFSCObj::d_iff_true_str, LFSCObj::d_iff_false_elim_str, LFSCObj::d_iff_true_elim_str, LFSCObj::d_not_not_elim_str, and LFSCObj::d_not_to_iff_str.
Referenced by cvc3_to_lfsc().
TReturn * LFSCConvert::cvc3_to_lfsc | ( | const Expr & | pf, |
bool | beneath_lc = false , |
||
bool | rev_pol = false |
||
) | [private] |
Definition at line 93 of file LFSCConvert.cpp.
References nodeCountTh, nodeCount, LFSCObj::lfsc_mode, LFSCObj::cvc3_mimic, LFSCObj::cvc3_mimic_input, d_th_trans_map, d_th_trans_lam, LFSCObj::debug_conv, std::endl(), unodeCountTh, unodeCount, get_proof_pattern(), LFSCObj::d_CNF_str, LFSCProof::Make_CNF(), RefPtr::get(), LFSCObj::nullRat, LFSCObj::d_CNFITE_str, CVC3::isRational(), LFSCObj::d_ite_s, LFSCObj::d_cnf_add_unit_str, TReturn::normalize_tr(), LFSCObj::d_cnf_convert_str, ignore_theory_lemmas, LFSCObj::d_learned_clause_str, make_trusted(), LFSCClausify::Make(), TReturn::getLFSCProof(), LFSCObj::d_bool_res_str, TReturn::getProvesY(), LFSCBoolRes::Make(), LFSCObj::d_minisat_proof_str, LFSCObj::d_assump_str, LFSCObj::cascade_expr(), LFSCObj::queryM(), LFSCObj::d_assump_map, CVC3::ExprMap::find(), CVC3::ExprMap::end(), LFSCPfVar::Make(), CVC3::abs(), LFSCProof::Make_not_not_elim(), LFSCPfVar::MakeV(), LFSCObj::d_formulas_printed, LFSCObj::queryAtomic(), Obj::print_error(), LFSCObj::getY(), LFSCLraPoly::Make(), LFSCObj::d_iff_trans_str, isTrivialBooleanAxiom(), LFSCObj::d_rewrite_not_true_str, TReturn::getL(), TReturn::normalize_tret(), CVC3::Expr::getKind(), is_eq_kind(), TReturn::hasRational(), LFSCLraMulC::Make(), TReturn::getRational(), EQ, LFSCLraAdd::Make(), TReturn::mult_rational(), FALSE_EXPR, TRUE_EXPR, get_normalized(), LFSCLraSub::Make(), LFSCProofGeneric::Make(), LFSCObj::d_iff_mp_str, LFSCLraContra::Make(), is_comparison(), CVC3::GT, DISTINCT, LFSCObj::d_iff_symm_str, LFSCProof::Make_mimic(), LFSCObj::d_impl_mp_str, CVC3::GE, kind_to_str(), LFSCObj::d_basic_subst_op_str, LFSCObj::d_basic_subst_op1_str, IFF, AND, OR, LFSCObj::getNumNodes(), do_bso(), LFSCObj::d_basic_subst_op0_str, CVC3::UMINUS, LFSCObj::d_optimized_subst_op_str, ITE, LFSCProofExpr::Make(), LFSCObj::isFormula(), LFSCObj::what_is_proven(), CVC3::PLUS, LFSCObj::queryMt(), CVC3::MINUS, LFSCObj::pntNeeded, PF_APPLY, LFSCObj::d_eq_trans_str, LFSCObj::d_eq_symm_str, LFSCObj::d_real_shadow_str, LFSCObj::d_addInequalities_str, LFSCObj::d_real_shadow_eq_str, LFSCObj::d_cycle_conflict_str, getLFSCProof(), CVC3::Expr::isFalse(), LFSCAssume::Make(), LFSCObj::d_andE_str, LFSCProof::Make_and_elim(), LFSCObj::d_and_mid_s, LFSCObj::d_rewrite_implies_str, IMPLIES, LFSCObj::d_imp_s, LFSCObj::d_rewrite_ite_same_str, LFSCObj::d_rewrite_and_str, LFSCObj::d_rewrite_or_str, isFlat(), make_flatten_expr(), LFSCObj::d_rewrite_iff_symm_str, LFSCObj::d_implyEqualities_str, LFSCObj::d_implyWeakerInequality_str, LFSCLraAxiom::MakeEq(), getRat(), print_rational(), LFSCObj::d_implyNegatedInequality_str, CVC3::MULT, LFSCObj::d_rewrite_iff_str, LFSCObj::d_pf_expr, CVC3::Expr::getEM(), CVC3::ExprManager::trueExpr(), CVC3::ExprManager::falseExpr(), isIgnoredRule(), isTrivialTheoryAxiom(), LFSCObj::d_mult_ineqn_str, LFSCObj::d_mult_eqn_str, LFSCObj::d_rewrite_eq_symm_str, LFSCObj::d_int_const_eq_str, CVC3::Expr::arity(), LFSCObj::d_refl_str, LFSCObj::d_flip_inequality_str, LFSCObj::d_right_minus_left_str, LFSCObj::d_minus_to_plus_str, LFSCObj::d_plus_predicate_str, LFSCObj::d_canon_plus_str, LFSCObj::d_canon_mult_str, LFSCProofGeneric::MakeStr(), LFSCObj::d_canon_invert_divide_str, CVC3::ExprManager::newRatExpr(), LFSCObj::d_negated_inequality_str, get_not(), LFSCObj::d_rewrite_eq_refl_str, LFSCObj::d_uminus_to_mult_str, LFSCObj::d_rewrite_not_false_str, LFSCObj::d_lessThan_To_LE_rhs_rwr_str, LFSCObj::d_rewrite_not_not_str, LFSCLem::Make(), LFSCObj::d_const_predicate_str, LFSCObj::d_rules, LFSCProofGeneric::MakeUnk(), LFSCObj::debug_var, LFSCProof::isTrivial(), LFSCProof::get_string_length(), and d_th_trans.
Referenced by convert().
TReturn* LFSCConvert::cvc3_to_lfsc_h | ( | const Expr & | pf, |
bool | beneath_lc = false , |
||
bool | rev_pol = false |
||
) | [private] |
TReturn * LFSCConvert::do_bso | ( | const Expr & | pf, |
bool | beneath_lc, | ||
bool | rev_pol, | ||
TReturn * | t1, | ||
TReturn * | t2, | ||
ostringstream & | ose | ||
) | [private] |
Definition at line 1718 of file LFSCConvert.cpp.
References TReturn::getL(), CVC3::PLUS, CVC3::MINUS, CVC3::MULT, is_eq_kind(), TReturn::normalize_tret(), LFSCLraAdd::Make(), TReturn::getLFSCProof(), EQ, LFSCObj::nullRat, LFSCLraSub::Make(), std::endl(), getRat(), LFSCLraMulC::Make(), Obj::print_error(), is_opposite(), RefPtr::get(), LFSCObj::debug_conv, kind_to_str(), TReturn::getProvesY(), TReturn::normalize_tr(), OR, AND, IFF, LFSCProofExpr::Make(), LFSCObj::cascade_expr(), LFSCProofGeneric::Make(), CVC3::Expr::arity(), and LFSCObj::what_is_proven().
Referenced by cvc3_to_lfsc().
Definition at line 1641 of file LFSCConvert.cpp.
References LFSCObj::d_cnf_add_unit_str, LFSCObj::d_iff_mp_str, LFSCObj::d_eq_symm_str, LFSCObj::d_if_lift_rule_str, LFSCObj::d_var_intro_str, and LFSCObj::d_assump_str.
Referenced by cvc3_to_lfsc().
Definition at line 1663 of file LFSCConvert.cpp.
References LFSCObj::debug_conv, std::endl(), d_th_trans, CVC3::ExprMap::empty(), CVC3::ExprMap::begin(), CVC3::ExprMap::end(), d_th_trans_map, TReturn::getL(), d_th_trans_lam, LFSCProof::make_lambda(), LFSCPfVar::Make(), and LFSCPfLet::Make().
Referenced by convert().
Definition at line 1705 of file LFSCConvert.cpp.
References LFSCObj::what_is_proven(), LFSCObj::queryM(), LFSCPfVar::Make(), LFSCObj::nullRat, and LFSCProofGeneric::MakeStr().
Referenced by cvc3_to_lfsc().
void LFSCConvert::convert | ( | const Expr & | pf | ) |
Definition at line 18 of file LFSCConvert.cpp.
References cvc3_to_lfsc(), pfinal, TReturn::getLFSCProof(), TReturn::getProvesY(), std::endl(), LFSCProofGeneric::Make(), RefPtr::get(), and make_let_proof().
LFSCProof* LFSCConvert::getLFSCProof | ( | ) | [inline] |
Definition at line 51 of file LFSCConvert.h.
References pfinal, and RefPtr::get().
Referenced by cvc3_to_lfsc().
RefPtr< LFSCProof > LFSCConvert::pfinal [private] |
Definition at line 10 of file LFSCConvert.h.
Referenced by convert(), and getLFSCProof().
ExprMap<bool> LFSCConvert::d_th_trans [private] |
Definition at line 13 of file LFSCConvert.h.
Referenced by cvc3_to_lfsc(), and make_let_proof().
ExprMap<TReturn*> LFSCConvert::d_th_trans_map[2] [private] |
Definition at line 14 of file LFSCConvert.h.
Referenced by cvc3_to_lfsc(), and make_let_proof().
std::map<TReturn*, bool> LFSCConvert::d_th_trans_lam[2] [private] |
Definition at line 16 of file LFSCConvert.h.
Referenced by cvc3_to_lfsc(), and make_let_proof().
int LFSCConvert::nodeCount [private] |
Definition at line 18 of file LFSCConvert.h.
Referenced by LFSCConvert(), and cvc3_to_lfsc().
int LFSCConvert::nodeCountTh [private] |
Definition at line 19 of file LFSCConvert.h.
Referenced by LFSCConvert(), and cvc3_to_lfsc().
int LFSCConvert::unodeCount [private] |
Definition at line 20 of file LFSCConvert.h.
Referenced by LFSCConvert(), and cvc3_to_lfsc().
int LFSCConvert::unodeCountTh [private] |
Definition at line 21 of file LFSCConvert.h.
Referenced by LFSCConvert(), and cvc3_to_lfsc().
bool LFSCConvert::ignore_theory_lemmas [private] |
Definition at line 23 of file LFSCConvert.h.
Referenced by LFSCConvert(), and cvc3_to_lfsc().