## Property-Based Tests for Resolution Completeness
##
## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
## **Validates: Requirements 5.1, 5.4**
##
## Property: For any satisfiable dependency graph, the resolver SHALL find a solution
##
## This property verifies that:
## 1. If a solution exists, the resolver finds it
## 2. The solution satisfies all dependencies
## 3. The installation order respects dependency relationships
## 4. The resolver is deterministic (same input → same output)

import std/[unittest, tables, sets, options, random, sequtils]
import ../src/nip/resolver/[
  resolver_integration,
  dependency_graph,
  variant_types,
  cnf_translator,
  cdcl_solver
]
import ../src/nip/manifest_parser

# --- Test Data Generators ---

proc generateVariant(rng: var Rand, numFlags: int = 0): VariantProfile =
  ## Generate a random variant profile
  var domains = initTable[string, VariantDomain]()
  
  if numFlags > 0:
    var flagSet = initHashSet[string]()
    for i in 0..<numFlags:
      flagSet.incl("flag" & $i)
    
    domains["features"] = VariantDomain(
      name: "features",
      exclusivity: NonExclusive,
      flags: flagSet
    )
  
  result = VariantProfile(
    domains: domains,
    hash: "hash-" & $rng.rand(1000000)
  )

proc generateAcyclicGraph(rng: var Rand, numPackages: int): DependencyGraph =
  ## Generate a random acyclic dependency graph
  ## Uses a layered approach to ensure no cycles
  result = newDependencyGraph()
  
  if numPackages == 0:
    return
  
  # Create packages in layers (layer 0 has no dependencies)
  let layerSize = max(1, numPackages div 3)
  var packages: seq[seq[PackageTermId]] = @[]
  var currentLayer: seq[PackageTermId] = @[]
  
  for i in 0..<numPackages:
    let variant = generateVariant(rng, numFlags = 0)
    let packageName = "pkg" & $i
    let termId = createTermId(packageName, variant.hash)
    
    result.addTerm(PackageTerm(
      id: termId,
      packageName: packageName,
      variantProfile: variant,
      optional: false,
      source: "test"
    ))
    
    currentLayer.add(termId)
    
    # Start new layer
    if currentLayer.len >= layerSize:
      packages.add(currentLayer)
      currentLayer = @[]
  
  # Add remaining packages to last layer
  if currentLayer.len > 0:
    packages.add(currentLayer)
  
  # Add edges between layers (only from higher layer to lower layer)
  for layerIdx in 1..<packages.len:
    for termId in packages[layerIdx]:
      # Each package depends on 0-2 packages from previous layer
      let numDeps = rng.rand(min(2, packages[layerIdx - 1].len))
      
      for _ in 0..<numDeps:
        let depIdx = rng.rand(packages[layerIdx - 1].len - 1)
        let depTermId = packages[layerIdx - 1][depIdx]
        
        result.addEdge(DependencyEdge(
          fromTerm: termId,
          toTerm: depTermId,
          dependencyType: Required
        ))

proc generateChainGraph(numPackages: int): DependencyGraph =
  ## Generate a simple chain: P0 -> P1 -> P2 -> ... -> Pn
  result = newDependencyGraph()
  
  var prevTermId: Option[PackageTermId] = none(PackageTermId)
  
  for i in 0..<numPackages:
    let variant = VariantProfile(
      domains: initTable[string, VariantDomain](),
      hash: "hash-" & $i
    )
    let packageName = "pkg" & $i
    let termId = createTermId(packageName, variant.hash)
    
    result.addTerm(PackageTerm(
      id: termId,
      packageName: packageName,
      variantProfile: variant,
      optional: false,
      source: "test"
    ))
    
    if prevTermId.isSome:
      result.addEdge(DependencyEdge(
        fromTerm: prevTermId.get(),
        toTerm: termId,
        dependencyType: Required
      ))
    
    prevTermId = some(termId)

