Skip to content

Commit c29507d

Browse files
Petr BauchPetr Bauch
Petr Bauch
authored and
Petr Bauch
committed
Lower-case invariant messages
1 parent c740461 commit c29507d

File tree

2 files changed

+29
-29
lines changed

2 files changed

+29
-29
lines changed

‎src/solvers/miniBDD/miniBDD.cpp‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com
2323
void mini_bdd_nodet::remove_reference()
2424
{
2525
PRECONDITION_WITH_DIAGNOSTICS(
26-
reference_counter != 0, "All references were already removed.");
26+
reference_counter != 0, "all references were already removed");
2727

2828
reference_counter--;
2929

@@ -211,10 +211,10 @@ mini_bddt mini_bdd_applyt::APP_rec(const mini_bddt &x, const mini_bddt &y)
211211
{
212212
PRECONDITION_WITH_DIAGNOSTICS(
213213
x.is_initialized() && y.is_initialized(),
214-
"Apply can only be called on initialized BDDs.");
214+
"apply can only be called on initialized BDDs");
215215
PRECONDITION_WITH_DIAGNOSTICS(
216216
x.node->mgr == y.node->mgr,
217-
"Apply can only be called on BDDs with the same manager.");
217+
"apply can only be called on BDDs with the same manager");
218218

219219
// dynamic programming
220220
std::pair<unsigned, unsigned> key(x.node_number(), y.node_number());
@@ -278,10 +278,10 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
278278

279279
INVARIANT(
280280
x.is_initialized() && y.is_initialized(),
281-
"Apply can only be called on initialized BDDs");
281+
"apply can only be called on initialized BDDs");
282282
INVARIANT(
283283
x.node->mgr == y.node->mgr,
284-
"Apply can only be called on BDDs with the same manager");
284+
"apply can only be called on BDDs with the same manager");
285285

286286
switch(t.phase)
287287
{
@@ -309,13 +309,13 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
309309
t.phase=stack_elementt::phaset::FINISH;
310310

311311
INVARIANT(
312-
x.low().var() > t.var, "Applying won't break variable order.");
312+
x.low().var() > t.var, "applying won't break variable order");
313313
INVARIANT(
314-
y.low().var() > t.var, "Applying won't break variable order.");
314+
y.low().var() > t.var, "applying won't break variable order");
315315
INVARIANT(
316-
x.high().var() > t.var, "Applying won't break variable order.");
316+
x.high().var() > t.var, "applying won't break variable order");
317317
INVARIANT(
318-
y.high().var() > t.var, "Applying won't break variable order.");
318+
y.high().var() > t.var, "applying won't break variable order");
319319

320320
stack.push(stack_elementt(t.lr, x.low(), y.low()));
321321
stack.push(stack_elementt(t.hr, x.high(), y.high()));
@@ -326,9 +326,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
326326
t.phase=stack_elementt::phaset::FINISH;
327327

328328
INVARIANT(
329-
x.low().var() > t.var, "Applying won't break variable order.");
329+
x.low().var() > t.var, "applying won't break variable order");
330330
INVARIANT(
331-
x.high().var() > t.var, "Applying won't break variable order.");
331+
x.high().var() > t.var, "applying won't break variable order");
332332

333333
stack.push(stack_elementt(t.lr, x.low(), y));
334334
stack.push(stack_elementt(t.hr, x.high(), y));
@@ -339,9 +339,9 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
339339
t.phase=stack_elementt::phaset::FINISH;
340340

341341
INVARIANT(
342-
y.low().var() > t.var, "Applying won't break variable order.");
342+
y.low().var() > t.var, "applying won't break variable order");
343343
INVARIANT(
344-
y.high().var() > t.var, "Applying won't break variable order.");
344+
y.high().var() > t.var, "applying won't break variable order");
345345

346346
stack.push(stack_elementt(t.lr, x, y.low()));
347347
stack.push(stack_elementt(t.hr, x, y.high()));
@@ -362,7 +362,7 @@ mini_bddt mini_bdd_applyt::APP_non_rec(
362362
}
363363

364364
POSTCONDITION_WITH_DIAGNOSTICS(
365-
u.is_initialized(), "The resulting BDD is initialized.");
365+
u.is_initialized(), "the resulting BDD is initialized");
366366

