CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Member Functions | Private Attributes
LFSCAssume Class Reference

#include <LFSCBoolProof.h>

Inheritance diagram for LFSCAssume:
LFSCProof LFSCObj Obj

List of all members.

Public Member Functions

virtual LFSCAssumeAsLFSCAssume ()
void print_pf (std::ostream &s, int ind=0)
void print_struct (std::ostream &s, int ind=0)
LFSCProofclone ()
int getNumChildren ()
LFSCProofgetChild (int n)
int checkBoolRes (std::vector< int > &clause)
- Public Member Functions inherited from LFSCProof
virtual LFSCProofExprAsLFSCProofExpr ()
virtual LFSCLraAddAsLFSCLraAdd ()
virtual LFSCLraSubAsLFSCLraSub ()
virtual LFSCLraMulCAsLFSCLraMulC ()
virtual LFSCLraAxiomAsLFSCLraAxiom ()
virtual LFSCLraContraAsLFSCLraContra ()
virtual LFSCLraPolyAsLFSCLraPoly ()
virtual LFSCBoolResAsLFSCBoolRes ()
virtual LFSCLemAsLFSCLem ()
virtual LFSCClausifyAsLFSCClausify ()
virtual LFSCProofGenericAsLFSCProofGeneric ()
virtual LFSCPfVarAsLFSCPfVar ()
virtual LFSCPfLambdaAsLFSCPfLambda ()
virtual LFSCPfLetAsLFSCPfLet ()
virtual bool isLraMulC ()
void print (std::ostream &s, int ind=0)
virtual bool isTrivial ()
long int get_string_length ()
void print_structure (std::ostream &s, int ind=0)
void setRplProof (LFSCProof *p)
virtual void fillHoles ()
virtual int checkOp ()
int getChOp ()
void setChOp (int c)
- 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

Static Public Member Functions

static LFSCProofMake (int v, LFSCProof *pf, bool assm=true, int type=3)
- Static Public Member Functions inherited from LFSCProof
static int make_lambda (LFSCProof *p)
static LFSCProofMake_CNF (const Expr &form, const Expr &reason, int pos)
static LFSCProofMake_not_not_elim (const Expr &pf, LFSCProof *p)
static LFSCProofMake_mimic (const Expr &pf, LFSCProof *p, int numHoles)
static LFSCProofMake_and_elim (const Expr &form, LFSCProof *p, int n, const Expr &expected)
static int get_proof_counter ()
- 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 ()

Private Member Functions

 LFSCAssume (int v, LFSCProof *pf, bool assm, int type)
virtual ~LFSCAssume ()
long int get_length ()

Private Attributes

int d_var
RefPtr< LFSCProofd_pf
bool d_assm
int d_type

Additional Inherited Members

- Protected Member Functions inherited from LFSCProof
 LFSCProof ()
virtual ~LFSCProof ()
- Protected Attributes inherited from LFSCProof
int printCounter
LFSCProofrplProof
long int strLen
int chOp
int assumeVar
int assumeVarUsed
std::vector< int > br
bool brComputed
- Static Protected Attributes inherited from LFSCProof
static int pf_counter = 0
static std::map< LFSCProof *, int > lambdaMap
static std::map< LFSCProof
*, LFSCProof * > 
lambdaPrintMap
static int lambdaCounter = 1
- 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 90 of file LFSCBoolProof.h.


Constructor & Destructor Documentation

LFSCAssume::LFSCAssume ( int  v,
LFSCProof pf,
bool  assm,
int  type 
)
inlineprivate

Definition at line 96 of file LFSCBoolProof.h.

Referenced by clone(), and Make().

virtual LFSCAssume::~LFSCAssume ( )
inlineprivatevirtual

Definition at line 97 of file LFSCBoolProof.h.


Member Function Documentation

long int LFSCAssume::get_length ( )
inlineprivatevirtual

Reimplemented from LFSCProof.

Definition at line 98 of file LFSCBoolProof.h.

References d_pf, and LFSCProof::get_string_length().

virtual LFSCAssume* LFSCAssume::AsLFSCAssume ( )
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 100 of file LFSCBoolProof.h.

void LFSCAssume::print_pf ( std::ostream &  s,
int  ind = 0 
)
virtual

Implements LFSCProof.

Definition at line 161 of file LFSCBoolProof.cpp.

References CVC3::abs(), d_assm, d_pf, d_type, d_var, and LFSCProof::print().

void LFSCAssume::print_struct ( std::ostream &  s,
int  ind = 0 
)
virtual

Reimplemented from LFSCProof.

Definition at line 172 of file LFSCBoolProof.cpp.

References d_assm, d_pf, d_var, and LFSCProof::print_structure().

static LFSCProof* LFSCAssume::Make ( int  v,
LFSCProof pf,
bool  assm = true,
int  type = 3 
)
inlinestatic
LFSCProof* LFSCAssume::clone ( )
inlinevirtual

Implements LFSCProof.

Definition at line 106 of file LFSCBoolProof.h.

References d_assm, d_pf, d_type, d_var, RefPtr< T >::get(), and LFSCAssume().

int LFSCAssume::getNumChildren ( )
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 107 of file LFSCBoolProof.h.

LFSCProof* LFSCAssume::getChild ( int  n)
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 108 of file LFSCBoolProof.h.

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

int LFSCAssume::checkBoolRes ( std::vector< int > &  clause)
inlinevirtual

Reimplemented from LFSCProof.

Definition at line 110 of file LFSCBoolProof.h.

References LFSCProof::checkBoolRes(), d_pf, d_type, and d_var.


Member Data Documentation

int LFSCAssume::d_var
private

Definition at line 92 of file LFSCBoolProof.h.

Referenced by checkBoolRes(), clone(), print_pf(), and print_struct().

RefPtr< LFSCProof > LFSCAssume::d_pf
private

Definition at line 93 of file LFSCBoolProof.h.

Referenced by checkBoolRes(), clone(), get_length(), getChild(), print_pf(), and print_struct().

bool LFSCAssume::d_assm
private

Definition at line 94 of file LFSCBoolProof.h.

Referenced by clone(), print_pf(), and print_struct().

int LFSCAssume::d_type
private

Definition at line 95 of file LFSCBoolProof.h.

Referenced by checkBoolRes(), clone(), and print_pf().


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