package none;

import java.awt.Color;
import java.awt.Desktop;
import java.awt.MouseInfo;
import java.awt.Point;
import java.awt.Robot;
import java.awt.event.InputEvent;
import java.net.URI;
import java.util.Calendar;
import java.util.Random;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 *
 * @author rohan
 */
public class PetFloofer {

	/**
	 * @param args the command line arguments
	 */
	public static void main(String[] args) throws Exception {
        Thread.sleep(3000);
		int NUM_PETS = 25;
		int pause = 334;
		Robot robot = new Robot();
		int steps = 334;
		int startX = 780;
		int endX = 1150;
	    double stepSize = ((double) (endX - startX) / steps);
		for(int i = 0;i<=NUM_PETS-1;i++){
            for(int step_num = 0;step_num<=steps-1;step_num++){
            int x = (int) (startX + step_num * stepSize);
            robot.mouseMove(x, 400);
            Thread.sleep(pause/steps);
            }
		}

		}

	}
        

        javac PetFloofer.java && java PetFloofer.java

        
            import pysmt as pysmt
import sys
from pysmt.shortcuts import SBV, Symbol, is_valid, Equals
from pysmt.typing import BV32

from pysmt.shortcuts import Symbol, Or, And, GE, LT, Plus, Equals, Int,  get_model, BV
from pysmt.typing import INT

import time

import mip

from mip import Model, xsum, maximize, BINARY, OptimizationStatus, ConstrsGenerator, GRB, CBC

from collections import Counter

if len(sys.argv) == 2:
    print("here!")
    dic = sys.argv[1]
else:
    dic = "wordle_guesses.txt"

ALPHABET = "abcdefghijklmnopqrstuvwxyz"

WORDLE_LEN = 5
CHARS = 5

with open(dic) as fh:
    WORD_LIST = list(set([word.strip() for word in fh.readlines() if len(word.strip()) == CHARS and CHARS == len(set(word.strip()))]))




# Too slow: takes one hour
# TODO: figure out how to get all solutions (solution re-run with additional constraints. SOlution counting is known
# to be #P complete, so not much too do but have runtime rpoporational to number of solutions
def get_all_wordle_solutions_mip(dictionary: list[str], blacklist: list[list[str]] = []) -> None | list[str]:
    solutions = set()

    m = Model("Quick milp wordle model. Perf benchmark CBC free solver", solver_name = CBC)

    words = {word:m.add_var(var_type=BINARY) for word in  dictionary}

    m += xsum(word for word in words.values()) == 5

    word_counts = {word: Counter(word) for word in words}

    for ch in ALPHABET:
        m += xsum(words[word] * word_counts[word][ch] for word in words) <= 1

    for solution in blacklist:
        m += get_constraint_from_solution(solution)

    class KeepOnSolving(ConstrsGenerator):
        def generate_constrs(self, model, depth = 0, npass = 0):
            solution = tuple(dictionary[i] for i in range(len(model.vars)) if model.vars[i].x >= .99)
            solutions.add(solution)
            model += xsum(var for var in model.vars if var.x >= .99) <= 4
            print(solution)
            time.sleep(0.25)


    m.lazy_constrs_generator = KeepOnSolving()
    m.infeas_tol = 1e-2
    status = m.optimize(max_seconds = 1000000000000)

    return solutions

def get_bitvec(word: str) -> int:
    out = 0
    counts = Counter(word)
    for i, ch in enumerate(ALPHABET):
        out += counts[ch] << i
    return out

def get_all_solutions_smt(dictionary: list[str]):
    solutions = []



    unique_chars = [word for word in dictionary if len(set(word)) == len(word)]

    bitvecs = [get_bitvec(word) for word in unique_chars]

    def get_one_solution_smt(blacklist: list[list[str]] = []) -> list[str]:
        words = [Symbol("word" + str(i), BV32) for i in range(WORDLE_LEN)]
        domains = And(Or(Equals(word, BV(vec, 32)) for vec in bitvecs) for word in words)


        problem = And(And(Equals(words[i] & words[j], BV(0, 32))for j in range(i)) for i in range(WORDLE_LEN))
        formula = And(domains, problem)

        print("Serialization of the formula:")
        print(formula)

        model = get_model(formula)
        if model:
            print(model)

        return None

    solutions.append(get_one_solution_smt())


    return solutions

