From 8357210d3cd9f03bc29c3d87e0a12a29a020afe8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 1 Dec 2017 01:07:41 -0800
Subject: [PATCH] fix lack of warning/error for unbounded objectives in context
of quantifiers #1382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/opt_context.cpp | 19 +++++++++++++++----
src/opt/opt_context.h | 3 ++-
src/opt/optsmt.cpp | 8 ++++++++
src/opt/optsmt.h | 2 ++
4 files changed, 27 insertions(+), 5 deletions(-)
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 8d73ea7c8..3d296d92b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -345,12 +345,24 @@ namespace opt {
fix_model(mdl);
}
+ bool context::contains_quantifiers() const {
+ for (expr* f : m_hard_constraints) {
+ if (has_quantifiers(f)) return true;
+ }
+ return false;
+ }
+
+
lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
if (scoped) get_solver().push();
lbool result = m_optsmt.lex(index, is_max);
if (result == l_true) m_optsmt.get_model(m_model, m_labels);
if (scoped) get_solver().pop(1);
if (result == l_true && committed) m_optsmt.commit_assignment(index);
+ if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) {
+ throw default_exception("unbounded objectives on quantified constraints is not supported");
+ result = l_undef;
+ }
return result;
}
@@ -646,8 +658,7 @@ namespace opt {
expr_fast_mark1 visited;
is_bv proc(m);
try {
- for (unsigned i = 0; i < m_objectives.size(); ++i) {
- objective & obj = m_objectives[i];
+ for (objective& obj : m_objectives) {
if (obj.m_type != O_MAXSMT) return false;
maxsmt& ms = *m_maxsmts.find(obj.m_id);
for (unsigned j = 0; j < ms.size(); ++j) {
@@ -658,8 +669,8 @@ namespace opt {
for (unsigned i = 0; i < sz; i++) {
quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
}
- for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
- quick_for_each_expr(proc, visited, m_hard_constraints[i].get());
+ for (expr* f : m_hard_constraints) {
+ quick_for_each_expr(proc, visited, f);
}
}
catch (is_bv::found) {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index ad40db074..1ae60ef87 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -233,13 +233,14 @@ namespace opt {
private:
lbool execute(objective const& obj, bool committed, bool scoped);
- lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
+ lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
lbool execute_maxsat(symbol const& s, bool committed, bool scoped);
lbool execute_lex();
lbool execute_box();
lbool execute_pareto();
lbool adjust_unknown(lbool r);
bool scoped_lex();
+ bool contains_quantifiers() const;
expr_ref to_expr(inf_eps const& n);
void to_exprs(inf_eps const& n, expr_ref_vector& es);
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index f8f75fbfd..3258cb33d 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -161,6 +161,14 @@ namespace opt {
return l_true;
}
+ bool optsmt::is_unbounded(unsigned obj_index, bool is_maximize) {
+ if (is_maximize) {
+ return !m_upper[obj_index].is_finite();
+ }
+ else {
+ return !m_lower[obj_index].is_finite();
+ }
+ }
lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) {
arith_util arith(m);
diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h
index 921352898..93fa3f624 100644
--- a/src/opt/optsmt.h
+++ b/src/opt/optsmt.h
@@ -49,6 +49,8 @@ namespace opt {
lbool lex(unsigned obj_index, bool is_maximize);
+ bool is_unbounded(unsigned obj_index, bool is_maximize);
+
unsigned add(app* t);
void updt_params(params_ref& p);