From 022a1fd3ddd733848914619f5e1aec3912760400 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 Mar 2021 15:00:23 -0800
Subject: [PATCH] fix #5080 assertion is violated on legal input, add an
example
---
examples/python/hs.py | 62 +++++++++++++++++++++++++++++++++++++
examples/python/rc2.py | 2 --
src/sat/smt/pb_constraint.h | 1 -
3 files changed, 62 insertions(+), 3 deletions(-)
create mode 100644 examples/python/hs.py
diff --git a/examples/python/hs.py b/examples/python/hs.py
new file mode 100644
index 000000000..740c3a972
--- /dev/null
+++ b/examples/python/hs.py
@@ -0,0 +1,62 @@
+#
+# Unweighted hitting set maxsat solver.
+#
+
+class Soft:
+ __init__(self, soft):
+ self.formulas = soft
+ self.name2formula = { Bool(f"s{s}") : s for s in soft }
+ self.formula2name = { s : v for (v, s) in self._name2formula.items() }
+
+def improve(hi, mdl, new_model, soft):
+ cost = len([f for f in soft.formulas if not is_true(new_model.eval(f))])
+ if cost <= hi:
+ mdl = new_model
+ if cost < hi:
+ hi = cost
+ return hi, mdl
+
+def pick_hs(K, soft):
+ opt = Optimize()
+ for k in K:
+ opt.add(Or(soft.formula2name[f] for f in k))
+ for n in soft.formula2name.values():
+ opt.add_soft(Not(n))
+ print(opt.check())
+ mdl = opt.model()
+ hs = [soft.name2formula[n] for n in soft.formula2name.values() if is_true(mdl.eval(n))]
+ return hs, True
+
+def hs(lo, hi, mdl, K, s, soft):
+ hs, is_min = pick_hs(K, soft)
+ is_sat = s.check(set(soft.formulas) - set(hs))
+ if is_sat == sat:
+ hi, mdl = improve(hi, mdl, s.model(), soft)
+ elif is_sat == unsat:
+ core = s.unsat_core()
+ K += [set(core)]
+ if is_min:
+ lo = max(lo, len(hs))
+ else:
+ print("unknown")
+ print(lo, hi)
+ return lo, hi, mdl, K
+
+
+def main(file):
+ s = Solver()
+ opt = Optimize()
+ opt.from_file(file)
+ s.add(opt.assertions())
+ soft = [f.arg(0) for f in opt.objectives()[0].children()]
+ K = []
+ lo = 0
+ hi = len(soft)
+ soft = Soft(soft)
+ while lo < hi:
+ lo, hi, mdl, K = hs(lo, hi, None, K, s, soft)
+
+def __main__():
+ main(sys.argv[0])
+
+
diff --git a/examples/python/rc2.py b/examples/python/rc2.py
index c4e811eb1..6904b46ea 100644
--- a/examples/python/rc2.py
+++ b/examples/python/rc2.py
@@ -8,8 +8,6 @@
from z3 import *
-from z3 import *
-
def tt(s, f):
return is_true(s.model().eval(f))
diff --git a/src/sat/smt/pb_constraint.h b/src/sat/smt/pb_constraint.h
index 6ab8fcf9d..076151395 100644
--- a/src/sat/smt/pb_constraint.h
+++ b/src/sat/smt/pb_constraint.h
@@ -51,7 +51,6 @@ namespace pb {
public:
constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k):
m_tag(t), m_lit(l), m_size(sz), m_obj_size(osz), m_id(id), m_k(k) {
- VERIFY(k < 400000000);
}
sat::ext_constraint_idx cindex() const { return sat::constraint_base::mem2base(this); }
void deallocate(small_object_allocator& a) { a.deallocate(obj_size(), sat::constraint_base::mem2base_ptr(this)); }