CVC3
|
#include <LFSCObject.h>
Inherits Obj.
Inherited by LFSCConvert, LFSCPrinter, LFSCProof, and TReturn.
Public Member Functions | |
LFSCObj () | |
![]() | |
Obj () | |
virtual | ~Obj () |
int | GetRefCount () |
get ref count | |
void | Ref () |
reference | |
void | Unref () |
unreference | |
Static Public Member Functions | |
static void | initialize (const Expr &pf_expr, int lfscm) |
![]() | |
static void | print_error (const char *c, std::ostream &s) |
static void | print_warning (const char *c) |
static void | initialize () |
Static Protected Member Functions | |
static int | getNumNodes (const Expr &pf, bool recount=false) |
static Expr | cascade_expr (const Expr &e) |
static void | define_skolem_vars (const Expr &e) |
static bool | isVar (const Expr &e) |
static void | collect_vars (const Expr &e, bool readPred=true) |
static Expr | queryElimNotNot (const Expr &expr) |
static Expr | queryAtomic (const Expr &expr, bool getBase=false) |
static int | queryM (const Expr &expr, bool add=true, bool trusted=false) |
static int | queryMt (const Expr &expr) |
static int | queryT (const Expr &e) |
static bool | getY (const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true) |
static bool | isFormula (const Expr &e) |
static bool | can_pnorm (const Expr &e) |
static bool | what_is_proven (const Expr &pf, Expr &pe) |
Additional Inherited Members | |
![]() | |
void | indent (std::ostream &s, int ind=0) |
![]() | |
ostringstream | oignore |
int | refCount |
Definition at line 9 of file LFSCObject.h.
|
inline |
Definition at line 12 of file LFSCObject.h.
|
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().
|
staticprotected |
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().
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(), LFSCBoolRes::Make(), LFSCClausify::Make(), LFSCProof::Make_and_elim(), LFSCProof::Make_CNF(), LFSCPrinter::print_formula(), LFSCPrinter::print_LFSC(), LFSCPrinter::print_terms(), queryAtomic(), queryM(), queryMt(), and queryT().
|
staticprotected |
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().
|
staticprotected |
Definition at line 337 of file LFSCObject.cpp.
References d_rules, CVC3::Expr::getKind(), and UCONST.
Referenced by collect_vars().
|
staticprotected |
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().
Definition at line 356 of file LFSCObject.cpp.
References CVC3::Expr::isNot().
Referenced by TReturn::normalize_tr(), queryAtomic(), queryM(), and what_is_proven().
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().
|
staticprotected |
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(), LFSCBoolRes::Make(), LFSCClausify::Make(), LFSCLraPoly::Make(), LFSCProof::Make_CNF(), LFSCClausify::Make_i(), LFSCConvert::make_trusted(), LFSCBoolRes::MakeC(), TReturn::normalize_to_tf(), TReturn::normalize_tr(), and LFSCPrinter::print_LFSC().
|
staticprotected |
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().
|
staticprotected |
Definition at line 436 of file LFSCObject.cpp.
References cascade_expr(), d_terms, and term_i.
Referenced by can_pnorm(), and define_skolem_vars().
|
staticprotected |
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().
|
staticprotected |
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().
|
staticprotected |
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().
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().
|
staticprotected |
Definition at line 16 of file LFSCObject.h.
Referenced by LFSCProofExpr::initialize(), LFSCPrinter::LFSCPrinter(), TReturn::normalize_tr(), and LFSCProofExpr::print_pf().
|
staticprotected |
Definition at line 18 of file LFSCObject.h.
Referenced by queryM().
|
staticprotected |
Definition at line 19 of file LFSCObject.h.
Referenced by queryM().
|
staticprotected |
Definition at line 20 of file LFSCObject.h.
Referenced by queryT().
|
staticprotected |
Definition at line 21 of file LFSCObject.h.
Referenced by queryMt().
|
staticprotected |
Definition at line 23 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::LFSCConvert(), and LFSCPrinter::print_LFSC().
|
staticprotected |
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().
|
staticprotected |
Definition at line 25 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().
|
staticprotected |
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().
|
staticprotected |
Definition at line 27 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().
|
staticprotected |
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().
|
staticprotected |
Definition at line 31 of file LFSCObject.h.
Referenced by getNumNodes().
Definition at line 34 of file LFSCObject.h.
Referenced by cascade_expr().
Definition at line 37 of file LFSCObject.h.
Referenced by cascade_expr(), define_skolem_vars(), and LFSCPrinter::print_poly_norm().
|
staticprotected |
Definition at line 38 of file LFSCObject.h.
Referenced by define_skolem_vars().
|
staticprotected |
Definition at line 46 of file LFSCObject.h.
Referenced by LFSCPrinter::print_LFSC(), and queryM().
|
staticprotected |
Definition at line 48 of file LFSCObject.h.
Referenced by LFSCPrinter::print_LFSC(), and queryM().
|
staticprotected |
Definition at line 50 of file LFSCObject.h.
Referenced by LFSCPrinter::print_LFSC(), and queryMt().
|
staticprotected |
Definition at line 52 of file LFSCObject.h.
Referenced by LFSCLraPoly::Make(), and LFSCPrinter::print_LFSC().
|
staticprotected |
Definition at line 54 of file LFSCObject.h.
Referenced by LFSCPrinter::print_LFSC(), LFSCPrinter::print_poly_norm(), and queryT().
|
staticprotected |
Definition at line 56 of file LFSCObject.h.
Referenced by collect_vars(), and LFSCPrinter::print_LFSC().
|
staticprotected |
Definition at line 58 of file LFSCObject.h.
Referenced by can_pnorm(), collect_vars(), isFormula(), and LFSCPrinter::print_LFSC().
|
staticprotected |
Definition at line 60 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCPrinter::print_LFSC().
|
staticprotected |
Definition at line 62 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCPrinter::print_LFSC().
|
staticprotected |
Definition at line 64 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), getY(), initialize(), queryAtomic(), and what_is_proven().
|
staticprotected |
Definition at line 66 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), and LFSCPrinter::print_LFSC().
|
staticprotected |
Definition at line 90 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), getNumNodes(), initialize(), isVar(), and what_is_proven().
|
staticprotected |
Definition at line 92 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().
|
staticprotected |
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().
|
staticprotected |
Definition at line 95 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::get_proof_pattern(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 96 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 97 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 98 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 99 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 100 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 101 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 102 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 103 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 104 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 105 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::get_proof_pattern(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 106 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 107 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 108 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 109 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), and initialize().
|
staticprotected |
Definition at line 110 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 111 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 112 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 113 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 114 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 115 of file LFSCObject.h.
Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().
|
staticprotected |
Definition at line 116 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 117 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 118 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 119 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 120 of file LFSCObject.h.
Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().
|
staticprotected |
Definition at line 121 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 122 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 123 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 124 of file LFSCObject.h.
Referenced by initialize().
|
staticprotected |
Definition at line 125 of file LFSCObject.h.
Referenced by initialize().
|
staticprotected |
Definition at line 126 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 127 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 128 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 129 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 130 of file LFSCObject.h.
Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().
|
staticprotected |
Definition at line 131 of file LFSCObject.h.
Referenced by initialize().
|
staticprotected |
Definition at line 132 of file LFSCObject.h.
Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().
|
staticprotected |
Definition at line 133 of file LFSCObject.h.
Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().
|
staticprotected |
Definition at line 134 of file LFSCObject.h.
Referenced by initialize(), and LFSCConvert::isIgnoredRule().
|
staticprotected |
Definition at line 135 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 136 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialBooleanAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 137 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 138 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 139 of file LFSCObject.h.
Referenced by LFSCConvert::get_proof_pattern(), and initialize().
|
staticprotected |
Definition at line 140 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().
|
staticprotected |
Definition at line 141 of file LFSCObject.h.
Referenced by LFSCConvert::get_proof_pattern(), and initialize().
|
staticprotected |
Definition at line 142 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 143 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 144 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 145 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 146 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 147 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), LFSCConvert::isTrivialTheoryAxiom(), and what_is_proven().
|
staticprotected |
Definition at line 148 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 149 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 150 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 151 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 152 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().
|
staticprotected |
Definition at line 154 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().
|
staticprotected |
Definition at line 155 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::get_proof_pattern(), initialize(), and what_is_proven().
|
staticprotected |
Definition at line 156 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().
|
staticprotected |
Definition at line 158 of file LFSCObject.h.
Referenced by initialize(), and LFSCProof::Make_CNF().
|
staticprotected |
Definition at line 159 of file LFSCObject.h.
Referenced by initialize(), and LFSCProof::Make_CNF().
|
staticprotected |
Definition at line 160 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().
|
staticprotected |
Definition at line 161 of file LFSCObject.h.
Referenced by initialize(), and LFSCProof::Make_CNF().
|
staticprotected |
Definition at line 162 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().
|
staticprotected |
Definition at line 163 of file LFSCObject.h.
Referenced by initialize(), and LFSCProof::Make_CNF().
|
staticprotected |
Definition at line 164 of file LFSCObject.h.
Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().