CVC3
Public Member Functions | Static Public Member Functions | Static Protected Member Functions | Static Protected Attributes

LFSCObj Class Reference

#include <LFSCObject.h>

Inherits Obj.

Inherited by LFSCConvert, LFSCPrinter, LFSCProof, and TReturn.

Collaboration diagram for LFSCObj:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Static Public Member Functions

Static Protected Member Functions

Static Protected Attributes

Detailed Description

Definition at line 9 of file LFSCObject.h.

Constructor & Destructor Documentation

LFSCObj::LFSCObj ( ) [inline]

Definition at line 12 of file LFSCObject.h.

Member Function Documentation

void LFSCObj::initialize ( const Expr &  pf_expr,
int  lfscm 
) [static]

Definition at line 104 of file LFSCObject.cpp.

References cvc3_mimic, cvc3_mimic_input, d_addInequalities_str, d_and_final_s, d_and_mid_s, d_andE_str, d_assump_str, d_basic_subst_op0_str, d_basic_subst_op1_str, d_basic_subst_op_str, d_bool_res_str, d_canon_invert_divide_str, d_canon_mult_str, d_canon_plus_str, d_cnf_add_unit_str, d_cnf_convert_str, d_CNF_str, d_CNFITE_str, d_const_predicate_str, d_cycle_conflict_str, d_eq_symm_str, d_eq_trans_str, d_flip_inequality_str, d_if_lift_rule_str, d_iff_false_elim_str, d_iff_false_str, d_iff_mp_str, d_iff_not_false_str, d_iff_s, d_iff_symm_str, d_iff_trans_str, d_iff_true_elim_str, d_iff_true_str, d_imp_mp_str, d_imp_s, d_impl_mp_str, d_implyEqualities_str, d_implyNegatedInequality_str, d_implyWeakerInequality_str, d_implyWeakerInequalityDiffLogic_str, d_int_const_eq_str, d_ite_s, d_learned_clause_str, d_lessThan_To_LE_rhs_rwr_str, d_minisat_proof_str, d_minus_to_plus_str, d_mult_eqn_str, d_mult_ineqn_str, d_negated_inequality_str, d_not_not_elim_str, d_not_to_iff_str, d_optimized_subst_op_str, d_or_final_s, d_or_mid_s, d_pf_expr, d_plus_predicate_str, d_real_shadow_eq_str, d_real_shadow_str, d_refl_str, d_rewrite_and_str, d_rewrite_eq_refl_str, d_rewrite_eq_symm_str, d_rewrite_iff_str, d_rewrite_iff_symm_str, d_rewrite_implies_str, d_rewrite_ite_same_str, d_rewrite_not_false_str, d_rewrite_not_not_str, d_rewrite_not_true_str, d_rewrite_or_str, d_right_minus_left_str, d_rules, d_uminus_to_mult_str, d_var_intro_str, debug_conv, debug_var, CVC3::Expr::getEM(), lfsc_mode, CVC3::ExprManager::newStringExpr(), and CVC3::ExprManager::newVarExpr().

int LFSCObj::getNumNodes ( const Expr &  pf,
bool  recount = false 
) [static, protected]

Definition at line 263 of file LFSCObject.cpp.

References CVC3::Expr::arity(), d_rules, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), and nnode_map.

Referenced by LFSCConvert::cvc3_to_lfsc().

Expr LFSCObj::cascade_expr ( const Expr &  e) [static, protected]

Definition at line 281 of file LFSCObject.cpp.

References CVC3::Expr::arity(), cas_map, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getKind(), ITE, SKOLEM_VAR, and skolem_vars.

Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), LFSCConvert::do_bso(), LFSCPrinter::LFSCPrinter(), LFSCProofExpr::LFSCProofExpr(), LFSCClausify::Make(), LFSCBoolRes::Make(), LFSCProof::Make_and_elim(), LFSCProof::Make_CNF(), LFSCPrinter::print_formula(), LFSCPrinter::print_LFSC(), LFSCPrinter::print_terms(), queryAtomic(), queryM(), queryMt(), and queryT().

void LFSCObj::define_skolem_vars ( const Expr &  e) [static, protected]

Definition at line 308 of file LFSCObject.cpp.

References CVC3::Expr::arity(), cascade_expr(), d_assump_map, d_assump_str, d_learned_clause_str, d_rules, CVC3::Expr::getKind(), CVC3::Expr::isEq(), Obj::print_error(), queryT(), SKOLEM_VAR, skolem_vars, and temp_visited.