def get_one_solution_hardcoded_smt(dictionary: list[str]) -> list[list[str]]:
    """
    Output of hardcoded run
    word4 := 35668104_32
word0 := 656404_32
word1 := 17863168_32
word2 := 10562_32
word3 := 4522017_32

    :param dictionary:
    :return:
    """
    hardcoded = [35668104, 656404, 17863168, 10562, 4522017]
    out = [[]]

    for vec in hardcoded:
        for word in dictionary:
            if len(set(word)) == len(word) and get_bitvec(word) == vec:
                out[0].append(word)
                break

    return out



strategies = [get_all_wordle_solutions_mip, get_one_solution_hardcoded_smt]

for strategy in reversed(strategies):
    solutions = strategy(WORD_LIST)
    print(str(strategy), "found", len(solutions), "solutions")
    for words in solutions:
        print(str(strategy), " Solution: ", *words)


        

        javac PetFloofer.java && java PetFloofer.java

        
var counter = 30;
var counterInterval;

E.setFlags({pretokenise:1});

gameOver = false;

var stop = false;
var score = 0;
STANFORD_COLOR = 182;
SCREEN_SIZE= 240;
MIDDLE = SCREEN_SIZE >> 1;
BOARD_HEIGHT = 24;
BOARD_WIDTH = 12;

TETRIS_FILL = BOARD_WIDTH;

SQUARE_SIZE = 8;
X_SQUARES = SCREEN_SIZE / SQUARE_SIZE;
Y_SQUARES = SCREEN_SIZE / SQUARE_SIZE;

START_X = (X_SQUARES - BOARD_WIDTH) / 2;
START_Y = (Y_SQUARES - BOARD_HEIGHT) / 2;

colors = [0x000000, 16, 204, 51, 162];
// Long, S,  Box, T, L, Right handed L, trimino, monomino
pieces = [[4, 15 << 4], [3, 51], [2, 15], [3, 23], [3, 15], [3, 39], [3, 56], [1,1]];

function getBit(n, b){
  "ram";
  // assumes n is a 32 bit integer. UB otherwise.
 return (n & (1 << b)) >> b;
}


function setBit(n, b, val){
  "ram";
  // assumes n is a 32 bit integer. UB otherwise.
 return (n | (val << b));
}

function rotate(piece){
 /* Rotate piece 90 degrees counter clockwise */
  // yeah yeah,. there's a better way
  // math math.
  var len = piece[0];
  if(piece[0] == 2){
  return piece;
  }
  var new_locs;
  if(piece[0] == 4){
  new_locs = [12, 8, 4, 0, 13, 9, 5, 1, 14, 10, 6, 2, 15, 11, 7, 3];
  }else{
   new_locs = [6, 3, 0, 7, 4, 1, 8, 5, 2];
  }

  var out = 0;

  for(var i = 0; i < len * len; i++){
  out = setBit(out, new_locs[i], getBit(piece[1], i));
  }

  return [piece[0], out];


}

function rotateOptions(piece){
  var out = [piece];
  for(var i = 0; i< 3;i++){
    out[i + 1] = rotate(out[i]);
  }
  return out;
}
pieces = pieces.map(rotateOptions);


function check(buff, x, y){
  "ram";
  return  buff[(y + START_Y) * Y_SQUARES + (x + START_X)];
}

function set(buff, x, y, val){
"ram";
  buff[(y  + START_Y) * Y_SQUARES + (x + START_X)] = val;
}


function getRandomPiece(){
  "ram";
  return [colors[ 1 + Math.floor(Math.random()* (colors.length -1))],
                 pieces[Math.floor(pieces.length * Math.random())], BOARD_WIDTH >> 1 - 2, 0, 0];
}

current_piece = getRandomPiece();


function assignValuesToPiece(piece, colorMultiplier){
  "ram";
  var len = piece[1][0][0];
  for(var i = 0; i< len; i++){
    for(var j = 0; j< len; j++){
      x = piece[2];
      y = piece[3];
      piece_bm = piece[1][piece[4]][1]
      color = piece[0] * colorMultiplier;
      if(getBit(piece_bm, j * len + i)){
        set(board, x + i, y + j, color);
        }
    }
  }
}

