Lines Matching refs:LFSCProof

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()
113 LFSCProof* LFSCProofGeneric::MakeStr( const char* c, bool db_str)  in MakeStr()
115   vector< RefPtr< LFSCProof > > d_pfs;  in MakeStr()
124 LFSCPfLet::LFSCPfLet( LFSCProof* letPf, LFSCPfVar* pv, LFSCProof* body,  in LFSCPfLet()
125                       bool isTh, std::vector< int >& fv ) : LFSCProof(), d_letPf( letPf ),  in LFSCPfLet()
138     RefPtr< LFSCProof > pv1 = LFSCPfVar::Make( "@@v", abs( fv[a] ) );  in LFSCPfLet()
139     RefPtr< LFSCProof > pv2 = LFSCPfVar::MakeV( abs( fv[a] ) );  in LFSCPfLet()
147     RefPtr< LFSCProof > pv2 = LFSCPfVar::MakeV( abs( fv[a] ) );  in LFSCPfLet()