<commit_before>from z3 import *
from third_party import enum
from core.callhistory import CallHistory
from core.call import Call
from core.hand import Hand
from core.callexplorer import CallExplorer
import core.suit as suit
from itertools import chain
import copy
from third_party.memoized import memoized



spades, hearts, diamonds, clubs, points = Ints('spades hearts diamonds clubs points')

axioms = [
    spades + hearts + diamonds + clubs == 13,
    spades >= 0,
    hearts >= 0,
    diamonds >= 0,
    clubs >= 0,
    0 <= points <= 37,
]

rule_of_twenty = Or(
    spades + hearts + points >= 20,
    spades + diamonds + points >= 20,
    spades + clubs + points >= 20,
    hearts + diamonds + points >= 20,
    hearts + clubs + points >= 20,
    diamonds + clubs + points >= 20)

rule_of_nineteen = Or(
    spades + hearts + points >= 19,
    spades + diamonds + points >= 19,
    spades + clubs + points >= 19,
    hearts + diamonds + points >= 19,
    hearts + clubs + points >= 19,
    diamonds + clubs + points >= 19)

rule_of_fifteen = spades + points >= 15

balanced = And(clubs >= 2, diamonds >= 2, hearts >= 2, spades >= 2,
    Or(
        And(hearts > 2, diamonds > 2, clubs > 2),
        And(spades > 2, diamonds > 2, clubs > 2),
        And(spades > 2, hearts > 2, clubs > 2),
        And(spades > 2, hearts > 2, diamonds > 2),
    )
)

# Intra-bid priorities, first phase, "interpretation priorities", like "natural, conventional" (possibly should be called types?) These select which "1N" meaning is correct.
# Inter-bid priorities, "which do you look at first" -- these order preference between "1H, vs. 1S"
# Tie-breaker-priorities -- planner stage, when 2 bids match which we make.

positions = enum.Enum(
    "RHO",
    "Partner",
    "LHO",
    "Me",
)


annotations = enum.Enum(
    "Opening",
)

def expr_for_suit(suit):
    return (clubs, diamonds, hearts, spades)[suit]

class Precondition(object):
    def __repr__(self):
        return "%s()" % self.name()

    def name(self):
        return self.__class__.__name__

    def fits(self, history, call):
        pass


class NoOpening(Precondition):
    def fits(self, history, call):
        return annotations.Opening not in history.annotations


class Opened(Precondition):
    def __init__(self, position):
        self.position = position

    def fits(self, history, call):
        return annotations.Opening in history.annotations_for_position(self.position)


class RaiseOfPartnersLastSuit(Precondition):
    def fits(self, history, call):
        partner_last_call = history.partner.last_call
        if not partner_last_call or partner_last_call.strain not in suit.SUITS:
            return False
        return call.strain == partner_last_call.strain and history.partner.min_length(partner_last_call.strain) >= 3


class UnbidSuit(Precondition):
    def fits(self, history, call):
        if call.strain not in suit.SUITS:
            return False
        return history.is_unbid_suit(call.strain)


class Jump(Precondition):
    def __init__(self, exact_size=None):
        self.exact_size = exact_size

    def _jump_size(self, last_call, call):
        if call.strain <= last_call.strain:
            # If the new suit is less than the last bid one, than we need to change more than one level for it to be a jump.
            return call.level() - last_call.level() - 1
        # Otherwise any bid not at the current level is a jump.
        return call.level() - last_call.level()

    def fits(self, history, call):
        if call.is_pass():
            return False
        if call.is_double() or call.is_redouble():
            call = history.call_history.last_contract()

        last_call = self._last_call(history)
        if not last_call or not last_call.is_contract():  # If we don't have a previous bid to compare to, this can't be a jump.
            return False
        jump_size = self._jump_size(last_call, call)
        if self.exact_size is None:
            return jump_size != 0
        return self.exact_size == jump_size

    def _last_call(self, history):
        raise NotImplementedError


class JumpFromLastContract(Jump):
    def _last_call(self, history):
        return history.call_history.last_contract()


class JumpFromMyLastBid(Jump):
    def _last_call(self, history):
        return history.me.last_call


