AsLFSCAssume() | LFSCProof | inlinevirtual |
AsLFSCBoolRes() | LFSCProof | inlinevirtual |
AsLFSCClausify() | LFSCProof | inlinevirtual |
AsLFSCLem() | LFSCProof | inlinevirtual |
AsLFSCLraAdd() | LFSCProof | inlinevirtual |
AsLFSCLraAxiom() | LFSCLraAxiom | inlinevirtual |
AsLFSCLraContra() | LFSCProof | inlinevirtual |
AsLFSCLraMulC() | LFSCProof | inlinevirtual |
AsLFSCLraPoly() | LFSCProof | inlinevirtual |
AsLFSCLraSub() | LFSCProof | inlinevirtual |
AsLFSCPfLambda() | LFSCProof | inlinevirtual |
AsLFSCPfLet() | LFSCProof | inlinevirtual |
AsLFSCPfVar() | LFSCProof | inlinevirtual |
AsLFSCProofExpr() | LFSCProof | inlinevirtual |
AsLFSCProofGeneric() | LFSCProof | inlinevirtual |
assumeVar | LFSCProof | protected |
assumeVarUsed | LFSCProof | protected |
br | LFSCProof | protected |
brComputed | LFSCProof | protected |
can_pnorm(const Expr &e) | LFSCObj | protectedstatic |
cas_map | LFSCObj | protectedstatic |
cascade_expr(const Expr &e) | LFSCObj | protectedstatic |
checkBoolRes(std::vector< int > &clause) | LFSCProof | inlinevirtual |
checkOp() | LFSCLraAxiom | inlinevirtual |
chOp | LFSCProof | protected |
clone() | LFSCLraAxiom | inlinevirtual |
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_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_op | LFSCLraAxiom | private |
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_r | LFSCLraAxiom | 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 |
eq | LFSCLraAxiom | privatestatic |
errs | Obj | protectedstatic |
errsInit | Obj | protectedstatic |
fillHoles() | LFSCProof | virtual |
formula_i | LFSCObj | protectedstatic |
get_length() | LFSCLraAxiom | inlineprivate |
get_proof_counter() | LFSCProof | inlinestatic |
get_string_length() | LFSCProof | inline |
getChild(int n) | LFSCProof | inlinevirtual |
getChOp() | LFSCProof | inline |
getNumChildren() | LFSCProof | inlinevirtual |
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 |
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 |
isLraMulC() | LFSCProof | inlinevirtual |
isTrivial() | LFSCLraAxiom | inlinevirtual |
isVar(const Expr &e) | LFSCObj | protectedstatic |
lambdaCounter | LFSCProof | protectedstatic |
lambdaMap | LFSCProof | protectedstatic |
lambdaPrintMap | LFSCProof | protectedstatic |
lfsc_mode | LFSCObj | protectedstatic |
LFSCLraAxiom(int op) | LFSCLraAxiom | inlineprivate |
LFSCLraAxiom(int op, Rational r) | LFSCLraAxiom | inlineprivate |
LFSCObj() | LFSCObj | inline |
LFSCProof() | LFSCProof | protected |
Make(Rational r, int op) | LFSCLraAxiom | inlinestatic |
Make_and_elim(const Expr &form, LFSCProof *p, int n, const Expr &expected) | LFSCProof | static |
Make_CNF(const Expr &form, const Expr &reason, int pos) | LFSCProof | static |
make_lambda(LFSCProof *p) | LFSCProof | inlinestatic |
Make_mimic(const Expr &pf, LFSCProof *p, int numHoles) | LFSCProof | static |
Make_not_not_elim(const Expr &pf, LFSCProof *p) | LFSCProof | static |
MakeEq() | LFSCLraAxiom | static |
nnode_map | LFSCObj | protectedstatic |
nullRat | LFSCObj | protectedstatic |
Obj() | Obj | inline |
oignore | Obj | protected |
pf_counter | LFSCProof | protectedstatic |
pntNeeded | LFSCObj | protectedstatic |
print(std::ostream &s, int ind=0) | LFSCProof | |
print_error(const char *c, std::ostream &s) | Obj | inlinestatic |
print_pf(std::ostream &s, int ind=0) | LFSCLraAxiom | virtual |
print_struct(std::ostream &s, int ind=0) | LFSCProof | inlinevirtual |
print_structure(std::ostream &s, int ind=0) | LFSCProof | |
print_warning(const char *c) | Obj | inlinestatic |
printCounter | LFSCProof | protected |
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 |
rplProof | LFSCProof | protected |
setChOp(int c) | LFSCProof | inline |
setRplProof(LFSCProof *p) | LFSCProof | inline |
skolem_vars | LFSCObj | protectedstatic |
strLen | LFSCProof | protected |
temp_visited | LFSCObj | protectedstatic |
term_i | LFSCObj | protectedstatic |
tnorm_i | LFSCObj | protectedstatic |
trusted_i | LFSCObj | protectedstatic |
Unref() | Obj | inline |
what_is_proven(const Expr &pf, Expr &pe) | LFSCObj | protectedstatic |
~LFSCLraAxiom() | LFSCLraAxiom | inlineprivatevirtual |
~LFSCProof() | LFSCProof | inlineprotectedvirtual |
~Obj() | Obj | inlinevirtual |