| /dports/math/z3/z3-z3-4.8.13/src/muz/spacer/ |
| H A D | spacer_legacy_frames.cpp | 103 add_lemma(curr, solver_level); in propagate_to_next_level()
123 bool pred_transformer::legacy_frames::add_lemma(expr * lemma, unsigned lvl) in add_lemma() function in spacer::pred_transformer::legacy_frames
155 { add_lemma(lemmas.get(j), infty_level()); } in propagate_to_infinity()
166 for (; it != end; ++it) { add_lemma(it->m_key, it->m_value); } in inherit_frames()
|
| H A D | spacer_legacy_frames.h | 26 bool add_lemma (expr * lemma, unsigned level);
|
| H A D | spacer_context.h | 276 add_lemma(new_lemma.get()); in inherit_frames()
282 bool add_lemma (lemma *new_lemma);
507 bool add_lemma(expr * e, unsigned lvl, bool bg);
508 bool add_lemma(lemma* lem) {return m_frames.add_lemma(lem);} in add_lemma() function
688 void add_lemma(lemma* new_lemma) {m_lemmas.push_back(new_lemma);} in add_lemma() function
|
| H A D | spacer_context.cpp | 970 bool pred_transformer::add_lemma (expr *e, unsigned lvl, bool bg) { in add_lemma() function in spacer::pred_transformer
973 return m_frames.add_lemma(lem.get()); in add_lemma()
1225 add_lemma(f, level, bg); in add_cover()
1964 bool pred_transformer::frames::add_lemma(lemma *new_lemma) in add_lemma() function in spacer::pred_transformer::frames
1994 pob->add_lemma(old_lemma); in add_lemma()
2047 if (new_lemma->has_pob()) {new_lemma->get_pob()->add_lemma(new_lemma);} in add_lemma()
3603 bool v = n.pt().add_lemma (lemma.get()); in expand_pob()
4085 if (r->add_lemma(lem.get())) { in add_constraint()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/spacer/ |
| H A D | spacer_legacy_frames.cpp | 103 add_lemma(curr, solver_level); in propagate_to_next_level()
123 bool pred_transformer::legacy_frames::add_lemma(expr * lemma, unsigned lvl) in add_lemma() function in spacer::pred_transformer::legacy_frames
155 { add_lemma(lemmas.get(j), infty_level()); } in propagate_to_infinity()
166 for (; it != end; ++it) { add_lemma(it->m_key, it->m_value); } in inherit_frames()
|
| H A D | spacer_legacy_frames.h | 26 bool add_lemma (expr * lemma, unsigned level);
|
| H A D | spacer_context.h | 276 add_lemma(new_lemma.get()); in inherit_frames()
282 bool add_lemma (lemma *new_lemma);
509 bool add_lemma(expr * e, unsigned lvl, bool bg);
510 bool add_lemma(lemma* lem) {return m_frames.add_lemma(lem);} in add_lemma() function
690 void add_lemma(lemma* new_lemma) {m_lemmas.push_back(new_lemma);} in add_lemma() function
|
| H A D | spacer_context.cpp | 970 bool pred_transformer::add_lemma (expr *e, unsigned lvl, bool bg) { in add_lemma() function in spacer::pred_transformer
973 return m_frames.add_lemma(lem.get()); in add_lemma()
1225 add_lemma(f, level, bg); in add_cover()
1964 bool pred_transformer::frames::add_lemma(lemma *new_lemma) in add_lemma() function in spacer::pred_transformer::frames
1994 pob->add_lemma(old_lemma); in add_lemma()
2047 if (new_lemma->has_pob()) {new_lemma->get_pob()->add_lemma(new_lemma);} in add_lemma()
3603 bool v = n.pt().add_lemma (lemma.get()); in expand_pob()
4085 if (r->add_lemma(lem.get())) { in add_constraint()
|
| /dports/math/abella/abella-2.0.7/src/ |
| H A D | abella.ml | 353 Prover.add_lemma name tys thm ;
678 Prover.add_lemma name tys thm
693 Prover.add_lemma n tys t ;
|
| H A D | prover.ml | 553 let add_lemma name tys lemma = function
|
| /dports/lang/ocaml/ocaml-4.05.0/testsuite/tests/misc/ |
| H A D | boyer.ml | 33 let add_lemma = function
104 let add t = add_lemma (cterm_to_term t)
|
| /dports/lang/ocaml-nox11/ocaml-4.05.0/testsuite/tests/misc/ |
| H A D | boyer.ml | 33 let add_lemma = function
104 let add t = add_lemma (cterm_to_term t)
|
| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btorslvfun.c | 1418 add_lemma (Btor *btor, BtorNode *fun, BtorNode *app1, BtorNode *app2) in add_lemma() function
1739 add_lemma (btor, fun, hashed_app, app); in propagate()
1798 add_lemma (btor, fun, app, 0); in propagate()
1860 add_lemma (btor, fun, app, 0); in propagate()
|
| /dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
| H A D | smt_core.c | 4413 static void add_lemma(smt_core_t *s, uint32_t n, literal_t *a) { in add_lemma() function
4458 add_lemma(s, n, lemma); in add_all_lemmas()
|