Referenced by LFSCPrinter::print_LFSC().

bool LFSCObj::isVar ( const Expr &  e) [static, protected]

Definition at line 337 of file LFSCObject.cpp.

References d_rules, CVC3::Expr::getKind(), and UCONST.

Referenced by collect_vars().

void LFSCObj::collect_vars ( const Expr &  e,
bool  readPred = true 
) [static, protected]

Definition at line 342 of file LFSCObject.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getKind(), input_preds, input_vars, is_eq_kind(), isVar(), and ITE.

Referenced by LFSCPrinter::print_LFSC().

Expr LFSCObj::queryElimNotNot ( const Expr &  expr) [static, protected]

Definition at line 356 of file LFSCObject.cpp.

References CVC3::Expr::isNot().

Referenced by TReturn::normalize_tr(), queryAtomic(), queryM(), and what_is_proven().

Expr LFSCObj::queryAtomic ( const Expr &  expr,
bool  getBase = false 
) [static, protected]

Definition at line 365 of file LFSCObject.cpp.

References cascade_expr(), d_pf_expr, CVC3::ExprManager::falseExpr(), get_not(), CVC3::Expr::getEM(), is_eq_kind(), CVC3::Expr::isNot(), queryElimNotNot(), and CVC3::ExprManager::trueExpr().

Referenced by LFSCConvert::cvc3_to_lfsc(), getY(), LFSCLraPoly::Make(), TReturn::normalize_to_tf(), and TReturn::normalize_tr().

int LFSCObj::queryM ( const Expr &  expr,
bool  add = true,
bool  trusted = false 
) [static, protected]

Definition at line 386 of file LFSCObject.cpp.

References cascade_expr(), d_formulas, d_trusted, formula_i, CVC3::Expr::isInitialized(), CVC3::Expr::isNot(), Obj::print_error(), queryElimNotNot(), and trusted_i.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCLraPoly::Make(), LFSCClausify::Make(), LFSCBoolRes::Make(), LFSCProof::Make_CNF(), LFSCClausify::Make_i(), LFSCConvert::make_trusted(), LFSCBoolRes::MakeC(), TReturn::normalize_to_tf(), TReturn::normalize_tr(), and LFSCPrinter::print_LFSC().

int LFSCObj::queryMt ( const Expr &  expr) [static, protected]

Definition at line 418 of file LFSCObject.cpp.

References can_pnorm(), cascade_expr(), d_pn, std::endl(), Obj::print_error(), and tnorm_i.

Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCLraPoly::Make().

int LFSCObj::queryT ( const Expr &  e) [static, protected]

Definition at line 436 of file LFSCObject.cpp.

References cascade_expr(), d_terms, and term_i.

Referenced by can_pnorm(), and define_skolem_vars().

bool LFSCObj::getY ( const Expr &  e,
Expr &  pe,
bool  doIff = true,
bool  doLogic = true 
) [static, protected]

Definition at line 448 of file LFSCObject.cpp.

References CVC3::Expr::arity(), can_pnorm(), d_pf_expr, std::endl(), EQ, FALSE_EXPR, CVC3::GE, get_normalized(), CVC3::Expr::getEM(), CVC3::Expr::getKind(), CVC3::GT, is_comparison(), is_eq_kind(), is_opposite(), CVC3::Expr::isFalse(), CVC3::Expr::isIff(), CVC3::Expr::isImpl(), CVC3::Expr::isTrue(), CVC3::MINUS, Obj::print_error(), queryAtomic(), TRUE_EXPR, and CVC3::ExprManager::trueExpr().

Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCConvert::isTrivialTheoryAxiom().

bool LFSCObj::isFormula ( const Expr &  e) [static, protected]

Definition at line 514 of file LFSCObject.cpp.

References CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getKind(), input_preds, is_eq_kind(), CVC3::Expr::isAnd(), CVC3::Expr::isFalse(), CVC3::Expr::isIff(), CVC3::Expr::isImpl(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Expr::isTrue(), and ITE.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCPrinter::print_expr(), LFSCPrinter::print_LFSC(), and what_is_proven().

bool LFSCObj::can_pnorm ( const Expr &  e) [static, protected]

Definition at line 520 of file LFSCObject.cpp.

References CVC3::DIVIDE, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getKind(), input_preds, is_eq_kind(), CVC3::Expr::isRational(), CVC3::Expr::isVar(), ITE, CVC3::MINUS, CVC3::MULT, CVC3::PLUS, queryT(), and CVC3::UMINUS.

Referenced by getY(), TReturn::normalize_tr(), and queryMt().

bool LFSCObj::what_is_proven ( const Expr &  pf,
Expr &  pe 
) [static, protected]

Definition at line 539 of file LFSCObject.cpp.

References AND, CVC3::Expr::arity(), d_andE_str, d_assump_str, d_basic_subst_op0_str, d_basic_subst_op1_str, d_basic_subst_op_str, d_canon_invert_divide_str, d_canon_mult_str, d_canon_plus_str, d_cnf_add_unit_str, d_cnf_convert_str, d_const_predicate_str, d_cycle_conflict_str, d_eq_symm_str, d_eq_trans_str, d_flip_inequality_str, d_iff_false_elim_str, d_iff_mp_str, d_iff_not_false_str, d_iff_symm_str, d_iff_trans_str, d_iff_true_elim_str, d_iff_true_str, d_impl_mp_str, d_implyEqualities_str, d_implyNegatedInequality_str, d_implyWeakerInequality_str, d_int_const_eq_str, d_lessThan_To_LE_rhs_rwr_str, d_minus_to_plus_str, d_mult_eqn_str, d_mult_ineqn_str, d_negated_inequality_str, d_not_to_iff_str, d_optimized_subst_op_str, d_pf_expr, d_plus_predicate_str, d_real_shadow_eq_str, d_real_shadow_str, d_refl_str, d_rewrite_and_str, d_rewrite_eq_refl_str, d_rewrite_eq_symm_str, d_rewrite_iff_str, d_rewrite_iff_symm_str, d_rewrite_implies_str, d_rewrite_ite_same_str, d_rewrite_not_false_str, d_rewrite_not_not_str, d_rewrite_not_true_str, d_rewrite_or_str, d_right_minus_left_str, d_rules, d_uminus_to_mult_str, EQ, CVC3::ExprManager::falseExpr(), get_not(), CVC3::Expr::getEM(), CVC3::Rational::getInt(), CVC3::Rational::getNumerator(), CVC3::Expr::getRational(), IFF, CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), IMPLIES, is_eq_kind(), isFormula(), ITE, CVC3::LE, CVC3::LT, CVC3::MINUS, CVC3::MULT, CVC3::ExprManager::newRatExpr(), NOT, OR, CVC3::PLUS, Obj::print_error(), queryElimNotNot(), CVC3::ExprManager::trueExpr(), UCONST, and CVC3::UMINUS.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCConvert::isTrivialTheoryAxiom(), LFSCConvert::make_trusted(), and TReturn::normalize_tr().

Member Data Documentation

LFSCPrinter * LFSCObj::printer [static, protected]

Definition at line 16 of file LFSCObject.h.

Referenced by LFSCProofExpr::initialize(), LFSCPrinter::LFSCPrinter(), TReturn::normalize_tr(), and LFSCProofExpr::print_pf().

int LFSCObj::formula_i = 1 [static, protected]

Definition at line 18 of file LFSCObject.h.

Referenced by queryM().

int LFSCObj::trusted_i = 1 [static, protected]

Definition at line 19 of file LFSCObject.h.

Referenced by queryM().

int LFSCObj::term_i = 1 [static, protected]

Definition at line 20 of file LFSCObject.h.

Referenced by queryT().

int LFSCObj::tnorm_i = 1 [static, protected]

Definition at line 21 of file LFSCObject.h.

Referenced by queryMt().

int LFSCObj::lfsc_mode [static, protected]

Definition at line 23 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::LFSCConvert(), and LFSCPrinter::print_LFSC().

bool LFSCObj::debug_conv [static, protected]

Definition at line 24 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), initialize(), LFSCConvert::make_let_proof(), TReturn::normalize_tr(), and TReturn::normalize_tret().

bool LFSCObj::debug_var [static, protected]

Definition at line 25 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

bool LFSCObj::cvc3_mimic [static, protected]

Definition at line 26 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCPrinter::print_LFSC(), LFSCPrinter::print_poly_norm(), and LFSCPrinter::print_terms_h().

bool LFSCObj::cvc3_mimic_input [static, protected]

Definition at line 27 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Rational LFSCObj::nullRat [static, protected]

