mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add warning message for optimization with quantifiers. Fix #1580

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-23 07:20:24 +02:00
parent 0b4e54be38
commit 480e1c4dab
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/opt/opt_context.cpp
View file

@ -265,6 +265,9 @@ namespace opt {
normalize(); normalize();
internalize(); internalize();
update_solver(); update_solver();
if (contains_quantifiers()) {
warning_msg("optimization with quantified constraints is not supported");
}
#if 0 #if 0
if (is_qsat_opt()) { if (is_qsat_opt()) {
return run_qsat_opt(); return run_qsat_opt();
@ -368,7 +371,6 @@ namespace opt {
if (result == l_true && committed) m_optsmt.commit_assignment(index); if (result == l_true && committed) m_optsmt.commit_assignment(index);
if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) { if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) {
throw default_exception("unbounded objectives on quantified constraints is not supported"); throw default_exception("unbounded objectives on quantified constraints is not supported");
result = l_undef;
} }
return result; return result;
} }