Skip to content
Snippets Groups Projects
Unverified Commit 092e923c authored by Andrea Franchini's avatar Andrea Franchini
Browse files

Add solve time to result

parent af69733d
No related branches found
No related tags found
No related merge requests found
__version__ = '2.6.0'
__version__ = '2.6.1'
......@@ -29,7 +29,7 @@
<li class="message is-danger">
<div class="message-header">
<p>
Unsatisfied
Unsatisfied ({{req.time}}s)
</p>
<p>
<span class="tag is-family-monospace is-danger is-light">
......@@ -49,7 +49,7 @@
<li class="message is-success sat-req is-hidden">
<div class="message-header">
<p>
Satisfied
Satisfied ({{req.time}}s)
</p>
<p>
<span class="tag is-family-monospace is-success is-light">
......
......@@ -3,7 +3,7 @@ from dataclasses import dataclass
from typing import Literal
from z3 import (Context, DatatypeSortRef, ExprRef, FuncDeclRef, Solver,
SortRef, sat)
SortRef, Z3Exception)
from .intermediate_model.doml_element import IntermediateModel
from .mc_result import MCResult, MCResults
......@@ -166,14 +166,18 @@ class IntermediateModelChecker:
req_type, req_err_desc_fn = req.error_description
req_is_sat = MCResult.from_z3result(res, flipped=req.flipped)
req_id = req.assert_name
try:
req_time = self.solver.statistics().get_key_value("time")
except Z3Exception:
req_time = "???"
results.append((
req_is_sat,
req_type,
req_err_desc_fn(self.solver, self.smt_sorts, self.intermediate_model) if req_is_sat else "",
req_id,
req.description
# if res == sat else "" # not needed since we're try/catching model() errors
# in each requirement now
req.description,
req_time
))
self.solver.pop()
......
......@@ -83,7 +83,7 @@ def verify_model(
req_store,
threads=threads,
user_str_values=user_req_str_consts,
disable_multithreading=True #(threads == 1)
disable_multithreading=(threads == 1)
)
res = results.summarize()
......
......@@ -35,22 +35,22 @@ class MCResults:
SATISFIED_MSG = "All requirements are satisfied."
def __init__(self, results: list[tuple[MCResult, Literal["BUILTIN", "USER"], str, str, str]]):
"""It receives a list of tuples (result, type, error message, id)"""
"""It receives a list of tuples (result, type, error message, id, desc, time)"""
self.results = results
def summarize(self) -> dict[str, any]:
some_unsat = any(res == MCResult.unsat for res, _, _, _, _ in self.results)
some_dontknow = any(res == MCResult.dontknow for res, _, _, _, _ in self.results)
some_unsat = any(res == MCResult.unsat for res, _, _, _, _, _ in self.results)
some_dontknow = any(res == MCResult.dontknow for res, _, _, _, _, _ in self.results)
if some_unsat:
builtin_err_msgs = [
(id, msg) for res, type, msg, id, _ in self.results if res == MCResult.unsat and type == "BUILTIN"]
(id, msg, time) for res, type, msg, id, _, time in self.results if res == MCResult.unsat and type == "BUILTIN"]
user_err_msgs = [
(id, msg) for res, type, msg, id, _ in self.results if res == MCResult.unsat and type == "USER"]
(id, msg, time) for res, type, msg, id, _, time in self.results if res == MCResult.unsat and type == "USER"]
# Print to text (instead of HTML)
builtin_err_msg = "\n".join([f"[{id}] {msg}" for id, msg in builtin_err_msgs])
user_err_msg = "\n".join([f"[{id}] {msg}" for id, msg in user_err_msgs])
builtin_err_msg = "\n".join([f"[{id}][{time}s] {msg}" for id, msg, time in builtin_err_msgs])
user_err_msg = "\n".join([f"[{id}][{time}s] {msg}" for id, msg, time in user_err_msgs])
err_msg = ""
if builtin_err_msgs:
......@@ -66,9 +66,10 @@ class MCResults:
"type": type,
"message": msg,
"result": res.name,
"description": desc
"description": desc,
"time": time
}
for res, type, msg, id, desc in self.results
for res, type, msg, id, desc, time in self.results
]
return {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment