mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

local changes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-27 09:18:52 -07:00
parent 4d8af9191c
commit cb00555635
5 changed files with 18 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/api/java/InterpolationContext.java
View file

@ -90,7 +90,7 @@ public class InterpolationContext extends Context
public class ComputeInterpolantResult
{
public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
public ASTVector interp = null;
public BoolExpr[] interp = null;
public Model model = null;
};
@ -109,8 +109,13 @@ public class InterpolationContext extends Context
ComputeInterpolantResult res = new ComputeInterpolantResult();
Native.LongPtr n_i = new Native.LongPtr();
Native.LongPtr n_m = new Native.LongPtr();
res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value);
res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
if (res.status == Z3_lbool.Z3_L_FALSE) {xx
res.interp = new BoolExpr[Native.astVectorSize(nCtx(), n_i.value)];
for (int i = 0; i < res.interp.Length; ++i) {
res.interp[i] = new BoolExpr(this, Native.astVectorGet(nCtx(), i));
}
}
if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
return res;
}

1
src/math/euclid/euclidean_solver.cpp
View file

@ -609,6 +609,7 @@ struct euclidean_solver::imp {
// neg coeffs... to make sure that m_next_x is -1
neg_coeffs(eq.m_as);
neg_coeffs(eq.m_bs);
m().neg(eq.m_c);
}
unsigned sz = eq.size();
for (unsigned i = 0; i < sz; i++) {

6
src/smt/smt_internalizer.cpp
View file

@ -1411,6 +1411,10 @@ namespace smt {
void context::mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params) {
justification * js = 0;
TRACE("mk_th_axiom",
display_literals_verbose(tout, num_lits, lits);
tout << "\n";);
if (m_manager.proofs_enabled()) {
js = mk_justification(theory_axiom_justification(tid, m_region, num_lits, lits, num_params, params));
}
@ -1425,13 +1429,11 @@ namespace smt {
void context::mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params, parameter * params) {
literal ls[2] = { l1, l2 };
TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << "\n";);
mk_th_axiom(tid, 2, ls, num_params, params);
}
void context::mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
literal ls[3] = { l1, l2, l3 };
TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << " "; display_literal(tout, l3); tout << "\n";);
mk_th_axiom(tid, 3, ls, num_params, params);
}

2
src/smt/theory_arith_core.h
View file

@ -439,6 +439,7 @@ namespace smt {
j += rational(1);
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.begin());
#else
// performs slightly worse.
literal_buffer lits;
@ -2788,6 +2789,7 @@ namespace smt {
tout << " --> ";
ctx.display_detailed_literal(tout, l);
tout << "\n";);
SASSERT(false);
if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
literal_vector & lits = m_tmp_literal_vector2;
lits.reset();

4
src/smt/theory_arith_int.h
View file

@ -1061,6 +1061,7 @@ namespace smt {
}
if (!failed) {
m_solver.assert_eq(as.size(), as.c_ptr(), xs.c_ptr(), c, j);
TRACE("euclidean_solver", tout << "add definition: v" << v << " := " << mk_ismt2_pp(n, t.get_manager()) << "\n";);
}
else {
TRACE("euclidean_solver", tout << "failed for:\n" << mk_ismt2_pp(n, t.get_manager()) << "\n";);
@ -1191,7 +1192,8 @@ namespace smt {
if (l != 0) {
rational l_old = l->get_value().get_rational().to_rational();
rational l_new = g*ceil((l_old - c2)/g) + c2;
TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";);
TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";
tout << "c: " << c2 << " ceil((l_old - c2)/g): " << (ceil((l_old - c2)/g)) << "\n";);
if (l_new > l_old) {
propagated = true;
mk_lower(v, l_new, l, m_js);