add ability to create and manipulate model objects

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

examples/c++/example.cpp

@@ -470,7 +470,7 @@ void unsat_core_example2() {
     // The solver s already contains p1 => F
     // To disable F, we add (not p1) as an additional assumption
     qs.push_back(!p1);
-    std::cout << s.check(qs.size(), &qs[0]) << "\n";
+    std::cout << s.check((unsigned)qs.size(), &qs[0]) << "\n";
     expr_vector core2 = s.unsat_core();
     std::cout << core2 << "\n";
     std::cout << "size: " << core2.size() << "\n";

src/api/api_model.cpp

@@ -30,6 +30,17 @@ Revision History:
 
 extern "C" {
 
+    Z3_model Z3_API Z3_mk_model(Z3_context c) {
+        Z3_TRY;
+        LOG_Z3_mk_model(c);
+        RESET_ERROR_CODE();
+        Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
+        m_ref->m_model = alloc(model, mk_c(c)->m());
+        mk_c(c)->save_object(m_ref);
+        RETURN_Z3(of_model(m_ref));
+        Z3_CATCH_RETURN(0);
+    }
+
     void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m) {
         Z3_TRY;
         LOG_Z3_model_inc_ref(c, m);
@@ -224,6 +235,31 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast else_val) {
+        Z3_TRY;
+        LOG_Z3_add_func_interp(c, m, f, else_val);
+        RESET_ERROR_CODE();
+        func_decl* d = to_func_decl(f);
+        model* mdl = to_model_ref(m);
+        Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl); 
+        f_ref->m_func_interp = alloc(func_interp, mk_c(c)->m(), d->get_arity());
+        mk_c(c)->save_object(f_ref);
+        mdl->register_decl(d, f_ref->m_func_interp);
+        f_ref->m_func_interp->set_else(to_expr(else_val));
+        RETURN_Z3(of_func_interp(f_ref));
+        Z3_CATCH_RETURN(0);        
+    }
+
+    void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_add_const_interp(c, m, f, a);
+        RESET_ERROR_CODE();
+        func_decl* d = to_func_decl(f);
+        model* mdl = to_model_ref(m);
+        mdl->register_decl(d, to_expr(a));
+        Z3_CATCH;
+    }
+
     void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f) {
         Z3_TRY;
         LOG_Z3_func_interp_inc_ref(c, f);
@@ -292,6 +328,24 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) {
+        Z3_TRY;
+        LOG_Z3_add_func_entry(c, fi, args, value);
+        //CHECK_NON_NULL(fi, void);
+        //CHECK_NON_NULL(args, void);
+        //CHECK_NON_NULL(value, void);
+        func_interp* _fi = to_func_interp_ref(fi);
+        expr* _value = to_expr(value);
+        if (to_ast_vector_ref(args).size() != _fi->get_arity()) {
+            SET_ERROR_CODE(Z3_IOB);
+            return;
+        }
+        // check sorts of value
+        expr* const* _args = (expr* const*) to_ast_vector_ref(args).c_ptr();
+        _fi->insert_entry(_args, _value);
+        Z3_CATCH;
+    }
+
     void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e) {
         Z3_TRY;
         LOG_Z3_func_entry_inc_ref(c, e);

src/api/c++/z3++.h

@@ -1731,6 +1731,10 @@ namespace z3 {
         expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }
         unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }
         func_entry entry(unsigned i) const { Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }
+        void add_entry(expr_vector const& args, expr& value) {
+            Z3_add_func_entry(ctx(), m_interp, args, value);
+            check_error();
+        }
     };
 
     class model : public object {
@@ -1740,6 +1744,7 @@ namespace z3 {
             Z3_model_inc_ref(ctx(), m);
         }
     public:
+        model(context & c):object(c) { init(Z3_mk_model(c)); }
         model(context & c, Z3_model m):object(c) { init(m); }
         model(model const & s):object(s) { init(s.m_model); }
         ~model() { Z3_model_dec_ref(ctx(), m_model); }
@@ -1795,6 +1800,17 @@ namespace z3 {
             return 0 != Z3_model_has_interp(ctx(), m_model, f);
         }
 
+        func_interp add_func_interp(func_decl& f, expr& else_val) {
+            Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
+            check_error();
+            return func_interp(ctx(), r);
+        }
+
+        void add_const_interp(func_decl& f, expr& value) {
+            Z3_add_const_interp(ctx(), m_model, f, value);
+            check_error();
+        }
+
         friend std::ostream & operator<<(std::ostream & out, model const & m);
     };
     inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; }

src/api/z3_api.h

@@ -4680,6 +4680,14 @@ extern "C" {
 
     /** @name Models */
     /*@{*/
+
+    /**
+       \brief Create a fresh model object. It has reference count 0.
+
+       def_API('Z3_mk_model', MODEL, (_in(CONTEXT),))
+    */
+    Z3_model Z3_API Z3_mk_model(Z3_context c);
+
     /**
        \brief Increment the reference counter of the given model.
 
@@ -4850,6 +4858,21 @@ extern "C" {
     */
     Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a);
 
+    /**
+       \brief Create a fresh func_interp object, add it to a model for a specified function. 
+       It has reference count 0.       
+
+       def_API('Z3_add_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST)))
+    */
+    Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast else_val);
+
+    /**
+       \brief Add a constant interpretation.
+
+       def_API('Z3_add_const_interp', VOID, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST)))
+     */
+    void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a);
+
     /**
        \brief Increment the reference counter of the given Z3_func_interp object.
 
@@ -4904,6 +4927,13 @@ extern "C" {
     */
     unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f);
 
+    /**
+       \brief add a function entry to a function interpretation.
+
+       def_API('Z3_add_func_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST)))
+     */
+    void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
+
     /**
        \brief Increment the reference counter of the given Z3_func_entry object.