CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Static Protected Member Functions | Static Protected Attributes | List of all members
LFSCObj Class Reference

#include <LFSCObject.h>

Inheritance diagram for LFSCObj:
Obj LFSCConvert LFSCPrinter LFSCProof TReturn LFSCAssume LFSCBoolRes LFSCClausify LFSCLem LFSCLraAdd LFSCLraAxiom LFSCLraContra LFSCLraMulC LFSCLraPoly LFSCLraSub LFSCPfLambda LFSCPfLet LFSCPfVar LFSCProofExpr LFSCProofGeneric

Public Member Functions

 LFSCObj ()
- Public Member Functions inherited from Obj
 Obj ()
virtual ~Obj ()
int GetRefCount ()
 get ref count
void Ref ()
 reference
void Unref ()
 unreference

Static Public Member Functions

static void initialize (const Expr &pf_expr, int lfscm)
- Static Public Member Functions inherited from Obj
static void print_error (const char *c, std::ostream &s)
static void print_warning (const char *c)
static void initialize ()

Static Protected Member Functions

static int getNumNodes (const Expr &pf, bool recount=false)
static Expr cascade_expr (const Expr &e)
static void define_skolem_vars (const Expr &e)
static bool isVar (const Expr &e)
static void collect_vars (const Expr &e, bool readPred=true)
static Expr queryElimNotNot (const Expr &expr)
static Expr queryAtomic (const Expr &expr, bool getBase=false)
static int queryM (const Expr &expr, bool add=true, bool trusted=false)
static int queryMt (const Expr &expr)
static int queryT (const Expr &e)
static bool getY (const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true)
static bool isFormula (const Expr &e)
static bool can_pnorm (const Expr &e)
static bool what_is_proven (const Expr &pf, Expr &pe)

Static Protected Attributes

static LFSCPrinterprinter
static int formula_i = 1
static int trusted_i = 1
static int term_i = 1
static int tnorm_i = 1
static int lfsc_mode
static bool debug_conv
static bool debug_var
static bool cvc3_mimic
static bool cvc3_mimic_input
static Rational nullRat
static ExprMap< int > nnode_map
static ExprMap< Exprcas_map
static ExprMap< Exprskolem_vars
static ExprMap< bool > temp_visited
static ExprMap< int > d_formulas
static ExprMap< int > d_trusted
static ExprMap< int > d_pn
static ExprMap< int > d_pn_form
static ExprMap< int > d_terms
static ExprMap< bool > input_vars
static ExprMap< bool > input_preds
static std::map< int, bool > pntNeeded
static ExprMap< bool > d_formulas_printed
static Expr d_pf_expr
static ExprMap< bool > d_assump_map
static ExprMap< bool > d_rules
static Expr d_bool_res_str
static Expr d_assump_str
static Expr d_iff_mp_str
static Expr d_impl_mp_str
static Expr d_iff_trans_str
static Expr d_real_shadow_str
static Expr d_cycle_conflict_str
static Expr d_real_shadow_eq_str
static Expr d_basic_subst_op_str
static Expr d_mult_ineqn_str
static Expr d_right_minus_left_str
static Expr d_eq_trans_str
static Expr d_eq_symm_str
static Expr d_canon_plus_str
static Expr d_refl_str
static Expr d_cnf_convert_str
static Expr d_learned_clause_str
static Expr d_minus_to_plus_str
static Expr d_plus_predicate_str
static Expr d_negated_inequality_str
static Expr d_flip_inequality_str
static Expr d_optimized_subst_op_str
static Expr d_iff_true_elim_str
static Expr d_basic_subst_op1_str
static Expr d_basic_subst_op0_str
static Expr d_canon_mult_str
static Expr d_canon_invert_divide_str
static Expr d_iff_true_str
static Expr d_mult_eqn_str
static Expr d_rewrite_eq_symm_str
static Expr d_implyWeakerInequality_str
static Expr d_implyWeakerInequalityDiffLogic_str
static Expr d_imp_mp_str
static Expr d_rewrite_implies_str
static Expr d_rewrite_or_str
static Expr d_rewrite_and_str
static Expr d_rewrite_iff_symm_str
static Expr d_iff_not_false_str
static Expr d_iff_false_str
static Expr d_iff_false_elim_str
static Expr d_not_to_iff_str
static Expr d_not_not_elim_str
static Expr d_const_predicate_str
static Expr d_rewrite_not_not_str
static Expr d_rewrite_not_true_str
static Expr d_rewrite_not_false_str
static Expr d_if_lift_rule_str
static Expr d_CNFITE_str
static Expr d_var_intro_str
static Expr d_int_const_eq_str
static Expr d_rewrite_eq_refl_str
static Expr d_iff_symm_str
static Expr d_rewrite_iff_str
static Expr d_implyNegatedInequality_str
static Expr d_uminus_to_mult_str
static Expr d_lessThan_To_LE_rhs_rwr_str
static Expr d_rewrite_ite_same_str
static Expr d_andE_str
static Expr d_implyEqualities_str
static Expr d_addInequalities_str
static Expr d_CNF_str
static Expr d_cnf_add_unit_str
static Expr d_minisat_proof_str
static Expr d_or_final_s
static Expr d_and_final_s
static Expr d_ite_s
static Expr d_iff_s
static Expr d_imp_s
static Expr d_or_mid_s
static Expr d_and_mid_s
- Static Protected Attributes inherited from Obj
static bool errsInit = false
static ofstream errs
static bool indentFlag = false

