add recfuns to Java #4820

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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}. 

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()));
 
     }
 

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -165,6 +165,14 @@ void bit_blaster_tpl<Cfg>::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);
 }
 

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:

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() {

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);