## Unit Tests for CDCL Solver
##
## Tests for the Conflict-Driven Clause Learning SAT solver
## adapted for package dependency resolution.
##
## Requirements tested:
## - 5.1: Use PubGrub algorithm with CDCL
## - 5.2: Learn new incompatibility clauses from conflicts
## - 5.3: Backjump to earliest decision causing conflict
## - 5.4: Produce deterministic installation order
## - 5.5: Report minimal conflicting requirements

import std/[unittest, tables, options, sequtils, strutils]
import ../src/nip/resolver/cdcl_solver
import ../src/nip/resolver/cnf_translator
import ../src/nip/resolver/solver_types
import ../src/nip/resolver/variant_types
import ../src/nip/manifest_parser

suite "CDCL Solver Tests":
  
  test "Create CDCL solver":
    ## Test creating a CDCL solver with a CNF formula
    ## Requirements: 5.1
    
    var formula = newCNFFormula()
    discard formula.translateRootRequirement(
      package = "nginx",
      version = SemanticVersion(major: 1, minor: 24, patch: 0),
      variant = newVariantProfile()
    )
    
    var solver = newCDCLSolver(formula)
    
    check solver.decisionLevel == 0
    check solver.assignments.len == 0
    check solver.learnedClauses.len == 0
    check solver.propagationQueue.len == 0
  
  test "Assign variable":
    ## Test assigning a value to a variable
    ## Requirements: 5.1
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let variable = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    solver.assign(variable, true, Decision)
    
    check solver.isAssigned(variable)
    check solver.getValue(variable).isSome
    check solver.getValue(variable).get() == true
    
    let assignment = solver.getAssignment(variable).get()
    check assignment.value == true
    check assignment.assignmentType == Decision
    check assignment.decisionLevel == 0
  
  test "Evaluate literal":
    ## Test evaluating a literal with current assignments
    ## Requirements: 5.1
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let variable = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let positiveLit = makeLiteral(variable, isNegated = false)
    let negativeLit = makeLiteral(variable, isNegated = true)
    
    # Before assignment
    check solver.evaluateLiteral(positiveLit).isNone
    check solver.evaluateLiteral(negativeLit).isNone
    
    # Assign variable to true
    solver.assign(variable, true, Decision)
    
    # After assignment
    check solver.evaluateLiteral(positiveLit).isSome
    check solver.evaluateLiteral(positiveLit).get() == true
    check solver.evaluateLiteral(negativeLit).isSome
    check solver.evaluateLiteral(negativeLit).get() == false
  
  test "Evaluate clause":
    ## Test evaluating a clause with current assignments
    ## Requirements: 5.1
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    # Clause: ¬var1 ∨ var2
    let clause = makeClause(@[
      makeLiteral(var1, isNegated = true),
      makeLiteral(var2, isNegated = false)
    ])
    
    # Before any assignments
    check solver.evaluateClause(clause).isNone
    
    # Assign var1 = false (satisfies ¬var1)
    solver.assign(var1, false, Decision)
    check solver.evaluateClause(clause).isSome
    check solver.evaluateClause(clause).get() == true
    
    # Reset and try different assignment
    solver.unassign(var1)
    
    # Assign var1 = true, var2 = false (falsifies clause)
    solver.assign(var1, true, Decision)
    solver.assign(var2, false, Decision)
    check solver.evaluateClause(clause).isSome
    check solver.evaluateClause(clause).get() == false
  
  test "Detect unit clause":
    ## Test detecting unit clauses for unit propagation
    ## Requirements: 5.1
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    # Clause: ¬var1 ∨ var2
    let clause = makeClause(@[
      makeLiteral(var1, isNegated = true),
      makeLiteral(var2, isNegated = false)
    ])
    
    # Before assignments - not unit
    check solver.isUnitClause(clause).isNone
    
    # Assign var1 = true (makes ¬var1 false, so var2 must be true)
    solver.assign(var1, true, Decision)
    let unitLit = solver.isUnitClause(clause)
    check unitLit.isSome
    check unitLit.get().variable == var2
    check not unitLit.get().isNegated
  
  test "Unit propagation - simple":
    ## Test basic unit propagation
    ## Requirements: 5.1
    
    var formula = newCNFFormula()
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    # Add unit clause: var1
    formula.addClause(makeClause(@[makeLiteral(var1, isNegated = false)]))
    
    var solver = newCDCLSolver(formula)
    
    # Unit propagation should assign var1 = true
    let conflict = solver.unitPropagate()
    check conflict.isNone
    check solver.isAssigned(var1)
    check solver.getValue(var1).get() == true
  
  test "Unit propagation - chain":
    ## Test unit propagation with chained implications
    ## Requirements: 5.1
    
    var formula = newCNFFormula()
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    let var3 = BoolVar(
      package: "pcre",
      version: SemanticVersion(major: 8, minor: 45, patch: 0),
      variant: newVariantProfile()
    )
    
    # Add clauses:
    # 1. var1 (unit clause)
    # 2. ¬var1 ∨ var2 (if var1 then var2)
    # 3. ¬var2 ∨ var3 (if var2 then var3)
    formula.addClause(makeClause(@[makeLiteral(var1, isNegated = false)]))
    formula.addClause(makeClause(@[
      makeLiteral(var1, isNegated = true),
      makeLiteral(var2, isNegated = false)
    ]))
    formula.addClause(makeClause(@[
      makeLiteral(var2, isNegated = true),
      makeLiteral(var3, isNegated = false)
    ]))
    
    var solver = newCDCLSolver(formula)
    
    # Unit propagation should assign all three variables
    let conflict = solver.unitPropagate()
    check conflict.isNone
    check solver.isAssigned(var1)
    check solver.isAssigned(var2)
    check solver.isAssigned(var3)
    check solver.getValue(var1).get() == true
    check solver.getValue(var2).get() == true
    check solver.getValue(var3).get() == true
  
  test "Detect conflict":
    ## Test conflict detection during unit propagation
    ## Requirements: 5.1, 5.2
    
    var formula = newCNFFormula()
    
    let variable = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    # Add contradictory unit clauses:
    # 1. variable (must be true)
    # 2. ¬variable (must be false)
    formula.addClause(makeClause(@[makeLiteral(variable, isNegated = false)]))
    formula.addClause(makeClause(@[makeLiteral(variable, isNegated = true)]))
    
    var solver = newCDCLSolver(formula)
    
    # Unit propagation should detect conflict
    let conflict = solver.unitPropagate()
    check conflict.isSome
  
  test "Solve satisfiable formula":
    ## Test solving a simple satisfiable formula
    ## Requirements: 5.1, 5.4
    
    var formula = newCNFFormula()
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    # Register variables
    discard formula.getOrCreateVarId(var1)
    discard formula.getOrCreateVarId(var2)
    
    # Add clauses:
    # 1. var1 ∨ var2 (at least one must be true)
    formula.addClause(makeClause(@[
      makeLiteral(var1, isNegated = false),
      makeLiteral(var2, isNegated = false)
    ]))
    
    var solver = newCDCLSolver(formula)
    let result = solver.solve()
    
    check result.isSat
    check result.model.len >= 1
  
  test "Solve unsatisfiable formula":
    ## Test solving an unsatisfiable formula
    ## Requirements: 5.1, 5.5
    
    var formula = newCNFFormula()
    
    let variable = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    # Add contradictory clauses:
    # 1. variable (must be true)
    # 2. ¬variable (must be false)
    formula.addClause(makeClause(@[makeLiteral(variable, isNegated = false)]))
    formula.addClause(makeClause(@[makeLiteral(variable, isNegated = true)]))
    
    var solver = newCDCLSolver(formula)
    let result = solver.solve()
    
    check not result.isSat
  
  test "Backjumping":
    ## Test backjumping to earlier decision level
    ## Requirements: 5.3
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    let var3 = BoolVar(
      package: "pcre",
      version: SemanticVersion(major: 8, minor: 45, patch: 0),
      variant: newVariantProfile()
    )
    
    # Make decisions at different levels
    solver.decisionLevel = 1
    solver.assign(var1, true, Decision)
    
    solver.decisionLevel = 2
    solver.assign(var2, true, Decision)
    
    solver.decisionLevel = 3
    solver.assign(var3, true, Decision)
    
    check solver.assignments.len == 3
    check solver.decisionLevel == 3
    
    # Backjump to level 1
    solver.backjump(1)
    
    check solver.decisionLevel == 1
    check solver.assignments.len == 1
    check solver.isAssigned(var1)
    check not solver.isAssigned(var2)
    check not solver.isAssigned(var3)
  
  test "Learn clause from conflict":
    ## Test learning a new clause from conflict analysis
    ## Requirements: 5.2
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    # Create a conflict
    solver.decisionLevel = 1
    solver.assign(var1, true, Decision)
    solver.assign(var2, true, Decision)
    
    let conflictClause = makeClause(@[
      makeLiteral(var1, isNegated = true),
      makeLiteral(var2, isNegated = true)
    ])
    
    let conflict = Conflict(
      clause: conflictClause,
      assignments: solver.assignments.values.toSeq
    )
    
    # Analyze conflict and learn
    let learnedClause = solver.analyzeConflict(conflict)
    
    check learnedClause.literals.len > 0
  
  test "Select unassigned variable":
    ## Test variable selection heuristic
    ## Requirements: 5.1
    
    var formula = newCNFFormula()
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    discard formula.getOrCreateVarId(var1)
    discard formula.getOrCreateVarId(var2)
    
    var solver = newCDCLSolver(formula)
    
    # Both unassigned
    let selected1 = solver.selectUnassignedVariable()
    check selected1.isSome
    
    # Assign one
    solver.assign(var1, true, Decision)
    let selected2 = solver.selectUnassignedVariable()
    check selected2.isSome
    check selected2.get() != var1
    
    # Assign both
    solver.assign(var2, true, Decision)
    let selected3 = solver.selectUnassignedVariable()
    check selected3.isNone
  
  test "String representations":
    ## Test string conversion for debugging
    ## Requirements: 5.5
    
    let variable = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let assignment = SolverAssignment(
      variable: variable,
      value: true,
      assignmentType: Decision,
      decisionLevel: 1,
      antecedent: none(Clause)
    )
    
    let assignmentStr = $assignment
    check assignmentStr.len > 0
    check assignmentStr.contains("nginx")
    check assignmentStr.contains("decision")

  
  test "Conflict analysis - simple conflict":
    ## Test analyzing a simple conflict
    ## Requirements: 5.2
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    # Make a decision
    solver.decisionLevel = 1
    solver.assign(var1, true, Decision)
    
    # Create a conflict clause that conflicts with this decision
    let conflictClause = makeClause(@[
      makeLiteral(var1, isNegated = true)
    ], reason = "Conflict with var1=true")
    
    let conflict = Conflict(
      clause: conflictClause,
      assignments: solver.assignments.values.toSeq
    )
    
    # Analyze the conflict
    let learnedClause = solver.analyzeConflict(conflict)
    
    # Learned clause should prevent this conflict
    check learnedClause.literals.len > 0
  
  test "Conflict analysis - complex conflict":
    ## Test analyzing a conflict with multiple decisions
    ## Requirements: 5.2
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    let var3 = BoolVar(
      package: "pcre",
      version: SemanticVersion(major: 8, minor: 45, patch: 0),
      variant: newVariantProfile()
    )
    
    # Make multiple decisions at different levels
    solver.decisionLevel = 1
    solver.assign(var1, true, Decision)
    
    solver.decisionLevel = 2
    solver.assign(var2, true, Decision)
    
    solver.decisionLevel = 3
    solver.assign(var3, true, Decision)
    
    # Create a conflict
    let conflictClause = makeClause(@[
      makeLiteral(var1, isNegated = true),
      makeLiteral(var2, isNegated = true),
      makeLiteral(var3, isNegated = true)
    ], reason = "All three conflict")
    
    let conflict = Conflict(
      clause: conflictClause,
      assignments: solver.assignments.values.toSeq
    )
    
    # Analyze the conflict
    let learnedClause = solver.analyzeConflict(conflict)
    
    # Learned clause should contain negations of decisions
    check learnedClause.literals.len > 0
  
  test "Backjump level calculation - simple":
    ## Test calculating backjump level for a simple learned clause
    ## Requirements: 5.3
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    # Make decisions at different levels
    solver.decisionLevel = 1
    solver.assign(var1, true, Decision)
    
    solver.decisionLevel = 2
    solver.assign(var2, true, Decision)
    
    # Create a learned clause involving both variables
    let learnedClause = makeClause(@[
      makeLiteral(var1, isNegated = true),
      makeLiteral(var2, isNegated = true)
    ])
    
    # Find backjump level (should be 1, the second-highest level)
    let backjumpLevel = solver.findBackjumpLevel(learnedClause)
    
    check backjumpLevel == 1
  
  test "Backjump level calculation - complex":
    ## Test calculating backjump level with multiple decision levels
    ## Requirements: 5.3
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    let var3 = BoolVar(
      package: "pcre",
      version: SemanticVersion(major: 8, minor: 45, patch: 0),
      variant: newVariantProfile()
    )
    
    let var4 = BoolVar(
      package: "openssl",
      version: SemanticVersion(major: 3, minor: 0, patch: 0),
      variant: newVariantProfile()
    )
    
    # Make decisions at different levels
    solver.decisionLevel = 1
    solver.assign(var1, true, Decision)
    
    solver.decisionLevel = 2
    solver.assign(var2, true, Decision)
    
    solver.decisionLevel = 3
    solver.assign(var3, true, Decision)
    
    solver.decisionLevel = 4
    solver.assign(var4, true, Decision)
    
    # Create a learned clause involving variables at levels 1, 2, and 4
    let learnedClause = makeClause(@[
      makeLiteral(var1, isNegated = true),
      makeLiteral(var2, isNegated = true),
      makeLiteral(var4, isNegated = true)
    ])
    
    # Find backjump level (should be 2, the second-highest level)
    let backjumpLevel = solver.findBackjumpLevel(learnedClause)
    
    check backjumpLevel == 2
  
  test "Backjump state restoration":
    ## Test that backjumping correctly restores solver state
    ## Requirements: 5.3, 5.4
    
    var formula = newCNFFormula()
    var solver = newCDCLSolver(formula)
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: newVariantProfile()
    )
    
    let var2 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    let var3 = BoolVar(
      package: "pcre",
      version: SemanticVersion(major: 8, minor: 45, patch: 0),
      variant: newVariantProfile()
    )
    
    # Make decisions at different levels
    solver.decisionLevel = 1
    solver.assign(var1, true, Decision)
    
    solver.decisionLevel = 2
    solver.assign(var2, true, Decision)
    
    solver.decisionLevel = 3
    solver.assign(var3, true, Decision)
    
    check solver.assignments.len == 3
    check solver.decisionLevel == 3
    
    # Backjump to level 1
    solver.backjump(1)
    
    # Check state is correctly restored
    check solver.decisionLevel == 1
    check solver.assignments.len == 1
    check solver.isAssigned(var1)
    check not solver.isAssigned(var2)
    check not solver.isAssigned(var3)
    check solver.propagationQueue.len == 0