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