class JumpFromPartnerLastBid(Jump):
    def _last_call(self, history):
        return history.partner.last_call


class NotJumpFromLastContract(JumpFromLastContract):
    def __init__(self):
        Jump.__init__(self, exact_size=0)


class NotJumpFromMyLastBid(JumpFromMyLastBid):
    def __init__(self):
        JumpFromMyLastBid.__init__(self, exact_size=0)


class NotJumpFromPartnerLastBid(JumpFromPartnerLastBid):
    def __init__(self):
        JumpFromPartnerLastBid.__init__(self, exact_size=0)


class Rule(object):
    preconditions = []
    category = None # Intra-bid priority

    call_name = None # FIXME: We will likely support more than one call per rule eventually.
    constraints = []
    z3_constraint = None
    annotations = []
    conditional_priorities = []
    priority = None

    def create_call(self, history):
        # FIXME: kbb rules can make more than one type of call, it's unclear
        # if we should follow that model here or not.
        call = Call(self.call_name)
        for precondition in self.preconditions:
            if not precondition.fits(history, call):
                return None
        return call

    def possible_priorities_and_conditions_for_call(self, call):
        # We're eventually going to allow more than one call per rule.
        assert call.name == self.call_name, self.call_name
        for condition, priority in self.conditional_priorities:
            yield priority, condition
        yield self.priority, BoolVal(True)

    @memoized
    def priority_for_call_and_hand(self, solver, history, call, hand):
        if not is_possible(solver, self.constraints_expr_for_call(history, call)):
            return None

        for condition, priority in self.conditional_priorities:
            if is_possible(solver, condition):
                return priority
        return self.priority

    def constraints_expr_for_call(self, history, call):
        exprs = [constraint.expr(history, call) for constraint in self.constraints]
        if self.z3_constraint:
            exprs.append(self.z3_constraint)
        return And(exprs)


opening_priorities = enum.Enum(
    "StrongTwoClubs",
    "NoTrumpOpening",
    "LongestMajor",
    "HigherMajor",
    "LowerMajor",
    "LongestMinor",
    "HigherMinor",
    "LowerMinor",
)


class Opening(Rule):
    annotations = [annotations.Opening]
    preconditions = [NoOpening()]


class OneClubOpening(Opening):
    call_name = '1C'
    z3_constraint = And(rule_of_twenty, clubs >= 3)
    conditional_priorities = [
        (Or(clubs > diamonds, And(clubs == 3, diamonds == 3)), opening_priorities.LongestMinor),
    ]
    priority = opening_priorities.LowerMinor


class OneDiamondOpening(Opening):
    call_name = '1D'
    z3_constraint = And(rule_of_twenty, diamonds >= 3)
    conditional_priorities = [
        (diamonds > clubs, opening_priorities.LongestMinor),
    ]
    priority = opening_priorities.HigherMinor


class OneHeartOpening(Opening):
    call_name = '1H'
    z3_constraint = And(rule_of_twenty, hearts >= 5)
    conditional_priorities = [
        (hearts > spades, opening_priorities.LongestMajor),
    ]
    priority = opening_priorities.LowerMajor


class OneSpadeOpening(Opening):
    call_name = '1S'
    z3_constraint = And(rule_of_twenty, spades >= 5)
    conditional_priorities = [
        (spades > hearts, opening_priorities.LongestMajor),
    ]
    priority = opening_priorities.HigherMajor


class OneNoTrumpOpening(Opening):
    call_name = '1N'
    z3_constraint = And(points >= 15, points <= 17, balanced)
    priority = opening_priorities.NoTrumpOpening


class StrongTwoClubs(Opening):
    call_name = '2C'
    z3_constraint = points >= 22  # FIXME: Should support "or 9+ winners"
    priority = opening_priorities.StrongTwoClubs


response_priorities = enum.Enum(
    "MajorLimitRaise",
    "MajorMinimumRaise",
    "LongestNewMajor",
    "OneSpadeWithFiveResponse",
    "OneHeartWithFiveResponse",
    "OneDiamondResponse",
    "OneHeartWithFourResponse",
    "OneSpadeWithFourResponse",
    "TwoHeartNewSuitResponse",
    "TwoSpadeNewSuitResponse",
    "TwoClubNewSuitResponse",
    "TwoDiamondNewSuitResponse",
    "OneNotrumpResponse",
)


