fixed regressions

ivy/ivy_alpha.py

@@ -12,6 +12,8 @@ from ivy_logic_utils import *
 from ivy_concept_space import *
 from ivy_utils import Parameter
 
+test_bottom = True
+
 def alpha(state):
 #    print "prestate: {}".format(state.clauses)
     d = ProgressiveDomain(state.domain.concept_spaces,verbose = False)
@@ -111,8 +113,7 @@ class ProgressiveDomain(object):
             print "concrete state: %s" % theory
             print "background: %s" % background_theory
         add_clauses(self.solver, and_clauses(theory,background_theory))
-#        self.unsat = self.solver.check() == z3.unsat
-        self.unsat = False
+        self.unsat = test_bottom and self.solver.check() == z3.unsat
         if self.unsat:
             print "core: %s" % unsat_core(and_clauses(theory,background_theory),true_clauses())
         

ivy/ivy_ast.py

@@ -1059,7 +1059,12 @@ def subst_subscripts_comp(s,subst):
 #    print 'g: {}'.format(g)
     if not g:
         return s
-    res =  str_subst(g[0],subst) + ''.join(('[' + str_subst(x[1:-1],subst) + ']' if x.startswith('[') else x) for x in g[1:])
+    pref = str_subst(g[0],subst)
+    if isinstance(pref,This):
+        if len(g) > 1:
+            raise iu.IvyError(None,'cannot substitute "this" for {} in {}'.format(g[0],s))
+        return pref
+    res =  pref + ''.join(('[' + str_subst(x[1:-1],subst) + ']' if x.startswith('[') else x) for x in g[1:])
 #    print "res: {}".format(res)
     return res
 
@@ -1067,8 +1072,11 @@ def subst_subscripts(s,subst):
 #    return compose_names(*[subst_subscripts_comp(t,subst) for t in split_name(s)])
     return subst_subscripts_comp(s,subst)
 
+def my_base_name(x):
+    return x if isinstance(x,This) else base_name(x)
+
 def base_name_differs(x,y):
-    return base_name(x) != base_name(y)
+    return my_base_name(x) != my_base_name(y)
 
 class AstRewriteSubstConstants(object):
     def __init__(self,subst):
@@ -1141,7 +1149,7 @@ def ast_rewrite(x,rewrite):
         copy_attributes_ast(x,atom)
         if hasattr(x,'sort'):
             atom.sort = rewrite_sort(rewrite,x.sort)
-        if not isinstance(x.rep,This) and base_name_differs(x.rep,atom.rep):
+        if base_name_differs(x.rep,atom.rep):
             return atom
         return rewrite.rewrite_atom(atom)
     if isinstance(x,Literal):

ivy/ivy_check.py

@@ -157,6 +157,8 @@ def check_module():
 def main():
     import signal
     signal.signal(signal.SIGINT,signal.SIG_DFL)
+    import ivy_alpha
+    ivy_alpha.test_bottom = False # this prevents a useless SAT check
     ivy_init.read_params()
     if len(sys.argv) != 2 or not sys.argv[1].endswith('ivy'):
         usage()

ivy/ivy_compiler.py

@@ -531,10 +531,10 @@ def compile_action_def(a,sig):
             for suba in res.iter_subactions():
                 if isinstance(suba,CallAction):
                     if any(lu.used_variables_ast(a) for a in suba.args[0].args):
-                        iu.dbg('a.args[0]')
-                        iu.dbg('a.formal_params')
-                        iu.dbg('suba.lineno')
-                        iu.dbg('suba')
+#                        iu.dbg('a.args[0]')
+#                        iu.dbg('a.formal_params')
+#                        iu.dbg('suba.lineno')
+#                        iu.dbg('suba')
                         raise iu.IvyError(suba,"call may not have free variables")
             res.formal_params = formals
             res.formal_returns = returns

ivy/ivy_graph_ui.py

@@ -311,8 +311,6 @@ class GraphWidget(object):
             with self.ui_parent.run_context():  # to catch errors
                 lit = self.g.string_to_concept(text)
                 self.add_concept(lit)
-                iu.dbg('"after add_concept"')
-            iu.dbg('"after with"')
 
 
     # Record the current goal with a string name
