Nothing
# Test the creation of a CnfAtom
test_that("CnfAtom is created correctly from CnfSymbol", {
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
atom = CnfAtom(X, c("a", "b"))
expect_s3_class(atom, "CnfAtom")
expect_equal(atom$symbol, "X")
expect_equal(atom$values, c("a", "b"))
})
# Test the creation of a tautology and contradiction with CnfAtom
test_that("CnfAtom handles tautologies and contradictions correctly", {
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
tautology = CnfAtom(X, c("a", "b", "c"))
contradiction = CnfAtom(X, character(0))
# Tautology should evaluate to TRUE
expect_true(as.logical(tautology))
# Contradiction should evaluate to FALSE
expect_false(as.logical(contradiction))
})
# Test negation of CnfAtom
test_that("Negation of CnfAtom works correctly", {
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
atom = CnfAtom(X, c("a", "b"))
negated_atom = !atom
# Check that negation works correctly
expect_s3_class(negated_atom, "CnfAtom")
expect_equal(negated_atom$symbol, "X")
expect_equal(negated_atom$values, "c") # Negation should result in the complement of the original values
# Check that negation of a tautology is a contradiction
expect_false(as.logical(!CnfAtom(X, c("a", "b", "c"))))
# Check that negation of a contradiction is a tautology
expect_true(as.logical(!CnfAtom(X, character(0))))
})
# Test conjunction (&) of CnfAtoms
test_that("Conjunction of CnfAtoms works correctly", {
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
Y = CnfSymbol(u, "Y", c("d", "e", "f"))
atom1 = CnfAtom(X, c("a", "b"))
atom2 = CnfAtom(Y, c("d", "e"))
formula = atom1 & atom2
expect_s3_class(formula, "CnfFormula")
expect_length(as.list(formula), 2)
atoms = unlist(lapply(as.list(formula), as.list), recursive = FALSE)
# we don't know if atoms[[1]] is atom1 or atom2
if (identical(atoms[[1]]$symbol, "X")) {
expect_identical(atoms[[1]], atom1)
expect_identical(atoms[[2]], atom2)
} else {
expect_identical(atoms[[1]], atom2)
expect_identical(atoms[[2]], atom1)
}
# Check that conjunction of a tautology with another atom is the other atom
ttl = CnfAtom(X, c("a", "b", "c")) & atom2
expect_s3_class(ttl, "CnfFormula")
expect_identical(lapply(as.list(ttl), as.list), list(list(atom2)))
# Check that conjunction of a contradiction with another atom is a contradiction
ctn = CnfAtom(X, character(0)) & atom2
expect_s3_class(ctn, "CnfFormula")
expect_false(as.logical(ctn))
})
# Test disjunction (|) of CnfAtoms
test_that("Disjunction of CnfAtoms works correctly", {
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
Y = CnfSymbol(u, "Y", c("d", "e", "f"))
atom1 = CnfAtom(X, c("a", "b"))
atom2 = CnfAtom(Y, c("d", "e"))
clause = atom1 | atom2
expect_s3_class(clause, "CnfClause")
expect_length(as.list(clause), 2)
atoms = as.list(clause)
if (identical(atoms[[1]]$symbol, "X")) {
expect_identical(atoms[[1]], atom1)
expect_identical(atoms[[2]], atom2)
} else {
expect_identical(atoms[[1]], atom2)
expect_identical(atoms[[2]], atom1)
}
# Check that disjunction of a tautology with another atom is a tautology
ttl = CnfAtom(X, c("a", "b", "c")) | atom2
expect_true(as.logical(ttl))
expect_s3_class(ttl, "CnfClause")
# Check that disjunction of a contradiction with another atom is the other atom
ctn = CnfAtom(X, character(0)) | atom2
expect_identical(as.list(ctn), list(atom2))
})
# Test print and format methods for CnfAtom
test_that("print and format methods for CnfAtom work correctly", {
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
atom = CnfAtom(X, c("a", "b"))
# Test print method
expect_output(print(atom), "CnfAtom: X ∈ \\{a, b\\}.")
# Test format method
expect_equal(format(atom), "CnfAtom(X)")
})
# Test conversion between logical and CnfAtom
test_that("as.logical and as.CnfAtom conversions work correctly", {
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
atom_true = CnfAtom(X, c("a", "b", "c"))
atom_false = CnfAtom(X, character(0))
atom_neither = CnfAtom(X, c("a", "b"))
# Convert CnfAtom to logical
expect_true(as.logical(atom_true))
expect_false(as.logical(atom_false))
expect_identical(as.logical(atom_neither), NA)
# Convert logical to CnfAtom
expect_s3_class(as.CnfAtom(TRUE), "CnfAtom")
expect_true(as.logical(as.CnfAtom(TRUE)))
expect_s3_class(as.CnfAtom(FALSE), "CnfAtom")
expect_false(as.logical(as.CnfAtom(FALSE)))
expect_error(as.CnfAtom(NA), "May not be NA")
expect_error(as.CnfAtom(c(TRUE, TRUE)), "Must have length 1.")
})
# Test invalid creation of CnfAtom with values not in the domain
test_that("CnfAtom throws error when values are not in the symbol's domain", {
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
expect_error(CnfAtom(X, c("d", "e")), "Must be a subset of \\{'a','b','c'\\}")
})
test_that("all.equal recognizes (in)equality", {
# Test equality between identical CnfAtoms
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
atom1 = CnfAtom(X, c("a", "b"))
atom2 = CnfAtom(X, c("a", "b"))
expect_true(all.equal(atom1, atom2))
# Test equality for different CnfAtoms with the same symbol but different values
atom1 = CnfAtom(X, c("a", "b"))
atom2 = CnfAtom(X, c("b", "c"))
expect_string(all.equal(atom1, atom2), pattern = "string mismatch")
# Test equality for different CnfAtoms with the same values but different order
atom1 = CnfAtom(X, c("a", "b"))
atom2 = CnfAtom(X, c("b", "a"))
expect_true(all.equal(atom1, atom2))
# Test equality for CnfAtoms with different symbols
Y = CnfSymbol(u, "Y", c("d", "e", "f"))
atom1 = CnfAtom(X, c("a", "b"))
atom2 = CnfAtom(Y, c("d"))
expect_string(paste(all.equal(atom1, atom2), collapse = "\n"), pattern = "string mismatch")
# Test equality between a logical CnfAtom and a CnfAtom object
u = CnfUniverse()
X = CnfSymbol(u, "X", c("a", "b", "c"))
atom1 = CnfAtom(X, c("a", "b"))
atom2 = CnfAtom(X, c("a", "b", "c"))
expect_string(all.equal(atom1, atom2), pattern = "not both logicals")
expect_string(all.equal(atom2, atom1), pattern = "not both logicals")
# Test equality for a logical TRUE CnfAtom and another logical TRUE CnfAtom
atom3 = CnfAtom(Y, c("d", "e", "f"))
expect_true(all.equal(atom2, atom3))
expect_true(all.equal(atom2, as.CnfAtom(TRUE)))
# Test equality for a logical FALSE CnfAtom and another logical FALSE CnfAtom
logical_atom1 = CnfAtom(X, character(0))
logical_atom2 = CnfAtom(Y, character(0))
expect_true(all.equal(logical_atom1, logical_atom2))
expect_string(all.equal(atom1, logical_atom1), pattern = "not both logicals")
expect_string(all.equal(atom2, logical_atom1), pattern = "both logicals but not equal")
expect_true(all.equal(logical_atom1, as.CnfAtom(FALSE)))
# Test for a case where a CnfAtom is compared with a non-CnfAtom object
expect_string(all.equal(atom1, "not a CnfAtom"), pattern = "current is not a CnfAtom")
# Test that all.equal accepts differences in the universe of the CnfAtoms
u1 = CnfUniverse()
u2 = CnfUniverse()
X1 = CnfSymbol(u1, "X", c("a", "b", "c"))
X2 = CnfSymbol(u2, "X", c("a", "b", "c"))
atom1 = CnfAtom(X1, c("a", "b"))
atom2 = CnfAtom(X2, c("a", "b"))
expect_true(all.equal(atom1, atom2))
# .. unless the universes differ
u3 = CnfUniverse()
X3 = CnfSymbol(u3, "X", c("a", "b", "c", "d"))
atom3 = CnfAtom(X3, c("a", "b"))
expect_string(all.equal(atom1, atom3), pattern = "Lengths \\(3, 4\\) differ")
})
Any scripts or data that you put into this service are public.
Add the following code to your website.
For more information on customizing the embed code, read Embedding Snippets.