class Response(Rule):
    preconditions = [Opened(positions.Partner)]


class OneDiamondResponse(Response):
    call_name = '1D'
    z3_constraint = And(points >= 6, diamonds >= 4)
    priority = response_priorities.OneDiamondResponse

# FAIL: None (expected 1S) for 432.K765.K8.A753 (hcp: 10 lp: 10 sp: 11), history: 1H P
# FAIL: None (expected 2D) for Q98.KJ732.KJ.JT9 (hcp: 11 lp: 12 sp: 11), history: 1H P
# FAIL: None (expected 2C) for QJ54.J753.KT2.A4 (hcp: 11 lp: 11 sp: 12), history: 1S P

class OneHeartResponse(Response):
    call_name = '1H'
    z3_constraint = And(points >= 6, hearts >= 4)
    conditional_priorities = [
        (And(hearts >= 5, hearts > spades), response_priorities.LongestNewMajor),
        (hearts >= 5, response_priorities.OneHeartWithFiveResponse),
    ]
    priority = response_priorities.OneHeartWithFourResponse


class OneSpadeResponse(Response):
    call_name = '1S'
    z3_constraint = And(points >= 6, spades >= 4)
    conditional_priorities = [
        (spades >= 5, response_priorities.OneSpadeWithFiveResponse)
    ]
    priority = response_priorities.OneSpadeWithFourResponse


class OneNotrumpResponse(Response):
    call_name = '1N'
    z3_constraint = points >= 6
    priority = response_priorities.OneNotrumpResponse


# Move to z3_constraint for constraints?
# Add Constraint type, and Z3() wrapper


class Constraint(object):
    def expr(self, history, call):
        pass


class Z3(object):
    def __init__(self, expr):
        self._expr = expr

    def expr(self, history, call):
        return self._expr


class MinimumCombinedLength(Constraint):
    def __init__(self, min_count):
        self.min_count = min_count

    def expr(self, history, call):
        suit = call.strain
        partner_promised_length = history.partner.min_length(suit)
        implied_length = max(self.min_count - partner_promised_length, 0)
        return expr_for_suit(suit) >= implied_length


class TwoHeartMinimumRaise(Response):
    call_name = '2H'
    preconditions = Response.preconditions + [RaiseOfPartnersLastSuit()]
    constraints = [MinimumCombinedLength(8), Z3(points >= 6)]
    priority = response_priorities.MajorMinimumRaise


class TwoSpadeMinimumRaise(Response):
    call_name = '2S'
    preconditions = Response.preconditions + [RaiseOfPartnersLastSuit()]
    constraints = [MinimumCombinedLength(8), Z3(points >= 6)]
    priority = response_priorities.MajorMinimumRaise


class ThreeHeartLimitRaise(Response):
    call_name = '3H'
    preconditions = Response.preconditions + [RaiseOfPartnersLastSuit()]
    constraints = [MinimumCombinedLength(8), Z3(points >= 10)]
    priority = response_priorities.MajorLimitRaise


# We should bid longer suits when possible, up the line for 4 cards.
# we don't currently bid 2D over 2C when we have longer diamonds.
class TwoClubNewSuitResponse(Response):
    call_name = '2C'
    preconditions = Response.preconditions + [UnbidSuit(), NotJumpFromLastContract()]
    z3_constraint = And(clubs >= 4, points >= 10)
    priority = response_priorities.TwoClubNewSuitResponse


class TwoDiamondNewSuitResponse(Response):
    call_name = '2D'
    preconditions = Response.preconditions + [UnbidSuit(), NotJumpFromLastContract()]
    z3_constraint = And(diamonds >= 4, points >= 10)
    priority = response_priorities.TwoDiamondNewSuitResponse


class TwoHeartNewSuitResponse(Response):
    call_name = '2H'
    preconditions = Response.preconditions + [UnbidSuit(), NotJumpFromLastContract()]
    z3_constraint = And(hearts >= 5, points >= 10)
    priority = response_priorities.TwoHeartNewSuitResponse


