| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | inst_strategy_cegqi.h | 46 bool addLemma(Node lem) override;
101 bool addLemma(Node lem);
|
| H A D | inst_strategy_cegqi.cpp | 48 bool CegqiOutputInstStrategy::addLemma(Node lem) in addLemma() function in CegqiOutputInstStrategy
50 return d_out->addLemma(lem); in addLemma()
432 d_quantEngine->addLemma(mlem); in preRegisterQuantifier()
571 d_quantEngine->addLemma(lems[i], false); in registerCounterexampleLemma()
648 bool InstStrategyCegqi::addLemma( Node lem ) { in addLemma() function in InstStrategyCegqi
649 return d_quantEngine->addLemma( lem ); in addLemma()
|
| H A D | ceg_instantiator.h | 33 virtual bool addLemma( Node lem ) = 0;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_engine.cpp | 308 d_quantEngine->addLemma(lem); in checkConjecture()
334 if (d_quantEngine->addLemma(lem)) in checkConjecture()
374 bool res = d_quantEngine->addLemma(lem); in checkConjecture()
|
| H A D | ce_guided_single_inv.h | 41 bool addLemma(Node lem) override;
227 bool addLemma( Node lem );
|
| H A D | ce_guided_single_inv.cpp | 41 bool CegqiOutputSingleInv::addLemma( Node n ) { in addLemma() function in CVC4::CegqiOutputSingleInv
42 return d_out->addLemma( n ); in addLemma()
445 bool CegSingleInv::addLemma(Node n) in addLemma() function in CVC4::CegSingleInv
|
| /dports/math/cvc3/cvc3-2.4.1/src/search/ |
| H A D | search_sat.cpp | 51 void addLemma(const Theorem& thm, int priority, bool atBottomScope) in addLemma() function in CVC3::SearchSatCoreSatAPI
52 { d_ss->addLemma(thm, priority, atBottomScope); } in addLemma()
170 void SearchSat::addLemma(const Theorem& thm, int priority, bool atBottomScope) in addLemma() function in SearchSat
189 addLemma(d_commonRules->excludedMiddle(e), priority); in addSplitter()
324 l = d_cnfManager->addLemma(d_pendingLemmas[i].first, d_lemmas); in getNewClauses()
|
| H A D | search_impl_base.cpp | 45 virtual void addLemma(const Theorem& thm, int priority, bool atBottomScope) in addLemma() function in CVC3::CoreSatAPI_implBase
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | cnf_manager.h | 261 Lit addLemma(CVC3::Theorem thm, CNF_Formula& cnf);
|
| H A D | search_sat.h | 182 void addLemma(const Theorem& thm, int priority = 0, bool atBotomScope = false);
|
| H A D | theory_core.h | 224 virtual void addLemma(const Theorem& thm, int priority = 0,
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | quant_split.cpp | 142 d_quantEngine->addLemma( lemmas[i], false ); in check()
|
| H A D | equality_query.cpp | 72 d_qe->addLemma(split); in processInferences()
|
| H A D | local_theory_ext.cpp | 141 d_quantEngine->addLemma( lemmas[i], false ); in check()
|
| H A D | anti_skolem.cpp | 295 return d_quantEngine->addLemma( lem ); in sendAntiSkolemizeLemma()
|
| H A D | instantiate.cpp | 275 if (!d_qe->addLemma(lem, true, false)) in addInstantiation()
|
| H A D | term_database.cpp | 405 d_quantEngine->addLemma(lem); in computeUfTerms()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | theory_datatypes.cpp | 2068 bool addLemma = false; in mustCommunicateFact() local
2070 addLemma = true; in mustCommunicateFact()
2074 addLemma = true; in mustCommunicateFact()
2077 addLemma = dt.involvesExternalType(); in mustCommunicateFact()
2080 addLemma = true; in mustCommunicateFact()
2082 if( addLemma ){ in mustCommunicateFact()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.h | 207 bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
|
| H A D | quantifiers_engine.cpp | 979 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ in addLemma() function in QuantifiersEngine
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
| H A D | ho_trigger.cpp | 502 if (d_quantEngine->addLemma(au)) in addHoTypeMatchPredicateLemmas()
|
| H A D | inst_strategy_e_matching.cpp | 529 d_quantEngine->addLemma( lem ); in addTrigger()
|
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | cnf_manager.cpp | 674 Lit CNF_Manager::addLemma(Theorem thm, CNF_Formula& cnf) in addLemma() function in CNF_Manager
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_core/ |
| H A D | theory.cpp | 158 d_theoryCore->d_coreSatAPI->addLemma(thm, priority, true); in addGlobalLemma()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | bounded_integers.cpp | 296 d_quantEngine->addLemma(prangeLem); in check()
|