From 655b44c07bcaa30a0652dc23a74ac7277d381439 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 15 Aug 2015 00:48:22 +0200
Subject: [PATCH] make :weight understand both decimal and integral values,
remove dweight, remove deprecated commands for optimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/opt_cmds.cpp | 171 +++++++++++++-------------
src/parsers/smt2/smt2parser.cpp | 1 +
src/sat/sat_solver/inc_sat_solver.cpp | 2 +-
src/smt/theory_arith_aux.h | 3 +-
4 files changed, 90 insertions(+), 87 deletions(-)
diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index 01324fc67..7041265de 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -39,80 +39,6 @@ static opt::context& get_opt(cmd_context& cmd) {
return dynamic_cast<opt::context&>(*cmd.get_opt());
}
-class assert_weighted_cmd : public cmd {
- unsigned m_idx;
- expr* m_formula;
- rational m_weight;
- symbol m_id;
-
-public:
- assert_weighted_cmd():
- cmd("assert-weighted"),
- m_idx(0),
- m_formula(0),
- m_weight(0)
- {}
-
- virtual ~assert_weighted_cmd() {
- }
-
- virtual void reset(cmd_context & ctx) {
- m_idx = 0;
- m_formula = 0;
- m_id = symbol::null;
- }
-
- virtual char const * get_usage() const { return "<formula> <rational-weight>"; }
- virtual char const * get_descr(cmd_context & ctx) const { return "assert soft constraint with weight"; }
- virtual unsigned get_arity() const { return VAR_ARITY; }
-
- // command invocation
- virtual void prepare(cmd_context & ctx) {}
- virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
- switch(m_idx) {
- case 0: return CPK_EXPR;
- case 1: return CPK_NUMERAL;
- default: return CPK_SYMBOL;
- }
- }
- virtual void set_next_arg(cmd_context & ctx, rational const & val) {
- SASSERT(m_idx == 1);
- if (!val.is_pos()) {
- throw cmd_exception("Invalid weight. Weights must be positive.");
- }
- m_weight = val;
- ++m_idx;
- }
-
- virtual void set_next_arg(cmd_context & ctx, expr * t) {
- SASSERT(m_idx == 0);
- if (!ctx.m().is_bool(t)) {
- throw cmd_exception("Invalid type for expression. Expected Boolean type.");
- }
- m_formula = t;
- ++m_idx;
- }
-
- virtual void set_next_arg(cmd_context & ctx, symbol const& s) {
- SASSERT(m_idx > 1);
- m_id = s;
- ++m_idx;
- }
-
- virtual void failure_cleanup(cmd_context & ctx) {
- reset(ctx);
- }
-
- virtual void execute(cmd_context & ctx) {
- get_opt(ctx).add_soft_constraint(m_formula, m_weight, m_id);
- reset(ctx);
- }
-
- virtual void finalize(cmd_context & ctx) {
- }
-
-};
-
class assert_soft_cmd : public parametric_cmd {
unsigned m_idx;
@@ -148,7 +74,6 @@ public:
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
p.insert("weight", CPK_NUMERAL, "(default: 1) penalty of not satisfying constraint.");
- p.insert("dweight", CPK_DECIMAL, "(default: 1.0) penalty as double of not satisfying constraint.");
p.insert("id", CPK_SYMBOL, "(default: null) partition identifier for soft constraints.");
}
@@ -168,9 +93,6 @@ public:
virtual void execute(cmd_context & ctx) {
symbol w("weight");
rational weight = ps().get_rat(symbol("weight"), rational(0));
- if (weight.is_zero()) {
- weight = ps().get_rat(symbol("dweight"), rational(0));
- }
if (weight.is_zero()) {
weight = rational::one();
}
@@ -217,6 +139,20 @@ public:
}
};
+
+
+void install_opt_cmds(cmd_context & ctx) {
+ ctx.insert(alloc(assert_soft_cmd));
+ ctx.insert(alloc(min_maximize_cmd, true));
+ ctx.insert(alloc(min_maximize_cmd, false));
+}
+
+
+#if 0
+ ctx.insert(alloc(optimize_cmd));
+ ctx.insert(alloc(assert_weighted_cmd));
+
+
class optimize_cmd : public parametric_cmd {
public:
optimize_cmd():
@@ -329,13 +265,78 @@ private:
}
};
+class assert_weighted_cmd : public cmd {
+ unsigned m_idx;
+ expr* m_formula;
+ rational m_weight;
+ symbol m_id;
+public:
+ assert_weighted_cmd():
+ cmd("assert-weighted"),
+ m_idx(0),
+ m_formula(0),
+ m_weight(0)
+ {}
-void install_opt_cmds(cmd_context & ctx) {
- ctx.insert(alloc(assert_weighted_cmd));
- ctx.insert(alloc(assert_soft_cmd));
- ctx.insert(alloc(min_maximize_cmd, true));
- ctx.insert(alloc(min_maximize_cmd, false));
- ctx.insert(alloc(optimize_cmd));
-}
+ virtual ~assert_weighted_cmd() {
+ }
+ virtual void reset(cmd_context & ctx) {
+ m_idx = 0;
+ m_formula = 0;
+ m_id = symbol::null;
+ }
+
+ virtual char const * get_usage() const { return "<formula> <rational-weight>"; }
+ virtual char const * get_descr(cmd_context & ctx) const { return "assert soft constraint with weight"; }
+ virtual unsigned get_arity() const { return VAR_ARITY; }
+
+ // command invocation
+ virtual void prepare(cmd_context & ctx) {}
+ virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
+ switch(m_idx) {
+ case 0: return CPK_EXPR;
+ case 1: return CPK_NUMERAL;
+ default: return CPK_SYMBOL;
+ }
+ }
+ virtual void set_next_arg(cmd_context & ctx, rational const & val) {
+ SASSERT(m_idx == 1);
+ if (!val.is_pos()) {
+ throw cmd_exception("Invalid weight. Weights must be positive.");
+ }
+ m_weight = val;
+ ++m_idx;
+ }
+
+ virtual void set_next_arg(cmd_context & ctx, expr * t) {
+ SASSERT(m_idx == 0);
+ if (!ctx.m().is_bool(t)) {
+ throw cmd_exception("Invalid type for expression. Expected Boolean type.");
+ }
+ m_formula = t;
+ ++m_idx;
+ }
+
+ virtual void set_next_arg(cmd_context & ctx, symbol const& s) {
+ SASSERT(m_idx > 1);
+ m_id = s;
+ ++m_idx;
+ }
+
+ virtual void failure_cleanup(cmd_context & ctx) {
+ reset(ctx);
+ }
+
+ virtual void execute(cmd_context & ctx) {
+ get_opt(ctx).add_soft_constraint(m_formula, m_weight, m_id);
+ reset(ctx);
+ }
+
+ virtual void finalize(cmd_context & ctx) {
+ }
+
+};
+
+#endif
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 785f578f3..ebed375d0 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -387,6 +387,7 @@ namespace smt2 {
void check_keyword(char const * msg) { if (!curr_is_keyword()) throw parser_exception(msg); }
void check_string(char const * msg) { if (!curr_is_string()) throw parser_exception(msg); }
void check_int(char const * msg) { if (!curr_is_int()) throw parser_exception(msg); }
+ void check_int_or_float(char const * msg) { if (!curr_is_int() || !curr_is_float()) throw parser_exception(msg); }
void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
void error(unsigned line, unsigned pos, char const * msg) {
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 742a02d3c..e06267208 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -113,7 +113,7 @@ public:
r = initialize_soft_constraints();
if (r != l_true) return r;
- m_solver.display_dimacs(std::cout);
+ //m_solver.display_dimacs(std::cout);
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
switch (r) {
case l_true:
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index ebdd1386c..60af00195 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1556,7 +1556,8 @@ namespace smt {
SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain));
- if (!picked_var) {
+ if (!picked_var && r.size() > 1) {
+ TRACE("opt", tout << "no variable picked\n";);
best_efforts++;
}
else if (curr_x_i == null_theory_var) {