def refinements(hla, state, library):  # TODO - refinements may be (multiple) HLA themselves ...
     """
     state is a Problem, containing the current state kb
     library is a dictionary containing details for every possible refinement. eg:
     {
     'HLA': ['Go(Home,SFO)', 'Go(Home,SFO)', 'Drive(Home, SFOLongTermParking)', 'Shuttle(SFOLongTermParking, SFO)', 'Taxi(Home, SFO)'],
     'steps': [['Drive(Home, SFOLongTermParking)', 'Shuttle(SFOLongTermParking, SFO)'], ['Taxi(Home, SFO)'], [], [], []],
     # empty refinements ie primitive action
     'precond': [['At(Home), Have(Car)'], ['At(Home)'], ['At(Home)', 'Have(Car)'], ['At(SFOLongTermParking)'], ['At(Home)']],
     'effect': [['At(SFO)'], ['At(SFO)'], ['At(SFOLongTermParking)'], ['At(SFO)'], ['At(SFO)'], ['~At(Home)'], ['~At(Home)'], ['~At(Home)'], ['~At(SFOLongTermParking)'], ['~At(Home)']]
     }
     """
     e = Expr(hla.name, hla.args)
     indices = [i for i, x in enumerate(library['HLA']) if expr(x).op == hla.name]
     for i in indices:
         # TODO multiple refinements
         precond = []
         for p in library['precond'][i]:
             if p[0] == '~':
                 precond.append(expr('Not' + p[1:]))
             else:
                 precond.append(expr(p))
         effect = []
         for e in library['effect'][i]:
             if e[0] == '~':
                 effect.append(expr('Not' + e[1:]))
             else:
                 effect.append(expr(e))
         action = HLA(library['steps'][i][0], precond, effect)
         if action.check_precond(state.init, action.args):
             yield action

    def __init__(self, goals, initial_clauses=None):
        if initial_clauses is None:
            initial_clauses = []

        initial_clauses = [expr(c) if not isinstance(c, Expr) else c for c in initial_clauses]
        self.clause_set = frozenset(initial_clauses)

        goals = [expr(g) if not isinstance(g, Expr) else g for g in goals]
        self.goal_clauses = frozenset(goals)

def test_extend_example():
    assert list(test_network.extend_example({x: A, y: B}, expr('Conn(x, z)'))) == [
        {x: A, y: B, z: B}, {x: A, y: B, z: D}]
    assert list(test_network.extend_example({x: G}, expr('Conn(x, y)'))) == [{x: G, y: I}]
    assert list(test_network.extend_example({x: C}, expr('Conn(x, y)'))) == []
    assert len(list(test_network.extend_example({}, expr('Conn(x, y)')))) == 10
    assert len(list(small_family.extend_example({x: expr('Andrew')}, expr('Father(x, y)')))) == 2
    assert len(list(small_family.extend_example({x: expr('Andrew')}, expr('Mother(x, y)')))) == 0
    assert len(list(small_family.extend_example({x: expr('Andrew')}, expr('Female(y)')))) == 6

def test_have_cake_and_eat_cake_too():
    p = have_cake_and_eat_cake_too()
    assert p.goal_test() is False
    solution = [expr("Eat(Cake)"),
                expr("Bake(Cake)")]

    for action in solution:
        p.act(action)

    assert p.goal_test()

def test_spare_tire():
    p = spare_tire()
    assert p.goal_test() is False
    solution = [expr("Remove(Flat, Axle)"),
                expr("Remove(Spare, Trunk)"),
                expr("PutOn(Spare, Axle)")]

    for action in solution:
        p.act(action)

    assert p.goal_test()

def test_three_block_tower():
    p = three_block_tower()
    assert p.goal_test() is False
    solution = [expr("MoveToTable(C, A)"),
                expr("Move(B, Table, C)"),
                expr("Move(A, Table, B)")]

    for action in solution:
        p.act(action)

    assert p.goal_test()

def to_cnf(s):
    """Convert a propositional logical sentence to conjunctive normal form.
    That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 253]
    >>> to_cnf('~(B | C)')
    (~B & ~C)
    """
    s = expr(s)
    if isinstance(s, str):
        s = expr(s)
    s = eliminate_implications(s)  # Steps 1, 2 from p. 253
    s = move_not_inwards(s)  # Step 3
    return distribute_and_over_or(s)  # Step 4

