1		% (c) 2014-2026 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(smtlib2_environment,[empty_env/1,
6		add_identifier/4,
7
8		add_assertion/3,
9		get_assertions/2,
10		push_assertion_stack/3,
11		pop_assertion_stack/3,
12
13		get_type/3,
14		add_function/6,
15		get_function/5,
16		create_local_env/3,
17		get_custom_types/2,
18		is_custom_type/2,
19		add_custom_type/3,
20		portray_smtlib2_env/1]).
21
22		:- use_module(probsrc(module_information),[module_info/2]).
23		:- module_info(group,smtlib).
24		:- module_info(description,'The SMT-LIB 2 Interpreter - Environment').
25
26		:- use_module(library(lists)).
27		:- use_module(library(avl)).
28
29		% environment: env(Identifiers,Functions,Assertions,CustomTypes)
30		% identifiers: avl tree of b(identifier(ID),Type,[]) stored at ID
31		% functions: avl tree of function(Parameters,RetType,Definition) at ID
32		% Assertions: Stack (List) of Lists of predicates
33		% CustomTypes: List of custom types, i.e. deferred sets
34
35		empty_env(env(IDs,Funs,[[]],[])) :-
36		empty_avl(IDs),
37		empty_avl(Funs).
38
39		get_custom_types(env(_,_,_,Ct),Ct).
40		is_custom_type(env(_,_,_,Cts),Ct) :-
41		member(Ct,Cts).
42		add_custom_type(env(IDs,Funs,As,Ct),ID,env(IDs,Funs,As,[ID|Ct])).
43
44		create_local_env(env(IDs,Funs,As,Ct),LocalIDs,env(NIDs,Funs,As,Ct)) :-
45		avl_store_all_ids(LocalIDs,IDs,NIDs).
46
47		avl_store_all_ids([],A,A).
48		avl_store_all_ids([b(identifier(ID),Type,[])|T],AIn,AOut) :-
49		avl_store(ID,AIn,b(identifier(ID),Type,[]),ATemp),
50		avl_store_all_ids(T,ATemp,AOut).
51
52		add_function(env(IDs,Funs,As,Ct),ID,P,R,D,env(IDs,NFuns,As,Ct)) :-
53		avl_store(ID,Funs,function(P,R,D),NFuns).
54		get_function(ID,env(_,Funs,_,_),Params,Results,Definition) :- atomic(ID),!,
55		avl_fetch(ID,Funs,function(Params,Results,Definition)).
56		get_function(ID,env(_,Funs,_,_),Params,Results,Definition) :-
57		print(var_get_function(ID)),nl,
58		avl_member(ID,Funs,function(Params,Results,Definition)).
59
60		pop_assertion_stack(Env,0,Env) :- !.
61		pop_assertion_stack(env(IDs,Funs,[_|Ass],Types),Count,EnvOut) :- Count > 0, !,
62		NCount is Count - 1,
63		pop_assertion_stack(env(IDs,Funs,Ass,Types),NCount,EnvOut).
64
65		push_assertion_stack(Env,0,Env) :- !.
66		push_assertion_stack(env(IDs,Funs,Ass,Types),Count,EnvOut) :- Count > 0, !,
67		NCount is Count - 1,
68		pop_assertion_stack(env(IDs,Funs,[[]|Ass],Types),NCount,EnvOut).
69
70		get_assertions(env(_,_,As,_),AllAssertions) :- append(As,AllAssertions).
71		add_assertion(env(IDs,Funs,[CurrentAssertionSet|AssertionSets],Ct),Term,env(IDs,Funs,[NAs|AssertionSets],Ct)) :-
72		NAs = [Term|CurrentAssertionSet].
73
74		add_identifier(env(IDs,Funs,As,Ct),ID,Type,env(NIDs,Funs,As,Ct)) :-
75		avl_store(ID,IDs,b(identifier(ID),Type,[]),NIDs).
76
77		get_type(Id,env(IDs,_,_,_),Type) :- atomic(Id),!,
78		avl_fetch(Id,IDs,b(identifier(Id),Type,[])).
79		get_type(Id,env(IDs,_,_,_),Type) :-
80		print(var_get_type(Id)),nl,
81		avl_member(Id,IDs,b(identifier(Id),Type,[])).
82
83
84		portray_smtlib2_env(env(IDs,Funs,As,Ct)) :- !,
85		write('Identifiers:'),nl,
86		portray_avl(IDs),nl,
87		write('Functions:'),nl,
88		portray_avl(Funs),nl,
89		write('Assertions:'),nl,
90		write(As),nl,
91		write('Types:'),
92		write(Ct),nl.
93		portray_smtlib2_env(E) :- write('*** UNEXPECTED ENVIRONMENT ***'),nl,
94		write(E),nl.
95