From c7b8fae58eb3ed56f20de4d9a7859fd3a15f1e89 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Thu, 12 Dec 2019 19:58:04 +0100
Subject: [PATCH] [lib] Rename __list_variant_constraints to
__precomputed_variant_constraints; Update doc max_step can't be >= to
__precomputed_variant_constraints
---
.../clause_constraints/mcl/CLUnfolder.py | 72 +++++++++++--------
.../clause_constraints/mcl/TestCLUnfolder.py | 2 +-
2 files changed, 42 insertions(+), 32 deletions(-)
diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index 8e6cc89..a37c5d1 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -99,10 +99,14 @@ init_forward_unfolding():
Query data
- __invariant_constraints:
List of Query data
- - __list_variant_constraints:
+ - __precomputed_variant_constraints:
Query data (automatic merge of textual and DIMACS forms)
- __variant_constraints:
- Initilized with the first item of __list_variant_constraints
+ Initialized with the first item of __precomputed_variant_constraints
+ - __precomputed_dynamic_constraints:
+ Initialized with the whole previously shifted system
+ if the size of the system hasn't changed, and if no auxiliary
+ clauses has been added meanwhile.
Shifted attributes with __shift_step (nb of variables in the system):
- __forward_init_dynamic(): __dynamic_constraints:
@@ -138,8 +142,8 @@ shift():
- __shift_dynamic(): __dynamic_constraints:
Shift + append of the last element of __dynamic_constraints
- __shift_variant(): __variant_constraints:
- Shift clauses of the current step in __list_variant_constraints, and
- append them to __variant_constraints.
+ Shift clauses of the current step in __precomputed_variant_constraints,
+ and append them to __variant_constraints.
- __shift_invariant()
...
- __shift_final()
@@ -359,7 +363,7 @@ class CLUnfolder(object):
"""Reset the unfolder before a new query
Reset only properties and dimacs clauses from the current query;
- AND __list_variant_constraints.
+ AND __precomputed_variant_constraints.
=> __initial_constraints, __final_constraints, __invariant_constraints,
__variant_constraints and __dynamic_constraints ARE NOT reset here
@@ -379,7 +383,7 @@ class CLUnfolder(object):
self.__variant_property = None # list<logic formulas>
self.__dimacs_variant = None # list<list<DIMACS clauses>>
# list of variant temporal constraints in Dimacs ground code
- self.__list_variant_constraints = None # list<list<DIMACS clauses>>
+ self.__precomputed_variant_constraints = None # list<list<DIMACS clauses>>
# If this function is called from the constructor,
# the following variables are just redefined here.
@@ -918,8 +922,8 @@ class CLUnfolder(object):
def __shift_variant(self):
"""Shift variant property - depends on unfolding direction
- Shift clauses of the current step in __list_variant_constraints, and
- append them to __variant_constraints.
+ Shift clauses of the current step in __precomputed_variant_constraints,
+ and append them to __variant_constraints.
.. warning:: Refactor note: unclear function. No apparent reason for
only the first clause to be shifted...
@@ -937,11 +941,11 @@ class CLUnfolder(object):
.. note:: Called by shift()
"""
- if not self.__list_variant_constraints:
+ if not self.__precomputed_variant_constraints:
return
if self.__shift_direction == "FORWARD":
# Constraint t0 already included from the query during initialisation
- current_constraint = self.__list_variant_constraints[self.__current_step]
+ current_constraint = self.__precomputed_variant_constraints[self.__current_step]
# Shift constraints at current step and append them to __variant_constraints
for clause in current_constraint:
s_clause = self.__m_shift_clause(clause, self.__current_step)
@@ -963,8 +967,8 @@ class CLUnfolder(object):
Shift + append of the last element of __dynamic_constraints
- __invariant_constraints[-1] (last element)
Shift + append of the last element of __invariant_constraints
- - __list_variant_constraints[current_step]
- Shift clauses of the current step in __list_variant_constraints,
+ - __precomputed_variant_constraints[current_step]
+ Shift clauses of the current step in __precomputed_variant_constraints,
and append them to __variant_constraints.
- __final_constraints if __shift_direction is "FORWARD"
- __initial_constraints if __shift_direction is "BACKWARD"
@@ -1166,27 +1170,27 @@ class CLUnfolder(object):
The two variant constraint forms must be compatible (same length) in
order to allow a merge.
- self.__list_variant_constraints:
+ self.__precomputed_variant_constraints:
Built here and is used later to shift current variant properties
and update self.__variant_constraints in __shift_variant().
self.__variant_constraints:
- the only element passed to the solver.
- - initilised with the first item of self.__list_variant_constraints
+ - initilised with the first item of self.__precomputed_variant_constraints
"""
# coding of variant properties
# Take __variant_property in priority on __dimacs_variant
if self.__variant_property:
- self.__list_variant_constraints = list()
+ self.__precomputed_variant_constraints = list()
for prop in self.__variant_property:
# compile initial (X0) property into numeric form
# For each property in step of __variant_property
- self.__list_variant_constraints.append(
+ self.__precomputed_variant_constraints.append(
[self.__code_clause(clause)
for clause in self.__compile_event(prop)]
)
- print(self.__list_variant_constraints)
+ print(self.__precomputed_variant_constraints)
if self.__dimacs_variant:
# Add DIMACS aux clauses initial properties
@@ -1199,26 +1203,26 @@ class CLUnfolder(object):
# Merge together all steps content
# Ex:
- # __list_variant_constraints due to __variant_property convertion:
+ # __precomputed_variant_constraints due to __variant_property convertion:
# [[], [[4]], [], []]
# __dimacs_variant:
# [[], [[4]], [[6], [7]], []]
# Result:
# [[], [[4], [4]], [[6], [7]], []]
- self.__list_variant_constraints = \
+ self.__precomputed_variant_constraints = \
[list(it.chain(*cpl)) for cpl
- in zip(self.__dimacs_variant, self.__list_variant_constraints)]
+ in zip(self.__dimacs_variant, self.__precomputed_variant_constraints)]
elif self.__dimacs_variant:
# No __variant_property, keep only __dimacs_variant
- self.__list_variant_constraints = self.__dimacs_variant
+ self.__precomputed_variant_constraints = self.__dimacs_variant
# Initialisation
- if self.__list_variant_constraints:
+ if self.__precomputed_variant_constraints:
if self.__shift_direction == "FORWARD":
# For now, keep only the events of the first step (t0)
# Other steps are taken during shift() calls
- self.__variant_constraints = self.__list_variant_constraints[0]
+ self.__variant_constraints = self.__precomputed_variant_constraints[0]
elif self.__shift_direction == "BACKWARD":
raise MCLException("Not yet implemented")
else:
@@ -1242,10 +1246,14 @@ class CLUnfolder(object):
Query data
- __invariant_constraints:
List of Query data
- - __list_variant_constraints:
+ - __precomputed_variant_constraints:
Query data (automatic merge of textual and DIMACS forms)
- __variant_constraints:
- Initilized with the first item of __list_variant_constraints
+ Initialized with the first item of __precomputed_variant_constraints
+ - __precomputed_dynamic_constraints:
+ Initialized with the whole previously shifted system
+ if the size of the system hasn't changed, and if no auxiliary
+ clauses has been added meanwhile.
Shifted attributes with __shift_step (nb of variables in the system):
- __dynamic_constraints:
@@ -1447,7 +1455,8 @@ class CLUnfolder(object):
is not tested for interesting variables like in squery_solve().
.. note:: This function checks and corrects incoherent data on step number.
- __steps_before_check can't be >= max_step
+ __steps_before_check can't be >= max_step.
+ max_step can't be >= to __precomputed_variant_constraints.
:param max_step: The horizon on which the properties must be satisfied.
:type max_step: <int>
@@ -1455,8 +1464,8 @@ class CLUnfolder(object):
# Initialization
self.init_forward_unfolding()
# Horizon adjustment
- if self.__list_variant_constraints:
- max_step = min(max_step, len(self.__list_variant_constraints)-1) ## TODO: -1 ?
+ if self.__precomputed_variant_constraints:
+ max_step = min(max_step, len(self.__precomputed_variant_constraints)-1)
if self.__invariant_property and not self.__final_property:
# 1 satisfiability test is made only after all shift() calls for each step
@@ -1511,7 +1520,8 @@ class CLUnfolder(object):
Otherwise, 1 test is made for each remaining step after each shift() call.
.. note:: This function checks and corrects incoherent data on step number.
- __steps_before_check can't be >= max_step
+ __steps_before_check can't be >= max_step.
+ max_step can't be >= to __precomputed_variant_constraints.
:param max_step: bounded horizon for computations
:param max_sol: The maximum number of solutions to be returned
@@ -1529,8 +1539,8 @@ class CLUnfolder(object):
# Initialization
self.init_forward_unfolding()
# Horizon adjustment
- if self.__list_variant_constraints:
- max_step = min(max_step, len(self.__list_variant_constraints)-1) ## TODO: -1 ?
+ if self.__precomputed_variant_constraints:
+ max_step = min(max_step, len(self.__precomputed_variant_constraints)-1)
if self.__invariant_property and not self.__final_property:
# Shift all remaining steps
diff --git a/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py
index dfea5cf..33cf753 100644
--- a/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py
@@ -462,7 +462,7 @@ def test_init_forward(feed_mclanalyser, textual_properties, numerical_properties
self.__dimacs_variant = None # list<list<DIMACS clauses>>
CLUnfolder attributes that contain clauses:
- self.__list_variant_constraints = None # list<list<DIMACS clauses>>
+ self.__precomputed_variant_constraints = None # list<list<DIMACS clauses>>
dynamic_constraints => __dynamic_constraints
initial_constraints => __initial_constraints
--
GitLab