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

fix #3201

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-07 15:27:04 +01:00
parent dd5744a357
commit 99b291e78d
1 changed files with 9 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/nlsat/nlsat_solver.cpp
View file

@ -59,12 +59,14 @@ namespace nlsat {
unsynch_mpq_manager m_qm; unsynch_mpq_manager m_qm;
pmanager m_pm; pmanager m_pm;
anum_manager m_am; anum_manager m_am;
ctx(reslimit& rlim, params_ref const & p): bool m_incremental;
ctx(reslimit& rlim, params_ref const & p, bool incremental):
m_params(p), m_params(p),
m_rlimit(rlim), m_rlimit(rlim),
m_allocator("nlsat"), m_allocator("nlsat"),
m_pm(rlim, m_qm, &m_allocator), m_pm(rlim, m_qm, &m_allocator),
m_am(rlim, m_qm, p, &m_allocator) m_am(rlim, m_qm, p, &m_allocator),
m_incremental(incremental)
{} {}
}; };
@ -215,12 +217,12 @@ namespace nlsat {
unsigned m_stages; unsigned m_stages;
unsigned m_irrational_assignments; // number of irrational witnesses unsigned m_irrational_assignments; // number of irrational witnesses
imp(solver& s, ctx& c, bool incremental): imp(solver& s, ctx& c):
m_ctx(c), m_ctx(c),
m_solver(s), m_solver(s),
m_rlimit(c.m_rlimit), m_rlimit(c.m_rlimit),
m_allocator(c.m_allocator), m_allocator(c.m_allocator),
m_incremental(incremental), m_incremental(c.m_incremental),
m_qm(c.m_qm), m_qm(c.m_qm),
m_pm(c.m_pm), m_pm(c.m_pm),
m_cache(m_pm), m_cache(m_pm),
@ -3434,13 +3436,13 @@ namespace nlsat {
}; };
solver::solver(reslimit& rlim, params_ref const & p, bool incremental) { solver::solver(reslimit& rlim, params_ref const & p, bool incremental) {
m_ctx = alloc(ctx, rlim, p); m_ctx = alloc(ctx, rlim, p, incremental);
m_imp = alloc(imp, *this, *m_ctx, incremental); m_imp = alloc(imp, *this, *m_ctx);
} }
solver::solver(ctx& ctx) { solver::solver(ctx& ctx) {
m_ctx = nullptr; m_ctx = nullptr;
m_imp = alloc(imp, *this, ctx, false); m_imp = alloc(imp, *this, ctx);
} }
solver::~solver() { solver::~solver() {