# Only possible in competative bidding.
class TwoSpadeNewSuitResponse(Response):
    call_name = '2S'
    preconditions = Response.preconditions + [UnbidSuit(), NotJumpFromLastContract()]
    z3_constraint = And(spades >= 5, points >= 10)
    priority = response_priorities.TwoSpadeNewSuitResponse


def expr_from_hand(hand):
    return And(
        clubs == len(hand.cards_in_suit(suit.CLUBS)),
        diamonds == len(hand.cards_in_suit(suit.DIAMONDS)),
        hearts == len(hand.cards_in_suit(suit.HEARTS)),
        spades == len(hand.cards_in_suit(suit.SPADES)),
        points == hand.high_card_points()
    )


class PartialOrdering(object):
    def less_than(self, left, right):
        # Our enums are written highest to lowest, so we use > for less_than. :)
        return left > right


class StandardAmericanYellowCard(object):
    # Rule ordering does not matter.  We could have python crawl the files to generate this list instead.
    rules = [
        OneClubOpening(),
        OneDiamondOpening(),
        OneHeartOpening(),
        OneSpadeOpening(),
        OneDiamondResponse(),
        OneHeartResponse(),
        OneSpadeResponse(),
        OneNotrumpResponse(),
        OneNoTrumpOpening(),
        StrongTwoClubs(),
        TwoHeartMinimumRaise(),
        TwoSpadeMinimumRaise(),
        ThreeHeartLimitRaise(),
        TwoClubNewSuitResponse(),
        TwoDiamondNewSuitResponse(),
        TwoHeartNewSuitResponse(),
        TwoSpadeNewSuitResponse(),
    ]
    priority_ordering = PartialOrdering()


# The dream:
# history.my.knowledge
# history.my.solver
# history.partner.knowledge
# annotations.Opening in history.rho.annotations
# annotations.Opening in history.rho.last_call.annotations
# history.partner.min_length(suit)
# history.partner.max_length(suit)<commit_msg>Add Rule auto-discovery<commit_after>from z3 import *
from third_party import enum
from core.callhistory import CallHistory
from core.call import Call
from core.hand import Hand
from core.callexplorer import CallExplorer
import core.suit as suit
from itertools import chain
import copy
from third_party.memoized import memoized



spades, hearts, diamonds, clubs, points = Ints('spades hearts diamonds clubs points')

axioms = [
    spades + hearts + diamonds + clubs == 13,
    spades >= 0,
    hearts >= 0,
    diamonds >= 0,
    clubs >= 0,
    0 <= points <= 37,
]

rule_of_twenty = Or(
    spades + hearts + points >= 20,
    spades + diamonds + points >= 20,
    spades + clubs + points >= 20,
    hearts + diamonds + points >= 20,
    hearts + clubs + points >= 20,
    diamonds + clubs + points >= 20)

rule_of_nineteen = Or(
    spades + hearts + points >= 19,
    spades + diamonds + points >= 19,
    spades + clubs + points >= 19,
    hearts + diamonds + points >= 19,
    hearts + clubs + points >= 19,
    diamonds + clubs + points >= 19)

rule_of_fifteen = spades + points >= 15

balanced = And(clubs >= 2, diamonds >= 2, hearts >= 2, spades >= 2,
    Or(
        And(hearts > 2, diamonds > 2, clubs > 2),
        And(spades > 2, diamonds > 2, clubs > 2),
        And(spades > 2, hearts > 2, clubs > 2),
        And(spades > 2, hearts > 2, diamonds > 2),
    )
)

# Intra-bid priorities, first phase, "interpretation priorities", like "natural, conventional" (possibly should be called types?) These select which "1N" meaning is correct.
# Inter-bid priorities, "which do you look at first" -- these order preference between "1H, vs. 1S"
# Tie-breaker-priorities -- planner stage, when 2 bids match which we make.

positions = enum.Enum(
    "RHO",
    "Partner",
    "LHO",
    "Me",
)


annotations = enum.Enum(
    "Opening",
)

def expr_for_suit(suit):
    return (clubs, diamonds, hearts, spades)[suit]

class Precondition(object):
    def __repr__(self):
        return "%s()" % self.name()

    def name(self):
        return self.__class__.__name__

    def fits(self, history, call):
        pass


