CVC3
Public Member Functions | Private Member Functions | Private Attributes

LFSCConvert Class Reference

#include <LFSCConvert.h>

Inherits LFSCObj.

Collaboration diagram for LFSCConvert:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Definition at line 6 of file LFSCConvert.h.

Constructor & Destructor Documentation

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 ignore_theory_lemmas, LFSCObj::lfsc_mode, nodeCount, nodeCountTh, unodeCount, and unodeCountTh.

Member Function Documentation

bool LFSCConvert::isTrivialTheoryAxiom ( const Expr &  expr,
bool  checkBody = false 
) [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().

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

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 CVC3::abs(), AND, CVC3::Expr::arity(), 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(), getLFSCProof(), TReturn::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, LFSCLem::Make(), LFSCAssume::Make(), LFSCProofExpr::Make(), LFSCLraContra::Make(), LFSCProofGeneric::Make(), LFSCLraSub::Make(), LFSCLraAdd::Make(), LFSCLraMulC::Make(), LFSCLraPoly::Make(), LFSCPfVar::Make(), LFSCBoolRes::Make(), LFSCClausify::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(), TRUE_EXPR, CVC3::ExprManager::trueExpr(), CVC3::UMINUS, unodeCount, unodeCountTh, vMap, and LFSCObj::what_is_proven().

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 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(), LFSCProofGeneric::Make(), LFSCProofExpr::Make(), LFSCLraMulC::Make(), LFSCLraSub::Make(), LFSCLraAdd::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().

int LFSCConvert::get_proof_pattern ( const Expr &  pf,
Expr &  modE 
) [private]

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

LFSCProof * LFSCConvert::make_let_proof ( LFSCProof *  p) [private]

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(), LFSCPfLet::Make(), LFSCPfVar::Make(), and LFSCProof::make_lambda().

Referenced by convert().

TReturn * LFSCConvert::make_trusted ( const Expr &  pf) [private]

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.

LFSCProof* LFSCConvert::getLFSCProof ( ) [inline]

Definition at line 51 of file LFSCConvert.h.

References RefPtr< T >::get(), and pfinal.

Referenced by cvc3_to_lfsc().

Member Data Documentation

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 cvc3_to_lfsc(), and LFSCConvert().

int LFSCConvert::nodeCountTh [private]

Definition at line 19 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().

int LFSCConvert::unodeCount [private]

Definition at line 20 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().

int LFSCConvert::unodeCountTh [private]

Definition at line 21 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().

bool LFSCConvert::ignore_theory_lemmas [private]

Definition at line 23 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().

The documentation for this class was generated from the following files:
Generated on Thu Sep 1 2011 19:35:08 for CVC3 by  doxygen 1.7.3