From 1ef17cbe679884c434a95c2039959f2c0cd61034 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 5 Apr 2013 18:12:58 -0700 Subject: [PATCH] add dl_context::has_facts(pred) Signed-off-by: Nuno Lopes --- src/muz_qe/dl_context.cpp | 4 ++++ src/muz_qe/dl_context.h | 1 + src/muz_qe/rel_context.cpp | 5 +++++ src/muz_qe/rel_context.h | 7 ++++++- 4 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 852d8f847..7a1e3b8fc 100644 --- a/src/muz_qe/dl_context.cpp +++ b/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(); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index cb432d4e9..d23cf2c0c 100644 --- a/src/muz_qe/dl_context.h +++ b/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); diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 12045047b..58263b9d0 100644 --- a/src/muz_qe/rel_context.cpp +++ b/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); } diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 08ee868c0..d2f6973da 100644 --- a/src/muz_qe/rel_context.h +++ b/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