@@ -332,8 +332,8 @@ def print_statements(
332
332
code = code .replace (var_name , f"{ computation .name } ({ args_str } )" )
333
333
html_parts .append (f"<code>{ code } </code>" )
334
334
html_parts .append ("</p>" )
335
- val = cost_stmt . validation or cost_val
336
- if val .satisfiable is not None and val .message is not None :
335
+ val = cost_val or cost_stmt . validation
336
+ if val and val .satisfiable is not None and val .message is not None :
337
337
html_parts .append (f'<p><span class="label">Satisfiable:</span> { val .satisfiable } </p>' )
338
338
html_parts .append (f'<p><span class="label">Reason:</span> { val .message } </p>' )
339
339
html_parts .append ("</div>" )
@@ -344,8 +344,8 @@ def print_statements(
344
344
):
345
345
if (param_stmt .formalization is None or param_stmt .formalization .mapping is None ) and only_formalized :
346
346
continue
347
- val = param_stmt . validation or param_val
348
- if val .holds is not None :
347
+ val = param_val or param_stmt . validation
348
+ if val and val .holds is not None :
349
349
holds_tag = "holds" if val .holds else "not-hold"
350
350
else :
351
351
holds_tag = ''
@@ -367,44 +367,12 @@ def print_statements(
367
367
code = code .replace (var_name , f"{ computation .name } ({ args_str } )" )
368
368
html_parts .append (f"<code>{ code } </code>" )
369
369
html_parts .append ("</p>" )
370
- if val .satisfiable is not None and val .message is not None and val .holds is not None :
370
+ if val and val .satisfiable is not None and val .message is not None and val .holds is not None :
371
371
html_parts .append (f'<p><span class="label">Satisfiable:</span> { val .satisfiable } </p>' )
372
372
html_parts .append (f'<p><span class="label">Holds:</span> { val .holds } </p>' )
373
373
html_parts .append (f'<p><span class="label">Reason:</span> { val .message } </p>' )
374
374
html_parts .append ("</div>" )
375
375
376
- # Structure Constraints Rendering
377
- for struct_stmt , struct_val in zip (
378
- statements .structure_constraints or [], validation .structure_constraints or []
379
- ):
380
- if struct_stmt .formalization is None and only_formalized :
381
- continue
382
-
383
- if val .holds is not None :
384
- holds_tag = "holds" if struct_val .holds else "not-hold"
385
- else :
386
- holds_tag = ''
387
- html_parts .append (f'<div class="block { holds_tag } ">' )
388
- html_parts .append (f"<h2>{ struct_stmt .type } </h2>" )
389
- html_parts .append (f'<p><span class="label ">Statement:</span> { struct_stmt .text } </p>' )
390
- if struct_stmt .formalization is None :
391
- html_parts .append ("UNFORMALIZED" )
392
- else :
393
- html_parts .append ('<p><span class="label">Formalization:</span> ' )
394
- func_constr = struct_stmt .formalization
395
- args_str = ", " .join (
396
- f"{ argname } =" + (f"'{ argvalue } '" if isinstance (argvalue , str ) else str (argvalue ))
397
- for argname , argvalue in func_constr .arguments .items ()
398
- )
399
- func_str = f"{ func_constr .function_name } ({ args_str } ) == { func_constr .expected_result } "
400
- html_parts .append (f"<code>{ func_str } </code>" )
401
- html_parts .append ("</p>" )
402
- val = struct_stmt .validation or struct_val
403
- if val .satisfiable is not None and val .holds is not None :
404
- html_parts .append (f'<p><span class="label">Satisfiable:</span> { val .satisfiable } </p>' )
405
- html_parts .append (f'<p><span class="label">Holds:</span> { val .holds } </p>' )
406
- html_parts .append ("</div>" )
407
-
408
376
# Unformalizable Statements Rendering (if applicable)
409
377
if not only_formalized :
410
378
for unf_stmt in statements .unformalizable_statements or []:
@@ -447,8 +415,8 @@ def print_statements(
447
415
)
448
416
code = code .replace (var_name , f"{ computation .name } ({ args_str } )" )
449
417
print (code )
450
- val = cost_stmt . validation or cost_val
451
- if val .satisfiable is not None and val .message is not None :
418
+ val = cost_val or cost_stmt . validation
419
+ if val and val .satisfiable is not None and val .message is not None :
452
420
print (f"Satisfiable: { val .satisfiable } " )
453
421
print (val .message )
454
422
print ("\n -----------------------------------\n " )
@@ -475,36 +443,11 @@ def print_statements(
475
443
)
476
444
code = code .replace (var_name , f"{ computation .name } ({ args_str } )" )
477
445
print (code )
478
- val = param_stmt . validation or param_val
479
- if val .satisfiable is not None and val .message is not None and val .holds is not None :
446
+ val = param_val or param_stmt . validation
447
+ if val and val .satisfiable is not None and val .message is not None and val .holds is not None :
480
448
print (f"Satisfiable: { val .satisfiable } " )
481
449
print (f"Holds: { val .holds } ({ val .message } )" )
482
450
print ("\n -----------------------------------\n " )
483
- for struct_stmt , struct_val in zip (
484
- statements .structure_constraints or [], validation .structure_constraints or []
485
- ):
486
- if struct_stmt .formalization is None and only_formalized :
487
- continue
488
- print ("Type:" , struct_stmt .type )
489
- print ("Statement:" , struct_stmt .text )
490
- print ("Formalization:" , end = " " )
491
- if struct_stmt .formalization is None :
492
- print ("UNFORMALIZED" )
493
- else :
494
- func_constr = struct_stmt .formalization
495
- args_str = ", " .join (
496
- [
497
- f"{ argname } =" + (f"'{ argvalue } '" if isinstance (argvalue , str ) else str (argvalue ))
498
- for argname , argvalue in func_constr .arguments .items ()
499
- ]
500
- )
501
- func_str = f"{ func_constr .function_name } ({ args_str } ) == { func_constr .expected_result } "
502
- print (func_str )
503
- val = struct_stmt .validation or struct_val
504
- if val .satisfiable is not None and val .holds is not None :
505
- print (f"Satisfiable: { val .satisfiable } " )
506
- print (f"Holds: { val .holds } " )
507
- print ("\n -----------------------------------\n " )
508
451
if not only_formalized :
509
452
for unf_stmt in statements .unformalizable_statements or []:
510
453
print ("Type:" , unf_stmt .type )
0 commit comments