feat: Update SMT Circuit class and add gate relaxation functionality (#…

…5176)

This pr adds gate relaxation functionality to Circuit class. It
substitutes subcircuits with their "arithmetic" equivalents.
Also it adds `util` directory.

### Util

- `default_model` and `default_model_single` will output pretty
formatted result of Solver work
- `smt_timer` will measure the amount of time that it took to solve
something
- `base4` provides you with accumulators and base4 decomposition of a
number

### Terms

- Added `isBitVector()` method that foreshadows future `BitVector` api

### Subcircuits

- functions in `subcircuits.cpp` now return new structure:
`CircuitProps`.
- `CircuitProps` consists of 
    -  `start_gate` indicates where to start subcircuit comparison
    - `num_gates` tells a pure subcircuit size
- `idxs` and and `gate_idxs` indicate where to search for the values
that are used in optimized operation

Also added tests to confirm that all the indices 

### Circuit

- Added members `bool optimizations` and `map<uint32_t, bool> optimized`
to keep track of optimized out variables that should not be considered
by solver
- Added functions `handle_range_constraint`, `handle_logic_constraint`.
They perform binary search to indicate the bit_length of specific
operation and apply optimization to subcircuit
- Added cache for subcircuits to avoid recomputing them each time

Tests check that

- all the `assert_equal`'d variables handled properly during circuit
initialization
- `range_constraints` are optimized properly

---------

Co-authored-by: Innokentii Sennovskii <isennovskiy@gmail.com>

barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.cpp

@@ -25,8 +25,9 @@ std::pair<Circuit<FF>, Circuit<FF>> unique_witness_ext(CircuitSchema& circuit_in
                                                        const std::vector<std::string>& equal_at_the_same_time,
                                                        const std::vector<std::string>& not_equal_at_the_same_time)
 {
-    Circuit<FF> c1(circuit_info, s, "circuit1");
-    Circuit<FF> c2(circuit_info, s, "circuit2");
+    // TODO(alex): set optimizations to be true once they are confirmed
+    Circuit<FF> c1(circuit_info, s, "circuit1", false);
+    Circuit<FF> c2(circuit_info, s, "circuit2", false);
 
     for (const auto& term : equal) {
         c1[term] == c2[term];
@@ -95,8 +96,9 @@ std::pair<Circuit<FF>, Circuit<FF>> unique_witness(CircuitSchema& circuit_info,
                                                    Solver* s,
                                                    const std::vector<std::string>& equal)
 {
-    Circuit<FF> c1(circuit_info, s, "circuit1");
-    Circuit<FF> c2(circuit_info, s, "circuit2");
+    // TODO(alex): set optimizations to be true once they are confirmed
+    Circuit<FF> c1(circuit_info, s, "circuit1", false);
+    Circuit<FF> c2(circuit_info, s, "circuit2", false);
 
     for (const auto& term : equal) {
         c1[term] == c2[term];
@@ -108,6 +110,9 @@ std::pair<Circuit<FF>, Circuit<FF>> unique_witness(CircuitSchema& circuit_info,
         if (std::find(equal.begin(), equal.end(), std::string(c1.variable_names[i])) != equal.end()) {
             continue;
         }
+        if (c1.optimized[i]) {
+            continue;
+        }
         Bool tmp = Bool(c1[i]) != Bool(c2[i]);
         neqs.push_back(tmp);
     }