#
# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
# ITP engine: interpolation-based model checking using Craig interpolants
#
# Contributor:  Pratik Deshmukh <deshmukhpratik931@gmail.com>
#
# Permission to use, copy, modify, and/or distribute this software for any
# purpose with or without fee is hereby granted, provided that the above
# copyright notice and this permission notice appear in all copies.
#
# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
# Usage in .sby file:
#   [engines]
#   itp [bound] [skip]
#
#   bound: maximum unrolling depth (default: task opt_depth or 20)
#   skip:  number of initial timeframes to skip before checking bad states
#          (default: task opt_skip or 0)
#
# The engine uses the 'itp-bmc' binary which must be either:
#   1. Available in PATH as 'itp-bmc'
#   2. Specified via the ITP_BMC environment variable
#
# Note: This engine currently does not produce counterexample witness traces.
# When a property violation is found (FAIL), no .aiw or .yw trace file is
# generated. Trace generation support is planned for a future version.
#

import os, getopt
from sby_core import SbyProc

def run(mode, task, engine_idx, engine):
    if mode not in ["prove", "bmc"]:
        task.error(f"engine_{engine_idx}: The itp engine is only supported in prove and bmc modes.")

    # Parse options
    args = engine[1:]

    # Defaults from task options
    bound = task.opt_depth
    skip  = task.opt_skip

    # Positional args override: itp [bound] [skip]
    if len(args) > 0:
        try:
            bound = int(args[0])
        except ValueError:
            task.error(f"engine_{engine_idx}: Invalid bound value '{args[0]}', expected integer.")
    if len(args) > 1:
        try:
            skip = int(args[1])
        except ValueError:
            task.error(f"engine_{engine_idx}: Invalid skip value '{args[1]}', expected integer.")
    if len(args) > 2:
        task.error(f"engine_{engine_idx}: Too many arguments to itp engine.")

    if skip >= bound:
        task.error(f"engine_{engine_idx}: skip ({skip}) must be less than bound ({bound}).")

    # Locate binary and derive workdir (for minisat relative path)
    bmc_binary = task.exe_paths["itp-bmc"]
    bmc_workdir = os.path.dirname(os.path.realpath(bmc_binary))

    log = task.log_prefix(f"engine_{engine_idx}")

    # Input: binary AIGER model generated by sby
    aig_src = f"{task.workdir}/model/design_aiger.aig"

    log(f"Running interpolation-based model checker: bound={bound}, skip={skip}")

    proc_status = None

    def output_callback(line):
        nonlocal proc_status
        if "Fixpoint reached" in line:
            log("Interpolation fixpoint reached — property proved SAFE")
            proc_status = "PASS"
        elif "Counterexample found" in line:
            log("Counterexample found — property UNSAFE")
        elif "Safe up to bound" in line:
            log(f"Bounded safety result (fixpoint not reached): {line.strip()}")
            proc_status = "PASS"
        return line

    def exit_callback(retcode):
        nonlocal proc_status

        # If output_callback already determined status (e.g. from output lines),
        # trust that over the exit code
        if proc_status is None:
            proc_status = "PASS" if retcode == 0 else "FAIL"

        task.update_status(proc_status)
        task.summary.set_engine_status(engine_idx, proc_status)
        task.terminate()

    proc = SbyProc(
        task,
        f"engine_{engine_idx}",
        task.model("aig"),
        f"BMC_WORKDIR={bmc_workdir} {bmc_binary} {bound} {aig_src} {skip}",
        logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w"),
    )

    proc.output_callback = output_callback
    proc.register_exit_callback(exit_callback)