, including all inherited members.
can_pnorm(const Expr &e) | LFSCObj | [protected, static] |
cas_map | LFSCObj | [protected, static] |
cascade_expr(const Expr &e) | LFSCObj | [protected, static] |
collect_vars(const Expr &e, bool readPred=true) | LFSCObj | [protected, static] |
cvc3_mimic | LFSCObj | [protected, static] |
cvc3_mimic_input | LFSCObj | [protected, static] |
d_addInequalities_str | LFSCObj | [protected, static] |
d_and_final_s | LFSCObj | [protected, static] |
d_and_mid_s | LFSCObj | [protected, static] |
d_andE_str | LFSCObj | [protected, static] |
d_assump_map | LFSCObj | [protected, static] |
d_assump_str | LFSCObj | [protected, static] |
d_basic_subst_op0_str | LFSCObj | [protected, static] |
d_basic_subst_op1_str | LFSCObj | [protected, static] |
d_basic_subst_op_str | LFSCObj | [protected, static] |
d_bool_res_str | LFSCObj | [protected, static] |
d_c | TReturn | [private] |
d_canon_invert_divide_str | LFSCObj | [protected, static] |
d_canon_mult_str | LFSCObj | [protected, static] |
d_canon_plus_str | LFSCObj | [protected, static] |
d_cnf_add_unit_str | LFSCObj | [protected, static] |
d_cnf_convert_str | LFSCObj | [protected, static] |
d_CNF_str | LFSCObj | [protected, static] |
d_CNFITE_str | LFSCObj | [protected, static] |
d_const_predicate_str | LFSCObj | [protected, static] |
d_cycle_conflict_str | LFSCObj | [protected, static] |
d_eq_symm_str | LFSCObj | [protected, static] |
d_eq_trans_str | LFSCObj | [protected, static] |
d_flip_inequality_str | LFSCObj | [protected, static] |
d_formulas | LFSCObj | [protected, static] |
d_formulas_printed | LFSCObj | [protected, static] |
d_hasRt | TReturn | [private] |
d_if_lift_rule_str | LFSCObj | [protected, static] |
d_iff_false_elim_str | LFSCObj | [protected, static] |
d_iff_false_str | LFSCObj | [protected, static] |
d_iff_mp_str | LFSCObj | [protected, static] |
d_iff_not_false_str | LFSCObj | [protected, static] |
d_iff_s | LFSCObj | [protected, static] |
d_iff_symm_str | LFSCObj | [protected, static] |
d_iff_trans_str | LFSCObj | [protected, static] |
d_iff_true_elim_str | LFSCObj | [protected, static] |
d_iff_true_str | LFSCObj | [protected, static] |
d_imp_mp_str | LFSCObj | [protected, static] |
d_imp_s | LFSCObj | [protected, static] |
d_impl_mp_str | LFSCObj | [protected, static] |
d_implyEqualities_str | LFSCObj | [protected, static] |
d_implyNegatedInequality_str | LFSCObj | [protected, static] |
d_implyWeakerInequality_str | LFSCObj | [protected, static] |
d_implyWeakerInequalityDiffLogic_str | LFSCObj | [protected, static] |
d_int_const_eq_str | LFSCObj | [protected, static] |
d_ite_s | LFSCObj | [protected, static] |
d_L | TReturn | [private] |
d_L_used | TReturn | [private] |
d_learned_clause_str | LFSCObj | [protected, static] |
d_lessThan_To_LE_rhs_rwr_str | LFSCObj | [protected, static] |
d_lfsc_pf | TReturn | [private] |
d_minisat_proof_str | LFSCObj | [protected, static] |
d_minus_to_plus_str | LFSCObj | [protected, static] |
d_mult_eqn_str | LFSCObj | [protected, static] |
d_mult_ineqn_str | LFSCObj | [protected, static] |
d_negated_inequality_str | LFSCObj | [protected, static] |
d_not_not_elim_str | LFSCObj | [protected, static] |
d_not_to_iff_str | LFSCObj | [protected, static] |
d_optimized_subst_op_str | LFSCObj | [protected, static] |
d_or_final_s | LFSCObj | [protected, static] |
d_or_mid_s | LFSCObj | [protected, static] |
d_pf_expr | LFSCObj | [protected, static] |
d_plus_predicate_str | LFSCObj | [protected, static] |
d_pn | LFSCObj | [protected, static] |
d_pn_form | LFSCObj | [protected, static] |
d_provesY | TReturn | [private] |
d_real_shadow_eq_str | LFSCObj | [protected, static] |
d_real_shadow_str | LFSCObj | [protected, static] |
d_refl_str | LFSCObj | [protected, static] |
d_rewrite_and_str | LFSCObj | [protected, static] |
d_rewrite_eq_refl_str | LFSCObj | [protected, static] |
d_rewrite_eq_symm_str | LFSCObj | [protected, static] |
d_rewrite_iff_str | LFSCObj | [protected, static] |
d_rewrite_iff_symm_str | LFSCObj | [protected, static] |
d_rewrite_implies_str | LFSCObj | [protected, static] |
d_rewrite_ite_same_str | LFSCObj | [protected, static] |
d_rewrite_not_false_str | LFSCObj | [protected, static] |
d_rewrite_not_not_str | LFSCObj | [protected, static] |
d_rewrite_not_true_str | LFSCObj | [protected, static] |
d_rewrite_or_str | LFSCObj | [protected, static] |
d_right_minus_left_str | LFSCObj | [protected, static] |
d_rules | LFSCObj | [protected, static] |
d_terms | LFSCObj | [protected, static] |
d_trusted | LFSCObj | [protected, static] |
d_uminus_to_mult_str | LFSCObj | [protected, static] |
d_var_intro_str | LFSCObj | [protected, static] |
debug_conv | LFSCObj | [protected, static] |
debug_var | LFSCObj | [protected, static] |
define_skolem_vars(const Expr &e) | LFSCObj | [protected, static] |
errs | Obj | [protected, static] |
errsInit | Obj | [protected, static] |
formula_i | LFSCObj | [protected, static] |
getL(std::vector< int > &lget, std::vector< int > &lgetu) | TReturn | |
getLFSCProof() | TReturn | [inline] |
getNumNodes(const Expr &pf, bool recount=false) | LFSCObj | [protected, static] |
getProvesY() | TReturn | [inline] |
getRational() | TReturn | [inline] |
GetRefCount() | Obj | [inline] |
getY(const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true) | LFSCObj | [protected, static] |
hasFv() | TReturn | [inline] |
hasRational() | TReturn | [inline] |
indent(std::ostream &s, int ind=0) | Obj | [inline, protected] |
indentFlag | Obj | [protected, static] |
initialize(const Expr &pf_expr, int lfscm) | LFSCObj | [static] |
Obj::initialize() | Obj | [inline, static] |
input_preds | LFSCObj | [protected, static] |
input_vars | LFSCObj | [protected, static] |
isFormula(const Expr &e) | LFSCObj | [protected, static] |
isVar(const Expr &e) | LFSCObj | [protected, static] |
lcalced | TReturn | [private] |
lfsc_mode | LFSCObj | [protected, static] |
LFSCObj() | LFSCObj | [inline] |
mult_rational(TReturn *lhs) | TReturn | |
nnode_map | LFSCObj | [protected, static] |
normalize_to_tf(const Expr &pf, TReturn *&t1, int y) | TReturn | [static] |
normalize_tr(const Expr &pf1, TReturn *&t1, int y, bool rev_pol=false, bool printErr=true) | TReturn | [static] |
normalize_tret(const Expr &pf1, TReturn *&t1, const Expr &pf2, TReturn *&t2, bool rev_pol=false) | TReturn | [static] |
nullRat | LFSCObj | [protected, static] |
Obj() | Obj | [inline] |
oignore | Obj | [protected] |
pntNeeded | LFSCObj | [protected, static] |
print_error(const char *c, std::ostream &s) | Obj | [inline, static] |
print_warning(const char *c) | Obj | [inline, static] |
printer | LFSCObj | [protected, static] |
queryAtomic(const Expr &expr, bool getBase=false) | LFSCObj | [protected, static] |
queryElimNotNot(const Expr &expr) | LFSCObj | [protected, static] |
queryM(const Expr &expr, bool add=true, bool trusted=false) | LFSCObj | [protected, static] |
queryMt(const Expr &expr) | LFSCObj | [protected, static] |
queryT(const Expr &e) | LFSCObj | [protected, static] |
Ref() | Obj | [inline] |
refCount | Obj | [protected] |
skolem_vars | LFSCObj | [protected, static] |
temp_visited | LFSCObj | [protected, static] |
term_i | LFSCObj | [protected, static] |
tnorm_i | LFSCObj | [protected, static] |
TReturn(LFSCProof *lfsc_pf, std::vector< int > &L, std::vector< int > &Lused, Rational r, bool hasR, int pvY) | TReturn | |
trusted_i | LFSCObj | [protected, static] |
Unref() | Obj | [inline] |
what_is_proven(const Expr &pf, Expr &pe) | LFSCObj | [protected, static] |
~Obj() | Obj | [inline, virtual] |