function getBoard(){
  const img = new Uint8Array(X_SQUARES * Y_SQUARES).fill(STANFORD_COLOR);
  for(var i = 0; i < BOARD_HEIGHT; i++){
  for(var j = 0; j < BOARD_WIDTH; j++){
      img[(i + START_Y) * Y_SQUARES +  j + START_X] = 0;
    }
  }
  return img;
}

var board = getBoard();

function drawBoard(board){
  "ram";
  const imgObj = {width: X_SQUARES, height: Y_SQUARES, bpp: 8,
                  buffer: board, msb: true};
  g.drawImage(imgObj, 0, 0, {scale: SQUARE_SIZE});


  g.setFontAlign(0,0); // center font
  g.setFont("6x8",1.5); // bitmap font, 8x magnified
  g.setColor(-1).drawString("Score:", 210, 112);
  g.setFontAlign(0,0); // center font
  g.setFont("6x8",2.5); // bitmap font, 8x magnified
  g.setColor(-1).drawString(score, 210, 130);
}

function isValidPlacement(piece){
  "ram";
  len = piece[1][0][0];
  console.log(len);
  console.log(piece);


  for(var i = 0; i< len; i++){
    for(var j = 0; j< len; j++){
      x = piece[2] + i;
      y = piece[3] + j;
      pieceSet = getBit(piece[1][piece[4]][1], j * len + i);

      if(pieceSet){
      inBounds = x >= 0 && x < BOARD_WIDTH && y >= 0 && y < BOARD_HEIGHT;
      invalid = pieceSet != 0 && (!inBounds || (check(board, x, y) != 0));

      if(invalid){
      return false;
      }
      }
    }

}
      return true;
}



function onlyFall(piece){
  "ram";
    // TODO: implement rotation ?
  return [piece[0], piece[1], piece[2], piece[3] + 1, piece[4]];
}
function updatePiecePlacement(piece){
  dx = 0;
  dx += BTN1.read() || BTN4.read()? -1 : 0;
  dx += BTN3.read() || BTN5.read() ? 1 : 0;

  return [piece[0], piece[1], piece[2] + dx, piece[3] + 1, (piece[4] + (BTN2.read() ? 1 : 0)) & 3];

}

function countLastRow(n){
  "ram";
  sum = 0;
  for(var i = 0; i< BOARD_WIDTH; i++){
   sum += !!check(board, i, n);
  }
  return sum;
}


function updateBoard(){
  "ram";
  score += 1;
  assignValuesToPiece(current_piece, 0);
  var new_piece = updatePiecePlacement(current_piece);
  if(isValidPlacement(new_piece)){

    current_piece = new_piece;
    assignValuesToPiece(current_piece, 1);
  } else {
     var new_piece_fall = onlyFall(current_piece);
  if(isValidPlacement(new_piece_fall)){
    assignValuesToPiece(current_piece, 0);
    current_piece = new_piece_fall;
    assignValuesToPiece(current_piece, 1);
  } else {
    assignValuesToPiece(current_piece, 1)
    extra = 0;

    var keep = Array(BOARD_HEIGHT).fill(0);

    for(var i = 0; i < BOARD_HEIGHT ; i++){
     if(countLastRow(i) >= TETRIS_FILL){
       extra += 1
       score += 10;
     } else {
       keep[i] = 1;
     }

    }

    if(extra > 0){
      newBoard = getBoard();
      count = 0;
      for(var i = 0; i< keep.length; i++){
        if(keep[keep.length - i]){

          var h_new = BOARD_HEIGHT + START_Y - count -1;
          var h = BOARD_HEIGHT + START_Y - i;
        slice = board.subarray((h) * Y_SQUARES, (h + 1) * Y_SQUARES);
        newBoard.set(slice, Y_SQUARES * h_new);
        count += 1
        }
      }
      board = newBoard;
    }

    current_piece = getRandomPiece();

    if(!isValidPlacement(current_piece)){
       gameOver = true;
       }


  }
  }
}

function drawBg(){
  "ram";

}

