new gui does leader example pretty well

ivy/concept_alpha.py

@@ -27,7 +27,7 @@ def alpha(concept_domain, state, cache=None, projection=None):
 
     slvr.solver_add(solver,state)
 
-    iu.dbg('state')
+#    iu.dbg('state')
 
     if cache is None:
         cache = dict()
@@ -35,7 +35,7 @@ def alpha(concept_domain, state, cache=None, projection=None):
     for tag, formula in facts:
         if tag in cache:
             value = cache[tag]
-#           print "cached: {} = {}".format(tag,value)
+#            print "cached: {} = {}".format(tag,value)
         else:
             # assert len(cache) == 0, tag
             solver.push()

ivy/concept_interactive_session.py

@@ -256,7 +256,7 @@ class ConceptInteractiveSession(object):
         if filter_polarity is not None and filter_polarity != polarity:
             return []
 
-        return _get_edge_fact(edge,source,target,polarity)
+        return self._get_edge_fact(edge,source,target,polarity)
 
     def get_facts(self,projection=None):
         """

ivy/dot_layout.py

@@ -128,7 +128,7 @@ def _to_coord_list(st):
     return map(_to_position,pairs)
 
 
-def dot_layout(cy_elements,edge_labels=False,subgraph_boxes=False,node_gt=lambda X,y:False):
+def dot_layout(cy_elements,edge_labels=False,subgraph_boxes=False,node_gt=None):
     """
     Get a CyElements object and augment it (in-place) with positions,
     widths, heights, and spline data from a dot based layout.
@@ -157,12 +157,27 @@ def dot_layout(cy_elements,edge_labels=False,subgraph_boxes=False,node_gt=lambda
         "transitive" in e["data"] and
         e["data"]["transitive"]
     ]
-    print "order: {}".format(order)
     elements = topological_sort(elements, order, lambda e: e["data"]["id"])
 
+    # get the node id's and stable sort them by cluster
+    # the idea here is to convert the graph into a dag by sorting
+    # the nodes, then reversing the back edges. In particular, we try to make
+    # all the edges between two clusters go in the same direction so clustering
+    # doesn't result in horizontal edges, which dot renders badly.
+
+    sorted_nodes = [e["data"]["id"] for e in elements if e["group"] == "nodes"]
+    sorted_nodes = sorted(enumerate(sorted_nodes),key = lambda x: (nodes_by_id[x[1]]["data"]["cluster"],x[0]))
+    sorted_nodes = [y for idx,y in sorted_nodes]
+    node_key = dict((id,idx) for idx,id in enumerate(sorted_nodes))
+
+    if node_gt is None:
+        node_gt = lambda X,y:False
+    else:
+        node_gt = lambda x,y: node_key[x] > node_key[y] 
+
     # add nodes to the graph
     for e in elements:
-        if e["group"] == "nodes":
+        if e["group"] == "nodes" and e["classes"]  != 'non_existing':
             g.add_node(e["data"]["id"], label=e["data"]["label"].replace('\n', '\\n'))
 
     # TODO: remove this, it's specific to leader_demo
@@ -179,8 +194,8 @@ def dot_layout(cy_elements,edge_labels=False,subgraph_boxes=False,node_gt=lambda
     for e in elements:
         if e["group"] == "edges":
 #            kwargs = {'weight': weight.get(e["data"]["obj"], 0)},
-            kwargs = {'label':e["data"]["label"]}  if edge_labels else {'label':'     '}
-            if node_gt(e["data"]["source_obj"],e["data"]["target_obj"]):
+            kwargs = {'label':e["data"]["label"]}  if edge_labels else {}
+            if node_gt(e["data"]["source"],e["data"]["target"]):
                 g.add_edge(
                     e["data"]["target"],
                     e["data"]["source"],
@@ -201,7 +216,7 @@ def dot_layout(cy_elements,edge_labels=False,subgraph_boxes=False,node_gt=lambda
     # add clusters
     clusters = defaultdict(list)
     for e in elements:
-        if e["group"] == "nodes" and e["data"]["cluster"] is not None:
+        if e["group"] == "nodes" and e["data"]["cluster"] is not None and e["classes"]  != 'non_existing':
             clusters[e["data"]["cluster"]].append(e["data"]["id"])
     for i, k in enumerate(sorted(clusters.keys())):
         g.add_subgraph(
@@ -233,14 +248,14 @@ def dot_layout(cy_elements,edge_labels=False,subgraph_boxes=False,node_gt=lambda
                 y_origin = top
 
     for e in elements:
-        if e["group"] == "nodes":
+        if e["group"] == "nodes" and e["classes"]  != 'non_existing':
             attr = g.get_node(e["data"]["id"]).attr
             e["position"] = _to_position(attr['pos'])
             e["data"]["width"] = 72 * float(attr['width'])
             e["data"]["height"] = 72 * float(attr['height'])
 
         elif e["group"] == "edges":
-            if node_gt(e["data"]["source_obj"],e["data"]["target_obj"]):
+            if node_gt(e["data"]["source"],e["data"]["target"]):
                 attr = g.get_edge(e["data"]["target"], e["data"]["source"], e["data"]["id"]).attr
                 pos = attr['pos']
                 pe = pos.split()
@@ -250,11 +265,10 @@ def dot_layout(cy_elements,edge_labels=False,subgraph_boxes=False,node_gt=lambda
             else:
                 attr = g.get_edge(e["data"]["source"], e["data"]["target"], e["data"]["id"]).attr
                 pos = attr['pos']
-            iu.dbg("attr['pos']")
             e["data"].update(_to_edge_position(pos))
             if edge_labels and e["data"]["label"] != '':
                 e["data"]["lp"] = _to_position(attr['lp'])
-    g.draw('g.png')
+#    g.draw('g.png')
 
     if subgraph_boxes:
         for sg in g.subgraphs():

src/ivy/ivy_art.py

@@ -303,7 +303,7 @@ class AnalysisGraph(object):
         if clauses == None:
             clauses = state.clauses
         bg = self.domain.background_theory(state.in_scope)
-        print "bg: {}".format(bg)
+#        print "bg: {}".format(bg)
         sg = standard_graph(state)
         # TODO: following shouldn't be needed.
         sg.current.set_state(and_clauses(clauses,bg))
@@ -355,7 +355,6 @@ class AnalysisGraph(object):
     def copy_path(self,state,other,bound=None):
         other_state = State(other.domain)
         other_state.arg_node = state
-        print "foo: {}".format(state.id if hasattr(state,'id') else "None")
         if hasattr(state,'pred') and state.pred != None and bound != 0:
             next_bound = None if bound is None else bound - 1
             pred = self.copy_path(state.pred,other,next_bound)

src/ivy/ivy_graph.py

@@ -217,8 +217,6 @@ def render_concept_graph(widget):
     # add nodes
     non_existing_nodes = set()
 
-    iu.dbg('nodes')
-
     for node in nodes:
         if a[('node_info', 'none', node)]:
             non_existing_nodes.add(node)
@@ -367,7 +365,6 @@ def render_concept_graph(widget):
     return g
 
 def node_gt(n1,n2):
-    iu.dbg('n1')
     return n1 > n2
 
 # In concept labels, we drop the variable X from formulas
@@ -453,6 +450,10 @@ class Graph(object):
         """ Get a relational concept from its id """
         return concept.name
 
+    def edge_cy_id(self,edge):
+        """Get the cy_elements id of an edge """
+        return self.cy_elements.edge_id[tuple(self.id_from_concept(c) for c in edge)]
+
     @property
     def relations(self):
         """ Returns all the concepts that need check-boxes """
@@ -478,7 +479,7 @@ class Graph(object):
         if len(concept.variables) == 1:
             v = concept.variables[0]
             if can_abbreviate_formula(v,fmla):
-                res = str(ilu.substitute_ast(fmla,{v.rep:Variable('',v.sort)}))
+                res = il.fmla_to_str_ambiguous(ilu.substitute_ast(fmla,{v.rep:Variable('',v.sort)}))
                 return res.replace(' ','').replace('()','')
         return str(fmla)
 
@@ -539,7 +540,6 @@ class Graph(object):
 
     def set_state(self,clauses,recomp=True,clear_constraints=False,reset=False):
         self.state = clauses        
-        iu.dbg('self.concept_session.state')
         
         if clear_constraints:
             self.concept_session.suppose_constraints = []
@@ -557,7 +557,6 @@ class Graph(object):
 
     def get_facts(self,rels,definite=True):
         facts = self.concept_session.get_facts(self.projection)
-        iu.dbg('facts')
         self.concept_session.suppose_constraints = facts
 
     def set_facts(self,facts):
@@ -593,7 +592,6 @@ class Graph(object):
                 res = any(boxes[i].value for i in boxes if i != 'transitive')
             else:
                 res = boxes[concept_combiner].value
-                iu.dbg('res')
             return res
         return True
 

src/ivy/ivy_graph_ui.py

@@ -230,12 +230,28 @@ class GraphWidget(object):
         self.g.get_facts(rels)
         self.update()
 
+    def clear_elem_selection(self):
+        self.node_selection = set()
+        self.edge_selection = set()
+
+    def highlight_selected_facts(self):
+        self.clear_elem_selection()
+        if hasattr(self,'fact_elems'):
+            for fact in self.get_active_facts():
+                for elem in self.fact_elems[fact]:
+                    concepts = map(self.g.concept_from_id,elem)
+                    if len(elem) == 1: # a node
+                        self.select_node(concepts[0],True)
+                    elif len(elem) == 3: # an edge
+                        self.select_edge(concepts,True)
+
     # Set the current facts
     
     def set_facts(self,facts):
         self.checkpoint()
         self.g.set_facts(facts)
         self.update()
+            
         
     # Find a current fact whose printed form is "text"
 
@@ -328,7 +344,6 @@ class GraphWidget(object):
         self.checkpoint()
         self.g.parent_state = new_parent_state
         self.g.set_state(clauses if clauses else new_parent_state.clauses, reset=reset)
-        iu.dbg('self.g.relation_ids')
         self.update_relations()
         self.update()
                          
@@ -355,7 +370,6 @@ class GraphWidget(object):
     def set_state(self,clauses):
         self.checkpoint()
         self.g.set_state(clauses)
-        iu.dbg('self.g.relation_ids')
         self.update_relations()
         self.update()
 
@@ -495,7 +509,6 @@ class GraphWidget(object):
     # tick a checkbox on a concept
 
     def show_relation(self,concept,boxes='+',value=True,update=True):
-        iu.dbg('concept')
         for box in boxes:
             self.show_edge(concept,box,value)
         if update:

src/ivy/ivy_isolate.py

@@ -281,14 +281,10 @@ def isolate_component(mod,isolate_name):
 class SortOrder(object):
     def __init__(self,arcs):
         self.arcs = arcs
-        iu.dbg('arcs')
     def __call__(self,x,y):
         x = x.args[0].relname
         y = y.args[0].relname
-        iu.dbg('x')
-        iu.dbg('y')
         res =  -1 if y in self.arcs[x] else 1 if x in self.arcs[y] else 0   
-        iu.dbg('res')
         return res
 
 # class SortOrder(object):
@@ -307,7 +303,6 @@ def get_mixin_order(iso,mod):
     for action in actions:
         mixins = mod.mixins[action]
         mixers = iu.topological_sort(list(set(m.mixer() for m in mixins)),arcs)
-        iu.dbg('mixers')
         keymap = dict((x,y) for y,x in enumerate(mixers))
         key = lambda m: keymap[m.mixer()]
         before = sorted([m for m in mixins if isinstance(m,ivy_ast.MixinBeforeDef)],key=key)

src/ivy/ivy_logic.py

@@ -205,6 +205,9 @@ lg.Apply.relname = property(lambda self: self.func)
 for cls in [lg.Apply] + lg_ops:
     cls.is_numeral = lambda self: False
 
+def is_numeral(term):
+    return isinstance(term,Symbol) and term.is_numeral()
+
 for cls in [lg.Const, lg.Var, lg.Apply]:
     cls.get_sort = lambda self: self.sort
 
@@ -720,25 +723,43 @@ def nary_str(op,args):
 
 infix_symbols = set(['<','<=','+','-','*','/'])
 
+to_str_ambiguous = False
+
+# This converts to string leaving variables and numerals without type decorations
+
+def fmla_to_str_ambiguous(term):
+    global to_str_ambiguous
+    to_str_ambiguous = True
+    res = str(term)
+    to_str_ambiguous = False
+    return res
+
 def app_arg_str(self,poly):
-    if not poly or not is_variable(self):
+    if to_str_ambiguous or not poly or (not is_variable(self) and not is_numeral(self)):
         return str(self)
     return self.name + ':' + str(self.sort)
 
 def app_str(self):
     name = self.func.name
     poly = name in polymorphic_symbols
+    if poly and any(not(is_variable(a) or is_numeral(a)) for a in self.args):
+        poly = false
     args = [app_arg_str(a,poly) for a in self.args]
     if name in infix_symbols:
         return (' ' + name + ' ').join(args)
     if len(args) == 0:
         return name
     return name + '(' + ','.join(args) + ')'
+
+def eq_args_str(self):
+    poly = not any(not(is_variable(a) or is_numeral(a)) for a in self.args)
+    return [app_arg_str(a,poly) for a in self.args]
+
     
-lg.Eq.__str__ = lambda self: '{} = {}'.format(self.t1, self.t2)
+lg.Eq.__str__ = lambda self: '{} = {}'.format(*eq_args_str(self))
 lg.And.__str__ = lambda self: nary_str('&',self.args) if self.args else 'true'
 lg.Or.__str__ = lambda self: nary_str('|',self.args) if self.args else 'false'
-lg.Not.__str__ = lambda self: ('{} ~= {}'.format(self.body.t1, self.body.t2)
+lg.Not.__str__ = lambda self: ('{} ~= {}'.format(*eq_args_str(self.body))
                                if type(self.body) is lg.Eq
                                else '~{}'.format(self.body))
 lg.Implies.__str__ = lambda self: '{} -> {}'.format(self.t1, self.t2)

src/ivy/ivy_solver.py

@@ -508,8 +508,8 @@ class HerbrandModel(object):
         self.constants = dict((sort_from_z3(s),model.get_universe(s))
                               for s in model.sorts())
         self.constants.update(mine_interpreted_constants(model,vocab))
-        print "model: %s" % model
-        print "univ: %s" % self.constants
+#        print "model: %s" % model
+#        print "univ: %s" % self.constants
 
     def sorts(self):
         return [s for s in self.constants]
@@ -696,8 +696,8 @@ def clause_model_simp(m,c):
         if not is_ground_lit(l):
             res.append(l)
             continue
-        if isinstance(l.atom,ivy_logic.And):
-            print "clause_model_simp: {}".format(c)
+#        if isinstance(l.atom,ivy_logic.And):
+#            print "clause_model_simp: {}".format(c)
         v = m.eval(literal_to_z3(l))
         if z3.is_true(v):
             return [l]
@@ -746,7 +746,7 @@ def relation_size_constraint(relation, size):
         ))
         for cs in consts
     ))
-    print "relation_size_constraint: {}".format(result)
+#    print "relation_size_constraint: {}".format(result)
     return result
 
 
@@ -878,7 +878,7 @@ def numeral_assign(clauses,h):
     used = set()
 #    print "starting: foom = {}".format(foom)
     for s in h.sorts():
-        print "na sort: {}".format(repr(s))
+#        print "na sort: {}".format(repr(s))
         if ivy_logic.is_interpreted_sort(s):
             print "interpreted"
             continue
@@ -925,7 +925,7 @@ def clauses_model_to_clauses(clauses1,ignore = None, implied = None,model = None
                  for s in h.sorts() for c in h.sort_universe(s))
     res = substitute_constants_clauses(res,m)
 #    print "core after rename: {} ".format(unsat_core(res,true_clauses()))
-    print "clauses_model_to_clauses res = {}".format(res)
+#    print "clauses_model_to_clauses res = {}".format(res)
     return res
 
 def clauses_model_to_diagram(clauses1,ignore = None, implied = None,model = None,axioms=None,weaken=True):
@@ -933,13 +933,13 @@ def clauses_model_to_diagram(clauses1,ignore = None, implied = None,model = None
     provided, returns true for symbols that should be ignored in the
     diagram.
     """
-    print "clauses_model_to_diagram clauses1 = {}".format(clauses1)
+#    print "clauses_model_to_diagram clauses1 = {}".format(clauses1)
     if axioms == None:
         axioms = true_clauses
     h = model_if_none(and_clauses(clauses1,axioms),implied,model)
     ignore = ignore if ignore != None else lambda x: False
     res = model_facts(h,(lambda x: False),clauses1,upclose=True) # why not pass axioms?
-    print "clauses_model_to_diagram res = {}".format(res)
+#    print "clauses_model_to_diagram res = {}".format(res)
     # find representative elements
     # find representatives of universe elements
     reps = dict()
@@ -953,33 +953,33 @@ def clauses_model_to_diagram(clauses1,ignore = None, implied = None,model = None
         for e in h.sort_universe(s):
             if e.rep not in reps:
                 reps[e.rep] = e.rep.skolem()()
-    print "clauses_model_to_diagram reps = {}".format(reps)
+#    print "clauses_model_to_diagram reps = {}".format(reps)
     # filter out clauses using universe elements without reps
 #    res = [cls for cls in res if all(c in reps for c in used_constants_clause(cls))]
     # replace universe elements with their reps
-    print "clauses_model_to_diagram res = {}".format(res)
+#    print "clauses_model_to_diagram res = {}".format(res)
     res = substitute_constants_clauses(res,reps)
     # filter defined skolems
     # this caused a bug in the leader example. the generated diagram did not satisfy clauses1
     res.fmlas = [f for f in res.fmlas if not any((x.is_skolem() and x in clauses1.defidx) for x in used_symbols_ast(f))]
-    print "clauses_model_to_diagram res = {}".format(res)
+#    print "clauses_model_to_diagram res = {}".format(res)
     uc = Clauses([[ivy_logic._eq_lit(ivy_logic.Variable('X',c.get_sort()),reps[c.rep])
                    for c in h.sort_universe(s)] for s in h.sorts()])
-    print "clauses_model_to_diagram uc = {}".format(uc)
+#    print "clauses_model_to_diagram uc = {}".format(uc)
 
     #    uc = true_clauses()
     if weaken:
         res = unsat_core(res,and_clauses(uc,axioms),clauses1) # implied not used here
-    print "clauses_model_to_diagram res = {}".format(res)
+#    print "clauses_model_to_diagram res = {}".format(res)
 
 #    print "foo = {}".format(unsat_core(and_clauses(uc,axioms),true_clauses(),clauses1))
 
     # filter out non-rep skolems
     repset = set(c.rep for e,c in reps.iteritems())
-    print "clauses_model_to_diagram repset = {}".format(repset)
+#    print "clauses_model_to_diagram repset = {}".format(repset)
     ign = lambda x,ignore=ignore: (ignore(x) and not x in repset)
     res = Clauses([cl for cl in res.fmlas if not any(ign(c) for c in used_symbols_ast(cl))])
-    print "clauses_model_to_diagram res = {}".format(res)
+#    print "clauses_model_to_diagram res = {}".format(res)
     return res
 
 def relation_model_to_clauses(h,r,n):

src/ivy/ivy_ui.py

@@ -60,6 +60,7 @@ class AnalysisGraphUI(object):
 
     def start(self):
         self.g.initialize(self.init_alpha())
+        self.rebuild()
 
     def init_alpha(self):
         if 'mode' in self.radios:
@@ -119,10 +120,10 @@ class AnalysisGraphUI(object):
 
     def view_state(self,n,clauses = None, reset=False):
         clauses = clauses or n.clauses
-        print "state: {}".format(clauses)
+#        print "state: {}".format(clauses)
         if hasattr(self,'current_concept_graph'):
            #  and self.current_concept_graph.winfo_exists():
-            print "current cg: {}".format(type(self.current_concept_graph))
+#            print "current cg: {}".format(type(self.current_concept_graph))
             self.current_concept_graph.set_parent_state(n,clauses,reset=reset)
             return
         sg = self.g.concept_graph(n,clauses)

src/ivy/ivy_ui_cti.py

@@ -36,20 +36,24 @@ class AnalysisGraphUI(ivy_ui.AnalysisGraphUI):
         return [("menu","File",
                  [
                   ("button","Remove tab",lambda self=self: self.ui_parent.remove(self)),
+                  ("button","Save invariant",self.save_conjectures),
                   ("button","Exit", lambda self=self: self.ui_parent.exit()),]),
-                ("menu","Action",
+                ("menu","Invariant",
                  [("button","Check induction",self.check_inductiveness),
                   ("button","Weaken",self.weaken),
                   ])]
 
     def start(self):
         ivy_ui.AnalysisGraphUI.start(self)
+        self.node(0).clauses = ilu.false_clauses() # just to make CG empty initially
         self.transitive_relations = []
         self.transitive_relation_concepts = []
         self.relations_to_minimize = Thing('relations to minimize')
         self.conjectures = im.module.conjs
         self.view_state(self.node(0))
-        self.autodetect_transitive()
+        with self.ui_parent.run_context():
+            self.autodetect_transitive()
+
         
 
 
@@ -96,81 +100,82 @@ class AnalysisGraphUI(ivy_ui.AnalysisGraphUI):
     def check_inductiveness(self, button=None):
         import ivy_transrel
         from ivy_solver import get_small_model
-        import tactics_api as ta
         from proof import ProofGoal
         from ivy_logic_utils import Clauses, and_clauses, dual_clauses
         from random import randrange
+        
+        with self.ui_parent.run_context():
 
-        ag = self.new_ag()
+            ag = self.new_ag()
 
-        pre = State()
-        pre.clauses = and_clauses(*self.conjectures)
+            pre = State()
+            pre.clauses = and_clauses(*self.conjectures)
 
-        action = im.module.actions['ext']
-        post = ag.execute(action, pre, None, 'ext')
-        post.clauses = ilu.true_clauses()
+            action = im.module.actions['ext']
+            post = ag.execute(action, pre, None, 'ext')
+            post.clauses = ilu.true_clauses()
 
-        to_test = list(self.conjectures)
-        while len(to_test) > 0:
-            # choose randomly, so the user can get another result by
-            # clicking again
-            conj = to_test.pop(randrange(len(to_test)))
-            assert conj.is_universal_first_order()
-            used_names = frozenset(x.name for x in il.sig.symbols.values())
-            def witness(v):
-                c = lg.Const('@' + v.name, v.sort)
-                assert c.name not in used_names
-                return c
-            clauses = dual_clauses(conj, witness)
-            history = ag.get_history(post)
+            to_test = list(self.conjectures)
+            while len(to_test) > 0:
+                # choose randomly, so the user can get another result by
+                # clicking again
+                conj = to_test.pop(randrange(len(to_test)))
+                assert conj.is_universal_first_order()
+                used_names = frozenset(x.name for x in il.sig.symbols.values())
+                def witness(v):
+                    c = lg.Const('@' + v.name, v.sort)
+                    assert c.name not in used_names
+                    return c
+                clauses = dual_clauses(conj, witness)
+                history = ag.get_history(post)
 
-            # TODO: this is still a bit hacky, and without nice error reporting
-            if self.relations_to_minimize.value == 'relations to minimize':
-                self.relations_to_minimize.value = ' '.join(sorted(
-                    k for k, v in il.sig.symbols.iteritems()
-                    if (type(v.sort) is lg.FunctionSort and
-                        v.sort.range == lg.Boolean and
-                        v.name not in self.transitive_relations and
-                        '.' not in v.name
-                    )
+                # TODO: this is still a bit hacky, and without nice error reporting
+                if self.relations_to_minimize.value == 'relations to minimize':
+                    self.relations_to_minimize.value = ' '.join(sorted(
+                        k for k, v in il.sig.symbols.iteritems()
+                        if (type(v.sort) is lg.FunctionSort and
+                            v.sort.range == lg.Boolean and
+                            v.name not in self.transitive_relations and
+                            '.' not in v.name
+                        )
+                    ))
+
+                res = ag.bmc(post, clauses, None, None, lambda clauses: get_small_model(
+                    clauses,
+                    sorted(il.sig.sorts.values()),
+                    [
+                        # TODO: this is still a bit hacky, and without nice error reporting
+                        history.maps[0].get(relation, relation)
+                        for x in self.relations_to_minimize.value.split()
+                        for relation in [il.sig.symbols[x]]
+                    ],
                 ))
+                if res is not None:
+                    self.current_conjecture = conj
+                    assert len(res.states) == 2
+                    rels = self.current_concept_graph.g.relations
+                    used = lu.used_constants(clauses.to_formula())
+    #                self.set_states(res.states[0], res.states[1])
+    #                self.cti = self.ui_parent.add(res)
+                    self.g = res
+                    self.rebuild()
+                    self.view_state(self.g.states[0], reset=True)
+                    for rel in rels:
+                        if any(c in used and not c.name.startswith('@')
+                               for c in lu.used_constants(rel.formula)):
+                            self.current_concept_graph.show_relation(rel,'+',update=False)
+                    self.current_concept_graph.update()
+                    #self.post_graph.selected = self.get_relevant_elements(self.post_state[2], clauses)
+                    self.ui_parent.text_dialog('The following conjecture is not relatively inductive:',
+                                               str(conj.to_formula()),on_cancel=None)
+                    return False
 
-            res = ag.bmc(post, clauses, None, None, lambda clauses: get_small_model(
-                clauses,
-                sorted(il.sig.sorts.values()),
-                [
-                    # TODO: this is still a bit hacky, and without nice error reporting
-                    history.maps[0].get(relation, relation)
-                    for x in self.relations_to_minimize.value.split()
-                    for relation in [il.sig.symbols[x]]
-                ],
-            ))
-            if res is not None:
-                self.current_conjecture = conj
-                assert len(res.states) == 2
-                rels = self.current_concept_graph.g.relations
-                used = lu.used_constants(clauses.to_formula())
-#                self.set_states(res.states[0], res.states[1])
-                self.cti = self.ui_parent.add(res)
-                for rel in rels:
-                    if any(c in used for c in lu.used_constants(rel.formula)):
-                        self.cti.current_concept_graph.show_relation(rel,'+',update=False)
-                self.cti.current_concept_graph.update()
-                #self.post_graph.selected = self.get_relevant_elements(self.post_state[2], clauses)
-                self.show_result('The following conjecture is not inductive:\n{}'.format(
-                    str(conj.to_formula()),
-                ))
-                return False
-
-#        self.set_states(False, False)
-        self.ui_parent.text_dialog('Inductive invariant found:',
-                                   '\n'.join(str(conj) for conj in self.conjectures))
-        return True
-
-
+    #        self.set_states(False, False)
+            self.ui_parent.text_dialog('Inductive invariant found:',
+                                       '\n'.join(str(conj) for conj in self.conjectures))
+            return True
 
     def set_states(self,s0,s1):
-        iu.dbg('s0.universe')
         self.cg = self.view_state(s0, reset=True)
         
     def show_result(self,res):
@@ -184,20 +189,55 @@ class AnalysisGraphUI(ivy_ui.AnalysisGraphUI):
             cmd = lambda sel: self.weaken([udc[idx] for idx in sel])
             self.ui_parent.listbox_dialog(msg,udc_text,command=cmd,multiple=True)
         else:
-            iu.dbg('conjs')
             for conj in conjs:
                 self.conjectures.remove(conj)
             self.ui_parent.text_dialog('Removed the following conjectures:',
                                        '\n'.join(str(conj) for conj in conjs))
 
-    pass
+    def save_conjectures(self):
+        f = self.ui_parent.saveas_dialog('Save invariant as...',[('ivy files', '.ivy')])
+        if f:
+
+            old_conjs_set = set(str(c) for c in im.module.conjs)
+            new_conjs_set = set(str(c) for c in self.conjectures)
+
+            old_kept = [lc for lc in im.module.labeled_conjs if str(lc.formula) in new_conjs_set]
+            old_dropped = [lc for lc in im.module.labeled_conjs if str(lc.formula) not in new_conjs_set]
+            new = [conj for conj in self.conjectures if str(conj) not in old_conjs_set]
+
+            f.write('# This file was generated by ivy.\n\n')
+
+            if old_kept:
+                f.write('\n# original conjectures kept\n\n')
+                for lc in old_kept:
+                    _write_conj(f,lc.label,lc.formula)
+
+            if old_dropped:
+                f.write('\n# original conjectures dropped\n\n')
+                for lc in old_dropped:
+                    f.write('# ')
+                    _write_conj(f,lc.label,lc.formula)
+                    
+            if new:
+                f.write('\n# new conjectures\n\n')
+                for conj in new:
+                    _write_conj(f,None,conj)
+
+            f.close()
+
+def _write_conj(f,lab,fmla):
+    fmla = il.drop_universals(fmla)
+    if lab:
+        f.write("conjecture [{}] {}\n".format(lab,str(fmla)))
+    else:
+        f.write("conjecture {}\n".format(str(fmla)))
 
 class ConceptGraphUI(ivy_graph_ui.GraphWidget):
     def menus(self):
-        return [("menu","Action",
+        return [("menu","Conjecture",
                  [("button","Undo",self.undo),
                   ("button","Redo",self.redo),
-                  ("button","Gather",self.gather),
+                  ("button","Gather",self.gather_facts),
                   ("button","Bounded check",self.bmc_conjecture),
                   ("button","Minimize",self.minimize_conjecture),
                   ("button","Check sufficient",self.is_sufficient),
@@ -210,6 +250,18 @@ class ConceptGraphUI(ivy_graph_ui.GraphWidget):
                   ])]
 
 
+    def get_node_actions(self,node,click='left'):
+        if click == 'left':
+            return [("<>",self.select_node)]
+        else:
+            return [] # nothing on right click
+
+    def get_edge_actions(self,node,click='left'):
+        if click == 'left':
+            return [("<>",self.select_edge)]
+        else:
+            return [] # nothing on right click
+
     def get_selected_conjecture(self):
         """
         Return a positive universal conjecture based on the selected facts.
@@ -281,59 +333,62 @@ class ConceptGraphUI(ivy_graph_ui.GraphWidget):
                                         command = c, minval=0, initval=iv)
             return
 
-        step_action = im.module.actions['ext']
-        
-        n_steps = bound
-        self.current_bound = bound
 
-        if conjecture is None:
-            conj = self.get_selected_conjecture()
-        else:
-            conj = conjecture
+        with self.ui_parent.run_context():
 
-        assert conj.is_universal_first_order()
-        used_names = frozenset(x.name for x in il.sig.symbols.values())
-        def witness(v):
-            c = lg.Const('@' + v.name, v.sort)
-            assert c.name not in used_names
-            return c
-        clauses = dual_clauses(conj, witness)
+            step_action = im.module.actions['ext']
 
-        ag = self.parent.new_ag()
-        with ag.context as ac:
-            post = ac.new_state(ag.init_cond)
-        if 'initialize' in im.module.actions:
-            init_action = im.module.actions['initialize']
-            post = ag.execute(init_action, None, None, 'initialize')
+            n_steps = bound
+            self.current_bound = bound
 
-        for n in range(n_steps + 1):
-            res = ag.bmc(post, clauses)
-            if verbose:
-                if res is None:
-                    msg = 'BMC with bound {} did not find a counter-example to:\n{}'.format(
-                        n,
-                        str(conj.to_formula()),
-                    )
-                else:
-                    msg = 'BMC with bound {} found a counter-example to:\n{}'.format(
-                        n,
-                        str(conj.to_formula()),
-                    )
-                print '\n' + msg + '\n'
-            if res is not None:
-#                ta.step()
-                self.ui_parent.text_dialog('BMC with bound {} found a counter-example to:'.format(n),
-                                           str(conj.to_formula()),
-                                           command = lambda: self.ui_parent.add(res),
-                                           command_label = 'View')
-                return True
-            post = ag.execute(step_action, None, None, 'ext')
+            if conjecture is None:
+                conj = self.get_selected_conjecture()
+            else:
+                conj = conjecture
 
-        self.ui_parent.text_dialog('BMC with bound {} did not find a counter-example to:'.format(n_steps),
-                                   str(conj.to_formula()),
-                                   on_cancel = None)
-                                   
-        return False
+            assert conj.is_universal_first_order()
+            used_names = frozenset(x.name for x in il.sig.symbols.values())
+            def witness(v):
+                c = lg.Const('@' + v.name, v.sort)
+                assert c.name not in used_names
+                return c
+            clauses = dual_clauses(conj, witness)
+
+            ag = self.parent.new_ag()
+            with ag.context as ac:
+                post = ac.new_state(ag.init_cond)
+            if 'initialize' in im.module.actions:
+                init_action = im.module.actions['initialize']
+                post = ag.execute(init_action, None, None, 'initialize')
+
+            for n in range(n_steps + 1):
+                res = ag.bmc(post, clauses)
+                if verbose:
+                    if res is None:
+                        msg = 'BMC with bound {} did not find a counter-example to:\n{}'.format(
+                            n,
+                            str(conj.to_formula()),
+                        )
+                    else:
+                        msg = 'BMC with bound {} found a counter-example to:\n{}'.format(
+                            n,
+                            str(conj.to_formula()),
+                        )
+                    print '\n' + msg + '\n'
+                if res is not None:
+    #                ta.step()
+                    self.ui_parent.text_dialog('BMC with bound {} found a counter-example to:'.format(n),
+                                               str(conj.to_formula()),
+                                               command = lambda: self.ui_parent.add(res),
+                                               command_label = 'View')
+                    return True
+                post = ag.execute(step_action, None, None, 'ext')
+
+#            self.ui_parent.text_dialog('BMC with bound {} did not find a counter-example to:'.format(n_steps),
+#                                       str(conj.to_formula()),
+#                                       on_cancel = None)
+
+            return False
 
     def minimize_conjecture(self, button=None, bound=None):
         import ivy_transrel
@@ -347,39 +402,43 @@ class ConceptGraphUI(ivy_graph_ui.GraphWidget):
             # found a BMC counter-example
             return
 
-        step_action = im.module.actions['ext']
+        with self.ui_parent.run_context():
+            step_action = im.module.actions['ext']
 
-        n_steps = self.current_bound
+            n_steps = self.current_bound
 
-        ag = self.parent.new_ag()
-        with ag.context as ac:
-            post = ac.new_state(ag.init_cond)
-        if 'initialize' in im.module.actions:
-            init_action = im.module.actions['initialize']
-            post = ag.execute(init_action, None, None, 'initialize')
-        for n in range(n_steps):
-            post = ag.execute(step_action, None, None, 'ext')
-        axioms = im.module.background_theory()
-        post_clauses = and_clauses(post.clauses, axioms)
+            ag = self.parent.new_ag()
+            with ag.context as ac:
+                post = ac.new_state(ag.init_cond)
+            if 'initialize' in im.module.actions:
+                init_action = im.module.actions['initialize']
+                post = ag.execute(init_action, None, None, 'initialize')
+            for n in range(n_steps):
+                post = ag.execute(step_action, None, None, 'ext')
+            axioms = im.module.background_theory()
+            post_clauses = and_clauses(post.clauses, axioms)
 
-        used_names = (
-            frozenset(x.name for x in il.sig.symbols.values()) |
-            frozenset(x.name for x in used_symbols_clauses(post_clauses))
-        )
-        facts = self.get_active_facts()
-        assert not any(
-            c.is_skolem() and c.name in used_names for c in lu.used_constants(*facts)
-        )
-        core = unsat_core(Clauses(facts), post_clauses)
-        assert core is not None, "bmc_conjecture returned False but unsat core is None"
-        core_formulas = frozenset(core.fmlas)
-        self.set_facts([fact for fact in facts if fact in core_formulas])
-        self.highlight_selected_facts()
-        self.ui_parent.text_dialog("BMC found the following possible conjecture:",
-                                   str(self.get_selected_conjecture()))
+            used_names = (
+                frozenset(x.name for x in il.sig.symbols.values()) |
+                frozenset(x.name for x in used_symbols_clauses(post_clauses))
+            )
+            facts = self.get_active_facts()
+            assert not any(
+                c.is_skolem() and c.name in used_names for c in lu.used_constants(*facts)
+            )
+            core = unsat_core(Clauses(facts), post_clauses)
+            if core is None:
+                core = Clauses([]) ## can happen if we are proving true
+#            assert core is not None, "bmc_conjecture returned False but unsat core is None"
+            core_formulas = frozenset(core.fmlas)
+            self.set_facts([fact for fact in facts if fact in core_formulas])
+            self.highlight_selected_facts()
+            self.ui_parent.text_dialog("BMC found the following possible conjecture:",
+                                       str(self.get_selected_conjecture()))
 
-    def highlight_selected_facts(self):
-            pass # TODO
+
+#    def highlight_selected_facts(self):
+#            pass # TODO
 
     def is_sufficient(self, button=None):
         """
@@ -391,40 +450,41 @@ class ConceptGraphUI(ivy_graph_ui.GraphWidget):
         """
         import ivy_transrel
         import ivy_solver
-        import tactics_api as ta
         from proof import ProofGoal
         from ivy_logic_utils import Clauses, and_clauses, dual_clauses
         from random import randrange
 
-        conj = self.get_selected_conjecture()
-        target_conj = self.parent.current_conjecture
+        with self.ui_parent.run_context():
 
-        ag = self.parent.new_ag()
+            conj = self.get_selected_conjecture()
+            target_conj = self.parent.current_conjecture
 
-        pre = State()
-        pre.clauses = and_clauses(conj, *self.parent.conjectures)
+            ag = self.parent.new_ag()
 
-        action = im.module.actions['ext']
-        post = ag.execute(action, pre, None, 'ext')
-        post.clauses = ilu.true_clauses()
+            pre = State()
+            pre.clauses = and_clauses(conj, *self.parent.conjectures)
 
-        assert target_conj.is_universal_first_order()
-        used_names = frozenset(x.name for x in il.sig.symbols.values())
-        def witness(v):
-            c = lg.Const('@' + v.name, v.sort)
-            assert c.name not in used_names
-            return c
-        clauses = dual_clauses(target_conj, witness)
-        res = ag.bmc(post, clauses)
+            action = im.module.actions['ext']
+            post = ag.execute(action, pre, None, 'ext')
+            post.clauses = ilu.true_clauses()
 
-        text = '(1) ' + str(conj.to_formula()) + '\n(2) ' + str(target_conj.to_formula())
-        if res is not None:
-            self.ui_parent.text_dialog('(1) does not imply (2) at the next time. View counterexample?',
-                                       text,command_label='View',command = lambda: self.ui_parent.add(res))
-            return False
-        else:
-            self.ui_parent.text_dialog('(1) implies (2) at the next time:',text,on_cancel=None)
-            return True
+            assert target_conj.is_universal_first_order()
+            used_names = frozenset(x.name for x in il.sig.symbols.values())
+            def witness(v):
+                c = lg.Const('@' + v.name, v.sort)
+                assert c.name not in used_names
+                return c
+            clauses = dual_clauses(target_conj, witness)
+            res = ag.bmc(post, clauses)
+
+            text = '(1) ' + str(conj.to_formula()) + '\n(2) ' + str(target_conj.to_formula())
+            if res is not None:
+                self.ui_parent.text_dialog('(1) does not imply (2) at the next time. View counterexample?',
+                                           text,command_label='View',command = lambda: self.ui_parent.add(res))
+                return False
+            else:
+                self.ui_parent.text_dialog('(1) implies (2) at the next time:',text,on_cancel=None)
+                return True
 
 
     def is_inductive(self, button=None):
@@ -436,38 +496,150 @@ class ConceptGraphUI(ivy_graph_ui.GraphWidget):
         """
         import ivy_transrel
         import ivy_solver
-        import tactics_api as ta
         from proof import ProofGoal
         from ivy_logic_utils import Clauses, and_clauses, dual_clauses
         from random import randrange
 
-        conj = self.get_selected_conjecture()
-        target_conj = conj
+        with self.ui_parent.run_context():
+            conj = self.get_selected_conjecture()
+            target_conj = conj
 
-        ag = self.parent.new_ag()
+            ag = self.parent.new_ag()
 
-        pre = State()
-        pre.clauses = and_clauses(conj, *self.parent.conjectures)
+            pre = State()
+            pre.clauses = and_clauses(conj, *self.parent.conjectures)
 
-        action = im.module.actions['ext']
-        post = ag.execute(action, pre, None, 'ext')
-        post.clauses = ilu.true_clauses()
+            action = im.module.actions['ext']
+            post = ag.execute(action, pre, None, 'ext')
+            post.clauses = ilu.true_clauses()
 
-        assert target_conj.is_universal_first_order()
-        used_names = frozenset(x.name for x in il.sig.symbols.values())
-        def witness(v):
-            c = lg.Const('@' + v.name, v.sort)
-            assert c.name not in used_names
-            return c
-        clauses = dual_clauses(target_conj, witness)
-        res = ag.bmc(post, clauses)
+            assert target_conj.is_universal_first_order()
+            used_names = frozenset(x.name for x in il.sig.symbols.values())
+            def witness(v):
+                c = lg.Const('@' + v.name, v.sort)
+                assert c.name not in used_names
+                return c
+            clauses = dual_clauses(target_conj, witness)
+            res = ag.bmc(post, clauses)
 
-        text = '(1) ' + str(conj.to_formula()) 
-        if res is not None:
-            self.ui_parent.text_dialog('(1) is not relatively inductive. View counterexample?',
-                                       text,command_label='View',command = lambda: self.ui_parent.add(res))
-            return False
-        else:
-            self.ui_parent.text_dialog('(1) is relatively inductive:',text,on_cancel=None)
-            return True
+            text = '(1) ' + str(conj.to_formula()) 
+            if res is not None:
+                self.ui_parent.text_dialog('(1) is not relatively inductive. View counterexample?',
+                                           text,command_label='View',command = lambda: self.ui_parent.add(res))
+                return False
+            else:
+                self.ui_parent.text_dialog('(1) is relatively inductive:',text,on_cancel=None)
+                return True
+
+    # TODO: this is not used yet
+
+    def unused_highlight_selected_facts(self):
+        """
+        Add custom node labels and edges to reflect the selected
+        conjecture in pre_graph
+        """
+        # first collect all atoms that appear in the facts
+        atoms = []
+        def collect_atoms(x):
+            if type(x) in (lg.Apply, lg.Eq):
+                atoms.append(x)
+            else:
+                for y in x:
+                    collect_atoms(y)
+        collect_atoms(self.get_active_facts())
+
+        # now collect relevant edges and node labels elements
+        self.g.concept_session.widget = None
+        self.g.concept_session.domain.concepts['edges'] = []
+        self.g.concept_session.domain.concepts['node_labels'] = []
+        nodes = frozenset(self.g.concept_session.domain.concepts['nodes'])
+        for atom in atoms:
+            if type(atom) is lg.Eq:
+                assert type(atom.t2) is lg.Const
+                if type(atom.t1) is lg.Const:
+                    n1 = atom.t1.name
+                    n2 = atom.t2.name
+                    if n1 in nodes and n2 in nodes:
+                        self.g.concept_session.add_custom_edge('=', n1, n2)
+                    elif n1 in nodes:
+                        label_name = '={}'.format(n2)
+                        assert label_name in self.g.concept_session.domain.concepts, atom
+                        self.g.concept_session.add_custom_node_label(n1, label_name)
+                    else:
+                        # TODO
+                        # assert False, atom
+                        pass
+                else:
+                    assert type(atom.t1) is lg.Apply
+                    if atom.t1.func.sort.arity == 1:
+                        assert type(atom.t1.terms[0]) is lg.Const
+                        self.g.concept_session.add_custom_edge(
+                            atom.t1.func.name,
+                            atom.t1.terms[0].name,
+                            atom.t2.name,
+                        )
+                    else:
+                        # TODO: support higher arity
+                        pass
+            elif type(atom) is lg.Apply:
+                if atom.func.sort.arity == 1:
+                    self.g.concept_session.add_custom_node_label(atom.terms[0].name, atom.func.name)
+                elif atom.func.sort.arity == 2:
+                    self.g.concept_session.add_custom_edge(*(c.name for c in atom))
+                else:
+                    # TODO: support higher arity
+                    pass
+            else:
+                assert False, lit
+        self.g.recompute()
+#        self.g.pre_graph.selected = tuple(set(chain(*(elements for fact, elements in self.g.facts_list.value))))
+
+
+    def gather_facts(self, button=None):
+        """
+        Gather only based on selected nodes, taking all visible edges.
+        """
+        g = self.g
+        facts = [] # list of pairs (formula, graph_elements)
+        selected_nodes = sorted(self.node_selection)
+        # if nothing is selected, use all nodes
+        if not selected_nodes:
+            selected_nodes = [n.name for n in g.nodes]
+        for node in selected_nodes:
+            elements = ((node,),)
+            facts += [(formula, elements) for formula in g.concept_session.get_node_facts(node)]
+        selected_nodes = frozenset(selected_nodes)
+        edges = set(
+            tag[-3:]
+            for tag, value in g.concept_session.abstract_value
+            if tag[0] == 'edge_info' and
+            tag[-2] in selected_nodes and
+            tag[-1] in selected_nodes
+        )
+        for edge, source, target in sorted(edges):
+            elements = ((source,), (target,), (edge,source,target))
+            if (g.edge_display_checkboxes[edge]['all_to_all'].value):
+                if g.edge_display_checkboxes[edge]['transitive'].value and source==target:
+                    continue # don't use reflective edges for orders
+                facts += [(formula, elements) for formula in
+                          g.concept_session.get_edge_facts(edge, source, target, True)]
+            if g.edge_display_checkboxes[edge]['none_to_none'].value or edge == '=':
+                # get dis-equalities, don't get other negative
+                # transitive facts unless checkboxed
+                facts += [(formula, elements) for formula in
+                          g.concept_session.get_edge_facts(edge, source, target, False)]
+        # filter double equalities and self-edges of reflexive relations
+        facts = [(f, elements) for f, elements in facts if not (
+            #(type(f) is Eq and f.t1 >= f.t2) or
+            (type(f) is lg.Not and type(f.body) is lg.Eq and f.body.t1 >= f.body.t2) #or
+            # (
+            #     type(f) is Apply and
+            #     g.edge_display_checkboxes[f.func.name]['transitive'].value and
+            #     f.terms[0] == f.terms[1]
+            # )
+        )]
+        g.set_facts([x for x,y in facts])
+        self.fact_elems = dict(facts)
+        self.update()
+        self.highlight_selected_facts()
 

src/ivy/ivy_ui_util.py

@@ -124,7 +124,7 @@ def listbox_dialog(tk,root,msg,items,command=lambda:None,on_cancel=lambda:None,m
     S = Scrollbar(dlg)
     T = Listbox(dlg, height=8, width=50, selectmode=SINGLE)
     S.pack(side=RIGHT, fill=Y)
-    T.pack(side=LEFT, fill=Y)
+    T.pack(side=LEFT, fill=BOTH,expand=1)
     S.config(command=T.yview)
     T.config(yscrollcommand=S.set)
     for item in items:

src/tkui/tk_cy.py

@@ -100,6 +100,7 @@ class TkCyCanvas(Canvas):
     def create_elements(self,cy_elements):
 #        print 'cy_elements" {}'.format(cy_elements.elements)
         self.elem_ids = {}
+        self.edge_points = {}
         for idx,elem in enumerate(cy_elements.elements):
             eid = get_id(elem)
             group = get_group(elem)
@@ -115,6 +116,7 @@ class TkCyCanvas(Canvas):
             elif group == 'edges':
                 coords = get_bspline(elem)
                 styles = self.get_edge_styles(elem)
+                self.edge_points[eid] = coords
                 line = self.create_line(*coords,tags=eid,smooth="bezier",**styles)
                 arrow = self.create_line(*get_arrowend(elem),tags=eid,arrow=LAST,**styles)
                 lp = get_label_pos(elem)
@@ -162,3 +164,14 @@ class TkCyCanvas(Canvas):
         # display the popup menu 
         edge = self.edge_from_cy_elem(elem)
         self.make_popup(event,self.get_edge_actions(edge,click=click),edge)
+
+    def highlight_edge(self,eid,val=True):
+        tag = eid + 'h'
+        for item in self.find_withtag(tag):
+            self.delete(item)
+        if val:
+            item = self.create_line(*self.edge_points[eid],tags=tag,
+                                     smooth="bezier",width=6,capstyle=ROUND,fill='grey')
+            self.tag_lower(item)
+
+            

src/tkui/tk_graph_ui.py

@@ -40,6 +40,8 @@ class TkGraphWidget(TkCyCanvas,uu.WithMenuBar):
         self.update_callback = None
         self.ui_parent = ui_parent
         self.elem_ids = {}
+        self.node_selection = set()
+        self.edge_selection = set()
         self.rebuild()
 
     # This is in case the widget is detroyed by the user. We could
@@ -142,6 +144,9 @@ class TkGraphWidget(TkCyCanvas,uu.WithMenuBar):
             if hasattr(self,'mark'):
                 del self.mark
 
+            # clear the selection (TODO: keep it and redraw it)
+            self.clear_elem_selection()
+
             self.create_elements(g.cy_elements)
 
             # show the constraint if there is one
@@ -205,6 +210,33 @@ class TkGraphWidget(TkCyCanvas,uu.WithMenuBar):
                 if 'shape' in self.gettags(item):
                     self.itemconfig(item,fill=('red' if on else ''))
 
+    def select_node(self,node,val=None):
+        cid = self.g.id_from_concept(node)
+        tag = self.elem_ids[cid]
+        ns = self.node_selection
+        newval = val if val is not None else cid not in ns
+        ns.discard(cid)
+        if newval:
+            ns.add(cid)
+        for item in self.find_withtag(tag):
+            if 'shape' in self.gettags(item):
+                self.itemconfig(item,fill=('grey' if newval else ''))
+
+    def select_edge(self,edge,val=None):
+        cid = tuple(self.g.id_from_concept(c) for c in edge)
+
+        es = self.edge_selection
+        newval = val if val is not None else cid not in es
+        es.discard(cid)
+        if newval:
+            es.add(cid)
+#        for item in self.find_withtag(tag):
+#            self.itemconfig(item,fill=('grey' if newval else 'black'))
+        try:
+            tag = self.g.edge_cy_id(edge)
+            self.highlight_edge(tag,newval)
+        except KeyError:
+            pass
 
     # Export the display in DOT format. This also depends on tcldot.