#!/usr/bin/env python3
"""Existing integer CP-SAT proposer plus exact original-item witness evidence."""
import argparse
import hashlib
import json
import math
from pathlib import Path

import ortools
from ortools.sat.python import cp_model

from subset_sum_reference import MAX_RECORDS, MAX_WORK, audit_subset, calculate, integer, parse

MAX_TOTAL = 2**62 - 1


def propose(record, time_limit=2.0, record_budget=MAX_RECORDS, work_budget=MAX_WORK):
    if type(time_limit) not in (int, float) or not math.isfinite(time_limit) or not 0 < time_limit <= 10:
        raise ValueError('Require finite solver seconds greater than zero and at most ten')
    integer(record_budget, 1, MAX_RECORDS, 'record budget')
    integer(work_budget, 1, MAX_WORK, 'work budget')
    ids, values, target = parse(record)
    independent = calculate(record, record_budget=record_budget, work_budget=work_budget)
    base = dict(ortools_version=ortools.__version__, solver_limits=dict(seconds=float(time_limit), workers=1, random_seed=138),
                adapter_maximum_total=MAX_TOTAL, solver_status=None, proposed_subset=None,
                direct_witness_audit=None, solver_reported_wall_time_seconds=None,
                independently_evaluated_feasibility=independent['exact_feasible'],
                independent_index_subset_count=independent['exact_index_subset_count'], independent_reference=independent,
                source_algorithms_implemented=False, source_proof_verification='not_run', formal_program_verification='not_run',
                interpretation='A checked original-ID subset proves this exact positive-integer instance feasible. Solver infeasibility is a solver report; independent negative evidence requires a complete exact reference. Satisfaction status does not establish uniqueness or count. This adapter accepts only bounded exact integer totals, with no rounding or scale conversion, and models no reconciliation business rules.')
    if sum(values) > MAX_TOTAL or target > MAX_TOTAL:
        return dict(base, status='unsupported_solver_integer_range', independently_certified_feasible=independent['exact_feasible'],
                    reason='Input total or target exceeds the deliberately conservative CP-SAT adapter range')
    model = cp_model.CpModel()
    choices = [model.new_bool_var('choose_' + str(i)) for i in range(len(ids))]
    model.add(sum(value * choice for value, choice in zip(values, choices)) == target)
    validation = model.validate()
    if validation:
        return dict(base, status='model_invalid', solver_status='MODEL_INVALID', reason=validation,
                    independently_certified_feasible=independent['exact_feasible'])
    solver = cp_model.CpSolver()
    solver.parameters.max_time_in_seconds = float(time_limit)
    solver.parameters.num_search_workers = 1
    solver.parameters.random_seed = 138
    status = solver.solve(model)
    subset, audit = None, None
    if status in (cp_model.OPTIMAL, cp_model.FEASIBLE):
        subset = [identity for identity, choice in zip(ids, choices) if solver.value(choice)]
        audit = audit_subset(ids, values, target, subset)
        if not audit['valid']:
            raise ArithmeticError('Solver proposal failed exact original-item witness check')
        if independent['exact_feasible'] is False:
            raise ArithmeticError('Checked positive solver proposal conflicts with complete negative reference')
    if status == cp_model.INFEASIBLE and independent['exact_feasible'] is True:
        raise ArithmeticError('Solver negative report conflicts with complete positive reference')
    return dict(base, status='proposal_checked' if subset is not None else 'no_solver_witness',
                solver_status=solver.status_name(status), proposed_subset=subset, direct_witness_audit=audit,
                independently_certified_feasible=True if audit is not None else independent['exact_feasible'],
                solver_reported_wall_time_seconds=float(solver.wall_time),
                model_text_sha256=hashlib.sha256(str(model.proto).encode()).hexdigest(),
                model_text_hash_interpretation='UTF-8 text of this runtime model proto, not a canonical cross-version encoding')


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('--record-budget', type=int, default=MAX_RECORDS)
    parser.add_argument('--work-budget', type=int, default=MAX_WORK)
    args = parser.parse_args()
    result = propose(json.loads(args.input.read_text()), args.seconds, args.record_budget, args.work_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()