@@ -329,9 +327,7 @@ class GraphWidget(object):
 
     def update_relations(self):
         if self.update_callback != None:
-            iu.dbg('"before update_callback"')
             self.update_callback()
-            iu.dbg('"after update_callback"')
             
         
 

ivy/ivy_isolate.py

@@ -1371,9 +1371,6 @@ def check_isolate_completeness(mod = None):
         for callee in action.iter_calls():
             if not (callee in checked or not has_assertions(mod,callee)
                     or callee in delegates and actname in checked_context[callee]):
-                iu.dbg('callee')
-                iu.dbg('actname')
-                iu.dbg('checked_context[callee]')
                 missing.append((actname,callee,None))
             for mixin in mod.mixins[callee]:
                 mixed = mixin.args[0].relname

ivy/ivy_logic.py

@@ -995,8 +995,6 @@ def all_concretely_sorted(*terms):
 def check_concretely_sorted(term,no_error=False,unsorted_var_names=()):
     for x in chain(lu.used_variables(term),lu.used_constants(term)):
         if lg.contains_topsort(x.sort) or lg.is_polymorphic(x.sort):
-            iu.dbg('unsorted_var_names')
-            iu.dbg('x.name')
             if x.name not in unsorted_var_names:
                 if no_error:
                     raise lg.SortError

ivy/ivy_theory.py

@@ -167,7 +167,7 @@ def create_strat_map(assumes,asserts,macros):
 #    for f in all_fmlas:
 #        print f
     symbols_over_universals = il.symbols_over_universals(all_fmlas)
-    iu.dbg('[str(x) for x in symbols_over_universals]')
+#    iu.dbg('[str(x) for x in symbols_over_universals]')
     universally_quantified_variables = il.universal_variables(all_fmlas)
     
     strat_map = defaultdict(UFNode)

ivy/ivy_to_cpp.py

@@ -1812,7 +1812,6 @@ class z3_thunk : public thunk<D,R> {
     for native in im.module.natives:
         tag = native_type(native)
         if tag == "init":
-            iu.dbg('native')
             vs = [il.Symbol(v.rep,im.module.sig.sorts[v.sort]) for v in native.args[0].args] if native.args[0] is not None else []
             global indent_level
             indent_level += 1

ivy/ivy_ui_util.py

@@ -103,9 +103,7 @@ def center_window_on_window(toplevel,win):
     toplevel.geometry("%dx%d+%d+%d" % (size + (x, y)))
 
 def destroy_then_aux(dlg,command):
-    iu.dbg('"command started"')
     command()
-    iu.dbg('"command finished"')
     dlg.destroy()
 
 def destroy_then(dlg,command):

ivy/tk_graph_ui.py

@@ -270,15 +270,10 @@ class TkGraphWidget(TkCyCanvas,uu.WithMenuBar):
     # Call this when UI needs to be updated.
 
     def update(self):
-        iu.dbg('"updating graph"')
         self.delete(ALL)
-        iu.dbg('"after delete"')
         self.sync_checkboxes()
-        iu.dbg('"after sync checkboxes"')
         self.g.recompute()
-        iu.dbg('"after recompute"')
         self.rebuild()
-        iu.dbg('"after rebuild"')
 
 
 # Wrap a concept graph object in a user interface
@@ -379,7 +374,6 @@ def update_relbuttons(gw,rb):
     line_color = gw.line_color
     command = gw.update
     for idx,(num,rel) in enumerate(rels):
-        iu.dbg('rel')
         label = gw.g.concept_label(gw.g.concept_from_id(rel))
         btns.add(str(idx+1))
         foo = Checkbutton(btns,fg=line_color(num),variable=gw.get_enabled(rel)[0],command=command)
@@ -419,7 +413,6 @@ def update_relbuttons(gw,rb):
 # #        foo.bind("<Button-1>", lambda e: askcolor())
 #         foo = Checkbutton(btns,fg=line_color(num),variable=gw.get_enabled(rel)[3],command=command)
 #         foo.grid(row = idx+1, column = 4)
-    iu.dbg('"finished updating relbuttons"')
         
 
 def onFrameConfigure(canvas):