mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix mutex finding for smt-core: it was returning mutexes for negations of literals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-20 22:13:23 -07:00
parent 881e82e3fa
commit 9cd7b9b4f6
2 changed files with 15 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_consequences.cpp
View file

@ -373,7 +373,7 @@ namespace smt {
expr* n = vars[i]; expr* n = vars[i];
bool neg = m_manager.is_not(n, n); bool neg = m_manager.is_not(n, n);
if (b_internalized(n)) { if (b_internalized(n)) {
lits.insert(literal(get_bool_var(n), !neg).index()); lits.insert(literal(get_bool_var(n), neg).index());
} }
} }
while (!lits.empty()) { while (!lits.empty()) {

21
src/tactic/arith/pb2bv_tactic.cpp
View file

@ -29,10 +29,11 @@ Notes:
#include"filter_model_converter.h" #include"filter_model_converter.h"
#include"pb2bv_model_converter.h" #include"pb2bv_model_converter.h"
#include"pb2bv_tactic.h" #include"pb2bv_tactic.h"
#include"ast_pp.h"
class pb2bv_tactic : public tactic { class pb2bv_tactic : public tactic {
public: public:
struct non_pb {}; struct non_pb { expr* e; non_pb(expr* e) : e(e) {}};
struct only_01_visitor { struct only_01_visitor {
typedef rational numeral; typedef rational numeral;
@ -48,7 +49,7 @@ public:
void throw_non_pb(expr * n) { void throw_non_pb(expr * n) {
TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";); TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";);
throw non_pb(); throw non_pb(n);
} }
void operator()(var * n) { void operator()(var * n) {
@ -575,7 +576,7 @@ private:
void throw_non_pb(expr * n) { void throw_non_pb(expr * n) {
TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";); TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";);
throw non_pb(); throw non_pb(n);
} }
// check if polynomial is encoding // check if polynomial is encoding
@ -910,8 +911,8 @@ private:
try { try {
quick_pb_check(g); quick_pb_check(g);
} }
catch (non_pb) { catch (non_pb& p) {
throw tactic_exception("goal is in a fragment unsupported by pb2bv"); throw_tactic(p.e);
} }
unsigned size = g->size(); unsigned size = g->size();
@ -940,8 +941,8 @@ private:
new_exprs.push_back(new_f); new_exprs.push_back(new_f);
} }
} }
catch (non_pb) { catch (non_pb& p) {
throw tactic_exception("goal is in a fragment unsupported by pb2bv"); throw_tactic(p.e);
} }
for (unsigned idx = 0; idx < size; idx++) for (unsigned idx = 0; idx < size; idx++)
@ -966,6 +967,12 @@ private:
TRACE("pb2bv", g->display(tout);); TRACE("pb2bv", g->display(tout););
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
} }
void throw_tactic(expr* e) {
std::stringstream strm;
strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m);
throw tactic_exception(strm.str().c_str());
}
}; };
imp * m_imp; imp * m_imp;