mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-22 20:32:05 +00:00
Code Activity

fix #6571

Browse source 
most solvers don't support background properties
This commit is contained in:
Nikolaj Bjorner 2023-02-07 11:04:58 -08:00
parent 601e506d54
commit 6a2d60a6ba
3 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -577,6 +577,7 @@ namespace datalog {
m_rule_properties.check_uninterpreted_free(); m_rule_properties.check_uninterpreted_free();
m_rule_properties.check_nested_free(); m_rule_properties.check_nested_free();
m_rule_properties.check_infinite_sorts(); m_rule_properties.check_infinite_sorts();
m_rule_properties.check_background_free();
break; break;
case SPACER_ENGINE: case SPACER_ENGINE:
m_rule_properties.collect(r); m_rule_properties.collect(r);
@ -584,6 +585,7 @@ namespace datalog {
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); m_rule_properties.check_quantifier_free(exists_k);
m_rule_properties.check_background_free();
break; break;
case BMC_ENGINE: case BMC_ENGINE:
m_rule_properties.collect(r); m_rule_properties.collect(r);
@ -598,13 +600,16 @@ namespace datalog {
m_rule_properties.collect(r); m_rule_properties.collect(r);
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_background_free();
break; break;
case CLP_ENGINE: case CLP_ENGINE:
m_rule_properties.collect(r); m_rule_properties.collect(r);
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_background_free();
break; break;
case DDNF_ENGINE: case DDNF_ENGINE:
m_rule_properties.check_background_free();
break; break;
case LAST_ENGINE: case LAST_ENGINE:
default: default:

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

@ -139,6 +139,12 @@ void rule_properties::check_nested_free() {
} }
} }
void rule_properties::check_background_free() {
if (m_ctx.get_num_assertions() > 0)
throw default_exception("engine does not support background assertions");
}
void rule_properties::check_existential_tail() { void rule_properties::check_existential_tail() {
ast_mark visited; ast_mark visited;
ptr_vector<expr> todo, tocheck; ptr_vector<expr> todo, tocheck;

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

@ -68,6 +68,7 @@ namespace datalog {
void check_for_negated_predicates(); void check_for_negated_predicates();
void check_nested_free(); void check_nested_free();
void check_infinite_sorts(); void check_infinite_sorts();
void check_background_free();
bool is_monotone() { return m_is_monotone; } bool is_monotone() { return m_is_monotone; }
void operator()(var* n); void operator()(var* n);
void operator()(quantifier* n); void operator()(quantifier* n);