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

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-15 18:34:12 -08:00
parent 6ddc838628 6da4bae840
commit aadfe007c1
2 changed files with 33 additions and 2 deletions
Show stats 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) {
// 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<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 {
theory_pb& th;
context& ctx;

1
src/smt/theory_pb.h
View file

@ -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;