def test_double_tennis():
    p = double_tennis_problem()
    assert p.goal_test() is False

    solution = [expr("Go(A, RightBaseLine, LeftBaseLine)"),
                expr("Hit(A, Ball, RightBaseLine)"),
                expr("Go(A, LeftNet, RightBaseLine)")]

    for action in solution:
        p.act(action)

    assert p.goal_test()

def test_new_clause():
    target = expr('Open(x, y)')
    examples_pos = [{x: B}, {x: A}, {x: G}]
    examples_neg = [{x: C}, {x: F}, {x: I}]
    clause = test_network.new_clause([examples_pos, examples_neg], target)[0][1]
    assert len(clause) == 1 and clause[0].op == 'Conn' and clause[0].args[0] == x
    target = expr('Flow(x, y)')
    examples_pos = [{x: B}, {x: D}, {x: E}, {x: G}]
    examples_neg = [{x: A}, {x: C}, {x: F}, {x: I}, {x: H}]
    clause = test_network.new_clause([examples_pos, examples_neg], target)[0][1]
    assert len(clause) == 2 and \
        ((clause[0].args[0] == x and clause[1].args[1] == x) or \
        (clause[0].args[1] == x and clause[1].args[0] == x))

def have_cake_and_eat_cake_too():
    init = [expr('Have(Cake)')]

    def goal_test(kb):
        required = [expr('Have(Cake)'), expr('Eaten(Cake)')]
        for q in required:
            if kb.ask(q) is False:
                return False
        return True

    ##Actions
    # Eat cake
    precond_pos = [expr('Have(Cake)')]
    precond_neg = []
    effect_add = [expr('Eaten(Cake)')]
    effect_rem = [expr('Have(Cake)')]
    eat_cake = Action(expr('Eat(Cake)'), [precond_pos, precond_neg], [effect_add, effect_rem])

    #Bake Cake
    precond_pos = []
    precond_neg = [expr('Have(Cake)')]
    effect_add = [expr('Have(Cake)')]
    effect_rem = []
    bake_cake = Action(expr('Bake(Cake)'), [precond_pos, precond_neg], [effect_add, effect_rem])

    return PDLL(init, [eat_cake, bake_cake], goal_test)

 def from_action(cls, action):
     op = action.name
     args = action.args
     preconds = []
     for p in action.precond:
         precond_op = p.op.replace('Not', '~')
         precond_args = [repr(a) for a in p.args]
         preconds.append(expr(build_expr_string(precond_op, precond_args)))
     effects = []
     for e in action.effect:
         effect_op = e.op.replace('Not', '~')
         effect_args = [repr(a) for a in e.args]
         effects.append(expr(build_expr_string(effect_op, effect_args)))
     return cls(Expr(op, *args), preconds, effects)

def distribute_and_over_or(s):
    """Given a sentence s consisting of conjunctions and disjunctions
    of literals, return an equivalent sentence in CNF.
    >>> distribute_and_over_or((A & B) | C)
    ((A | C) & (B | C))
    """
    s = expr(s)
    if s.op == '|':
        s = associate('|', s.args)
        if s.op != '|':
            return distribute_and_over_or(s)
        if len(s.args) == 0:
            return False
        if len(s.args) == 1:
            return distribute_and_over_or(s.args[0])
        conj = first(arg for arg in s.args if arg.op == '&')
        if not conj:
            return s
        others = [a for a in s.args if a is not conj]
        rest = associate('|', others)
        return associate('&', [distribute_and_over_or(c | rest)
                               for c in conj.args])
    elif s.op == '&':
        return associate('&', list(map(distribute_and_over_or, s.args)))
    else:
        return s

def tt_true(s):
    """Is a propositional sentence a tautology?
    >>> tt_true('P | ~P')
    True
    """
    s = expr(s)
    return tt_entails(True, s)

def test_graph_call():
    pddl = spare_tire()
    negkb = FolKB([expr('At(Flat, Trunk)')])
    graph = Graph(pddl, negkb)

    levels_size = len(graph.levels)
    graph()

    assert levels_size == len(graph.levels) - 1

    def convert(self, clauses):
        """Converts strings into exprs"""
        if not isinstance(clauses, Expr):
            if len(clauses) > 0:
                clauses = expr(clauses)
            else:
                clauses = []
        try:
            clauses = conjuncts(clauses)
        except AttributeError:
            clauses = clauses

        new_clauses = []
        for clause in clauses:
            if clause.op == '~':
                new_clauses.append(expr('Not' + str(clause.args[0])))
            else:
                new_clauses.append(clause)
        return new_clauses