function gameOverScreen(){
g.setFontAlign(0,0); // center font
g.setFont("6x8",3); // bitmap font, 8x magnified
  g.setColor(-1).drawString("Game Over!", MIDDLE, MIDDLE);
 stop = true;
}

function tetris() {
  "ram";

  if(stop){
  return;
  }

  drawBoard(board);
  if(!gameOver){

  updateBoard();
  }
  else{
    gameOverScreen();
  }
  Bangle.setLCDPower(1);
}

function loop() {
  "ram";
  tetris();
  setTimeout(loop, 100 - (score >> 4));
}



g.clear();
loop();


        

        
import random
import pandas as pd
import collections
import time
import pysmt
from pysmt.shortcuts import Symbol, LE, GE, Int, And, Equals, Plus, Solver, Or, Iff, Bool, get_model
from pysmt.typing import INT
from mip import *
from functools import reduce
from itertools import combinations
from operator import mul
from scipy.optimize import minimize
from hyperopt import fmin, tpe, space_eval, hp

critical_ratio = 4.4
REPEATS = 10
TIMEOUT = 20
MIN_N = 3
MAX_N = 1000

# https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/descr.html#:~:text=One%20particularly%20interesting%20property%20of%20uniform%20Random-3-SAT%20is,systematically%20increasing%20%28or%20decreasing%29%20the%20number%20of%20kclauses
# We vigorously handwave the phase transition for 3sat


"""
Benchmark various free ways to solve 3sat
"""

def create_random_ksat(num_variables, num_clauses, k = 3):
    """
    Return a random 3sat clause with num_variable  number of variables and num_clauses clauses

    :param num_variables:
    :param num_clauses:
    :param k: k in ksat
    :return: A list of K-tlists of variables. Each variable is tuple contains a pair, which is an integer (the name of the variable)
    and whether or not it is negated. This is a 3sat clause,in CnF
    """
    def valid(clause):
        return len(set(var for var, _ in clause)) == len(clause)
    def create_clause():
        while True:
            clause = tuple((random.choice(range(num_variables)), random.random() < .5) for i in range(k))
            if valid(clause):
                return clause

    clauses = set()
    while len(clauses) < num_clauses:
        new_clause = create_clause()
        while new_clause in clauses:
            new_clause = create_clause()
        clauses.add(new_clause)

    return list(clauses)

def evaluate(cnf, variables):
    return all(any(variables[name] == val for name, val in clause) for clause in cnf)

def get_num_symbols(sat_instance):
    return max(max(tup[0] for tup in clause) for clause in sat_instance) + 1

def canonical_solver(sat_instance):
    """
    Reference solver. Assume complete and sound.
    :param sat_instance:
    :return:
    """

    num_symbols = get_num_symbols(sat_instance)
    symbols = [Symbol(str(i)) for i in range(num_symbols)]
    domains = [Or([Iff(Bool(is_true), symbols[variable]) for variable, is_true in clause]) for clause in sat_instance]

    formula = And(domains)

    model = get_model(formula)
    if model:
        return True
    else:
        return False

def assignment_from_num(i, num):
    return [bool((i >> index) & 1) for index in range(num)]

def nonconvex_local(sat_instance):
    n = get_num_symbols(sat_instance)

    def cost(x):
        return [sum(
            min(int(1 - x[variable]) if is_true else int(x[variable]) for variable, is_true in clause)
            for clause in sat_instance
        )
        ]

    results = []

    for i in range(10):
        start = [int(random.random() < .5) for i in range(n)]
        result = minimize(cost, start, bounds = [(0, 1) for i in range(n)])

        guessed_output = [int(a >= 0.5) for a in result.x]

        results.append(evaluate(sat_instance, guessed_output))

    return any(results)

def hyperopt(sat_instance):
    n = get_num_symbols(sat_instance)
    def cost(x):
        return sum([
            min(int(1 - x[variable]) if is_true else int(x[variable]) for variable, is_true in clause)
            for clause in sat_instance
        ])
    c = 2.1
    best = fmin(fn=cost,
                space=[hp.randint('x' + str(i), 0, 2) for i in range(n)],
                algo=tpe.suggest,
                max_evals = 2 * int(n ** c))

    return cost(list(best.values())) < 1

