add unit extraction

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ackermannization/ackr_model_converter.cpp

@@ -39,6 +39,8 @@ public:
 
     virtual ~ackr_model_converter() { }
 
+    virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
     virtual void operator()(model_ref & md, unsigned goal_idx) {
         SASSERT(goal_idx == 0);
         SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));

src/ackermannization/lackr_model_converter_lazy.cpp

@@ -43,6 +43,8 @@ public:
         operator()(md, 0);
     }
 
+    virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
     //void display(std::ostream & out);
 
     virtual model_converter * translate(ast_translation & translator) {

src/api/api_solver.cpp

@@ -347,6 +347,22 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+
+    Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s) {
+        Z3_TRY;
+        LOG_Z3_solver_get_units(c, s);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        expr_ref_vector fmls = to_solver_ref(s)->get_units(mk_c(c)->m());
+        for (expr* f : fmls) {
+            v->m_ast_vector.push_back(f);
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+
     static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {
         for (unsigned i = 0; i < num_assumptions; i++) {
             if (!is_expr(to_ast(assumptions[i]))) {

src/api/dotnet/Solver.cs

@@ -265,6 +265,20 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Currently inferred units.
+        /// </summary>
+        public BoolExpr[] Units
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
+
+                ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_units(Context.nCtx, NativeObject));
+                return assertions.ToBoolExprArray();
+            }
+        }
+
         /// <summary>
         /// Checks whether the assertions in the solver are consistent or not.
         /// </summary>

src/api/python/z3/z3.py

@@ -6369,6 +6369,11 @@ class Solver(Z3PPObject):
         """
         return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
 
+    def units(self):
+        """Return an AST vector containing all currently inferred units.
+        """
+        return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
+
     def statistics(self):
         """Return statistics for the last `check()`.
 

src/api/z3_api.h

@@ -6163,6 +6163,13 @@ extern "C" {
     */
     Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
 
+    /**
+       \brief Return the set of units modulo model conversion.
+
+       def_API('Z3_solver_get_units', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
+    */
+    Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
+
     /**
        \brief Check whether the assertions in a given solver are consistent or not.
 

src/muz/base/dl_util.cpp

@@ -387,6 +387,9 @@ namespace datalog {
         void operator()(model_ref&) override {}
 
         void display(std::ostream & out) override { }
+
+        void get_units(obj_map<expr, bool>& units) override {}
+
     };
 
     model_converter* mk_skip_model_converter() { return alloc(skip_model_converter); }

src/muz/transforms/dl_mk_bit_blast.cpp

@@ -63,6 +63,8 @@ namespace datalog {
             return alloc(bit_blast_model_converter, m);
         }
 
+        virtual void get_units(obj_map<expr, bool>& units)  {}
+
         virtual void display(std::ostream& out) { out << "(bit-blast-model-converter)\n"; }
 
         virtual void operator()(model_ref & model) {

src/muz/transforms/dl_mk_karr_invariants.cpp

@@ -120,6 +120,8 @@ namespace datalog {
             }
         }
 
+        virtual void get_units(obj_map<expr, bool>& units) {}
+
         virtual void operator()(model_ref & mr) {
             for (unsigned i = 0; i < m_funcs.size(); ++i) {
                 func_decl* p = m_funcs[i].get();

src/muz/transforms/dl_mk_quantifier_abstraction.cpp

@@ -55,6 +55,8 @@ namespace datalog {
 
         virtual void display(std::ostream& out) { display_add(out, m); }
 
+        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }        
+
         void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector<bool> const& bound) {
             m_old_funcs.push_back(old_p);
             m_new_funcs.push_back(new_p);

src/muz/transforms/dl_mk_scale.cpp

@@ -38,13 +38,13 @@ namespace datalog {
             m_new2old.insert(new_f, old_f);
         }
        
+        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
         virtual void operator()(model_ref& md) {
             model_ref old_model = alloc(model, m);
-            obj_map<func_decl, func_decl*>::iterator it  = m_new2old.begin();
-            obj_map<func_decl, func_decl*>::iterator end = m_new2old.end();
-            for (; it != end; ++it) {
-                func_decl* old_p = it->m_value;
-                func_decl* new_p = it->m_key;
+            for (auto const& kv : m_new2old) {
+                func_decl* old_p = kv.m_value;
+                func_decl* new_p = kv.m_key;
                 func_interp* old_fi = alloc(func_interp, m, old_p->get_arity());
 
                 if (new_p->get_arity() == 0) {

src/muz/transforms/dl_mk_slice.cpp

@@ -308,6 +308,8 @@ namespace datalog {
             m_sliceable.insert(f, bv);
         }
 
+        void get_units(obj_map<expr, bool>& units) override {}
+
         void operator()(model_ref & md) override {
             if (m_slice2old.empty()) {
                 return;

src/sat/tactic/goal2sat.cpp

@@ -981,6 +981,12 @@ void sat2goal::mc::display(std::ostream& out) {
     if (m_gmc) m_gmc->display(out);
 }
 
+void sat2goal::mc::get_units(obj_map<expr, bool>& units) {
+    flush_gmc();
+    if (m_gmc) m_gmc->get_units(units);
+}
+
+
 void sat2goal::mc::operator()(model_ref & md) {
     model_evaluator ev(*md);
     ev.set_model_completion(false);

src/sat/tactic/goal2sat.h

@@ -94,7 +94,7 @@ public:
         model_converter* translate(ast_translation& translator) override;
         void collect(ast_pp_util& visitor) override;
         void display(std::ostream& out) override;
-        
+        void get_units(obj_map<expr, bool>& units) override;
         app* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); }
         expr_ref lit2expr(sat::literal l);
         void insert(sat::bool_var v, app * atom, bool aux);

src/solver/solver.cpp

@@ -211,7 +211,35 @@ void solver::updt_params(params_ref const & p) {
     m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
 }
 
-void solver::hoist_converter(model_converter_ref& mc) {
-    
-}
 
+expr_ref_vector solver::get_units(ast_manager& m) {
+    expr_ref_vector fmls(m), result(m), tmp(m);
+    get_assertions(fmls);
+    obj_map<expr, bool> units;
+    for (expr* f : fmls) {
+        if (m.is_not(f, f) && is_literal(m, f)) {
+            m.inc_ref(f);
+            units.insert(f, false);
+        }
+        else if (is_literal(m, f)) {
+            m.inc_ref(f);
+            units.insert(f, true);
+        }
+    }
+    model_converter_ref mc = get_model_converter();
+    if (mc) {
+        mc->get_units(units);
+    }
+    for (auto const& kv : units) {
+        tmp.push_back(kv.m_key);
+        if (kv.m_value) 
+            result.push_back(kv.m_key); 
+        else 
+            result.push_back(m.mk_not(kv.m_key));
+    }
+    for (expr* e : tmp) {
+        m.dec_ref(e);
+    }
+
+    return result;
+}

src/solver/solver.h

@@ -203,6 +203,11 @@ public:
 
     virtual model_converter_ref get_model_converter() const { return m_mc0; }
 
+    /**
+       \brief extract units from solver.
+    */
+    expr_ref_vector get_units(ast_manager& m);
+
     class scoped_push {
         solver& s;
         bool    m_nopop;
@@ -220,7 +225,6 @@ protected:
 
     bool is_literal(ast_manager& m, expr* e);
 
-    void hoist_converter(model_converter_ref& mc);
 };
 
 typedef ref<solver> solver_ref;

src/tactic/arith/eq2bv_tactic.cpp

@@ -119,6 +119,8 @@ class eq2bv_tactic : public tactic {
             }
         }
 
+        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
     };
 
 public:

src/tactic/arith/fm_tactic.cpp

@@ -180,6 +180,8 @@ class fm_tactic : public tactic {
             m_clauses.back().swap(c);
         }
 
+        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
         virtual void operator()(model_ref & md) {
             TRACE("fm_mc", model_v2_pp(tout, *md); display(tout););
             model_evaluator ev(*(md.get()));

src/tactic/arith/pb2bv_model_converter.cpp

@@ -50,6 +50,10 @@ pb2bv_model_converter::~pb2bv_model_converter() {
     }
 }
 
+void pb2bv_model_converter::get_units(obj_map<expr, bool>& units) { 
+    if (!m_c2bit.empty()) units.reset(); 
+}
+
 
 void pb2bv_model_converter::operator()(model_ref & md) {
     TRACE("pb2bv", tout << "converting model:\n"; model_v2_pp(tout, *md); display(tout););

src/tactic/arith/pb2bv_model_converter.h

@@ -33,6 +33,7 @@ public:
     virtual ~pb2bv_model_converter();
     void operator()(model_ref & md) override;
     void display(std::ostream & out) override;
+    void get_units(obj_map<expr, bool>& units) override;
     model_converter * translate(ast_translation & translator) override;
 };
 

src/tactic/bv/bit_blaster_model_converter.cpp

@@ -206,6 +206,10 @@ struct bit_blaster_model_converter : public model_converter {
         }
     }
 
