Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/strings/
H A Dtheory_strings.cpp1009 addedLemma = !d_lemma_cache.empty(); in check()
1019 Assert( d_lemma_cache.empty() ); in check()
1344 if( !d_conflict && !d_lemma_cache.empty() ){ in doPendingLemmas()
1345 for( unsigned i=0; i<d_lemma_cache.size(); i++ ){ in doPendingLemmas()
1347 d_out->lemma( d_lemma_cache[i] ); in doPendingLemmas()
1354 d_lemma_cache.clear(); in doPendingLemmas()
1359 return d_conflict || !d_lemma_cache.empty() || !d_pending.empty(); in hasProcessed()
4112 d_lemma_cache.push_back( lem ); in sendLemma()
4155 d_lemma_cache.push_back(lemma_or); in sendSplit()
4432 if( cols[i].size()>1 && d_lemma_cache.empty() ){ in checkNormalFormsDeq()
[all …]
H A Dtheory_strings.h305 std::vector< Node > d_lemma_cache; variable
/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dtheory_uf_strong_solver.h284 NodeBoolMap d_lemma_cache; variable
H A Dtheory_uf_strong_solver.cpp476 d_lemma_cache(u), in SortModel()
1141 if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){ in doSendLemma()
1142 d_lemma_cache[lem] = true; in doSendLemma()