From 530d44f7b4a773ca17153b1f47ce4fe5f6133e5f Mon Sep 17 00:00:00 2001
From: Hari Govind V K <hgvk94@gmail.com>
Date: Thu, 30 Apr 2020 17:03:48 -0400
Subject: [PATCH] [spacer] implement spacer::is_clause() (#4170)

Spacer has a different defintion of is_clause() than ast_util.
It is currently only used in assertions.

Main difference:
  x=y
where x and y are Bool atoms is considered to be an atom, so that
(or (= x y) (not (= z y)))
is a literal

Co-authored-by: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
---
 src/muz/spacer/spacer_context.cpp           |  6 ++--
 src/muz/spacer/spacer_unsat_core_plugin.cpp |  4 +--
 src/muz/spacer/spacer_util.cpp              | 38 +++++++++++++++++++++
 src/muz/spacer/spacer_util.h                |  3 ++
 4 files changed, 47 insertions(+), 4 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index e7e8f3e04f7..21f8a0fdcbf 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -941,8 +941,10 @@ void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only)
     SASSERT(!lemma->is_background());
     unsigned lvl = lemma->level();
     expr* l = lemma->get_expr();
-    SASSERT(!lemma->is_ground() || is_clause(m, l));
-    SASSERT(!is_quantifier(l) || is_clause(m, to_quantifier(l)->get_expr()));
+    CTRACE("spacer", !spacer::is_clause(m, l),
+           tout << "Lemma not a clause: " << mk_pp(l, m) << "\n";);
+    SASSERT(!lemma->is_ground() || spacer::is_clause(m, l));
+    SASSERT(!is_quantifier(l) || spacer::is_clause(m, to_quantifier(l)->get_expr()));
 
     get_context().log_add_lemma(*this, *lemma);
 
diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp
index 77e88fb32e7..e0c5a39f5d2 100644
--- a/src/muz/spacer/spacer_unsat_core_plugin.cpp
+++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp
@@ -73,7 +73,7 @@ namespace spacer {
                 // the current step needs to be interpolated:
                 expr* fact = m.get_fact(pf);
                 // if we trust the current step and we are able to use it
-                if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || is_literal(m, fact))) {
+                if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || spacer::is_literal(m, fact))) {
                     // just add it to the core
                     m_ctx.add_lemma_to_core(fact);
                 }
@@ -558,7 +558,7 @@ namespace spacer {
                     // if we trust the current step and we are able to use it
                     if (m_ctx.is_b_pure (current) &&
                         (m.is_asserted(current) ||
-                         is_literal(m, m.get_fact(current))))
+                         spacer::is_literal(m, m.get_fact(current))))
                     {
                         // we found a leaf of the subproof, so
                         // 1) we add corresponding edges
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 8441a5fbdbe..19ae867bf7d 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -69,6 +69,44 @@ Revision History:
 
 namespace spacer {
 
+    bool is_clause(ast_manager &m, expr *n) {
+      if (spacer::is_literal(m, n))
+        return true;
+      if (m.is_or(n)) {
+        for (expr *arg : *to_app(n)){
+          if (!spacer::is_literal(m, arg))
+            return false;
+          return true;
+        }
+      }
+      return false;
+    }
+
+    bool is_literal(ast_manager &m, expr *n) {
+      return spacer::is_atom(m, n) || (m.is_not(n) && spacer::is_atom(m, to_app(n)->get_arg(0)));
+    }
+
+    bool is_atom(ast_manager &m, expr *n) {
+      if (is_quantifier(n) || !m.is_bool(n))
+        return false;
+      if (is_var(n))
+        return true;
+      SASSERT(is_app(n));
+      if (to_app(n)->get_family_id() != m.get_basic_family_id()) {
+        return true;
+      }
+
+      if ((m.is_eq(n) && !m.is_bool(to_app(n)->get_arg(0))) ||
+          m.is_true(n) || m.is_false(n))
+        return true;
+
+      // x=y is atomic if x and y are Bool and atomic
+      expr *e1, *e2;
+      if (m.is_eq(n, e1, e2) && spacer::is_atom(m, e1) && spacer::is_atom(m, e2))
+        return true;
+      return false;
+    }
+
     void subst_vars(ast_manager& m,
                     app_ref_vector const& vars, model& mdl, expr_ref& fml) {
         model::scoped_model_completion _sc_(mdl, true);
diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h
index 9fdfe48a40a..645f620955a 100644
--- a/src/muz/spacer/spacer_util.h
+++ b/src/muz/spacer/spacer_util.h
@@ -142,6 +142,9 @@ namespace spacer {
     /// Returns number of free variables in a given expression
     unsigned get_num_vars(expr *e);
     void get_uninterp_consts(expr *a, expr_ref_vector &out);
+    bool is_clause(ast_manager &m, expr *n); 
+    bool is_literal(ast_manager &m, expr *n);
+    bool is_atom(ast_manager &m, expr *n);
 }
 
 #endif