my solution to https://shapr.github.io/posts/2019-07-10-smt-solvers.html

knapsack.py

#!/usr/bin/env python3
# run like:
# python3 knapsack.py write | yices --logic=QF_BV | python3 knapsack.py read

from collections import namedtuple

# settings

# work our way up incrementally:
minimum_scores = (30000, 60000, 90000, 92000, 94000, 95000, 96000)

thrust_weight = 36
turn_weight = 1
cost_limit = 210
individual_limit = 7

# data

Engine = namedtuple('Engine', ['name', 'size', 'thrust', 'turn'])

# from https://github.com/endless-sky/endless-sky/blob/master/data/engines.txt
engines = [
    Engine("X1050", 20, 40, 1100),  # has both thrust and turning!
    Engine("X1200", 12, 0, 1600),
    Engine("X1700", 16, 60, 0),
    Engine("X2200", 20, 0, 3070),
    Engine("X2700", 27, 115, 0),
    Engine("X3200", 35, 0, 5900),
    Engine("X3700", 46, 221, 0),
    Engine("X4200", 59, 0, 11320),
    Engine("X4700", 79, 425, 0),
    Engine("X5200", 100, 0, 21740),
    Engine("X5700", 134, 815, 0),
    Engine("Chipmunk Thruster", 20, 96, 0),
    Engine("Chipmunk Steering", 15, 0, 2560),
    Engine("Greyhound Steering", 26, 0, 4920),
    Engine("Greyhound Thruster", 34, 184, 0),
    Engine("Impala Steering", 43, 0, 9440),
    Engine("Impala Thruster", 58, 354, 0),
    Engine("Orca Steering", 74, 0, 18120),
    Engine("Orca Thruster", 98, 679, 0),
    Engine("Tyrant Steering", 125, 0, 34790),
    Engine("Tyrant Thruster", 167, 1305, 0),
    Engine("A120 Thruster", 22, 154, 0),
    Engine("A125 Steering", 16, 0, 3920),
    Engine("A250 Thruster", 34, 273, 0),
    Engine("A255 Steering", 25, 0, 6870),
    Engine("A370 Thruster", 53, 476, 0),
    Engine("A375 Steering", 38, 0, 11920),
    Engine("A520 Thruster", 82, 819, 0),
    Engine("A525 Steering", 60, 0, 20500),
    Engine("A860 Thruster", 127, 1397, 0),
    Engine("A865 Steering", 92, 0, 35090),
    Engine("Baellie", 24, 101, 2500),  # hai
    Engine("Basrem Thruster", 18, 132, 0),
    Engine("Benga Thruster", 28, 236, 0),
    Engine("Biroo Thruster", 44, 415, 0),
    Engine("Bondir Thruster", 63, 661, 0),
    Engine("Bufaer Thruster", 104, 1201, 0),
    Engine("Basrem Steering", 12, 0, 3090),
    Engine("Benga Steering", 20, 0, 5770),
    Engine("Biroo Steering", 32, 0, 10540),
    Engine("Bondir Steering", 49, 0, 17580),
    Engine("Bufaer Steering", 76, 0, 30430),
    Engine("Coalition Large Steering", 25, 0, 7119),  # coalition
    Engine("Coalition Large Thruster", 32, 262, 0),
    Engine("Coalition Small Steering", 7, 0, 1788),
    Engine("Coalition Small Thruster", 9, 66, 0),
    Engine("Korath Asteroid Steering", 10, 0, 2800),  # Korath
    Engine("Korath Asteroid Thruster", 14, 112, 0),
    Engine("Korath Comet Steering", 18, 0, 5688),
    Engine("Korath Comet Thruster", 24, 218, 0),
    Engine("Korath Lunar Steering", 30, 0, 10560),
    Engine("Korath Lunar Thruster", 40, 412, 0),
    Engine("Korath Planetary Steering", 52, 0, 20696),
    Engine("Korath Planetary Thruster", 69, 800, 0),
    Engine("Korath Stellar Steering", 89, 0, 40050),
    Engine("Korath Stellar Thruster", 118, 1534, 0),
    Engine("Pug Akfar Thruster", 43, 280, 0),  # pug
    Engine("Pug Akfar Steering", 33, 0, 7500),
    Engine("Pug Cormet Thruster", 60, 440, 0),
    Engine("Pug Comet Steering", 46, 0, 11300),
    Engine("Pug Lohmar Thruster", 84, 660, 0),
    Engine("Pug Lohmar Steering", 64, 0, 17000),
    Engine("Quarg Medium Thruster", 70, 800, 0),  # quarg
    Engine("Quarg Medium Steering", 50, 0, 16000),
    Engine("Crucible Thruster", 20, 180, 0),  # remnant
    Engine("Crucible Steering", 14, 0, 4480),
    Engine("Forge Thruster", 39, 370, 0),
    Engine("Forge Steering", 28, 0, 9520),
    Engine("Smelter Thruster", 76, 768, 0),
    Engine("Smelter Steering", 55, 0, 19800),
    Engine("Type 1 Radiant Thruster", 12, 66, 0),  # wanderer
    Engine("Type 1 Radiant Steering", 9, 0, 1728),
    Engine("Type 2 Radiant Thruster", 27, 176, 0),
    Engine("Type 2 Radiant Steering", 20, 0, 4540),
    Engine("Type 3 Radiant Thruster", 42, 315, 0),
    Engine("Type 3 Radiant Steering", 30, 0, 7860),
    Engine("Type 4 Radiant Thruster", 64, 552, 0),
    Engine("Type 4 Radiant Steering", 47, 0, 13959),
]

