mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 23:33:41 +00:00
Code Activity

Datalog: save memory in the compiler by using a union

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-02-02 10:34:19 +00:00
parent 6017dcace3
commit c0e0b39a1d
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz/rel/dl_compiler.h
View file

@ -82,9 +82,11 @@ namespace datalog {
relation_sort domain; // domain of the column relation_sort domain; // domain of the column
assembling_column_kind kind; // "instruction" tag assembling_column_kind kind; // "instruction" tag
unsigned source_column; // for ACK_BOUND_VAR union {
unsigned var_index; // for ACK_UNBOUND_VAR unsigned source_column; // for ACK_BOUND_VAR
relation_element constant; // for ACK_CONSTANT unsigned var_index; // for ACK_UNBOUND_VAR
relation_element constant; // for ACK_CONSTANT
};
}; };
class instruction_observer : public instruction_block::instruction_observer { class instruction_observer : public instruction_block::instruction_observer {