CVC3  2.4.1
LFSCBoolRes Member List

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

AsLFSCAssume()LFSCProofinlinevirtual
AsLFSCBoolRes()LFSCBoolResinlinevirtual
AsLFSCClausify()LFSCProofinlinevirtual
AsLFSCLem()LFSCProofinlinevirtual
AsLFSCLraAdd()LFSCProofinlinevirtual
AsLFSCLraAxiom()LFSCProofinlinevirtual
AsLFSCLraContra()LFSCProofinlinevirtual
AsLFSCLraMulC()LFSCProofinlinevirtual
AsLFSCLraPoly()LFSCProofinlinevirtual
AsLFSCLraSub()LFSCProofinlinevirtual
AsLFSCPfLambda()LFSCProofinlinevirtual
AsLFSCPfLet()LFSCProofinlinevirtual
AsLFSCPfVar()LFSCProofinlinevirtual
AsLFSCProofExpr()LFSCProofinlinevirtual
AsLFSCProofGeneric()LFSCProofinlinevirtual
assumeVarLFSCProofprotected
assumeVarUsedLFSCProofprotected
brLFSCProofprotected
brComputedLFSCProofprotected
can_pnorm(const Expr &e)LFSCObjprotectedstatic
cas_mapLFSCObjprotectedstatic
cascade_expr(const Expr &e)LFSCObjprotectedstatic
checkBoolRes(std::vector< int > &clause)LFSCBoolResvirtual
checkOp()LFSCProofvirtual
chOpLFSCProofprotected
clone()LFSCBoolResinlinevirtual
collect_vars(const Expr &e, bool readPred=true)LFSCObjprotectedstatic
cvc3_mimicLFSCObjprotectedstatic
cvc3_mimic_inputLFSCObjprotectedstatic
d_addInequalities_strLFSCObjprotectedstatic
d_and_final_sLFSCObjprotectedstatic
d_and_mid_sLFSCObjprotectedstatic
d_andE_strLFSCObjprotectedstatic
d_assump_mapLFSCObjprotectedstatic
d_assump_strLFSCObjprotectedstatic
d_basic_subst_op0_strLFSCObjprotectedstatic
d_basic_subst_op1_strLFSCObjprotectedstatic
d_basic_subst_op_strLFSCObjprotectedstatic
d_bool_res_strLFSCObjprotectedstatic
d_canon_invert_divide_strLFSCObjprotectedstatic
d_canon_mult_strLFSCObjprotectedstatic
d_canon_plus_strLFSCObjprotectedstatic
d_childrenLFSCBoolResprivate
d_cnf_add_unit_strLFSCObjprotectedstatic
d_cnf_convert_strLFSCObjprotectedstatic
d_CNF_strLFSCObjprotectedstatic
d_CNFITE_strLFSCObjprotectedstatic
d_colLFSCBoolResprivate
d_const_predicate_strLFSCObjprotectedstatic
d_cycle_conflict_strLFSCObjprotectedstatic
d_eq_symm_strLFSCObjprotectedstatic
d_eq_trans_strLFSCObjprotectedstatic
d_flip_inequality_strLFSCObjprotectedstatic
d_formulasLFSCObjprotectedstatic
d_formulas_printedLFSCObjprotectedstatic
d_if_lift_rule_strLFSCObjprotectedstatic
d_iff_false_elim_strLFSCObjprotectedstatic
d_iff_false_strLFSCObjprotectedstatic
d_iff_mp_strLFSCObjprotectedstatic
d_iff_not_false_strLFSCObjprotectedstatic
d_iff_sLFSCObjprotectedstatic
d_iff_symm_strLFSCObjprotectedstatic
d_iff_trans_strLFSCObjprotectedstatic
d_iff_true_elim_strLFSCObjprotectedstatic
d_iff_true_strLFSCObjprotectedstatic
d_imp_mp_strLFSCObjprotectedstatic
d_imp_sLFSCObjprotectedstatic
d_impl_mp_strLFSCObjprotectedstatic
d_implyEqualities_strLFSCObjprotectedstatic
d_implyNegatedInequality_strLFSCObjprotectedstatic
d_implyWeakerInequality_strLFSCObjprotectedstatic
d_implyWeakerInequalityDiffLogic_strLFSCObjprotectedstatic
d_int_const_eq_strLFSCObjprotectedstatic
d_ite_sLFSCObjprotectedstatic
d_learned_clause_strLFSCObjprotectedstatic
d_lessThan_To_LE_rhs_rwr_strLFSCObjprotectedstatic
d_minisat_proof_strLFSCObjprotectedstatic
d_minus_to_plus_strLFSCObjprotectedstatic
d_mult_eqn_strLFSCObjprotectedstatic
d_mult_ineqn_strLFSCObjprotectedstatic
d_negated_inequality_strLFSCObjprotectedstatic
d_not_not_elim_strLFSCObjprotectedstatic
d_not_to_iff_strLFSCObjprotectedstatic
d_optimized_subst_op_strLFSCObjprotectedstatic
d_or_final_sLFSCObjprotectedstatic
d_or_mid_sLFSCObjprotectedstatic
d_pf_exprLFSCObjprotectedstatic
d_plus_predicate_strLFSCObjprotectedstatic
d_pnLFSCObjprotectedstatic
d_pn_formLFSCObjprotectedstatic
d_real_shadow_eq_strLFSCObjprotectedstatic
d_real_shadow_strLFSCObjprotectedstatic
d_refl_strLFSCObjprotectedstatic
d_rewrite_and_strLFSCObjprotectedstatic
d_rewrite_eq_refl_strLFSCObjprotectedstatic
d_rewrite_eq_symm_strLFSCObjprotectedstatic
d_rewrite_iff_strLFSCObjprotectedstatic
d_rewrite_iff_symm_strLFSCObjprotectedstatic
d_rewrite_implies_strLFSCObjprotectedstatic
d_rewrite_ite_same_strLFSCObjprotectedstatic
d_rewrite_not_false_strLFSCObjprotectedstatic
d_rewrite_not_not_strLFSCObjprotectedstatic
d_rewrite_not_true_strLFSCObjprotectedstatic
d_rewrite_or_strLFSCObjprotectedstatic
d_right_minus_left_strLFSCObjprotectedstatic
d_rulesLFSCObjprotectedstatic
d_termsLFSCObjprotectedstatic
d_trustedLFSCObjprotectedstatic
d_uminus_to_mult_strLFSCObjprotectedstatic
d_varLFSCBoolResprivate
d_var_intro_strLFSCObjprotectedstatic
debug_convLFSCObjprotectedstatic
debug_varLFSCObjprotectedstatic
define_skolem_vars(const Expr &e)LFSCObjprotectedstatic
errsObjprotectedstatic
errsInitObjprotectedstatic
fillHoles()LFSCProofvirtual
formula_iLFSCObjprotectedstatic
get_length()LFSCBoolResinlineprivatevirtual
get_proof_counter()LFSCProofinlinestatic
get_string_length()LFSCProofinline
getChild(int n)LFSCBoolResinlinevirtual
getChOp()LFSCProofinline
getNumChildren()LFSCBoolResinlinevirtual
getNumNodes(const Expr &pf, bool recount=false)LFSCObjprotectedstatic
GetRefCount()Objinline
getY(const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true)LFSCObjprotectedstatic
indent(std::ostream &s, int ind=0)Objinlineprotected
indentFlagObjprotectedstatic
initialize(const Expr &pf_expr, int lfscm)LFSCObjstatic
Obj::initialize()Objinlinestatic
input_predsLFSCObjprotectedstatic
input_varsLFSCObjprotectedstatic
isFormula(const Expr &e)LFSCObjprotectedstatic
isLraMulC()LFSCProofinlinevirtual
isTrivial()LFSCProofinlinevirtual
isVar(const Expr &e)LFSCObjprotectedstatic
lambdaCounterLFSCProofprotectedstatic
lambdaMapLFSCProofprotectedstatic
lambdaPrintMapLFSCProofprotectedstatic
lfsc_modeLFSCObjprotectedstatic
LFSCBoolRes(LFSCProof *pf1, LFSCProof *pf2, int v, bool col)LFSCBoolResinlineprivate
LFSCObj()LFSCObjinline
LFSCProof()LFSCProofprotected
Make(LFSCProof *pf1, LFSCProof *pf2, int v, bool col)LFSCBoolResstatic
Make(LFSCProof *p1, LFSCProof *p2, const Expr &res, const Expr &pf, bool cascadeOr=false)LFSCBoolResstatic
Make_and_elim(const Expr &form, LFSCProof *p, int n, const Expr &expected)LFSCProofstatic
Make_CNF(const Expr &form, const Expr &reason, int pos)LFSCProofstatic
make_lambda(LFSCProof *p)LFSCProofinlinestatic
Make_mimic(const Expr &pf, LFSCProof *p, int numHoles)LFSCProofstatic
Make_not_not_elim(const Expr &pf, LFSCProof *p)LFSCProofstatic
MakeC(LFSCProof *p, const Expr &res)LFSCBoolResstatic
nnode_mapLFSCObjprotectedstatic
nullRatLFSCObjprotectedstatic
Obj()Objinline
oignoreObjprotected
pf_counterLFSCProofprotectedstatic
pntNeededLFSCObjprotectedstatic
print(std::ostream &s, int ind=0)LFSCProof
print_error(const char *c, std::ostream &s)Objinlinestatic
print_pf(std::ostream &s, int ind=0)LFSCBoolResvirtual
print_struct(std::ostream &s, int ind=0)LFSCBoolResvirtual
print_structure(std::ostream &s, int ind=0)LFSCProof
print_warning(const char *c)Objinlinestatic
printCounterLFSCProofprotected
printerLFSCObjprotectedstatic
queryAtomic(const Expr &expr, bool getBase=false)LFSCObjprotectedstatic
queryElimNotNot(const Expr &expr)LFSCObjprotectedstatic
queryM(const Expr &expr, bool add=true, bool trusted=false)LFSCObjprotectedstatic
queryMt(const Expr &expr)LFSCObjprotectedstatic
queryT(const Expr &e)LFSCObjprotectedstatic
Ref()Objinline
refCountObjprotected
rplProofLFSCProofprotected
setChOp(int c)LFSCProofinline
setRplProof(LFSCProof *p)LFSCProofinline
skolem_varsLFSCObjprotectedstatic
strLenLFSCProofprotected
temp_visitedLFSCObjprotectedstatic
term_iLFSCObjprotectedstatic
tnorm_iLFSCObjprotectedstatic
trusted_iLFSCObjprotectedstatic
Unref()Objinline
what_is_proven(const Expr &pf, Expr &pe)LFSCObjprotectedstatic
~LFSCBoolRes()LFSCBoolResinlineprivatevirtual
~LFSCProof()LFSCProofinlineprotectedvirtual
~Obj()Objinlinevirtual