mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
test output predicates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
65a202873f
commit
9b34350646
|
@ -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();
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -38,7 +38,6 @@ class elim_uncnstr_tactic : public tactic {
|
|||
typedef std::pair<expr *, unsigned> frame;
|
||||
svector<frame> m_stack;
|
||||
ptr_vector<app> m_vars;
|
||||
expr_sparse_mark m_uncnstr_vars;
|
||||
|
||||
bool visit(expr * t) {
|
||||
if (m_visited.is_marked(t)) {
|
||||
|
|
Loading…
Reference in a new issue