Definition at line 29 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCConvert::make_trusted(), TReturn::normalize_to_tf(), and TReturn::normalize_tr().

ExprMap< int > LFSCObj::nnode_map [static, protected]

Definition at line 31 of file LFSCObject.h.

Referenced by getNumNodes().

ExprMap< Expr > LFSCObj::cas_map [static, protected]

Definition at line 34 of file LFSCObject.h.

Referenced by cascade_expr().

ExprMap< Expr > LFSCObj::skolem_vars [static, protected]

Definition at line 37 of file LFSCObject.h.

Referenced by cascade_expr(), define_skolem_vars(), and LFSCPrinter::print_poly_norm().

ExprMap< bool > LFSCObj::temp_visited [static, protected]

Definition at line 38 of file LFSCObject.h.

Referenced by define_skolem_vars().

ExprMap< int > LFSCObj::d_formulas [static, protected]

Definition at line 46 of file LFSCObject.h.

Referenced by LFSCPrinter::print_LFSC(), and queryM().

ExprMap< int > LFSCObj::d_trusted [static, protected]

Definition at line 48 of file LFSCObject.h.

Referenced by LFSCPrinter::print_LFSC(), and queryM().

ExprMap< int > LFSCObj::d_pn [static, protected]

Definition at line 50 of file LFSCObject.h.

Referenced by LFSCPrinter::print_LFSC(), and queryMt().

ExprMap< int > LFSCObj::d_pn_form [static, protected]

Definition at line 52 of file LFSCObject.h.

Referenced by LFSCLraPoly::Make(), and LFSCPrinter::print_LFSC().

ExprMap< int > LFSCObj::d_terms [static, protected]

Definition at line 54 of file LFSCObject.h.

Referenced by LFSCPrinter::print_LFSC(), LFSCPrinter::print_poly_norm(), and queryT().

ExprMap< bool > LFSCObj::input_vars [static, protected]

Definition at line 56 of file LFSCObject.h.

Referenced by collect_vars(), and LFSCPrinter::print_LFSC().

ExprMap< bool > LFSCObj::input_preds [static, protected]

Definition at line 58 of file LFSCObject.h.

Referenced by can_pnorm(), collect_vars(), isFormula(), and LFSCPrinter::print_LFSC().

std::map< int, bool > LFSCObj::pntNeeded [static, protected]

Definition at line 60 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCPrinter::print_LFSC().

ExprMap< bool > LFSCObj::d_formulas_printed [static, protected]

Definition at line 62 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCPrinter::print_LFSC().

Expr LFSCObj::d_pf_expr [static, protected]

Definition at line 64 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), getY(), initialize(), queryAtomic(), and what_is_proven().

ExprMap< bool > LFSCObj::d_assump_map [static, protected]

Definition at line 66 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), and LFSCPrinter::print_LFSC().

ExprMap< bool > LFSCObj::d_rules [static, protected]

Definition at line 90 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), getNumNodes(), initialize(), isVar(), and what_is_proven().

Expr LFSCObj::d_bool_res_str [static, protected]

Definition at line 92 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_assump_str [static, protected]

Definition at line 93 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), LFSCConvert::get_proof_pattern(), initialize(), and what_is_proven().

Expr LFSCObj::d_iff_mp_str [static, protected]

Definition at line 95 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::get_proof_pattern(), initialize(), and what_is_proven().

Expr LFSCObj::d_impl_mp_str [static, protected]

Definition at line 96 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_iff_trans_str [static, protected]

Definition at line 97 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_real_shadow_str [static, protected]

Definition at line 98 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_cycle_conflict_str [static, protected]

Definition at line 99 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_real_shadow_eq_str [static, protected]

Definition at line 100 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_basic_subst_op_str [static, protected]

Definition at line 101 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_mult_ineqn_str [static, protected]

Definition at line 102 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_right_minus_left_str [static, protected]

Definition at line 103 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_eq_trans_str [static, protected]

Definition at line 104 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_eq_symm_str [static, protected]

Definition at line 105 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::get_proof_pattern(), initialize(), and what_is_proven().

Expr LFSCObj::d_canon_plus_str [static, protected]

Definition at line 106 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_refl_str [static, protected]

Definition at line 107 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_cnf_convert_str [static, protected]

Definition at line 108 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_learned_clause_str [static, protected]

Definition at line 109 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), and initialize().

