1		% (c) 2009-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(kernel_propagation,
6		[ do_not_enumerate_binary_boolean_operator/3
7		]).
8
9
10
11		:- use_module(module_information,[module_info/2]).
12		:- module_info(group,kernel).
13		:- module_info(description,'This module has rules about when and how to propagate in the ProB kernel.').
14
15
16
17		% avoid enumerating possible values for arguments:
18		do_not_enumerate_binary_boolean_operator(subset,LHS,_) :- cannot_propagate_value_to_expr(LHS).
19
20		cannot_propagate_value_to_expr(b(E,T,_)) :- cannot_propagate(E,T).
21		% we cannot effectively propagate values to such expressions
22		cannot_propagate(domain(_),_). % when knowing dom(f) we cannot derive f
23		cannot_propagate(range(_),_).
24		%cannot_propagate(_,_).
25		% TO DO: unary_in_boolean_type(pow_subset,kernel_objects:check_subset_of_wf).
26		% unary_in_boolean_type(fin_subset,kernel_objects:check_finite_subset_of_wf).
27		% unary_in_boolean_type(pow1_subset,kernel_objects:check_non_empty_subset_of_wf).
28
29