add dl_context::has_facts(pred)

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>

src/muz_qe/dl_context.cpp

@@ -780,6 +780,10 @@ namespace datalog {
         add_fact(head->get_decl(), fact);
     }
 
+    bool context::has_facts(func_decl * pred) const {
+        return m_rel && m_rel->has_facts(pred);
+    }
+
     void context::add_table_fact(func_decl * pred, const table_fact & fact) {
         if (get_engine() == DATALOG_ENGINE) {
             ensure_rel();

src/muz_qe/dl_context.h

@@ -249,6 +249,7 @@ namespace datalog {
         void add_fact(app * head);
         void add_fact(func_decl * pred, const relation_fact & fact);
 
+        bool has_facts(func_decl * pred) const;
         
         void add_rule(rule_ref& r);
         void add_rules(rule_ref_vector& rs);

src/muz_qe/rel_context.cpp

@@ -497,6 +497,11 @@ namespace datalog {
         }
     }
 
+    bool rel_context::has_facts(func_decl * pred) const {
+        relation_base* r = try_get_relation(pred);
+        return r && !r->empty();
+    }
+
     void rel_context::store_relation(func_decl * pred, relation_base * rel) {
         get_rmanager().store_relation(pred, rel);
     }

src/muz_qe/rel_context.h

@@ -92,9 +92,14 @@ namespace datalog {
          */
         bool result_contains_fact(relation_fact const& f);
 
+        /** \brief add facts to relation
+        */
         void add_fact(func_decl* pred, relation_fact const& fact);
-
         void add_fact(func_decl* pred, table_fact const& fact);
+
+        /** \brief check if facts were added to relation
+        */
+        bool has_facts(func_decl * pred) const;
         
         /**
            \brief Store the relation \c rel under the predicate \c pred. The \c context object