Commit 44ce61b5 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

Last few improvements in code exec

parent ced3e88e
......@@ -651,21 +651,37 @@ class CLUnfolder(object):
base variable form - we have to wait until all variables are num coded
before shifting anything!!
"""
self.__initial_constraints = []
if no_frontier_init:
# OLD
# self.__initial_constraints = []
# if no_frontier_init:
# # initialize no frontier places to False
# for nfp in self.__no_frontier_init:
# self.__initial_constraints.append(nfp)
# if self.__initial_property:
# # compile initial property
# l_clauses = self.__compile_property(self.__initial_property)
# # compile numeric form
# for clause in l_clauses:
# self.__initial_constraints.append(self.__code_clause(clause))
# # dimacs aux initial properties
# dim_init = self.__dim_initial
# if dim_init:
# self.__initial_constraints = self.__initial_constraints + dim_init
self.__initial_constraints = list()
# initialize no frontier places to False
for nfp in self.__no_frontier_init:
self.__initial_constraints.append(nfp)
if no_frontier_init:
self.__initial_constraints += [elem for elem in self.__no_frontier_init]
if self.__initial_property:
# compile initial property
l_clauses = self.__compile_property(self.__initial_property)
# compile numeric form
for clause in l_clauses:
self.__initial_constraints.append(self.__code_clause(clause))
self.__initial_constraints += [self.__code_clause(clause) for clause in self.__compile_property(self.__initial_property)]
# dimacs aux initial properties
dim_init = self.__dim_initial
if dim_init:
self.__initial_constraints = self.__initial_constraints + dim_init
if self.__dim_initial:
self.__initial_constraints += self.__dim_initial
def set_final_property(self, property_text):
"""
......@@ -1072,18 +1088,18 @@ class CLPropertyVisitor(object):
notnl2 = nl2.lit_not()
# clauses generation
if operator == 'and': # x = lh and rh
cl1 = Clause([nl1, notnl]) # not x or not lh
cl2 = Clause([nl2, notnl]) # not x or not rh
cl3 = Clause([notnl1, notnl2, newl]) # x or not lh or not 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
if operator == 'or': # x = lh or rh
cl1 = Clause([notnl1, newl]) # x or not lh
cl2 = Clause([notnl2, newl]) # x or not rh
cl3 = Clause([nl1, nl2, notnl]) # not x or not lh or not 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.append(cl1)
self.clauses.append(cl2)
self.clauses.append(cl3)
# self.clauses.append(cl1)
# self.clauses.append(cl2)
# self.clauses.append(cl3)
if top:
self.clauses.append(Clause([newl]))
return None
......
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