367367
return u;
368368
}
@@ -390,7 +390,7 @@ mini_bddt mini_bddt::operator^(const mini_bddt &other) const
390390
mini_bddt mini_bddt::operator!() const
391391
{
392392
PRECONDITION_WITH_DIAGNOSTICS(
393-
is_initialized(), "BDD has to be initialized for negation.");
393+
is_initialized(), "BDD has to be initialized for negation");
394394
return node->mgr->True()^*this;
395395
}
396396

@@ -433,12 +433,12 @@ mini_bddt mini_bdd_mgrt::mk(
433433
const mini_bddt &high)
434434
{
435435
PRECONDITION_WITH_DIAGNOSTICS(
436-
var <= var_table.size(), "Cannot make a BDD for an unknown variable.");
436+
var <= var_table.size(), "cannot make a BDD for an unknown variable");
437437
PRECONDITION_WITH_DIAGNOSTICS(
438-
low.var() > var, "Low-edge would break variable ordering.");
438+
low.var() > var, "low-edge would break variable ordering");
439439
// NOLINTNEXTLINE(build/deprecated)
440440
PRECONDITION_WITH_DIAGNOSTICS(
441-
high.var() > var, "High-edge would break variable ordering.");
441+
high.var() > var, "high-edge would break variable ordering");
442442

443443
if(low.node_number()==high.node_number())
444444
return low;
@@ -539,7 +539,7 @@ mini_bddt restrictt::RES(const mini_bddt &u)
539539

540540
PRECONDITION_WITH_DIAGNOSTICS(
541541
u.is_initialized(),
542-
"Restricting variables can only be done in initialized BDDs.");
542+
"restricting variables can only be done in initialized BDDs");
543543
mini_bdd_mgrt *mgr=u.node->mgr;
544544

545545
mini_bddt t;

‎src/solvers/miniBDD/miniBDD.inc‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ inline mini_bddt::mini_bddt(class mini_bdd_nodet *_node):node(_node)
1818

1919
inline mini_bddt &mini_bddt::operator=(const mini_bddt &x)
2020
{
21-
PRECONDITION_WITH_DIAGNOSTICS(&x!=this, "Cannot assign itself.");
21+
PRECONDITION_WITH_DIAGNOSTICS(&x!=this, "cannot assign itself");
2222
clear();
2323

2424
node=x.node;
@@ -35,45 +35,45 @@ inline mini_bddt::~mini_bddt()
3535

3636
inline bool mini_bddt::is_constant() const
3737
{
38-
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized.");
38+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
3939
return node->node_number<=1;
4040
}
4141

4242
inline bool mini_bddt::is_true() const
4343
{
44-
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized.");
44+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
4545
return node->node_number==1;
4646
}
4747

4848
inline bool mini_bddt::is_false() const
4949
{
50-
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized.");
50+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
5151
return node->node_number==0;
5252
}
5353

5454
inline unsigned mini_bddt::var() const
5555
{
56-
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized.");
56+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
5757
return node->var;
5858
}
5959

6060
inline unsigned mini_bddt::node_number() const
6161
{
62-
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized.");
62+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
6363
return node->node_number;
6464
}
6565

6666
inline const mini_bddt &mini_bddt::low() const
6767
{
68-
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized.");
69-
PRECONDITION_WITH_DIAGNOSTICS(node->node_number>=2, "Only non-terminal nodes have out-going edges.");
68+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
69+
PRECONDITION_WITH_DIAGNOSTICS(node->node_number>=2, "only non-terminal nodes have out-going edges");
7070
return node->low;
7171
}
7272

7373
inline const mini_bddt &mini_bddt::high() const
7474
{
75-
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized.");
76-
PRECONDITION_WITH_DIAGNOSTICS(node->node_number>=2, "Only non-terminal nodes have out-going edges.");
75+
PRECONDITION_WITH_DIAGNOSTICS(is_initialized(), "BDD has to be initialized");
76+
PRECONDITION_WITH_DIAGNOSTICS(node->node_number>=2, "only non-terminal nodes have out-going edges");
7777
return node->high;
7878
}
7979

0 commit comments

Comments
 (0)