| /dports/math/yices/yices-2.6.2/src/solvers/egraph/ |
| H A D | theory_explanations.c | 44 if (e->diseqs != NULL) { in delete_th_explanation()
45 safe_free(diseqv_header(e->diseqs)); in delete_th_explanation()
46 e->diseqs = NULL; in delete_th_explanation()
61 if (e->diseqs != NULL) { in reset_th_explanation()
62 diseqv_header(e->diseqs)->size = 0; in reset_th_explanation()
146 diseq_pre_expl_t *diseqs; in th_explanation_add_diseq() local
150 diseqs = e->diseqs; in th_explanation_add_diseq()
151 if (diseqs == NULL) { in th_explanation_add_diseq()
155 e->diseqs = diseqv->data; in th_explanation_add_diseq()
158 diseqv = diseqv_header(diseqs); in th_explanation_add_diseq()
[all …]
|
| H A D | egraph_printer.c | 373 diseq_pre_expl_t *diseqs; in print_theory_explanation() local
391 diseqs = e->diseqs; in print_theory_explanation()
392 if (diseqs != NULL && get_diseqv_size(diseqs) > 0) { in print_theory_explanation()
394 print_th_diseq_array(f, diseqs, get_diseqv_size(diseqs)); in print_theory_explanation()
|
| H A D | egraph_explanations.c | 855 diseq_pre_expl_t *diseqs; in explain_theory_equality() local
895 diseqs = e->diseqs; in explain_theory_equality()
896 if (diseqs != NULL) { in explain_theory_equality()
897 n = get_diseqv_size(diseqs); in explain_theory_equality()
899 cmp = diseqs[i].hint; in explain_theory_equality()
908 explain_eq(egraph, pos_occ(diseqs[i].t1), pos_occ(diseqs[i].u1), v); in explain_theory_equality()
909 explain_eq(egraph, pos_occ(diseqs[i].t2), pos_occ(diseqs[i].u2), v); in explain_theory_equality()
|
| H A D | theory_explanations.h | 129 e->diseqs = NULL; in init_th_explanation()
|
| H A D | egraph_types.h | 1091 diseq_pre_expl_t *diseqs; member
|
| /dports/math/vampire/vampire-4.5.1/Shell/ |
| H A D | DistinctGroupExpansion.cpp | 123 FormulaList* diseqs = 0; in expand() local
135 if(diseqs) FormulaList::push(new_dis,diseqs); in expand()
136 else diseqs = new FormulaList(new_dis); in expand()
142 return new JunctionFormula(Connective::AND, diseqs); in expand()
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
| H A D | diff_neq_tactic.cpp | 44 typedef svector<diseq> diseqs; typedef
45 vector<diseqs> m_var_diseqs;
87 m_var_diseqs.push_back(diseqs()); in mk_var()
190 diseqs::iterator it = m_var_diseqs[x].begin(); in display()
191 diseqs::iterator end = m_var_diseqs[x].end(); in display()
227 diseqs const & ds = m_var_diseqs[x]; in choose_value()
228 diseqs::const_iterator it = ds.begin(); in choose_value()
229 diseqs::const_iterator end = ds.end(); in choose_value()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
| H A D | diff_neq_tactic.cpp | 44 typedef svector<diseq> diseqs; typedef
45 vector<diseqs> m_var_diseqs;
87 m_var_diseqs.push_back(diseqs()); in mk_var()
190 diseqs::iterator it = m_var_diseqs[x].begin(); in display()
191 diseqs::iterator end = m_var_diseqs[x].end(); in display()
227 diseqs const & ds = m_var_diseqs[x]; in choose_value()
228 diseqs::const_iterator it = ds.begin(); in choose_value()
229 diseqs::const_iterator end = ds.end(); in choose_value()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_model_checker.cpp | 302 expr_ref_buffer diseqs(m); in add_blocking_clause() local
310 diseqs.push_back(m.mk_not(m.mk_eq(sk, sk_value))); in add_blocking_clause()
313 blocking_clause = m.mk_or(diseqs.size(), diseqs.data()); in add_blocking_clause()
|
| H A D | theory_str_mc.cpp | 869 expr_ref_vector diseqs(m); in fixed_length_reduce_diseq() local
873 diseqs.push_back(sub_m.mk_not(sub_m.mk_eq(cLHS, cRHS))); in fixed_length_reduce_diseq()
876 expr_ref final_diseq(mk_or(diseqs), sub_m); in fixed_length_reduce_diseq()
|
| H A D | theory_str.cpp | 8857 expr_ref_vector diseqs(m); in refine_eq() local
8858 diseqs.push_back(ctx.mk_eq_atom(lhs, rhs)); in refine_eq()
8869 diseqs.push_back(sublen_eq); in refine_eq()
8873 diseqs.push_back(extra_left_cond); in refine_eq()
8877 diseqs.push_back(extra_right_cond); in refine_eq()
8880 diseqs.push_back(m.mk_and(extra_deps.size(), extra_deps.data())); in refine_eq()
8881 … TRACE("str", tout << "extra_deps " << mk_pp(diseqs.get(diseqs.size()-1), m) << std::endl;); in refine_eq()
8883 expr* final_diseq = m.mk_and(diseqs.size(), diseqs.data()); in refine_eq()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_model_checker.cpp | 301 expr_ref_buffer diseqs(m); in add_blocking_clause() local
309 diseqs.push_back(m.mk_not(m.mk_eq(sk, sk_value))); in add_blocking_clause()
312 blocking_clause = m.mk_or(diseqs.size(), diseqs.c_ptr()); in add_blocking_clause()
|
| H A D | theory_str_mc.cpp | 869 expr_ref_vector diseqs(m); in fixed_length_reduce_diseq() local
873 diseqs.push_back(sub_m.mk_not(sub_m.mk_eq(cLHS, cRHS))); in fixed_length_reduce_diseq()
876 expr_ref final_diseq(mk_or(diseqs), sub_m); in fixed_length_reduce_diseq()
|
| H A D | theory_str.cpp | 9232 expr_ref_vector diseqs(m); in refine_eq() local
9233 diseqs.push_back(ctx.mk_eq_atom(lhs, rhs)); in refine_eq()
9244 diseqs.push_back(sublen_eq); in refine_eq()
9248 diseqs.push_back(extra_left_cond); in refine_eq()
9252 diseqs.push_back(extra_right_cond); in refine_eq()
9255 diseqs.push_back(m.mk_and(extra_deps.size(), extra_deps.c_ptr())); in refine_eq()
9256 … TRACE("str", tout << "extra_deps " << mk_pp(diseqs.get(diseqs.size()-1), m) << std::endl;); in refine_eq()
9258 expr* final_diseq = m.mk_and(diseqs.size(), diseqs.c_ptr()); in refine_eq()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/builtin/ |
| H A D | theory_builtin_rewriter.cpp | 43 vector<Node> diseqs; in blastDistinct() local
49 diseqs.push_back(neq); in blastDistinct()
52 Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs); in blastDistinct()
|
| /dports/math/z3/z3-z3-4.8.13/src/qe/mbp/ |
| H A D | mbp_term_graph.cpp | 1215 hashtable<pair_t, pair_t::hash, pair_t::eq> diseqs; in dcert() local
1223 diseqs.insert(pair_t(a, b)); in dcert()
1226 diseqs.insert(pair_t(e, m.mk_false())); in dcert()
1229 diseqs.insert(pair_t(ne, m.mk_true())); in dcert()
1232 for (auto& p : diseqs) todo.push_back(p); in dcert()
1243 return diseqs.contains(pair_t(a, b)); in dcert()
1273 diseqs.insert(q); in dcert()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/mbp/ |
| H A D | mbp_term_graph.cpp | 1215 hashtable<pair_t, pair_t::hash, pair_t::eq> diseqs; in dcert() local
1223 diseqs.insert(pair_t(a, b)); in dcert()
1226 diseqs.insert(pair_t(e, m.mk_false())); in dcert()
1229 diseqs.insert(pair_t(ne, m.mk_true())); in dcert()
1232 for (auto& p : diseqs) todo.push_back(p); in dcert()
1243 return diseqs.contains(pair_t(a, b)); in dcert()
1273 diseqs.insert(q); in dcert()
|
| /dports/math/vampire/vampire-4.5.1/Parse/ |
| H A D | SMTLIB2.cpp | 1800 FormulaList* diseqs = nullptr; in parseAsBuiltinFormulaSymbol() local
1805 FormulaList::push(new_dis,diseqs); in parseAsBuiltinFormulaSymbol()
1809 res = new JunctionFormula(AND, diseqs); in parseAsBuiltinFormulaSymbol()
|