Additional Inherited Members

- Protected Member Functions inherited from Obj
void indent (std::ostream &s, int ind=0)
- Protected Attributes inherited from Obj
ostringstream oignore
int refCount

Detailed Description

Definition at line 9 of file LFSCObject.h.

Constructor & Destructor Documentation

LFSCObj::LFSCObj ( )
inline

Definition at line 12 of file LFSCObject.h.

Member Function Documentation

void LFSCObj::initialize ( const Expr pf_expr,
int  lfscm 
)
static

Definition at line 104 of file LFSCObject.cpp.

References cvc3_mimic, cvc3_mimic_input, d_addInequalities_str, d_and_final_s, d_and_mid_s, d_andE_str, d_assump_str, d_basic_subst_op0_str, d_basic_subst_op1_str, d_basic_subst_op_str, d_bool_res_str, d_canon_invert_divide_str, d_canon_mult_str, d_canon_plus_str, d_cnf_add_unit_str, d_cnf_convert_str, d_CNF_str, d_CNFITE_str, d_const_predicate_str, d_cycle_conflict_str, d_eq_symm_str, d_eq_trans_str, d_flip_inequality_str, d_if_lift_rule_str, d_iff_false_elim_str, d_iff_false_str, d_iff_mp_str, d_iff_not_false_str, d_iff_s, d_iff_symm_str, d_iff_trans_str, d_iff_true_elim_str, d_iff_true_str, d_imp_mp_str, d_imp_s, d_impl_mp_str, d_implyEqualities_str, d_implyNegatedInequality_str, d_implyWeakerInequality_str, d_implyWeakerInequalityDiffLogic_str, d_int_const_eq_str, d_ite_s, d_learned_clause_str, d_lessThan_To_LE_rhs_rwr_str, d_minisat_proof_str, d_minus_to_plus_str, d_mult_eqn_str, d_mult_ineqn_str, d_negated_inequality_str, d_not_not_elim_str, d_not_to_iff_str, d_optimized_subst_op_str, d_or_final_s, d_or_mid_s, d_pf_expr, d_plus_predicate_str, d_real_shadow_eq_str, d_real_shadow_str, d_refl_str, d_rewrite_and_str, d_rewrite_eq_refl_str, d_rewrite_eq_symm_str, d_rewrite_iff_str, d_rewrite_iff_symm_str, d_rewrite_implies_str, d_rewrite_ite_same_str, d_rewrite_not_false_str, d_rewrite_not_not_str, d_rewrite_not_true_str, d_rewrite_or_str, d_right_minus_left_str, d_rules, d_uminus_to_mult_str, d_var_intro_str, debug_conv, debug_var, CVC3::Expr::getEM(), lfsc_mode, CVC3::ExprManager::newStringExpr(), and CVC3::ExprManager::newVarExpr().

int LFSCObj::getNumNodes ( const Expr pf,
bool  recount = false 
)
staticprotected
Expr LFSCObj::cascade_expr ( const Expr e)
staticprotected
void LFSCObj::define_skolem_vars ( const Expr e)
staticprotected
bool LFSCObj::isVar ( const Expr e)
staticprotected

Definition at line 337 of file LFSCObject.cpp.

References d_rules, CVC3::Expr::getKind(), and UCONST.

Referenced by collect_vars().

