mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-02 08:10:14 -07:00
parent 61d887b36f
commit 4820e51c53
2 changed files with 13 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_lra.cpp
View file

@ -693,8 +693,6 @@ class theory_lra::imp {
void internalize_eq(theory_var v1, theory_var v2) { void internalize_eq(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1); enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2); enode* n2 = get_enode(v2);
expr* o1 = n1->get_owner();
expr* o2 = n2->get_owner();
app_ref term(m.mk_fresh_const("eq", a.mk_real()), m); app_ref term(m.mk_fresh_const("eq", a.mk_real()), m);
scoped_internalize_state st(*this); scoped_internalize_state st(*this);
st.vars().push_back(v1); st.vars().push_back(v1);
@ -706,8 +704,12 @@ class theory_lra::imp {
add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero())); add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero()));
add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero())); add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero()));
TRACE("arith", TRACE("arith",
{
expr* o1 = n1->get_owner();
expr* o2 = n2->get_owner();
tout << "v" << v1 << " = " << "v" << v2 << ": " tout << "v" << v1 << " = " << "v" << v2 << ": "
<< mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";); << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";
});
} }
void del_bounds(unsigned old_size) { void del_bounds(unsigned old_size) {
@ -1177,9 +1179,14 @@ public:
const lp::lar_term& term = m_solver->get_term(wi); const lp::lar_term& term = m_solver->get_term(wi);
result += term.m_v * coeff; result += term.m_v * coeff;
for (const auto & i : term.m_coeffs) { for (const auto & i : term.m_coeffs) {
if (m_variable_values.count(i.first) > 0) {
result += m_variable_values[i.first] * coeff * i.second;
}
else {
m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second)); m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second));
} }
} }
}
else { else {
result += m_variable_values[wi] * coeff; result += m_variable_values[wi] * coeff;
} }

3
src/smt/theory_seq.h
View file

@ -50,8 +50,6 @@ namespace smt {
class seq_value_proc; class seq_value_proc;
theory_seq_params const & m_params;
// cache to track evaluations under equalities // cache to track evaluations under equalities
class eval_cache { class eval_cache {
eqdep_map_t m_map; eqdep_map_t m_map;
@ -295,6 +293,7 @@ namespace smt {
typedef hashtable<rational, rational::hash_proc, rational::eq_proc> rational_set; typedef hashtable<rational, rational::hash_proc, rational::eq_proc> rational_set;
ast_manager& m; ast_manager& m;
theory_seq_params const & m_params;
dependency_manager m_dm; dependency_manager m_dm;
solution_map m_rep; // unification representative. solution_map m_rep; // unification representative.
bool m_reset_cache; // invalidate cache. bool m_reset_cache; // invalidate cache.