mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

Fix #3907

Browse source 
Protect spacer from existential quantifiers in the tail.

Some transformations seem to introduce existentially quantified terms.
This commit is contained in:
Arie Gurfinkel 2020-04-11 11:21:13 -04:00
parent 337c07a44c
commit f821ee38e5
3 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz/base/dl_context.cpp
View file

@ -582,6 +582,7 @@ namespace datalog {
m_rule_properties.check_existential_tail(); m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates(); m_rule_properties.check_for_negated_predicates();
m_rule_properties.check_uninterpreted_free(); m_rule_properties.check_uninterpreted_free();
m_rule_properties.check_quantifier_free(exists_k);
break; break;
case BMC_ENGINE: case BMC_ENGINE:
m_rule_properties.collect(r); m_rule_properties.collect(r);

23
src/muz/base/rule_properties.cpp
View file

@ -72,6 +72,27 @@ void rule_properties::check_quantifier_free() {
} }
} }
static const std::string qkind_str(quantifier_kind qkind) {
switch(qkind) {
case forall_k: return "FORALL";
case exists_k: return "EXISTS";
case lambda_k: return "LAMBDA";
}
}
void rule_properties::check_quantifier_free(quantifier_kind qkind) {
for (auto &kv : m_quantifiers) {
if (kv.get_key().get_kind() == qkind) {
rule *r = kv.get_value();
std::stringstream stm;
stm << "cannot process " << qkind_str(qkind) << " quantifier in rule ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
}
void rule_properties::check_for_negated_predicates() { void rule_properties::check_for_negated_predicates() {
if (!m_negative_rules.empty()) { if (!m_negative_rules.empty()) {
rule* r = m_negative_rules[0]; rule* r = m_negative_rules[0];
@ -235,5 +256,7 @@ void rule_properties::reset() {
m_negative_rules.reset(); m_negative_rules.reset();
m_inf_sort.reset(); m_inf_sort.reset();
m_collected = false; m_collected = false;
m_is_monotone = true;
m_generate_proof = false;
} }

2
src/muz/base/rule_properties.h
View file

@ -27,6 +27,7 @@ Notes:
#include "ast/array_decl_plugin.h" #include "ast/array_decl_plugin.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "muz/base/dl_rule.h" #include "muz/base/dl_rule.h"
#include "ast/expr_functors.h"
namespace datalog { namespace datalog {
class rule_properties { class rule_properties {
@ -58,6 +59,7 @@ namespace datalog {
void set_generate_proof(bool generate_proof) { m_generate_proof = generate_proof; } void set_generate_proof(bool generate_proof) { m_generate_proof = generate_proof; }
void collect(rule_set const& r); void collect(rule_set const& r);
void check_quantifier_free(); void check_quantifier_free();
void check_quantifier_free(quantifier_kind qkind);
void check_uninterpreted_free(); void check_uninterpreted_free();
void check_existential_tail(); void check_existential_tail();
void check_for_negated_predicates(); void check_for_negated_predicates();