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

Added limit to "visit" to allow detecting multiple visits (#6435)

Browse source 
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Added limit to "visit" to allow detecting multiple visits

* Putting visit in a separate class
(Reason: We will probably need two of them in the sat::solver)

* Bugfix
This commit is contained in:
Clemens Eisenhofer 2022-11-03 11:34:52 +01:00 • committed by GitHub
parent e0bbe8dfc0
commit 6790f18132
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
7 changed files with 68 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/sat/sat_solver.h
View file

@ -28,6 +28,7 @@ Revision History:
#include "util/rlimit.h"
#include "util/scoped_ptr_vector.h"
#include "util/scoped_limit_trail.h"
#include "util/visit_helper.h"
#include "sat/sat_types.h"
#include "sat/sat_clause.h"
#include "sat/sat_watched.h"
@ -176,8 +177,7 @@ namespace sat {
std::string m_reason_unknown;
bool m_trim = false;
svector<unsigned> m_visited;
unsigned m_visited_ts;
visit_helper m_visited;
struct scope {
unsigned m_trail_lim;
@ -342,13 +342,8 @@ namespace sat {
void detach_nary_clause(clause & c);
void push_reinit_stack(clause & c);
void push_reinit_stack(literal l1, literal l2);
void init_ts(unsigned n, svector<unsigned>& v, unsigned& ts);
void init_visited();
void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; }
void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
bool is_visited(bool_var v) const { return is_visited(literal(v, false)); }
bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; }
void init_visited(unsigned lim = 1) { m_visited.init_visited(num_vars(), lim); }
bool all_distinct(literal_vector const& lits);
bool all_distinct(clause const& cl);