| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | inst_match_trie.cpp | 112 Node lem, in recordInstLemma()
145 Node lem = getInstLemma(); in print() local
200 Node lem = getInstLemma(); in getInstantiations() local
241 Node lem = getInstLemma(); in getExplanationForInstLemmas() local
368 Node lem, in recordInstLemma()
404 Node lem = getInstLemma(); in print() local
459 Node lem = getInstLemma(); in getInstantiations() local
504 Node lem; in getExplanationForInstLemmas() local
|
| H A D | instantiate.cpp | 271 Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body); in addInstantiation() local
362 Node lem, in removeInstantiation()
579 for (const Node& lem : active_lemmas) in getUnsatCoreLemmas() local
|
| H A D | alpha_equivalence.cpp | 132 Node lem; in reduceQuantifier() local
|
| H A D | inst_propagator.h | 124 Node lem, in notifyInstantiation()
|
| H A D | inst_propagator.cpp | 592 void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) { in init()
629 Node lem, in notifyInstantiation()
693 unsigned InstPropagator::allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node … in allocateInstantiation()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | cegis.cpp | 157 for (const Node& lem : cre_lems) in addEvalLemmas() local
186 Node lem = nm->mkNode( in addEvalLemmas() local
297 void Cegis::addRefinementLemma(Node lem) in addRefinementLemma()
328 Node lem = waiting[wcounter]; in addRefinementLemmaConjunct() local
425 Node lem, in registerRefinementLemma()
461 for (const Node& lem : rlemmas) in getRefinementEvalLemmas() local
599 Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem); in sampleAddRefinementLemma() local
|
| H A D | synth_engine.cpp | 246 Node lem = q.eqNode(nq); in assignConjecture() local
303 for (const Node& lem : clems) in checkConjecture() local
330 for (const Node& lem : cclems) in checkConjecture() local
371 Node lem = rlems[i]; in checkConjecture() local
|
| H A D | sygus_module.h | 127 Node lem, in registerRefinementLemma()
|
| H A D | synth_conjecture.cpp | 236 Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]); in assign() local
467 Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false)); in doCheck() local
484 Node lem; in doCheck() local
920 Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp); in getEnumeratedValue() local
|
| H A D | cegis_unif.cpp | 355 for (const Node& lem : lemmas) in processConstructCandidates() local
366 Node lem, in registerRefinementLemma()
664 Node lem = NodeManager::currentNM()->mkNode(OR, disj); in registerEvalPtAtSize() local
|
| H A D | sygus_pbe.cpp | 258 Node lem = itsl->second.size() == 1 ? itsl->second[0] in initialize() local
274 Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj); in initialize() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | inst_strategy_cegqi.cpp | 48 bool CegqiOutputInstStrategy::addLemma(Node lem) in addLemma()
99 Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); in registerCbqiLemma() local
545 Node lem, in doNestedQE()
552 void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) in registerCounterexampleLemma()
648 bool InstStrategyCegqi::addLemma( Node lem ) { in addLemma()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.cpp | 796 Node lem; in reduceQuantifier() local
908 Node lem = d_skolemize->process(f); in assertQuantifier() local
979 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ in addLemma()
1003 bool QuantifiersEngine::removeLemma( Node lem ) { in removeLemma()
1022 Node lem = d_qepr->mkEPRAxiom( tn ); in addEPRAxiom() local
|
| H A D | ext_theory.cpp | 218 Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, n, nr); in doInferencesInternal() local
253 Node lem = eq; in doInferencesInternal() local
340 bool ExtTheory::sendLemma(Node lem, bool preprocess) in sendLemma()
|
| /dports/science/cdcl/dcl-5.4.8-C/src/grph2/uipack/ |
| H A D | uiybar.c | 29 static logical lem, lcx, lcy; in uiybar_() local
|
| H A D | uixbar.c | 29 static logical lem, lcx, lcy; in uixbar_() local
|
| H A D | uipcmp.c | 28 static logical lem, lcx, lcy; in uipcmp_() local
|
| /dports/textproc/miller/miller-5.10.2/c/parsing/ |
| H A D | lemon_main.c | 74 struct lemon lem; in main() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf_strong_solver.cpp | 1031 Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() ); in addSplit() local
1061 Node lem = NodeManager::currentNM()->mkNode(OR, eqs); in addCliqueLemma() local
1098 Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax ); in addTotalityAxiom() local
1111 Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax ); in addTotalityAxiom() local
1132 Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ), in simpleCheckCardinality() local
1140 bool SortModel::doSendLemma( Node lem ) { in doSendLemma()
1241 …Node lem = NodeManager::currentNM()->mkNode( OR, cl, NodeManager::currentNM()->mkNode( AND, force_… in debugModel() local
1304 Node lem = var.eqNode(d_totality_terms[0][i - 1]).notNode(); in getCardinalityLiteral() local
1596 Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() ); in check() local
|
| /dports/multimedia/v4l_compat/linux-5.13-rc2/drivers/net/fddi/skfp/ |
| H A D | pcmplc.c | 1057 struct lem_counter *lem = &phy->lem ; in reset_lem_struct() local
1070 struct lem_counter *lem = &phy->lem ; in lem_evaluate() local
1175 struct lem_counter *lem = &phy->lem ; in lem_check_lct() local
1219 struct lem_counter *lem = &smc->y[np].lem ; in sm_ph_lem_start() local
1237 struct lem_counter *lem = &smc->y[np].lem ; in sm_ph_lem_stop() local
|
| /dports/multimedia/libv4l/linux-5.13-rc2/drivers/net/fddi/skfp/ |
| H A D | pcmplc.c | 1057 struct lem_counter *lem = &phy->lem ; in reset_lem_struct() local
1070 struct lem_counter *lem = &phy->lem ; in lem_evaluate() local
1175 struct lem_counter *lem = &phy->lem ; in lem_check_lct() local
1219 struct lem_counter *lem = &smc->y[np].lem ; in sm_ph_lem_start() local
1237 struct lem_counter *lem = &smc->y[np].lem ; in sm_ph_lem_stop() local
|
| /dports/multimedia/v4l-utils/linux-5.13-rc2/drivers/net/fddi/skfp/ |
| H A D | pcmplc.c | 1057 struct lem_counter *lem = &phy->lem ; in reset_lem_struct() local
1070 struct lem_counter *lem = &phy->lem ; in lem_evaluate() local
1175 struct lem_counter *lem = &phy->lem ; in lem_check_lct() local
1219 struct lem_counter *lem = &smc->y[np].lem ; in sm_ph_lem_start() local
1237 struct lem_counter *lem = &smc->y[np].lem ; in sm_ph_lem_stop() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arrays/ |
| H A D | theory_arrays.cpp | 1620 RowLemmaType lem; in setNonLinear() local
1852 RowLemmaType lem; in checkStore() local
1890 RowLemmaType lem; in checkRowForIndex() local
1946 RowLemmaType lem; in checkRowLemmas() local
1980 void TheoryArrays::propagate(RowLemmaType lem) in propagate()
2035 void TheoryArrays::queueRowLemma(RowLemmaType lem) in queueRowLemma()
2243 Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r); in dischargeLemmas() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
| H A D | theory_sep.cpp | 347 Node lem; in check() local
432 Node lem; in check() local
471 Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit.negate(), conc ); in check() local
476 Node lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), conc ); in check() local
732 Node lem = NodeManager::currentNM()->mkNode( kind::OR, lemc ); in check() local
783 …Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, NodeManager::currentNM()->mkNode( kind… in check() local
1750 …Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, d_pending_exp[index], d_pending[index]… in doPendingFacts() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | theory_strings_preprocess.cpp | 195 Node lem = nm->mkNode(GEQ, leni, d_one); in simplify() local
274 Node lem = stoit.eqNode(d_neg_one); in simplify() local
436 std::vector<Node> lem; in simplify() local
|