481 lines
15 KiB
Nim
481 lines
15 KiB
Nim
## 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")
|