CVC3
2.4.1
|
#include <LFSCProof.h>
LFSCProof::LFSCProof | ( | ) | [protected] |
Definition at line 11 of file LFSCProof.cpp.
References pf_counter, printCounter, strLen, rplProof, chOp, brComputed, assumeVar, and assumeVarUsed.
virtual LFSCProof::~LFSCProof | ( | ) | [inline, protected, virtual] |
Definition at line 44 of file LFSCProof.h.
virtual long int LFSCProof::get_length | ( | ) | [inline, protected, virtual] |
Reimplemented in LFSCLraContra, LFSCLraPoly, LFSCPfLet, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCLraMulC, LFSCClausify, LFSCPfLambda, LFSCLem, LFSCLraAxiom, LFSCPfVar, LFSCLraAdd, LFSCBoolRes, and LFSCProofExpr.
Definition at line 43 of file LFSCProof.h.
Referenced by get_string_length().
virtual LFSCProofExpr* LFSCProof::AsLFSCProofExpr | ( | ) | [inline, virtual] |
Reimplemented in LFSCProofExpr.
Definition at line 46 of file LFSCProof.h.
virtual LFSCLraAdd* LFSCProof::AsLFSCLraAdd | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraAdd.
Definition at line 47 of file LFSCProof.h.
virtual LFSCLraSub* LFSCProof::AsLFSCLraSub | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraSub.
Definition at line 48 of file LFSCProof.h.
virtual LFSCLraMulC* LFSCProof::AsLFSCLraMulC | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraMulC.
Definition at line 49 of file LFSCProof.h.
Referenced by LFSCLraMulC::Make().
virtual LFSCLraAxiom* LFSCProof::AsLFSCLraAxiom | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraAxiom.
Definition at line 50 of file LFSCProof.h.
virtual LFSCLraContra* LFSCProof::AsLFSCLraContra | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraContra.
Definition at line 51 of file LFSCProof.h.
virtual LFSCLraPoly* LFSCProof::AsLFSCLraPoly | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraPoly.
Definition at line 52 of file LFSCProof.h.
Referenced by TReturn::normalize_to_tf().
virtual LFSCBoolRes* LFSCProof::AsLFSCBoolRes | ( | ) | [inline, virtual] |
Reimplemented in LFSCBoolRes.
Definition at line 53 of file LFSCProof.h.
virtual LFSCLem* LFSCProof::AsLFSCLem | ( | ) | [inline, virtual] |
Reimplemented in LFSCLem.
Definition at line 54 of file LFSCProof.h.
virtual LFSCClausify* LFSCProof::AsLFSCClausify | ( | ) | [inline, virtual] |
Reimplemented in LFSCClausify.
Definition at line 55 of file LFSCProof.h.
virtual LFSCAssume* LFSCProof::AsLFSCAssume | ( | ) | [inline, virtual] |
Reimplemented in LFSCAssume.
Definition at line 56 of file LFSCProof.h.
virtual LFSCProofGeneric* LFSCProof::AsLFSCProofGeneric | ( | ) | [inline, virtual] |
Reimplemented in LFSCProofGeneric.
Definition at line 57 of file LFSCProof.h.
virtual LFSCPfVar* LFSCProof::AsLFSCPfVar | ( | ) | [inline, virtual] |
Reimplemented in LFSCPfVar.
Definition at line 58 of file LFSCProof.h.
virtual LFSCPfLambda* LFSCProof::AsLFSCPfLambda | ( | ) | [inline, virtual] |
Reimplemented in LFSCPfLambda.
Definition at line 59 of file LFSCProof.h.
virtual LFSCPfLet* LFSCProof::AsLFSCPfLet | ( | ) | [inline, virtual] |
Reimplemented in LFSCPfLet.
Definition at line 60 of file LFSCProof.h.
virtual bool LFSCProof::isLraMulC | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraMulC.
Definition at line 62 of file LFSCProof.h.
static int LFSCProof::make_lambda | ( | LFSCProof * | p | ) | [inline, static] |
Definition at line 63 of file LFSCProof.h.
References lambdaMap, and lambdaCounter.
Referenced by LFSCConvert::make_let_proof().
void LFSCProof::print | ( | std::ostream & | s, |
int | ind = 0 |
||
) |
Definition at line 23 of file LFSCProof.cpp.
References rplProof, lambdaPrintMap, print(), lambdaMap, printCounter, Obj::print_warning(), Obj::indent(), and print_pf().
Referenced by print(), and print_structure().
virtual void LFSCProof::print_pf | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [pure virtual] |
Implemented in LFSCLraContra, LFSCLraPoly, LFSCPfLet, LFSCLraSub, LFSCAssume, LFSCProofGeneric, LFSCLraMulC, LFSCClausify, LFSCPfLambda, LFSCLem, LFSCLraAxiom, LFSCPfVar, LFSCLraAdd, LFSCBoolRes, and LFSCProofExpr.
Referenced by print().
virtual bool LFSCProof::isTrivial | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraAxiom.
Definition at line 72 of file LFSCProof.h.
Referenced by LFSCBoolRes::Make(), LFSCConvert::cvc3_to_lfsc(), LFSCLraAdd::Make(), LFSCLraMulC::Make(), and LFSCLraSub::Make().
long int LFSCProof::get_string_length | ( | ) | [inline] |
Definition at line 73 of file LFSCProof.h.
References strLen, get_length(), getNumChildren(), getChild(), and get_string_length().
Referenced by LFSCConvert::cvc3_to_lfsc(), get_string_length(), and LFSCProofGeneric::get_length().
void LFSCProof::print_structure | ( | std::ostream & | s, |
int | ind = 0 |
||
) |
Definition at line 43 of file LFSCProof.cpp.
References rplProof, lambdaPrintMap, print(), Obj::indent(), lambdaMap, printCounter, Obj::print_warning(), and print_struct().
virtual void LFSCProof::print_struct | ( | std::ostream & | s, |
int | ind = 0 |
||
) | [inline, virtual] |
Reimplemented in LFSCPfLet, LFSCAssume, LFSCClausify, LFSCLem, LFSCPfVar, and LFSCBoolRes.
Definition at line 86 of file LFSCProof.h.
Referenced by print_structure().
void LFSCProof::setRplProof | ( | LFSCProof * | p | ) | [inline] |
Definition at line 91 of file LFSCProof.h.
References rplProof.
void LFSCProof::fillHoles | ( | ) | [virtual] |
Reimplemented in LFSCProofExpr.
Definition at line 61 of file LFSCProof.cpp.
References getNumChildren(), getChild(), and fillHoles().
Referenced by fillHoles().
virtual LFSCProof* LFSCProof::clone | ( | ) | [pure virtual] |
Implemented in LFSCLraContra, LFSCLraPoly, LFSCPfLet, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCClausify, LFSCLraMulC, LFSCPfLambda, LFSCLem, LFSCLraAxiom, LFSCPfVar, LFSCBoolRes, LFSCLraAdd, and LFSCProofExpr.
virtual int LFSCProof::getNumChildren | ( | ) | [inline, virtual] |
Reimplemented in LFSCLraContra, LFSCLraPoly, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCClausify, LFSCLraMulC, LFSCPfLambda, LFSCBoolRes, and LFSCLraAdd.
Definition at line 100 of file LFSCProof.h.
Referenced by fillHoles(), checkOp(), and get_string_length().
virtual LFSCProof* LFSCProof::getChild | ( | int | n | ) | [inline, virtual] |
Reimplemented in LFSCLraContra, LFSCLraPoly, LFSCAssume, LFSCLraSub, LFSCProofGeneric, LFSCClausify, LFSCLraMulC, LFSCPfLambda, LFSCBoolRes, and LFSCLraAdd.
Definition at line 101 of file LFSCProof.h.
Referenced by fillHoles(), checkOp(), get_string_length(), and TReturn::normalize_to_tf().
int LFSCProof::checkOp | ( | ) | [virtual] |
Reimplemented in LFSCLraContra, LFSCLraPoly, LFSCLraSub, LFSCLraMulC, LFSCLraAxiom, and LFSCLraAdd.
Definition at line 83 of file LFSCProof.cpp.
References chOp, getNumChildren(), getChild(), and checkOp().
Referenced by LFSCLraAdd::Make(), LFSCLraMulC::LFSCLraMulC(), LFSCLraSub::LFSCLraSub(), LFSCLraPoly::LFSCLraPoly(), LFSCLraContra::LFSCLraContra(), and checkOp().
int LFSCProof::getChOp | ( | ) | [inline] |
Definition at line 103 of file LFSCProof.h.
References chOp.
Referenced by TReturn::normalize_tr(), and TReturn::normalize_to_tf().
void LFSCProof::setChOp | ( | int | c | ) | [inline] |
Definition at line 104 of file LFSCProof.h.
References chOp.
Referenced by LFSCLraPoly::Make(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().
virtual int LFSCProof::checkBoolRes | ( | std::vector< int > & | clause | ) | [inline, virtual] |
Reimplemented in LFSCAssume, LFSCClausify, LFSCLem, and LFSCBoolRes.
Definition at line 105 of file LFSCProof.h.
Definition at line 104 of file LFSCProof.cpp.
References LFSCObj::cascade_expr(), std::endl(), LFSCObj::queryM(), LFSCObj::d_or_final_s, LFSCPfVar::Make(), CVC3::abs(), LFSCClausify::Make(), RefPtr::get(), LFSCAssume::Make(), CVC3::Expr::arity(), LFSCProofGeneric::Make(), LFSCObj::d_and_final_s, LFSCProofGeneric::MakeStr(), CVC3::Expr::getKind(), AND, LFSCObj::d_imp_s, LFSCObj::d_ite_s, NOT, LFSCObj::d_iff_s, LFSCObj::d_or_mid_s, LFSCObj::d_and_mid_s, Make_and_elim(), and Obj::print_error().
Referenced by LFSCConvert::cvc3_to_lfsc().
Definition at line 372 of file LFSCProof.cpp.
References CVC3::Expr::isNot(), and LFSCProofGeneric::Make().
Referenced by LFSCConvert::cvc3_to_lfsc().
Definition at line 384 of file LFSCProof.cpp.
References LFSCProofGeneric::Make().
Referenced by LFSCConvert::cvc3_to_lfsc().
LFSCProof * LFSCProof::Make_and_elim | ( | const Expr & | form, |
LFSCProof * | p, | ||
int | n, | ||
const Expr & | expected | ||
) | [static] |
Definition at line 397 of file LFSCProof.cpp.
References LFSCObj::cascade_expr(), CVC3::Expr::arity(), Obj::print_error(), and LFSCProofGeneric::Make().
Referenced by LFSCConvert::cvc3_to_lfsc(), and Make_CNF().
static int LFSCProof::get_proof_counter | ( | ) | [inline, static] |
Definition at line 114 of file LFSCProof.h.
References pf_counter.
friend class LFSCPrinter [friend] |
Reimplemented in LFSCClausify.
Definition at line 97 of file LFSCProof.h.
int LFSCProof::pf_counter = 0 [static, protected] |
Definition at line 28 of file LFSCProof.h.
Referenced by LFSCProof(), and get_proof_counter().
std::map< LFSCProof *, int > LFSCProof::lambdaMap [static, protected] |
Definition at line 29 of file LFSCProof.h.
Referenced by print(), print_structure(), and make_lambda().
std::map< LFSCProof *, LFSCProof * > LFSCProof::lambdaPrintMap [static, protected] |
Definition at line 30 of file LFSCProof.h.
Referenced by print(), print_structure(), LFSCPfLambda::print_pf(), LFSCPfLet::print_pf(), and LFSCPfLet::print_struct().
int LFSCProof::printCounter [protected] |
Definition at line 31 of file LFSCProof.h.
Referenced by LFSCProof(), print(), and print_structure().
LFSCProof* LFSCProof::rplProof [protected] |
Definition at line 32 of file LFSCProof.h.
Referenced by LFSCProof(), print(), print_structure(), and setRplProof().
int LFSCProof::lambdaCounter = 1 [static, protected] |
Definition at line 33 of file LFSCProof.h.
Referenced by make_lambda().
long int LFSCProof::strLen [protected] |
Definition at line 34 of file LFSCProof.h.
Referenced by LFSCProof(), and get_string_length().
int LFSCProof::chOp [protected] |
Definition at line 35 of file LFSCProof.h.
Referenced by LFSCProof(), checkOp(), getChOp(), and setChOp().
int LFSCProof::assumeVar [protected] |
Definition at line 36 of file LFSCProof.h.
Referenced by LFSCProof().
int LFSCProof::assumeVarUsed [protected] |
Definition at line 37 of file LFSCProof.h.
Referenced by LFSCProof().
std::vector< int > LFSCProof::br [protected] |
Definition at line 39 of file LFSCProof.h.
bool LFSCProof::brComputed [protected] |
Definition at line 40 of file LFSCProof.h.
Referenced by LFSCProof().