From e234bede4cb0bb6db0afedc88ae504b9f3a47592 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 30 Apr 2019 17:36:12 -0700
Subject: [PATCH] fixes (#96)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_lra.cpp | 3 ++-
src/util/lp/lar_term.h | 16 ++++++++--------
src/util/lp/nla_core.cpp | 4 ++--
src/util/lp/nla_solver.cpp | 5 +++++
src/util/lp/nla_solver.h | 1 +
src/util/map.h | 10 ++++++++++
6 files changed, 28 insertions(+), 11 deletions(-)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index bf4dae9ff..99bae39bc 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1642,6 +1642,7 @@ public:
return FC_CONTINUE;
}
+ TRACE("arith", display(tout););
switch (check_lia()) {
case l_true:
break;
@@ -3574,7 +3575,7 @@ public:
for (const auto & ti : term) {
theory_var w;
if (lp().is_term(ti.var())) {
- //w = m_term_index2theory_var.get(lp().adjust_term_index(ti.var()), null_theory_var);
+ //w = m_term_index2theory_var.get(lp().adjust_term_index(ti.m_key), null_theory_var);
//if (w == null_theory_var) // if extracting expressions directly from nested term
lp::lar_term const& term1 = lp().get_term(ti.var());
rational coeff2 = coeff * ti.coeff();
diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h
index 1ed012f4b..7ce1e3f88 100644
--- a/src/util/lp/lar_term.h
+++ b/src/util/lp/lar_term.h
@@ -41,13 +41,8 @@ public:
}
}
- void add_var(unsigned j) {
- rational c(1);
- add_coeff_var(c, j);
- }
-
bool is_empty() const {
- return m_coeffs.empty();
+ return m_coeffs.empty(); // && is_zero(m_v);
}
unsigned size() const { return static_cast<unsigned>(m_coeffs.size()); }
@@ -57,7 +52,12 @@ public:
return m_coeffs;
}
- bool operator==(const lar_term & a) const { return m_coeffs == a.m_coeffs; }
+ lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
+ for (const auto & p : coeffs) {
+ add_monomial(p.first, p.second);
+ }
+ }
+ bool operator==(const lar_term & a) const { return false; } // take care not to create identical terms
bool operator!=(const lar_term & a) const { return ! (*this == a);}
// some terms get used in add constraint
// it is the same as the offset in the m_constraints
@@ -76,7 +76,7 @@ public:
if (it == nullptr) return;
const mpq & b = it->get_data().m_value;
for (unsigned it_j :li.m_index) {
- add_coeff_var(- b * li.m_data[it_j], it_j);
+ add_monomial(- b * li.m_data[it_j], it_j);
}
m_coeffs.erase(j);
}
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index 69f823ead..f7aa8801e 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -47,8 +47,8 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
rational core::value(const lp::lar_term& r) const {
rational ret(0);
- for (const auto & t : r.coeffs()) {
- ret += t.second * val(t.first);
+ for (const auto & t : r) {
+ ret += t.coeff() * val(t.var());
}
return ret;
}
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 284099c9b..9d229569a 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -45,6 +45,11 @@ void solver::push(){
void solver::pop(unsigned n) {
m_core->pop(n);
}
+
+ std::ostream& solver::display(std::ostream& out) {
+ return m_core->print_monomials(out);
+ }
+
solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) {
m_core = alloc(core, s, lim, p);
diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h
index a4bc4b911..f20561f07 100644
--- a/src/util/lp/nla_solver.h
+++ b/src/util/lp/nla_solver.h
@@ -41,5 +41,6 @@ public:
void pop(unsigned scopes);
bool need_check();
lbool check(vector<lemma>&);
+ std::ostream& display(std::ostream& out);
};
}
diff --git a/src/util/map.h b/src/util/map.h
index 72ce9219a..4ee5139e2 100644
--- a/src/util/map.h
+++ b/src/util/map.h
@@ -180,6 +180,16 @@ public:
void swap(table2map & other) {
m_table.swap(other.m_table);
}
+
+ bool operator==(table2map const& other) const {
+ if (size() != other.size()) return false;
+ for (auto const& kv : *this) {
+ auto* e = other.find_core(kv.m_key);
+ if (!e) return false;
+ if (e->get_data().m_value != kv.m_value) return false;
+ }
+ return true;
+ }
#ifdef Z3DEBUG