class NoOpening(Precondition):
    def fits(self, history, call):
        return annotations.Opening not in history.annotations


class Opened(Precondition):
    def __init__(self, position):
        self.position = position

    def fits(self, history, call):
        return annotations.Opening in history.annotations_for_position(self.position)


class RaiseOfPartnersLastSuit(Precondition):
    def fits(self, history, call):
        partner_last_call = history.partner.last_call
        if not partner_last_call or partner_last_call.strain not in suit.SUITS:
            return False
        return call.strain == partner_last_call.strain and history.partner.min_length(partner_last_call.strain) >= 3


class UnbidSuit(Precondition):
    def fits(self, history, call):
        if call.strain not in suit.SUITS:
            return False
        return history.is_unbid_suit(call.strain)


class Jump(Precondition):
    def __init__(self, exact_size=None):
        self.exact_size = exact_size

    def _jump_size(self, last_call, call):
        if call.strain <= last_call.strain:
            # If the new suit is less than the last bid one, than we need to change more than one level for it to be a jump.
            return call.level() - last_call.level() - 1
        # Otherwise any bid not at the current level is a jump.
        return call.level() - last_call.level()

    def fits(self, history, call):
        if call.is_pass():
            return False
        if call.is_double() or call.is_redouble():
            call = history.call_history.last_contract()

        last_call = self._last_call(history)
        if not last_call or not last_call.is_contract():  # If we don't have a previous bid to compare to, this can't be a jump.
            return False
        jump_size = self._jump_size(last_call, call)
        if self.exact_size is None:
            return jump_size != 0
        return self.exact_size == jump_size

    def _last_call(self, history):
        raise NotImplementedError


class JumpFromLastContract(Jump):
    def _last_call(self, history):
        return history.call_history.last_contract()


class JumpFromMyLastBid(Jump):
    def _last_call(self, history):
        return history.me.last_call


class JumpFromPartnerLastBid(Jump):
    def _last_call(self, history):
        return history.partner.last_call


class NotJumpFromLastContract(JumpFromLastContract):
    def __init__(self):
        Jump.__init__(self, exact_size=0)


class NotJumpFromMyLastBid(JumpFromMyLastBid):
    def __init__(self):
        JumpFromMyLastBid.__init__(self, exact_size=0)


class NotJumpFromPartnerLastBid(JumpFromPartnerLastBid):
    def __init__(self):
        JumpFromPartnerLastBid.__init__(self, exact_size=0)


class Rule(object):
    preconditions = []
    category = None # Intra-bid priority

    call_name = None # FIXME: We will likely support more than one call per rule eventually.
    constraints = []
    z3_constraint = None
    annotations = []
    conditional_priorities = []
    priority = None

    def create_call(self, history):
        # FIXME: kbb rules can make more than one type of call, it's unclear
        # if we should follow that model here or not.
        call = Call(self.call_name)
        for precondition in self.preconditions:
            if not precondition.fits(history, call):
                return None
        return call

    def possible_priorities_and_conditions_for_call(self, call):
        # We're eventually going to allow more than one call per rule.
        assert call.name == self.call_name, self.call_name
        for condition, priority in self.conditional_priorities:
            yield priority, condition
        yield self.priority, BoolVal(True)

    @memoized
    def priority_for_call_and_hand(self, solver, history, call, hand):
        if not is_possible(solver, self.constraints_expr_for_call(history, call)):
            return None

        for condition, priority in self.conditional_priorities:
            if is_possible(solver, condition):
                return priority
        return self.priority

    def constraints_expr_for_call(self, history, call):
        exprs = [constraint.expr(history, call) for constraint in self.constraints]
        if self.z3_constraint:
            exprs.append(self.z3_constraint)
        return And(exprs)


opening_priorities = enum.Enum(
    "StrongTwoClubs",
    "NoTrumpOpening",
    "LongestMajor",
    "HigherMajor",
    "LowerMajor",
    "LongestMinor",
    "HigherMinor",
    "LowerMinor",
)


class Opening(Rule):
    annotations = [annotations.Opening]
    preconditions = [NoOpening()]