def brute_force(sat_instance):
    """
    Solve in Exponential time. For fun. O(c * (2 ** n))
    :param sat_instance:
    :return:
    """
    def all_instances(num):
        for i in range(2 ** num):
            yield assignment_from_num(i, num)
    return any(evaluate(sat_instance, s) for s in all_instances(get_num_symbols(sat_instance)))

def do_benchmark() -> pd.DataFrame:
    solution_strategies = {"canonical":canonical_solver, "ilp": do_cbc_solver, "schonig": schonig,
                           "crank_algorithm": crank_algorithm, "local_sat": local_sat,
                           "brute_force": brute_force, "nonconvex_local": nonconvex_local, "hyperopt": hyperopt}
    hit_cutoffs = set()
    ns = [int(a / REPEATS) for a in range(MIN_N * REPEATS, MAX_N * REPEATS, 1)]
    cols = collections.defaultdict(list)

    for n in ns:
        new_row = dict()
        new_row["n"] = n
        instance = create_random_ksat(n, int(n * critical_ratio))
        for solution_name, solution in solution_strategies.items():
            start = time.time()
            new_row[solution_name] = solution(instance) if solution_name not in hit_cutoffs else False
            end = time.time()
            new_time = end - start
            new_row[solution_name + "_time"] = new_time
            if new_time > TIMEOUT:
                hit_cutoffs.add(solution_name)
        right_solution = new_row["canonical"]

        for solution_name in solution_strategies:
            if solution_name in hit_cutoffs:
                new_row[solution_name + "_correct"] = False
            else:
                new_row[solution_name + "_correct"] = right_solution == new_row[solution_name]

        for key in new_row:
            cols[key].append(new_row[key])

    return pd.DataFrame(cols)

def do_cbc_solver(sat_instance):
    n = get_num_symbols(sat_instance)

    m = Model("knapsack", solver_name = CBC)

    x = [m.add_var(var_type=BINARY) for i in range(n)]

    for clause in sat_instance:
        m += xsum(x[var] if is_true else 1 - x[var] for var, is_true in clause) >= 1

    status = m.optimize()

    return status == OptimizationStatus.OPTIMAL or status == OptimizationStatus.FEASIBLE


def schonig(sat_instance):
    """
    Schonig's algorithm
    :param sat_instance:
    :return:
    """
    n = get_num_symbols(sat_instance)

    def attempt_greedy_walk():
        randomized_assignment = [random.random() < .5 for i in range(n)]
        c = len(sat_instance)
        for i in range(5 * c):
            evaluation = evaluate(sat_instance, randomized_assignment)
            if evaluation:
                return True
            for clause in sat_instance:
                if not evaluate([clause], randomized_assignment):
                    var, _ = random.choice(clause)
                    randomized_assignment[var] = not randomized_assignment[var]
                    break

        return False


    return any(attempt_greedy_walk() for i in range(10))

def local_sat(sat_instance):
    """
    Gradient descent esque sat, with some simulated annealing. Should be worse than schonig better better than the crank
    :return:
    """
    """
    Schonig's algorithm
    :param sat_instance:
    :return:
    """
    n = get_num_symbols(sat_instance)

    map = [0] * n

    for clause in sat_instance:
        for variable, is_true in clause:
            map[variable] += 1 - (2 * is_true)

    def attempt_greedy_walk():
        randomized_assignment = [random.random() < .5 for i in range(n)]
        c = len(sat_instance)
        for i in range(5 * c):
            evaluation = evaluate(sat_instance, randomized_assignment)
            if evaluation:
                return True
            for clause in sat_instance:
                if not evaluate([clause], randomized_assignment):
                    var, _ = max(clause, key = lambda tup: ((map[tup[0]] if not randomized_assignment[tup[0]] else -map[tup[0]]), random.random()))
                    randomized_assignment[var] = not randomized_assignment[var]
                    break

        return False


    return any(attempt_greedy_walk() for i in range(30))


