From 13c97d12a8f4302a924acf5708ce4f485738f76b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Nov 2013 17:31:31 -0800 Subject: [PATCH] snapshot Signed-off-by: Nikolaj Bjorner --- src/smt/theory_pb.cpp | 34 ++++++++++++++++++++++++++++++++-- src/smt/theory_pb.h | 1 + 2 files changed, 33 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 171615c95..52d525bde 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -196,7 +196,7 @@ namespace smt { lbool theory_pb::normalize_ineq(arg_t& args, int& k) { // 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) { if (args[i].first.sign()) { args[i].first.neg(); @@ -451,7 +451,7 @@ namespace smt { if (m_watch.find(v, ineqs)) { 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)) { @@ -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(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(c.m_watch_sz)); + } +#endif + } + struct theory_pb::sort_expr { theory_pb& th; context& ctx; diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 432d4e497..5fb66f3f4 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -78,6 +78,7 @@ namespace smt { lbool normalize_ineq(arg_t& args, int& k); literal compile_arg(expr* arg); 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;