Merge pull request #9 from TheRealNebus/opt

Opt

src/api/dotnet/Solver.cs

@@ -429,11 +429,12 @@ public IEnumerable<BoolExpr[]> Cube()
                 var lvl = BacktrackLevel;
                 BacktrackLevel = uint.MaxValue;
                 ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
-                if (r.Size == 1 && ((Expr)r[0]).IsFalse) {
+                var v = r.ToBoolExprArray();
+                if (v.Length == 1 && v[0].IsFalse) {
                    break;
                 }
-                yield return r.ToBoolExprArray();
-	        if (r.Size == 0) {
+                yield return v; 
+ 	            if (v.Length == 0) {
                    break;
                 }
 	     }

src/sat/tactic/goal2sat.cpp

@@ -885,7 +885,8 @@ struct sat2goal::imp {
         sat::model_converter         m_mc;
         expr_ref_vector              m_var2expr;
         generic_model_converter_ref  m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion
-
+        generic_model_converter_ref  m_imc; // used to ensure correctness in incremental calls with simplifications that require model conversions
+
         sat_model_converter(ast_manager & m):
             m_var2expr(m) {
         }
@@ -894,6 +895,7 @@ struct sat2goal::imp {
         sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) {
             m_mc.copy(s.get_model_converter());
             m_fmc = alloc(generic_model_converter, m);
+            m_imc = nullptr;
         }
 
         ast_manager & m() { return m_var2expr.get_manager(); }
@@ -920,6 +922,7 @@ struct sat2goal::imp {
                     insert(l.var(), m().mk_fresh_const(0, m().mk_bool_sort()), true);
                 }
             }
+            m_imc = nullptr;
         }
 
         virtual void operator()(model_ref & md) {
@@ -1026,7 +1029,34 @@ struct sat2goal::imp {
         }
 
         void operator()(expr_ref& formula) override {
-            NOT_IMPLEMENTED_YET();
+            if (!m_imc) {
+                m_imc = alloc(generic_model_converter, m());
+                sat::literal_vector updates;
+                m_mc.expand(updates);
+                sat::literal_vector clause;
+                expr_ref_vector tail(m());
+                expr_ref def(m());
+                for (sat::literal l : updates) {
+                    if (l == sat::null_literal) {
+                        sat::literal lit0 = clause[0];
+                        for (unsigned i = 1; i < clause.size(); ++i) {
+                            tail.push_back(lit2expr(~clause[i]));
+                        }
+                        def = m().mk_or(lit2expr(lit0), mk_and(tail));
+                        if (lit0.sign()) {
+                            lit0.neg();
+                            def = m().mk_not(def);
+                        }
+                        m_imc->add(lit2expr(lit0), def);
+                        clause.reset();
+                        tail.reset();
+                    }
+                    else {
+                        clause.push_back(l);
+                    }
+                }
+            }
+            (*m_imc)(formula);
         }
     };
 

src/tactic/generic_model_converter.cpp

@@ -18,6 +18,7 @@ Module Name:
 
 --*/
 #include "ast/ast_pp.h"
+#include "ast/for_each_expr.h"
 #include "tactic/generic_model_converter.h"
 #include "model/model_v2_pp.h"
 #include "model/model_evaluator.h"
