From 3e019d57fab57afe7aad373385f32a23bd178941 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Mon, 17 Jul 2017 10:13:31 +0200 Subject: Initial commit. --- instr-to-kodkod/src/VHDLType.java | 76 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) create mode 100644 instr-to-kodkod/src/VHDLType.java (limited to 'instr-to-kodkod/src/VHDLType.java') diff --git a/instr-to-kodkod/src/VHDLType.java b/instr-to-kodkod/src/VHDLType.java new file mode 100644 index 0000000..c4c1b0f --- /dev/null +++ b/instr-to-kodkod/src/VHDLType.java @@ -0,0 +1,76 @@ +/* FIXME: Finer imports */ +import java.util.*; + +import kodkod.ast.*; +import kodkod.ast.operator.*; + +import kodkod.instance.*; + + +public class VHDLType +{ + private final Map members; + private final String name; + private final Relation as_relation; + + public VHDLType (final String name) + { + members = new HashMap(); + + this.name = name; + as_relation = Relation.unary(name); + } + + public void add_member (final String id) + { + members.put(id, Relation.unary(id)); + } + + public String get_name () + { + return name; + } + + public Relation get_as_relation () + { + return as_relation; + } + + + public Relation get_member_as_relation (final String id) + { + return members.get(id); + } + + public Collection get_all_members_as_atoms () + { + return members.keySet(); + } + + public Formula generate_declarations () + { + Formula result; + + result = Formula.TRUE; + + return result; + } + + public void add_to_bounds (final Bounds b, final TupleFactory f) + { + final Set> members_as_set; + + members_as_set = members.entrySet(); + + for (final Map.Entry member: members_as_set) + { + b.boundExactly(member.getValue(), f.setOf(member.getKey())); + } + + /* + * the toArray() is required to avoid the collection being considered as + * a single atom. + */ + b.boundExactly(as_relation, f.setOf(get_all_members_as_atoms().toArray())); + } +} -- cgit v1.2.3-70-g09d2