void LFSCObj::collect_vars ( const Expr e,
bool  readPred = true 
)
staticprotected
Expr LFSCObj::queryElimNotNot ( const Expr expr)
staticprotected

Definition at line 356 of file LFSCObject.cpp.

References CVC3::Expr::isNot().

Referenced by TReturn::normalize_tr(), queryAtomic(), queryM(), and what_is_proven().

Expr LFSCObj::queryAtomic ( const Expr expr,
bool  getBase = false 
)
staticprotected
int LFSCObj::queryM ( const Expr expr,
bool  add = true,
bool  trusted = false 
)
staticprotected
int LFSCObj::queryMt ( const Expr expr)
staticprotected
int LFSCObj::queryT ( const Expr e)
staticprotected

Definition at line 436 of file LFSCObject.cpp.

References cascade_expr(), d_terms, and term_i.

Referenced by can_pnorm(), and define_skolem_vars().

bool LFSCObj::getY ( const Expr e,
Expr pe,
bool  doIff = true,
bool  doLogic = true 
)
staticprotected
bool LFSCObj::isFormula ( const Expr e)
staticprotected
bool LFSCObj::can_pnorm ( const Expr e)
staticprotected
bool LFSCObj::what_is_proven ( const Expr pf,
Expr pe 
)
staticprotected

Definition at line 539 of file LFSCObject.cpp.

References AND, CVC3::Expr::arity(), d_andE_str, d_assump_str, d_basic_subst_op0_str, d_basic_subst_op1_str, d_basic_subst_op_str, d_canon_invert_divide_str, d_canon_mult_str, d_canon_plus_str, d_cnf_add_unit_str, d_cnf_convert_str, d_const_predicate_str, d_cycle_conflict_str, d_eq_symm_str, d_eq_trans_str, d_flip_inequality_str, d_iff_false_elim_str, d_iff_mp_str, d_iff_not_false_str, d_iff_symm_str, d_iff_trans_str, d_iff_true_elim_str, d_iff_true_str, d_impl_mp_str, d_implyEqualities_str, d_implyNegatedInequality_str, d_implyWeakerInequality_str, d_int_const_eq_str, d_lessThan_To_LE_rhs_rwr_str, d_minus_to_plus_str, d_mult_eqn_str, d_mult_ineqn_str, d_negated_inequality_str, d_not_to_iff_str, d_optimized_subst_op_str, d_pf_expr, d_plus_predicate_str, d_real_shadow_eq_str, d_real_shadow_str, d_refl_str, d_rewrite_and_str, d_rewrite_eq_refl_str, d_rewrite_eq_symm_str, d_rewrite_iff_str, d_rewrite_iff_symm_str, d_rewrite_implies_str, d_rewrite_ite_same_str, d_rewrite_not_false_str, d_rewrite_not_not_str, d_rewrite_not_true_str, d_rewrite_or_str, d_right_minus_left_str, d_rules, d_uminus_to_mult_str, EQ, CVC3::ExprManager::falseExpr(), get_not(), CVC3::Expr::getEM(), CVC3::Rational::getInt(), CVC3::Rational::getNumerator(), CVC3::Expr::getRational(), IFF, CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), IMPLIES, is_eq_kind(), isFormula(), ITE, CVC3::LE, CVC3::LT, CVC3::MINUS, CVC3::MULT, CVC3::ExprManager::newRatExpr(), NOT, OR, CVC3::PLUS, Obj::print_error(), queryElimNotNot(), CVC3::ExprManager::trueExpr(), UCONST, and CVC3::UMINUS.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCConvert::isTrivialTheoryAxiom(), LFSCConvert::make_trusted(), and TReturn::normalize_tr().

Member Data Documentation

LFSCPrinter * LFSCObj::printer
staticprotected
int LFSCObj::formula_i = 1
staticprotected

Definition at line 18 of file LFSCObject.h.

Referenced by queryM().

int LFSCObj::trusted_i = 1
staticprotected

Definition at line 19 of file LFSCObject.h.

Referenced by queryM().

int LFSCObj::term_i = 1
staticprotected

Definition at line 20 of file LFSCObject.h.

Referenced by queryT().

int LFSCObj::tnorm_i = 1
staticprotected

Definition at line 21 of file LFSCObject.h.

Referenced by queryMt().

int LFSCObj::lfsc_mode
staticprotected
bool LFSCObj::debug_conv
staticprotected
bool LFSCObj::debug_var
staticprotected

