mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

remove var_register_dio.h

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-01-20 07:33:33 -10:00 committed by Lev Nachmanson
parent 89eec4cc80
commit abac52e1d7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/dioph_eq.cpp
View file

@ -9,7 +9,7 @@
#include "math/lp/int_solver.h" #include "math/lp/int_solver.h"
#include "math/lp/lar_solver.h" #include "math/lp/lar_solver.h"
#include "math/lp/lp_utils.h" #include "math/lp/lp_utils.h"
#include "math/lp/var_register_dio.h" #include "math/lp/var_register.h"
/* /*
Following paper: "A Practical Approach to Satisfiability Modulo Linear Following paper: "A Practical Approach to Satisfiability Modulo Linear
Integer Arithmetic" by Alberto Griggio(griggio@fbk.eu). Integer Arithmetic" by Alberto Griggio(griggio@fbk.eu).
@ -213,7 +213,7 @@ namespace lp {
entry_status m_entry_status; entry_status m_entry_status;
}; };
var_register_dio m_var_register; var_register m_var_register;
std_vector<entry> m_entries; std_vector<entry> m_entries;
// the terms are stored in m_A and m_c // the terms are stored in m_A and m_c
static_matrix<mpq, mpq> m_e_matrix; // the rows of the matrix are the terms, static_matrix<mpq, mpq> m_e_matrix; // the rows of the matrix are the terms,