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

adjust parsing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-03 14:10:07 -08:00
parent 18815e3e53
commit 838a32206c
1 changed files with 8 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/opt/opt_cmds.cpp
View file

@ -148,15 +148,18 @@ public:
virtual char const * get_main_descr() const { return "assert soft constraint with optional weight and identifier"; }
// command invocation
virtual void prepare(cmd_context & ctx) {}
virtual void prepare(cmd_context & ctx) {
reset(ctx);
}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
if (m_idx == 0) return CPK_EXPR;
return parametric_cmd::next_arg_kind(ctx);
}
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
p.insert("weight", CPK_UINT, "(default: 1) penalty of not satisfying constraint.");
p.insert("dweight", CPK_DOUBLE, "(default: 1.0) penalty as double of not satisfying constraint.");
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.");
}
@ -175,14 +178,9 @@ public:
virtual void execute(cmd_context & ctx) {
symbol w("weight");
rational weight = rational(ps().get_uint(symbol("weight"), 0));
rational weight = ps().get_rat(symbol("weight"), rational(0));
if (weight.is_zero()) {
double d = ps().get_double(symbol("dweight"), 0.0);
if (d != 0.0) {
std::stringstream strm;
strm << d;
weight = rational(strm.str().c_str());
}
weight = ps().get_rat(symbol("dweight"), rational(0));
}
if (weight.is_zero()) {
weight = rational::one();