Home
last modified time | relevance | path

Searched refs:euf (Results 1 – 25 of 385) sorted by relevance

12345678910>>...16

/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Darray_solver.h23 namespace euf {
29 class solver : public euf::th_euf_solver {
30 typedef euf::theory_var theory_var;
31 typedef euf::theory_id theory_id;
76 void ensure_var(euf::enode* n);
94 euf::enode* n;
95 euf::enode* select;
97 …axiom_record(kind_t k, euf::enode* n, euf::enode* select = nullptr) : m_kind(k), n(n), select(sele… in m_kind()
204 euf::th_solver* clone(euf::solver& ctx) override;
210 void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
[all …]
H A Darray_model.cpp25 void solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { in add_dep()
30 for (euf::enode* p : euf::enode_parents(n)) { in add_dep()
41 for (euf::enode* k : euf::enode_class(n)) in add_dep()
57 for (euf::enode* k : euf::enode_class(n)) in add_value()
62 for (euf::enode* p : euf::enode_parents(n)) in add_value()
70 for (euf::enode* p : euf::enode_parents(n)) { in add_value()
89 for (euf::enode* p : euf::enode_parents(n)) { in add_value()
119 for (euf::enode* p : euf::enode_parents(r)) in have_different_model_values()
156 auto maps_diff = [&](euf::enode* p, euf::enode* else_, euf::enode* r) { in have_different_model_values()
159 auto table_diff = [&](euf::enode* r1, euf::enode* r2, euf::enode* else1) { in have_different_model_values()
[all …]
H A Darray_internalize.cpp39 euf::theory_var solver::mk_var(euf::enode* n) { in mk_var()
47 void solver::ensure_var(euf::enode* n) { in ensure_var()
49 if (v == euf::null_theory_var) { in ensure_var()
68 for (auto* arg : euf::enode_args(n)) { in internalize_map()
99 euf::enode* n = expr2enode(e); in visited()
108 euf::enode* n = expr2enode(e); in visit()
117 euf::enode* n = expr2enode(e); in post_visit()
124 for (auto* arg : euf::enode_args(n)) in post_visit()
171 euf::enode* n = var2enode(v); in is_shared()
172 euf::enode* r = n->get_root(); in is_shared()
[all …]
H A Dbv_ackerman.h30 euf::theory_var v1, v2;
33 vv():v1(euf::null_theory_var), v2(euf::null_theory_var) {} in vv()
34 vv(euf::theory_var v1, euf::theory_var v2):v1(v1), v2(v2) {} in vv()
35 …void set_var(euf::theory_var x, euf::theory_var y) { v1 = x; v2 = y; m_count = 0; m_glue = UINT_MA… in set_var()
68 void add_cc(euf::theory_var v1, euf::theory_var v2);
74 void used_eq_eh(euf::theory_var v1, euf::theory_var v2);
76 void used_diseq_eh(euf::theory_var v1, euf::theory_var v2);
H A Darray_solver.cpp77 solver::solver(euf::solver& ctx, theory_id id) : in solver()
129 for (euf::enode* p : v) in display_info()
154 euf::th_solver* solver::clone(euf::solver& dst_ctx) { in clone()
161 void solver::new_eq_eh(euf::th_eq const& eq) { in new_eq_eh()
168 euf::enode* n1 = var2enode(eq.v1()); in new_diseq_eh()
169 euf::enode* n2 = var2enode(eq.v2()); in new_diseq_eh()
187 euf::enode* n1 = var2enode(v1); in merge_eh()
188 euf::enode* n2 = var2enode(v2); in merge_eh()
197 for (euf::enode* lambda : d2.m_lambdas) in merge_eh()
213 euf::enode* child = var2enode(v_child); in add_parent_select()
[all …]
H A Dfpa_solver.h27 typedef euf::enode enode;
28 typedef euf::theory_var theory_var;
30 class solver : public euf::th_euf_solver {
51 solver(euf::solver& ctx);
55 void new_eq_eh(euf::th_eq const& eq) override;
57 void new_diseq_eh(euf::th_eq const& eq) override;
61 void apply_sort_cnstr(euf::enode* n, sort* s) override;
66 void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
67 void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
74 euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } in clone()
H A Ddt_solver.h23 namespace euf {
29 class solver : public euf::th_euf_solver {
30 typedef euf::theory_var theory_var;
31 typedef euf::theory_id theory_id;
32 typedef euf::enode enode;
33 typedef euf::enode_pair enode_pair;
34 typedef euf::enode_pair_vector enode_pair_vector;
132 solver(euf::solver& ctx, theory_id id);
144 euf::th_solver* clone(euf::solver& ctx) override;
148 void add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
[all …]
H A Dbv_solver.h23 namespace euf {
29 class solver : public euf::th_euf_solver {
31 typedef euf::theory_var theory_var;
32 typedef euf::theory_id theory_id;
36 typedef svector<euf::theory_var> vars;
116 euf::enode* m_node;
217 theory_var get_var(euf::enode* n);
218 euf::enode* get_arg(euf::enode* n, unsigned idx);
282 expr_ref eval_bv(euf::enode* n);
328 euf::th_solver* clone(euf::solver& ctx) override;
[all …]
H A Dsat_th.h25 namespace euf {
31 euf::enode_vector m_args;
82 virtual void add_dep(euf::enode* n, top_sort<euf::enode>& dep) { dep.insert(n, nullptr); } in add_dep()
106 virtual th_solver* clone(euf::solver& ctx) = 0;
108 virtual void new_eq_eh(euf::th_eq const& eq) {} in new_eq_eh()
126 euf::enode_vector m_var2enode;
155 euf::enode* e_internalize(expr* e);
172 th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id);
185 trail_stack<euf::solver>& get_trail_stack();
207 … static th_propagation* mk(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
[all …]
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Darray_solver.h23 namespace euf {
29 class solver : public euf::th_euf_solver {
30 typedef euf::theory_var theory_var;
31 typedef euf::theory_id theory_id;
75 void ensure_var(euf::enode* n);
99 euf::enode* n;
100 euf::enode* select;
240 void validate_extensionality(euf::enode* s, euf::enode* t) const;
253 euf::th_solver* clone(euf::solver& ctx) override;
260 bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
[all …]
H A Dq_eval.h22 namespace euf {
29 euf::solver& ctx;
32 euf::enode_vector m_eval;
33 euf::enode_vector m_indirect_nodes;
35 euf::enode_pair m_diseq_undef;
41 …lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& ev…
42 …lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector…
45 eval(euf::solver& ctx);
48 lbool operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence);
49 …lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evi…
[all …]
H A Darray_model.cpp29 bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { in add_dep()
34 for (euf::enode* p : euf::enode_parents(n->get_root())) { in add_dep()
45 for (euf::enode* k : euf::enode_class(n)) in add_dep()
80 for (euf::enode* p : euf::enode_parents(n->get_root())) { in add_value()
102 for (euf::enode* p : euf::enode_parents(n)) { in add_value()
137 bool operator()(euf::enode* n1, euf::enode* n2) const { in must_have_different_model_values()
160 euf::enode* p2 = nullptr; in must_have_different_model_values()
161 auto maps_diff = [&](euf::enode* p, euf::enode* else_, euf::enode* r) { in must_have_different_model_values()
164 auto table_diff = [&](euf::enode* r1, euf::enode* r2, euf::enode* else1) { in must_have_different_model_values()
166 for (euf::enode* p : euf::enode_parents(r1)) in must_have_different_model_values()
[all …]
H A Dbv_ackerman.h30 euf::theory_var v1, v2;
33 vv():v1(euf::null_theory_var), v2(euf::null_theory_var) {} in vv()
34 vv(euf::theory_var v1, euf::theory_var v2):v1(v1), v2(v2) {} in vv()
35 …void set_var(euf::theory_var x, euf::theory_var y) { v1 = x; v2 = y; m_count = 0; m_glue = UINT_MA… in set_var()
68 void add_cc(euf::theory_var v1, euf::theory_var v2);
74 void used_eq_eh(euf::theory_var v1, euf::theory_var v2);
76 void used_diseq_eh(euf::theory_var v1, euf::theory_var v2);
H A Darray_internalize.cpp39 euf::theory_var solver::mk_var(euf::enode* n) { in mk_var()
47 void solver::ensure_var(euf::enode* n) { in ensure_var()
49 if (v == euf::null_theory_var) { in ensure_var()
68 for (auto* arg : euf::enode_args(n)) { in internalize_map()
100 euf::enode* n = expr2enode(e); in visited()
109 euf::enode* n = expr2enode(e); in visit()
118 euf::enode* n = expr2enode(e); in post_visit()
125 for (auto* arg : euf::enode_args(n)) in post_visit()
172 euf::enode* n = var2enode(v); in is_shared()
173 euf::enode* r = n->get_root(); in is_shared()
[all …]
H A Dq_eval.cpp30 e.m_diseq_undef = euf::enode_pair(); in ~scoped_mark_reset()
34 eval::eval(euf::solver& ctx): in eval()
39 …lbool eval::operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vecto… in operator ()()
79 … lbool eval::operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence) { in operator ()()
84 …lbool eval::compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vect… in compare()
92 euf::enode* sr = sn ? sn->get_root() : sn; in compare()
93 euf::enode* tr = tn ? tn->get_root() : tn; in compare()
128 for (euf::enode* t1 : euf::enode_class(tn)) { in compare()
144 …lbool eval::compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_… in compare_rec()
186 …euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vect… in operator ()()
[all …]
H A Darray_solver.cpp77 solver::solver(euf::solver& ctx, theory_id id) : in solver()
116 euf::th_solver* solver::clone(euf::solver& dst_ctx) { in clone()
123 void solver::new_eq_eh(euf::th_eq const& eq) { in new_eq_eh()
130 euf::enode* n1 = var2enode(eq.v1()); in new_diseq_eh()
131 euf::enode* n2 = var2enode(eq.v2()); in new_diseq_eh()
149 euf::enode* n1 = var2enode(v1); in merge_eh()
150 euf::enode* n2 = var2enode(v2); in merge_eh()
160 for (euf::enode* lambda : d2.m_lambdas) in merge_eh()
175 euf::enode* child = var2enode(v_child); in add_parent_select()
206 for (euf::enode* lambda : d.m_lambdas) in add_parent_default()
[all …]
H A Dq_ematch.h30 namespace euf {
67 euf::solver& ctx;
91 euf::enode_pair_vector m_evidence;
93 euf::enode* const* copy_nodes(clause& c, euf::enode* const* _binding);
94 binding* tmp_binding(clause& c, app* pat, euf::enode* const* _binding);
97 sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b);
103 sat::literal instantiate(clause& c, euf::enode* const* binding, lit const& l);
106 void on_merge(euf::enode* root, euf::enode* other);
110 void add_watch(euf::enode* root, unsigned clause_idx);
132 ematch(euf::solver& ctx, solver& s);
[all …]
H A Ddt_solver.h23 namespace euf {
29 class solver : public euf::th_euf_solver {
30 typedef euf::theory_var theory_var;
31 typedef euf::theory_id theory_id;
32 typedef euf::enode enode;
33 typedef euf::enode_pair enode_pair;
34 typedef euf::enode_pair_vector enode_pair_vector;
136 solver(euf::solver& ctx, theory_id id);
148 euf::th_solver* clone(euf::solver& ctx) override;
152 bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
[all …]
H A Dfpa_solver.h27 typedef euf::enode enode;
28 typedef euf::theory_var theory_var;
30 class solver : public euf::th_euf_solver {
54 solver(euf::solver& ctx);
58 void new_eq_eh(euf::th_eq const& eq) override;
60 void new_diseq_eh(euf::th_eq const& eq) override;
64 void apply_sort_cnstr(euf::enode* n, sort* s) override;
69 void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
70 bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
77 euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } in clone()
H A Dsat_th.h25 namespace euf {
31 euf::enode_vector m_args;
82 …virtual bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) { dep.insert(n, nullptr); return tr… in add_dep()
106 virtual th_solver* clone(euf::solver& ctx) = 0;
108 virtual void new_eq_eh(euf::th_eq const& eq) {} in new_eq_eh()
126 euf::enode_vector m_var2enode;
171 th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id);
175 euf::enode* e_internalize(expr* e);
219 … static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
220 static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y);
[all …]
H A Dbv_solver.h23 namespace euf {
29 class solver : public euf::th_euf_solver {
31 typedef euf::theory_var theory_var;
32 typedef euf::theory_id theory_id;
36 typedef svector<euf::theory_var> vars;
119 euf::enode* m_node;
222 theory_var get_var(euf::enode* n);
223 euf::enode* get_arg(euf::enode* n, unsigned idx);
288 expr_ref eval_bv(euf::enode* n);
335 euf::th_solver* clone(euf::solver& ctx) override;
[all …]
H A Drecfun_solver.h25 namespace euf {
31 class solver : public euf::th_euf_solver {
68 bool is_defined(euf::enode * e) const { return is_defined(e->get_expr()); } in is_defined()
69 bool is_case_pred(euf::enode * e) const { return is_case_pred(e->get_expr()); } in is_case_pred()
92 solver(euf::solver& ctx);
102 euf::th_solver* clone(euf::solver& ctx) override;
106 bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
107 void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
108 bool is_shared(euf::theory_var v) const override { return true; } in is_shared()
H A Dq_solver.h26 namespace euf {
32 class solver : public euf::th_euf_solver {
67 solver(euf::solver& ctx, family_id fid);
78 euf::th_solver* clone(euf::solver& ctx) override;
82 euf::theory_var mk_var(euf::enode* n) override;
85 bool is_shared(euf::theory_var v) const override { return true; } in is_shared()
/dports/math/z3/z3-z3-4.8.13/src/test/
H A Degraph.cpp34 euf::egraph g(m); in test1()
40 euf::enode* na = g.mk(a, 0, 0, nullptr); in test1()
41 euf::enode* nfa = g.mk(fa, 0, 1, &na); in test1()
42 euf::enode* nffa = g.mk(ffa, 0, 1, &nfa); in test1()
55 euf::egraph g(m); in test2()
58 euf::enode_vector nodes, top_nodes; in test2()
77 for (euf::enode* n : nodes) { in test2()
83 for (euf::enode* n : top_nodes) { in test2()
94 euf::egraph g(m); in test3()
110 euf::enode* nfx = g.mk(fx, 0, 1, &nx); in test3()
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/
H A Degraph.cpp34 euf::egraph g(m); in test1()
40 euf::enode* na = g.mk(a, 0, 0, nullptr); in test1()
41 euf::enode* nfa = g.mk(fa, 0, 1, &na); in test1()
42 euf::enode* nffa = g.mk(ffa, 0, 1, &nfa); in test1()
55 euf::egraph g(m); in test2()
58 euf::enode_vector nodes, top_nodes; in test2()
77 for (euf::enode* n : nodes) { in test2()
83 for (euf::enode* n : top_nodes) { in test2()
94 euf::egraph g(m); in test3()
110 euf::enode* nfx = g.mk(fx, 0, 1, &nx); in test3()
[all …]

12345678910>>...16