| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | datatypes_sygus.cpp | 1177 Node lem = in registerSymBreakLemmaForValue() local
1185 void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz, Node a, std::vect… in registerSymBreakLemma()
1243 for (const Node& lem : it->second) in addSymBreakLemmasFor() local
1479 for (const Node& lem : it->second) in incrementCurrentSearchSize() local
1515 for (const Node& lem : sbl) in check() local
1639 for (const Node& lem : lemmas) in check() local
|
| H A D | theory_datatypes.cpp | 398 Node lem = fact; in flushPendingFacts() local
447 bool TheoryDatatypes::doSendLemma( Node lem ) { in doSendLemma()
1720 Node lem; in collectTerms() local
|
| /dports/devel/pear-PHP_ParserGenerator/PHP_ParserGenerator-0.1.7/ParserGenerator/ |
| H A D | Parser.php | 182 function __construct(PHP_ParserGenerator $lem)
|
| /dports/math/arb/arb-2.21.1/acb_dirichlet/test/ |
| H A D | t-platt_multieval.c | 94 arb_t lem, xi, x, beta, t0; in main() local
|
| /dports/games/heroes/heroes-0.21/src/ |
| H A D | render.c | 250 draw_lemming (a_pixel *dest, const a_lemming *lem, unsigned int pos) in draw_lemming()
295 draw_dead_lemming (a_pixel *dest_, const a_lemming *lem) in draw_dead_lemming()
|
| H A D | heroes.c | 331 find_lemming_direction (a_lemming *lem) in find_lemming_direction()
2359 a_lemming *lem; in update_lemmings() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/sets/ |
| H A D | theory_sets_private.cpp | 496 Node lem = NodeManager::currentNM()->mkNode( kind::OR, n, n.negate() ); in split() local
1013 …Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind… in checkDisequalities() local
1075 …Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::… in registerCardinalityTerm() local
1591 …Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp.size()==1 ? exp[0] : NodeManager::… in checkMinCard() local
1606 void TheorySetsPrivate::flushLemma( Node lem, bool preprocess ) { in flushLemma()
1690 bool TheorySetsPrivate::hasLemmaCached( Node lem ) { in hasLemmaCached()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | candidate_rewrite_database.cpp | 256 Node lem = d_tds->getExplain()->getExplanationForEquality(x, exc_sol); in addTerm() local
|
| H A D | skolemize.cpp | 43 Node lem = nb; in process() local
|
| H A D | anti_skolem.cpp | 292 Node lem = NodeManager::currentNM()->mkNode( kind::AND, quants ).negate(); in sendAntiSkolemizeLemma() local
|
| H A D | term_database.cpp | 392 Node lem = lits.size() == 1 ? lits[0] : nm->mkNode(OR, lits); in computeUfTerms() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | theory_arith_private.cpp | 1199 Node lem = mkAxiomForTotalIntDivision(n[0], one, toIntSkolem); in ppRewriteTerms() local
1230 Node lem; in ppRewriteTerms() local
1538 Node lem; in setupDivLike() local
1617 Node lem = abs_d.getMetaKind () == metakind::VARIABLE ? in axiomIteForTotalIntDivision() local
2205 void TheoryArithPrivate::outputLemma(TNode lem) { in outputLemma()
2878 Node lem = d_approxCuts.front(); in replayLogRec() local
2888 Node lem = d_acTmp.back(); in replayLogRec() local
3725 Node lem = d_approxCuts.front(); in check() local
3919 Node lem = NodeManager::currentNM()->mkNode(kind::OR, ub, lb); in branchIntegerVariable() local
4473 Node lem = *i; in presolve() local
[all …]
|
| H A D | nonlinear_extension.cpp | 658 int NonlinearExtension::flushLemma(Node lem) { in flushLemma()
2065 Node lem; in checkLastCall() local
2847 std::vector<Node>& lem) { in compareSign()
2889 NodeMultiset& b_exp_proc, std::vector<Node>& exp, std::vector<Node>& lem, in compareMonomial()
2937 std::vector<Node>& exp, std::vector<Node>& lem, in compareMonomial()
3878 Node lem; in checkTranscendentalInitialRefine() local
4367 Node lem = nm->mkNode(concavity == 1 ? GEQ : LEQ, tf, tplane); in checkTfTangentPlanesFun() local
4493 Node lem = nm->mkNode(concavity == 1 ? LEQ : GEQ, tf, splane); in checkTfTangentPlanesFun() local
|
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | resolution_bitvector_proof.cpp | 292 Expr lem = utils::mkOr(lemma); in printTheoryLemmaProof() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | bounded_integers.cpp | 76 Node lem = in proxyCurrentRangeLemma() local
690 Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] ); in getRsiSubsitution() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf.cpp | 196 Node lem; in getApplyUfForHoApply() local
798 Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq[0], conc ); in applyExtensionality() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | theory_bv.cpp | 444 Node lem = nm->mkNode(kind::AND, in doExtfInferences() local
486 Node lem = parent.eqNode(t); in doExtfInferences() local
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/spacer/ |
| H A D | spacer_context.cpp | 649 expr *lem = e == nullptr ? get_expr() : e; in instantiate() local
666 expr *lem = e == nullptr ? get_expr() : e; in mk_insts() local
971 lemma_ref lem = alloc(lemma, m, e, lvl); in add_lemma() local
1429 bool pred_transformer::is_ctp_blocked(lemma *lem) { in is_ctp_blocked()
1464 bool pred_transformer::is_invariant(unsigned level, lemma* lem, in is_invariant()
4083 lemma_ref lem = alloc(lemma, m, e2, level); in add_constraint() local
4095 void context::new_lemma_eh(pred_transformer &pt, lemma *lem) { in new_lemma_eh()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/ |
| H A D | spacer_context.cpp | 649 expr *lem = e == nullptr ? get_expr() : e; in instantiate() local
666 expr *lem = e == nullptr ? get_expr() : e; in mk_insts() local
971 lemma_ref lem = alloc(lemma, m, e, lvl); in add_lemma() local
1429 bool pred_transformer::is_ctp_blocked(lemma *lem) { in is_ctp_blocked()
1464 bool pred_transformer::is_invariant(unsigned level, lemma* lem, in is_invariant()
4083 lemma_ref lem = alloc(lemma, m, e2, level); in add_constraint() local
4095 void context::new_lemma_eh(pred_transformer &pt, lemma *lem) { in new_lemma_eh()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
| H A D | inst_strategy_e_matching.cpp | 528 Node lem = NodeManager::currentNM()->mkNode( OR, q.negate(), qq ); in addTrigger() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | term_database_sygus.cpp | 550 Node lem = getExplain()->getExplanationForEquality(x, exc_val); in registerEnumerator() local
686 Node lem = nm->mkNode(OR, ag, ag.negate()); in registerEnumerator() local
779 Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl) in registerSymBreakLemma()
|
| H A D | sygus_enumerator.cpp | 54 for (const Node& lem : sbl) in initialize() local
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | ceg_bv_instantiator.cpp | 732 Node lem, in collectExtracts()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/strings/ |
| H A D | regexp_operation.cpp | 1004 Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]); in simplifyPRegExp() local
1012 Node lem = s.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc) ); in simplifyPRegExp() local
|
| /dports/misc/urbit/urbit-urbit-0.6.0/jets/f/ |
| H A D | ut_mull.c | 667 u3_noun lem = _mull_in(van, sut, c3__noun, dox, p_gen); in _mull_in() local
|