extract also units from search state

src/smt/smt_context.cpp

@@ -4613,6 +4613,22 @@ namespace smt {
         return result;
     }
 
+    void context::get_units(expr_ref_vector& result) {
+        expr_mark visited;
+        for (expr* fml : result)
+            visited.mark(fml);
+        for (literal lit : m_assigned_literals) {
+            if (get_assign_level(lit) > m_base_lvl)
+                break;
+            expr_ref e(m);
+            literal2expr(lit, e);
+            if (visited.is_marked(e))
+                continue;
+            result.push_back(std::move(e));
+        }
+    }
+
+
     failure context::get_last_search_failure() const {
         return m_last_search_failure;
     }

src/smt/smt_context.h

@@ -1691,6 +1691,8 @@ namespace smt {
 
         void get_assertions(ptr_vector<expr> & result) { m_asserted_formulas.get_assertions(result); }
 
+        void get_units(expr_ref_vector& result);
+
         /*
          * user-propagator
          */

src/smt/smt_kernel.cpp

@@ -177,6 +177,10 @@ namespace smt {
     void kernel::get_assignments(expr_ref_vector & result) {
         m_imp->m_kernel.get_assignments(result);
     }
+
+    void kernel::get_units(expr_ref_vector & result) {
+        m_imp->m_kernel.get_units(result);
+    }    
         
     void kernel::get_relevant_labels(expr * cnstr, buffer<symbol> & result) {
         m_imp->m_kernel.get_relevant_labels(cnstr, result);
@@ -280,4 +284,4 @@ namespace smt {
         m_imp->m_kernel.user_propagate_register_created(r);
     }
 
-};
+};

src/smt/smt_kernel.h

@@ -202,6 +202,12 @@ namespace smt {
            \brief Return the set of formulas assigned by the kernel.
         */
         void get_assignments(expr_ref_vector & result);
+
+
+        /**
+           \brief Return units assigned by the kernel.
+        */
+        void get_units(expr_ref_vector& result);
         
         /**
            \brief Return the set of relevant labels in the last check command.

src/smt/smt_solver.cpp

@@ -318,6 +318,10 @@ namespace {
             return m_context.get_formula(idx);
         }
 
+        void get_units_core(expr_ref_vector& units) override {
+            m_context.get_units(units);
+        }
+
         expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override {
             ast_manager& m = get_manager();
             if (!m_cuber) {

src/solver/solver.cpp

@@ -242,6 +242,7 @@ expr_ref_vector solver::get_units() {
     ast_manager& m = get_manager();
     expr_ref_vector fmls(m), result(m), tmp(m);
     get_assertions(fmls);
+    get_units_core(fmls);
     obj_map<expr, bool> units;
     for (expr* f : fmls) {
         if (m.is_not(f, f) && is_literal(m, f)) {

src/solver/solver.h

@@ -261,6 +261,8 @@ public:
     */
     expr_ref_vector get_units();
 
+    virtual void get_units_core(expr_ref_vector& units) {} 
+
     expr_ref_vector get_non_units();
 
     virtual expr_ref_vector get_trail() = 0; // { return expr_ref_vector(get_manager()); }