mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

fix #3304

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-14 22:41:13 -07:00
parent 894702d600
commit f323da8f37
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_utvpi_def.h
View file

@ -329,6 +329,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
bool theory_utvpi<Ext>::internalize_atom(app * n, bool) { bool theory_utvpi<Ext>::internalize_atom(app * n, bool) {
context & ctx = get_context(); context & ctx = get_context();
std::cout << mk_pp(n, ctx.get_manager()) << "\n";
if (!a.is_le(n) && !a.is_ge(n) && !a.is_lt(n) && !a.is_gt(n)) { if (!a.is_le(n) && !a.is_ge(n) && !a.is_lt(n) && !a.is_gt(n)) {
found_non_utvpi_expr(n); found_non_utvpi_expr(n);
return false; return false;
@ -349,9 +350,15 @@ namespace smt {
rational w; rational w;
coeffs coeffs; coeffs coeffs;
mk_coeffs(m_test.get_linearization(), coeffs, w); mk_coeffs(m_test.get_linearization(), coeffs, w);
bool_var bv = ctx.mk_bool_var(n); bool_var bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id()); ctx.set_var_theory(bv, get_id());
literal l(bv); literal l(bv);
if (coeffs.empty()) {
throw default_exception("utvi formulas require pre-processing and dont work with quantifiers");
}
numeral w1 = mk_weight(a.is_real(e1), is_strict, w); numeral w1 = mk_weight(a.is_real(e1), is_strict, w);
edge_id pos = add_ineq(coeffs, w1, l); edge_id pos = add_ineq(coeffs, w1, l);
negate(coeffs, w); negate(coeffs, w);
@ -627,6 +634,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
edge_id theory_utvpi<Ext>::add_ineq(vector<std::pair<th_var, rational> > const& terms, numeral const& weight, literal l) { edge_id theory_utvpi<Ext>::add_ineq(vector<std::pair<th_var, rational> > const& terms, numeral const& weight, literal l) {
SASSERT(!terms.empty());
SASSERT(terms.size() <= 2); SASSERT(terms.size() <= 2);
SASSERT(terms.size() < 1 || terms[0].second.is_one() || terms[0].second.is_minus_one()); SASSERT(terms.size() < 1 || terms[0].second.is_one() || terms[0].second.is_minus_one());
SASSERT(terms.size() < 2 || terms[1].second.is_one() || terms[1].second.is_minus_one()); SASSERT(terms.size() < 2 || terms[1].second.is_one() || terms[1].second.is_minus_one());
@ -648,6 +656,7 @@ namespace smt {
// TRACE("utvpi", tout << (pos1?"$":"-$") << v1 << (pos2?" + $":" - $") << v2 << " + " << weight << " <= 0\n";); // TRACE("utvpi", tout << (pos1?"$":"-$") << v1 << (pos2?" + $":" - $") << v2 << " + " << weight << " <= 0\n";);
edge_id id = m_graph.get_num_edges(); edge_id id = m_graph.get_num_edges();
th_var w1 = to_var(v1), w2 = to_var(v2); th_var w1 = to_var(v1), w2 = to_var(v2);
if (terms.size() == 1 && pos1) { if (terms.size() == 1 && pos1) {
m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2)); m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2));
m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2)); m_graph.add_edge(neg(w1), pos(w1), -weight-weight, std::make_pair(l,2));