700 lines
20 KiB
Nim
700 lines
20 KiB
Nim
## 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
|