Thread labels through tactic system

src/tactic/filter_model_converter.cpp

@@ -51,6 +51,9 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx
     TRACE("filter_mc", tout << "after filter_model_converter\n"; model_v2_pp(tout, *old_model););
 }
 
+void filter_model_converter::operator()(svector<symbol> & labels, unsigned goal_idx) {
+}
+
 void filter_model_converter::display(std::ostream & out) {
     out << "(filter-model-converter";
     for (unsigned i = 0; i < m_decls.size(); i++) {

src/tactic/filter_model_converter.h

@@ -32,6 +32,8 @@ public:
     
     virtual void operator()(model_ref & md, unsigned goal_idx);
 
+    virtual void operator()(svector<symbol> & labels, unsigned goal_idx);
+    
     virtual void operator()(model_ref & md) { operator()(md, 0); } // TODO: delete
 
     virtual void cancel() {}

src/tactic/model_converter.cpp

@@ -33,6 +33,12 @@ public:
         this->m_c1->operator()(m, 0);
     }
 
+    virtual void operator()(svector<symbol> & r, unsigned goal_idx) {
+        this->m_c2->operator()(r, goal_idx);
+        this->m_c1->operator()(r, 0);
+    }
+
+  
     virtual char const * get_name() const { return "concat-model-converter"; }
 
     virtual model_converter * translate(ast_translation & translator) {
@@ -76,6 +82,24 @@ public:
         }
         UNREACHABLE();
     }
+
+    virtual void operator()(svector<symbol> & r, unsigned goal_idx) {
+        unsigned num = this->m_c2s.size();
+        for (unsigned i = 0; i < num; i++) {
+            if (goal_idx < this->m_szs[i]) {
+                // found the model converter that should be used
+                model_converter * c2 = this->m_c2s[i];
+                if (c2)
+                  c2->operator()(r, goal_idx);
+                if (m_c1)
+                  this->m_c1->operator()(r, i);
+                return;
+            }
+            // invalid goal
+            goal_idx -= this->m_szs[i];
+        }
+        UNREACHABLE();
+    }
     
     virtual char const * get_name() const { return "concat-star-model-converter"; }
 
@@ -102,8 +126,12 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter *
 
 class model2mc : public model_converter {
     model_ref m_model;
+    buffer<symbol> m_labels;
 public:
     model2mc(model * m):m_model(m) {}
+
+    model2mc(model * m, buffer<symbol> r):m_model(m), m_labels(r) {}
+
     virtual ~model2mc() {}
 
     virtual void operator()(model_ref & m) {
@@ -114,7 +142,11 @@ public:
         m = m_model;
     }
 
-    virtual void cancel() {
+    virtual void operator()(svector<symbol> & r, unsigned goal_idx) {
+      r.append(m_labels.size(), m_labels.c_ptr());
+    }
+
+  virtual void cancel() {
     }
     
     virtual void display(std::ostream & out) {
@@ -135,6 +167,12 @@ model_converter * model2model_converter(model * m) {
     return alloc(model2mc, m);
 }
 
+model_converter * model_and_labels2model_converter(model * m, buffer<symbol> & r) {
+    if (m == 0)
+        return 0;
+    return alloc(model2mc, m, r);
+}
+
 void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) {
     if (mc) {
         m = alloc(model, mng);

src/tactic/model_converter.h

@@ -32,6 +32,8 @@ public:
         SASSERT(goal_idx == 0);
         operator()(m);
     }
+
+    virtual void operator()(svector<symbol> & r, unsigned goal_idx) {}
     
     virtual model_converter * translate(ast_translation & translator) = 0;
 };
@@ -49,6 +51,8 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter *
 
 model_converter * model2model_converter(model * m);
 
+model_converter * model_and_labels2model_converter(model * m, buffer<symbol> &r);
+
 void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m);
 
 void apply(model_converter_ref & mc, model_ref & m, unsigned gidx);

src/tactic/tactic.cpp

@@ -174,7 +174,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve
     }
 }
 
-lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector<symbol> & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
     bool models_enabled = g->models_enabled();
     bool proofs_enabled = g->proofs_enabled();
     bool cores_enabled  = g->unsat_core_enabled();
@@ -199,6 +199,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d
 
     if (is_decided_sat(r)) {
         if (models_enabled) {
+            (*mc)(labels, 0);
             model_converter2model(m, mc.get(), md);
             if (!md) {
                 // create empty model.
@@ -215,7 +216,10 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d
         return l_false;
     }
     else {
-        if (models_enabled) model_converter2model(m, mc.get(), md);
+        if (models_enabled) {
+          model_converter2model(m, mc.get(), md);
+          (*mc)(labels, 0);
+        }
         reason_unknown = "incomplete";
         return l_undef;
     }

src/tactic/tactic.h

@@ -153,7 +153,7 @@ public:
 #define MK_SIMPLE_TACTIC_FACTORY(NAME, ST)  MK_TACTIC_FACTORY(NAME, return ST;)
 
 void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
-lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, svector<symbol> & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
 
 // Throws an exception if goal \c in requires proof generation.
 void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);