Skip to content

Commit fffa596

Browse files
authored
Merge pull request #494 from diffblue/ranking-witness-trace
ebmc: generate a witness that a given candidate isn't a ranking function
2 parents da710d1 + a9c5424 commit fffa596

File tree

4 files changed

+27
-8
lines changed

4 files changed

+27
-8
lines changed
Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
CORE
22
counter2.sv
3-
--ranking-function counter
3+
--ranking-function counter --numbered-trace
44
^\[main\.property\.p0\] always s_eventually main.counter == 10: INCONCLUSIVE$
5+
^main\.counter@0 = .*$
6+
^main\.counter@1 = .*$
57
^EXIT=10$
68
^SIGNAL=0$
79
--

src/ebmc/neural_liveness.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -307,12 +307,14 @@ tvt neural_livenesst::verify(
307307
solver_factory,
308308
message.get_message_handler());
309309

310-
if(result.is_true())
310+
property.witness_trace = std::move(result.second);
311+
312+
if(result.first.is_true())
311313
property.proved();
312314
else
313315
property.inconclusive();
314316

315-
return result;
317+
return result.first;
316318
}
317319

318320
int do_neural_liveness(

src/ebmc/ranking_function.cpp

Lines changed: 18 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,9 @@ int do_ranking_function(
114114
solver_factory,
115115
message_handler);
116116

117-
if(result.is_true())
117+
property.witness_trace = std::move(result.second);
118+
119+
if(result.first.is_true())
118120
{
119121
property.proved();
120122
}
@@ -129,7 +131,7 @@ int do_ranking_function(
129131
return properties.all_properties_proved() ? 0 : 10;
130132
}
131133

132-
tvt is_ranking_function(
134+
std::pair<tvt, std::optional<trans_tracet>> is_ranking_function(
133135
const transition_systemt &transition_system,
134136
const exprt &property,
135137
const exprt &ranking_function,
@@ -188,13 +190,25 @@ tvt is_ranking_function(
188190
message.result()
189191
<< "SAT: inductive proof failed, ranking function check is inconclusive"
190192
<< messaget::eom;
191-
return tvt::unknown();
193+
194+
{
195+
exprt::operandst timeframe_handles{true_exprt(), false_exprt()};
196+
197+
auto witness_trace = compute_trans_trace(
198+
timeframe_handles,
199+
solver,
200+
2, // number of timeframes
201+
ns,
202+
transition_system.main_symbol->name);
203+
204+
return {tvt::unknown(), witness_trace};
205+
}
192206

193207
case decision_proceduret::resultt::D_UNSATISFIABLE:
194208
message.result()
195209
<< "UNSAT: inductive proof successful, function is a ranking function"
196210
<< messaget::eom;
197-
return tvt(true);
211+
return {tvt(true), std::nullopt};
198212

199213
case decision_proceduret::resultt::D_ERROR:
200214
throw ebmc_errort() << "Error from decision procedure";

src/ebmc/ranking_function.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
1818

1919
class exprt;
2020
class transition_systemt;
21+
class trans_tracet;
2122

2223
int do_ranking_function(const cmdlinet &, message_handlert &);
2324

@@ -26,7 +27,7 @@ exprt parse_ranking_function(
2627
const transition_systemt &,
2728
message_handlert &);
2829

29-
tvt is_ranking_function(
30+
std::pair<tvt, std::optional<trans_tracet>> is_ranking_function(
3031
const transition_systemt &,
3132
const exprt &property,
3233
const exprt &ranking_function,

0 commit comments

Comments
 (0)