Open nrueh opened 2 months ago
Maybe there is a better way to implement the UNSAT.
This way Assert(All(), False_)
does not give a clintest error when the test fails but a python error:
Traceback (most recent call last):
File "/Users/nicolasruhling/projects/coom-solver/tests/test_sanity_checks.py", line 97, in test_empty_combinations
run_test(TEST_UNSAT, program=program_unsat)
File "/Users/nicolasruhling/projects/coom-solver/tests/__init__.py", line 47, in run_test
solver.solve(test_copy)
File "/Users/nicolasruhling/projects/coom-solver/tests/__init__.py", line 135, in solve
self.__application.main(control=ctl, files=self.__files) # type: ignore
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/nicolasruhling/projects/coom-solver/src/coomsolver/application.py", line 153, in main
control.solve()
File "/Users/nicolasruhling/projects/coom-solver/tests/__init__.py", line 101, in solve
self._ctl.solve(
File "/Users/nicolasruhling/projects/coom-solver/.nox/test-3-11/lib/python3.11/site-packages/clingo/control.py", line 848, in solve
_c_call(
File "/Users/nicolasruhling/projects/coom-solver/.nox/test-3-11/lib/python3.11/site-packages/clingo/_internal.py", line 44, in _c_call
_handle_error(c_fun(*args, p_ret), handler)
File "/Users/nicolasruhling/projects/coom-solver/.nox/test-3-11/lib/python3.11/site-packages/clingo/_internal.py", line 71, in _handle_error
raise handler.error[0](handler.error[1]).with_traceback(handler.error[2])
File "/Users/nicolasruhling/projects/coom-solver/.nox/test-3-11/lib/python3.11/site-packages/clingo/control.py", line 121, in _pyclingo_solve_event_callback
goon[0] = handler.on_model(_ffi.cast("clingo_model_t*", event))
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/nicolasruhling/projects/coom-solver/.nox/test-3-11/lib/python3.11/site-packages/clingo/control.py", line 93, in on_model
ret = self._on_model(Model(m))
^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/nicolasruhling/projects/coom-solver/tests/__init__.py", line 63, in f
on_test(*args)
File "/Users/nicolasruhling/projects/coom-solver/.nox/test-3-11/lib/python3.11/site-packages/clintest/test.py", line 363, in on_model
self.__quantifier.consume(self.__assertion.holds_for(model))
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
TypeError: False_.holds_for() missing 1 required positional argument: 'model'
Add built-in tests for special cases like UNSAT and empty model.
For example like this:
UNSAT:
Assert(All(), False_)
Empty Model:Assert(All(), SubsetOf(set()))