+    void get_units(obj_map<expr, bool>& units) override {
+        // no-op
+    }
+
 protected:
     bit_blaster_model_converter(ast_manager & m):m_vars(m), m_bits(m) { }
 public:

src/tactic/core/pb_preprocess_tactic.cpp

@@ -33,60 +33,13 @@ Notes:
 --*/
 #include "tactic/core/pb_preprocess_tactic.h"
 #include "tactic/tactical.h"
+#include "tactic/generic_model_converter.h"
 #include "ast/for_each_expr.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/expr_substitution.h"
 #include "ast/ast_pp.h"
 
-class pb_preproc_model_converter : public model_converter {
-    ast_manager& m;
-    pb_util      pb;
-    expr_ref_vector                  m_refs;
-    svector<std::pair<app*, expr*> > m_const;
-
-public:
-    pb_preproc_model_converter(ast_manager& m):m(m), pb(m), m_refs(m) {}
-
-    virtual void operator()(model_ref & mdl) {
-        for (auto const& kv : m_const) {
-            mdl->register_decl(kv.first->get_decl(), kv.second);
-        }
-    }
-
-    void set_value(expr* e, bool p) {
-        while (m.is_not(e, e)) {
-            p = !p;
-        }
-        SASSERT(is_app(e));
-        set_value_p(to_app(e), p?m.mk_true():m.mk_false());        
-    }
-
-    virtual model_converter * translate(ast_translation & translator) {
-        pb_preproc_model_converter* mc = alloc(pb_preproc_model_converter, translator.to());
-        for (auto const& kv : m_const) {
-            mc->set_value_p(translator(kv.first), translator(kv.second));
-        }
-        return mc;
-    }
-
-    virtual void display(std::ostream & out) {
-        for (auto const& kv : m_const) {
-            out << "(model-set " << mk_pp(kv.first, m) << " " << mk_pp(kv.second, m) << ")\n";
-        }
-    }
-
-private:
-    void set_value_p(app* e, expr* v) {
-        SASSERT(e->get_num_args() == 0);  
-        SASSERT(is_uninterp_const(e));
-        m_const.push_back(std::make_pair(e, v));
-        m_refs.push_back(e);
-        m_refs.push_back(v);
-    }
-
-};
-
 class pb_preprocess_tactic : public tactic {
     struct rec { unsigned_vector pos, neg; rec() { } };
     typedef obj_map<app, rec> var_map;
@@ -119,24 +72,31 @@ class pb_preprocess_tactic : public tactic {
         for (unsigned i = 0; i < m_other.size(); ++i) {
             out << "ot " << m_other[i] << ": " << mk_pp(g->form(m_other[i]), m) << "\n";
         }
-                
-        var_map::iterator it  = m_vars.begin();
-        var_map::iterator end = m_vars.end();
-        for (; it != end; ++it) {
-            app* e = it->m_key;
-            unsigned_vector const& pos = it->m_value.pos;
-            unsigned_vector const& neg = it->m_value.neg;
+         
+        for (auto const& kv : m_vars) {
+            app* e = kv.m_key;
+            unsigned_vector const& pos = kv.m_value.pos;
+            unsigned_vector const& neg = kv.m_value.neg;
             out << mk_pp(e, m) << ": ";
-            for (unsigned i = 0; i < pos.size(); ++i) {
-                out << "p: " << pos[i] << " ";
+            for (unsigned p : pos) {
+                out << "p: " << p << " ";
             }
-            for (unsigned i = 0; i < neg.size(); ++i) {
-                out << "n: " << neg[i] << " ";
+            for (unsigned n : neg) {
+                out << "n: " << n << " ";
             }
             out << "\n";
         }
     }
 
+    void set_value(generic_model_converter& mc, expr* e, bool p) {
+        while (m.is_not(e, e)) {
+            p = !p;
+        }
+        SASSERT(is_app(e));
+        mc.add(to_app(e), p?m.mk_true():m.mk_false());        
+    }
+
+
 public:
     pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): 
         m(m), pb(m), m_r(m) {}
@@ -156,7 +116,7 @@ public:
             throw tactic_exception("pb-preprocess does not support proofs");
         }
 
-        pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m);
+        generic_model_converter* pp = alloc(generic_model_converter, m, "pb-preprocess");
         g->add(pp);
 
         g->inc_depth();        
@@ -165,7 +125,7 @@ public:
         // decompose(g);
     }
 
