Home
last modified time | relevance | path

Searched refs:LFSCProof (Results 1 – 16 of 16) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/search/
H A DLFSCLraProof.h12 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 DLFSCUtilProof.h6 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 DLFSCBoolProof.h6 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 DLFSCProof.h26 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 DLFSCUtilProof.cpp31 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 DLFSCProof.cpp6 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 DLFSCLraProof.cpp17 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 DLFSCBoolProof.cpp32 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 DLFSCConvert.cpp146 …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 DLFSCConvert.h10 RefPtr< LFSCProof > pfinal;
41 LFSCProof* make_let_proof( LFSCProof* p );
51 LFSCProof* getLFSCProof() { return pfinal.get(); } in getLFSCProof()
H A DTReturn.h14 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 DTReturn.cpp8 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 DMakefile27 LFSCProof.cpp \
33 …hing.h decision_engine_mbtf.h Util.h TReturn.h Object.h LFSCUtilProof.h LFSCProof.h LFSCPrinter.h …
H A DLFSCPrinter.cpp164 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 Dproof_manager.h323 class LFSCProof : public Proof
326 LFSCProof(SmtEngine* smtEngine,
330 ~LFSCProof() override {} in ~LFSCProof()
H A Dproof_manager.cpp90 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()