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

perf in equiv_monomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-01-25 11:37:48 -08:00
parent 5104ec881a
commit 1230b46008
3 changed files with 15 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -122,7 +122,6 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
or_else(mk_qfnia_sat_solver(m, p), or_else(mk_qfnia_sat_solver(m, p),
try_for(mk_qfnia_smt_solver(m, p), 2000), try_for(mk_qfnia_smt_solver(m, p), 2000),
mk_qfnia_nlsat_solver(m, p), mk_qfnia_nlsat_solver(m, p),
mk_qfnia_smt_solver(m, p)) mk_qfnia_smt_solver(m, p))<
) );
;
} }

8
src/util/debug.h
View file

@ -38,11 +38,11 @@ bool assertions_enabled();
#include "util/error_codes.h" #include "util/error_codes.h"
#include "util/warning.h" #include "util/warning.h"
#ifdef Z3DEBUG //#ifdef Z3DEBUG
#define DEBUG_CODE(CODE) { CODE } ((void) 0) //#define DEBUG_CODE(CODE) { CODE } ((void) 0)
#else //#else
#define DEBUG_CODE(CODE) ((void) 0) #define DEBUG_CODE(CODE) ((void) 0)
#endif //#endif
#ifdef __APPLE__ #ifdef __APPLE__
#include <TargetConditionals.h> #include <TargetConditionals.h>

15
src/util/lp/equiv_monomials.h
View file

@ -20,12 +20,12 @@
namespace nla { namespace nla {
struct const_iterator_equiv_mon { struct const_iterator_equiv_mon {
// fields // fields
vector<const unsigned_vector*> m_same_abs_vals; const vector<const unsigned_vector*>& m_same_abs_vals;
vector<unsigned_vector::const_iterator> m_its; vector<unsigned_vector::const_iterator> m_its;
bool m_done; bool m_done;
std::function<unsigned (const unsigned_vector&)> m_find_monomial; std::function<unsigned (const unsigned_vector&)> m_find_monomial;
// constructor for begin() // constructor for begin()
const_iterator_equiv_mon(vector<const unsigned_vector*> abs_vals, const_iterator_equiv_mon(const vector<const unsigned_vector*>& abs_vals,
std::function<unsigned (const unsigned_vector&)> find_monomial) std::function<unsigned (const unsigned_vector&)> find_monomial)
: m_same_abs_vals(abs_vals), : m_same_abs_vals(abs_vals),
m_done(false), m_done(false),
@ -35,7 +35,7 @@ struct const_iterator_equiv_mon {
} }
} }
// constructor for end() // constructor for end()
const_iterator_equiv_mon() : m_done(true) {} const_iterator_equiv_mon(const vector<const unsigned_vector*>& abs_vals) : m_same_abs_vals(abs_vals), m_done(true) {}
//typedefs //typedefs
typedef const_iterator_equiv_mon self_type; typedef const_iterator_equiv_mon self_type;
@ -87,12 +87,15 @@ struct equiv_monomials {
const monomial & m_mon; const monomial & m_mon;
std::function<const unsigned_vector*(lpvar)> m_abs_eq_vars; std::function<const unsigned_vector*(lpvar)> m_abs_eq_vars;
std::function<unsigned (const unsigned_vector&)> m_find_monomial; std::function<unsigned (const unsigned_vector&)> m_find_monomial;
vector<const unsigned_vector*> m_vars_eqs;
equiv_monomials(const monomial & m, equiv_monomials(const monomial & m,
std::function<const unsigned_vector*(lpvar)> abs_eq_vars, std::function<const unsigned_vector*(lpvar)> abs_eq_vars,
std::function<unsigned (const unsigned_vector&)> find_monomial) : std::function<unsigned (const unsigned_vector&)> find_monomial) :
m_mon(m), m_mon(m),
m_abs_eq_vars(abs_eq_vars), m_abs_eq_vars(abs_eq_vars),
m_find_monomial(find_monomial) {} m_find_monomial(find_monomial),
m_vars_eqs(vars_eqs())
{}
vector<const unsigned_vector*> vars_eqs() const { vector<const unsigned_vector*> vars_eqs() const {
vector<const unsigned_vector*> r; vector<const unsigned_vector*> r;
@ -102,10 +105,10 @@ struct equiv_monomials {
return r; return r;
} }
const_iterator_equiv_mon begin() const { const_iterator_equiv_mon begin() const {
return const_iterator_equiv_mon(vars_eqs(), m_find_monomial); return const_iterator_equiv_mon(m_vars_eqs, m_find_monomial);
} }
const_iterator_equiv_mon end() const { const_iterator_equiv_mon end() const {
return const_iterator_equiv_mon(); return const_iterator_equiv_mon(m_vars_eqs);
} }
}; };
} // end of namespace nla } // end of namespace nla