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 |
convert(const Expr &pf) | LFSCConvert | |
cvc3_mimic | LFSCObj | protectedstatic |
cvc3_mimic_input | LFSCObj | protectedstatic |
cvc3_to_lfsc(const Expr &pf, bool beneath_lc=false, bool rev_pol=false) | LFSCConvert | private |
cvc3_to_lfsc_h(const Expr &pf, bool beneath_lc=false, bool rev_pol=false) | LFSCConvert | private |
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_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_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_learned_clause_str | LFSCObj | protectedstatic |
d_lessThan_To_LE_rhs_rwr_str | LFSCObj | protectedstatic |
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_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_th_trans | LFSCConvert | private |
d_th_trans_lam | LFSCConvert | private |
d_th_trans_map | LFSCConvert | private |
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 |
do_bso(const Expr &pf, bool beneath_lc, bool rev_pol, TReturn *t1, TReturn *t2, ostringstream &ose) | LFSCConvert | private |
errs | Obj | protectedstatic |
errsInit | Obj | protectedstatic |
formula_i | LFSCObj | protectedstatic |
get_proof_pattern(const Expr &pf, Expr &modE) | LFSCConvert | private |
getLFSCProof() | LFSCConvert | inline |
getNumNodes(const Expr &pf, bool recount=false) | LFSCObj | protectedstatic |
GetRefCount() | Obj | inline |
getY(const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true) | LFSCObj | protectedstatic |
ignore_theory_lemmas | LFSCConvert | private |
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 |
isIgnoredRule(const Expr &expr) | LFSCConvert | private |
isTrivialBooleanAxiom(const Expr &expr) | LFSCConvert | private |
isTrivialTheoryAxiom(const Expr &expr, bool checkBody=false) | LFSCConvert | private |
isVar(const Expr &e) | LFSCObj | protectedstatic |
lfsc_mode | LFSCObj | protectedstatic |
LFSCConvert(int lfscm) | LFSCConvert | |
LFSCObj() | LFSCObj | inline |
make_let_proof(LFSCProof *p) | LFSCConvert | private |
make_trusted(const Expr &pf) | LFSCConvert | private |
nnode_map | LFSCObj | protectedstatic |
nodeCount | LFSCConvert | private |
nodeCountTh | LFSCConvert | private |
nullRat | LFSCObj | protectedstatic |
Obj() | Obj | inline |
oignore | Obj | protected |
pfinal | LFSCConvert | private |
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 |
trusted_i | LFSCObj | protectedstatic |
unodeCount | LFSCConvert | private |
unodeCountTh | LFSCConvert | private |
Unref() | Obj | inline |
what_is_proven(const Expr &pf, Expr &pe) | LFSCObj | protectedstatic |
~LFSCConvert() | LFSCConvert | inlineprivatevirtual |
~Obj() | Obj | inlinevirtual |