// lintq.dl -- Souffle-LintQ analysis rules (from the proposal).
// Consumes the EDB facts emitted by ast_to_facts.py.

// --- Basic Control Flow & AST Facts (EDB) ---
.decl Stmt(id: number, line: number, func: symbol)
.input Stmt

.decl CFGEdge(from_stmt: number, to_stmt: number)
.input CFGEdge

.decl Assign(stmt: number, dest_var: symbol, src_var: symbol)
.input Assign

// --- Quantum Domain Facts (EDB) ---
.decl CircuitAlloc(stmt: number, var_name: symbol, num_qubits: number, num_clbits: number)
.input CircuitAlloc

.decl GateOp(stmt: number, circuit_var: symbol, gate_name: symbol, qubit_idx: number)
.input GateOp

.decl MeasureOp(stmt: number, circuit_var: symbol, qubit_idx: number, clbit_idx: number)
.input MeasureOp

.decl CircuitCall(stmt: number, method: symbol, target_var: symbol, arg_var: symbol)
.input CircuitCall

// ---------------------------------------------------------------------
// Analysis 1: OpAfterMeas
// Detects a unitary gate executed on qubit Q after Q has been measured.
// ---------------------------------------------------------------------
.decl ReachableAfterMeasure(circuit: symbol, qubit: number, stmt: number)
.decl WarnOpAfterMeas(stmt: number, circuit: symbol, gate: symbol, qubit: number, meas_stmt: number)
.output WarnOpAfterMeas

ReachableAfterMeasure(c, q, next_stmt) :-
    MeasureOp(meas_stmt, c, q, _),
    CFGEdge(meas_stmt, next_stmt).

ReachableAfterMeasure(c, q, next_stmt) :-
    ReachableAfterMeasure(c, q, curr_stmt),
    CFGEdge(curr_stmt, next_stmt).

WarnOpAfterMeas(gate_stmt, c, gate, q, meas_stmt) :-
    ReachableAfterMeasure(c, q, gate_stmt),
    GateOp(gate_stmt, c, gate, q),
    MeasureOp(meas_stmt, c, q, _),
    gate != "reset".

// ---------------------------------------------------------------------
// Analysis 2: DoubleMeas
// Detects two consecutive measurements of qubit Q without state changes.
// ---------------------------------------------------------------------
.decl ModifiedQubit(c: symbol, q: number, stmt: number)
ModifiedQubit(c, q, stmt) :- GateOp(stmt, c, _, q).

.decl MeasReachesMeas(c: symbol, q: number, first_meas: number, curr_stmt: number)
.decl WarnDoubleMeas(second_meas: number, circuit: symbol, qubit: number, first_meas: number)
.output WarnDoubleMeas

MeasReachesMeas(c, q, meas1, next_stmt) :-
    MeasureOp(meas1, c, q, _),
    CFGEdge(meas1, next_stmt).

MeasReachesMeas(c, q, meas1, next_stmt) :-
    MeasReachesMeas(c, q, meas1, curr_stmt),
    CFGEdge(curr_stmt, next_stmt),
    !ModifiedQubit(c, q, curr_stmt).

WarnDoubleMeas(meas2, c, q, meas1) :-
    MeasReachesMeas(c, q, meas1, meas2),
    MeasureOp(meas2, c, q, _),
    meas1 != meas2.

// ---------------------------------------------------------------------
// Analysis 3: GhostCompose
// Detects qc.compose(...) calls where the return value is discarded.
// ---------------------------------------------------------------------
.decl AssignedStmt(stmt_id: number)
AssignedStmt(stmt) :- Assign(stmt, _, _).

.decl WarnGhostCompose(stmt: number, circuit: symbol, subcircuit: symbol)
.output WarnGhostCompose

WarnGhostCompose(stmt, c, sub_c) :-
    CircuitCall(stmt, "compose", c, sub_c),
    !AssignedStmt(stmt).