-    bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) {
+    bool simplify(goal_ref const& g, generic_model_converter& mc) {
         reset();
         normalize(g);
         if (g->inconsistent()) {
@@ -203,11 +163,11 @@ public:
             TRACE("pb", tout << mk_pp(e, m) << " " << r.pos.size() << " " << r.neg.size() << "\n";);
             if (r.pos.empty()) {                
                 replace(r.neg, e, m.mk_false(), g);
-                mc.set_value(e, false);
+                set_value(mc, e, false);
             }
             else if (r.neg.empty()) {
                 replace(r.pos, e, m.mk_true(), g);
-                mc.set_value(e, true);
+                set_value(mc, e, true);
             }
             if (g->inconsistent()) return false;
             ++it;
@@ -509,7 +469,7 @@ private:
 
     // Implement very special case of resolution.
     
-    void resolve(pb_preproc_model_converter& mc, unsigned idx1, 
+    void resolve(generic_model_converter& mc, unsigned idx1, 
                  unsigned_vector const& positions, app* e, bool pos, goal_ref const& g) {
         if (positions.size() != 1) return;
         unsigned idx2 = positions[0];
@@ -558,7 +518,7 @@ private:
             else {
                 args2[j] = m.mk_true();
             }
-            mc.set_value(arg, j != min_index);
+            set_value(mc, arg, j != min_index);
         }
         
         tmp1 = pb.mk_ge(args2.size(), coeffs2.c_ptr(), args2.c_ptr(), k2);

src/tactic/generic_model_converter.cpp

@@ -181,6 +181,53 @@ void generic_model_converter::operator()(expr_ref& fml) {
     fml = mk_and(fmls);
 }
 
+void generic_model_converter::get_units(obj_map<expr, bool>& units) {
+    th_rewriter rw(m);
+    expr_safe_replace rep(m);
+    expr_ref tmp(m);
+    bool val = false;
+    expr* f = nullptr;
+    for (auto const& kv : units) {
+        rep.insert(kv.m_key, kv.m_value ? m.mk_true() : m.mk_false());
+    }
+    for (unsigned i = m_entries.size(); i-- > 0;) {
+        entry const& e = m_entries[i];
+        switch (e.m_instruction) {
+        case HIDE: 
+            tmp = m.mk_const(e.m_f);
+            if (units.contains(tmp)) {
+                m.dec_ref(tmp);
+                units.remove(tmp);
+            }
+            break;
+        case ADD:
+            if (e.m_f->get_arity() == 0 && m.is_bool(e.m_f->get_range())) {
+                tmp = m.mk_const(e.m_f);
+                if (units.contains(tmp)) {
+                    break;
+                }
+                tmp = e.m_def;
+                rep(tmp);
+                rw(tmp);
+                if (m.is_true(tmp)) {
+                    tmp = m.mk_const(e.m_f);
+                    m.inc_ref(tmp);
+                    units.insert(tmp, true);
+                    rep.insert(tmp, m.mk_true());
+                }
+                else if (m.is_false(tmp)) {
+                    tmp = m.mk_const(e.m_f);
+                    m.inc_ref(tmp);
+                    units.insert(tmp, false);
+                    rep.insert(tmp, m.mk_false());
+                }
+            }
+            break;
+        }
+    }
+}
+
+
 /*
  \brief simplify definition expansion from model converter in the case they come from blocked clauses.
  In this case the definitions are of the form:

src/tactic/generic_model_converter.h

@@ -71,6 +71,8 @@ public:
     void collect(ast_pp_util& visitor) override;
 
     void operator()(expr_ref& fml) override; 
+
+    void get_units(obj_map<expr, bool>& units) override;
 };
 
 typedef ref<generic_model_converter> generic_model_converter_ref;

src/tactic/horn_subsume_model_converter.h

@@ -80,6 +80,9 @@ public:
     ast_manager& get_manager() { return m; }
 
     void display(std::ostream & out) override {}
+
+    void get_units(obj_map<expr, bool>& units) override { units.reset(); }
+
 };
 
 #endif

src/tactic/model_converter.cpp

@@ -71,14 +71,19 @@ public:
     }
 
     void operator()(expr_ref & fml) override {
-        this->m_c1->operator()(fml);
         this->m_c2->operator()(fml);
+        this->m_c1->operator()(fml);
     }
     
     void operator()(labels_vec & r) override {
         this->m_c2->operator()(r);
         this->m_c1->operator()(r);
     }
+
+    void get_units(obj_map<expr, bool>& fmls) override {
+        m_c2->get_units(fmls);
+        m_c1->get_units(fmls);
+    }
   
     char const * get_name() const override { return "concat-model-converter"; }
 
@@ -125,6 +130,10 @@ public:
         fml = r;
     }
 
+    void get_units(obj_map<expr, bool>& fmls) override {
+        // no-op
+    }
+
     void cancel() override {
     }
     

src/tactic/model_converter.h

@@ -88,6 +88,8 @@ public:
        formula and removing these definitions from the model converter.
      */
     virtual void operator()(expr_ref& formula) { UNREACHABLE(); }
+
+    virtual void get_units(obj_map<expr, bool>& fmls) { UNREACHABLE(); }
 };
 
 typedef ref<model_converter> model_converter_ref;