Building Tests¶

Every test in clintest is assembled from a few building blocks. Here, you will learn what they are and how to combine them, building on the example from Getting Started.

Tests and outcomes¶

A test is an instance of Test. The simplest one is Assert, which checks a property of the models of a program.

from clintest.test import Assert
from clintest.quantifier import All
from clintest.assertion import Contains

test = Assert(All(), Contains("a"))

This test checks that all models contain the atom a.

Every test keeps track of its own outcome, which is one of the following:

• F?: possibly false
• T?: possibly true
• F!: certainly false
• T!: certainly true

An uncertain outcome means that the test is not complete yet. Once the outcome is certain, it never changes again. You can query the outcome at any time:

>>> print(test.outcome())
T?

The test has not been run yet, so its outcome is still uncertain. Since no model so far lacks the atom a, it is possibly true.

Assert combines an assertion (here: Contains("a")) with a quantifier (here: All()) into a test. The next two sections introduce both in turn.

Assertions¶

An Assertion is a statement about a single model. clintest provides the following assertions:

Contains checks all atoms of a model, while Equals, SubsetOf, and SupersetOf only look at the shown symbols. This matters as soon as your program uses #show.

Symbols can be given as strings, such as "p(1)", or as clingo.Symbol objects.

Assertions can be combined with Not, And, Or, Implies, and Equivalent. For example, the following assertion holds for every model that either lacks b or contains a:

from clintest.assertion import Contains, Implies

assertion = Implies(Contains("b"), Contains("a"))

Quantifiers¶

A Quantifier decides for how many models the assertion must hold. clintest provides the following quantifiers:

The quantifier also determines when the outcome becomes certain. For example, All is certainly false as soon as one model violates the assertion, and Any is certainly true as soon as one model satisfies it. Otherwise, the outcome only becomes certain once the solver has finished.

Quantifiers can be combined with Not, And, and Or. For example, the following quantifier demands that the assertion holds for two to five models, so it is certainly false as soon as the assertion holds for a sixth one:

from clintest.quantifier import And, GreaterEqual, LessEqual

quantifier = And(GreaterEqual(2), LessEqual(5))

Combinations also let you decide what happens if a program has no models. Without models, All is true and Any is false. If you need it the other way around, And(All(), Any()) behaves like All but is false without models, and Or(Any(), All()) behaves like Any but is true without models.

Quantifiers are stateful, so each test needs its own instance. The same goes for the operands of And and Or: in And(q, Not(q)), the quantifier q would count every model twice.

Solvers¶

A Solver runs a test. Most of the time, you will use Clingo:

from clintest.solver import Clingo

solver = Clingo(["0"], "a. {b}.")

Its constructor takes three optional arguments:

1. arguments: a list of command-line options for clingo. Here, "0" asks clingo for all models. Without it, clingo stops after the first model.
2. program: the program as a string.
3. files: a list of paths to files with additional program parts.

Calling solve runs the test and updates its outcome:

>>> solver.solve(test)
>>> print(test.outcome())
T!

A test is updated in place and cannot be reset. To run the same check again, create a new test.

If you want to test against a fixed list of models instead of running clingo, use Iterate.

Combining tests¶

Real-world programs need more than one check. Instead of running each check separately, you can combine tests with And, Or, and Not:

from clintest.test import Assert, And, Not
from clintest.quantifier import All, Any
from clintest.assertion import Contains

test = And(
    Assert(All(), Contains("a")),
    Not(Assert(Any(), Contains("c"))),
)

This test checks that all models contain a and that no model contains c. All operands see the same models, so clingo only has to solve the program once.

Compound tests also decide when to stop. And is certainly false as soon as one operand is certainly false, and Or is certainly true as soon as one operand is certainly true. From then on, the remaining operands no longer matter, so clintest stops the solver. This is why, in Getting Started, the last assertion was never completed.

You can turn this behavior off with short_circuit=False. The remaining operands then keep running until their own outcomes are certain.