class OneClubOpening(Opening):
    call_name = '1C'
    z3_constraint = And(rule_of_twenty, clubs >= 3)
    conditional_priorities = [
        (Or(clubs > diamonds, And(clubs == 3, diamonds == 3)), opening_priorities.LongestMinor),
    ]
    priority = opening_priorities.LowerMinor


class OneDiamondOpening(Opening):
    call_name = '1D'
    z3_constraint = And(rule_of_twenty, diamonds >= 3)
    conditional_priorities = [
        (diamonds > clubs, opening_priorities.LongestMinor),
    ]
    priority = opening_priorities.HigherMinor


class OneHeartOpening(Opening):
    call_name = '1H'
    z3_constraint = And(rule_of_twenty, hearts >= 5)
    conditional_priorities = [
        (hearts > spades, opening_priorities.LongestMajor),
    ]
    priority = opening_priorities.LowerMajor


class OneSpadeOpening(Opening):
    call_name = '1S'
    z3_constraint = And(rule_of_twenty, spades >= 5)
    conditional_priorities = [
        (spades > hearts, opening_priorities.LongestMajor),
    ]
    priority = opening_priorities.HigherMajor


class OneNoTrumpOpening(Opening):
    call_name = '1N'
    z3_constraint = And(points >= 15, points <= 17, balanced)
    priority = opening_priorities.NoTrumpOpening


class TwoNoTrumpOpening(Opening):
    call_name = '2N'
    z3_constraint = And(points >= 20, points <= 21, balanced)
    priority = opening_priorities.NoTrumpOpening


class StrongTwoClubs(Opening):
    call_name = '2C'
    z3_constraint = points >= 22  # FIXME: Should support "or 9+ winners"
    priority = opening_priorities.StrongTwoClubs


response_priorities = enum.Enum(
    "MajorLimitRaise",
    "MajorMinimumRaise",
    "LongestNewMajor",
    "OneSpadeWithFiveResponse",
    "OneHeartWithFiveResponse",
    "OneDiamondResponse",
    "OneHeartWithFourResponse",
    "OneSpadeWithFourResponse",
    "TwoHeartNewSuitResponse",
    "TwoSpadeNewSuitResponse",
    "TwoClubNewSuitResponse",
    "TwoDiamondNewSuitResponse",
    "OneNotrumpResponse",
)


class Response(Rule):
    preconditions = [Opened(positions.Partner)]


class OneDiamondResponse(Response):
    call_name = '1D'
    z3_constraint = And(points >= 6, diamonds >= 4)
    priority = response_priorities.OneDiamondResponse

# FAIL: None (expected 1S) for 432.K765.K8.A753 (hcp: 10 lp: 10 sp: 11), history: 1H P
# FAIL: None (expected 2D) for Q98.KJ732.KJ.JT9 (hcp: 11 lp: 12 sp: 11), history: 1H P
# FAIL: None (expected 2C) for QJ54.J753.KT2.A4 (hcp: 11 lp: 11 sp: 12), history: 1S P

class OneHeartResponse(Response):
    call_name = '1H'
    z3_constraint = And(points >= 6, hearts >= 4)
    conditional_priorities = [
        (And(hearts >= 5, hearts > spades), response_priorities.LongestNewMajor),
        (hearts >= 5, response_priorities.OneHeartWithFiveResponse),
    ]
    priority = response_priorities.OneHeartWithFourResponse


class OneSpadeResponse(Response):
    call_name = '1S'
    z3_constraint = And(points >= 6, spades >= 4)
    conditional_priorities = [
        (spades >= 5, response_priorities.OneSpadeWithFiveResponse)
    ]
    priority = response_priorities.OneSpadeWithFourResponse


class OneNotrumpResponse(Response):
    call_name = '1N'
    z3_constraint = points >= 6
    priority = response_priorities.OneNotrumpResponse


# Move to z3_constraint for constraints?
# Add Constraint type, and Z3() wrapper


class Constraint(object):
    def expr(self, history, call):
        pass


class Z3(object):
    def __init__(self, expr):
        self._expr = expr

    def expr(self, history, call):
        return self._expr


