Merge pull request #1710 from agurfinkel/deep_space

Deep space

src/muz/base/fp_params.pyg

@@ -150,6 +150,8 @@ def_module_params('fp',
                           ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'),
                           ('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'),
                           ('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'),
+                          ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
+                          ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
                           ('spacer.iuc', UINT, 1,
                            '0 = use old implementation of unsat-core-generation, ' +
                            '1 = use new implementation of IUC generation, ' +
@@ -164,8 +166,6 @@ def_module_params('fp',
                           ('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'),
                           ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'),
                           ('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'),
-                          ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
-                          ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
                           ('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'),
                           ('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"),
                           ('spacer.min_level', UINT, 0, 'Minimal level to explore'),

src/muz/spacer/spacer_context.cpp

@@ -126,7 +126,15 @@ void pob::get_skolems(app_ref_vector &v) {
     }
 }
 
-
+    std::ostream &pob::display(std::ostream &out, bool full) const {
+        out << pt().head()->get_name ()
+            << " level: " << level()
+            << " depth: " << depth()
+            << " post_id: " << post()->get_id()
+            << (is_in_queue() ? " in_queue" : "");
+        if (full) out << "\n" << m_post;
+        return out;
+    }
 
 // ----------------
 // pob_queue
@@ -538,7 +546,8 @@ void lemma::mk_expr_core() {
     SASSERT(!m_cube.empty());
     m_body = ::mk_and(m_cube);
     // normalize works better with a cube
-    normalize(m_body, m_body);
+    normalize(m_body, m_body, false /* no simplify bounds */, false /* term_graph */);
+
     m_body = ::push_not(m_body);
 
     if (!m_zks.empty() && has_zk_const(m_body)) {
@@ -2173,9 +2182,7 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent,
     p.set_post(post, b);
 
     if (m_pobs.contains(p.post())) {
-        auto &buf = m_pobs[p.post()];
+        for (auto *f : m_pobs[p.post()]) {
-        for (unsigned i = 0, sz = buf.size(); i < sz; ++i) {
-            pob *f = buf.get(i);
             if (f->parent() == parent && !f->is_in_queue()) {
                 f->inherit(p);
                 return f;

src/muz/spacer/spacer_context.h

@@ -693,6 +693,7 @@ public:
         if (m_ref_count == 0) {dealloc(this);}
     }
 
+    std::ostream &display(std::ostream &out, bool full = false) const;
     class on_expand_event
     {
         pob &m_p;
@@ -702,6 +703,9 @@ public:
     };
 };
 
+inline std::ostream &operator<<(std::ostream &out, pob const &p) {
+    return p.display(out);
+}
 
 struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> {
     bool operator() (const pob *pn1, const pob *pn2) const;

src/muz/spacer/spacer_prop_solver.cpp

@@ -56,6 +56,7 @@ prop_solver::prop_solver(ast_manager &m,
     m_use_push_bg(p.spacer_keep_proxy())
 {
 
+    m_random.set_seed(p.spacer_random_seed());
     m_solvers[0] = solver0;
     m_solvers[1] = solver1;
 
@@ -363,6 +364,8 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
     hard.append(_hard.size(), _hard.c_ptr());
     flatten_and(hard);
 
+    shuffle(hard.size(), hard.c_ptr(), m_random);
+
     m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get();
 
     // can be disabled if use_push_bg == true

src/muz/spacer/spacer_prop_solver.h

@@ -61,6 +61,8 @@ private:
     bool                m_use_push_bg;
     unsigned            m_current_level;    // set when m_in_level
 
+    random_gen          m_random;
+
     void assert_level_atoms(unsigned level);
 
     void ensure_level(unsigned lvl);

src/muz/spacer/spacer_quant_generalizer.cpp

@@ -80,6 +80,51 @@ struct index_lt_proc : public std::binary_function<app*, app *, bool> {
     }
 };
 
+
+    struct has_nlira_functor {
+        struct found{};
+
+        ast_manager &m;
+        arith_util   u;
+
+        has_nlira_functor(ast_manager &_m) : m(_m), u(m) {}
+
+        void operator()(var *) {}
+        void operator()(quantifier *) {}
+        void operator()(app *n) {
+            family_id fid = n->get_family_id();
+            if (fid != u.get_family_id()) return;
+
+            switch(n->get_decl_kind()) {
+            case OP_MUL:
+                if (n->get_num_args() != 2)
+                    throw found();
+                if (!u.is_numeral(n->get_arg(0)) && !u.is_numeral(n->get_arg(1)))
+                    throw found();
+                return;
+            case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
+                if (!u.is_numeral(n->get_arg(1)))
+                    throw found();
+                return;
+            default:
+                return;
+            }
+            return;
+        }
+    };
+
+    bool has_nlira(expr_ref_vector &v) {
+        has_nlira_functor fn(v.m());
+        expr_fast_mark1 visited;
+        try {
+            for (expr *e : v)
+                quick_for_each_expr(fn, visited, e);
+        }
+        catch (has_nlira_functor::found e) {
+            return true;
+        }
+        return false;
+    }
 }
 
 namespace spacer {
@@ -191,9 +236,15 @@ expr* times_minus_one(expr *e, arith_util &arith) {
     Find sub-expression of the form (select A (+ sk!0 t)) and replaces
     (+ sk!0 t) --> sk!0 and sk!0 --> (+ sk!0 (* (- 1) t))
 
-    Current implementation is an ugly hack for one special case
+
+    rewrites bind to  (+ bsk!0 t) where bsk!0 is the original binding for sk!0
+
+    Current implementation is an ugly hack for one special
+    case. Should be rewritten based on an equality solver from qe
 */
-void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector const &zks, expr_ref &bind) {
+void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube,
+                                           app_ref_vector const &zks,
+                                           expr_ref &bind) {
     if (zks.size() != 1) return;
 
     arith_util arith(m);
@@ -219,8 +270,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector
                     kids_bind.push_back(bind);
                 }
                 else {
-                    kids.push_back (times_minus_one(arg, arith));
+                    kids.push_back(times_minus_one(arg, arith));
-                    kids_bind.push_back (times_minus_one(arg, arith));
+                    kids_bind.push_back(arg);
                 }
             }
             if (!found) continue;
@@ -228,7 +279,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector
             rep = arith.mk_add(kids.size(), kids.c_ptr());
             bind = arith.mk_add(kids_bind.size(), kids_bind.c_ptr());
             TRACE("spacer_qgen",
-                  tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n";);
+                  tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n"
+                  << "bind is: " << bind << "\n";);
             break;
         }
     }
@@ -454,9 +506,15 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
 
     mk_abs_cube(lemma, term, var, gnd_cube, abs_cube, lb, ub, stride);
     if (abs_cube.empty()) {return false;}
+    if (has_nlira(abs_cube)) {
+        TRACE("spacer_qgen",
+              tout << "non-linear expression: " << abs_cube << "\n";);
+        return false;
+    }
 
     TRACE("spacer_qgen",
           tout << "abs_cube is: " << mk_and(abs_cube) << "\n";
+          tout << "term: " << mk_pp(term, m) << "\n";
           tout << "lb = ";
           if (lb) tout << mk_pp(lb, m); else tout << "none";
           tout << "\n";
@@ -473,7 +531,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
         lb = abs_cube.back();
     }
     if (!ub) {
-        abs_cube.push_back (m_arith.mk_lt(var, term));
+        abs_cube.push_back (m_arith.mk_le(var, term));
         ub = abs_cube.back();
     }
 
@@ -489,10 +547,10 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
         TRACE("spacer_qgen",
               tout << "mod=" << mod << " init=" << init << " stride=" << stride << "\n";
               tout.flush(););
-        abs_cube.push_back(m.mk_eq(
+        abs_cube.push_back
-                m_arith.mk_mod(var, m_arith.mk_numeral(rational(stride), true)),
+            (m.mk_eq(m_arith.mk_mod(var,
-                m_arith.mk_numeral(rational(mod), true)));
+                                    m_arith.mk_numeral(rational(stride), true)),
-    }
+                     m_arith.mk_numeral(rational(mod), true)));}
 
     // skolemize
     expr_ref gnd(m);
@@ -512,21 +570,21 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
               << "New CUBE is: " << gnd_cube << "\n";);
         SASSERT(zks.size() >= static_cast<unsigned>(m_offset));
 
-                // lift quantified variables to top of select
+        // lift quantified variables to top of select
         expr_ref ext_bind(m);
         ext_bind = term;
         cleanup(gnd_cube, zks, ext_bind);
 
-                // XXX better do that check before changing bind in cleanup()
+        // XXX better do that check before changing bind in cleanup()
-                // XXX Or not because substitution might introduce _n variable into bind
+        // XXX Or not because substitution might introduce _n variable into bind
         if (m_ctx.get_manager().is_n_formula(ext_bind)) {
-                    // XXX this creates an instance, but not necessarily the needed one
+            // XXX this creates an instance, but not necessarily the needed one
 
-                    // XXX This is sound because any instance of
+            // XXX This is sound because any instance of
-                    // XXX universal quantifier is sound
+            // XXX universal quantifier is sound
 
-                    // XXX needs better long term solution. leave
+            // XXX needs better long term solution. leave
-                    // comment here for the future
+            // comment here for the future
             m_ctx.get_manager().formula_n2o(ext_bind, ext_bind, 0);
         }
 

src/muz/spacer/spacer_util.cpp

@@ -666,9 +666,6 @@ namespace {
             flatten_and(out, v);
 
             if (v.size() > 1) {
-                // sort arguments of the top-level and
-                std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
-
                 if (use_simplify_bounds) {
                     // remove redundant inequalities
                     simplify_bounds(v);
@@ -680,6 +677,8 @@ namespace {
                     v.reset();
                     egraph.to_lits(v);
                 }
+                // sort arguments of the top-level and
+                std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
 
                 TRACE("spacer_normalize",
                       tout << "Normalized:\n"