mirror of
https://github.com/Z3Prover/z3
synced 2025-08-02 09:20:22 +00:00
parent
2ac8d3461e
commit
b686bb61fe
2 changed files with 7 additions and 2 deletions
|
@ -15,6 +15,7 @@ Author:
|
||||||
|
|
||||||
--*/
|
--*/
|
||||||
|
|
||||||
|
#include "ast/ast_util.h"
|
||||||
#include "smt/tactic/unit_subsumption_tactic.h"
|
#include "smt/tactic/unit_subsumption_tactic.h"
|
||||||
#include "smt/smt_context.h"
|
#include "smt/smt_context.h"
|
||||||
|
|
||||||
|
@ -92,7 +93,8 @@ struct unit_subsumption_tactic : public tactic {
|
||||||
m_context.push();
|
m_context.push();
|
||||||
for (unsigned j = 0; j < m_clause_count; ++j) {
|
for (unsigned j = 0; j < m_clause_count; ++j) {
|
||||||
if (i == j) {
|
if (i == j) {
|
||||||
m_context.assert_expr(m.mk_not(m_clauses.get(j)));
|
expr_ref fml(mk_not(m, m_clauses.get(j)), m);
|
||||||
|
m_context.assert_expr(fml);
|
||||||
}
|
}
|
||||||
else if (!m_is_deleted.get(j)) {
|
else if (!m_is_deleted.get(j)) {
|
||||||
m_context.assert_expr(m_clauses.get(j));
|
m_context.assert_expr(m_clauses.get(j));
|
||||||
|
|
|
@ -737,6 +737,7 @@ namespace smt {
|
||||||
*/
|
*/
|
||||||
template<typename Ext>
|
template<typename Ext>
|
||||||
void theory_utvpi<Ext>::enforce_parity() {
|
void theory_utvpi<Ext>::enforce_parity() {
|
||||||
|
SASSERT(m_graph.is_feasible());
|
||||||
unsigned_vector todo;
|
unsigned_vector todo;
|
||||||
unsigned sz = get_num_vars();
|
unsigned sz = get_num_vars();
|
||||||
for (unsigned i = 0; i < sz; ++i) {
|
for (unsigned i = 0; i < sz; ++i) {
|
||||||
|
@ -774,6 +775,7 @@ namespace smt {
|
||||||
}
|
}
|
||||||
display(tout);
|
display(tout);
|
||||||
);
|
);
|
||||||
|
SASSERT(m_graph.is_feasible());
|
||||||
|
|
||||||
for (auto v : zero_v) {
|
for (auto v : zero_v) {
|
||||||
m_graph.inc_assignment(v, numeral(-1));
|
m_graph.inc_assignment(v, numeral(-1));
|
||||||
|
@ -782,8 +784,8 @@ namespace smt {
|
||||||
todo.push_back(k);
|
todo.push_back(k);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
TRACE("utvpi", display(tout););
|
||||||
}
|
}
|
||||||
SASSERT(m_graph.is_feasible());
|
|
||||||
DEBUG_CODE(
|
DEBUG_CODE(
|
||||||
for (unsigned i = 0; i < sz; ++i) {
|
for (unsigned i = 0; i < sz; ++i) {
|
||||||
enode* e = get_enode(i);
|
enode* e = get_enode(i);
|
||||||
|
@ -792,6 +794,7 @@ namespace smt {
|
||||||
UNREACHABLE();
|
UNREACHABLE();
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
|
SASSERT(m_graph.is_feasible());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue