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

snapshot

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-15 17:31:31 -08:00
parent 314f03c12c
commit 13c97d12a8
2 changed files with 33 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/smt/theory_pb.cpp
View file

@ -196,7 +196,7 @@ namespace smt {
lbool theory_pb::normalize_ineq(arg_t& args, int& k) { lbool theory_pb::normalize_ineq(arg_t& args, int& k) {
// normalize first all literals to be positive: // normalize first all literals to be positive:
// then we can can compare them more easily. // then we can compare them more easily.
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
if (args[i].first.sign()) { if (args[i].first.sign()) {
args[i].first.neg(); args[i].first.neg();
@ -451,7 +451,7 @@ namespace smt {
if (m_watch.find(v, ineqs)) { if (m_watch.find(v, ineqs)) {
for (unsigned i = 0; i < ineqs->size(); ++i) { for (unsigned i = 0; i < ineqs->size(); ++i) {
// TBD: assign_use(v, is_true, *(*ineqs)[i]); assign_watch(v, is_true, *ineqs, i);
} }
} }
if (m_ineqs.find(v, c)) { if (m_ineqs.find(v, c)) {
@ -459,6 +459,36 @@ namespace smt {
} }
} }
void theory_pb::assign_watch(bool_var v, bool is_true, watch_list& watch, unsigned index) {
#if 0
TBD
ineq& c = *watch[i];
c.m_sum;
unsigned w;
for (w = 0; w < c.m_watch_sz; ++i) {
if (c.m_args[w].first.var() == v) {
break;
}
}
SASSERT(w < c.m_watch_sz);
literal l = c.m_args[w].first;
int coeff = c.m_args[w].second;
if (is_true == !l.sign()) {
ctx.push_trail(value_trail<context, int>(c.m_sum));
c.m_sum += coeff;
// optional propagate
}
else {
unsigned deficit = c.m_max_sum - coeff;
for (unsigned i = c.m_watch_sz; i < c.m_args.size(); ++i) {
if
}
// find a different literal to watch.
ctx.push_trail(value_trail<context, unsigned>(c.m_watch_sz));
}
#endif
}
struct theory_pb::sort_expr { struct theory_pb::sort_expr {
theory_pb& th; theory_pb& th;
context& ctx; context& ctx;

1
src/smt/theory_pb.h
View file

@ -78,6 +78,7 @@ namespace smt {
lbool normalize_ineq(arg_t& args, int& k); lbool normalize_ineq(arg_t& args, int& k);
literal compile_arg(expr* arg); literal compile_arg(expr* arg);
void add_watch(literal l, ineq* c); void add_watch(literal l, ineq* c);
void assign_watch(bool_var v, bool is_true, watch_list& watch, unsigned index);
std::ostream& display(std::ostream& out, ineq& c) const; std::ostream& display(std::ostream& out, ineq& c) const;