Searched refs:addedLemma (Results 1 – 10 of 10) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | regexp_solver.cpp | 87 bool addedLemma = false; in check() local
151 addedLemma = true; in check()
172 if (!addedLemma) in check()
227 addedLemma = true; in check()
234 flag = checkPDerivative(x, r, atom, addedLemma, rnfexp); in check()
263 addedLemma = true; in check()
280 if (addedLemma) in check()
301 Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp) in checkPDerivative() argument
314 addedLemma = true; in checkPDerivative()
330 addedLemma = true; in checkPDerivative()
[all …]
|
| H A D | regexp_solver.h | 75 Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp);
|
| H A D | theory_strings.h | 610 bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp);
|
| H A D | theory_strings.cpp | 1003 bool addedLemma = false; in check() local
1009 addedLemma = !d_lemma_cache.empty(); in check()
1013 }while( !d_conflict && !addedLemma && addedFact ); in check()
1015 …Trace("strings-check") << "Theory of strings done full effort check " << addedLemma << " " << d_co… in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_engine.cpp | 329 bool addedLemma = false; in checkConjecture() local
337 addedLemma = true; in checkConjecture()
346 if (addedLemma) in checkConjecture()
368 bool addedLemma = false; in checkConjecture() local
379 addedLemma = true; in checkConjecture()
386 if (addedLemma) in checkConjecture()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | anti_skolem.cpp | 215 bool addedLemma = false; in sendAntiSkolemizeLemma() local
219 addedLemma = addedLemma || ret; in sendAntiSkolemizeLemma()
221 return addedLemma; in sendAntiSkolemizeLemma()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | ext_theory.cpp | 202 bool addedLemma = false; in doInferencesInternal() local
223 addedLemma = true; in doInferencesInternal()
273 addedLemma = true; in doInferencesInternal()
304 return addedLemma; in doInferencesInternal()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | bounded_integers.cpp | 287 bool addedLemma = false; in check() local
297 addedLemma = true; in check()
300 Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl; in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.cpp | 636 bool addedLemma = false; in check() local
738 addedLemma = true; in check()
756 …Trace("sep-process") << "...finished check of negated assertions, addedLemma=" << addedLemma << ",… in check()
758 if( !addedLemma ){ in check()
789 addedLemma = true; in check()
800 if( !addedLemma ){ in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf_strong_solver.cpp | 715 bool addedLemma = false; in check() local
724 addedLemma = true; in check()
737 if( !addedLemma ){ in check()
|