CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes
LFSCConvert Class Reference

#include <LFSCConvert.h>

Inheritance diagram for LFSCConvert:
LFSCObj Obj

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Constructor & Destructor Documentation

virtual LFSCConvert::~LFSCConvert ( ) [inline, private, virtual]

Definition at line 45 of file LFSCConvert.h.

LFSCConvert::LFSCConvert ( int  lfscm)

Member Function Documentation

bool LFSCConvert::isTrivialTheoryAxiom ( const Expr expr,
bool  checkBody = false 
) [private]
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]
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]
int LFSCConvert::get_proof_pattern ( const Expr pf,
Expr modE 
) [private]
LFSCProof * LFSCConvert::make_let_proof ( LFSCProof p) [private]
TReturn * LFSCConvert::make_trusted ( const Expr pf) [private]
void LFSCConvert::convert ( const Expr pf)
LFSCProof* LFSCConvert::getLFSCProof ( ) [inline]

Definition at line 51 of file LFSCConvert.h.

References pfinal, and RefPtr::get().

Referenced by cvc3_to_lfsc().


Member Data Documentation

Definition at line 10 of file LFSCConvert.h.

Referenced by convert(), and getLFSCProof().

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

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

Definition at line 21 of file LFSCConvert.h.

Referenced by LFSCConvert(), and cvc3_to_lfsc().

Definition at line 23 of file LFSCConvert.h.

Referenced by LFSCConvert(), and cvc3_to_lfsc().


The documentation for this class was generated from the following files: