From c83779c9d5bf26960b502efeee8360abc8318fc9 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 13 Aug 2017 15:51:20 +0100
Subject: [PATCH] Declaration of the intermediate product variables for the
 reactions and entities that are actually used as products

---
 ...action_system_with_concentrations_param.py | 22 ++++++---
 rs_testing.py                                 |  2 +-
 smt/smt_checker_rsc_param.py                  | 48 +++++++++++++++++--
 3 files changed, 62 insertions(+), 10 deletions(-)

diff --git a/rs/reaction_system_with_concentrations_param.py b/rs/reaction_system_with_concentrations_param.py
index 20e2134..3dde9b3 100644
--- a/rs/reaction_system_with_concentrations_param.py
+++ b/rs/reaction_system_with_concentrations_param.py
@@ -201,19 +201,29 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
         self.show_meta_reactions()
         self.show_max_concentrations()
         
+    def get_producible_entities(self):
+        """
+        Returns the set of entities that appear as products of 
+        reactions.
+        """
+        
+        producible_entities = set()
+
+        for reaction in self.reactions:
+            product_entities = [e for e,c in reaction[2] if c > 0]
+            producible_entities = producible_entities.union(set(product_entities))
+            
+        return producible_entities
+        
     def get_reactions_by_product(self):
         """Sorts reactions by their products and returns a dictionary of products"""
 
-        assert False
+        # assert False
 
         if self.reactions_by_prod != None:
             return self.reactions_by_prod
 
-        producible_entities = set()
-
-        for reaction in self.reactions:
-            product_entities = [e for e,c in reaction[2]]
-            producible_entities = producible_entities.union(set(product_entities))
+        producible_entities = self.get_producible_entities()
 
         reactions_by_prod = {}
 
diff --git a/rs_testing.py b/rs_testing.py
index 4e61f7b..641bf88 100644
--- a/rs_testing.py
+++ b/rs_testing.py
@@ -90,7 +90,7 @@ def example44_param():
     #         )
     #     )
     # ))
-    # smt_rsc.check_rsltl(formula=neg_f1)
+    smt_rsc.check_rsltl(formula=neg_f1)
     
 def example44():
     
diff --git a/smt/smt_checker_rsc_param.py b/smt/smt_checker_rsc_param.py
index 399c3a6..8051744 100644
--- a/smt/smt_checker_rsc_param.py
+++ b/smt/smt_checker_rsc_param.py
@@ -34,7 +34,13 @@ class SmtCheckerRSCParam(object):
         self.v = []
         self.v_ctx = []
         self.ca_state = []
+        
+        # intermediate products:
+        self.v_improd = []
+
         self.next_level_to_encode = 0
+
+        self.producible_entities = self.rs.get_producible_entities()
         
         self.loop_position = Int("loop_position")
         
@@ -48,14 +54,15 @@ class SmtCheckerRSCParam(object):
         self.initialise()
         
     def prepare_all_variables(self):
-        """Encodes all the variables"""
+        """Prepares all the variables"""
 
         self.prepare_state_variables()
         self.prepare_context_variables()
+        self.prepare_intermediate_product_variables()
         self.next_level_to_encode += 1
         
     def prepare_context_variables(self):
-        """Encodes all the context variables"""
+        """Prepares all the context variables"""
 
         level = self.next_level_to_encode
 
@@ -66,7 +73,7 @@ class SmtCheckerRSCParam(object):
         self.v_ctx.append(variables)
 
     def prepare_state_variables(self):
-        """Encodes all the state variables"""
+        """Prepares all the state variables"""
 
         level = self.next_level_to_encode
 
@@ -77,6 +84,41 @@ class SmtCheckerRSCParam(object):
         
         self.ca_state.append(Int("CA"+str(level)+"_state"))
 
+    def prepare_intermediate_product_variables(self):
+        """
+        Prepares the intermediate product variables
+        carrying the individual concentration levels produced
+        the reactions.
+
+        These variables are used later on to encode the final
+        concentration levels for all the entities
+        """
+
+        level = self.next_level_to_encode
+
+        if level < 1:
+            self.v_improd.append([])
+        else:
+
+            variables = []
+            number_of_reactions = len(self.rs.reactions)
+
+            for reaction in self.rs.reactions:
+                *_, products = reaction
+
+                reaction_id = self.rs.reactions.index(reaction)
+
+                entities_dict = dict()
+                for entity, _ in products:
+                    varname = Int("IP" + str(level) + "_R" +
+                                  str(reaction_id) + "_e" + str(entity))
+                    entities_dict[entity] = varname
+
+                variables.append(entities_dict)
+
+            self.v_improd.append(variables)
+
+        
     def enc_concentration_levels_assertion(self, level):
         """Encodes assertions that (some) variables need to be >0