mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

call mux finder

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-31 12:00:16 -08:00
parent 4392b88718
commit 1e0d49512b
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_solver.cpp
View file

@ -4174,7 +4174,7 @@ namespace sat {
lbool solver::find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes) {
max_cliques<neg_literal> mc;
m_user_bin_clauses.reset();
m_binary_clause_graph.reset();
// m_binary_clause_graph.reset();
collect_bin_clauses(m_user_bin_clauses, true, false);
hashtable<literal_pair, pair_hash<literal_hash, literal_hash>, default_eq<literal_pair> > seen_bc;
for (auto const& b : m_user_bin_clauses) {
@ -4189,7 +4189,7 @@ namespace sat {
vector<unsigned_vector> _mutexes;
literal_vector _lits(lits);
if (m_ext) {
// m_ext->find_mutexes(_lits, mutexes);
m_ext->find_mutexes(_lits, mutexes);
}
unsigned_vector ps;
for (literal lit : _lits) {

2
src/sat/sat_solver.h
View file

@ -755,7 +755,7 @@ namespace sat {
u_map<index_set> m_antecedents;
literal_vector m_todo_antecedents;
vector<literal_vector> m_binary_clause_graph;
// vector<literal_vector> m_binary_clause_graph;
bool extract_assumptions(literal lit, index_set& s);