Home
last modified time | relevance | path

Searched refs:d_pending_lem (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/datatypes/
H A Dtheory_datatypes.cpp382 if( !d_pending_lem.empty() ){ in flushPendingFacts()
384 while( i<(int)d_pending_lem.size() ){ in flushPendingFacts()
385 doSendLemma( d_pending_lem[i] ); in flushPendingFacts()
388 d_pending_lem.clear(); in flushPendingFacts()
1029 d_pending_lem.push_back( eq ); in getTermSkolemFor()
1730 d_pending_lem.push_back( lem ); in collectTerms()
H A Dtheory_datatypes.h211 std::vector< Node > d_pending_lem; variable
/dports/math/cvc4/CVC4-1.7/src/theory/sep/
H A Dtheory_sep.h207 std::vector< int > d_pending_lem; variable
H A Dtheory_sep.cpp1723 d_pending_lem.push_back( d_pending.size()-1 ); in sendLemma()
1730 if( d_pending_lem.empty() ){ in doPendingFacts()
1745 for( unsigned i=0; i<d_pending_lem.size(); i++ ){ in doPendingFacts()
1749 int index = d_pending_lem[i]; in doPendingFacts()
1760 d_pending_lem.clear(); in doPendingFacts()