Definition at line 25 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

bool LFSCObj::cvc3_mimic
staticprotected
bool LFSCObj::cvc3_mimic_input
staticprotected

Definition at line 27 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Rational LFSCObj::nullRat
staticprotected
ExprMap< int > LFSCObj::nnode_map
staticprotected

Definition at line 31 of file LFSCObject.h.

Referenced by getNumNodes().

ExprMap< Expr > LFSCObj::cas_map
staticprotected

Definition at line 34 of file LFSCObject.h.

Referenced by cascade_expr().

ExprMap< Expr > LFSCObj::skolem_vars
staticprotected

Definition at line 37 of file LFSCObject.h.

Referenced by cascade_expr(), define_skolem_vars(), and LFSCPrinter::print_poly_norm().

ExprMap< bool > LFSCObj::temp_visited
staticprotected

Definition at line 38 of file LFSCObject.h.

Referenced by define_skolem_vars().

ExprMap< int > LFSCObj::d_formulas
staticprotected

Definition at line 46 of file LFSCObject.h.

Referenced by LFSCPrinter::print_LFSC(), and queryM().

ExprMap< int > LFSCObj::d_trusted
staticprotected

Definition at line 48 of file LFSCObject.h.

Referenced by LFSCPrinter::print_LFSC(), and queryM().

ExprMap< int > LFSCObj::d_pn
staticprotected

Definition at line 50 of file LFSCObject.h.

Referenced by LFSCPrinter::print_LFSC(), and queryMt().

ExprMap< int > LFSCObj::d_pn_form
staticprotected

Definition at line 52 of file LFSCObject.h.

Referenced by LFSCLraPoly::Make(), and LFSCPrinter::print_LFSC().

ExprMap< int > LFSCObj::d_terms
staticprotected

Definition at line 54 of file LFSCObject.h.

Referenced by LFSCPrinter::print_LFSC(), LFSCPrinter::print_poly_norm(), and queryT().

ExprMap< bool > LFSCObj::input_vars
staticprotected

Definition at line 56 of file LFSCObject.h.

Referenced by collect_vars(), and LFSCPrinter::print_LFSC().

ExprMap< bool > LFSCObj::input_preds
staticprotected

Definition at line 58 of file LFSCObject.h.

Referenced by can_pnorm(), collect_vars(), isFormula(), and LFSCPrinter::print_LFSC().

std::map< int, bool > LFSCObj::pntNeeded
staticprotected

Definition at line 60 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCPrinter::print_LFSC().

ExprMap< bool > LFSCObj::d_formulas_printed
staticprotected

Definition at line 62 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and LFSCPrinter::print_LFSC().

Expr LFSCObj::d_pf_expr
staticprotected

Definition at line 64 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), getY(), initialize(), queryAtomic(), and what_is_proven().

ExprMap< bool > LFSCObj::d_assump_map
staticprotected
ExprMap< bool > LFSCObj::d_rules
staticprotected
Expr LFSCObj::d_bool_res_str
staticprotected

Definition at line 92 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_assump_str
staticprotected
Expr LFSCObj::d_iff_mp_str
staticprotected
Expr LFSCObj::d_impl_mp_str
staticprotected

Definition at line 96 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_iff_trans_str
staticprotected

Definition at line 97 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_real_shadow_str
staticprotected

Definition at line 98 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_cycle_conflict_str
staticprotected

Definition at line 99 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_real_shadow_eq_str
staticprotected

Definition at line 100 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_basic_subst_op_str
staticprotected

Definition at line 101 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_mult_ineqn_str
staticprotected
Expr LFSCObj::d_right_minus_left_str
staticprotected
Expr LFSCObj::d_eq_trans_str
staticprotected

Definition at line 104 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_eq_symm_str
staticprotected
Expr LFSCObj::d_canon_plus_str
staticprotected
Expr LFSCObj::d_refl_str
staticprotected
Expr LFSCObj::d_cnf_convert_str
staticprotected

Definition at line 108 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_learned_clause_str
staticprotected

Definition at line 109 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), define_skolem_vars(), and initialize().

Expr LFSCObj::d_minus_to_plus_str
staticprotected
Expr LFSCObj::d_plus_predicate_str
staticprotected
Expr LFSCObj::d_negated_inequality_str
staticprotected
Expr LFSCObj::d_flip_inequality_str
staticprotected
Expr LFSCObj::d_optimized_subst_op_str
staticprotected

