CVC3 2.4.1
Public Member Functions | Static Public Member Functions | Static Protected Member Functions | Static Protected Attributes
LFSCObj Class Reference

#include <LFSCObject.h>

Inheritance diagram for LFSCObj:
Obj LFSCConvert LFSCPrinter LFSCProof TReturn LFSCAssume LFSCBoolRes LFSCClausify LFSCLem LFSCLraAdd LFSCLraAxiom LFSCLraContra LFSCLraMulC LFSCLraPoly LFSCLraSub LFSCPfLambda LFSCPfLet LFSCPfVar LFSCProofExpr LFSCProofGeneric

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]
Expr LFSCObj::cascade_expr ( const Expr e) [static, protected]
void LFSCObj::define_skolem_vars ( const Expr e) [static, protected]
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]
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]
int LFSCObj::queryM ( const Expr expr,
bool  add = true,
bool  trusted = false 
) [static, protected]
int LFSCObj::queryMt ( const Expr expr) [static, protected]
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]
bool LFSCObj::isFormula ( const Expr e) [static, protected]
bool LFSCObj::can_pnorm ( const Expr e) [static, protected]
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]
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]
bool LFSCObj::debug_conv [static, protected]
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]
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]
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]
ExprMap< bool > LFSCObj::d_rules [static, protected]
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]
Expr LFSCObj::d_iff_mp_str [static, protected]
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]
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]
Expr LFSCObj::d_canon_plus_str [static, protected]
Expr LFSCObj::d_refl_str [static, protected]
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]
Expr LFSCObj::d_plus_predicate_str [static, protected]
Expr LFSCObj::d_flip_inequality_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]
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]
Expr LFSCObj::d_rewrite_eq_symm_str [static, protected]

Definition at line 123 of file LFSCObject.h.

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

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

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]
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]
Expr LFSCObj::d_rewrite_eq_refl_str [static, protected]
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().

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 148 of file LFSCObject.h.

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

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]
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: