implemented spacer-specic muz API

src/muz/base/dl_context.cpp

@@ -229,6 +229,7 @@ namespace datalog {
         m_enable_bind_variables(true),
         m_last_status(OK),
         m_last_answer(m),
+        m_last_ground_answer(m),
         m_engine_type(LAST_ENGINE) {
         re.set_context(this);
         updt_params(pa);
@@ -306,6 +307,8 @@ namespace datalog {
     bool context::compress_unbound() const { return m_params->xform_compress_unbound(); }
     bool context::quantify_arrays() const { return m_params->xform_quantify_arrays(); }
     bool context::instantiate_quantifiers() const { return m_params->xform_instantiate_quantifiers(); }
+    bool context::array_blast() const { return m_params->xform_array_blast(); }
+    bool context::array_blast_full() const { return m_params->xform_array_blast_full(); }
 
 
     void context::register_finite_sort(sort * s, sort_kind k) {
@@ -546,10 +549,20 @@ namespace datalog {
         return m_engine->get_cover_delta(level, pred);
     }
 
+    expr_ref context::get_reachable(func_decl *pred) {
+        ensure_engine();
+        return m_engine->get_reachable(pred);
+    }
     void context::add_cover(int level, func_decl* pred, expr* property) {
         ensure_engine();
         m_engine->add_cover(level, pred, property);
     }
+  
+    void context::add_invariant(func_decl* pred, expr *property)
+    {
+        ensure_engine();
+        m_engine->add_invariant(pred, property);
+    }
 
     void context::check_rules(rule_set& r) {
         m_rule_properties.set_generate_proof(generate_proof_trace());
@@ -561,6 +574,7 @@ namespace datalog {
             m_rule_properties.check_nested_free(); 
             m_rule_properties.check_infinite_sorts();
             break;
+        case SPACER_ENGINE:
         case PDR_ENGINE:
             m_rule_properties.collect(r);
             m_rule_properties.check_existential_tail();
@@ -792,6 +806,9 @@ namespace datalog {
         if (e == symbol("datalog")) {
             m_engine_type = DATALOG_ENGINE;
         }
+        else if (e == symbol("spacer")) {
+            m_engine_type = SPACER_ENGINE;
+        }
         else if (e == symbol("pdr")) {
             m_engine_type = PDR_ENGINE;
         }
@@ -844,8 +861,10 @@ namespace datalog {
         m_mc = mk_skip_model_converter();
         m_last_status = OK;
         m_last_answer = 0;
+        m_last_ground_answer = 0;
         switch (get_engine()) {
         case DATALOG_ENGINE:
+        case SPACER_ENGINE:
         case PDR_ENGINE:
         case QPDR_ENGINE:
         case BMC_ENGINE:
@@ -867,6 +886,28 @@ namespace datalog {
         return m_engine->query(query);
     }
 
+    lbool context::query_from_lvl (expr* query, unsigned lvl) {
+        m_mc = mk_skip_model_converter();
+        m_last_status = OK;
+        m_last_answer = 0;
+        m_last_ground_answer = 0;
+        switch (get_engine()) {
+        case DATALOG_ENGINE:
+        case SPACER_ENGINE:
+        case PDR_ENGINE:
+        case QPDR_ENGINE:
+        case BMC_ENGINE:
+        case QBMC_ENGINE:
+        case TAB_ENGINE:
+        case CLP_ENGINE:
+            flush_add_rules();
+            break;
+        default:
+            UNREACHABLE();
+        }
+        ensure_engine();
+        return m_engine->query_from_lvl (query, lvl);
+    }
     model_ref context::get_model() {
         ensure_engine();
         return m_engine->get_model();
@@ -905,6 +946,42 @@ namespace datalog {
         return m_last_answer.get();
     }
 
+    expr* context::get_ground_sat_answer () {
+        if (m_last_ground_answer) {
+            return m_last_ground_answer;
+        }
+        ensure_engine ();
+        m_last_ground_answer = m_engine->get_ground_sat_answer ();
+        return m_last_ground_answer;
+    }
+
+    void context::get_rules_along_trace (rule_ref_vector& rules) {
+        ensure_engine ();
+        m_engine->get_rules_along_trace (rules);
+    }
+
+    void context::get_rules_along_trace_as_formulas (expr_ref_vector& rules, svector<symbol>& names) {
+        rule_manager& rm = get_rule_manager ();
+        rule_ref_vector rv (rm);
+        get_rules_along_trace (rv);
+        expr_ref fml (m);
+        rule_ref_vector::iterator it = rv.begin (), end = rv.end ();
+        for (; it != end; it++) {
+            m_rule_manager.to_formula (**it, fml);
+            rules.push_back (fml);
+            // The concatenated names are already stored last-first, so do not need to be reversed here
+            const symbol& rule_name = (*it)->name();
+            names.push_back (rule_name);
+
+            TRACE ("dl",
+                   if (rule_name == symbol::null) {
+                       tout << "Encountered unnamed rule: ";
+                       (*it)->display(*this, tout);
+                       tout << "\n";
+                   });
+        }
+    }
+
     void context::display_certificate(std::ostream& out) {
         ensure_engine();
         m_engine->display_certificate(out);

src/muz/base/dl_context.h

@@ -207,6 +207,7 @@ namespace datalog {
         bool               m_enable_bind_variables;
         execution_result   m_last_status;
         expr_ref           m_last_answer;
+        expr_ref           m_last_ground_answer;
         DL_ENGINE          m_engine_type;
 
 
@@ -277,6 +278,8 @@ namespace datalog {
         bool xform_bit_blast() const;        
         bool xform_slice() const;
         bool xform_coi() const;
+        bool array_blast() const;
+        bool array_blast_full() const;
 
         void register_finite_sort(sort * s, sort_kind k);
 
@@ -407,6 +410,10 @@ namespace datalog {
          */
         unsigned get_num_levels(func_decl* pred);
 
+        /**
+            Retrieve reachable facts of 'pred'.
+         */
+        expr_ref get_reachable(func_decl *pred);
         /**
            Retrieve the current cover of 'pred' up to 'level' unfoldings.
            Return just the delta that is known at 'level'. To
@@ -421,6 +428,11 @@ namespace datalog {
          */
         void add_cover(int level, func_decl* pred, expr* property);
 
+        /**
+          Add an invariant of predicate 'pred'.
+         */
+        void add_invariant (func_decl *pred, expr *property);
+      
         /**
            \brief Check rule subsumption.
         */
@@ -509,6 +521,7 @@ namespace datalog {
 
         lbool query(expr* q);
 
+        lbool query_from_lvl (expr* q, unsigned lvl);
         /**
            \brief retrieve model from inductive invariant that shows query is unsat.
            
@@ -545,6 +558,18 @@ namespace datalog {
            in the query that are derivable.
         */
         expr* get_answer_as_formula();
+        /**
+         * get bottom-up (from query) sequence of ground predicate instances
+         * (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query
+         */
+        expr* get_ground_sat_answer ();
+
+        /**
+         * \brief obtain the sequence of rules along the counterexample trace
+         */
+        void get_rules_along_trace (rule_ref_vector& rules);
+
+        void get_rules_along_trace_as_formulas (expr_ref_vector& rules, svector<symbol>& names);
 
 
         void collect_statistics(statistics& st) const;