CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes
LFSCConvert Class Reference

#include <LFSCConvert.h>

Inheritance diagram for LFSCConvert:
LFSCObj Obj

List of all members.

Public Member Functions

 LFSCConvert (int lfscm)
void convert (const Expr &pf)
LFSCProofgetLFSCProof ()
- Public Member Functions inherited from LFSCObj
 LFSCObj ()
- Public Member Functions inherited from Obj
 Obj ()
virtual ~Obj ()
int GetRefCount ()
 get ref count
void Ref ()
 reference
void Unref ()
 unreference

Private Member Functions

bool isTrivialTheoryAxiom (const Expr &expr, bool checkBody=false)
bool isTrivialBooleanAxiom (const Expr &expr)
bool isIgnoredRule (const Expr &expr)
TReturncvc3_to_lfsc (const Expr &pf, bool beneath_lc=false, bool rev_pol=false)
TReturncvc3_to_lfsc_h (const Expr &pf, bool beneath_lc=false, bool rev_pol=false)
TReturndo_bso (const Expr &pf, bool beneath_lc, bool rev_pol, TReturn *t1, TReturn *t2, ostringstream &ose)
int get_proof_pattern (const Expr &pf, Expr &modE)
LFSCProofmake_let_proof (LFSCProof *p)
TReturnmake_trusted (const Expr &pf)
virtual ~LFSCConvert ()

Private Attributes

RefPtr< LFSCProofpfinal
ExprMap< bool > d_th_trans
ExprMap< TReturn * > d_th_trans_map [2]
std::map< TReturn *, bool > d_th_trans_lam [2]
int nodeCount
int nodeCountTh
int unodeCount
int unodeCountTh
bool ignore_theory_lemmas

Additional Inherited Members

- Static Public Member Functions inherited from LFSCObj
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 inherited from LFSCObj
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 inherited from LFSCObj
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

Detailed Description

Definition at line 6 of file LFSCConvert.h.


Constructor & Destructor Documentation

virtual LFSCConvert::~LFSCConvert ( )
inlineprivatevirtual

Definition at line 45 of file LFSCConvert.h.

LFSCConvert::LFSCConvert ( int  lfscm)

Member Function Documentation

bool LFSCConvert::isTrivialTheoryAxiom ( const Expr expr,
bool  checkBody = false 
)
private
bool LFSCConvert::isTrivialBooleanAxiom ( const Expr expr)
private

Definition at line 79 of file LFSCConvert.cpp.

References LFSCObj::d_rewrite_not_not_str.

Referenced by cvc3_to_lfsc().

bool LFSCConvert::isIgnoredRule ( const Expr expr)
private
TReturn * LFSCConvert::cvc3_to_lfsc ( const Expr pf,
bool  beneath_lc = false,
bool  rev_pol = false 
)
private

Definition at line 93 of file LFSCConvert.cpp.

