/dports/math/cvc3/cvc3-2.4.1/src/search/ |
H A D | LFSCLraProof.h | 12 LFSCLraAdd(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2): LFSCProof(), in LFSCLraAdd() 25 static LFSCProof* Make(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2); 63 LFSCLraMulC(LFSCProof* pf, Rational r, int op): LFSCProof(), in LFSCLraMulC() 75 static LFSCProof* Make(LFSCProof* pf, Rational r, int op); 88 LFSCLraSub(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2): LFSCProof(), in LFSCLraSub() 103 static LFSCProof* Make(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2); 116 LFSCLraPoly( LFSCProof* pf, int var, int op ) : LFSCProof(), in LFSCLraPoly() 127 static LFSCProof* Make( LFSCProof* pf, int var, int op ){ in Make() 130 static LFSCProof* Make( const Expr& e, LFSCProof* p ); 145 LFSCLraContra( LFSCProof* pf, int op ) : LFSCProof(), in LFSCLraContra() [all …]
|
H A D | LFSCUtilProof.h | 6 class LFSCProofExpr : public LFSCProof 42 RefPtr< LFSCProof > body; 44 RefPtr< LFSCProof > abstVal; 46 LFSCPfLambda( LFSCPfVar* v, LFSCProof* bd, LFSCProof* aVal = NULL ) : LFSCProof(), in LFSCProof() function 53 static LFSCProof* Make( LFSCPfVar* v, LFSCProof* bd, LFSCProof* aVal = NULL ){ 58 LFSCProof* getChild( int n ) { return (n==0) ? (LFSCProof*)pfV.get() : body.get(); } in getChild() 86 …static LFSCProof* Make( string str_pre, LFSCProof* sub_pf1, LFSCProof* sub_pf2, string str_post, b… 105 LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body, in LFSCPfLet() 106 bool isTh, LFSCProof* letPfRpl, LFSCProof* pvRpl ) : LFSCProof(), in LFSCPfLet() 108 LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body, [all …]
|
H A D | LFSCBoolProof.h | 6 class LFSCBoolRes : public LFSCProof 12 LFSCBoolRes(LFSCProof* pf1, LFSCProof* pf2, int v, bool col): LFSCProof(), in LFSCBoolRes() 26 static LFSCProof* Make(LFSCProof* pf1, LFSCProof* pf2, int v, bool col); 29 …static LFSCProof* Make( LFSCProof* p1, LFSCProof* p2, const Expr& res, const Expr& pf, bool cascad… 31 static LFSCProof* MakeC( LFSCProof* p, const Expr& res ); 65 RefPtr< LFSCProof > d_pf; 66 LFSCClausify( int v, LFSCProof* pf ) : LFSCProof(), d_var( v ), d_pf( pf ){} in LFSCClausify() 76 static LFSCProof* Make( int v, LFSCProof* pf ){ return new LFSCClausify( v, pf ); } in Make() 78 static LFSCProof* Make( const Expr& e, LFSCProof* p, bool cascadeOr = false ); 93 RefPtr< LFSCProof > d_pf; [all …]
|
H A D | LFSCProof.h | 26 class LFSCProof : public LFSCObj{ 29 static std::map< LFSCProof*, int > lambdaMap; 30 static std::map< LFSCProof*, LFSCProof* > lambdaPrintMap; 32 LFSCProof* rplProof; 42 LFSCProof(); 44 virtual ~LFSCProof(){} in ~LFSCProof() 63 static int make_lambda( LFSCProof* p ){ in make_lambda() 99 virtual LFSCProof* clone() = 0; 110 static LFSCProof* Make_not_not_elim( const Expr& pf, LFSCProof* p ); 111 static LFSCProof* Make_mimic( const Expr& pf, LFSCProof* p, int numHoles ); [all …]
|
H A D | LFSCUtilProof.cpp | 31 std::map< int, RefPtr< LFSCProof > > LFSCPfVar::vMap; 33 LFSCProof* LFSCPfVar::Make( const char* c, int v ) in Make() 40 LFSCProof* LFSCPfVar::MakeV( int v ) in MakeV() 42 RefPtr< LFSCProof > pf = vMap[v]; in MakeV() 90 LFSCProof* LFSCProofGeneric::Make( string str_pre, LFSCProof* sub_pf, string str_post, bool db_str ) in Make() 92 vector< RefPtr< LFSCProof > > d_pfs; in Make() 100 LFSCProof* LFSCProofGeneric::Make( string str_pre, LFSCProof* sub_pf1, LFSCProof* sub_pf2, string s… in Make() 102 vector< RefPtr< LFSCProof > > d_pfs; in Make() 115 vector< RefPtr< LFSCProof > > d_pfs; in MakeStr() 124 LFSCPfLet::LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body, in LFSCPfLet() [all …]
|
H A D | LFSCProof.cpp | 6 int LFSCProof::pf_counter = 0; 7 std::map< LFSCProof*, int > LFSCProof::lambdaMap; 8 std::map< LFSCProof*, LFSCProof* > LFSCProof::lambdaPrintMap; 9 int LFSCProof::lambdaCounter = 1; 11 LFSCProof::LFSCProof() in LFSCProof() function in LFSCProof 83 int LFSCProof::checkOp() { in checkOp() 104 LFSCProof* LFSCProof::Make_CNF( const Expr& form, const Expr& reason, int pos ) in Make_CNF() 115 RefPtr< LFSCProof > p; in Make_CNF() 372 LFSCProof* LFSCProof::Make_not_not_elim( const Expr& pf, LFSCProof* p ) in Make_not_not_elim() 384 LFSCProof* LFSCProof::Make_mimic( const Expr& pf, LFSCProof* p, int numHoles ) in Make_mimic() [all …]
|
H A D | LFSCLraProof.cpp | 17 LFSCProof* LFSCLraAdd::Make(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2) in Make() 35 RefPtr< LFSCProof > LFSCLraAxiom::eq; 37 LFSCProof* LFSCLraAxiom::MakeEq(){ in MakeEq() 65 LFSCProof* LFSCLraMulC::Make(LFSCProof* pf, Rational r, int op) in Make() 89 LFSCProof* LFSCLraSub::Make(LFSCProof* pf1, LFSCProof* pf2, int op1, int op2){ in Make() 117 LFSCProof* LFSCLraPoly::Make( const Expr& e, LFSCProof* p ) in Make()
|
H A D | LFSCBoolProof.cpp | 32 LFSCProof* LFSCBoolRes::Make(LFSCProof* pf1, LFSCProof* pf2, int v, bool col){ in Make() 66 LFSCProof* LFSCBoolRes::Make( LFSCProof* p1, LFSCProof* p2, const Expr& res, in Make() 93 LFSCProof* LFSCBoolRes::MakeC( LFSCProof* p, const Expr& res ){ in MakeC() 121 LFSCProof* LFSCClausify::Make( const Expr& e, LFSCProof* p, bool cascadeOr ) in Make() 134 LFSCProof* LFSCClausify::Make_i( const Expr& e, LFSCProof* p, std::vector< Expr >& exprs, const Exp… in Make_i()
|
H A D | LFSCConvert.cpp | 146 …RefPtr< LFSCProof > p = LFSCProof::Make_CNF( pf[2], pf[1], pf[4].getRational().getNumerator().getI… 154 …RefPtr< LFSCProof > p = LFSCProof::Make_CNF( pf[1], d_ite_s, pf[5].getRational().getNumerator().ge… 199 RefPtr< LFSCProof > p; 285 RefPtr< LFSCProof > p; 872 … RefPtr< LFSCProof > p = LFSCProof::Make_and_elim( pf[2], t->getLFSCProof(), pos, pf[2][pos] ); 878 RefPtr< LFSCProof > p = LFSCProof::Make_CNF( pf[2], d_and_mid_s, 889 RefPtr< LFSCProof > p = LFSCProof::Make_CNF( ei, d_imp_s, 3 ); 1022 RefPtr <LFSCProof> p; 1467 RefPtr< LFSCProof > p; 1663 LFSCProof* LFSCConvert::make_let_proof( LFSCProof* p ) [all …]
|
H A D | LFSCConvert.h | 10 RefPtr< LFSCProof > pfinal; 41 LFSCProof* make_let_proof( LFSCProof* p ); 51 LFSCProof* getLFSCProof() { return pfinal.get(); } in getLFSCProof()
|
H A D | TReturn.h | 14 RefPtr< LFSCProof > d_lfsc_pf; 31 …TReturn(LFSCProof* lfsc_pf, std::vector<int>& L, std::vector<int>& Lused, Rational r, bool hasR, i… 37 LFSCProof* getLFSCProof(){ return d_lfsc_pf.get(); } in getLFSCProof()
|
H A D | TReturn.cpp | 8 TReturn::TReturn(LFSCProof* lfsc_pf, std::vector<int>& L, std::vector<int>& Lused, Rational r, bool… in TReturn() 184 RefPtr< LFSCProof > p = LFSCProofExpr::Make( e[0] ); in normalize_tr() 231 std::vector< RefPtr< LFSCProof > > pfs; in normalize_tr() 251 RefPtr< LFSCProof > p; in normalize_tr() 316 RefPtr< LFSCProof > p = LFSCPfVar::Make( "@v", abs( val1 ) ); in normalize_tr() 345 RefPtr< LFSCProof > p; in normalize_tr() 356 RefPtr< LFSCProof > p1 = LFSCPfVar::Make( "@v", abs( val1 ) ); in normalize_tr() 357 RefPtr< LFSCProof > p2 = LFSCPfVar::Make( "@v", abs( val2 ) ); in normalize_tr() 454 RefPtr< LFSCProof > p = LFSCPfVar::Make( "@v", abs( val ) ); in normalize_to_tf()
|
H A D | Makefile | 27 LFSCProof.cpp \ 33 …hing.h decision_engine_mbtf.h Util.h TReturn.h Object.h LFSCUtilProof.h LFSCProof.h LFSCPrinter.h …
|
H A D | LFSCPrinter.cpp | 164 RefPtr< LFSCProof > lambda_pf = converter->getLFSCProof(); in print_LFSC() 243 LFSCProof::indentFlag = true; in print_LFSC()
|
/dports/math/cvc4/CVC4-1.7/src/proof/ |
H A D | proof_manager.h | 323 class LFSCProof : public Proof 326 LFSCProof(SmtEngine* smtEngine, 330 ~LFSCProof() override {} in ~LFSCProof()
|
H A D | proof_manager.cpp | 90 currentPM()->d_fullProof.reset(new LFSCProof( in getProof() 546 LFSCProof::LFSCProof(SmtEngine* smtEngine, in LFSCProof() function in CVC4::LFSCProof 556 void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const in toStream() 561 void LFSCProof::toStream(std::ostream& out) const in toStream() 748 void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, in printPreprocessedAssertions() 848 void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) const in checkUnrewrittenAssertion()
|