# utilities

alphanumeric = 'abcdefghijklmnopqrstuvwxyz0123456789'

def encode(name):
    name = name.lower()
    # this code is a little brute but it works
    name = ''.join(c if c in alphanumeric else '_' for c in name)
    return name

def scoreit(engine):
    return thrust_weight * engine.thrust + turn_weight * engine.turn

# main

def read(f):
    variables = dict()
    sat = False
    any_sat = False

    def dump():
        nonlocal variables, sat
        if not sat:
            return

        print('[solution]')
        for k, v in variables.items():
            if v > 0:
                print(f'{k}={v}')
        print()

        variables = dict()
        sat = False

    for line in f:
        line = line.strip()
        if line.startswith('(=') and line.endswith(')'):
            _, name, value = line.split(' ')
            assert value.startswith('0b')
            variables[name] = int(value[2:-1], 2)
        elif line == 'sat':
            sat = True
            any_sat = True
        elif line == 'next':
            dump()
        else:
            print(line, file=sys.stderr)

    dump()
    return any_sat

def write():
    # compute the shortest bitvectors that hold the worst case scenario:
    big = sum(scoreit(engine) for engine in engines)
    N, C = (big * individual_limit).bit_length(), individual_limit.bit_length()

    print(f'(define-type num (bitvector {N}))')
    print(f'(define-type count (bitvector {C}))')
    print('(define cost::num)')
    print('(define score::num)')

    variable_names = [encode(engine.name) for engine in engines]

    for engine, v_count in zip(engines, variable_names):
        print(f'(define {v_count}::count)')

    for engine, v_count in zip(engines, variable_names):
        print(f'(assert (bv-le {v_count} (mk-bv {C} {individual_limit})))')

    print('(assert (= cost (bv-add')
    for engine, v_count in zip(engines, variable_names):
        if C < N:
            v_count = f'(bv-zero-extend {v_count} {N - C})'
        print(f'(bv-mul {v_count} (mk-bv {N} {engine.size}))')
    print(')))')

    print('(assert (= score (bv-add')
    for engine, v_count in zip(engines, variable_names):
        if C < N:
            v_count = f'(bv-zero-extend {v_count} {N - C})'
        print(f'(bv-mul {v_count} (mk-bv {N} {scoreit(engine)}))')
    print(')))')

    # at least one chosen engine must have thrust
    print('(assert (or')
    for engine, v_count in zip(engines, variable_names):
        if engine.thrust > 0:
            print(f'(bv-gt {v_count} (mk-bv {C} 0))')
    print('))')

    # at least one chosen engine must have turn
    print('(assert (or')
    for engine, v_count in zip(engines, variable_names):
        if engine.turn > 0:
            print(f'(bv-gt {v_count} (mk-bv {C} 0))')
    print('))')

    print(f'(assert (and (bv-ge cost (mk-bv {N} 0)) (bv-le cost (mk-bv {N} {cost_limit}))))')

    for minscore in minimum_scores:
        print(f'(assert (bv-ge score (mk-bv {N} {minscore})))')
        print('(check)')
        print('(show-model)')
        print('(echo "next\\n")')

if __name__ == '__main__':
    import sys
    if len(sys.argv) < 2 or sys.argv[1] not in ('read', 'write'):
        print(f'usage: {sys.argv[0]} (read|write)', file=sys.stderr)
        sys.exit(1)
    elif sys.argv[1] == 'read':
        sat = read(sys.stdin)
        if not sat:
            sys.exit(1)
    elif sys.argv[1] == 'write':
        write()

knapsack.ys