References CVC3::abs(), AND, CVC3::Expr::arity(), LFSCProof::assumeVar, LFSCProof::assumeVarUsed, LFSCObj::cascade_expr(), LFSCObj::cvc3_mimic, LFSCObj::cvc3_mimic_input, LFSCObj::d_addInequalities_str, LFSCObj::d_and_mid_s, LFSCObj::d_andE_str, LFSCObj::d_assump_map, LFSCObj::d_assump_str, LFSCObj::d_basic_subst_op0_str, LFSCObj::d_basic_subst_op1_str, LFSCObj::d_basic_subst_op_str, LFSCObj::d_bool_res_str, LFSCObj::d_canon_invert_divide_str, LFSCObj::d_canon_mult_str, LFSCObj::d_canon_plus_str, LFSCObj::d_cnf_add_unit_str, LFSCObj::d_cnf_convert_str, LFSCObj::d_CNF_str, LFSCObj::d_CNFITE_str, LFSCObj::d_const_predicate_str, LFSCObj::d_cycle_conflict_str, LFSCObj::d_eq_symm_str, LFSCObj::d_eq_trans_str, LFSCObj::d_flip_inequality_str, LFSCObj::d_formulas_printed, LFSCObj::d_iff_mp_str, LFSCObj::d_iff_symm_str, LFSCObj::d_iff_trans_str, LFSCObj::d_imp_s, LFSCObj::d_impl_mp_str, LFSCObj::d_implyEqualities_str, LFSCObj::d_implyNegatedInequality_str, LFSCObj::d_implyWeakerInequality_str, LFSCObj::d_int_const_eq_str, LFSCObj::d_ite_s, LFSCObj::d_learned_clause_str, LFSCObj::d_lessThan_To_LE_rhs_rwr_str, LFSCObj::d_minisat_proof_str, LFSCObj::d_minus_to_plus_str, LFSCObj::d_mult_eqn_str, LFSCObj::d_mult_ineqn_str, LFSCObj::d_negated_inequality_str, LFSCObj::d_optimized_subst_op_str, LFSCObj::d_pf_expr, LFSCObj::d_plus_predicate_str, LFSCObj::d_real_shadow_eq_str, LFSCObj::d_real_shadow_str, LFSCObj::d_refl_str, LFSCObj::d_rewrite_and_str, LFSCObj::d_rewrite_eq_refl_str, LFSCObj::d_rewrite_eq_symm_str, LFSCObj::d_rewrite_iff_str, LFSCObj::d_rewrite_iff_symm_str, LFSCObj::d_rewrite_implies_str, LFSCObj::d_rewrite_ite_same_str, LFSCObj::d_rewrite_not_false_str, LFSCObj::d_rewrite_not_not_str, LFSCObj::d_rewrite_not_true_str, LFSCObj::d_rewrite_or_str, LFSCObj::d_right_minus_left_str, LFSCObj::d_rules, d_th_trans, d_th_trans_lam, d_th_trans_map, LFSCObj::d_uminus_to_mult_str, LFSCObj::debug_conv, LFSCObj::debug_var, DISTINCT, do_bso(), CVC3::ExprMap< Data >::end(), std::endl(), EQ, FALSE_EXPR, CVC3::ExprManager::falseExpr(), CVC3::ExprMap< Data >::find(), CVC3::GE, RefPtr< T >::get(), get_normalized(), get_not(), get_proof_pattern(), LFSCProof::get_string_length(), CVC3::Expr::getEM(), CVC3::Expr::getKind(), TReturn::getL(), TReturn::getLFSCProof(), getLFSCProof(), LFSCObj::getNumNodes(), TReturn::getProvesY(), getRat(), TReturn::getRational(), LFSCObj::getY(), CVC3::GT, TReturn::hasRational(), IFF, ignore_theory_lemmas, IMPLIES, is_comparison(), is_eq_kind(), CVC3::Expr::isFalse(), isFlat(), LFSCObj::isFormula(), isIgnoredRule(), CVC3::isRational(), LFSCProof::isTrivial(), isTrivialBooleanAxiom(), isTrivialTheoryAxiom(), ITE, kind_to_str(), LFSCObj::lfsc_mode, LFSCProofExpr::Make(), LFSCLraAdd::Make(), LFSCBoolRes::Make(), LFSCPfVar::Make(), LFSCLem::Make(), LFSCLraMulC::Make(), LFSCClausify::Make(), LFSCProofGeneric::Make(), LFSCAssume::Make(), LFSCLraSub::Make(), LFSCLraPoly::Make(), LFSCLraContra::Make(), LFSCProof::Make_and_elim(), LFSCProof::Make_CNF(), make_flatten_expr(), LFSCProof::Make_mimic(), LFSCProof::Make_not_not_elim(), make_trusted(), LFSCLraAxiom::MakeEq(), LFSCProofGeneric::MakeStr(), LFSCProofGeneric::MakeUnk(), LFSCPfVar::MakeV(), CVC3::MINUS, CVC3::MULT, TReturn::mult_rational(), CVC3::ExprManager::newRatExpr(), nodeCount, nodeCountTh, TReturn::normalize_tr(), TReturn::normalize_tret(), LFSCObj::nullRat, OR, PF_APPLY, CVC3::PLUS, LFSCObj::pntNeeded, Obj::print_error(), print_rational(), LFSCObj::queryAtomic(), LFSCObj::queryM(), LFSCObj::queryMt(), LFSCProof::setChOp(), TRUE_EXPR, CVC3::ExprManager::trueExpr(), CVC3::UMINUS, unodeCount, unodeCountTh, and LFSCObj::what_is_proven().

Referenced by convert().

TReturn* LFSCConvert::cvc3_to_lfsc_h ( const Expr pf,
bool  beneath_lc = false,
bool  rev_pol = false 
)
private
TReturn * LFSCConvert::do_bso ( const Expr pf,
bool  beneath_lc,
bool  rev_pol,
TReturn t1,
TReturn t2,
ostringstream &  ose 
)
private
int LFSCConvert::get_proof_pattern ( const Expr pf,
Expr modE 
)
private
LFSCProof * LFSCConvert::make_let_proof ( LFSCProof p)
private
TReturn * LFSCConvert::make_trusted ( const Expr pf)
private
void LFSCConvert::convert ( const Expr pf)
LFSCProof* LFSCConvert::getLFSCProof ( )
inline

Definition at line 51 of file LFSCConvert.h.

References RefPtr< T >::get(), and pfinal.

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


Member Data Documentation

RefPtr< LFSCProof > LFSCConvert::pfinal
private

Definition at line 10 of file LFSCConvert.h.

Referenced by convert(), and getLFSCProof().

ExprMap<bool> LFSCConvert::d_th_trans
private

Definition at line 13 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and make_let_proof().

ExprMap<TReturn*> LFSCConvert::d_th_trans_map[2]
private

Definition at line 14 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and make_let_proof().

std::map<TReturn*, bool> LFSCConvert::d_th_trans_lam[2]
private

Definition at line 16 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and make_let_proof().

int LFSCConvert::nodeCount
private

Definition at line 18 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().

int LFSCConvert::nodeCountTh
private

Definition at line 19 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().

int LFSCConvert::unodeCount
private

Definition at line 20 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().

int LFSCConvert::unodeCountTh
private

Definition at line 21 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().

bool LFSCConvert::ignore_theory_lemmas
private

Definition at line 23 of file LFSCConvert.h.

Referenced by cvc3_to_lfsc(), and LFSCConvert().


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