proc generateDiamondGraph(): DependencyGraph =
  ## Generate a diamond: A -> B, A -> C, B -> D, C -> D
  result = newDependencyGraph()
  
  let variantA = VariantProfile(domains: initTable[string, VariantDomain](), hash: "hash-A")
  let variantB = VariantProfile(domains: initTable[string, VariantDomain](), hash: "hash-B")
  let variantC = VariantProfile(domains: initTable[string, VariantDomain](), hash: "hash-C")
  let variantD = VariantProfile(domains: initTable[string, VariantDomain](), hash: "hash-D")
  
  let termIdA = createTermId("A", variantA.hash)
  let termIdB = createTermId("B", variantB.hash)
  let termIdC = createTermId("C", variantC.hash)
  let termIdD = createTermId("D", variantD.hash)
  
  for (id, name, variant) in [(termIdA, "A", variantA), (termIdB, "B", variantB),
                               (termIdC, "C", variantC), (termIdD, "D", variantD)]:
    result.addTerm(PackageTerm(
      id: id,
      packageName: name,
      variantProfile: variant,
      optional: false,
      source: "test"
    ))
  
  result.addEdge(DependencyEdge(fromTerm: termIdA, toTerm: termIdB, dependencyType: Required))
  result.addEdge(DependencyEdge(fromTerm: termIdA, toTerm: termIdC, dependencyType: Required))
  result.addEdge(DependencyEdge(fromTerm: termIdB, toTerm: termIdD, dependencyType: Required))
  result.addEdge(DependencyEdge(fromTerm: termIdC, toTerm: termIdD, dependencyType: Required))

# --- Property Tests ---

