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

make :weight understand both decimal and integral values, remove dweight, remove deprecated commands for optimization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-15 00:48:22 +02:00
parent 94d83b7be9
commit 655b44c07b
4 changed files with 90 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

171
src/opt/opt_cmds.cpp
View file

@ -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

1
src/parsers/smt2/smt2parser.cpp
View file

@ -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) {

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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:

3
src/smt/theory_arith_aux.h
View file

@ -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) {