Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit d00efdc2 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Various and minor rewrites for optimization

parent 588ca633
......@@ -276,10 +276,7 @@ class CLUnfolder(object):
@param var_num: DIMACS literal coding of an initial variable
@return: name of the variable
"""
if var_num < 0:
varnum1 = -var_num
else: varnum1 = var_num
var_code = (varnum1 - 1) % self.__shift_step + 1
var_code = (abs(var_num) - 1) % self.__shift_step + 1
if var_code <= self.__shift_step_init: # variable from initial system
return self.__var_list[var_code]
else: # auxiliary variable introduced by properties compilation
......@@ -291,9 +288,7 @@ class CLUnfolder(object):
@param var_num: DIMACS literal coding
@return: name of the variable with time index
"""
if var_num < 0:
varnum1 = -var_num
else: varnum1 = var_num
varnum1 = abs(var_num)
var_code = (varnum1 - 1) % self.__shift_step + 1
var_step = (varnum1 - var_code)/self.__shift_step
if var_code <= self.__shift_step_init:
......@@ -1105,14 +1100,18 @@ class CLPropertyVisitor(object):
notnl2 = nl2.lit_not()
# clauses generation
if operator == 'and': # x = lh and rh
self.clauses.append(Clause([nl1, notnl])) # not x or not lh
self.clauses.append(Clause([nl2, notnl])) # not x or not rh
self.clauses.append(Clause([notnl1, notnl2, newl])) # x or not lh or not rh
self.clauses.extend([
Clause([nl1, notnl]), # not x or not lh
Clause([nl2, notnl]), # not x or not rh
Clause([notnl1, notnl2, newl]) # x or not lh or not rh
])
if operator == 'or': # x = lh or rh
self.clauses.append(Clause([notnl1, newl])) # x or not lh
self.clauses.append(Clause([notnl2, newl])) # x or not rh
self.clauses.append(Clause([nl1, nl2, notnl])) # not x or not lh or not rh
self.clauses.extend([
Clause([notnl1, newl]), # x or not lh
Clause([notnl2, newl]), # x or not rh
Clause([nl1, nl2, notnl]) # not x or not lh or not rh
])
# self.clauses.append(cl1)
# self.clauses.append(cl2)
......
......@@ -425,11 +425,7 @@ class MCLAnalyser(object):
"""
mac_list = self.__mac_exhaustive_search(query, nb_step)
# convert to FrontierSolution list
vmac_list = []
for mac in mac_list:
vmac = FrontierSolution.from_dimacs_front_sol(mac)
vmac_list.append(vmac)
return vmac_list
return tuple(FrontierSolution.from_dimacs_front_sol(mac) for mac in mac_list)
def is_strong_activator(self, act_sol, query):
"""
......@@ -439,7 +435,7 @@ class MCLAnalyser(object):
"""
nb_step = len(act_sol.ic_sequence) - 1
query_1 = MCLSimpleQuery.from_frontier_sol_same_timing(act_sol,
self.unfolder)
self.unfolder)
inv_prop = 'not('+query.final_prop+')'
query_2 = MCLSimpleQuery(None, inv_prop, None)
query_1 = query_2.merge(query_1)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment