Skip to content

Commit b8fb5cf

Browse files
committed
abstract constant name instead of variable, fixed indentation
1 parent 323549b commit b8fb5cf

File tree

1 file changed

+3
-6
lines changed

1 file changed

+3
-6
lines changed

localize.py

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#!/usr/bin env python 2.7
21
"""
32
Localize
43
Iterates the axioms in a ProverX object and replaces one of its variables with a constant
@@ -7,7 +6,7 @@
76
__authors__ = "Afonso Bras Sousa, Manuel Madelino, Henrique Duarte"
87
__maintainer__ = "Afonso Bras Sousa"
98
__email__ = "[email protected]"
10-
__version__ = 0.1
9+
__version__ = 0.2
1110

1211
import copy
1312
import re
@@ -52,15 +51,15 @@ def replaceAxiom(obj, oldAxiom, newAxiom):
5251
Iterates the axioms in a ProverX object and replaces one of its variables with a constant
5352
Ignores axioms in the ignore list
5453
"""
55-
def localize(obj, goal, ignore_list=[]):
54+
def localize(obj, goal, ignore_list=[],constant_name="cLOCAL"):
5655
result = []
5756
obj.goals.replace(goal) # replace original goals with our localize goal
5857
for axiom in obj.axioms:
5958
if axiom in ignore_list: continue # ignore axioms in ignore_list
6059
vars = getVars(axiom)
6160
for var in vars:
6261
# print "DEBUG %s" % var
63-
newAxiom = localizeVar(axiom, var, CONSTANT) # replace a variable with a constant
62+
newAxiom = localizeVar(axiom, var, constant_name) # replace a variable with a constant
6463
newObj = replaceAxiom(obj, axiom, newAxiom) # replace the original axiom with our localized axiom
6564
newObj = newObj.find_both() # check for proof
6665
if newObj.proofs.found:
@@ -71,8 +70,6 @@ def localize(obj, goal, ignore_list=[]):
7170
Main function
7271
"""
7372

74-
CONSTANT = "cLOCAL" # set name of constant
75-
7673
example = Proverx('abelian.in') # load a proverX file
7774
result = localize(example, "L(a) -> L(a').") # returns list of proverX objects where the specified goal proof was found -- in this case for L(a) -> L(a')
7875

0 commit comments

Comments
 (0)