assumptions

Module for checking the optional assumption program.

check_assumptions(assumptions: list[AST], inputs: set[Predicate], outputs: set[Predicate], left: list[AST], right: list[AST], aux: Auxiliaries) -> list[AST]

Check the assumption program and rename conflicting private predicates.

The assumption program may only contain input predicates and (fresh) private predicates. Predicates that are not input or output are renamed if they conflict with any private predicates of left or right. In addition, the assumptions may use the auxiliary domain predicate.

Raises an AnthemCXError (causing anthem-cx to exit) if an output predicate occurs in the assumption program. Returns the (possibly renamed) assumption program.