My Z3/Z3Py page

• Github Z3
• Github Z3 Wiki (links to resources)
• Stackoverflow labeled z3
• Stackoverflow labeled z3py
• SMT-LIB (SMT Logics)
• My Z3/Z3Py Github page: https://github.com/hakank/hakank/tree/master/z3

• makeIntVar(sol,name,min_val, max_val)
• makeIntVarVals(sol,name,vals)
• makeIntVars(sol,name,size, min_val, max_val)
• makeIntVector(sol,name,min_val, max_val)
• makeIntArray(sol,name,min_val, max_val)
• makeIntArrayVector(sol,name,min_val, max_val)
• makeRealVar(sol,name,min_val, max_val)
• makeRealVars(sol,name,size, min_val, max_val)
• makeRealVector(sol,name,min_val, max_val)
• getDifferentSolution(sol,mod,*params)
• getLessSolution(sol,mod,z)
• getGreaterSolution(sol,mod,z)
• evalArray(mod,a)
• print_grid(sol,mod,x,num_rows,num_cols)
• copyArray(sol,a1,name, min_val, max_val)
• copyArrayMatrix(sol,a1,name, rows, cols, min_val, max_val)

• all_different(sol,x)
• all_different_except_0(sol,x)
• element(sol,ix,x,v,n)
• element_matrix(sol,ix,jx,x,v,rows,cols)
• increasing(sol,x)
• decreasing(sol,x)
• count(sol, value, x, n)
• global_cardinality_count(sol, values, x, gcc)
• at_most(sol, v,x,max)
• at_least(sol, v,x,min)
• scalar_product(sol, a,x,product)
• product == scalar_product2(sol, a,x)
• circuit(sol,z,path,n)
• circuit2(sol,z,path,n) (doesn't require and Array as argument)
• inverse(sol,f,invf,n)
• maximum(sol,max,x)
• v == maximum2(sol,x)
• minimum(sol,min,x)
• v == minimum2(sol,x)
• abs(x)
• toNum(sol, t, s, base)
• subset_sum(sol, values, total)
• allowed_assignments(sol,t,allowed) (aka table, table_in)
• member_of(sol, e, v)
• no_overlap(sol, s1, d1, s2, d2)
• sliding_sum(sol, low, up, seq, x)
• bin_packing(sol,capacity, bins, weights)
• cumulative(sol, s, d, r, b,times_min,times_max1)
• global_contiguity(sol, x,start,end)
• regular(sol, x, Q, S, d, q0, F, x_len)
• regular2(sol, x, Q, S, d, q0, F, x_len) (doesn't use temporary Array)
• all_different_modulo(sol, x, m)
• among(sol, m, x, v)
• nvalue(sol, m, x, min_val,max_val)
• clique(sol, g, clique, card)
• all_min_dist(sol,min_dist, x, n)
• all_different_cst(sol, xs, cst)
• all_different_on_intersection(sol, x, y)
• all_different_pairs(sol, a, s)
• increasing_pairs(sol,a, s)
• decreasing_pairs(sol,a, s)
• pairs(sol, a, s)
• all_differ_from_at_least_k_pos(sol, k, x)
• all_differ_from_exact_k_pos(sol, k, vectors)
• all_differ_from_at_most_k_pos(sol, k, x)
• all_equal(sol,x)
• arith(sol, x, relop, val)
• arith_relop(sol, a, t, b)
• diffn(sol,x,y,dx,dy)
• argmax(sol,x,ix,max_val)
• argmin(sol,x,ix,min_val)

• 1_rm.py: 1RM calculations / Comparing Reps+Weights
• 3_jugs_mip.py: 3 jugs problem (aka water jugs problem), MIP modeling
• 3_jugs_regular.py: 3 jugs problem (aka water jugs problem), using regular constraint
• 3sum.py: 3SUM (Three Elements That Sum To Zero)
• 4x4_grid_equations.py: 4x4 Grid equation puzzle.
• 50_puzzle.py: Fifty puzzle (Martin Chlond)
• 5x5_puzzle.py: 5x5 puzzle (Five puzzle, Martin Chlond)
• a_puzzle.py: "A Puzzle", 8809=6,... (from God Plays Dice "A Puzzle")
• a_round_of_golf.py: A Round of Golf (Dell Logic Puzzles)
• abbots_puzzle.py: Abbot's puzzle (Dudeney)
• added_corner.py: Added corner puzzle
• age_changing.py: Age changing (Enigma 1224)
• ages.py: Ages problem ("How old are they?", Tony Hurlimann)
• agprice.py: Agricultural pricing (Williams)
• all_differ_from_at_least_k_pos.py: Example of global constraint all_different_from_at_least_k_pos, all_different_from_at_most_k_pos, all_different_from_exactly_k_pos
• all_different_cst.py: Example of global constraint all_different_cst
• all_different_except_0.py: Example of global constraint all_different_except_0
• all_different_modulo.py: Example of global constraint all_different_modulo
• all_different_on_intersection.py: Example of global constraint all_different_on_intersection
• all_different_pairs.py: Example of global constraint all_different_pairs
• all_equal.py: Example of global constraint all_equal
• all_intervals.py: All interval problem (CSPLib #7)
• all_min_dist.py: Example of global constraint all_min_dist
• all_partitions.py: All partitions
• alphametic.py: General alphametic solver (e.g. SEND+MORE=MONEY)
• among.py: Example of global constraint among
• appointment_scheduling.py: Appointment scheduling
• arch_friends.py: Arch friends puzzle (Dell Logic Puzzles)
• arch_friends.py: Archery puzzle (Sam Loyd)
• argmax.py: Example of global constraint argmax
• arith.py: Example of global constraint arith
• assignment.py: Some different assignment problems
• autoref.py: Autoref problem
• babysitting.py: Babysitting puzzle (Dell Logic Puzzles)
• balanced_brackets.py: Generating balanced brackets
• bales_of_hay.py: Bales of hay problem
• bananas.py: Bananas problem
• bin_packing.py: Bin packing
• birthday_coins.py: Tommy's Birthday Coins (L.H. Clarke, via Martin Chlond)
• bit_patterns.py: Bit patterns problem
• blending.py: Blending problem (mixed integer and real)
• book_buy.py: Book buy puzzle (M Kraitchik, via Martin Chlond)
• book_discount.py: Book discount puzzle (Poniachek, via Martin Chlond)
• bowls_and_oranges.py: Bowls and Oranges problem
• box.py: Designing a box (nonlinear real problem)
• breaking_news.py: Breaking news (Dell Logic Puzzles)
• broken_weights.py: Broken weights (a weighing problem)
• building_a_house.py: Scheduling problem: Building a house (OPL)
• bus_schedule.py: Bus scheduling problem (from Taha "Introduction to Operations Research")
• bus_scheduling_csplib.py: Bus driver scheduling problem (prob022 in CSPLib)
  Problem instances:
  • bus_scheduling_csplib/problems/c1
  • bus_scheduling_csplib/problems/c1a
  • bus_scheduling_csplib/problems/c2
  • bus_scheduling_csplib/problems/r1
  • bus_scheduling_csplib/problems/r1a
  • bus_scheduling_csplib/problems/r2
  • bus_scheduling_csplib/problems/r3
  • bus_scheduling_csplib/problems/r4
  • bus_scheduling_csplib/problems/r5
  • bus_scheduling_csplib/problems/r5a
  • bus_scheduling_csplib/problems/r5a
  • bus_scheduling_csplib/problems/t1
  • bus_scheduling_csplib/problems/t2
• calculus_d_enfer.py: Calculs d'enfer alphametic puzzle
• candies.py: Candies problem (HackerRank)
• capital_budget2.py: Capital budgeting (Winston)
• celsius_fahrenheit.py: Celsius - Fahrenheit conversion
• changepoint_detection.py: Changepoint detection
• circling_squares.py: Circling squares puzzle (Dudeney)
• circuit.py: Example of global constraint circuit
• clique.py: Example of global constraint clique
• coins2.py: Coins problem (Chlond)
• coins3.py: Coins problem
• coins_grid.py: Coins grid problem (Tony Hurlimann)
• coloring_ip.py: Map coloring (IP approach)
• combinatorial_auction2.py: Combinatorial auction
• contiguity_regular.py: Global contiguity using the global constraint regular
• costas_array.py: Costas array
• crew.py: Crew allocation problem (Gecode)
• crossword2.py: Simple crossword puzzle
• crypta.py: Cryptarithmetic puzzle
• crypto.py: Cryptarithmetic puzzle
• cumulative_tests.py: Some tests of the global constraint cumulative
• cur_num.py: Curious numbers (Dudeney)
• curious_set_of_integers.py: Curious set of integers (Martin Gardner)
• curve_fitting.py: Curve fitting, 3 approaches (Williams, GLPK)
• cyclohexane.py: Cyclohexane (non-linear reals)
• debruijn_binary.py: de Bruijn Sequences (both traditional and "arbitrary")
• devils_word.py: Devil's word (sum ASCII representation of a word to a specific sum, e.g. 666)
• diet.py: Simple diet (optimization) problem
• diffn_test.py: Test of global constraint diffn
• dinner.py: Dinner problem
• discrete_tomography.py: Discrete tomography
• divisible_by_9_through_1.py: Divisible by 1 to 9
• dog_cat_and_mouse.py: Dog, cat and mouse puzzle (Int version and Real version)
• einav_puzzle.py: Einav's puzzle
• eq10.py: Eq 10 benchmark
• eq20.py: Eq 20 benchmark
• exodus.py: Exodus puzzle (Dell Logic Puzzles)
• factorial.py: Factorial (reversible)
• fancy.py: Mr Greenguest's fancy dress puzzle
• fibonacci.py: Fibonacci (reversible)
• fill_a_pix.py: Fill-a-pix problem
• final_student.py: Final student puzzle (Chris Smith)
• finding_celebrities.py: Finding celebrities (Uwe Hoffmann)
• football.py: Football optimization problem (buying players)
• four_islands.py: Four Islands Puzzle (Dell Logic Puzzles)
• fraction_problem.py Fractions problem (Prolog benchmark)
• furniture_moving.py: Simple scheduling problem (Stuckey, Marriott)
• futoshiki.py: Futoshiki grid puzzle
• game_theory_taha.py: Game theory problem (Taha: OR)
• general_store.py: General Store alphametic puzzle
• geometric_puzzle.py: Geometric puzzle
• global_contiguity.py: Test of the global constraint global contiguity
• goal_programming1.py: Goal programming (Winston)
• golomb_ruler.py: Golomb Ruler
• grocery.py: Grocery problem (a.k.a. 7-11 problem)
• hamming_distance.py: Hamming distance
• heterosquare.py: Heterosquare
• hidato.py: Hidato
• hidato_function.py: Hidato using Function
• hidato_instance.py: Instances for the Hidato solvers
• hidato_table.py: Hidato using table constraint
• how_many_passengers_are_in_carriage_9.py: How many passengers are in carriage 9? (MindYourDecisions)
• huey_dewey_louie.py: Huey, Dewey, and Louie logical puzzle
• inverse.py: Global constraint inverse example
• isbn.py: Some explorations of ISBN13
• jobs_puzzle.py: Jobs puzzle
• just_forgotten.py: Just forgotten puzzle (Enigma 1517)
• k4p2_graceful_graph.py: K4P2 Graceful Graph
• kakuro.py: Kakuro grid puzzle
• kenken2.py: KenKen grid puzzle
• killer_sudoku.py: Killer Sudoku
• knapsack.py: Simple knapsack problem
• knapsack_problem.py: (Another) knapsack problem
• knapsack_investments.py: Investments problem (knapsack)
• labeled_dice.py: General solver for Labeled dice and Building Blocks problems
• langford.py: Langford's number problem (CSPLib #24), using Int Array
• langford2.py: Langford's number problem (CSPLib #24), using IntVector and element constraint
• latin_squares_diagonals.py: Latin squares with diagonals
• least_diff.py: Minimize the difference of ABCDE-FGHIJ where A..J are distinct integers
• least_square.py: Least square optimization problem (solving a fourth grade least square equation.)
• lecture_series.py: Lecture Series problem (Dell Logic Puzzles)
• lectures.py: Lectures problem (simple scheduling of lectures, from Biggs "Discrete Mathematics")
• magic_hexagon.py: Magic hexagon (CSPList #23)
• magic_sequence.py: Magic sequence (CSPLib #19)
• magic_square.py: Magic square
• magic_square2.py: Magic square alternative model
• magic_square_and_cards.py: Magic squares and cards (Martin Gardner)
• mamas_age.py: Mama's age problem
• map.py: Simple map coloring problem
• markov_chains_taha.py: : Markov chains (Taha)
• marathon2.py: : Marathon logic puzzle
• max_flow_taha.py: Max flow problem (Taha)
• max_flow_winston1.py: Max flow problem (Winston)
• maximal_fence.py: Maximal fence problem
• minesweeper.py: : Minesweeper solver
• monks_and_doors.py: Monks and doors problem
• mortgage.py: Mortgage calculation
• mortgage2.py: Mortgage calculation
• mr_smith.py: Mr Smith logic problem (IF Prolog)
• music_men.py: Music Men Puzzle (Dell Logic Puzzles)
• nadel.py: Nadel's construction problem (Rina Dechter "Constraint Processing")
• nadel_unsat_core.py: Nadel's construction problem (Rina Dechter "Constraint Processing"), this use unsat_core to get the minimal unsat core.
• nonogram_regular.py: Nonogram using the global constraint regular
  Instances:
  • nonogram_bear.py
  • nonogram_car.py
  • nonogram_castle.py
  • nonogram_crocodile.py
  • nonogram_difficult.py
  • nonogram_dragonfly.py
  • nonogram_gondola.py
  • nonogram_hard.py
  • nonogram_hen.py
  • nonogram_lambda.py
  • nonogram_n4.py
  • nonogram_n6.py
  • nonogram_nonunique.py
  • nonogram_p199.py
  • nonogram_p200.py
  • nonogram_ps.py
  • nonogram_soccer_player.py
  • nonogram_t2.py
• nontransitive_dice.py: Nontransitive dice
• nqueen.py: n-queen problem
• nqueen2.py: n-queen problem
• nqueen_array.py: n-queen problem (using Array)
• nqueen_boolean.py: n-queen problem (using Bool, AtMost/AtLeast)
• nqueen_intvector.py: n-queen problem (using IntVector)
• nqueen3.py: n-queen problem (MIP/SAT approach)
• number_of_days.py: Number of days (knapsack) problem
• nurse_rostering.py: Nurse rostering (using regular constraint)
• nvalue.py: Example of the global constraint nvalue
• olympic.py: Olympic logic puzzle (Prolog benchmark)
• organize_day.py: Organizing a day (very simple scheduling problem)
• ormat_game.py: Ormat game grid puzzle
• p_median.py: P-median problem (OPL)
• pandigital_numbers.py: Pandigital numbers
• perfect_square_sequence.py: Perfect square sequence
• pert.py: PERT problem
• photo_problem.py: Photo problem (from Mozart/Oz)
• pigeon_hole.py: Pigeon hole problem
• place_number_puzzle.py: Place number puzzle
• plan.py: Planning problem (GLPK)
• post_office_problem.py: Employment scheduling (from Wayne Winston "Operations Research")
• production.py: Simple production problem (OPL)
• pythagoras.py: Pythagoras problem
• quasigroup_completion.py: Quasigroup completions
• rabbits.py: Rabbits problem (Van Hentenryck, OPL book)
• read_test.py: Matching words of the form .*a.*.b*.c.*, .*b.*c.*d.*, etc (using Re's)
• regex.py: Generate all possible strings given a regular expression.
• relief_mission.py: Relief Mission (PuzzlOR)
• rogo2.py: Rogo grid puzzle
  Instances:
  • rogo_20110106.py
  • rogo_20110107.py
  • rogo_mike_trick.py
• rosenbrock.py: Rosenbrock function (nonlinear real)
• safe_cracking.py: Safe cracking (from Mozart/Oz)
• scheduling_speakers.py: Scheduling speakers (Rina Dechter "Constraint Processing")
• secret_santa.py: Secret Santa problem
• secret_santa2.py: Another Secret Santa problem
• send_more_money.py: SEND+MORE=MONEY
• send_more_money_any_base.py: SEND+MORE=MONEY in any base
• send_most_money.py: SEND+MOST=MONEY (optimizing MONEY)
• seseman.py: Seseman's Convent problem
• set_covering.py: Set covering (a couple of different problems)
• set_partition.py: Set partition problem
• seven_cups.py: Seven cups problem
• sicherman_dice.py: Sicherman's dice
• shifted_division.py: Shifted division
• shifted_division2.py: Shifted division, much faster and includes some analysis of 'interestingness' and number of solutions.
• shopping_with_delivery_costs.py: Shopping with delivery costs
• ski_assignment.py: Ski assignment puzzle
• sliding_sum.py: Example of global constraint sliding_sum
• spreadsheet.py: Simple spreadsheet
• steiner.py: Steiner triplets
• stable_marriage.py: Stable marriage problem
• strimko.py: Strimko Grid puzzle
  Instances:
  • strimko2_002.py
  • strimko2_067.py
  • strimko2_068.py
  • strimko2_069.py
  • strimko2_070.py
• stigler.py: Original Stigler's 1939 diet problem (GLPK)
• stuckey_seesaw.py: Balancing on a seesaw (Stuckey, Marriott: "Programming with Constraints")
• stuckey_finite_element.py: Finite element, Temperature in a grid (Stuckey, Marriott: "Programming with Constraints")
• subset_sum.py: Subset sum problem (from Katta G Murty)
• sudoku.py: Sudoku
• sudoku_ip.py: Sudoku using a (pseudo) boolean approach using a MIP inspired encoding.
• survo_puzzle.py: Survo puzzle
• talisman_square.py: Talisman square
• timpkin.py: : Mrs Timpin's Age (Dudeney)
• toNum.py: Example of constraint toNum (converting between a variable and an array of integers)
• tourist_site_competition.py: Tourist Site Competition
• traffic_lights.py: Traffic lights problem (CSPLib #16)
• transp.py: Transport problem (GLPK)
• tsp_circuit.py: TSP (using circuit constraint)
• tunapalooza.py: Tunapalooza problem (Dell Logic Puzzles)
• twin_letters.py: Twin letters
• two_circles.py: Two circles (Chris Smith)
• volsay.py: Volsay problem
• voltage_divider.py: Voltage divider (Stuckey et.al)
• warehouse_scheduling.py: Warehouse scheduling
• weak_hashes.py: Discovering password from a (weak) hash function
• who_killed_agatha.py: Who killed Agatha? (The Dreadsbury Mansion Murder Mystery)
• who_killed_agatha2.py: Who killed Agatha? (The Dreadsbury Mansion Murder Mystery), a "pure logic" approach (using EnumSort)
• who_killed_agatha3.py: Who killed Agatha? (The Dreadsbury Mansion Murder Mystery), using Function instead of Array (as in who_killed_agatha.py)
• word_square.py: Word square
• word_square2.py: Word square without Arrays (faster)
• wordle.py: Wordle solver: using String constraints, and two faster plain Python variants
• working_together.py: Working together (MindYourDecisions)
• xkcd.py: Solving the xkcd "knapsack" (or subset-sum) problem from http://xkcd.com/287/
• young_tableaux.py: Young tableaux and partitions
• z3_utils_hakank.py (See comment above.)
• zebra.py: Zebra puzzle