## Unit Tests for CNF Translation
##
## Tests for translating dependency constraints into Conjunctive Normal Form (CNF)
## for use with CDCL-based SAT solving.
##
## Requirements tested:
## - 6.1: Create boolean variables for each term
## - 6.2: Create implication clauses for dependencies (A → B)
## - 6.3: Create mutual exclusion clauses (¬(A ∧ B))
## - 6.4: Create satisfaction clauses for variants
## - 6.5: Validate CNF is ready for CDCL solving

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

suite "CNF Translation Tests":
  
  test "Create boolean variable":
    ## Test creating a boolean variable from package+version+variant
    ## Requirements: 6.1
    
    var variant = newVariantProfile()
    variant.addFlag("optimization", "lto")
    variant.calculateHash()
    
    let boolVar = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: variant
    )
    
    check boolVar.package == "nginx"
    check boolVar.version.major == 1
    check boolVar.variant.hash == variant.hash
    
    # Test string representation
    let varStr = $boolVar
    check varStr.contains("nginx")
    check varStr.contains("1.24.0")
  
  test "Create literal":
    ## Test creating positive and negative literals
    ## Requirements: 6.1
    
    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)
    
    check not positiveLit.isNegated
    check negativeLit.isNegated
    
    # Test negation
    let doubleNegated = negate(negativeLit)
    check not doubleNegated.isNegated
  
  test "Create clause":
    ## Test creating a clause from literals
    ## Requirements: 6.1
    
    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 clause = makeClause(
      @[
        makeLiteral(var1, isNegated = true),
        makeLiteral(var2, isNegated = false)
      ],
      reason = "nginx depends on zlib"
    )
    
    check clause.literals.len == 2
    check clause.literals[0].isNegated
    check not clause.literals[1].isNegated
    check clause.reason == "nginx depends on zlib"
  
  test "Create CNF formula":
    ## Test creating an empty CNF formula
    ## Requirements: 6.1
    
    var formula = newCNFFormula()
    
    check formula.clauses.len == 0
    check formula.variables.len() == 0
    check formula.nextVarId == 1
  
  test "Register variables in formula":
    ## Test variable registration and ID assignment
    ## Requirements: 6.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 id1 = formula.getOrCreateVarId(var1)
    let id2 = formula.getOrCreateVarId(var2)
    let id1Again = formula.getOrCreateVarId(var1)
    
    check id1 == 1
    check id2 == 2
    check id1Again == 1  # Same variable, same ID
    check formula.variables.len() == 2
  
  test "Translate dependency to implication clause":
    ## Test translating "A depends on B" to "¬A ∨ B"
    ## Requirements: 6.2 - Create implication clauses (A → B)
    
    var formula = newCNFFormula()
    
    let clause = formula.translateDependency(
      dependent = "nginx",
      dependentVersion = SemanticVersion(major: 1, minor: 24, patch: 0),
      dependentVariant = newVariantProfile(),
      dependency = "zlib",
      dependencyVersion = SemanticVersion(major: 1, minor: 2, patch: 13),
      dependencyVariant = newVariantProfile()
    )
    
    # Check clause structure: ¬A ∨ B
    check clause.literals.len == 2
    check clause.literals[0].isNegated  # ¬nginx
    check not clause.literals[1].isNegated  # zlib
    check clause.literals[0].variable.package == "nginx"
    check clause.literals[1].variable.package == "zlib"
    
    # Check formula was updated
    check formula.clauses.len == 1
    check formula.variables.len() == 2
  
  test "Translate multiple dependencies":
    ## Test translating multiple dependencies
    ## Requirements: 6.2
    
    var formula = newCNFFormula()
    
    # nginx depends on zlib
    discard formula.translateDependency(
      dependent = "nginx",
      dependentVersion = SemanticVersion(major: 1, minor: 24, patch: 0),
      dependentVariant = newVariantProfile(),
      dependency = "zlib",
      dependencyVersion = SemanticVersion(major: 1, minor: 2, patch: 13),
      dependencyVariant = newVariantProfile()
    )
    
    # nginx depends on pcre
    discard formula.translateDependency(
      dependent = "nginx",
      dependentVersion = SemanticVersion(major: 1, minor: 24, patch: 0),
      dependentVariant = newVariantProfile(),
      dependency = "pcre",
      dependencyVersion = SemanticVersion(major: 8, minor: 45, patch: 0),
      dependencyVariant = newVariantProfile()
    )
    
    check formula.clauses.len == 2
    check formula.variables.len() == 3  # nginx, zlib, pcre
  
  test "Translate mutual exclusion":
    ## Test translating "A and B are mutually exclusive" to "¬A ∨ ¬B"
    ## Requirements: 6.3 - Create mutual exclusion clauses (¬(A ∧ B))
    
    var formula = newCNFFormula()
    
    var variantWayland = newVariantProfile()
    variantWayland.addFlag("display", "wayland")
    variantWayland.calculateHash()
    
    var variantX11 = newVariantProfile()
    variantX11.addFlag("display", "x11")
    variantX11.calculateHash()
    
    let clause = formula.translateExclusivity(
      packageA = "firefox",
      versionA = SemanticVersion(major: 120, minor: 0, patch: 0),
      variantA = variantWayland,
      packageB = "firefox",
      versionB = SemanticVersion(major: 120, minor: 0, patch: 0),
      variantB = variantX11,
      reason = "wayland and x11 are mutually exclusive"
    )
    
    # Check clause structure: ¬A ∨ ¬B
    check clause.literals.len == 2
    check clause.literals[0].isNegated  # ¬firefox+wayland
    check clause.literals[1].isNegated  # ¬firefox+x11
    check clause.literals[0].variable.package == "firefox"
    check clause.literals[1].variable.package == "firefox"
    
    # Check formula was updated
    check formula.clauses.len == 1
    check formula.variables.len() == 2
  
  test "Translate variant satisfaction":
    ## Test translating variant satisfaction constraints
    ## Requirements: 6.4 - Create satisfaction clauses
    
    var formula = newCNFFormula()
    
    var requiredVariant = newVariantProfile()
    requiredVariant.addFlag("optimization", "lto")
    requiredVariant.calculateHash()
    
    var availableVariant = newVariantProfile()
    availableVariant.addFlag("optimization", "lto")
    availableVariant.addFlag("security", "hardened")
    availableVariant.calculateHash()
    
    let clause = formula.translateVariantSatisfaction(
      package = "nginx",
      version = SemanticVersion(major: 1, minor: 24, patch: 0),
      requiredVariant = requiredVariant,
      availableVariant = availableVariant
    )
    
    # Available variant satisfies required, so: ¬required ∨ available
    check clause.literals.len == 2
    check clause.literals[0].isNegated  # ¬required
    check not clause.literals[1].isNegated  # available
    
    # Check formula was updated
    check formula.clauses.len == 1
    check formula.variables.len() == 2
  
  test "Translate variant non-satisfaction":
    ## Test translating variant that doesn't satisfy requirements
    ## Requirements: 6.4
    
    var formula = newCNFFormula()
    
    var requiredVariant = newVariantProfile()
    requiredVariant.addFlag("optimization", "lto")
    requiredVariant.addFlag("security", "hardened")
    requiredVariant.calculateHash()
    
    var availableVariant = newVariantProfile()
    availableVariant.addFlag("optimization", "lto")
    # Missing "security: hardened"
    availableVariant.calculateHash()
    
    let clause = formula.translateVariantSatisfaction(
      package = "nginx",
      version = SemanticVersion(major: 1, minor: 24, patch: 0),
      requiredVariant = requiredVariant,
      availableVariant = availableVariant
    )
    
    # Available doesn't satisfy required, so: ¬required ∨ ¬available
    check clause.literals.len == 2
    check clause.literals[0].isNegated  # ¬required
    check clause.literals[1].isNegated  # ¬available (incompatible)
    
    # Check formula was updated
    check formula.clauses.len == 1
    check formula.variables.len() == 2
  
  test "Translate root requirement":
    ## Test translating user requirements to unit clauses
    ## Requirements: 6.1
    
    var formula = newCNFFormula()
    
    var variant = newVariantProfile()
    variant.addFlag("optimization", "lto")
    variant.calculateHash()
    
    let clause = formula.translateRootRequirement(
      package = "nginx",
      version = SemanticVersion(major: 1, minor: 24, patch: 0),
      variant = variant
    )
    
    # Root requirement is a unit clause: P
    check clause.literals.len == 1
    check not clause.literals[0].isNegated
    check clause.literals[0].variable.package == "nginx"
    
    # Check formula was updated
    check formula.clauses.len == 1
    check formula.variables.len() == 1
  
  test "Translate incompatibility":
    ## Test translating an incompatibility to CNF
    ## Requirements: 6.1, 6.2, 6.3
    
    var formula = newCNFFormula()
    
    let incomp = createDependencyIncompatibility(
      dependent = "nginx",
      dependentVersion = SemanticVersion(major: 1, minor: 24, patch: 0),
      dependency = "zlib",
      dependencyConstraint = Constraint(
        versionRange: VersionConstraint(
          operator: OpGreaterEq,
          version: SemanticVersion(major: 1, minor: 2, patch: 0)
        ),
        variantReq: newVariantProfile(),
        isNegative: false
      )
    )
    
    let clause = formula.translateIncompatibility(incomp)
    
    # Incompatibility should be translated to a clause
    check clause.literals.len == 2
    check formula.clauses.len == 1
  
  test "Validate CNF formula":
    ## Test CNF formula validation
    ## Requirements: 6.5 - CNF is ready for CDCL solving
    
    var formula = newCNFFormula()
    
    # Empty formula is invalid
    check not formula.isValidCNF()
    
    # Add a valid clause
    discard formula.translateRootRequirement(
      package = "nginx",
      version = SemanticVersion(major: 1, minor: 24, patch: 0),
      variant = newVariantProfile()
    )
    
    # Now formula is valid
    check formula.isValidCNF()
  
  test "Complex CNF formula":
    ## Test building a complex CNF formula with multiple clause types
    ## Requirements: 6.1, 6.2, 6.3, 6.4, 6.5
    
    var formula = newCNFFormula()
    
    # Root requirement: user wants nginx
    discard formula.translateRootRequirement(
      package = "nginx",
      version = SemanticVersion(major: 1, minor: 24, patch: 0),
      variant = newVariantProfile()
    )
    
    # Dependency: nginx depends on zlib
    discard formula.translateDependency(
      dependent = "nginx",
      dependentVersion = SemanticVersion(major: 1, minor: 24, patch: 0),
      dependentVariant = newVariantProfile(),
      dependency = "zlib",
      dependencyVersion = SemanticVersion(major: 1, minor: 2, patch: 13),
      dependencyVariant = newVariantProfile()
    )
    
    # Dependency: nginx depends on pcre
    discard formula.translateDependency(
      dependent = "nginx",
      dependentVersion = SemanticVersion(major: 1, minor: 24, patch: 0),
      dependentVariant = newVariantProfile(),
      dependency = "pcre",
      dependencyVersion = SemanticVersion(major: 8, minor: 45, patch: 0),
      dependencyVariant = newVariantProfile()
    )
    
    # Exclusivity: wayland and x11 are mutually exclusive
    var variantWayland = newVariantProfile()
    variantWayland.addFlag("display", "wayland")
    variantWayland.calculateHash()
    
    var variantX11 = newVariantProfile()
    variantX11.addFlag("display", "x11")
    variantX11.calculateHash()
    
    discard formula.translateExclusivity(
      packageA = "firefox",
      versionA = SemanticVersion(major: 120, minor: 0, patch: 0),
      variantA = variantWayland,
      packageB = "firefox",
      versionB = SemanticVersion(major: 120, minor: 0, patch: 0),
      variantB = variantX11
    )
    
    # Check formula structure
    check formula.clauses.len == 4
    check formula.variables.len() >= 4
    check formula.isValidCNF()
    
    # Test string representation
    let formulaStr = $formula
    check formulaStr.contains("CNF Formula")
    check formulaStr.contains("4 clauses")
  
  test "Variable equality and hashing":
    ## Test that boolean variables can be used in hash tables
    ## Requirements: 6.1
    
    var variant1 = newVariantProfile()
    variant1.addFlag("optimization", "lto")
    variant1.calculateHash()
    
    var variant2 = newVariantProfile()
    variant2.addFlag("optimization", "lto")
    variant2.calculateHash()
    
    let var1 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: variant1
    )
    
    let var2 = BoolVar(
      package: "nginx",
      version: SemanticVersion(major: 1, minor: 24, patch: 0),
      variant: variant2
    )
    
    let var3 = BoolVar(
      package: "zlib",
      version: SemanticVersion(major: 1, minor: 2, patch: 13),
      variant: newVariantProfile()
    )
    
    # Same package+version+variant should be equal
    check var1 == var2
    check hash(var1) == hash(var2)
    
    # Different package should not be equal
    check var1 != var3
  
  test "Clause string representation":
    ## Test that clauses have readable string representations
    ## Requirements: 6.5
    
    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 clause = makeClause(
      @[
        makeLiteral(var1, isNegated = true),
        makeLiteral(var2, isNegated = false)
      ],
      reason = "nginx depends on zlib"
    )
    
    let clauseStr = $clause
    check clauseStr.contains("nginx")
    check clauseStr.contains("zlib")
    check clauseStr.contains("¬")  # Negation symbol
    check clauseStr.contains("∨")  # OR symbol
    check clauseStr.contains("nginx depends on zlib")