Module Expr Str ImportFrom alias ImportFrom alias FunctionDef arguments args NameParam NameParam NameParam defaults NameLoad body Expr Str If Call NameLoad NameLoad Call NameLoad body Return ListComp TupleLoad NameLoad NameLoad comprehension TupleStore NameStore NameStore Call AttributeLoad NameLoad attr If CompareIs NameLoad NameLoad body Assign NameStore Call NameLoad Assign NameStore Call AttributeLoad NameLoad attr Assign NameStore ListLoad For TupleStore NameStore NameStore NameLoad body If CompareIn NameLoad NameLoad body Assign NameStore SubscriptLoad NameLoad Index NameLoad orelse Assign NameStore Call NameLoad NameLoad NameLoad Expr Call AttributeLoad NameLoad attr TupleLoad NameLoad NameLoad Return NameLoad decorator_list If CompareEq NameLoad Str body ImportFrom alias ImportFrom alias alias alias alias alias alias alias alias alias alias ImportFrom alias alias alias alias ImportFrom alias alias alias ImportFrom alias alias alias FunctionDef arguments args NameParam defaults body Print NameLoad Str Call NameLoad NameLoad decorator_list Assign NameStore Call NameLoad Str Assign NameStore Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad NameLoad NameLoad NameLoad Assign TupleStore NameStore NameStore NameStore GeneratorExp Call NameLoad NameLoad NameLoad comprehension NameStore ListLoad Str Str Str Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad Str NameLoad Assign NameStore Call NameLoad ListLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad Call NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad Call NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad Call NameLoad Call NameLoad ListLoad NameLoad Call NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad Call NameLoad ListLoad NameLoad Call NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad Call NameLoad ListLoad NameLoad NameLoad Call NameLoad Call NameLoad Call NameLoad NameLoad Call NameLoad NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad ListLoad NameLoad NameLoad NameLoad Call NameLoad ListLoad NameLoad NameLoad Call NameLoad Call NameLoad Call NameLoad NameLoad Call NameLoad NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad Call NameLoad ListLoad TupleLoad Str NameLoad TupleLoad Str NameLoad TupleLoad Str NameLoad TupleLoad Str NameLoad TupleLoad Str NameLoad TupleLoad Str NameLoad Call NameLoad ListLoad TupleLoad Str NameLoad TupleLoad Str NameLoad TupleLoad Str NameLoad TupleLoad Str NameLoad Call NameLoad ListLoad TupleLoad Str TupleLoad ListLoad Str Str Str ListLoad Str Str Str Str TupleLoad Str TupleLoad ListLoad Str ListLoad Str Str Str Str ListLoad Str Str Str Str ListLoad Str Str Assign NameStore Call AttributeLoad NameLoad attr Print Str For TupleStore NameStore NameStore NameLoad body Print Str NameLoad NameLoad Str Print Str Assign NameStore Call NameLoad Call NameLoad ListLoad NameLoad NameLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad ListLoad NameLoad Call NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad Call NameLoad NameLoad NameLoad Call NameLoad NameLoad NameLoad Assign NameStore Call NameLoad NameLoad NameLoad Print Str For TupleStore NameStore NameStore NameLoad body Print Str NameLoad NameLoad Str Print Str
N/A N/A z3_utils z3_implies logic Or alpha N/A N/A concept_domain state cache N/A None N/A N/A 
    Right now, state is just a plain formula

    This is a *very* unoptimized implementation
     N/A N/A z3_implies state N/A Or N/A N/A N/A N/A tag True N/A N/A tag formula N/A N/A concept_domain get_facts N/A N/A cache None N/A N/A cache N/A dict N/A facts N/A N/A concept_domain get_facts N/A result N/A N/A N/A tag formula facts N/A N/A N/A tag cache N/A N/A value N/A cache N/A tag N/A N/A value N/A z3_implies state formula N/A N/A N/A result append N/A tag value N/A result N/A N/A N/A __name__ __main__ N/A collections OrderedDict logic Var Const Apply Eq Not And Or Implies ForAll Exists logic UninterpretedSort FunctionSort first_order_sort Boolean logic_util free_variables substitute substitute_apply concept Concept ConceptCombiner ConceptDomain test N/A N/A st N/A N/A N/A st = N/A eval st N/A N/A S N/A UninterpretedSort S N/A UnaryRelation N/A FunctionSort S Boolean N/A BinaryRelation N/A FunctionSort S S Boolean N/A N/A X Y Z N/A N/A Var n S N/A n N/A X Y Z N/A U N/A Var U UnaryRelation N/A U1 N/A Var U1 UnaryRelation N/A U2 N/A Var U2 UnaryRelation N/A B N/A Var B BinaryRelation N/A B1 N/A Var B1 BinaryRelation N/A B2 N/A Var B2 BinaryRelation N/A nstar N/A Const nstar BinaryRelation N/A x N/A Const x S N/A y N/A Const y S N/A c11 N/A Concept N/A X N/A And N/A Eq x X N/A Eq y X N/A c10 N/A Concept N/A X N/A And N/A Eq x X N/A Not N/A Eq y X N/A c01 N/A Concept N/A X N/A And N/A Not N/A Eq x X N/A Eq y X N/A c00 N/A Concept N/A X N/A And N/A Not N/A Eq x X N/A Not N/A Eq y X N/A cnstar N/A Concept N/A X Y N/A nstar X Y N/A cnplus N/A Concept N/A X Y N/A And N/A nstar X Y N/A Not N/A Eq X Y N/A notexists N/A ConceptCombiner N/A U N/A Not N/A Exists N/A X N/A U X N/A exists N/A ConceptCombiner N/A U N/A Exists N/A X N/A U X N/A singleton N/A ConceptCombiner N/A U N/A ForAll N/A X Y N/A Implies N/A And N/A U X N/A U Y N/A Eq X Y N/A all_to_all N/A ConceptCombiner N/A U1 U2 B N/A ForAll N/A X Y N/A Implies N/A And N/A U1 X N/A U2 Y N/A B X Y N/A cd N/A ConceptDomain N/A OrderedDict N/A N/A xy c11 N/A other c00 N/A x c10 N/A y c01 N/A nstar cnstar N/A nplus cnplus N/A OrderedDict N/A N/A notexists notexists N/A exists exists N/A singleton singleton N/A all_to_all all_to_all N/A OrderedDict N/A N/A node_info N/A N/A notexists exists singleton N/A xy other x y N/A binary_info N/A N/A all_to_all N/A xy other x y N/A xy other x y N/A nstar nplus N/A facts N/A N/A cd get_facts N/A facts = [ N/A N/A tag formula facts N/A N/A tag formula , N/A ]
 N/A state N/A And N/A ForAll N/A X Y Z N/A And N/A nstar X X N/A Implies N/A And N/A nstar X Y N/A nstar Y X N/A Eq X Y N/A Implies N/A And N/A nstar X Y N/A nstar Y Z N/A nstar X Z N/A Implies N/A And N/A nstar X Y N/A nstar X Z N/A Or N/A nstar Y Z N/A nstar Z Y N/A nstar x y N/A Not N/A Eq x y N/A ForAll N/A Z N/A Implies N/A And N/A nstar x Z N/A Not N/A Eq x Z N/A nstar y Z N/A abstract_value N/A alpha cd state N/A abstract_value = [ N/A N/A tag value abstract_value N/A N/A tag value , N/A ]