@@ -30,59 +31,89 @@ void generic_model_converter::operator()(model_ref & md) {
     ev.set_expand_array_equalities(false);
     expr_ref val(m);
     unsigned arity;
-    for (unsigned i = m_entries.size(); i-- > 0; ) {
-        entry const& e = m_entries[i];
-        switch (e.m_instruction) {
-        case HIDE:
-            md->unregister_decl(e.m_f);
-            break;
-        case ADD:
-            ev(e.m_def, val);
-            TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";);
-            arity = e.m_f->get_arity();
-            if (arity == 0) {
-                md->register_decl(e.m_f, val);
-            }
-            else {
-                func_interp * new_fi = alloc(func_interp, m, arity);
-                new_fi->set_else(val);
-                md->register_decl(e.m_f, new_fi);
-            }
-            break;
+    for (unsigned i = m_hide_entries.size(); i-- > 0; ) {
+        entry const& e = m_hide_entries[i];
+        md->unregister_decl(e.m_f);
+    }
+    for (unsigned i = m_add_entries.size(); i-- > 0; ) {
+        entry const& e = m_add_entries[i];
+        ev(e.m_def, val);
+        TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";);
+        arity = e.m_f->get_arity();
+        if (arity == 0) {
+            md->register_decl(e.m_f, val);
+        }
+        else {
+            func_interp * new_fi = alloc(func_interp, m, arity);
+            new_fi->set_else(val);
+            md->register_decl(e.m_f, new_fi);
         }
     }
     TRACE("model_converter", tout << "after generic_model_converter\n"; model_v2_pp(tout, *md););
 }
 
 void generic_model_converter::display(std::ostream & out) {
-    for (entry const& e : m_entries) {
-        switch (e.m_instruction) {
-        case HIDE:
-            display_del(out, e.m_f);
-            break;
-        case ADD:
-            display_add(out, m, e.m_f, e.m_def);
-            break;
-        }
+    for (entry const& e : m_hide_entries) {
+        display_del(out, e.m_f);
+    }
+    for (entry const& e : m_add_entries) {
+        display_del(out, e.m_f);
     }
 }
 
 model_converter * generic_model_converter::translate(ast_translation & translator) {
     ast_manager& to = translator.to();
     generic_model_converter * res = alloc(generic_model_converter, to);
-    for (entry const& e : m_entries) 
-        res->m_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction));
+    for (entry const& e : m_hide_entries) {
+        res->m_hide_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction));
+    }
+    for (entry const& e : m_add_entries) {
+        res->m_add_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction));
+    }
     return res;
 }
 
 void generic_model_converter::collect(ast_pp_util& visitor) { 
     m_env = &visitor.env(); 
-    for (entry const& e : m_entries) {
+    for (entry const& e : m_hide_entries) {
+        visitor.coll.visit_func(e.m_f);
+    }
+    for (entry const& e : m_add_entries) {
         visitor.coll.visit_func(e.m_f);
         if (e.m_def) visitor.coll.visit(e.m_def);
     }
 }
 
+struct min_app_idx_proc {
+    unsigned m_min;
+    obj_map<func_decl, unsigned>& m_idxs;
+    min_app_idx_proc(obj_map<func_decl, unsigned>& idxs) : m_min(UINT_MAX), m_idxs(idxs) {}
+    void operator()(app * n) {
+        unsigned idx;
+        if (m_idxs.find(n->get_decl(), idx)) {
+            m_min = std::min(m_min, idx);
+        }
+    }
+    void operator()(var * n) {}
+    void operator()(quantifier * n) {}
+};
+
 void generic_model_converter::operator()(expr_ref& fml) {
-    NOT_IMPLEMENTED_YET();
+    min_app_idx_proc min_proc(m_first_idx);
+    for_each_expr(min_proc, fml);
+    unsigned min_idx = min_proc.m_min;
+    for (unsigned i = m_add_entries.size(); i-- > min_idx;) {
+        entry const& e = m_add_entries[i];
+        unsigned arity = e.m_f->get_arity();
+        if (arity == 0) {
+            fml = m.mk_and(fml, m.mk_eq(m.mk_const(e.m_f), e.m_def));
+        }
+        else {
+            NOT_IMPLEMENTED_YET();
+        }
+        if (m_first_idx[e.m_f] == i) {
+            m_first_idx.remove(e.m_f);
+        }
+        m_add_entries.pop_back();
+    }
 }

src/tactic/generic_model_converter.h

@@ -32,19 +32,25 @@ class generic_model_converter : public model_converter {
             m_f(f, m), m_def(d, m), m_instruction(i) {}
     };
     ast_manager& m;
-    vector<entry> m_entries;
+    vector<entry> m_add_entries;
+    vector<entry> m_hide_entries;
+    obj_map<func_decl, unsigned> m_first_idx;
 public:
-    generic_model_converter(ast_manager & m): m(m) {}
+    generic_model_converter(ast_manager & m) : m(m) {}
 
     virtual ~generic_model_converter() { }
 
     void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); }
 
-    void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); }
+    void hide(func_decl * f) { m_hide_entries.push_back(entry(f, 0, m, HIDE)); }
 
-    void add(func_decl * d, expr* e) { m_entries.push_back(entry(d, e, m, ADD)); }
+    void add(func_decl * d, expr* e) {
+        struct entry et(d, e, m, ADD);
+        m_first_idx.insert_if_not_there(et.m_f, m_add_entries.size());
+        m_add_entries.push_back(et);
+    }
 
-    void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); m_entries.push_back(entry(to_app(d)->get_decl(), e, m, ADD)); }
+    void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); add(to_app(d)->get_decl(), e); }
 
     void operator()(labels_vec & labels) override {}