mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

rebase with Z3Prover

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-06 17:55:49 -08:00
parent a83425bec6
commit 976f10c613
4 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -53,7 +53,7 @@ add_subdirectory(parsers/util)
add_subdirectory(math/grobner) add_subdirectory(math/grobner)
add_subdirectory(sat) add_subdirectory(sat)
add_subdirectory(nlsat) add_subdirectory(nlsat)
add_subdirectory(util/lp) add_subdirectory(math/lp)
add_subdirectory(math/euclid) add_subdirectory(math/euclid)
add_subdirectory(tactic/core) add_subdirectory(tactic/core)
add_subdirectory(math/subpaving/tactic) add_subdirectory(math/subpaving/tactic)

4
src/math/grobner/pdd_solver.h
View file

@ -130,8 +130,8 @@ public:
private: private:
bool step(); bool step();
equation* pick_next(); equation* pick_next();
bool canceled() const; bool canceled();
bool done() const; bool done();
void superpose(equation const& eq1, equation const& eq2); void superpose(equation const& eq1, equation const& eq2);
void superpose(equation const& eq); void superpose(equation const& eq);
void simplify_using(equation& eq, equation_vector const& eqs); void simplify_using(equation& eq, equation_vector const& eqs);

8
src/math/lp/nla_core.cpp
View file

@ -20,7 +20,7 @@ Revision History:
#include "math/lp/nla_core.h" #include "math/lp/nla_core.h"
#include "math/lp/factorization_factory_imp.h" #include "math/lp/factorization_factory_imp.h"
#include "math/lp/nex.h" #include "math/lp/nex.h"
#include "math/grobner/pdd_grobner.h" #include "math/grobner/pdd_solver.h"
#include "math/dd/pdd_interval.h" #include "math/dd/pdd_interval.h"
#include "math/dd/pdd_eval.h" #include "math/dd/pdd_eval.h"
namespace nla { namespace nla {
@ -1429,11 +1429,11 @@ void core::run_pdd_grobner() {
tree_size = std::max(tree_size, e->poly().tree_size()); tree_size = std::max(tree_size, e->poly().tree_size());
} }
tree_size *= 10; tree_size *= 10;
struct dd::grobner::config cfg; struct dd::solver::config cfg;
cfg.m_expr_size_limit = (unsigned)tree_size; cfg.m_expr_size_limit = (unsigned)tree_size;
cfg.m_eqs_threshold = m_pdd_grobner.equations().size()*5; cfg.m_eqs_threshold = m_pdd_grobner.equations().size()*5;
cfg.m_max_steps = m_pdd_grobner.equations().size(); cfg.m_max_steps = m_pdd_grobner.equations().size();
m_pdd_grobner = cfg; m_pdd_grobner.set(cfg);
m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes. m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
@ -1480,7 +1480,7 @@ std::ostream& core::diagnose_pdd_miss(std::ostream& out) {
return out; return out;
} }
bool core::check_pdd_eq(const dd::grobner::equation* e) { bool core::check_pdd_eq(const dd::solver::equation* e) {
dd::pdd_interval eval(m_pdd_manager, m_reslim); dd::pdd_interval eval(m_pdd_manager, m_reslim);
eval.var2interval() = eval.var2interval() =
[this](lpvar j, bool deps) { [this](lpvar j, bool deps) {

6
src/math/lp/nla_core.h
View file

@ -30,7 +30,7 @@
#include "math/lp/nex.h" #include "math/lp/nex.h"
#include "math/lp/horner.h" #include "math/lp/horner.h"
#include "math/lp/nla_intervals.h" #include "math/lp/nla_intervals.h"
#include "math/grobner/pdd_grobner.h" #include "math/grobner/pdd_solver.h"
namespace nla { namespace nla {
@ -95,7 +95,7 @@ public:
horner m_horner; horner m_horner;
nla_settings m_nla_settings; nla_settings m_nla_settings;
dd::pdd_manager m_pdd_manager; dd::pdd_manager m_pdd_manager;
dd::grobner m_pdd_grobner; dd::solver m_pdd_grobner;
private: private:
emonics m_emons; emonics m_emons;
@ -408,7 +408,7 @@ public:
void set_active_vars_weights(nex_creator&); void set_active_vars_weights(nex_creator&);
unsigned get_var_weight(lpvar) const; unsigned get_var_weight(lpvar) const;
void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row); void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);
bool check_pdd_eq(const dd::grobner::equation*); bool check_pdd_eq(const dd::solver::equation*);
const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep); const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&); dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
void set_level2var_for_pdd_grobner(); void set_level2var_for_pdd_grobner();