From 7da3854a8b488188641b4b8c2d691e5d59df1df8 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 28 Sep 2015 01:56:13 -0400
Subject: [PATCH] really lousy model-building, WIP

---
 src/smt/theory_str.cpp | 46 ++++++++++++++++++++++++++++--------------
 src/smt/theory_str.h   | 23 ++++++++++++++++++++-
 2 files changed, 53 insertions(+), 16 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index bba37f5f0..aaae3e373 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -35,18 +35,9 @@ theory_str::~theory_str() {
 }
 
 void theory_str::assert_axiom(ast * a) {
-    /*
-    if (search_started) {
-        // effectively Z3_theory_assert_axiom
-        NOT_IMPLEMENTED_YET();
-    } else {
-        // effectively Z3_assert_cnstr
-        context & ctx = get_context();
-        ctx.assert_expr(to_expr(a));
-    }
-    */
-    TRACE("t_str_detail", tout << "asserting " << mk_ismt2_pp(a, get_manager()) << "\n";);
     expr * e = to_expr(a);
+    if (get_manager().is_true(e)) return;
+    TRACE("t_str_detail", tout << "asserting " << mk_ismt2_pp(a, get_manager()) << "\n";);
     context & ctx = get_context();
     ctx.internalize(e, false);
     literal lit(ctx.get_literal(e));
@@ -381,11 +372,11 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
         if (const_str == "") {
             TRACE("t_str", tout << "quick path: concat == \"\"" << std::endl;);
             // assert the following axiom:
-            // ( (Concat a1 a2) == str ) -> ( (a1 == "") AND (a2 == "") )
-            expr_ref premise(m.mk_eq(concat, str), m);
+            // ( (Concat a1 a2) == "" ) -> ( (a1 == "") AND (a2 == "") )
             expr_ref empty_str(m_strutil.mk_string(""), m);
-            expr_ref c1(m.mk_eq(a1, empty_str), m);
-            expr_ref c2(m.mk_eq(a2, empty_str), m);
+            expr_ref premise(ctx.mk_eq_atom(concat, empty_str), m);
+            expr_ref c1(ctx.mk_eq_atom(a1, empty_str), m);
+            expr_ref c2(ctx.mk_eq_atom(a2, empty_str), m);
             expr_ref conclusion(m.mk_and(c1, c2), m);
             expr_ref axiom(m.mk_implies(premise, conclusion), m);
             TRACE("t_str_detail", tout << "learn " << mk_ismt2_pp(axiom, m) << std::endl;);
@@ -643,4 +634,29 @@ final_check_status theory_str::final_check_eh() {
     return FC_DONE;
 }
 
+void theory_str::init_model(model_generator & mg) {
+    TRACE("t_str", tout << "initializing model" << std::endl; display(tout););
+    m_factory = alloc(str_value_factory, get_manager(), get_family_id());
+    mg.register_factory(m_factory);
+}
+
+model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) {
+    TRACE("t_str", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
+                                " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
+    ast_manager & m = get_manager();
+    context & ctx = get_context();
+    app_ref owner(m);
+    owner = n->get_owner();
+
+    // If the owner is not internalized, it doesn't have an enode associated.
+    SASSERT(ctx.e_internalized(owner));
+
+    if (m_strutil.is_string(owner)) {
+        return alloc(expr_wrapper_proc, owner);
+    }
+    NOT_IMPLEMENTED_YET(); // TODO
+}
+
+void theory_str::finalize_model(model_generator & mg) {}
+
 }; /* namespace smt */
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 76bef4561..65a401580 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -28,7 +28,22 @@ Revision History:
 namespace smt {
 
     class str_value_factory : public value_factory {
-        // TODO
+        str_util m_util;
+    public:
+        str_value_factory(ast_manager & m, family_id fid) :
+            value_factory(m, fid),
+            m_util(m) {}
+        virtual ~str_value_factory() {}
+        virtual expr * get_some_value(sort * s) {
+            return m_util.mk_string("some value");
+        }
+        virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
+            v1 = m_util.mk_string("value 1");
+            v2 = m_util.mk_string("value 2");
+            return true;
+        }
+        virtual expr * get_fresh_value(sort * s) { NOT_IMPLEMENTED_YET(); }
+        virtual void register_value(expr * n) { /* Ignore */ }
     };
 
     class theory_str : public theory {
@@ -38,6 +53,8 @@ namespace smt {
         arith_util m_autil;
         str_util m_strutil;
 
+        str_value_factory * m_factory;
+
         ptr_vector<enode> m_basicstr_axiom_todo;
         svector<std::pair<enode*,enode*> > m_str_eq_todo;
     protected:
@@ -83,6 +100,10 @@ namespace smt {
 
         virtual final_check_status final_check_eh();
         void attach_new_th_var(enode * n);
+
+        virtual void init_model(model_generator & m);
+        virtual model_value_proc * mk_value(enode * n, model_generator & mg);
+        virtual void finalize_model(model_generator & mg);
     };
 
 };