def spare_tire_graphplan():
    pddl = spare_tire()
    negkb = FolKB([expr('At(Flat, Trunk)')])
    graphplan = GraphPlan(pddl, negkb)

    def goal_test(kb, goals):
        return all(kb.ask(q) is not False for q in goals)

    # Not sure
    goals_pos = [expr('At(Spare, Axle)'), expr('At(Flat, Ground)')]
    goals_neg = []

    while True:
        if (goal_test(graphplan.graph.levels[-1].poskb, goals_pos) and
                graphplan.graph.non_mutex_goals(goals_pos+goals_neg, -1)):
            solution = graphplan.extract_solution(goals_pos, goals_neg, -1)
            if solution:
                return solution
        graphplan.graph.expand_graph()
        if len(graphplan.graph.levels)>=2 and graphplan.check_leveloff():
            return None

def main():
    a = [i for i in range(10) if i % 2 == 1]
    b = [i for i in range(10, 16) if i % 2 == 1]
    print(a)
    print(b)
    c = [(i, j) for (i, j) in zip(a, b)]
    print(c)

    testThing()

    a = utils.expr('A & B')
    A = Expr('A')
    B = Expr('B')
    print(logic.pl_true(a, {A: True, B: True}))

 def refinements(hla, state, library): # TODO - refinements may be (multiple) HLA themselves ...
     """
     state is a Problem, containing the current state kb
     library is a dictionary containing details for every possible refinement. eg:
     {
     "HLA": [
         "Go(Home,SFO)",
         "Go(Home,SFO)",
         "Drive(Home, SFOLongTermParking)",
         "Shuttle(SFOLongTermParking, SFO)",
         "Taxi(Home, SFO)"
            ],
     "steps": [
         ["Drive(Home, SFOLongTermParking)", "Shuttle(SFOLongTermParking, SFO)"],
         ["Taxi(Home, SFO)"],
         [], # empty refinements ie primitive action
         [],
         []
            ],
     "precond_pos": [
         ["At(Home), Have(Car)"],
         ["At(Home)"],
         ["At(Home)", "Have(Car)"]
         ["At(SFOLongTermParking)"]
         ["At(Home)"]
                    ],
     "precond_neg": [[],[],[],[],[]],
     "effect_pos": [
         ["At(SFO)"],
         ["At(SFO)"],
         ["At(SFOLongTermParking)"],
         ["At(SFO)"],
         ["At(SFO)"]
                   ],
     "effect_neg": [
         ["At(Home)"],
         ["At(Home)"],
         ["At(Home)"],
         ["At(SFOLongTermParking)"],
         ["At(Home)"]
                   ]
     }
     """
     e = Expr(hla.name, hla.args)
     indices = [i for i,x in enumerate(library["HLA"]) if expr(x).op == hla.name]
     for i in indices:
         action = HLA(expr(library["steps"][i][0]), [ # TODO multiple refinements
                 [expr(x) for x in library["precond_pos"][i]],
                 [expr(x) for x in library["precond_neg"][i]]
             ], 
             [
                 [expr(x) for x in library["effect_pos"][i]],
                 [expr(x) for x in library["effect_neg"][i]]
             ])
         if action.check_precond(state.kb, action.args):
             yield action

 def goal_test(kb):
     # print(kb.clauses)
     required = [expr('Has(C1, W1)'), expr('Has(C1, E1)'), expr('Inspected(C1)'),
                 expr('Has(C2, W2)'), expr('Has(C2, E2)'), expr('Inspected(C2)')]
     for q in required:
         # print(q)
         # print(kb.ask(q))
         if kb.ask(q) is False:
             return False
     return True

def socks_and_shoes_graphplan():
    pddl = socks_and_shoes()
    graphplan = GraphPlan(pddl)

    def goal_test(kb, goals):
        return all(kb.ask(q) is not False for q in goals)

    goals = expr('RightShoeOn, LeftShoeOn')

    while True:
        if (goal_test(graphplan.graph.levels[-1].kb, goals) and graphplan.graph.non_mutex_goals(goals, -1)):
            solution = graphplan.extract_solution(goals, -1)
            if solution:
                return solution

        graphplan.graph.expand_graph()
        if len(graphplan.graph.levels) >= 2 and graphplan.check_leveloff():
            return None