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