Definition at line 114 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_iff_true_elim_str
staticprotected

Definition at line 115 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_basic_subst_op1_str
staticprotected

Definition at line 116 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_basic_subst_op0_str
staticprotected

Definition at line 117 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_canon_mult_str
staticprotected
Expr LFSCObj::d_canon_invert_divide_str
staticprotected
Expr LFSCObj::d_iff_true_str
staticprotected

Definition at line 120 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_mult_eqn_str
staticprotected
Expr LFSCObj::d_rewrite_eq_symm_str
staticprotected
Expr LFSCObj::d_implyWeakerInequality_str
staticprotected

Definition at line 123 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_implyWeakerInequalityDiffLogic_str
staticprotected

Definition at line 124 of file LFSCObject.h.

Referenced by initialize().

Expr LFSCObj::d_imp_mp_str
staticprotected

Definition at line 125 of file LFSCObject.h.

Referenced by initialize().

Expr LFSCObj::d_rewrite_implies_str
staticprotected

Definition at line 126 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_or_str
staticprotected

Definition at line 127 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_and_str
staticprotected

Definition at line 128 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_iff_symm_str
staticprotected

Definition at line 129 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_iff_not_false_str
staticprotected

Definition at line 130 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_iff_false_str
staticprotected

Definition at line 131 of file LFSCObject.h.

Referenced by initialize().

Expr LFSCObj::d_iff_false_elim_str
staticprotected

Definition at line 132 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_not_to_iff_str
staticprotected

Definition at line 133 of file LFSCObject.h.

Referenced by initialize(), LFSCConvert::isIgnoredRule(), and what_is_proven().

Expr LFSCObj::d_not_not_elim_str
staticprotected

Definition at line 134 of file LFSCObject.h.

Referenced by initialize(), and LFSCConvert::isIgnoredRule().

Expr LFSCObj::d_const_predicate_str
staticprotected

Definition at line 135 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_not_not_str
staticprotected
Expr LFSCObj::d_rewrite_not_true_str
staticprotected
Expr LFSCObj::d_rewrite_not_false_str
staticprotected
Expr LFSCObj::d_if_lift_rule_str
staticprotected

Definition at line 139 of file LFSCObject.h.

Referenced by LFSCConvert::get_proof_pattern(), and initialize().

Expr LFSCObj::d_CNFITE_str
staticprotected

Definition at line 140 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_var_intro_str
staticprotected

Definition at line 141 of file LFSCObject.h.

Referenced by LFSCConvert::get_proof_pattern(), and initialize().

Expr LFSCObj::d_int_const_eq_str
staticprotected
Expr LFSCObj::d_rewrite_eq_refl_str
staticprotected
Expr LFSCObj::d_iff_symm_str
staticprotected

Definition at line 144 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_iff_str
staticprotected

Definition at line 145 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_implyNegatedInequality_str
staticprotected

Definition at line 146 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_uminus_to_mult_str
staticprotected
Expr LFSCObj::d_lessThan_To_LE_rhs_rwr_str
staticprotected

Definition at line 148 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_rewrite_ite_same_str
staticprotected

Definition at line 149 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_andE_str
staticprotected

Definition at line 150 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_implyEqualities_str
staticprotected

Definition at line 151 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and what_is_proven().

Expr LFSCObj::d_addInequalities_str
staticprotected

Definition at line 152 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_CNF_str
staticprotected

Definition at line 154 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_cnf_add_unit_str
staticprotected
Expr LFSCObj::d_minisat_proof_str
staticprotected

Definition at line 156 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), and initialize().

Expr LFSCObj::d_or_final_s
staticprotected

Definition at line 158 of file LFSCObject.h.

Referenced by initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_and_final_s
staticprotected

Definition at line 159 of file LFSCObject.h.

Referenced by initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_ite_s
staticprotected

Definition at line 160 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_iff_s
staticprotected

Definition at line 161 of file LFSCObject.h.

Referenced by initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_imp_s
staticprotected

Definition at line 162 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_or_mid_s
staticprotected

Definition at line 163 of file LFSCObject.h.

Referenced by initialize(), and LFSCProof::Make_CNF().

Expr LFSCObj::d_and_mid_s
staticprotected

Definition at line 164 of file LFSCObject.h.

Referenced by LFSCConvert::cvc3_to_lfsc(), initialize(), and LFSCProof::Make_CNF().


The documentation for this class was generated from the following files: