move value factories to model

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

src/model/CMakeLists.txt

@@ -1,5 +1,7 @@
 z3_add_component(model
   SOURCES
+    array_factory.cpp
+    datatype_factory.cpp
     func_interp.cpp
     model2expr.cpp
     model_core.cpp
@@ -9,6 +11,9 @@ z3_add_component(model
     model_pp.cpp
     model_smt2_pp.cpp
     model_v2_pp.cpp
+    numeral_factory.cpp
+    struct_factory.cpp
+    value_factory.cpp
   COMPONENT_DEPENDENCIES
     rewriter
   PYG_FILES

src/smt/proto_model/array_factory.cpp → src/model/array_factory.cpp

@@ -20,8 +20,8 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "model/func_interp.h"
-#include "smt/proto_model/array_factory.h"
-#include "smt/proto_model/proto_model.h"
+#include "model/model_core.h"
+#include "model/array_factory.h"
 
 func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) {
     ptr_buffer<sort> domain;
@@ -33,7 +33,7 @@ func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) {
     return m.mk_fresh_func_decl(symbol::null, symbol::null, arity, domain.c_ptr(), range);
 }
 
-array_factory::array_factory(ast_manager & m, proto_model & md):
+array_factory::array_factory(ast_manager & m, model_core & md):
     struct_factory(m, m.mk_family_id("array"), md) {
 }
 
@@ -67,13 +67,7 @@ expr * array_factory::get_some_value(sort * s) {
         return *(set->begin());
     func_interp * fi;
     expr * val = mk_array_interp(s, fi);
-#if 0
-    ptr_buffer<expr> args;
-    get_some_args_for(s, args);
-    fi->insert_entry(args.c_ptr(), m_model.get_some_value(get_array_range(s)));
-#else
     fi->set_else(m_model.get_some_value(get_array_range(s)));
-#endif
     return val;
 }
 
@@ -147,13 +141,7 @@ expr * array_factory::get_fresh_value(sort * s) {
         // easy case
         func_interp * fi;
         expr * val = mk_array_interp(s, fi);
-#if 0
-        ptr_buffer<expr> args;
-        get_some_args_for(s, args);
-        fi->insert_entry(args.c_ptr(), range_val);
-#else
         fi->set_else(range_val);
-#endif
         return val;
     }
     else {

src/smt/proto_model/array_factory.h → src/model/array_factory.h

@@ -19,7 +19,7 @@ Revision History:
 #ifndef ARRAY_FACTORY_H_
 #define ARRAY_FACTORY_H_
 
-#include "smt/proto_model/struct_factory.h"
+#include "model/struct_factory.h"
 
 class func_interp;
 
@@ -30,7 +30,7 @@ class array_factory : public struct_factory {
     void get_some_args_for(sort * s, ptr_buffer<expr> & args);
     bool mk_two_diff_values_for(sort * s);
 public:
-    array_factory(ast_manager & m, proto_model & md);
+    array_factory(ast_manager & m, model_core & md);
 
     ~array_factory() override {}
 

src/smt/proto_model/datatype_factory.cpp → src/model/datatype_factory.cpp

@@ -16,12 +16,12 @@ Module Name:
 Revision History:
 
 --*/
-#include "smt/proto_model/datatype_factory.h"
-#include "smt/proto_model/proto_model.h"
+#include "model/datatype_factory.h"
+#include "model/model_core.h"
 #include "ast/ast_pp.h"
 #include "ast/expr_functors.h"
 
-datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
+datatype_factory::datatype_factory(ast_manager & m, model_core & md):
     struct_factory(m, m.mk_family_id("datatype"), md),
     m_util(m) {
 }

src/smt/proto_model/datatype_factory.h → src/model/datatype_factory.h

@@ -19,7 +19,7 @@ Revision History:
 #ifndef DATATYPE_FACTORY_H_
 #define DATATYPE_FACTORY_H_
 
-#include "smt/proto_model/struct_factory.h"
+#include "model/struct_factory.h"
 #include "ast/datatype_decl_plugin.h"
 
 class datatype_factory : public struct_factory {
@@ -32,7 +32,7 @@ class datatype_factory : public struct_factory {
     bool is_subterm_of_last_value(app* e);
 
 public:
-    datatype_factory(ast_manager & m, proto_model & md);
+    datatype_factory(ast_manager & m, model_core & md);
     ~datatype_factory() override {}
     expr * get_some_value(sort * s) override;
     expr * get_fresh_value(sort * s) override;

src/model/model.cpp

@@ -98,14 +98,25 @@ struct model::value_proc : public some_value_proc {
                 return u->get(0);
         }
         return nullptr;
-    }
+    }    
 };
 
 expr * model::get_some_value(sort * s) {
     value_proc p(*this);
     return m.get_some_value(s, &p);
 }
 
+expr * model::get_fresh_value(sort * s) {
+    value_proc p(*this);
+    return m.get_some_value(s, &p);
+}
+
+bool model::get_some_values(sort * s, expr_ref& v1, expr_ref& v2) {
+    v1 = get_some_value(s);
+    v2 = get_some_value(s);
+    return true;
+}
+
 ptr_vector<expr> const & model::get_universe(sort * s) const {
     ptr_vector<expr> * u = nullptr;
     m_usort2universe.find(s, u);

src/model/model.h

@@ -66,6 +66,9 @@ class model : public model_core {
     bool eval_expr(expr * e, expr_ref & result, bool model_completion = false);
 
     expr * get_some_value(sort * s) override;
+    expr * get_fresh_value(sort * s) override;
+    bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override;
+
     ptr_vector<expr> const & get_universe(sort * s) const override;
     unsigned get_num_uninterpreted_sorts() const override;
     sort * get_uninterpreted_sort(unsigned idx) const override;

src/model/model_core.h

@@ -71,6 +71,8 @@ class model_core {
     void unregister_decl(func_decl * d);
 
     virtual expr * get_some_value(sort * s) = 0;
+    virtual expr * get_fresh_value(sort * s) = 0;
+    virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;
 
     expr * get_some_const_interp(func_decl * d) { 
         expr * r = get_const_interp(d); 

src/smt/proto_model/numeral_factory.cpp → src/model/numeral_factory.cpp

@@ -16,8 +16,8 @@ Module Name:
 Revision History:
 
 --*/
-#include "smt/proto_model/numeral_factory.h"
 #include "ast/ast_pp.h"
+#include "model/numeral_factory.h"
 
 app * arith_factory::mk_value_core(rational const & val, sort * s) {
     return m_util.mk_numeral(val, s);

src/smt/proto_model/numeral_factory.h → src/model/numeral_factory.h

@@ -19,9 +19,9 @@ Revision History:
 #ifndef NUMERAL_FACTORY_H_
 #define NUMERAL_FACTORY_H_
 
-#include "smt/proto_model/value_factory.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
+#include "model/value_factory.h"
 
 class numeral_factory : public simple_factory<rational> {
 public:

src/smt/proto_model/struct_factory.cpp → src/model/struct_factory.cpp

@@ -16,8 +16,8 @@ Module Name:
 Revision History:
 
 --*/
-#include "smt/proto_model/struct_factory.h"
-#include "smt/proto_model/proto_model.h"
+#include "model/struct_factory.h"
+#include "model/model_core.h"
 
 struct_factory::value_set * struct_factory::get_value_set(sort * s) {
     value_set * set = nullptr;
@@ -31,7 +31,7 @@ struct_factory::value_set * struct_factory::get_value_set(sort * s) {
     return set;
 }
 
-struct_factory::struct_factory(ast_manager & m, family_id fid, proto_model & md):
+struct_factory::struct_factory(ast_manager & m, family_id fid, model_core & md):
     value_factory(m, fid),
     m_model(md),
     m_values(m),

src/smt/proto_model/struct_factory.h → src/model/struct_factory.h

@@ -19,10 +19,10 @@ Revision History:
 #ifndef STRUCT_FACTORY_H_
 #define STRUCT_FACTORY_H_
 
-#include "smt/proto_model/value_factory.h"
+#include "model/value_factory.h"
 #include "util/obj_hashtable.h"
 
-class proto_model;
+class model_core;
 
 /**
    \brief Abstract factory for structured values such as: arrays and algebraic datatypes.
@@ -32,7 +32,7 @@ class struct_factory : public value_factory {
     typedef obj_hashtable<expr> value_set;
     typedef obj_map<sort, value_set *> sort2value_set;
 
-    proto_model &         m_model;
+    model_core &          m_model;
     sort2value_set        m_sort2value_set;
     expr_ref_vector       m_values;
     sort_ref_vector       m_sorts;
@@ -41,7 +41,7 @@ class struct_factory : public value_factory {
     value_set * get_value_set(sort * s);
 
 public:
-    struct_factory(ast_manager & m, family_id fid, proto_model & md);
+    struct_factory(ast_manager & m, family_id fid, model_core & md);
 
     ~struct_factory() override;
 

src/smt/proto_model/value_factory.cpp → src/model/value_factory.cpp

@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "smt/proto_model/value_factory.h"
+#include "model/value_factory.h"
 
 value_factory::value_factory(ast_manager & m, family_id fid):
     m_manager(m), 

src/sat/tactic/goal2sat.cpp

@@ -29,6 +29,7 @@ Module Name:
 #include "util/ref_util.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/ast_util.h"
 #include "ast/for_each_expr.h"
@@ -142,7 +143,7 @@ struct goal2sat::imp {
                 sat::bool_var v = m_solver.add_var(ext);
                 m_map.insert(t, v);
                 l = sat::literal(v, sign);
-                TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
+                TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << "\n";);
                 if (ext && !is_uninterp_const(t)) {
                     m_interpreted_atoms.push_back(t);
                 }
@@ -228,7 +229,7 @@ struct goal2sat::imp {
     }
 
     void convert_or(app * t, bool root, bool sign) {
-        TRACE("goal2sat", tout << "convert_or:\n" << mk_ismt2_pp(t, m) << "\n";);
+        TRACE("goal2sat", tout << "convert_or:\n" << mk_bounded_pp(t, m, 2) << "\n";);
         unsigned num = t->get_num_args();
         if (root) {
             SASSERT(num == m_result_stack.size());
@@ -348,7 +349,7 @@ struct goal2sat::imp {
     }
 
     void convert_iff2(app * t, bool root, bool sign) {
-        TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_ismt2_pp(t, m) << "\n";);
+        TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";);
         unsigned sz = m_result_stack.size();
         SASSERT(sz >= 2);
         sat::literal  l1 = m_result_stack[sz-1];
@@ -381,7 +382,7 @@ struct goal2sat::imp {
     }
 
     void convert_iff(app * t, bool root, bool sign) {
-        TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_ismt2_pp(t, m) << "\n";);
+        TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_bounded_pp(t, m, 2) << "\n";);
         unsigned sz = m_result_stack.size();
         unsigned num = get_num_args(t);
         SASSERT(sz >= num && num >= 2);
@@ -512,7 +513,6 @@ struct goal2sat::imp {
     }
 
     void convert_pb_eq(app* t, bool root, bool sign) {
-        //IF_VERBOSE(0, verbose_stream() << "pbeq: " << mk_pp(t, m) << "\n";);
         rational k = pb.get_k(t);
         SASSERT(k.is_unsigned());
         svector<wliteral> wlits;
@@ -741,7 +741,7 @@ struct goal2sat::imp {
 
     void process(expr * n) {
         //SASSERT(m_result_stack.empty());
-        TRACE("goal2sat", tout << "converting: " << mk_ismt2_pp(n, m) << "\n";);
+        TRACE("goal2sat", tout << "converting: " << mk_bounded_pp(n, m, 2) << "\n";);
         if (visit(n, true, false)) {
             SASSERT(m_result_stack.empty());
             return;
@@ -839,7 +839,7 @@ struct goal2sat::imp {
                 }                
                 f = m.mk_or(fmls.size(), fmls.c_ptr());
             }
-            TRACE("goal2sat", tout << f << "\n";);
+            TRACE("goal2sat", tout << mk_bounded_pp(f, m, 2) << "\n";);
             process(f);
         skip_dep:
             ;

src/smt/proto_model/CMakeLists.txt

@@ -1,11 +1,6 @@
 z3_add_component(proto_model
   SOURCES
-    array_factory.cpp
-    datatype_factory.cpp
-    numeral_factory.cpp
     proto_model.cpp
-    struct_factory.cpp
-    value_factory.cpp
   COMPONENT_DEPENDENCIES
     model
     rewriter