|
static LFSCProof * | Make (vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false) |
|
static LFSCProof * | Make (string str_pre, LFSCProof *sub_pf, string str_post, bool db_str=false) |
|
static LFSCProof * | Make (string str_pre, LFSCProof *sub_pf1, LFSCProof *sub_pf2, string str_post, bool db_str=false) |
|
static LFSCProof * | MakeStr (const char *c, bool db_str=false) |
|
static LFSCProof * | MakeUnk () |
|
static int | make_lambda (LFSCProof *p) |
|
static LFSCProof * | Make_CNF (const Expr &form, const Expr &reason, int pos) |
|
static LFSCProof * | Make_not_not_elim (const Expr &pf, LFSCProof *p) |
|
static LFSCProof * | Make_mimic (const Expr &pf, LFSCProof *p, int numHoles) |
|
static LFSCProof * | Make_and_elim (const Expr &form, LFSCProof *p, int n, const Expr &expected) |
|
static int | get_proof_counter () |
|
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 () |
|
|
| LFSCProof () |
|
virtual | ~LFSCProof () |
|
void | indent (std::ostream &s, int ind=0) |
|
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) |
|
int | printCounter |
|
LFSCProof * | rplProof |
|
long int | strLen |
|
int | chOp |
|
int | assumeVar |
|
int | assumeVarUsed |
|
std::vector< int > | br |
|
bool | brComputed |
|
ostringstream | oignore |
|
int | refCount |
|
static int | pf_counter = 0 |
|
static std::map< LFSCProof *, int > | lambdaMap |
|
static std::map< LFSCProof *, LFSCProof * > | lambdaPrintMap |
|
static int | lambdaCounter = 1 |
|
static LFSCPrinter * | printer |
|
static int | formula_i = 1 |
|
static int | trusted_i = 1 |
|
static int | term_i = 1 |
|
static int | tnorm_i = 1 |
|
static int | lfsc_mode |
|
static bool | debug_conv |
|
static bool | debug_var |
|
static bool | cvc3_mimic |
|
static bool | cvc3_mimic_input |
|
static Rational | nullRat |
|
static ExprMap< int > | nnode_map |
|
static ExprMap< Expr > | cas_map |
|
static ExprMap< Expr > | skolem_vars |
|
static ExprMap< bool > | temp_visited |
|
static ExprMap< int > | d_formulas |
|
static ExprMap< int > | d_trusted |
|
static ExprMap< int > | d_pn |
|
static ExprMap< int > | d_pn_form |
|
static ExprMap< int > | d_terms |
|
static ExprMap< bool > | input_vars |
|
static ExprMap< bool > | input_preds |
|
static std::map< int, bool > | pntNeeded |
|
static ExprMap< bool > | d_formulas_printed |
|
static Expr | d_pf_expr |
|
static ExprMap< bool > | d_assump_map |
|
static ExprMap< bool > | d_rules |
|
static Expr | d_bool_res_str |
|
static Expr | d_assump_str |
|
static Expr | d_iff_mp_str |
|
static Expr | d_impl_mp_str |
|
static Expr | d_iff_trans_str |
|
static Expr | d_real_shadow_str |
|
static Expr | d_cycle_conflict_str |
|
static Expr | d_real_shadow_eq_str |
|
static Expr | d_basic_subst_op_str |
|
static Expr | d_mult_ineqn_str |
|
static Expr | d_right_minus_left_str |
|
static Expr | d_eq_trans_str |
|
static Expr | d_eq_symm_str |
|
static Expr | d_canon_plus_str |
|
static Expr | d_refl_str |
|
static Expr | d_cnf_convert_str |
|
static Expr | d_learned_clause_str |
|
static Expr | d_minus_to_plus_str |
|
static Expr | d_plus_predicate_str |
|
static Expr | d_negated_inequality_str |
|
static Expr | d_flip_inequality_str |
|
static Expr | d_optimized_subst_op_str |
|
static Expr | d_iff_true_elim_str |
|
static Expr | d_basic_subst_op1_str |
|
static Expr | d_basic_subst_op0_str |
|
static Expr | d_canon_mult_str |
|
static Expr | d_canon_invert_divide_str |
|
static Expr | d_iff_true_str |
|
static Expr | d_mult_eqn_str |
|
static Expr | d_rewrite_eq_symm_str |
|
static Expr | d_implyWeakerInequality_str |
|
static Expr | d_implyWeakerInequalityDiffLogic_str |
|
static Expr | d_imp_mp_str |
|
static Expr | d_rewrite_implies_str |
|
static Expr | d_rewrite_or_str |
|
static Expr | d_rewrite_and_str |
|
static Expr | d_rewrite_iff_symm_str |
|
static Expr | d_iff_not_false_str |
|
static Expr | d_iff_false_str |
|
static Expr | d_iff_false_elim_str |
|
static Expr | d_not_to_iff_str |
|
static Expr | d_not_not_elim_str |
|
static Expr | d_const_predicate_str |
|
static Expr | d_rewrite_not_not_str |
|
static Expr | d_rewrite_not_true_str |
|
static Expr | d_rewrite_not_false_str |
|
static Expr | d_if_lift_rule_str |
|
static Expr | d_CNFITE_str |
|
static Expr | d_var_intro_str |
|
static Expr | d_int_const_eq_str |
|
static Expr | d_rewrite_eq_refl_str |
|
static Expr | d_iff_symm_str |
|
static Expr | d_rewrite_iff_str |
|
static Expr | d_implyNegatedInequality_str |
|
static Expr | d_uminus_to_mult_str |
|
static Expr | d_lessThan_To_LE_rhs_rwr_str |
|
static Expr | d_rewrite_ite_same_str |
|
static Expr | d_andE_str |
|
static Expr | d_implyEqualities_str |
|
static Expr | d_addInequalities_str |
|
static Expr | d_CNF_str |
|
static Expr | d_cnf_add_unit_str |
|
static Expr | d_minisat_proof_str |
|
static Expr | d_or_final_s |
|
static Expr | d_and_final_s |
|
static Expr | d_ite_s |
|
static Expr | d_iff_s |
|
static Expr | d_imp_s |
|
static Expr | d_or_mid_s |
|
static Expr | d_and_mid_s |
|
static bool | errsInit = false |
|
static ofstream | errs |
|
static bool | indentFlag = false |
|
Definition at line 61 of file LFSCUtilProof.h.