Merge pull request #1693 from NikolajBjorner/master

fix #1675

src/tactic/generic_model_converter.cpp

@@ -114,11 +114,16 @@ model_converter * generic_model_converter::translate(ast_translation & translato
     return res;
 }
 
-void generic_model_converter::collect(ast_pp_util& visitor) { 
-    m_env = &visitor.env(); 
-    for (entry const& e : m_entries) {
-        visitor.coll.visit_func(e.m_f);
-        if (e.m_def) visitor.coll.visit(e.m_def);
+void generic_model_converter::set_env(ast_pp_util* visitor) { 
+    if (!visitor) {
+        m_env = nullptr;
+    }
+    else {
+        m_env = &visitor->env();       
+        for (entry const& e : m_entries) {
+            visitor->coll.visit_func(e.m_f);
+            if (e.m_def) visitor->coll.visit(e.m_def);
+        }
     }
 }
 

src/tactic/generic_model_converter.h

@@ -68,7 +68,7 @@ public:
 
     model_converter * translate(ast_translation & translator) override;
 
-    void collect(ast_pp_util& visitor) override;
+    void set_env(ast_pp_util* visitor) override;
 
     void operator()(expr_ref& fml) override; 
 

src/tactic/horn_subsume_model_converter.cpp

@@ -195,8 +195,7 @@ void horn_subsume_model_converter::operator()(model_ref& mr) {
         SASSERT(m.is_bool(body));
                 
         TRACE("mc", tout << "eval: " << h->get_name() << "\n" << body << "\n";);
-        expr_ref tmp(body);
-        mr->eval(tmp, body);
+        body = (*mr)(body);
         
         TRACE("mc", tout << "to:\n" << body << "\n";);
                 

src/tactic/model_converter.cpp

@@ -43,6 +43,16 @@ void model_converter::display_del(std::ostream& out, func_decl* f) const {
     }
 }
 
+void model_converter::set_env(ast_pp_util* visitor) {
+    if (visitor) {
+        m_env = &visitor->env();
+    }
+    else {
+        m_env = nullptr;
+    }
+}
+
+
 void model_converter::display_add(std::ostream& out, ast_manager& m) {
     // default printer for converter that adds entries
     model_ref mdl = alloc(model, m);
@@ -91,9 +101,9 @@ public:
         return this->translate_core<concat_model_converter>(translator);
     }
 
-    void collect(ast_pp_util& visitor) override { 
-        this->m_c1->collect(visitor);
-        this->m_c2->collect(visitor);
+    void set_env(ast_pp_util* visitor) override {
+        this->m_c1->set_env(visitor);
+        this->m_c2->set_env(visitor);
     }
 };
 
@@ -125,9 +135,8 @@ public:
     }
 
     void operator()(expr_ref& fml) override {
-        expr_ref r(m_model->get_manager());
-        m_model->eval(fml, r, false);
-        fml = r;
+        model::scoped_model_completion _scm(m_model, false);
+        fml = (*m_model)(fml);
     }
 
     void get_units(obj_map<expr, bool>& fmls) override {

src/tactic/model_converter.h

@@ -80,7 +80,7 @@ public:
     
     virtual model_converter * translate(ast_translation & translator) = 0;
     
-    virtual void collect(ast_pp_util& visitor) { m_env = &visitor.env(); }
+    virtual void set_env(ast_pp_util* visitor);
 
     /**
        \brief we are adding a formula to the context of the model converter.

src/tactic/sls/sls_engine.cpp

@@ -100,36 +100,27 @@ void sls_engine::checkpoint() {
 }
 
 bool sls_engine::full_eval(model & mdl) {
-    bool res = true;
-
-    unsigned sz = m_assertions.size();
-    for (unsigned i = 0; i < sz && res; i++) {
-        checkpoint();
-        expr_ref o(m_manager);
-
-        if (!mdl.eval(m_assertions[i], o, true))
-            exit(ERR_INTERNAL_FATAL);
-
-        res = m_manager.is_true(o.get());
-    }
-
-    TRACE("sls", tout << "Evaluation: " << res << std::endl;);
-
-    return res;
+    model::scoped_model_completion _scm(mdl, true);
+    for (expr* a : m_assertions) {
+        checkpoint();        
+        if (!mdl.is_true(a)) {
+            TRACE("sls", tout << "Evaluation: false\n";);
+            return false;
+        }
+    }    
+    return true;
 }
 
 double sls_engine::top_score() {
     double top_sum = 0.0;
-    unsigned sz = m_assertions.size();
-    for (unsigned i = 0; i < sz; i++) {
-        expr * e = m_assertions[i];
+    for (expr* e : m_assertions) {
         top_sum += m_tracker.get_score(e);
     }
 
     TRACE("sls_top", tout << "Score distribution:";
-    for (unsigned i = 0; i < sz; i++)
-        tout << " " << m_tracker.get_score(m_assertions[i]);
-    tout << " AVG: " << top_sum / (double)sz << std::endl;);
+          for (expr* e : m_assertions) 
+              tout << " " << m_tracker.get_score(e);
+          tout << " AVG: " << top_sum / (double)m_assertions.size() << std::endl;);
 
     m_tracker.set_top_sum(top_sum);