feat: Merge SMT Terms in one class (#5254)

This pr brings major changes in symbolic terms usage.

### STerm

A new class that is merged from `FFTerm` and `FFITerm` classes. Now you
can use `FFTerm` or `FFITerm` by providing a `TermType::FFTerm` or
`TermType::FFITerm` to `STerm` constructor.

All the operations are now stored in `unordered_map<OpType, cvc5::Kind>
operations`. e.g. if the type is `FFTerm`, then `operations[OpType::ADD]
= cvc5::Kind::FINITE_FIELD_ADD`, and `operations[OpType::ADD] =
cvc5::Kind::ADD` for `FFITerm`

Also now you can use new `BVTerm` type. It can be used to solve
constraints with lots of bitwise operations. However, it can be used
only once all the optimizations are added. You simply can't use it to
simulate finite field operations and it's not really optimal.


Symbolic variables can be initialized using new functions `FFVar`,
`FFIVar` and `BVVar`

### Solver

Added `bv_sort` member

Added bitvector operations parser to `stringify_term`

### Circuit

No more templates. All the circuit methods are moved to .cpp file

Fixes:
- range constraint is now made to be `<= 2^n - 1` instead of `< 2^n`
- changed `xor_gate` to `logic_gate` in `info` function
- Removed setting optimized variables to zero, since it didn't affect
anything except polluted output
- Restored public_variables initialization. It was deleted some time
ago. I don't know why.

### Utils

- `smt_timer` now has `bool mins` param, that tells in what format to
output elapsed time

---------

Co-authored-by: Innokentii Sennovskii <[email protected]>

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

@@ -3,9 +3,11 @@
 #include <string>
 
 #include "barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp"
+#include "barretenberg/stdlib/primitives/field/field.hpp"
+#include "barretenberg/stdlib/primitives/uint/uint.hpp"
+
 #include "barretenberg/smt_verification/circuit/circuit.hpp"
 #include "barretenberg/smt_verification/util/smt_util.hpp"
-#include "barretenberg/stdlib/primitives/field/field.hpp"
 
 #include <gtest/gtest.h>
 
@@ -19,6 +21,7 @@ auto& engine = numeric::get_debug_randomness();
 using field_t = stdlib::field_t<StandardCircuitBuilder>;
 using witness_t = stdlib::witness_t<StandardCircuitBuilder>;
 using pub_witness_t = stdlib::public_witness_t<StandardCircuitBuilder>;
+using uint_ct = stdlib::uint32<StandardCircuitBuilder>;
 
 TEST(circuit, assert_equal)
 {
@@ -49,7 +52,7 @@ TEST(circuit, assert_equal)
     auto buf = builder.export_circuit();
     CircuitSchema circuit_info = unpack_from_buffer(buf);
     Solver s(circuit_info.modulus);
-    Circuit<FFTerm> circuit(circuit_info, &s);
+    Circuit circuit(circuit_info, &s, TermType::FFTerm);
 
     ASSERT_EQ(circuit[k.get_witness_index()].term, circuit["c"].term);
     ASSERT_EQ(circuit[d.get_witness_index()].term, circuit["a"].term);
@@ -59,6 +62,23 @@ TEST(circuit, assert_equal)
     ASSERT_EQ(circuit[i.get_witness_index()].term, circuit[j.get_witness_index()].term);
 }
 
+TEST(circuit, cached_subcircuits)
+{
+    StandardCircuitBuilder builder = StandardCircuitBuilder();
+    field_t a(witness_t(&builder, fr::zero()));
+    builder.set_variable_name(a.get_witness_index(), "a");
+    a.create_range_constraint(5);
+    field_t b(witness_t(&builder, fr::zero()));
+    b.create_range_constraint(5);
+    builder.set_variable_name(b.get_witness_index(), "b");
+
+    auto buf = builder.export_circuit();
+    CircuitSchema circuit_info = unpack_from_buffer(buf);
+    Solver s(circuit_info.modulus);
+    Circuit circuit(circuit_info, &s, TermType::FFITerm);
+    s.print_assertions();
+}
+
 TEST(circuit, range_relaxation_assertions)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
@@ -75,7 +95,7 @@ TEST(circuit, range_relaxation_assertions)
     auto buf = builder.export_circuit();
     CircuitSchema circuit_info = unpack_from_buffer(buf);
     Solver s(circuit_info.modulus);
-    Circuit<FFITerm> circuit(circuit_info, &s);
+    Circuit circuit(circuit_info, &s, TermType::FFITerm);
 
     s.print_assertions();
 }
@@ -90,25 +110,42 @@ TEST(circuit, range_relaxation)
         auto buf = builder.export_circuit();
         CircuitSchema circuit_info = unpack_from_buffer(buf);
         Solver s(circuit_info.modulus);
-        Circuit<FFITerm> circuit(circuit_info, &s);
+        Circuit circuit(circuit_info, &s, TermType::FFITerm);
     }
 }
 
-TEST(circuit, cached_subcircuits)
+TEST(circuit, xor_relaxation_assertions)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
-    field_t a(witness_t(&builder, fr::zero()));
+    uint_ct a(witness_t(&builder, static_cast<uint32_t>(fr(120))));
+    uint_ct b(witness_t(&builder, static_cast<uint32_t>(fr(120))));
+    uint_ct c = a ^ b;
     builder.set_variable_name(a.get_witness_index(), "a");
-    a.create_range_constraint(5);
-    field_t b(witness_t(&builder, fr::zero()));
-    b.create_range_constraint(5);
     builder.set_variable_name(b.get_witness_index(), "b");
+    builder.set_variable_name(c.get_witness_index(), "c");
 
     auto buf = builder.export_circuit();
     CircuitSchema circuit_info = unpack_from_buffer(buf);
-    Solver s(circuit_info.modulus);
-    Circuit<FFITerm> circuit(circuit_info, &s);
+    Solver s(circuit_info.modulus, default_solver_config, 16, 32);
+    Circuit circuit(circuit_info, &s, TermType::BVTerm);
+
     s.print_assertions();
 }
 
-// TODO(alex): check xor relaxations after bivector is here
+TEST(circuit, and_relaxation_assertions)
+{
+    StandardCircuitBuilder builder = StandardCircuitBuilder();
+    uint_ct a(witness_t(&builder, static_cast<uint32_t>(fr(120))));
+    uint_ct b(witness_t(&builder, static_cast<uint32_t>(fr(120))));
+    uint_ct c = a & b;
+    builder.set_variable_name(a.get_witness_index(), "a");
+    builder.set_variable_name(b.get_witness_index(), "b");
+    builder.set_variable_name(c.get_witness_index(), "c");
+
+    auto buf = builder.export_circuit();
+    CircuitSchema circuit_info = unpack_from_buffer(buf);
+    Solver s(circuit_info.modulus, default_solver_config, 16, 32);
+    Circuit circuit(circuit_info, &s, TermType::BVTerm);
+
+    s.print_assertions();
+}