Least Change

exercises/practice/least_change/.docs/instructions.md

@@ -0,0 +1,11 @@
+#Instructions
+Determine the fewest number of coins to be given to a customer such
+that the sum of the coins' value would equal the correct amount of change.
+
+The first parameter for your function is coins, an array of integer coin values.  The second parameter is target, the 
+value we want to find the least amount of coins to add up to. 
+Your function should return a Z3 model with the variables named after the coin values, and include a variable of the number of coins in the solution as min_coins.
+
+## Examples
+- coins = [1, 5, 10, 21, 25] and target = 63 should return a model that looks like [10 = 0, 25 = 0, 21 = 3, 5 = 0, min_coins = 3, 1 = 0].
+- coins = [2, 5, 10, 20, 50] and target = 21 should return a model that looks like [10 = 1, 50 = 0, 2 = 3, 20 = 0, 5 = 1, min_coins = 5].

exercises/practice/least_change/.meta/config.json

@@ -0,0 +1,21 @@
+{
+  "blurb": "A mathematical exercise. Implement a function to calculate the least amount of coins from a given set that add up to a target value",
+  "authors": [
+    "JimmyQuenichet"
+  ],
+  "contributors": [
+  ],
+  "files": {
+    "solution": [
+      "least_change.py"
+    ],
+    "test": [
+      "least_change_test.py"
+    ],
+    "example": [
+      ".meta/least_change_example.py"
+    ]
+  },
+  "source": "This is an exercise to introduce users to interacting with numbers and models in Z3",
+  "source_url": "https://en.wikipedia.org/wiki/Change-making_problem"
+}

exercises/practice/least_change/.meta/least_change_example.py

@@ -0,0 +1,31 @@
+from z3 import *
+
+def least_change(coins, target):
+    s = Optimize()
+    coin_var = []
+    equation_1 = IntVal(0)
+    equation_2 = IntVal(0)
+    min_coins = Int("min_coins")
+
+    # Fill in the solver with the necessary constraints
+    for i in range(len(coins)):
+        coin_var.append(Int(str(coins[i])))
+        s.add(coin_var[i] >= 0)
+        equation_1 += coins[i] * coin_var[i]
+        equation_2 += coin_var[i]
+
+    s.add(equation_1 == target,
+          equation_2 == min_coins,
+          min_coins > 0,
+          )
+
+    s.minimize(min_coins)
+
+    if s.check() == sat:
+        return s.model()
+    else:
+        return None
+
+if __name__ == "__main__":
+    s = least_change([1, 5, 10, 25, 100], 15)
+    print(s)

exercises/practice/least_change/least_change.py

@@ -0,0 +1,27 @@
+from z3 import *
+
+def least_change(coins, target):
+    s = Optimize()
+    coin_var = []
+    equation_1 = IntVal(0)
+    equation_2 = IntVal(0)
+    min_coins = Int("min_coins")
+
+    # Fill in the solver with the equations
+    for i in range(len(coins)):
+        coin_var.append(Int(str(coins[i])))
+        s.add(coin_var[i] >= 0)
+        equation_1 += coins[i] * coin_var[i]
+        equation_2 += coin_var[i]
+
+    s.add(equation_1 == target,
+          equation_2 == min_coins,
+          min_coins > 0,
+          )
+
+    s.minimize(min_coins)
+
+    if s.check() == sat:
+        return s.model()
+    else:
+        return None

exercises/practice/least_change/least_change_test.py

@@ -0,0 +1,49 @@
+import unittest
+from z3 import *
+from .least_change import *
+
+# Tests adapted from https://github.com/exercism/python/blob/main/exercises/practice/change/change_test.py
+
+class ChangeTest(unittest.TestCase):
+    def test_single_coin_change(self):
+        self.assertEqual(str(least_change([1, 5, 10, 25, 100], 25)), "[10 = 0, 25 = 1, 100 = 0, 5 = 0, min_coins = 1, "
+                                                                     "1 = 0]")
+
+    def test_multiple_coin_change(self):
+        self.assertEqual(str(least_change([1, 5, 10, 25, 100], 15)), "[10 = 1, 25 = 0, 100 = 0, 5 = 1, min_coins = 2, 1 = 0]")
+
+    def test_change_with_lilliputian_coins(self):
+        self.assertEqual(str(least_change([1, 4, 15, 20, 50], 23)), "[15 = 1, 4 = 2, 20 = 0, 50 = 0, min_coins = 3, "
+                                                                    "1 = 0]")
+
+    def test_change_with_lower_elbonia_coins(self):
+        self.assertEqual(str(least_change([1, 5, 10, 21, 25], 63)), "[5 = 0, 21 = 3, 25 = 0, 10 = 0, min_coins = 3, "
+                                                                    "1 = 0]")
+
+    def test_large_target_values(self):
+        self.assertEqual(str(least_change([1, 2, 5, 10, 20, 50, 100], 999)).replace('\n', ''), "[5 = 1, 50 = 1, 100 = "
+                                                                                               "9, 2 = 2, 20 = 2, "
+                                                                                               "10 = 0, min_coins = "
+                                                                                               "15, 1 = 0]")
+
+    def test_possible_change_without_unit_coins_available(self):
+        self.assertEqual(str(least_change([2, 5, 10, 20, 50], 21)), "[10 = 1, 50 = 0, 2 = 3, 20 = 0, 5 = 1, min_coins "
+                                                                    "= 5]")
+
+    def test_another_possible_change_without_unit_coins_available(self):
+        self.assertEqual(str(least_change([4, 5], 27)), "[4 = 3, 5 = 3, min_coins = 6]")
+
+    def test_no_coins_make_0_change(self):
+        self.assertEqual(least_change([1, 5, 10, 21, 25], 0), None)
+
+    def test_for_change_smaller_than_the_smallest_of_coins(self):
+        self.assertEqual(least_change([5, 10], 3), None)
+
+    def test_if_no_combination_can_add_up_to_target(self):
+        self.assertEqual(least_change([5, 10], 94), None)
+
+    def test_cannot_find_negative_change_values(self):
+        self.assertEqual(least_change([1, 2, 5], -5), None)
+
+if __name__ == "__main__":
+    unittest.main()

exercises/practice/propositional-logic/.docs/instructions.md

@@ -6,7 +6,6 @@ recreate the following properties:
 1. A & B == (A' | B')' (DeMorgan's Law)
 2. [A -> (A -> B)] -> (A -> B)
 3. A & (B' -> A') -> B
-
-The function should return the three theorems written in Z3 notation.  
+
 Use the prove() function to confirm the accuracy of your theorems.  
 Return the three theorems, in order, at the end of the function.