Merge pull request #881 from dwoos/tactic-labels

Thread labels through tactic system

src/cmd_context/tactic_cmds.cpp

@@ -165,7 +165,21 @@ public:
     }
 };
 
-typedef simple_check_sat_result check_sat_tactic_result;
+struct check_sat_tactic_result : public simple_check_sat_result {
+public:
+  labels_vec labels;
+
+  check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) {
+  }
+
+  virtual void get_labels(svector<symbol> & r) {
+    r.append(labels);
+  }
+
+  virtual void add_labels(svector<symbol> & r) {
+    labels.append(r);
+  }
+};
 
 class check_sat_using_tactict_cmd : public exec_given_tactic_cmd {
 public:
@@ -189,6 +203,7 @@ public:
         ast_manager & m = ctx.m();
         unsigned timeout   = p.get_uint("timeout", ctx.params().m_timeout);
         unsigned rlimit  =   p.get_uint("rlimit", ctx.params().m_rlimit);
+        labels_vec labels;
         goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
         assert_exprs_from(ctx, *g);
         TRACE("check_sat_using", g->display(tout););
@@ -208,7 +223,7 @@ public:
                 cmd_context::scoped_watch sw(ctx);
                 lbool r = l_undef;
                 try {
-                    r = check_sat(t, g, md, pr, core, reason_unknown);
+                    r = check_sat(t, g, md, result->labels, pr, core, reason_unknown);
                     ctx.display_sat_result(r);
                     result->set_status(r);
                     if (r == l_undef) {

src/smt/tactic/smt_tactic.cpp

@@ -204,7 +204,9 @@ public:
                 if (in->models_enabled()) {
                     model_ref md;
                     m_ctx->get_model(md);
-                    mc = model2model_converter(md.get());
+                    buffer<symbol> r;
+                    m_ctx->get_relevant_labels(0, r);
+                    mc = model_and_labels2model_converter(md.get(), r);
                     mc = concat(fmc.get(), mc.get());
                 }
                 return;
@@ -251,7 +253,9 @@ public:
                         if (in->models_enabled()) {
                             model_ref md;
                             m_ctx->get_model(md);
-                            mc = model2model_converter(md.get());
+                            buffer<symbol> r;
+                            m_ctx->get_relevant_labels(0, r);
+                            mc = model_and_labels2model_converter(md.get(), r);
                         }
                         return;
                     default:

src/solver/tactic2solver.cpp

@@ -146,8 +146,9 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
     proof_ref           pr(m);
     expr_dependency_ref core(m);
     std::string         reason_unknown = "unknown";
+    labels_vec labels;
     try {
-        switch (::check_sat(*m_tactic, g, md, pr, core, reason_unknown)) {
+        switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) {
         case l_true: 
             m_result->set_status(l_true);
             break;

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()(labels_vec & 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) {
@@ -77,6 +83,24 @@ public:
         UNREACHABLE();
     }
 
+    virtual void operator()(labels_vec & 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"; }
 
     virtual model_converter * translate(ast_translation & translator) {
@@ -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> const & r):m_model(m), m_labels(r) {}
+
     virtual ~model2mc() {}
 
     virtual void operator()(model_ref & m) {
@@ -114,6 +142,10 @@ public:
         m = m_model;
     }
 
+    virtual void operator()(labels_vec & r, unsigned goal_idx) {
+      r.append(m_labels.size(), m_labels.c_ptr());
+    }
+
   virtual void cancel() {
     }
     
@@ -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

@@ -23,6 +23,8 @@ Notes:
 #include"converter.h"
 #include"ref.h"
 
+class labels_vec : public svector<symbol> {};
+
 class model_converter : public converter {
 public:
     virtual void operator()(model_ref & m) {}  // TODO: delete
@@ -33,6 +35,8 @@ public:
         operator()(m);
     }
 
+    virtual void operator()(labels_vec & r, unsigned goal_idx) {}
+    
     virtual model_converter * translate(ast_translation & translator) = 0;
 };
 
@@ -49,6 +53,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

@@ -175,7 +175,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, labels_vec & 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();
@@ -200,6 +200,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.
@@ -216,7 +217,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, labels_vec & 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);