Expr LFSCObj::d_minus_to_plus_str [static, protected]

Definition at line 110 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_plus_predicate_str [static, protected]

Definition at line 111 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_negated_inequality_str [static, protected]

Definition at line 112 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_flip_inequality_str [static, protected]

Definition at line 113 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_optimized_subst_op_str [static, protected]

Definition at line 114 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_iff_true_elim_str [static, protected]

Definition at line 115 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_basic_subst_op1_str [static, protected]

Definition at line 116 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_basic_subst_op0_str [static, protected]

Definition at line 117 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_canon_mult_str [static, protected]

Definition at line 118 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_canon_invert_divide_str [static, protected]

Definition at line 119 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_iff_true_str [static, protected]

Definition at line 120 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_mult_eqn_str [static, protected]

Definition at line 121 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_rewrite_eq_symm_str [static, protected]

Definition at line 122 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_implyWeakerInequality_str [static, protected]

Definition at line 123 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_implyWeakerInequalityDiffLogic_str [static, protected]

Definition at line 124 of file LFSCObject.h.

Referenced by initialize().

Expr LFSCObj::d_imp_mp_str [static, protected]

Definition at line 125 of file LFSCObject.h.

Referenced by initialize().

Expr LFSCObj::d_rewrite_implies_str [static, protected]

Definition at line 126 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_or_str [static, protected]

Definition at line 127 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_and_str [static, protected]

Definition at line 128 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_iff_symm_str [static, protected]

Definition at line 129 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_iff_not_false_str [static, protected]

Definition at line 130 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_iff_false_str [static, protected]

Definition at line 131 of file LFSCObject.h.

Referenced by initialize().

Expr LFSCObj::d_iff_false_elim_str [static, protected]

Definition at line 132 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_not_to_iff_str [static, protected]

Definition at line 133 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_not_not_elim_str [static, protected]

Definition at line 134 of file LFSCObject.h.

Referenced by initialize(), and LFSCConvert::isIgnoredRule().

Expr LFSCObj::d_const_predicate_str [static, protected]

Definition at line 135 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_not_not_str [static, protected]

Definition at line 136 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialBooleanAxiom(), and what_is_proven().

Expr LFSCObj::d_rewrite_not_true_str [static, protected]

Definition at line 137 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_rewrite_not_false_str [static, protected]

Definition at line 138 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_if_lift_rule_str [static, protected]

Definition at line 139 of file LFSCObject.h.

Referenced by LFSCConvert::get_proof_pattern(), and initialize().

Expr LFSCObj::d_CNFITE_str [static, protected]

Definition at line 140 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_var_intro_str [static, protected]

Definition at line 141 of file LFSCObject.h.

Referenced by LFSCConvert::get_proof_pattern(), and initialize().

Expr LFSCObj::d_int_const_eq_str [static, protected]

Definition at line 142 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_rewrite_eq_refl_str [static, protected]

Definition at line 143 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_iff_symm_str [static, protected]

Definition at line 144 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_iff_str [static, protected]

Definition at line 145 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_implyNegatedInequality_str [static, protected]

Definition at line 146 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_uminus_to_mult_str [static, protected]

Definition at line 147 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().

Expr LFSCObj::d_lessThan_To_LE_rhs_rwr_str [static, protected]

Definition at line 148 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_ite_same_str [static, protected]

Definition at line 149 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_andE_str [static, protected]

Definition at line 150 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_implyEqualities_str [static, protected]

Definition at line 151 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_addInequalities_str [static, protected]

Definition at line 152 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_CNF_str [static, protected]

Definition at line 154 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_cnf_add_unit_str [static, protected]

Definition at line 155 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::get_proof_pattern(), initialize(), and what_is_proven().

Expr LFSCObj::d_minisat_proof_str [static, protected]

Definition at line 156 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_or_final_s [static, protected]

Definition at line 158 of file LFSCObject.h.

Referenced by initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_and_final_s [static, protected]

Definition at line 159 of file LFSCObject.h.

Referenced by initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_ite_s [static, protected]

Definition at line 160 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_iff_s [static, protected]

Definition at line 161 of file LFSCObject.h.

Referenced by initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_imp_s [static, protected]

Definition at line 162 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_or_mid_s [static, protected]

Definition at line 163 of file LFSCObject.h.

Referenced by initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_and_mid_s [static, protected]

Definition at line 164 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().

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