mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix #2375

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-03 10:04:00 +07:00
parent 1202554dbc
commit 807095a344
2 changed files with 31 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
examples/python/rc2.py
View file

@ -8,6 +8,8 @@
from z3 import * from z3 import *
from z3 import *
def tt(s, f): def tt(s, f):
return is_true(s.model().eval(f)) return is_true(s.model().eval(f))
@ -38,7 +40,7 @@ class RC2:
name = Bool("%s" % fml) name = Bool("%s" % fml)
self.solver.add(Implies(name, fml)) self.solver.add(Implies(name, fml))
self.bounds[name] = (S, k) self.bounds[name] = (S, k)
sel.names[fml] = name self.names[fml] = name
return name return name
def print_cost(self): def print_cost(self):
@ -51,16 +53,18 @@ class RC2:
# sort W, and incrementally add elements of W # sort W, and incrementally add elements of W
# in sorted order to prefer cores with high weight. # in sorted order to prefer cores with high weight.
def check(self, Ws): def check(self, Ws):
ws = sorted(list(Ws), lambda f,w : -w) def compare(fw):
# print(ws) f, w = fw
return -w
ws = sorted([(k,Ws[k]) for k in Ws], key = compare)
i = 0 i = 0
while i < len(ws): while i < len(ws):
j = i j = i
# increment j until making 5% progress or exhausting equal weight entries # increment j until making 5% progress or exhausting equal weight entries
while (j < len(ws) and ws[j][1] == ws[i][1]) or (i > 0 and (i - j)*20 < len(ws)): while (j < len(ws) and ws[j][1] == ws[i][1]) or (i > 0 and (j - i)*20 < len(ws)):
j += 1 j += 1
i = j i = j
r = self.solver.check(ws[j][0] for j in range(i)) r = self.solver.check([ws[j][0] for j in range(i)])
if r == sat: if r == sat:
self.update_max_cost() self.update_max_cost()
else: else:
@ -121,7 +125,7 @@ class RC2:
self.min_cost += w self.min_cost += w
self.print_cost() self.print_cost()
self.update_bounds(Ws, core, w) self.update_bounds(Ws, core, w)
return sel.min_cost, { f for f in self.Ws0 if not tt(self.solver, f) } return self.min_cost, { f for f in self.Ws0 if not tt(self.solver, f) }
def from_file(self, file): def from_file(self, file):
opt = Optimize() opt = Optimize()
@ -133,6 +137,14 @@ class RC2:
assert(f.arg(1).as_long() == 0) assert(f.arg(1).as_long() == 0)
add(Ws, f.arg(0), f.arg(2).as_long()) add(Ws, f.arg(0), f.arg(2).as_long())
return self.maxsat(Ws) return self.maxsat(Ws)
def from_formulas(self, hard, soft):
self.solver.add(hard)
Ws = {}
for f, cost in soft:
add(Ws, f, cost)
return self.maxsat(Ws)
def main(file): def main(file):
s = SolverFor("QF_FD") s = SolverFor("QF_FD")

23
src/qe/nlqsat.cpp
View file

@ -149,8 +149,8 @@ namespace qe {
} }
} }
TRACE("qe", display(tout); TRACE("qe", display(tout);
for (unsigned i = 0; i < m_asms.size(); ++i) { for (nlsat::literal a : m_asms) {
m_solver.display(tout, m_asms[i]); tout << "\n"; m_solver.display(tout, a) << "\n";
}); });
save_model(); save_model();
} }
@ -291,7 +291,7 @@ namespace qe {
} }
nlsat::var_vector vs; nlsat::var_vector vs;
m_solver.vars(l, vs); m_solver.vars(l, vs);
TRACE("qe", m_solver.display(tout, l); tout << "\n";); TRACE("qe", m_solver.display(tout << vs << " ", l) << "\n";);
for (unsigned v : vs) { for (unsigned v : vs) {
level.merge(m_rvar2level[v]); level.merge(m_rvar2level[v]);
} }
@ -492,10 +492,10 @@ namespace qe {
return; return;
} }
expr* n1, *n2; expr* n1, *n2;
if (a.is_div(n, n1, n2) && a.is_numeral(n2)) { rational r;
if (a.is_div(n, n1, n2) && a.is_numeral(n2, r) && !r.is_zero()) {
return; return;
} }
rational r;
if (a.is_power(n, n1, n2) && a.is_numeral(n2, r) && r.is_unsigned()) { if (a.is_power(n, n1, n2) && a.is_numeral(n2, r) && r.is_unsigned()) {
return; return;
} }
@ -511,7 +511,7 @@ namespace qe {
bool has_divs() const { return m_has_divs; } bool has_divs() const { return m_has_divs; }
}; };
void purify(expr_ref& fml, app_ref_vector& pvars, expr_ref_vector& paxioms) { void purify(expr_ref& fml, div_rewriter_star& rw, expr_ref_vector& paxioms) {
is_pure_proc is_pure(*this); is_pure_proc is_pure(*this);
{ {
expr_fast_mark1 visited; expr_fast_mark1 visited;
@ -519,12 +519,12 @@ namespace qe {
} }
if (is_pure.has_divs()) { if (is_pure.has_divs()) {
arith_util arith(m); arith_util arith(m);
div_rewriter_star rw(*this);
proof_ref pr(m); proof_ref pr(m);
TRACE("qe", tout << fml << "\n";);
rw(fml, fml, pr); rw(fml, fml, pr);
TRACE("qe", tout << fml << "\n";);
vector<div> const& divs = rw.divs(); vector<div> const& divs = rw.divs();
for (unsigned i = 0; i < divs.size(); ++i) { for (unsigned i = 0; i < divs.size(); ++i) {
pvars.push_back(divs[i].name);
paxioms.push_back( paxioms.push_back(
m.mk_or(m.mk_eq(divs[i].den, arith.mk_numeral(rational(0), false)), m.mk_or(m.mk_eq(divs[i].den, arith.mk_numeral(rational(0), false)),
m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name)))); m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name))));
@ -540,12 +540,15 @@ namespace qe {
void ackermanize_div(bool is_forall, vector<app_ref_vector>& qvars, expr_ref& fml) { void ackermanize_div(bool is_forall, vector<app_ref_vector>& qvars, expr_ref& fml) {
app_ref_vector pvars(m); app_ref_vector pvars(m);
expr_ref_vector paxioms(m); expr_ref_vector paxioms(m);
purify(fml, pvars, paxioms); div_rewriter_star rw(*this);
purify(fml, rw, paxioms);
if (paxioms.empty()) { if (paxioms.empty()) {
return; return;
} }
expr_ref ante = mk_and(paxioms); expr_ref ante = mk_and(paxioms);
qvars[qvars.size()-2].append(pvars); for (div const& d : rw.divs()) {
qvars[qvars.size()-2].push_back(d.name);
}
if (!is_forall) { if (!is_forall) {
fml = m.mk_implies(ante, fml); fml = m.mk_implies(ante, fml);
} }