From 9f2bafbf10d44e5395c42666b5fbc95dbafcebc0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 Jul 2018 08:52:13 -0700
Subject: [PATCH 01/10] tidy model generator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_model_generator.cpp | 71 +++++++++++++++------------------
src/smt/smt_model_generator.h | 10 +++--
src/smt/theory_datatype.cpp | 1 +
3 files changed, 39 insertions(+), 43 deletions(-)
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 5417785d6..190f7f79e 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -28,6 +28,15 @@ Revision History:
namespace smt {
+ void fresh_value_proc::get_dependencies(buffer<model_value_dependency>& result) {
+ result.push_back(model_value_dependency(m_value));
+ }
+
+ std::ostream& operator<<(std::ostream& out, model_value_dependency const& src) {
+ if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx();
+ else return out << "#" << src.get_enode()->get_owner_id();
+ }
+
model_generator::model_generator(ast_manager & m):
m_manager(m),
m_context(nullptr),
@@ -161,20 +170,20 @@ namespace smt {
source2color & colors,
obj_hashtable<sort> & already_traversed,
svector<source> & todo) {
+
if (src.is_fresh_value()) {
- // there is an implicit dependency between a fresh value stub of sort S and the root enodes of sort S that are not associated with fresh values.
+ // there is an implicit dependency between a fresh value stub of
+ // sort S and the root enodes of sort S that are not associated with fresh values.
+ //
sort * s = src.get_value()->get_sort();
if (already_traversed.contains(s))
return true;
bool visited = true;
- unsigned sz = roots.size();
- for (unsigned i = 0; i < sz; i++) {
- enode * r = roots[i];
+ for (enode * r : roots) {
if (m_manager.get_sort(r->get_owner()) != s)
continue;
SASSERT(r == r->get_root());
- model_value_proc * proc = nullptr;
- root2proc.find(r, proc);
+ model_value_proc * proc = root2proc[r];
SASSERT(proc);
if (proc->is_fresh())
continue; // r is associated with a fresh value...
@@ -192,17 +201,12 @@ namespace smt {
enode * n = src.get_enode();
SASSERT(n == n->get_root());
bool visited = true;
- model_value_proc * proc = nullptr;
- root2proc.find(n, proc);
- SASSERT(proc);
+ model_value_proc * proc = root2proc[n];
buffer<model_value_dependency> dependencies;
proc->get_dependencies(dependencies);
for (model_value_dependency const& dep : dependencies) {
visit_child(dep, colors, todo, visited);
- TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> ";
- if (dep.is_fresh_value()) tout << "fresh!" << dep.get_value()->get_idx();
- else tout << "#" << dep.get_enode()->get_owner_id();
- tout << "\n";);
+ TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> " << dep << " already visited: " << visited << "\n";);
}
return visited;
}
@@ -215,9 +219,7 @@ namespace smt {
svector<source> & todo,
svector<source> & sorted_sources) {
TRACE("mg_top_sort", tout << "process source, is_fresh: " << src.is_fresh_value() << " ";
- if (src.is_fresh_value()) tout << "fresh!" << src.get_value()->get_idx();
- else tout << "#" << src.get_enode()->get_owner_id();
- tout << ", todo.size(): " << todo.size() << "\n";);
+ tout << src << ", todo.size(): " << todo.size() << "\n";);
int color = get_color(colors, src);
SASSERT(color != Grey);
if (color == Black)
@@ -227,17 +229,16 @@ namespace smt {
while (!todo.empty()) {
source curr = todo.back();
TRACE("mg_top_sort", tout << "current source, is_fresh: " << curr.is_fresh_value() << " ";
- if (curr.is_fresh_value()) tout << "fresh!" << curr.get_value()->get_idx();
- else tout << "#" << curr.get_enode()->get_owner_id();
- tout << ", todo.size(): " << todo.size() << "\n";);
+ tout << curr << ", todo.size(): " << todo.size() << "\n";);
switch (get_color(colors, curr)) {
case White:
set_color(colors, curr, Grey);
visit_children(curr, roots, root2proc, colors, already_traversed, todo);
break;
case Grey:
- SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo));
+ // SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo));
set_color(colors, curr, Black);
+ TRACE("mg_top_sort", tout << "append " << curr << "\n";);
sorted_sources.push_back(curr);
break;
case Black:
@@ -266,18 +267,15 @@ namespace smt {
// topological sort
// traverse all extra fresh values...
- unsigned sz = m_extra_fresh_values.size();
- for (unsigned i = 0; i < sz; i++) {
- extra_fresh_value * f = m_extra_fresh_values[i];
+ for (extra_fresh_value * f : m_extra_fresh_values) {
process_source(source(f), roots, root2proc, colors, already_traversed, todo, sorted_sources);
}
// traverse all enodes that are associated with fresh values...
- sz = roots.size();
+ unsigned sz = roots.size();
for (unsigned i = 0; i < sz; i++) {
enode * r = roots[i];
- model_value_proc * proc = nullptr;
- root2proc.find(r, proc);
+ model_value_proc * proc = root2proc[r];
SASSERT(proc);
if (!proc->is_fresh())
continue;
@@ -303,43 +301,38 @@ namespace smt {
TRACE("sorted_sources",
for (source const& curr : sources) {
if (curr.is_fresh_value()) {
- tout << "fresh!" << curr.get_value()->get_idx() << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
+ tout << curr << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
}
else {
enode * n = curr.get_enode();
SASSERT(n->get_root() == n);
sort * s = m_manager.get_sort(n->get_owner());
- tout << "#" << n->get_owner_id() << " " << mk_pp(s, m_manager);
- model_value_proc * proc = 0;
- root2proc.find(n, proc);
- SASSERT(proc);
- tout << " is_fresh: " << proc->is_fresh() << "\n";
+ tout << curr << " " << mk_pp(s, m_manager);
+ tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
}
});
for (source const& curr : sources) {
if (curr.is_fresh_value()) {
sort * s = curr.get_value()->get_sort();
- TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " : " << mk_pp(s, m_manager) << "\n";);
+ TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m_manager) << "\n";);
expr * val = m_model->get_fresh_value(s);
- TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " := #" << (val == 0 ? UINT_MAX : val->get_id()) << "\n";);
+ TRACE("model_fresh_bug", tout << curr << " := #" << (val == nullptr ? UINT_MAX : val->get_id()) << "\n";);
m_asts.push_back(val);
curr.get_value()->set_value(val);
}
else {
enode * n = curr.get_enode();
SASSERT(n->get_root() == n);
- TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << "\n";);
+ TRACE("mg_top_sort", tout << curr << "\n";);
dependencies.reset();
dependency_values.reset();
- model_value_proc * proc = nullptr;
- VERIFY(root2proc.find(n, proc));
+ model_value_proc * proc = root2proc[n];
SASSERT(proc);
proc->get_dependencies(dependencies);
for (model_value_dependency const& d : dependencies) {
if (d.is_fresh_value()) {
CTRACE("mg_top_sort", !d.get_value()->get_value(),
- tout << "#" << n->get_owner_id() << " -> ";
- tout << "fresh!" << d.get_value()->get_idx() << "\n";);
+ tout << "#" << n->get_owner_id() << " -> " << d << "\n";);
SASSERT(d.get_value()->get_value());
dependency_values.push_back(d.get_value()->get_value());
}
diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h
index 7466b8877..1f69eb324 100644
--- a/src/smt/smt_model_generator.h
+++ b/src/smt/smt_model_generator.h
@@ -100,14 +100,16 @@ namespace smt {
extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value
};
public:
- model_value_dependency():m_fresh(true), m_value(nullptr) {}
- model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {}
- model_value_dependency(extra_fresh_value * v):m_fresh(true), m_value(v) {}
+ model_value_dependency():m_fresh(true), m_value(nullptr) { }
+ explicit model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {}
+ explicit model_value_dependency(extra_fresh_value * v) :m_fresh(true), m_value(v) { SASSERT(v); }
bool is_fresh_value() const { return m_fresh; }
enode * get_enode() const { SASSERT(!is_fresh_value()); return m_enode; }
extra_fresh_value * get_value() const { SASSERT(is_fresh_value()); return m_value; }
};
+ std::ostream& operator<<(std::ostream& out, model_value_dependency const& d);
+
typedef model_value_dependency source;
struct source_hash_proc {
@@ -166,7 +168,7 @@ namespace smt {
extra_fresh_value * m_value;
public:
fresh_value_proc(extra_fresh_value * v):m_value(v) {}
- void get_dependencies(buffer<model_value_dependency> & result) override { result.push_back(m_value); }
+ void get_dependencies(buffer<model_value_dependency> & result) override;
app * mk_value(model_generator & m, ptr_vector<expr> & values) override { return to_app(values[0]); }
bool is_fresh() const override { return true; }
};
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 049555297..c3befced6 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -636,6 +636,7 @@ namespace smt {
void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); }
~datatype_value_proc() override {}
void get_dependencies(buffer<model_value_dependency> & result) override {
+ for (model_value_dependency& d : m_dependencies) { }
result.append(m_dependencies.size(), m_dependencies.c_ptr());
}
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
From 3a5aebd1d32c8cd889b582dde4277a3e0fb11d67 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 Jul 2018 08:52:57 -0700
Subject: [PATCH 02/10] tidy model generator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_datatype.cpp | 1 -
1 file changed, 1 deletion(-)
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index c3befced6..049555297 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -636,7 +636,6 @@ namespace smt {
void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); }
~datatype_value_proc() override {}
void get_dependencies(buffer<model_value_dependency> & result) override {
- for (model_value_dependency& d : m_dependencies) { }
result.append(m_dependencies.size(), m_dependencies.c_ptr());
}
app * mk_value(model_generator & mg, ptr_vector<expr> & values) override {
From 167969d6c2148b274749eaa98967862912e59d61 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Jul 2018 07:52:36 -0700
Subject: [PATCH 03/10] remove debug/non-debug difference
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_lra.cpp | 2 --
src/util/lp/hnf_cutter.h | 28 +++++++++++++---------------
src/util/lp/int_solver.cpp | 26 ++++++++++++++++++--------
3 files changed, 31 insertions(+), 25 deletions(-)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3bdd2d784..ff5b72159 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2712,7 +2712,6 @@ public:
if (dump_lemmas()) {
unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
(void)id;
- //SASSERT(id != 55);
}
}
@@ -2732,7 +2731,6 @@ public:
if (dump_lemmas()) {
unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
(void)id;
- // SASSERT(id != 71);
}
}
diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h
index dff0b8ef8..9a06e1bc9 100644
--- a/src/util/lp/hnf_cutter.h
+++ b/src/util/lp/hnf_cutter.h
@@ -177,43 +177,41 @@ public:
bool overflow() const { return m_overflow; }
- lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper
- #ifdef Z3DEBUG
- ,
- const vector<mpq> & x0
- #endif
- ) {
+ lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper, const vector<mpq> & x0) {
// we suppose that x0 has at least one non integer element
+ (void)x0;
+
init_matrix_A();
svector<unsigned> basis_rows;
mpq big_number = m_abs_max.expt(3);
mpq d = hnf_calc::determinant_of_rectangular_matrix(m_A, basis_rows, big_number);
- // std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
- //std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
+ // std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
+ // std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
if (d >= big_number) {
return lia_move::undef;
}
- if (m_settings.get_cancel_flag())
+ if (m_settings.get_cancel_flag()) {
return lia_move::undef;
+ }
+
if (basis_rows.size() < m_A.row_count()) {
m_A.shrink_to_rank(basis_rows);
shrink_explanation(basis_rows);
}
- hnf<general_matrix> h(m_A, d);
- // general_matrix A_orig = m_A;
-
+ hnf<general_matrix> h(m_A, d);
vector<mpq> b = create_b(basis_rows);
lp_assert(m_A * x0 == b);
- // vector<mpq> bcopy = b;
find_h_minus_1_b(h.W(), b);
- // lp_assert(bcopy == h.W().take_first_n_columns(b.size()) * b);
int cut_row = find_cut_row_index(b);
- if (cut_row == -1)
+
+ if (cut_row == -1) {
return lia_move::undef;
+ }
+
// the matrix is not square - we can get
// all integers in b's projection
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index f49ecabfd..8bc2056b4 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -577,17 +577,27 @@ lia_move int_solver::make_hnf_cut() {
return lia_move::undef;
}
settings().st().m_hnf_cutter_calls++;
- TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls;);
+ TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls << "\n";
+ for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
+ m_lar_solver->print_constraint(i, tout);
+ }
+ m_lar_solver->print_constraints(tout);
+ );
#ifdef Z3DEBUG
vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x);
+#else
+ vector<mpq> x0;
#endif
- lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper
-#ifdef Z3DEBUG
- , x0
-#endif
- );
- CTRACE("hnf_cut", r == lia_move::cut, tout<< "cut:"; m_lar_solver->print_term(*m_t, tout); tout << " <= " << *m_k << std::endl;);
- if (r == lia_move::cut) {
+ lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0);
+
+ if (r == lia_move::cut) {
+ TRACE("hnf_cut",
+ m_lar_solver->print_term(*m_t, tout << "cut:");
+ tout << " <= " << *m_k << std::endl;
+ for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
+ m_lar_solver->print_constraint(i, tout);
+ }
+ );
lp_assert(current_solution_is_inf_on_cut());
settings().st().m_hnf_cuts++;
m_ex->clear();
From 774fa33bfe050bc8f035290b794d7f838114bc2d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Jul 2018 08:49:46 -0700
Subject: [PATCH 04/10] fix parameter lookup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/seq_decl_plugin.cpp | 15 ++++++++-------
1 file changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 00ba93ccb..07c6fd06a 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -363,12 +363,12 @@ bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) {
bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
if (s == sP) return true;
- unsigned i;
- if (is_sort_param(sP, i)) {
- if (binding.size() <= i) binding.resize(i+1);
- if (binding[i] && (binding[i] != s)) return false;
- TRACE("seq_verbose", tout << "setting binding @ " << i << " to " << mk_pp(s, *m_manager) << "\n";);
- binding[i] = s;
+ unsigned idx;
+ if (is_sort_param(sP, idx)) {
+ if (binding.size() <= idx) binding.resize(idx+1);
+ if (binding[idx] && (binding[idx] != s)) return false;
+ TRACE("seq_verbose", tout << "setting binding @ " << idx << " to " << mk_pp(s, *m_manager) << "\n";);
+ binding[idx] = s;
return true;
}
@@ -376,7 +376,8 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
if (s->get_family_id() == sP->get_family_id() &&
s->get_decl_kind() == sP->get_decl_kind() &&
s->get_num_parameters() == sP->get_num_parameters()) {
- for (parameter const& p : s->parameters()) {
+ for (unsigned i = 0, sz = s->get_num_parameters(); i < sz; ++i) {
+ parameter const& p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast())) {
parameter const& p2 = sP->get_parameter(i);
if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;
From 88f4ce68fd46b2200c9d75d568eded5accc4c27f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Jul 2018 13:51:07 -0700
Subject: [PATCH 05/10] fix model generation regression exposed in nightly
builds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_lra.cpp | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ff5b72159..9c054830c 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1118,7 +1118,7 @@ public:
(v != null_theory_var) &&
(v < static_cast<theory_var>(m_theory_var2var_index.size())) &&
(UINT_MAX != m_theory_var2var_index[v]) &&
- !m_variable_values.empty();
+ (!m_variable_values.empty() || m_solver->is_term(m_theory_var2var_index[v]));
}
bool can_get_bound(theory_var v) const {
@@ -1163,13 +1163,19 @@ public:
}
rational get_value(theory_var v) const {
- if (!can_get_value(v)) return rational::zero();
+
+ if (v == null_theory_var ||
+ v >= static_cast<theory_var>(m_theory_var2var_index.size()))
+ return rational::zero();
+
lp::var_index vi = m_theory_var2var_index[v];
if (m_variable_values.count(vi) > 0)
return m_variable_values[vi];
- if(!m_solver->is_term(vi))
+ if (!m_solver->is_term(vi)) {
+ TRACE("arith", tout << "not a term v" << v << "\n";);
return rational::zero();
+ }
m_todo_terms.push_back(std::make_pair(vi, rational::one()));
rational result(0);
From bdd8685146c91a159c5cb336d8dc439787eb49b7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 13 Jul 2018 18:09:30 -0700
Subject: [PATCH 06/10] use params for arguments to Fixedpoint methods
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/dotnet/Fixedpoint.cs | 4 ++--
src/smt/theory_lra.cpp | 8 ++++++--
2 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index e2fb7fe5a..102a96ac5 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -146,7 +146,7 @@ namespace Microsoft.Z3
/// The query is satisfiable if there is an instance of some relation that is non-empty.
/// The query is unsatisfiable if there are no derivations satisfying any of the relations.
/// </summary>
- public Status Query(FuncDecl[] relations)
+ public Status Query(params FuncDecl[] relations)
{
Contract.Requires(relations != null);
Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
@@ -262,7 +262,7 @@ namespace Microsoft.Z3
/// <summary>
/// Convert benchmark given as set of axioms, rules and queries to a string.
/// </summary>
- public string ToString(BoolExpr[] queries)
+ public string ToString(params BoolExpr[] queries)
{
return Native.Z3_fixedpoint_to_string(Context.nCtx, NativeObject,
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 9c054830c..ef1cd5f0a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1163,10 +1163,12 @@ public:
}
rational get_value(theory_var v) const {
-
+
if (v == null_theory_var ||
- v >= static_cast<theory_var>(m_theory_var2var_index.size()))
+ v >= static_cast<theory_var>(m_theory_var2var_index.size())) {
+ TRACE("arith", tout << "Variable v" << v << " not internalized\n";);
return rational::zero();
+ }
lp::var_index vi = m_theory_var2var_index[v];
if (m_variable_values.count(vi) > 0)
@@ -1207,6 +1209,7 @@ public:
if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
reset_variable_values();
m_solver->get_model(m_variable_values);
+ TRACE("arith", display(tout););
}
}
@@ -2642,6 +2645,7 @@ public:
}
else {
rational r = get_value(v);
+ TRACE("arith", tout << "v" << v << " := " << r << "\n";);
if (a.is_int(o) && !r.is_int()) r = floor(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
}
From 7d20fbb28094f27e399d4d8cbc47bcee93f572f0 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sat, 14 Jul 2018 12:21:43 +0100
Subject: [PATCH 07/10] do not cooperate if OMP mode is disabled (i.e. it's
single threaded only)
---
src/util/cooperate.cpp | 31 ++++---------------------------
src/util/cooperate.h | 19 ++++---------------
src/util/mpq.h | 3 ---
3 files changed, 8 insertions(+), 45 deletions(-)
diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp
index 2b2e7958e..df8f67968 100644
--- a/src/util/cooperate.cpp
+++ b/src/util/cooperate.cpp
@@ -16,6 +16,8 @@ Author:
Notes:
--*/
+
+#ifndef _NO_OMP_
#include "util/cooperate.h"
#include "util/trace.h"
#include "util/debug.h"
@@ -36,7 +38,7 @@ struct cooperation_lock {
}
};
-cooperation_lock g_lock;
+static cooperation_lock g_lock;
bool cooperation_ctx::g_cooperate = false;
@@ -59,29 +61,4 @@ void cooperation_ctx::checkpoint(char const * task) {
}
}
-cooperation_section::cooperation_section() {
- SASSERT(!cooperation_ctx::enabled());
- SASSERT(!omp_in_parallel());
- cooperation_ctx::g_cooperate = true;
-}
-
-cooperation_section::~cooperation_section() {
- SASSERT(cooperation_ctx::enabled());
- cooperation_ctx::g_cooperate = false;
-}
-
-init_task::init_task(char const * task) {
- SASSERT(cooperation_ctx::enabled());
- SASSERT(omp_in_parallel());
- cooperation_ctx::checkpoint(task);
-}
-
-init_task::~init_task() {
- int tid = omp_get_thread_num();
- if (g_lock.m_owner_thread == tid) {
- g_lock.m_owner_thread = -1;
- omp_unset_nest_lock(&(g_lock.m_lock));
- }
-}
-
-
+#endif
diff --git a/src/util/cooperate.h b/src/util/cooperate.h
index af2cff55c..6220c4c51 100644
--- a/src/util/cooperate.h
+++ b/src/util/cooperate.h
@@ -19,10 +19,9 @@ Notes:
#ifndef COOPERATE_H_
#define COOPERATE_H_
-class cooperation_section;
+#ifndef _NO_OMP_
class cooperation_ctx {
- friend class cooperation_section;
static bool g_cooperate;
public:
static bool enabled() { return g_cooperate; }
@@ -33,18 +32,8 @@ inline void cooperate(char const * task) {
if (cooperation_ctx::enabled()) cooperation_ctx::checkpoint(task);
}
-// must be declared before "#pragma parallel" to enable cooperation
-class cooperation_section {
-public:
- cooperation_section();
- ~cooperation_section();
-};
-
-// must be first declaration inside "#pragma parallel for"
-class init_task {
-public:
- init_task(char const * task);
- ~init_task();
-};
+#else
+inline void cooperate(char const *) {}
+#endif
#endif
diff --git a/src/util/mpq.h b/src/util/mpq.h
index b7bdbf400..77301371d 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -814,9 +814,6 @@ public:
bool is_even(mpz const & a) { return mpz_manager<SYNCH>::is_even(a); }
public:
bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
-
- friend bool operator==(mpq const & a, mpq const & b) ;
- friend bool operator>=(mpq const & a, mpq const & b);
};
typedef mpq_manager<true> synch_mpq_manager;
From b88596283ff4484a835601b49bee8599943fb179 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sat, 14 Jul 2018 20:44:35 +0100
Subject: [PATCH 08/10] don't use mp[zq] synchronized mode if OpenMP mode is
disabled
---
src/util/mpff.cpp | 10 ++++++++++
src/util/mpff.h | 19 ++++++++++++++++---
src/util/mpfx.cpp | 8 ++++++++
src/util/mpfx.h | 15 +++++++++++++--
src/util/mpq.cpp | 30 ++++++++++++++----------------
src/util/mpq.h | 44 ++++++++++++++++++++++++--------------------
src/util/mpq_inf.cpp | 2 ++
src/util/mpq_inf.h | 4 ++++
src/util/mpz.cpp | 2 ++
src/util/mpz.h | 4 ++++
10 files changed, 97 insertions(+), 41 deletions(-)
diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp
index e00a25b1b..8ca2e983f 100644
--- a/src/util/mpff.cpp
+++ b/src/util/mpff.cpp
@@ -376,9 +376,11 @@ void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
+#ifndef _NO_OMP_
void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
+#endif
template<bool SYNCH>
void mpff_manager::set_core(mpff & n, mpq_manager<SYNCH> & m, mpq const & v) {
@@ -397,9 +399,11 @@ void mpff_manager::set(mpff & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
+#ifndef _NO_OMP_
void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
+#endif
bool mpff_manager::eq(mpff const & a, mpff const & b) const {
if (is_zero(a) && is_zero(b))
@@ -1077,9 +1081,11 @@ void mpff_manager::significand(mpff const & n, unsynch_mpz_manager & m, mpz & t)
significand_core(n, m, t);
}
+#ifndef _NO_OMP_
void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) {
significand_core(n, m, t);
}
+#endif
template<bool SYNCH>
void mpff_manager::to_mpz_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & t) {
@@ -1109,9 +1115,11 @@ void mpff_manager::to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
+#ifndef _NO_OMP_
void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
+#endif
template<bool SYNCH>
void mpff_manager::to_mpq_core(mpff const & n, mpq_manager<SYNCH> & m, mpq & t) {
@@ -1154,9 +1162,11 @@ void mpff_manager::to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
+#ifndef _NO_OMP_
void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
+#endif
void mpff_manager::display_raw(std::ostream & out, mpff const & n) const {
if (is_neg(n))
diff --git a/src/util/mpff.h b/src/util/mpff.h
index 8023053d2..6f1e9d23c 100644
--- a/src/util/mpff.h
+++ b/src/util/mpff.h
@@ -58,9 +58,14 @@ class mpz;
class mpq;
template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager;
+#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager;
-typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager;
+#else
+typedef mpz_manager<false> synch_mpz_manager;
+typedef mpq_manager<false> synch_mpq_manager;
+#endif
+typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<false> unsynch_mpq_manager;
class mpff_manager {
@@ -213,7 +218,9 @@ public:
\brief Return the significand as a mpz numeral.
*/
void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r);
+#ifndef _NO_OMP_
void significand(mpff const & n, synch_mpz_manager & m, mpz & r);
+#endif
/**
\brief Return true if n is negative
@@ -378,9 +385,11 @@ public:
void set(mpff & n, int64_t num, uint64_t den);
void set(mpff & n, mpff const & v);
void set(mpff & n, unsynch_mpz_manager & m, mpz const & v);
- void set(mpff & n, synch_mpz_manager & m, mpz const & v);
void set(mpff & n, unsynch_mpq_manager & m, mpq const & v);
+#ifndef _NO_OMP_
void set(mpff & n, synch_mpq_manager & m, mpq const & v);
+ void set(mpff & n, synch_mpz_manager & m, mpz const & v);
+#endif
void set_plus_epsilon(mpff & n);
void set_minus_epsilon(mpff & n);
void set_max(mpff & n);
@@ -420,6 +429,7 @@ public:
*/
void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t);
+#ifndef _NO_OMP_
/**
\brief Convert n into a mpz numeral.
@@ -428,6 +438,7 @@ public:
\remark if exponent(n) is too big, we may run out of memory.
*/
void to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t);
+#endif
/**
\brief Convert n into a mpq numeral.
@@ -436,13 +447,15 @@ public:
*/
void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t);
+#ifndef _NO_OMP_
/**
\brief Convert n into a mpq numeral.
\remark if exponent(n) is too big, we may run out of memory.
*/
void to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t);
-
+#endif
+
/**
\brief Return n as an int64.
diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp
index 2ebc54840..8ed16ec68 100644
--- a/src/util/mpfx.cpp
+++ b/src/util/mpfx.cpp
@@ -272,9 +272,11 @@ void mpfx_manager::set(mpfx & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
+#ifndef _NO_OMP_
void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v);
}
+#endif
template<bool SYNCH>
void mpfx_manager::set_core(mpfx & n, mpq_manager<SYNCH> & m, mpq const & v) {
@@ -309,9 +311,11 @@ void mpfx_manager::set(mpfx & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
+#ifndef _NO_OMP_
void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v);
}
+#endif
bool mpfx_manager::eq(mpfx const & a, mpfx const & b) const {
if (is_zero(a) && is_zero(b))
@@ -714,9 +718,11 @@ void mpfx_manager::to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
+#ifndef _NO_OMP_
void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t);
}
+#endif
template<bool SYNCH>
void mpfx_manager::to_mpq_core(mpfx const & n, mpq_manager<SYNCH> & m, mpq & t) {
@@ -738,9 +744,11 @@ void mpfx_manager::to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
+#ifndef _NO_OMP_
void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t);
}
+#endif
void mpfx_manager::display_raw(std::ostream & out, mpfx const & n) const {
if (is_neg(n))
diff --git a/src/util/mpfx.h b/src/util/mpfx.h
index a8e93f0b0..6de3f251b 100644
--- a/src/util/mpfx.h
+++ b/src/util/mpfx.h
@@ -51,9 +51,14 @@ class mpz;
class mpq;
template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager;
+#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager;
-typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager;
+#else
+typedef mpz_manager<false> synch_mpz_manager;
+typedef mpq_manager<false> synch_mpq_manager;
+#endif
+typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<false> unsynch_mpq_manager;
class mpfx_manager {
@@ -312,9 +317,11 @@ public:
void set(mpfx & n, int64_t num, uint64_t den);
void set(mpfx & n, mpfx const & v);
void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v);
- void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v);
+#ifndef _NO_OMP_
+ void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
void set(mpfx & n, synch_mpq_manager & m, mpq const & v);
+#endif
/**
\brief Set n to the smallest representable numeral greater than zero.
@@ -359,22 +366,26 @@ public:
*/
void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t);
+#ifndef _NO_OMP_
/**
\brief Convert n into a mpz numeral.
\pre is_int(n)
*/
void to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t);
+#endif
/**
\brief Convert n into a mpq numeral.
*/
void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t);
+#ifndef _NO_OMP_
/**
\brief Convert n into a mpq numeral.
*/
void to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t);
+#endif
/**
\brief Return the biggest k s.t. 2^k <= a.
diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp
index 30ac0f410..207614ee0 100644
--- a/src/util/mpq.cpp
+++ b/src/util/mpq.cpp
@@ -26,12 +26,12 @@ mpq_manager<SYNCH>::mpq_manager() {
template<bool SYNCH>
mpq_manager<SYNCH>::~mpq_manager() {
- del(m_n_tmp);
- del(m_add_tmp1);
- del(m_add_tmp2);
- del(m_lt_tmp1);
- del(m_lt_tmp2);
- del(m_addmul_tmp);
+ del(m_tmp1);
+ del(m_tmp2);
+ del(m_tmp3);
+ del(m_tmp4);
+ del(m_q_tmp1);
+ del(m_q_tmp2);
}
@@ -68,9 +68,9 @@ bool mpq_manager<SYNCH>::rat_lt(mpq const & a, mpq const & b) {
return r;
}
else {
- mul(na, db, m_lt_tmp1);
- mul(nb, da, m_lt_tmp2);
- return lt(m_lt_tmp1, m_lt_tmp2);
+ mul(na, db, m_q_tmp1);
+ mul(nb, da, m_q_tmp2);
+ return lt(m_q_tmp1, m_q_tmp2);
}
}
@@ -384,8 +384,7 @@ void mpq_manager<SYNCH>::rat_mul(mpq const & a, mpq const & b, mpq & c) {
del(tmp2);
}
else {
- mpz& g1 = m_n_tmp, &g2 = m_addmul_tmp.m_num, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2;
- rat_mul(a, b, c, g1, g2, tmp1, tmp2);
+ rat_mul(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
}
STRACE("rat_mpq", tout << to_string(c) << "\n";);
}
@@ -402,8 +401,7 @@ void mpq_manager<SYNCH>::rat_add(mpq const & a, mpq const & b, mpq & c) {
del(g);
}
else {
- mpz& g = m_n_tmp, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2, &tmp3 = m_addmul_tmp.m_num;
- lin_arith_op<false>(a, b, c, g, tmp1, tmp2, tmp3);
+ lin_arith_op<false>(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
}
STRACE("rat_mpq", tout << to_string(c) << "\n";);
}
@@ -420,13 +418,13 @@ void mpq_manager<SYNCH>::rat_sub(mpq const & a, mpq const & b, mpq & c) {
del(g);
}
else {
- mpz& g = m_n_tmp, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2, &tmp3 = m_addmul_tmp.m_num;
- lin_arith_op<true>(a, b, c, g, tmp1, tmp2, tmp3);
+ lin_arith_op<true>(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
}
STRACE("rat_mpq", tout << to_string(c) << "\n";);
}
+#ifndef _NO_OMP_
template class mpq_manager<true>;
+#endif
template class mpq_manager<false>;
-
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 77301371d..20802f786 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -41,12 +41,12 @@ inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
template<bool SYNCH = true>
class mpq_manager : public mpz_manager<SYNCH> {
- mpz m_n_tmp;
- mpz m_add_tmp1;
- mpz m_add_tmp2;
- mpq m_addmul_tmp;
- mpq m_lt_tmp1;
- mpq m_lt_tmp2;
+ mpz m_tmp1;
+ mpz m_tmp2;
+ mpz m_tmp3;
+ mpz m_tmp4;
+ mpq m_q_tmp1;
+ mpq m_q_tmp2;
void reset_denominator(mpq & a) {
del(a.m_den);
@@ -66,11 +66,11 @@ class mpq_manager : public mpz_manager<SYNCH> {
del(tmp);
}
else {
- gcd(a.m_num, a.m_den, m_n_tmp);
- if (is_one(m_n_tmp))
+ gcd(a.m_num, a.m_den, m_tmp1);
+ if (is_one(m_tmp1))
return;
- div(a.m_num, m_n_tmp, a.m_num);
- div(a.m_den, m_n_tmp, a.m_den);
+ div(a.m_num, m_tmp1, a.m_num);
+ div(a.m_den, m_tmp1, a.m_den);
}
}
@@ -87,9 +87,9 @@ class mpq_manager : public mpz_manager<SYNCH> {
del(tmp1);
}
else {
- mul(b, a.m_den, m_add_tmp1);
+ mul(b, a.m_den, m_tmp1);
set(c.m_den, a.m_den);
- add(a.m_num, m_add_tmp1, c.m_num);
+ add(a.m_num, m_tmp1, c.m_num);
normalize(c);
}
STRACE("rat_mpq", tout << to_string(c) << "\n";);
@@ -320,8 +320,8 @@ public:
del(tmp);
}
else {
- mul(b,c,m_addmul_tmp);
- add(a, m_addmul_tmp, d);
+ mul(b, c, m_q_tmp1);
+ add(a, m_q_tmp1, d);
}
}
}
@@ -342,8 +342,8 @@ public:
del(tmp);
}
else {
- mul(b,c,m_addmul_tmp);
- add(a, m_addmul_tmp, d);
+ mul(b,c, m_q_tmp1);
+ add(a, m_q_tmp1, d);
}
}
}
@@ -365,8 +365,8 @@ public:
del(tmp);
}
else {
- mul(b,c,m_addmul_tmp);
- sub(a, m_addmul_tmp, d);
+ mul(b,c, m_q_tmp1);
+ sub(a, m_q_tmp1, d);
}
}
}
@@ -387,8 +387,8 @@ public:
del(tmp);
}
else {
- mul(b,c,m_addmul_tmp);
- sub(a, m_addmul_tmp, d);
+ mul(b,c, m_q_tmp1);
+ sub(a, m_q_tmp1, d);
}
}
}
@@ -816,7 +816,11 @@ public:
bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
};
+#ifndef _NO_OMP_
typedef mpq_manager<true> synch_mpq_manager;
+#else
+typedef mpq_manager<false> synch_mpq_manager;
+#endif
typedef mpq_manager<false> unsynch_mpq_manager;
typedef _scoped_numeral<unsynch_mpq_manager> scoped_mpq;
diff --git a/src/util/mpq_inf.cpp b/src/util/mpq_inf.cpp
index c6c160941..69de425cf 100644
--- a/src/util/mpq_inf.cpp
+++ b/src/util/mpq_inf.cpp
@@ -39,5 +39,7 @@ std::string mpq_inf_manager<SYNCH>::to_string(mpq_inf const & a) {
}
+#ifndef _NO_OMP_
template class mpq_inf_manager<true>;
+#endif
template class mpq_inf_manager<false>;
diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h
index 7b866994d..c7bd261e6 100644
--- a/src/util/mpq_inf.h
+++ b/src/util/mpq_inf.h
@@ -279,7 +279,11 @@ public:
mpq_manager<SYNCH>& get_mpq_manager() { return m; }
};
+#ifndef _NO_OMP_
typedef mpq_inf_manager<true> synch_mpq_inf_manager;
+#else
+typedef mpq_inf_manager<false> synch_mpq_inf_manager;
+#endif
typedef mpq_inf_manager<false> unsynch_mpq_inf_manager;
#endif
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 7ad4797b7..32a074eb3 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -2369,5 +2369,7 @@ bool mpz_manager<SYNCH>::divides(mpz const & a, mpz const & b) {
return r;
}
+#ifndef _NO_OMP_
template class mpz_manager<true>;
+#endif
template class mpz_manager<false>;
diff --git a/src/util/mpz.h b/src/util/mpz.h
index f480b097e..187532a87 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -692,7 +692,11 @@ public:
bool decompose(mpz const & n, svector<digit_t> & digits);
};
+#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager;
+#else
+typedef mpz_manager<false> synch_mpz_manager;
+#endif
typedef mpz_manager<false> unsynch_mpz_manager;
typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz;
From dfa8c4432fed9e1c47b32681c3fcda0389b58ae2 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sat, 14 Jul 2018 20:50:49 +0100
Subject: [PATCH 09/10] add parameter(rational&&)
---
src/ast/ast.h | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 364be8a77..89df04961 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -122,6 +122,7 @@ public:
explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {}
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s.c_ptr()) {}
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {}
+ explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {}
explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s).c_ptr()) {}
explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
From f7ac0966965781eda14e468bfba672c9f741490f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sun, 15 Jul 2018 15:29:13 -0700
Subject: [PATCH 10/10] avoid a vector copy
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/util/lp/lar_solver.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 72705dfb3..3735fbb9f 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -112,7 +112,7 @@ private:
public :
unsigned terms_start_index() const { return m_terms_start_index; }
- const vector<lar_term*> terms() const { return m_terms; }
+ const vector<lar_term*> & terms() const { return m_terms; }
const vector<lar_base_constraint*>& constraints() const {
return m_constraints;
}