From 1530a39a9648e0380532f8909cba1ad70c58d34e Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 31 Jul 2017 15:42:44 -0400
Subject: [PATCH] stubs for spacer-specific API

---
 src/muz/base/dl_engine_base.h | 16 ++++++++++++++++
 src/muz/base/dl_util.h        |  1 +
 2 files changed, 17 insertions(+)

diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h
index 380ae6e07..9c20c712d 100644
--- a/src/muz/base/dl_engine_base.h
+++ b/src/muz/base/dl_engine_base.h
@@ -20,6 +20,7 @@ Revision History:
 #define DL_ENGINE_BASE_H_
 
 #include "model/model.h"
+#include "muz/base/dl_util.h"
 
 namespace datalog {
     enum DL_ENGINE {
@@ -44,6 +45,9 @@ namespace datalog {
         virtual ~engine_base() {}
 
         virtual expr_ref get_answer() = 0;
+        virtual expr_ref get_ground_sat_answer () {
+            throw default_exception(std::string("operation is not supported for ") + m_name);
+        }
         virtual lbool query(expr* q) = 0;
         virtual lbool query(unsigned num_rels, func_decl*const* rels) { 
             if (num_rels != 1) return l_undef;
@@ -65,6 +69,9 @@ namespace datalog {
             }
             return query(q);
         }
+        virtual lbool query_from_lvl (expr* q, unsigned lvl) {
+            throw default_exception(std::string("operation is not supported for ") + m_name);
+        }
 
         virtual void reset_statistics() {}
         virtual void display_profile(std::ostream& out) {}
@@ -72,18 +79,27 @@ namespace datalog {
         virtual unsigned get_num_levels(func_decl* pred) {
             throw default_exception(std::string("get_num_levels is not supported for ") + m_name);
         }
+        virtual expr_ref get_reachable(func_decl* pred) {
+              throw default_exception(std::string("operation is not supported for ") + m_name);
+        }
         virtual expr_ref get_cover_delta(int level, func_decl* pred) {
             throw default_exception(std::string("operation is not supported for ") + m_name);
         }
         virtual void add_cover(int level, func_decl* pred, expr* property) {
             throw default_exception(std::string("operation is not supported for ") + m_name);
         }
+        virtual void add_invariant (func_decl *pred, expr *property) {
+            throw default_exception(std::string("operation is not supported for ") + m_name);
+        }
         virtual void display_certificate(std::ostream& out) const {
             throw default_exception(std::string("certificates are not supported for ") + m_name);
         }
         virtual model_ref get_model() {
             return model_ref(alloc(model, m));
         }
+        virtual void get_rules_along_trace (rule_ref_vector& rules) {
+            throw default_exception(std::string("get_rules_along_trace is not supported for ") + m_name);
+        }
         virtual proof_ref get_proof() {
             return proof_ref(m.mk_asserted(m.mk_true()), m);
         }
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index 48d420bfb..d04e4037c 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -52,6 +52,7 @@ namespace datalog {
         ~verbose_action();
     };
 
+    typedef ref_vector<rule, rule_manager> rule_ref_vector;
     enum PDR_CACHE_MODE {
         NO_CACHE,
         HASH_CACHE,