mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

check parameters

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-01-06 16:06:47 -08:00
parent 3fa0e6f3fb
commit f1710e5618
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/opt/opt_context.cpp
View file

@ -53,6 +53,15 @@ namespace opt {
unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) {
maxsmt* ms;
if (w.is_neg()) {
throw default_exception("Negative weight supplied. Weight should be positive");
}
if (w.is_zero()) {
throw default_exception("Zero weight supplied. Weight should be positive");
}
if (!m.is_bool(f)) {
throw default_exception("Soft constraint should be Boolean");
}
if (!m_maxsmts.find(id, ms)) {
ms = alloc(maxsmt, m);
ms->updt_params(m_params);