class MinimumCombinedLength(Constraint):
    def __init__(self, min_count):
        self.min_count = min_count

    def expr(self, history, call):
        suit = call.strain
        partner_promised_length = history.partner.min_length(suit)
        implied_length = max(self.min_count - partner_promised_length, 0)
        return expr_for_suit(suit) >= implied_length


class TwoHeartMinimumRaise(Response):
    call_name = '2H'
    preconditions = Response.preconditions + [RaiseOfPartnersLastSuit()]
    constraints = [MinimumCombinedLength(8), Z3(points >= 6)]
    priority = response_priorities.MajorMinimumRaise


class TwoSpadeMinimumRaise(Response):
    call_name = '2S'
    preconditions = Response.preconditions + [RaiseOfPartnersLastSuit()]
    constraints = [MinimumCombinedLength(8), Z3(points >= 6)]
    priority = response_priorities.MajorMinimumRaise


class ThreeHeartLimitRaise(Response):
    call_name = '3H'
    preconditions = Response.preconditions + [RaiseOfPartnersLastSuit()]
    constraints = [MinimumCombinedLength(8), Z3(points >= 10)]
    priority = response_priorities.MajorLimitRaise


# We should bid longer suits when possible, up the line for 4 cards.
# we don't currently bid 2D over 2C when we have longer diamonds.
class TwoClubNewSuitResponse(Response):
    call_name = '2C'
    preconditions = Response.preconditions + [UnbidSuit(), NotJumpFromLastContract()]
    z3_constraint = And(clubs >= 4, points >= 10)
    priority = response_priorities.TwoClubNewSuitResponse


class TwoDiamondNewSuitResponse(Response):
    call_name = '2D'
    preconditions = Response.preconditions + [UnbidSuit(), NotJumpFromLastContract()]
    z3_constraint = And(diamonds >= 4, points >= 10)
    priority = response_priorities.TwoDiamondNewSuitResponse


class TwoHeartNewSuitResponse(Response):
    call_name = '2H'
    preconditions = Response.preconditions + [UnbidSuit(), NotJumpFromLastContract()]
    z3_constraint = And(hearts >= 5, points >= 10)
    priority = response_priorities.TwoHeartNewSuitResponse


# Only possible in competative bidding.
class TwoSpadeNewSuitResponse(Response):
    call_name = '2S'
    preconditions = Response.preconditions + [UnbidSuit(), NotJumpFromLastContract()]
    z3_constraint = And(spades >= 5, points >= 10)
    priority = response_priorities.TwoSpadeNewSuitResponse


def expr_from_hand(hand):
    return And(
        clubs == len(hand.cards_in_suit(suit.CLUBS)),
        diamonds == len(hand.cards_in_suit(suit.DIAMONDS)),
        hearts == len(hand.cards_in_suit(suit.HEARTS)),
        spades == len(hand.cards_in_suit(suit.SPADES)),
        points == hand.high_card_points()
    )


class PartialOrdering(object):
    def less_than(self, left, right):
        # Our enums are written highest to lowest, so we use > for less_than. :)
        return left > right


# FIXME: This is wrong as soon as we try to support more than one system.
def _get_subclasses(base_class):
    subclasses = base_class.__subclasses__()
    for subclass in list(subclasses):
        subclasses.extend(_get_subclasses(subclass))
    return subclasses

def _concrete_rule_classes():
    return filter(lambda rule: rule.call_name, _get_subclasses(Rule))

class StandardAmericanYellowCard(object):
    # Rule ordering does not matter.  We could have python crawl the files to generate this list instead.
    rules = [rule() for rule in _concrete_rule_classes()]
    priority_ordering = PartialOrdering()


# The dream:
# history.my.knowledge
# history.my.solver
# history.partner.knowledge
# annotations.Opening in history.rho.annotations
# annotations.Opening in history.rho.last_call.annotations
# history.partner.min_length(suit)
# history.partner.max_length(suit)
{'fraction_non_alphanumeric': 0.09622817062696823, 'fraction_numerical': 0.014171199541941026, 'mean_word_length': 3.413994629600379, 'pattern_counts': {'":': 0, '<': 12, '<?xml version=': 0, '>': 142, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6299308', 'n_tokens_mistral': 9241, 'n_tokens_neox': 8507, 'n_words': 2194}