(define-type num (bitvector 23))
(define-type count (bitvector 3))
(define cost::num)
(define score::num)
(define x1050::count)
(define x1200::count)
(define x1700::count)
(define x2200::count)
(define x2700::count)
(define x3200::count)
(define x3700::count)
(define x4200::count)
(define x4700::count)
(define x5200::count)
(define x5700::count)
(define chipmunk_thruster::count)
(define chipmunk_steering::count)
(define greyhound_steering::count)
(define greyhound_thruster::count)
(define impala_steering::count)
(define impala_thruster::count)
(define orca_steering::count)
(define orca_thruster::count)
(define tyrant_steering::count)
(define tyrant_thruster::count)
(define a120_thruster::count)
(define a125_steering::count)
(define a250_thruster::count)
(define a255_steering::count)
(define a370_thruster::count)
(define a375_steering::count)
(define a520_thruster::count)
(define a525_steering::count)
(define a860_thruster::count)
(define a865_steering::count)
(define baellie::count)
(define basrem_thruster::count)
(define benga_thruster::count)
(define biroo_thruster::count)
(define bondir_thruster::count)
(define bufaer_thruster::count)
(define basrem_steering::count)
(define benga_steering::count)
(define biroo_steering::count)
(define bondir_steering::count)
(define bufaer_steering::count)
(define coalition_large_steering::count)
(define coalition_large_thruster::count)
(define coalition_small_steering::count)
(define coalition_small_thruster::count)
(define korath_asteroid_steering::count)
(define korath_asteroid_thruster::count)
(define korath_comet_steering::count)
(define korath_comet_thruster::count)
(define korath_lunar_steering::count)
(define korath_lunar_thruster::count)
(define korath_planetary_steering::count)
(define korath_planetary_thruster::count)
(define korath_stellar_steering::count)
(define korath_stellar_thruster::count)
(define pug_akfar_thruster::count)
(define pug_akfar_steering::count)
(define pug_cormet_thruster::count)
(define pug_comet_steering::count)
(define pug_lohmar_thruster::count)
(define pug_lohmar_steering::count)
(define quarg_medium_thruster::count)
(define quarg_medium_steering::count)
(define crucible_thruster::count)
(define crucible_steering::count)
(define forge_thruster::count)
(define forge_steering::count)
(define smelter_thruster::count)
(define smelter_steering::count)
(define type_1_radiant_thruster::count)
(define type_1_radiant_steering::count)
(define type_2_radiant_thruster::count)
(define type_2_radiant_steering::count)
(define type_3_radiant_thruster::count)
(define type_3_radiant_steering::count)
(define type_4_radiant_thruster::count)
(define type_4_radiant_steering::count)
(assert (bv-le x1050 (mk-bv 3 7)))
(assert (bv-le x1200 (mk-bv 3 7)))
(assert (bv-le x1700 (mk-bv 3 7)))
(assert (bv-le x2200 (mk-bv 3 7)))
(assert (bv-le x2700 (mk-bv 3 7)))
(assert (bv-le x3200 (mk-bv 3 7)))
(assert (bv-le x3700 (mk-bv 3 7)))
(assert (bv-le x4200 (mk-bv 3 7)))
(assert (bv-le x4700 (mk-bv 3 7)))
(assert (bv-le x5200 (mk-bv 3 7)))
(assert (bv-le x5700 (mk-bv 3 7)))
(assert (bv-le chipmunk_thruster (mk-bv 3 7)))
(assert (bv-le chipmunk_steering (mk-bv 3 7)))
(assert (bv-le greyhound_steering (mk-bv 3 7)))
(assert (bv-le greyhound_thruster (mk-bv 3 7)))
(assert (bv-le impala_steering (mk-bv 3 7)))
(assert (bv-le impala_thruster (mk-bv 3 7)))
(assert (bv-le orca_steering (mk-bv 3 7)))
(assert (bv-le orca_thruster (mk-bv 3 7)))
(assert (bv-le tyrant_steering (mk-bv 3 7)))
(assert (bv-le tyrant_thruster (mk-bv 3 7)))
(assert (bv-le a120_thruster (mk-bv 3 7)))
(assert (bv-le a125_steering (mk-bv 3 7)))
(assert (bv-le a250_thruster (mk-bv 3 7)))
(assert (bv-le a255_steering (mk-bv 3 7)))
(assert (bv-le a370_thruster (mk-bv 3 7)))
(assert (bv-le a375_steering (mk-bv 3 7)))
(assert (bv-le a520_thruster (mk-bv 3 7)))
(assert (bv-le a525_steering (mk-bv 3 7)))
(assert (bv-le a860_thruster (mk-bv 3 7)))
(assert (bv-le a865_steering (mk-bv 3 7)))
(assert (bv-le baellie (mk-bv 3 7)))
(assert (bv-le basrem_thruster (mk-bv 3 7)))
(assert (bv-le benga_thruster (mk-bv 3 7)))
(assert (bv-le biroo_thruster (mk-bv 3 7)))
(assert (bv-le bondir_thruster (mk-bv 3 7)))
(assert (bv-le bufaer_thruster (mk-bv 3 7)))
(assert (bv-le basrem_steering (mk-bv 3 7)))
(assert (bv-le benga_steering (mk-bv 3 7)))
(assert (bv-le biroo_steering (mk-bv 3 7)))
(assert (bv-le bondir_steering (mk-bv 3 7)))
(assert (bv-le bufaer_steering (mk-bv 3 7)))
(assert (bv-le coalition_large_steering (mk-bv 3 7)))
(assert (bv-le coalition_large_thruster (mk-bv 3 7)))
(assert (bv-le coalition_small_steering (mk-bv 3 7)))
(assert (bv-le coalition_small_thruster (mk-bv 3 7)))
(assert (bv-le korath_asteroid_steering (mk-bv 3 7)))
(assert (bv-le korath_asteroid_thruster (mk-bv 3 7)))
(assert (bv-le korath_comet_steering (mk-bv 3 7)))
(assert (bv-le korath_comet_thruster (mk-bv 3 7)))
(assert (bv-le korath_lunar_steering (mk-bv 3 7)))
(assert (bv-le korath_lunar_thruster (mk-bv 3 7)))
(assert (bv-le korath_planetary_steering (mk-bv 3 7)))
(assert (bv-le korath_planetary_thruster (mk-bv 3 7)))
(assert (bv-le korath_stellar_steering (mk-bv 3 7)))
(assert (bv-le korath_stellar_thruster (mk-bv 3 7)))
(assert (bv-le pug_akfar_thruster (mk-bv 3 7)))
(assert (bv-le pug_akfar_steering (mk-bv 3 7)))
(assert (bv-le pug_cormet_thruster (mk-bv 3 7)))
(assert (bv-le pug_comet_steering (mk-bv 3 7)))
(assert (bv-le pug_lohmar_thruster (mk-bv 3 7)))
(assert (bv-le pug_lohmar_steering (mk-bv 3 7)))
(assert (bv-le quarg_medium_thruster (mk-bv 3 7)))
(assert (bv-le quarg_medium_steering (mk-bv 3 7)))
(assert (bv-le crucible_thruster (mk-bv 3 7)))
(assert (bv-le crucible_steering (mk-bv 3 7)))
(assert (bv-le forge_thruster (mk-bv 3 7)))
(assert (bv-le forge_steering (mk-bv 3 7)))
(assert (bv-le smelter_thruster (mk-bv 3 7)))
(assert (bv-le smelter_steering (mk-bv 3 7)))
(assert (bv-le type_1_radiant_thruster (mk-bv 3 7)))
(assert (bv-le type_1_radiant_steering (mk-bv 3 7)))
(assert (bv-le type_2_radiant_thruster (mk-bv 3 7)))
(assert (bv-le type_2_radiant_steering (mk-bv 3 7)))
(assert (bv-le type_3_radiant_thruster (mk-bv 3 7)))
(assert (bv-le type_3_radiant_steering (mk-bv 3 7)))
(assert (bv-le type_4_radiant_thruster (mk-bv 3 7)))
(assert (bv-le type_4_radiant_steering (mk-bv 3 7)))
(assert (= cost (bv-add
(bv-mul (bv-zero-extend x1050 20) (mk-bv 23 20))
(bv-mul (bv-zero-extend x1200 20) (mk-bv 23 12))
(bv-mul (bv-zero-extend x1700 20) (mk-bv 23 16))
(bv-mul (bv-zero-extend x2200 20) (mk-bv 23 20))
(bv-mul (bv-zero-extend x2700 20) (mk-bv 23 27))
(bv-mul (bv-zero-extend x3200 20) (mk-bv 23 35))
(bv-mul (bv-zero-extend x3700 20) (mk-bv 23 46))
(bv-mul (bv-zero-extend x4200 20) (mk-bv 23 59))
(bv-mul (bv-zero-extend x4700 20) (mk-bv 23 79))
(bv-mul (bv-zero-extend x5200 20) (mk-bv 23 100))
(bv-mul (bv-zero-extend x5700 20) (mk-bv 23 134))
(bv-mul (bv-zero-extend chipmunk_thruster 20) (mk-bv 23 20))
(bv-mul (bv-zero-extend chipmunk_steering 20) (mk-bv 23 15))
(bv-mul (bv-zero-extend greyhound_steering 20) (mk-bv 23 26))
(bv-mul (bv-zero-extend greyhound_thruster 20) (mk-bv 23 34))
(bv-mul (bv-zero-extend impala_steering 20) (mk-bv 23 43))
(bv-mul (bv-zero-extend impala_thruster 20) (mk-bv 23 58))
(bv-mul (bv-zero-extend orca_steering 20) (mk-bv 23 74))
(bv-mul (bv-zero-extend orca_thruster 20) (mk-bv 23 98))
(bv-mul (bv-zero-extend tyrant_steering 20) (mk-bv 23 125))
(bv-mul (bv-zero-extend tyrant_thruster 20) (mk-bv 23 167))
(bv-mul (bv-zero-extend a120_thruster 20) (mk-bv 23 22))
(bv-mul (bv-zero-extend a125_steering 20) (mk-bv 23 16))
(bv-mul (bv-zero-extend a250_thruster 20) (mk-bv 23 34))
(bv-mul (bv-zero-extend a255_steering 20) (mk-bv 23 25))
(bv-mul (bv-zero-extend a370_thruster 20) (mk-bv 23 53))
(bv-mul (bv-zero-extend a375_steering 20) (mk-bv 23 38))
(bv-mul (bv-zero-extend a520_thruster 20) (mk-bv 23 82))
(bv-mul (bv-zero-extend a525_steering 20) (mk-bv 23 60))
(bv-mul (bv-zero-extend a860_thruster 20) (mk-bv 23 127))
(bv-mul (bv-zero-extend a865_steering 20) (mk-bv 23 92))
(bv-mul (bv-zero-extend baellie 20) (mk-bv 23 24))
(bv-mul (bv-zero-extend basrem_thruster 20) (mk-bv 23 18))
(bv-mul (bv-zero-extend benga_thruster 20) (mk-bv 23 28))
(bv-mul (bv-zero-extend biroo_thruster 20) (mk-bv 23 44))
(bv-mul (bv-zero-extend bondir_thruster 20) (mk-bv 23 63))
(bv-mul (bv-zero-extend bufaer_thruster 20) (mk-bv 23 104))
(bv-mul (bv-zero-extend basrem_steering 20) (mk-bv 23 12))
(bv-mul (bv-zero-extend benga_steering 20) (mk-bv 23 20))
(bv-mul (bv-zero-extend biroo_steering 20) (mk-bv 23 32))
(bv-mul (bv-zero-extend bondir_steering 20) (mk-bv 23 49))
(bv-mul (bv-zero-extend bufaer_steering 20) (mk-bv 23 76))
(bv-mul (bv-zero-extend coalition_large_steering 20) (mk-bv 23 25))
(bv-mul (bv-zero-extend coalition_large_thruster 20) (mk-bv 23 32))
(bv-mul (bv-zero-extend coalition_small_steering 20) (mk-bv 23 7))
(bv-mul (bv-zero-extend coalition_small_thruster 20) (mk-bv 23 9))
(bv-mul (bv-zero-extend korath_asteroid_steering 20) (mk-bv 23 10))
(bv-mul (bv-zero-extend korath_asteroid_thruster 20) (mk-bv 23 14))
(bv-mul (bv-zero-extend korath_comet_steering 20) (mk-bv 23 18))
(bv-mul (bv-zero-extend korath_comet_thruster 20) (mk-bv 23 24))
(bv-mul (bv-zero-extend korath_lunar_steering 20) (mk-bv 23 30))
(bv-mul (bv-zero-extend korath_lunar_thruster 20) (mk-bv 23 40))
(bv-mul (bv-zero-extend korath_planetary_steering 20) (mk-bv 23 52))
(bv-mul (bv-zero-extend korath_planetary_thruster 20) (mk-bv 23 69))
(bv-mul (bv-zero-extend korath_stellar_steering 20) (mk-bv 23 89))
(bv-mul (bv-zero-extend korath_stellar_thruster 20) (mk-bv 23 118))
(bv-mul (bv-zero-extend pug_akfar_thruster 20) (mk-bv 23 43))
(bv-mul (bv-zero-extend pug_akfar_steering 20) (mk-bv 23 33))
(bv-mul (bv-zero-extend pug_cormet_thruster 20) (mk-bv 23 60))
(bv-mul (bv-zero-extend pug_comet_steering 20) (mk-bv 23 46))
(bv-mul (bv-zero-extend pug_lohmar_thruster 20) (mk-bv 23 84))
(bv-mul (bv-zero-extend pug_lohmar_steering 20) (mk-bv 23 64))
(bv-mul (bv-zero-extend quarg_medium_thruster 20) (mk-bv 23 70))
(bv-mul (bv-zero-extend quarg_medium_steering 20) (mk-bv 23 50))
(bv-mul (bv-zero-extend crucible_thruster 20) (mk-bv 23 20))
(bv-mul (bv-zero-extend crucible_steering 20) (mk-bv 23 14))
(bv-mul (bv-zero-extend forge_thruster 20) (mk-bv 23 39))
(bv-mul (bv-zero-extend forge_steering 20) (mk-bv 23 28))
(bv-mul (bv-zero-extend smelter_thruster 20) (mk-bv 23 76))
(bv-mul (bv-zero-extend smelter_steering 20) (mk-bv 23 55))
(bv-mul (bv-zero-extend type_1_radiant_thruster 20) (mk-bv 23 12))
(bv-mul (bv-zero-extend type_1_radiant_steering 20) (mk-bv 23 9))
(bv-mul (bv-zero-extend type_2_radiant_thruster 20) (mk-bv 23 27))
(bv-mul (bv-zero-extend type_2_radiant_steering 20) (mk-bv 23 20))
(bv-mul (bv-zero-extend type_3_radiant_thruster 20) (mk-bv 23 42))
(bv-mul (bv-zero-extend type_3_radiant_steering 20) (mk-bv 23 30))
(bv-mul (bv-zero-extend type_4_radiant_thruster 20) (mk-bv 23 64))
(bv-mul (bv-zero-extend type_4_radiant_steering 20) (mk-bv 23 47))
)))
(assert (= score (bv-add
(bv-mul (bv-zero-extend x1050 20) (mk-bv 23 2540))
(bv-mul (bv-zero-extend x1200 20) (mk-bv 23 1600))
(bv-mul (bv-zero-extend x1700 20) (mk-bv 23 2160))
(bv-mul (bv-zero-extend x2200 20) (mk-bv 23 3070))
(bv-mul (bv-zero-extend x2700 20) (mk-bv 23 4140))
(bv-mul (bv-zero-extend x3200 20) (mk-bv 23 5900))
(bv-mul (bv-zero-extend x3700 20) (mk-bv 23 7956))
(bv-mul (bv-zero-extend x4200 20) (mk-bv 23 11320))
(bv-mul (bv-zero-extend x4700 20) (mk-bv 23 15300))
(bv-mul (bv-zero-extend x5200 20) (mk-bv 23 21740))
(bv-mul (bv-zero-extend x5700 20) (mk-bv 23 29340))
(bv-mul (bv-zero-extend chipmunk_thruster 20) (mk-bv 23 3456))
(bv-mul (bv-zero-extend chipmunk_steering 20) (mk-bv 23 2560))
(bv-mul (bv-zero-extend greyhound_steering 20) (mk-bv 23 4920))
(bv-mul (bv-zero-extend greyhound_thruster 20) (mk-bv 23 6624))
(bv-mul (bv-zero-extend impala_steering 20) (mk-bv 23 9440))
(bv-mul (bv-zero-extend impala_thruster 20) (mk-bv 23 12744))
(bv-mul (bv-zero-extend orca_steering 20) (mk-bv 23 18120))
(bv-mul (bv-zero-extend orca_thruster 20) (mk-bv 23 24444))
(bv-mul (bv-zero-extend tyrant_steering 20) (mk-bv 23 34790))
(bv-mul (bv-zero-extend tyrant_thruster 20) (mk-bv 23 46980))
(bv-mul (bv-zero-extend a120_thruster 20) (mk-bv 23 5544))
(bv-mul (bv-zero-extend a125_steering 20) (mk-bv 23 3920))
(bv-mul (bv-zero-extend a250_thruster 20) (mk-bv 23 9828))
(bv-mul (bv-zero-extend a255_steering 20) (mk-bv 23 6870))
(bv-mul (bv-zero-extend a370_thruster 20) (mk-bv 23 17136))
(bv-mul (bv-zero-extend a375_steering 20) (mk-bv 23 11920))
(bv-mul (bv-zero-extend a520_thruster 20) (mk-bv 23 29484))
(bv-mul (bv-zero-extend a525_steering 20) (mk-bv 23 20500))
(bv-mul (bv-zero-extend a860_thruster 20) (mk-bv 23 50292))
(bv-mul (bv-zero-extend a865_steering 20) (mk-bv 23 35090))
(bv-mul (bv-zero-extend baellie 20) (mk-bv 23 6136))
(bv-mul (bv-zero-extend basrem_thruster 20) (mk-bv 23 4752))
(bv-mul (bv-zero-extend benga_thruster 20) (mk-bv 23 8496))
(bv-mul (bv-zero-extend biroo_thruster 20) (mk-bv 23 14940))
(bv-mul (bv-zero-extend bondir_thruster 20) (mk-bv 23 23796))
(bv-mul (bv-zero-extend bufaer_thruster 20) (mk-bv 23 43236))
(bv-mul (bv-zero-extend basrem_steering 20) (mk-bv 23 3090))
(bv-mul (bv-zero-extend benga_steering 20) (mk-bv 23 5770))
(bv-mul (bv-zero-extend biroo_steering 20) (mk-bv 23 10540))
(bv-mul (bv-zero-extend bondir_steering 20) (mk-bv 23 17580))
(bv-mul (bv-zero-extend bufaer_steering 20) (mk-bv 23 30430))
(bv-mul (bv-zero-extend coalition_large_steering 20) (mk-bv 23 7119))
(bv-mul (bv-zero-extend coalition_large_thruster 20) (mk-bv 23 9432))
(bv-mul (bv-zero-extend coalition_small_steering 20) (mk-bv 23 1788))
(bv-mul (bv-zero-extend coalition_small_thruster 20) (mk-bv 23 2376))
(bv-mul (bv-zero-extend korath_asteroid_steering 20) (mk-bv 23 2800))
(bv-mul (bv-zero-extend korath_asteroid_thruster 20) (mk-bv 23 4032))
(bv-mul (bv-zero-extend korath_comet_steering 20) (mk-bv 23 5688))
(bv-mul (bv-zero-extend korath_comet_thruster 20) (mk-bv 23 7848))
(bv-mul (bv-zero-extend korath_lunar_steering 20) (mk-bv 23 10560))
(bv-mul (bv-zero-extend korath_lunar_thruster 20) (mk-bv 23 14832))
(bv-mul (bv-zero-extend korath_planetary_steering 20) (mk-bv 23 20696))
(bv-mul (bv-zero-extend korath_planetary_thruster 20) (mk-bv 23 28800))
(bv-mul (bv-zero-extend korath_stellar_steering 20) (mk-bv 23 40050))
(bv-mul (bv-zero-extend korath_stellar_thruster 20) (mk-bv 23 55224))
(bv-mul (bv-zero-extend pug_akfar_thruster 20) (mk-bv 23 10080))
(bv-mul (bv-zero-extend pug_akfar_steering 20) (mk-bv 23 7500))
(bv-mul (bv-zero-extend pug_cormet_thruster 20) (mk-bv 23 15840))
(bv-mul (bv-zero-extend pug_comet_steering 20) (mk-bv 23 11300))
(bv-mul (bv-zero-extend pug_lohmar_thruster 20) (mk-bv 23 23760))
(bv-mul (bv-zero-extend pug_lohmar_steering 20) (mk-bv 23 17000))
(bv-mul (bv-zero-extend quarg_medium_thruster 20) (mk-bv 23 28800))
(bv-mul (bv-zero-extend quarg_medium_steering 20) (mk-bv 23 16000))
(bv-mul (bv-zero-extend crucible_thruster 20) (mk-bv 23 6480))
(bv-mul (bv-zero-extend crucible_steering 20) (mk-bv 23 4480))
(bv-mul (bv-zero-extend forge_thruster 20) (mk-bv 23 13320))
(bv-mul (bv-zero-extend forge_steering 20) (mk-bv 23 9520))
(bv-mul (bv-zero-extend smelter_thruster 20) (mk-bv 23 27648))
(bv-mul (bv-zero-extend smelter_steering 20) (mk-bv 23 19800))
(bv-mul (bv-zero-extend type_1_radiant_thruster 20) (mk-bv 23 2376))
(bv-mul (bv-zero-extend type_1_radiant_steering 20) (mk-bv 23 1728))
(bv-mul (bv-zero-extend type_2_radiant_thruster 20) (mk-bv 23 6336))
(bv-mul (bv-zero-extend type_2_radiant_steering 20) (mk-bv 23 4540))
(bv-mul (bv-zero-extend type_3_radiant_thruster 20) (mk-bv 23 11340))
(bv-mul (bv-zero-extend type_3_radiant_steering 20) (mk-bv 23 7860))
(bv-mul (bv-zero-extend type_4_radiant_thruster 20) (mk-bv 23 19872))
(bv-mul (bv-zero-extend type_4_radiant_steering 20) (mk-bv 23 13959))
)))
(assert (or
(bv-gt x1050 (mk-bv 3 0))
(bv-gt x1700 (mk-bv 3 0))
(bv-gt x2700 (mk-bv 3 0))
(bv-gt x3700 (mk-bv 3 0))
(bv-gt x4700 (mk-bv 3 0))
(bv-gt x5700 (mk-bv 3 0))
(bv-gt chipmunk_thruster (mk-bv 3 0))
(bv-gt greyhound_thruster (mk-bv 3 0))
(bv-gt impala_thruster (mk-bv 3 0))
(bv-gt orca_thruster (mk-bv 3 0))
(bv-gt tyrant_thruster (mk-bv 3 0))
(bv-gt a120_thruster (mk-bv 3 0))
(bv-gt a250_thruster (mk-bv 3 0))
(bv-gt a370_thruster (mk-bv 3 0))
(bv-gt a520_thruster (mk-bv 3 0))
(bv-gt a860_thruster (mk-bv 3 0))
(bv-gt baellie (mk-bv 3 0))
(bv-gt basrem_thruster (mk-bv 3 0))
(bv-gt benga_thruster (mk-bv 3 0))
(bv-gt biroo_thruster (mk-bv 3 0))
(bv-gt bondir_thruster (mk-bv 3 0))
(bv-gt bufaer_thruster (mk-bv 3 0))
(bv-gt coalition_large_thruster (mk-bv 3 0))
(bv-gt coalition_small_thruster (mk-bv 3 0))
(bv-gt korath_asteroid_thruster (mk-bv 3 0))
(bv-gt korath_comet_thruster (mk-bv 3 0))
(bv-gt korath_lunar_thruster (mk-bv 3 0))
(bv-gt korath_planetary_thruster (mk-bv 3 0))
(bv-gt korath_stellar_thruster (mk-bv 3 0))
(bv-gt pug_akfar_thruster (mk-bv 3 0))
(bv-gt pug_cormet_thruster (mk-bv 3 0))
(bv-gt pug_lohmar_thruster (mk-bv 3 0))
(bv-gt quarg_medium_thruster (mk-bv 3 0))
(bv-gt crucible_thruster (mk-bv 3 0))
(bv-gt forge_thruster (mk-bv 3 0))
(bv-gt smelter_thruster (mk-bv 3 0))
(bv-gt type_1_radiant_thruster (mk-bv 3 0))
(bv-gt type_2_radiant_thruster (mk-bv 3 0))
(bv-gt type_3_radiant_thruster (mk-bv 3 0))
(bv-gt type_4_radiant_thruster (mk-bv 3 0))
))
(assert (or
(bv-gt x1050 (mk-bv 3 0))
(bv-gt x1200 (mk-bv 3 0))
(bv-gt x2200 (mk-bv 3 0))
(bv-gt x3200 (mk-bv 3 0))
(bv-gt x4200 (mk-bv 3 0))
(bv-gt x5200 (mk-bv 3 0))
(bv-gt chipmunk_steering (mk-bv 3 0))
(bv-gt greyhound_steering (mk-bv 3 0))
(bv-gt impala_steering (mk-bv 3 0))
(bv-gt orca_steering (mk-bv 3 0))
(bv-gt tyrant_steering (mk-bv 3 0))
(bv-gt a125_steering (mk-bv 3 0))
(bv-gt a255_steering (mk-bv 3 0))
(bv-gt a375_steering (mk-bv 3 0))
(bv-gt a525_steering (mk-bv 3 0))
(bv-gt a865_steering (mk-bv 3 0))
(bv-gt baellie (mk-bv 3 0))
(bv-gt basrem_steering (mk-bv 3 0))
(bv-gt benga_steering (mk-bv 3 0))
(bv-gt biroo_steering (mk-bv 3 0))
(bv-gt bondir_steering (mk-bv 3 0))
(bv-gt bufaer_steering (mk-bv 3 0))
(bv-gt coalition_large_steering (mk-bv 3 0))
(bv-gt coalition_small_steering (mk-bv 3 0))
(bv-gt korath_asteroid_steering (mk-bv 3 0))
(bv-gt korath_comet_steering (mk-bv 3 0))
(bv-gt korath_lunar_steering (mk-bv 3 0))
(bv-gt korath_planetary_steering (mk-bv 3 0))
(bv-gt korath_stellar_steering (mk-bv 3 0))
(bv-gt pug_akfar_steering (mk-bv 3 0))
(bv-gt pug_comet_steering (mk-bv 3 0))
(bv-gt pug_lohmar_steering (mk-bv 3 0))
(bv-gt quarg_medium_steering (mk-bv 3 0))
(bv-gt crucible_steering (mk-bv 3 0))
(bv-gt forge_steering (mk-bv 3 0))
(bv-gt smelter_steering (mk-bv 3 0))
(bv-gt type_1_radiant_steering (mk-bv 3 0))
(bv-gt type_2_radiant_steering (mk-bv 3 0))
(bv-gt type_3_radiant_steering (mk-bv 3 0))
(bv-gt type_4_radiant_steering (mk-bv 3 0))
))
(assert (and (bv-ge cost (mk-bv 23 0)) (bv-le cost (mk-bv 23 210))))
(assert (bv-ge score (mk-bv 23 30000)))
(check)
(show-model)
(echo "next\n")
(assert (bv-ge score (mk-bv 23 60000)))
(check)
(show-model)
(echo "next\n")
(assert (bv-ge score (mk-bv 23 90000)))
(check)
(show-model)
(echo "next\n")
(assert (bv-ge score (mk-bv 23 92000)))
(check)
(show-model)
(echo "next\n")
(assert (bv-ge score (mk-bv 23 94000)))
(check)
(show-model)
(echo "next\n")
(assert (bv-ge score (mk-bv 23 95000)))
(check)
(show-model)
(echo "next\n")
(assert (bv-ge score (mk-bv 23 96000)))
(check)
(show-model)
(echo "next\n")