From 9cdb63ae4ab6a8c869060bd1b54ac99d3cf5c2e8 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Fri, 29 Dec 2017 12:03:48 -0500
Subject: [PATCH] Handle conversion of quantified lemma to quantifier free

When a cube is updated, a lemma might loose all of its quantified
variables. In this case, it is effectively quantifier free
and might be a version of an already existing lemma.

For that reason, we convert it to quantifier free lemma when
this happens.
---
 src/muz/spacer/spacer_context.cpp           | 14 +++++++++++++-
 src/muz/spacer/spacer_quant_generalizer.cpp | 17 ++++++++++-------
 2 files changed, 23 insertions(+), 8 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 607bf2018..90103503b 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1300,6 +1300,18 @@ void lemma::update_cube (pob_ref const &p, expr_ref_vector &cube) {
     m_body.reset();
     m_cube.append(cube);
     if (m_cube.empty()) {m_cube.push_back(m.mk_true());}
+
+    // after the cube is updated, if there are no skolems,
+    // convert the lemma to quantifier-free
+    bool is_quant = false;
+    for (unsigned i = 0, sz = cube.size(); !is_quant && i < sz; ++i) {
+        is_quant = has_zk_const(cube.get(i));
+    }
+
+    if (!is_quant) {
+        m_zks.reset();
+        m_bindings.reset();
+    }
 }
 
 bool lemma::has_binding(app_ref_vector const &binding) {
@@ -2272,7 +2284,7 @@ void context::init_lemma_generalizers(datalog::rule_set& rules)
     }
 
     if (m_params.spacer_use_quant_generalizer()) {
-        m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer, *this, 0, false));
+        m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer, *this, 0, true));
         m_lemma_generalizers.push_back(alloc(lemma_quantifier_generalizer, *this));
     }
 
diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp
index 8be97122c..942fbfc6a 100644
--- a/src/muz/spacer/spacer_quant_generalizer.cpp
+++ b/src/muz/spacer/spacer_quant_generalizer.cpp
@@ -202,7 +202,11 @@ void lemma_quantifier_generalizer::find_matching_expressions(
             sem_matcher match(m);
             bool pos;
             substitution v_sub(m);
-            v_sub.reserve(2, subs.size()+1);
+
+            // allocate space for the largest variable in the pattern
+            unsigned max_idx = 0;
+            for (var* v : subs) {max_idx = std::max(max_idx, v->get_idx());}
+            v_sub.reserve(2, max_idx + 1);
 
             if (!match(pattern, lit, v_sub, pos)) {
                 continue;
@@ -378,13 +382,15 @@ void lemma_quantifier_generalizer::operator()(lemma_ref &lemma) {
 
     TRACE("spacer_qgen",
           tout << "initial cube: " << mk_and(lemma->get_cube()) << "\n";);
-    if (false) {
+    if (true) {
         // -- re-normalize the cube
         expr_ref c(m);
         c = mk_and(cube);
         normalize(c, c, true, true);
         cube.reset();
         flatten_and(c, cube);
+        TRACE("spacer_qgen",
+              tout << "normalized cube:\n" << mk_and(cube) << "\n";);
     }
 
     app_ref_vector skolems(m);
@@ -398,10 +404,6 @@ void lemma_quantifier_generalizer::operator()(lemma_ref &lemma) {
         // generate candidates
         app_ref_vector candidates(m);
         find_candidates(r, candidates);
-
-        // XXX Can candidates be empty and arguments not empty?
-        // XXX Why separate candidates and arguments?
-        // XXX Why are arguments processed before candidates?
         if (candidates.empty()) continue;
 
 
@@ -456,7 +458,7 @@ void lemma_quantifier_generalizer::operator()(lemma_ref &lemma) {
             unsigned weakness = lemma->weakness();
             pred_transformer &pt = lemma->get_pob()->pt();
             if (pt.check_inductive(lemma->level(), new_cube, uses_level, weakness)) {
-                TRACE("spacer",
+                TRACE("spacer_qgen",
                       tout << "Quantifier Generalization Succeeded!\n"
                       << "New CUBE is: " << mk_pp(mk_and(new_cube),m) << "\n";);
                 SASSERT(zks.size() >= offset);
@@ -482,6 +484,7 @@ void lemma_quantifier_generalizer::operator()(lemma_ref &lemma) {
                 lemma->update_cube(lemma->get_pob(), new_cube);
                 lemma->set_level(uses_level);
 
+                SASSERT(offset + 1 == zks.size());
                 // XXX Assumes that offset + 1 == zks.size();
                 for (unsigned sk=offset; sk < zks.size(); sk++)
                     lemma->add_skolem(zks.get(sk), to_app(bind));