Loge: DIMACS smoke test

root = Path.expand("..", __DIR__)

Mix.install([
  {:loge, path: Path.join(root, "loge"), override: true},
  {:loge_dimacs, path: Path.join(root, "loge_dimacs")},
  {:kino_loge, path: Path.join(root, "kino_loge")}
])

Solving

Expected: Satisfiable, one model, 1 -2 3.

Loge.run!(Loge.Dimacs.Engines.Clasp, "c x1, not x2, x2 or x3\np cnf 3 3\n1 0\n-2 0\n2 3 0\n",
  models: 1
)

Models 0 enumerates all of them. Expected: Satisfiable, three models.

Loge.run!(Loge.Dimacs.Engines.Clasp, "p cnf 2 1\n1 2 0\n", models: 0)

Expected: Unsatisfiable, no models.

Loge.run!(Loge.Dimacs.Engines.Clasp, "p cnf 1 2\n1 0\n-1 0\n", models: 1)

Linting

Expected: under the editor, variable 4 exceeds the header and the clause count differs from it; evaluating raises Loge.Error with both findings.

Loge.run!(Loge.Dimacs.Engines.Clasp, "p cnf 3 3\n1 -4 0\n2 0\n", models: 1)