artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Max encoding, WIP

Browse Source
This commit is contained in:
Artur Meski
2017-08-14 21:31:43 +01:00
parent 9ca4d3954f
commit 15cbf62e82
1 changed files with 42 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

44
smt/smt_checker_rsc_param.py
View File

@@ -39,6 +39,8 @@ class SmtCheckerRSCParam(object):
# intermediate products: # intermediate products:
self.v_improd = [] self.v_improd = []
self.v_improd_for_entities = []
self.next_level_to_encode = 0 self.next_level_to_encode = 0
self.producible_entities = self.rs.get_producible_entities() self.producible_entities = self.rs.get_producible_entities()
@@ -109,27 +111,36 @@ class SmtCheckerRSCParam(object):
# which are always at level+1. # which are always at level+1.
# #
self.v_improd.append(None) self.v_improd.append(None)
self.v_improd_for_entities.append(None)
else: else:
reactions_dict = dict() reactions_dict = dict()
number_of_reactions = len(self.rs.reactions) number_of_reactions = len(self.rs.reactions)
all_entities_dict = dict()
for reaction in self.rs.reactions: for reaction in self.rs.reactions:
*_, products = reaction *_, products = reaction
reaction_id = self.rs.reactions.index(reaction) reaction_id = self.rs.reactions.index(reaction)
entities_dict = dict() entities_dict = dict()
for entity, _ in products: for entity, conc in products:
varname = Int("IP" + str(level) + "_R" + varname = Int("IP" + str(level) + "_R" +
str(reaction_id) + "_e" + str(entity)) str(reaction_id) + "_e" + str(entity))
entities_dict[entity] = varname entities_dict[entity] = varname
all_entities_dict.setdefault(entity, [])
all_entities_dict[entity].append((conc,varname))
reactions_dict[reaction_id] = entities_dict reactions_dict[reaction_id] = entities_dict
self.v_improd.append(reactions_dict) self.v_improd.append(reactions_dict)
self.v_improd_for_entities.append(all_entities_dict)
print(self.v_improd) print(self.v_improd)
print(self.v_improd_for_entities)
def enc_concentration_levels_assertion(self, level): def enc_concentration_levels_assertion(self, level):
""" """
@@ -166,7 +177,7 @@ class SmtCheckerRSCParam(object):
def enc_transition_relation(self, level): def enc_transition_relation(self, level):
return simplify(And(self.enc_rs_trans(level), self.enc_automaton_trans(level))) return simplify(And(self.enc_rs_trans(level), self.enc_automaton_trans(level)))
def enc_rs_trans(self, level): def enc_rs_trans(self, level):
@@ -220,9 +231,38 @@ class SmtCheckerRSCParam(object):
# #
# Max of all the produced concentrations for each entity/product... # Max of all the produced concentrations for each entity/product...
enc_max_prod = True
current_v_improd_for_entities = self.v_improd_for_entities[level+1]
for entity, per_reaction_vars in current_v_improd_for_entities.items():
# enc_max_single_ent = True
sorted_vars_by_conc = sorted(per_reaction_vars, key=lambda conc_var: conc_var[0])
list_of_vars = [v for c,v in sorted_vars_by_conc]
print(list_of_vars)
return enc_trans return enc_trans
# def enc_max(self, elements):
#
# if len(elements) == 1:
# return elements[0]
#
# elif len(elements) > 1:
#
# # If(a > b, a, b)
# def MAX(a, b):
# return If(a > b, a, b)
#
# for i in range(1,len(elements)):
# MAX(elements[])
#
# else:
# return None
#
def enc_automaton_trans(self, level): def enc_automaton_trans(self, level):
"""Encodes the transition relation for the context automaton""" """Encodes the transition relation for the context automaton"""