#!/usr/bin/env python3

import argparse
from pathlib import Path
import csv
import os
import subprocess


def main(args):
    lbs, ubs, rows = dict(), dict(), dict()
    n_bad = 0
    with args.input_file.open("r") as csvfile:
        for row in csv.DictReader(csvfile):
            if row["solver"] == "proofmin-len":
                continue
            key = row["formula"]
            lb = row.get("best_bound")
            ub = row.get("best_proof")
            if lb != "":
                lbs[key] = max(lbs.get(key, 0), int(lb))
            if ub != "":
                ubs[key] = min(ubs.get(key, 10**9), int(ub))
            if key not in rows:
                rows[key] = list()
            rows[key].append(row)
            if lbs.get(key, 0) > ubs.get(key, 10**9):
                n_bad += 1
                print(f'Inconsistency at formula {key}')
                for row in rows[key]:
                    print(row)
    n_tot = len(lbs.keys() | ubs.keys())
    print(f'{n_bad} inconsistencies out of {n_tot} reported formulas')


if __name__ == "__main__":
    parser = argparse.ArgumentParser(description="Validates a synthetic formulas output")
    parser.add_argument(
        "input_file",
        type=Path,
        help="CSV file with the synthetic results"
    )
    args = parser.parse_args()
    main(args)
