From 9b34350646c4a75c718a914f2ffc0d14cec09c93 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Oct 2013 06:25:26 -0700 Subject: [PATCH] test output predicates Signed-off-by: Nikolaj Bjorner --- src/muz/bmc/dl_bmc_engine.cpp | 4 ++++ src/muz/clp/clp_context.cpp | 3 +++ src/tactic/core/elim_uncnstr_tactic.cpp | 1 - 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index eb4bc72c4..7a88c1188 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -1448,6 +1448,10 @@ namespace datalog { transformer.register_plugin(slice); m_ctx.transform_rules(transformer); } + if (m_ctx.get_rules().get_output_predicates().empty()) { + return l_false; + } + m_query_pred = m_ctx.get_rules().get_output_predicate(); m_rules.replace_rules(m_ctx.get_rules()); m_rules.close(); diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp index 5f3a09e2d..0cd08e5b3 100644 --- a/src/muz/clp/clp_context.cpp +++ b/src/muz/clp/clp_context.cpp @@ -70,6 +70,9 @@ namespace datalog { m_goals.reset(); rm.mk_query(query, m_ctx.get_rules()); apply_default_transformation(m_ctx); + if (m_ctx.get_rules().get_output_predicates().empty()) { + return l_false; + } func_decl* head_decl = m_ctx.get_rules().get_output_predicate(); rule_set& rules = m_ctx.get_rules(); rule_vector const& rv = rules.get_predicate_rules(head_decl); diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 00e14a41f..4d64bf061 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -38,7 +38,6 @@ class elim_uncnstr_tactic : public tactic { typedef std::pair frame; svector m_stack; ptr_vector m_vars; - expr_sparse_mark m_uncnstr_vars; bool visit(expr * t) { if (m_visited.is_marked(t)) {