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

fix assertions reported by Christoph

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-04-23 08:07:37 +02:00
parent d67b5226f0
commit 23a74b3c26
4 changed files with 21 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/api/python/z3.py
View file

@ -6010,6 +6010,22 @@ class Solver(Z3PPObject):
"""
return Z3_solver_to_string(self.ctx.ref(), self.solver)
def to_smt2(self):
"""return SMTLIB2 formatted benchmark for solver's assertions"""
es = self.assertions()
sz = len(es)
sz1 = sz
if sz1 > 0:
sz1 -= 1
v = (Ast * sz1)()
for i in range(sz1):
v[i] = es[i].as_ast()
if sz > 0:
e = es[sz1].as_ast()
else:
e = BoolVal(True, self.ctx).as_ast()
return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
def SolverFor(logic, ctx=None):
"""Create a solver customized for the given logic.

1
src/opt/opt_sls_solver.h
View file

@ -90,7 +90,6 @@ namespace opt {
m_solver->get_labels(r);
}
virtual void set_cancel(bool f) {
std::cout << "set cancel\n";
m_solver->set_cancel(f);
m_pb2bv.set_cancel(f);
#pragma omp critical (sls_solver)

7
src/opt/pb_sls.cpp
View file

@ -301,6 +301,7 @@ namespace smt {
clause const& cls = clauses[i];
for (unsigned j = 0; j < cls.m_lits.size(); ++j) {
literal lit = cls.m_lits[j];
if (occ.size() <= static_cast<unsigned>(lit.var())) occ.resize(lit.var() + 1);
occ[lit.var()].push_back(i);
}
}
@ -314,6 +315,10 @@ namespace smt {
m_soft_false.reset();
m_soft_occ.reset();
m_penalty.reset();
for (unsigned i = 0; i <= m_var2decl.size(); ++i) {
m_soft_occ.push_back(unsigned_vector());
m_hard_occ.push_back(unsigned_vector());
}
// initialize the occurs vectors.
init_occ(m_clauses, m_hard_occ);
@ -443,7 +448,6 @@ namespace smt {
}
int flip(literal l) {
SASSERT(get_value(l));
m_assignment[l.var()] = !m_assignment[l.var()];
int break_count = 0;
unsigned_vector const& occh = m_hard_occ[l.var()];
@ -484,7 +488,6 @@ namespace smt {
}
}
SASSERT(get_value(~l));
TRACE("opt", tout << "flip: " << l << " num false: " << m_hard_false.num_elems()
<< " penalty: " << m_penalty << " break count: " << break_count << "\n";);
return break_count;

1
src/opt/weighted_maxsat.cpp
View file

@ -162,7 +162,6 @@ namespace opt {
void enable_sls() {
if (m_enable_sls && probe_bv()) {
std::cout << "SLS enabled\n";
m_params.set_uint("restarts", 20);
m_s = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params);
}