#!/usr/bin/env python3
"""Existing CP-SAT proposer plus bounded independent unit-job evidence."""
import argparse
import hashlib
import json
import math
from pathlib import Path

import ortools
from ortools.sat.python import cp_model

from three_machine_reference import MAX_STATES, MAX_TRANSITIONS, audit_slots, calculate, integer, parse


def propose(record, time_limit=2.0, state_budget=MAX_STATES, transition_budget=MAX_TRANSITIONS):
    if type(time_limit) not in (int, float) or not math.isfinite(time_limit) or not 0 < time_limit <= 10:
        raise ValueError('Require a finite solver limit greater than zero and at most ten seconds')
    integer(state_budget, 1, MAX_STATES, 'state budget')
    integer(transition_budget, 1, MAX_TRANSITIONS, 'transition budget')
    jobs, pairs, _, _, _, deadline = parse(record)
    n = len(jobs)
    model = cp_model.CpModel()
    starts = [model.new_int_var(0, n - 1, 'start_' + str(i)) for i in range(n)]
    intervals = [model.new_fixed_size_interval_var(start, 1, 'job_' + str(i)) for i, start in enumerate(starts)]
    model.add_cumulative(intervals, [1] * n, 3)
    for a, b in pairs:
        model.add(starts[b] >= starts[a] + 1)
    makespan = model.new_int_var(1, n, 'makespan')
    model.add_max_equality(makespan, [start + 1 for start in starts])
    model.minimize(makespan)
    solver = cp_model.CpSolver()
    solver.parameters.max_time_in_seconds = float(time_limit)
    solver.parameters.num_search_workers = 1
    solver.parameters.random_seed = 124
    status = solver.solve(model)
    slots, witness, objective, solver_bound = None, None, None, None
    if status in (cp_model.OPTIMAL, cp_model.FEASIBLE):
        objective = int(solver.value(makespan))
        slots = [[] for _ in range(objective)]
        for job, start in zip(jobs, starts):
            slots[int(solver.value(start))].append(job)
        witness = audit_slots(jobs, pairs, slots)
        if not witness['valid'] or witness['makespan'] != objective:
            raise ArithmeticError('CP-SAT proposal failed direct witness checks')
        solver_bound = float(solver.best_objective_bound)
    checked_record = dict(record, proposed_slots=slots) if slots is not None else record
    independent = calculate(checked_record, state_budget, transition_budget)
    consistent = None if slots is None or independent['exact_optimum'] is None else objective == independent['exact_optimum']
    if consistent is False and status == cp_model.OPTIMAL:
        raise ArithmeticError('CP-SAT optimal status conflicts with finite independent optimum')
    return dict(status='proposal_checked' if slots is not None else 'no_solver_witness', ortools_version=ortools.__version__,
                solver_status=solver.status_name(status), proposed_slots=slots, direct_witness_audit=witness,
                input_proposed_schedule_audit=audit_slots(jobs, pairs, record['proposed_slots']) if 'proposed_slots' in record else None,
                solver_objective=objective, solver_reported_lower_bound=solver_bound,
                solver_reported_wall_time_seconds=float(solver.wall_time),
                solver_limits=dict(seconds=float(time_limit), workers=1, random_seed=124),
                independently_certified_optimum=independent['exact_optimum'], proposal_matches_independent_optimum=consistent,
                independently_evaluated_deadline=independent['feasibility_by_deadline'], independent_reference=independent,
                model_text_sha256=hashlib.sha256(str(model.proto).encode()).hexdigest(),
                model_text_hash_interpretation='UTF-8 text of this runtime model proto, not a cross-version canonical encoding.',
                source_polynomial_algorithm_implemented=False, source_proof_verification='not_run', formal_program_verification='not_run',
                interpretation='CP-SAT status and bound are solver reports. Independent finite optimality requires completed reference search or a directly checked schedule attaining its elementary lower bound. No performance comparison or broader model guarantee is inferred.')


def main():
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument('input', type=Path)
    parser.add_argument('--output', type=Path)
    parser.add_argument('--seconds', type=float, default=2.0)
    parser.add_argument('--state-budget', type=int, default=MAX_STATES)
    parser.add_argument('--transition-budget', type=int, default=MAX_TRANSITIONS)
    args = parser.parse_args()
    result = propose(json.loads(args.input.read_text()), args.seconds, args.state_budget, args.transition_budget)
    body = json.dumps(result, indent=2, allow_nan=False) + '\n'
    if args.output:
        with args.output.open('x') as stream:
            stream.write(body)
    else:
        print(body, end='')


if __name__ == '__main__':
    main()