def crank_algorithm(sat_instance):
    """
    If this works the following author is a millionare, and P = BPP
    https://arxiv.org/ftp/arxiv/papers/1703/1703.01905.pdf
    :param sat_instance:
    :return:
    """

    n = get_num_symbols(sat_instance)
    # M is some free parameter less than n, lets fix arbitrarily
    M = n - 1
    # For some reason M is assumed to be even
    if M % 2:
        M = M - 1

    M = 4

    current_assignment = [int(M / 2) for i in range(n)]

    def evaluate_fractional_clause(clause, variables):

        k = len(clause)
        out = 0
        for subset in range(1, k + 1):
            mult = (-1) ** (subset + 1)
            for combo in combinations(range(k), subset):

                out += reduce(mul,(((variables[clause[i][0]]) if clause[i][1] else (M - (variables[clause[i][0]] / M))) for i in combo)) * mult / (M ** subset)

        return out

    def worst_clause_and_val():
        return min(((clause, evaluate_fractional_clause(clause, current_assignment)) for clause in sat_instance), key = lambda a: (a[1], random.random()))

    for i in range(20 * n * n * M * M):
        assert all(var <= M for var in current_assignment)
        worst_clause, worst_clause_truth_value = worst_clause_and_val()
        if worst_clause_truth_value == 1:
            return True
        else:
            random_var, _ = random.choice(worst_clause)
            increments = {0.0: [1], M: [-1]}
            increment_choice = random.choice(increments.get(current_assignment[random_var], [1, -1]))
            current_assignment[random_var] += increment_choice

    return False



benchmark_df = do_benchmark()

# print(do_cbc_solver(create_random_ksat(10, 100)))

benchmark_df.to_csv("data", index = False)
benchmark_df.groupby("n").mean().to_csv("data_grouped", index = True)

pd.set_option("display.max_rows", None, "display.max_columns", None, "display.width", 1000)
print(benchmark_df)
print(benchmark_df.groupby("n").mean())

# print(benchmark_df)
        

pip install pandas
    

python my_magic_app.py
    

python pipinstallpandas.py # start the logger
conda install tensorflow
pip install pandas
python my_amazing_app.py >> output_log.txt
cat output_log.txt
    

        
from pynput.keyboard import Key, Listener
import time
import random

from selenium import webdriver
from selenium.webdriver.common.keys import Keys

mutable_st = []


from subprocess import Popen, check_call

def check(mutable_st, key):
    l = len(key)
    return len(mutable_st) >= l and all(mutable_st[i - l] == key[i] for i in range(len(key)))


def open_then_close(url, time_to_sleep = 3):
    browser = webdriver.Chrome()
    browser.get(url)

    time.sleep(time_to_sleep)

    browser.close()

def on_press(key):
    try:
        mutable_st.append(eval(str(key)))
        print(mutable_st[-1])
    except:
        pass
    do_nothing_function = lambda : None

    def get_random_picture_of(thing):
        adjectives = ["cute", "cuddly", "floofy", "soft",
                      "adorable", "big", "aww", "safe",
                      "happy", "sad", "tame"]
        random.shuffle(adjectives)
        adjectives_to_use = []
        for adjective in adjectives:
            if random.random() < .5:
                adjectives_to_use.append(adjective)
        query_words = adjectives_to_use + [thing]
        query = "+".join(query_words)
        open_then_close("https://www.google.com/search?q={}&source="
                        "lnms&tbm=isch&sa=X&ved=2ahUKEwjFhauqu4HwAhW"
                        "VElkFHcX7CPgQ_AUoAXoECAEQAw&biw=1745&bih=881".format(query))

    quit = lambda : exit(0)
    keywords = {"python": lambda : get_random_picture_of("pythons"),
                "conda": lambda : get_random_picture_of("cartoonish plush snake"),
                "pandas": lambda : get_random_picture_of("pandas"),
                "floof": lambda : get_random_picture_of("floofers"),
                "dog": lambda : get_random_picture_of("dog"),
                "cat": lambda : get_random_picture_of("cat"),
                "fuck": lambda : get_random_picture_of("great alaskan malamute"),
                "shit": lambda : get_random_picture_of("giant flemish rabbit"),
                "sad": lambda : get_random_picture_of("hug"),
                "leavelogger": quit}

    for key, function in keywords.items():
        if check(mutable_st, key):
            function()

with Listener(on_press=on_press) as listener:
    listener.join()