diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 06fe6061a..815de26b9 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -439,7 +439,6 @@ public class Context implements AutoCloseable { * Creates a new function declaration. **/ public FuncDecl mkFuncDecl(Symbol name, Sort[] domain, Sort range) - { checkContextMatch(name); checkContextMatch(domain); @@ -483,6 +482,33 @@ public class Context implements AutoCloseable { return new FuncDecl(this, mkSymbol(name), q, range); } + /** + * Creates a new recursive function declaration. + **/ + public FuncDecl mkRecFuncDecl(Symbol name, Sort[] domain, Sort range) + { + checkContextMatch(name); + checkContextMatch(domain); + checkContextMatch(range); + return new FuncDecl(this, name, domain, range, true); + } + + + /** + * Bind a definition to a recursive function declaration. + * The function must have previously been created using + * MkRecFuncDecl. The body may contain recursive uses of the function or + * other mutually recursive functions. + */ + public void AddRecDef(FuncDecl f, Expr[] args, Expr body) + { + checkContextMatch(f); + checkContextMatch(args); + checkContextMatch(body); + long[] argsNative = AST.arrayToNative(args); + Native.addRecDef(nCtx(), f.getNativeObject(), (uint)args.Length, argsNative, body.getNativeObject()); + } + /** * Creates a fresh function declaration with a name prefixed with * {@code prefix}. diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 255bc2c4a..124c13864 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -336,11 +336,17 @@ public class FuncDecl extends AST } FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) - { super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(), AST.arrayLength(domain), AST.arrayToNative(domain), range.getNativeObject())); + } + + FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range, bool is_rec) + { + super(ctx, Native.mkRecFuncDecl(ctx.nCtx(), name.getNativeObject(), + AST.arrayLength(domain), AST.arrayToNative(domain), + range.getNativeObject())); } diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 401b4085a..43cae35f0 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -165,6 +165,14 @@ void bit_blaster_tpl::mk_subtracter(unsigned sz, expr * const * a_bits, exp out_bits.push_back(out); cin = cout; } +#if 0 + for (unsigned j = 0; j < sz; ++j) { + std::cout << j << "\n"; + std::cout << mk_pp(a_bits[j], m()) << "\n"; + std::cout << mk_pp(b_bits[j], m()) << "\n"; + std::cout << mk_pp(out_bits.get(j), m()) << "\n"; + } +#endif SASSERT(out_bits.size() == sz); } diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 49a73b269..cfa2cc61a 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -212,11 +212,11 @@ public: } switch (is_sat) { case l_true: - CTRACE("opt", !m_model->is_true(m_asms), + CTRACE("opt", m_model->is_false(m_asms), tout << *m_model << "assumptions: "; for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " "; tout << "\n";); - SASSERT(m_model->is_true(m_asms) || m.limit().is_canceled()); + SASSERT(!m_model->is_false(m_asms) || m.limit().is_canceled()); found_optimum(); return l_true; case l_false: diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index c6e1fc87c..6f3ccd809 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -112,11 +112,6 @@ namespace sat { } } - if (n == 3 && c[0] == literal(9357, true) && c[1] == literal(25, true) && c[2] == literal(8691, false)) { - SASSERT(false); - UNREACHABLE(); - } - if (!st.is_sat()) { for (char ch : m_theory[st.get_th()]) buffer[len++] = ch; @@ -147,6 +142,11 @@ namespace sat { buffer[len++] = '\n'; m_out->write(buffer, len); + if (n == 3 && c[0] == literal(9357, true) && c[1] == literal(25, true) && c[2] == literal(8691, false)) { + m_out->flush(); + SASSERT(false); + UNREACHABLE(); + } } void drat::dump_activity() { diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 4aeb2ff43..a054c7202 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -341,18 +341,32 @@ namespace bv { void solver::log_drat(bv_justification const& c) { // introduce dummy literal for equality. sat::literal leq(s().num_vars() + 1, false); - expr* e1 = var2expr(c.m_v1); - expr* e2 = var2expr(c.m_v2); - expr_ref eq(m.mk_eq(e1, e2), m); - ctx.get_drat().def_begin('e', eq->get_id(), std::string("=")); - ctx.get_drat().def_add_arg(e1->get_id()); - ctx.get_drat().def_add_arg(e2->get_id()); - ctx.get_drat().def_end(); - ctx.get_drat().bool_def(leq.var(), eq->get_id()); + if (c.m_kind != bv_justification::kind_t::bit2ne) { + expr* e1 = var2expr(c.m_v1); + expr* e2 = var2expr(c.m_v2); + expr_ref eq(m.mk_eq(e1, e2), m); + ctx.get_drat().def_begin('e', eq->get_id(), std::string("=")); + ctx.get_drat().def_add_arg(e1->get_id()); + ctx.get_drat().def_add_arg(e2->get_id()); + ctx.get_drat().def_end(); + ctx.get_drat().bool_def(leq.var(), eq->get_id()); + } + + static unsigned s_count = 0; sat::literal_vector lits; switch (c.m_kind) { case bv_justification::kind_t::eq2bit: + ++s_count; + std::cout << "eq2bit " << s_count << "\n"; +#if 0 + if (s_count == 1899) { + std::cout << "eq2bit " << mk_pp(var2expr(c.m_v1), m) << " == " << mk_pp(var2expr(c.m_v2), m) << "\n"; + std::cout << literal2expr(~c.m_antecedent) << "\n"; + std::cout << literal2expr(c.m_consequent) << "\n"; + INVOKE_DEBUGGER(); + } +#endif lits.push_back(~leq); lits.push_back(~c.m_antecedent); lits.push_back(c.m_consequent);