| /dports/math/z3/z3-z3-4.8.13/src/test/ |
| H A D | doc.cpp | 242 fml1 = to_formula(*d, dm); in test_project()
256 fml2 = to_formula(*result, m2); in test_project()
326 fml2 = to_formula(*d, dm); in test_merge()
383 fml1 = to_formula(*d, dm); in test_project1()
390 fml2 = to_formula(*result, m2); in test_project1()
443 fml1 = to_formula(d1, dm); in test_subtract()
444 fml2 = to_formula(d2, dm); in test_subtract()
446 fml3 = to_formula(d1, dm); in test_subtract()
460 fml1 = to_formula(d1, dm); in test_intersect()
461 fml2 = to_formula(d2, dm); in test_intersect()
[all …]
|
| H A D | udoc_relation.cpp | 189 t->to_formula(fml); in test1()
199 t->to_formula(fml); in test1()
278 t1->to_formula(t10); in test1()
280 delta->to_formula(delta0); in test1()
864 dst.to_formula(dst0); in apply_filter_neg()
911 t.to_formula(fml0); in apply_filter()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/test/ |
| H A D | doc.cpp | 242 fml1 = to_formula(*d, dm);
256 fml2 = to_formula(*result, m2);
326 fml2 = to_formula(*d, dm);
383 fml1 = to_formula(*d, dm);
390 fml2 = to_formula(*result, m2);
443 fml1 = to_formula(d1, dm);
444 fml2 = to_formula(d2, dm);
446 fml3 = to_formula(d1, dm);
460 fml1 = to_formula(d1, dm);
461 fml2 = to_formula(d2, dm);
[all …]
|
| H A D | udoc_relation.cpp | 189 t->to_formula(fml); in test1()
199 t->to_formula(fml); in test1()
278 t1->to_formula(t10); in test1()
280 delta->to_formula(delta0); in test1()
864 dst.to_formula(dst0); in apply_filter_neg()
911 t.to_formula(fml0); in apply_filter()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/rel/ |
| H A D | check_relation.cpp | 51 dst.to_formula(fml); in ground()
247 src.to_formula(fml1); in verify_filter_project()
248 dst.to_formula(fml2); in verify_filter_project()
258 src.to_formula(fml1); in verify_project()
259 dst.to_formula(fml2); in verify_project()
313 t.to_formula(fml2); in verify_join_project()
327 t1.to_formula(fml1); in mk_join()
328 t2.to_formula(fml2); in mk_join()
371 src.to_formula(fml1); in verify_permutation()
372 dst.to_formula(fml2); in verify_permutation()
[all …]
|
| H A D | udoc_relation.h | 37 expr_ref to_formula(tbv const& t) const;
38 expr_ref to_formula(doc const& d) const;
48 void to_formula(expr_ref& fml) const override;
|
| H A D | dl_table_relation.h | 117 … void to_formula(expr_ref& fml) const override { get_table().to_formula(get_signature(), fml); } in to_formula() function
|
| H A D | doc.cpp | 608 expr_ref fml = to_formula(m, src); in is_empty_complete()
673 expr_ref fml1 = to_formula(m, src); in verify_project()
674 expr_ref fml2 = dstm.to_formula(m, dst); in verify_project()
698 expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) { in to_formula() function in doc_manager
701 conj.push_back(tbvm().to_formula(m, src.pos())); in to_formula()
703 conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i]))); in to_formula()
|
| H A D | rel_context.cpp | 259 rel.to_formula(e); in query()
293 rm.get_relation(p).to_formula(fml); in get_model()
372 m_last_result_relation->to_formula(m_answer); in query()
460 rb->to_formula(result); in try_get_formula()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/rel/ |
| H A D | check_relation.cpp | 51 dst.to_formula(fml); in ground()
247 src.to_formula(fml1); in verify_filter_project()
248 dst.to_formula(fml2); in verify_filter_project()
258 src.to_formula(fml1); in verify_project()
259 dst.to_formula(fml2); in verify_project()
313 t.to_formula(fml2); in verify_join_project()
327 t1.to_formula(fml1); in mk_join()
328 t2.to_formula(fml2); in mk_join()
371 src.to_formula(fml1); in verify_permutation()
372 dst.to_formula(fml2); in verify_permutation()
[all …]
|
| H A D | udoc_relation.h | 37 expr_ref to_formula(tbv const& t) const;
38 expr_ref to_formula(doc const& d) const;
48 void to_formula(expr_ref& fml) const override;
|
| H A D | dl_table_relation.h | 117 … void to_formula(expr_ref& fml) const override { get_table().to_formula(get_signature(), fml); } in to_formula() function
|
| H A D | doc.cpp | 608 expr_ref fml = to_formula(m, src); in is_empty_complete()
673 expr_ref fml1 = to_formula(m, src); in verify_project()
674 expr_ref fml2 = dstm.to_formula(m, dst); in verify_project()
698 expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) { in to_formula() function in doc_manager
701 conj.push_back(tbvm().to_formula(m, src.pos())); in to_formula()
703 conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i]))); in to_formula()
|
| H A D | rel_context.cpp | 259 rel.to_formula(e);
293 rm.get_relation(p).to_formula(fml);
372 m_last_result_relation->to_formula(m_answer);
460 rb->to_formula(result);
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/aig/ |
| H A D | aig.h | 70 void to_formula(aig_ref const & r, expr_ref & result);
71 void to_formula(aig_ref const & r, goal & result);
|
| H A D | aig_tactic.cpp | 76 m_aig_manager->to_formula(r, new_f); in operator ()()
86 m_aig_manager->to_formula(r, *(g.get())); in operator ()()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/aig/ |
| H A D | aig.h | 70 void to_formula(aig_ref const & r, expr_ref & result);
71 void to_formula(aig_ref const & r, goal & result);
|
| H A D | aig_tactic.cpp | 76 m_aig_manager->to_formula(r, new_f);
86 m_aig_manager->to_formula(r, *(g.get()));
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/transforms/ |
| H A D | dl_mk_coalesce.cpp | 137 rm.to_formula(src, fml1); in merge_rules()
138 rm.to_formula(*tgt.get(),fml2); in merge_rules()
139 rm.to_formula(*res.get(),fml); in merge_rules()
|
| H A D | dl_mk_bit_blast.cpp | 244 m_context.get_rule_manager().to_formula(*r2.get(), fml1); in blast()
285 rm.to_formula(*r, fml); in operator ()()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/transforms/ |
| H A D | dl_mk_coalesce.cpp | 137 rm.to_formula(src, fml1); in merge_rules()
138 rm.to_formula(*tgt.get(),fml2); in merge_rules()
139 rm.to_formula(*res.get(),fml); in merge_rules()
|
| /dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
| H A D | dl_util.cpp | 318 rm.to_formula(r1, fml1); in resolve_rule()
319 rm.to_formula(r2, fml2); in resolve_rule()
320 rm.to_formula(res, fml3); in resolve_rule()
358 rm.to_formula(res, fml); in resolve_rule()
|
| H A D | dl_rule.cpp | 207 to_formula(*r, fml1); in mk_horn_rule()
225 to_formula(*r, fml2); in mk_horn_rule()
557 void rule_manager::to_formula(rule const& r, expr_ref& fml) { in to_formula() function in datalog::rule_manager
602 to_formula(r, fml); in display_smt2()
795 to_formula(new_rule, fml); in mk_rule_rewrite_proof()
806 to_formula(r, fml); in mk_rule_asserted_proof()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
| H A D | dl_util.cpp | 318 rm.to_formula(r1, fml1); in resolve_rule()
319 rm.to_formula(r2, fml2); in resolve_rule()
320 rm.to_formula(res, fml3); in resolve_rule()
358 rm.to_formula(res, fml); in resolve_rule()
|
| H A D | dl_rule.cpp | 207 to_formula(*r, fml1); in ScopedUpdatesClearer()
225 to_formula(*r, fml2); in ScopedUpdatesClearer()
557 void rule_manager::to_formula(rule const& r, expr_ref& fml) { in ScopedUpdatesClearer()
602 to_formula(r, fml); in ScopedUpdatesClearer()
795 to_formula(new_rule, fml); in ScopedUpdatesClearer()
806 to_formula(r, fml); in ScopedUpdatesClearer()
|