suite "Resolution Completeness Properties":
  
  test "Property 5: Resolution Completeness - Chain graphs":
    ## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
    ## **Validates: Requirements 5.1, 5.4**
    ##
    ## Property: For any chain graph (no cycles), resolution SHALL succeed
    ## and produce a valid installation order
    
    var rng = initRand(12345)
    var successCount = 0
    var totalTests = 0
    
    # Test with various chain lengths
    for chainLength in [1, 2, 5, 10, 20]:
      for iteration in 0..<4:  # 4 iterations per length
        totalTests += 1
        
        let graph = generateChainGraph(chainLength)
        
        # Create resolution request for first package
        let request = ResolutionRequest(
          rootPackages: @[PackageSpec(
            packageName: "pkg0",
            versionConstraint: VersionConstraint(
              operator: OpAny,
              version: SemanticVersion(major: 1, minor: 0, patch: 0)
            ),
            variantProfile: VariantProfile(
              domains: initTable[string, VariantDomain](),
              hash: "hash-0"
            )
          )],
          constraints: @[]
        )
        
        let result = resolve(request, graph)
        
        # Property: Resolution should succeed
        if not result.success:
          echo "FAILED: Chain length ", chainLength, " iteration ", iteration
          echo "  Conflict: ", result.conflict.details
          check false
          continue
        
        # Property: All packages should be in solution
        check result.packages.len == chainLength
        
        # Property: Installation order should respect dependencies
        # In a chain, pkg(i) depends on pkg(i+1), so pkg(i+1) must come first
        var orderMap = initTable[string, int]()
        for i, name in result.installOrder:
          orderMap[name] = i
        
        for i in 0..<(chainLength - 1):
          let dependent = "pkg" & $i
          let dependency = "pkg" & $(i + 1)
          
          if orderMap.hasKey(dependent) and orderMap.hasKey(dependency):
            if orderMap[dependency] >= orderMap[dependent]:
              echo "FAILED: Dependency order violated"
              echo "  ", dependent, " (index ", orderMap[dependent], ") depends on ",
                   dependency, " (index ", orderMap[dependency], ")"
              check false
              continue
        
        successCount += 1
    
    echo "Property 5 (Chain): ", successCount, "/", totalTests, " tests passed"
    check successCount == totalTests
  
  test "Property 5: Resolution Completeness - Diamond graphs":
    ## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
    ## **Validates: Requirements 5.1, 5.4**
    ##
    ## Property: For diamond graphs, resolution SHALL succeed and D SHALL come before B and C
    
    var successCount = 0
    var totalTests = 20
    
    for iteration in 0..<totalTests:
      let graph = generateDiamondGraph()
      
      let request = ResolutionRequest(
        rootPackages: @[PackageSpec(
          packageName: "A",
          versionConstraint: VersionConstraint(
            operator: OpAny,
            version: SemanticVersion(major: 1, minor: 0, patch: 0)
          ),
          variantProfile: VariantProfile(
            domains: initTable[string, VariantDomain](),
            hash: "hash-A"
          )
        )],
        constraints: @[]
      )
      
      let result = resolve(request, graph)
      
      # Property: Resolution should succeed
      if not result.success:
        echo "FAILED: Diamond iteration ", iteration
        echo "  Conflict: ", result.conflict.details
        check false
        continue
      
      # Property: All 4 packages should be in solution
      check result.packages.len == 4
      
      # Property: D must come before B and C (shared dependency)
      var orderMap = initTable[string, int]()
      for i, name in result.installOrder:
        orderMap[name] = i
      
      if orderMap["D"] >= orderMap["B"] or orderMap["D"] >= orderMap["C"]:
        echo "FAILED: D should come before B and C"
        echo "  Order: ", result.installOrder
        check false
        continue
      
      # Property: B and C must come before A
      if orderMap["B"] >= orderMap["A"] or orderMap["C"] >= orderMap["A"]:
        echo "FAILED: B and C should come before A"
        echo "  Order: ", result.installOrder
        check false
        continue
      
      successCount += 1
    
    echo "Property 5 (Diamond): ", successCount, "/", totalTests, " tests passed"
    check successCount == totalTests
  
  test "Property 5: Resolution Completeness - Random acyclic graphs":
    ## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
    ## **Validates: Requirements 5.1, 5.4**
    ##
    ## Property: For any acyclic graph, resolution SHALL succeed
    
    var rng = initRand(54321)
    var successCount = 0
    var totalTests = 20
    
    for iteration in 0..<totalTests:
      # Generate random acyclic graph with 5-15 packages
      let numPackages = rng.rand(5..15)
      let graph = generateAcyclicGraph(rng, numPackages)
      
      if graph.nodeCount() == 0:
        continue
      
      # Pick first package as root
      let rootTerm = toSeq(graph.terms.values)[0]
      
      let request = ResolutionRequest(
        rootPackages: @[PackageSpec(
          packageName: rootTerm.packageName,
          versionConstraint: VersionConstraint(
            operator: OpAny,
            version: SemanticVersion(major: 1, minor: 0, patch: 0)
          ),
          variantProfile: rootTerm.variantProfile
        )],
        constraints: @[]
      )
      
      let result = resolve(request, graph)
      
      # Property: Resolution should succeed for acyclic graphs
      if not result.success:
        echo "FAILED: Random graph iteration ", iteration, " (", numPackages, " packages)"
        echo "  Conflict: ", result.conflict.details
        check false
        continue
      
      # Property: Solution should contain at least the root package
      check result.packages.len >= 1
      
      # Property: Installation order should be valid (no package before its dependencies)
      var orderMap = initTable[string, int]()
      for i, name in result.installOrder:
        orderMap[name] = i
      
      var orderValid = true
      for edge in graph.edges:
        let fromTerm = graph.getTerm(edge.fromTerm)
        let toTerm = graph.getTerm(edge.toTerm)
        
        if fromTerm.isSome and toTerm.isSome:
          let fromName = fromTerm.get().packageName
          let toName = toTerm.get().packageName
          
          if orderMap.hasKey(fromName) and orderMap.hasKey(toName):
            if orderMap[toName] >= orderMap[fromName]:
              echo "FAILED: Dependency order violated in random graph"
              echo "  ", fromName, " depends on ", toName
              echo "  But ", toName, " comes after ", fromName, " in install order"
              orderValid = false
              break
      
      if not orderValid:
        check false
        continue
      
      successCount += 1
    
    echo "Property 5 (Random): ", successCount, "/", totalTests, " tests passed"
    check successCount == totalTests
  
  test "Property 5: Determinism - Same input produces same output":
    ## **Feature: 02-nip-dependency-resolution, Property 5: Resolution Completeness**
    ## **Validates: Requirements 5.1, 5.4**
    ##
    ## Property: Resolving the same graph multiple times SHALL produce identical results
    
    let graph = generateDiamondGraph()
    
    let request = ResolutionRequest(
      rootPackages: @[PackageSpec(
        packageName: "A",
        versionConstraint: VersionConstraint(
          operator: OpAny,
          version: SemanticVersion(major: 1, minor: 0, patch: 0)
        ),
        variantProfile: VariantProfile(
          domains: initTable[string, VariantDomain](),
          hash: "hash-A"
        )
      )],
      constraints: @[]
    )
    
    # Resolve multiple times
    var results: seq[ResolutionResult] = @[]
    for _ in 0..<10:
      results.add(resolve(request, graph))
    
    # Property: All results should be identical
    let firstResult = results[0]
    
    for i in 1..<results.len:
      let result = results[i]
      
      # Check success status matches
      check result.success == firstResult.success
      
      if result.success:
        # Check same number of packages
        check result.packages.len == firstResult.packages.len
        
        # Check same installation order
        check result.installOrder == firstResult.installOrder
        
        # Check same package names
        let firstNames = firstResult.packages.mapIt(it.packageName).toHashSet
        let resultNames = result.packages.mapIt(it.packageName).toHashSet
        check firstNames == resultNames
    
    echo "Property 5 (Determinism): All 10 resolutions produced identical results"