LFSCClausify Member List

This is the complete list of members for LFSCClausify, including all inherited members.

AsLFSCAssume()	LFSCProof	[inline, virtual]
AsLFSCBoolRes()	LFSCProof	[inline, virtual]
AsLFSCClausify()	LFSCClausify	[inline, virtual]
AsLFSCLem()	LFSCProof	[inline, virtual]
AsLFSCLraAdd()	LFSCProof	[inline, virtual]
AsLFSCLraAxiom()	LFSCProof	[inline, virtual]
AsLFSCLraContra()	LFSCProof	[inline, virtual]
AsLFSCLraMulC()	LFSCProof	[inline, virtual]
AsLFSCLraPoly()	LFSCProof	[inline, virtual]
AsLFSCLraSub()	LFSCProof	[inline, virtual]
AsLFSCPfLambda()	LFSCProof	[inline, virtual]
AsLFSCPfLet()	LFSCProof	[inline, virtual]
AsLFSCPfVar()	LFSCProof	[inline, virtual]
AsLFSCProofExpr()	LFSCProof	[inline, virtual]
AsLFSCProofGeneric()	LFSCProof	[inline, virtual]
assumeVar	LFSCProof	[protected]
assumeVarUsed	LFSCProof	[protected]
br	LFSCProof	[protected]
brComputed	LFSCProof	[protected]
can_pnorm(const Expr &e)	LFSCObj	[protected, static]
cas_map	LFSCObj	[protected, static]
cascade_expr(const Expr &e)	LFSCObj	[protected, static]
checkBoolRes(std::vector< int > &clause)	LFSCClausify	[inline, virtual]
checkOp()	LFSCProof	[virtual]
chOp	LFSCProof	[protected]
clone()	LFSCClausify	[inline, virtual]
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_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_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_learned_clause_str	LFSCObj	[protected, static]
d_lessThan_To_LE_rhs_rwr_str	LFSCObj	[protected, static]
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	LFSCClausify	[private]
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_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	LFSCClausify	[private]
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]
fillHoles()	LFSCProof	[virtual]
formula_i	LFSCObj	[protected, static]
get_length()	LFSCClausify	[inline, private, virtual]
get_proof_counter()	LFSCProof	[inline, static]
get_string_length()	LFSCProof	[inline]
getChild(int n)	LFSCClausify	[inline, virtual]
getChOp()	LFSCProof	[inline]
getNumChildren()	LFSCClausify	[inline, virtual]
getNumNodes(const Expr &pf, bool recount=false)	LFSCObj	[protected, static]
GetRefCount()	Obj	[inline]
getY(const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true)	LFSCObj	[protected, static]
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]
isLraMulC()	LFSCProof	[inline, virtual]
isTrivial()	LFSCProof	[inline, virtual]
isVar(const Expr &e)	LFSCObj	[protected, static]
lambdaCounter	LFSCProof	[protected, static]
lambdaMap	LFSCProof	[protected, static]
lambdaPrintMap	LFSCProof	[protected, static]
lfsc_mode	LFSCObj	[protected, static]
LFSCClausify(int v, LFSCProof *pf)	LFSCClausify	[inline, private]
LFSCObj()	LFSCObj	[inline]
LFSCPrinter class	LFSCClausify	[friend]
LFSCProof()	LFSCProof	[protected]
Make(int v, LFSCProof *pf)	LFSCClausify	[inline, static]
Make(const Expr &e, LFSCProof *p, bool cascadeOr=false)	LFSCClausify	[static]
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_i(const Expr &e, LFSCProof *p, std::vector< Expr > &exprs, const Expr &end)	LFSCClausify	[private, static]
make_lambda(LFSCProof *p)	LFSCProof	[inline, static]
Make_mimic(const Expr &pf, LFSCProof *p, int numHoles)	LFSCProof	[static]
Make_not_not_elim(const Expr &pf, LFSCProof *p)	LFSCProof	[static]
nnode_map	LFSCObj	[protected, static]
nullRat	LFSCObj	[protected, static]
Obj()	Obj	[inline]
oignore	Obj	[protected]
pf_counter	LFSCProof	[protected, static]
pntNeeded	LFSCObj	[protected, static]
print(std::ostream &s, int ind=0)	LFSCProof
print_error(const char *c, std::ostream &s)	Obj	[inline, static]
print_pf(std::ostream &s, int ind=0)	LFSCClausify	[virtual]
print_struct(std::ostream &s, int ind=0)	LFSCClausify	[inline, virtual]
print_structure(std::ostream &s, int ind=0)	LFSCProof
print_warning(const char *c)	Obj	[inline, static]
printCounter	LFSCProof	[protected]
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]
rplProof	LFSCProof	[protected]
setChOp(int c)	LFSCProof	[inline]
setRplProof(LFSCProof *p)	LFSCProof	[inline]
skolem_vars	LFSCObj	[protected, static]
strLen	LFSCProof	[protected]
temp_visited	LFSCObj	[protected, static]
term_i	LFSCObj	[protected, static]
tnorm_i	LFSCObj	[protected, static]
trusted_i	LFSCObj	[protected, static]
Unref()	Obj	[inline]
what_is_proven(const Expr &pf, Expr &pe)	LFSCObj	[protected, static]
~LFSCClausify()	LFSCClausify	[inline, private, virtual]
~LFSCProof()	LFSCProof	[inline, protected, virtual]
~Obj()	Obj	[inline, virtual]