feat: Updating an SMT solver class

barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp

@@ -41,8 +41,6 @@ using fq_ct = bn254::BaseField;
 using public_witness_ct = bn254::public_witness_ct;
 using witness_ct = bn254::witness_ct;
 
-SolverConfiguration config = { true, 0 };
-
 msgpack::sbuffer create_circuit(bool pub_ab, bool ab)
 {
     StandardCircuitBuilder builder = StandardCircuitBuilder();
@@ -182,7 +180,7 @@ TEST(bigfield, multiplication_equal)
     auto buf = create_circuit(public_a_b, a_neq_b);
 
     CircuitSchema circuit_info = unpack_from_buffer(buf);
-    Solver s(circuit_info.modulus, config);
+    Solver s(circuit_info.modulus);
     Circuit<FFTerm> circuit(circuit_info, &s);
     std::vector<FFTerm> ev = correct_result(circuit, &s);
 
@@ -207,7 +205,7 @@ TEST(bigfield, unique_square)
 
     CircuitSchema circuit_info = unpack_from_buffer(buf);
 
-    Solver s(circuit_info.modulus, config);
+    Solver s(circuit_info.modulus);
 
     std::pair<Circuit<FFTerm>, Circuit<FFTerm>> cs =
         unique_witness<FFTerm>(circuit_info,

barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp

@@ -34,7 +34,7 @@ TEST(circuit_verification, multiplication_true)
     auto buf = builder.export_circuit();
 
     smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf);
-    smt_solver::Solver s(circuit_info.modulus, { true, 0 });
+    smt_solver::Solver s(circuit_info.modulus);
     smt_circuit::Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
     smt_terms::FFTerm a1 = circuit["a"];
     smt_terms::FFTerm b1 = circuit["b"];
@@ -65,7 +65,7 @@ TEST(circuit_verification, multiplication_true_kind)
     auto buf = builder.export_circuit();
 
     smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf);
-    smt_solver::Solver s(circuit_info.modulus, { true, 0 });
+    smt_solver::Solver s(circuit_info.modulus);
     smt_circuit::Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
     smt_terms::FFTerm a1 = circuit["a"];
     smt_terms::FFTerm b1 = circuit["b"];
@@ -96,7 +96,7 @@ TEST(circuit_verification, multiplication_false)
     auto buf = builder.export_circuit();
 
     smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf);
-    smt_solver::Solver s(circuit_info.modulus, { true, 0 });
+    smt_solver::Solver s(circuit_info.modulus);
     smt_circuit::Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
 
     smt_terms::FFTerm a1 = circuit["a"];
@@ -139,7 +139,7 @@ TEST(circuit_verifiaction, unique_witness)
     auto buf = builder.export_circuit();
 
     smt_circuit::CircuitSchema circuit_info = smt_circuit::unpack_from_buffer(buf);
-    smt_solver::Solver s(circuit_info.modulus, { true, 0 });
+    smt_solver::Solver s(circuit_info.modulus);
 
     std::pair<smt_circuit::Circuit<smt_terms::FFTerm>, smt_circuit::Circuit<smt_terms::FFTerm>> cirs =
         smt_circuit::unique_witness<smt_terms::FFTerm>(circuit_info, &s, { "ev" }, { "z" });
@@ -156,7 +156,7 @@ using namespace smt_terms;
 
 TEST(solver_use_case, solver)
 {
-    Solver s("11", { true, 0 }, 10);
+    Solver s("11", default_solver_config, 10);
     FFTerm x = FFTerm::Var("x", &s);
     FFTerm y = FFTerm::Var("y", &s);
 

barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp

@@ -120,7 +120,7 @@ TEST(polynomial_evaluation, correct)
 
     CircuitSchema circuit_info = unpack_from_buffer(buf);
 
-    Solver s(circuit_info.modulus, { true, 0 });
+    Solver s(circuit_info.modulus);
     Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
     FFTerm ev = polynomial_evaluation(circuit, n, true);
 
@@ -143,7 +143,7 @@ TEST(polynomial_evaluation, incorrect)
 
     CircuitSchema circuit_info = unpack_from_buffer(buf);
 
-    Solver s(circuit_info.modulus, { true, 0 });
+    Solver s(circuit_info.modulus);
     Circuit<smt_terms::FFTerm> circuit(circuit_info, &s);
     FFTerm ev = polynomial_evaluation(circuit, n, false);
 

barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp

@@ -11,13 +11,22 @@ namespace smt_solver {
 bool Solver::check()
 {
     cvc5::Result result = this->s.checkSat();
-    this->res = result.isSat();
     this->checked = true;
+    this->cvc_result = result;
+
+    if (result.isUnknown()) {
+        info("Unknown Result");
+    }
+    this->res = result.isSat();
     return this->res;
 }
 
 /**
  * If the system is solvable, extract the values for the given symbolic variables.
+ * Specify the map to retrieve the values you need using the keys that are convenient for you.
+ *
+ * e.g. {"a": a}, where a is a symbolic term with the name "var78".
+ * The return map will be {"a", value_of_a}
  *
  * @param terms A map containing pairs (name, symbolic term).
  * @return A map containing pairs (name, value).
@@ -32,9 +41,166 @@ std::unordered_map<std::string, std::string> Solver::model(std::unordered_map<st
     }
     std::unordered_map<std::string, std::string> resulting_model;
     for (auto& term : terms) {
-        std::string str_val = this->s.getValue(term.second).getFiniteFieldValue();
+        cvc5::Term val = this->s.getValue(term.second);
+        std::string str_val;
+        if (val.isIntegerValue()) {
+            str_val = val.getIntegerValue();
+        } else if (val.isFiniteFieldValue()) {
+            str_val = val.getFiniteFieldValue();
+        } else {
+            throw std::invalid_argument("Expected Integer or FiniteField sorts. Got: " + val.getSort().toString());
+        }
         resulting_model.insert({ term.first, str_val });
     }
     return resulting_model;
 }
+
+/**
+ * If the system is solvable, extract the values for the given symbolic variables.
+ * The return map will contain the resulting values, which are available by the
+ * names of the corresponding symboli variable.
+ *
+ * e.g. if the input vector is {a} and a is a term with name var78,
+ * it will return {"var78": value_of_var78}
+ *
+ * @param terms A vector containing symbolic terms.
+ * @return A map containing pairs (variable name, value).
+ * */
+std::unordered_map<std::string, std::string> Solver::model(std::vector<cvc5::Term>& terms) const
+{
+    if (!this->checked) {
+        throw std::length_error("Haven't checked yet");
+    }
+    if (!this->res) {
+        throw std::length_error("There's no solution");
+    }
+    std::unordered_map<std::string, std::string> resulting_model;
+    for (auto& term : terms) {
+        cvc5::Term val = this->s.getValue(term);
+        std::string str_val;
+        if (val.isIntegerValue()) {
+            str_val = val.getIntegerValue();
+        } else if (val.isFiniteFieldValue()) {
+            str_val = val.getFiniteFieldValue();
+        } else {
+            throw std::invalid_argument("Expected Integer or FiniteField sorts. Got: " + val.getSort().toString());
+        }
+        resulting_model.insert({ term.toString(), str_val });
+    }
+    return resulting_model;
+}
+
+/**
+ * A simple recursive function that converts native smt language
+ * to somewhat readable by humans.
+ *
+ * e.g. converts
+ * (or (= a0 #b0000000000) (= a0 #b0000000001)) to ((a0 == 0) || (a0 == 1))
+ * (= (* (+ a b) c) 10) to ((a + b) * c) == 10
+ *
+ * @param term cvc5 term.
+ * @return Parsed term.
+ * */
+std::string stringify_term(const cvc5::Term& term, bool parenthesis)
+{
+    if (term.getKind() == cvc5::Kind::CONSTANT) {
+        return term.toString();
+    }
+    if (term.getKind() == cvc5::Kind::CONST_FINITE_FIELD) {
+        return term.getFiniteFieldValue();
+    }
+    if (term.getKind() == cvc5::Kind::CONST_INTEGER) {
+        return term.getIntegerValue();
+    }
+    if (term.getKind() == cvc5::Kind::CONST_BOOLEAN) {
+        std::vector<std::string> bool_res = { "false", "true" };
+        return bool_res[static_cast<size_t>(term.getBooleanValue())];
+    }
+
+    std::string res;
+    std::string op;
+    bool child_parenthesis = true;
+    switch (term.getKind()) {
+    case cvc5::Kind::ADD:
+    case cvc5::Kind::FINITE_FIELD_ADD:
+        op = " + ";
+        child_parenthesis = false;
+        break;
+    case cvc5::Kind::SUB:
+        op = " - ";
+        child_parenthesis = false;
+        break;
+    case cvc5::Kind::NEG:
+    case cvc5::Kind::FINITE_FIELD_NEG:
+        res = "-";
+        break;
+    case cvc5::Kind::MULT:
+    case cvc5::Kind::FINITE_FIELD_MULT:
+        op = " * ";
+        break;
+    case cvc5::Kind::EQUAL:
+        op = " == ";
+        child_parenthesis = false;
+        break;
+    case cvc5::Kind::LT:
+        op = " < ";
+        break;
+    case cvc5::Kind::GT:
+        op = " > ";
+        break;
+    case cvc5::Kind::LEQ:
+        op = " <= ";
+        break;
+    case cvc5::Kind::GEQ:
+        op = " >= ";
+        break;
+    case cvc5::Kind::XOR:
+        op = " ^ ";
+        break;
+    case cvc5::Kind::OR:
+        op = " || ";
+        break;
+    case cvc5::Kind::AND:
+        op = " && ";
+        break;
+    case cvc5::Kind::NOT:
+        res = "!";
+        break;
+    case cvc5::Kind::INTS_MODULUS:
+        op = " % ";
+        parenthesis = true;
+        break;
+    default:
+        info("Invalid operand :", term.getKind());
+        break;
+    }
+
+    size_t i = 0;
+    cvc5::Term child;
+    for (const auto& t : term) {
+        if (i == term.getNumChildren() - 1) {
+            child = t;
+            break;
+        }
+        res += stringify_term(t, child_parenthesis) + op;
+        i += 1;
+    }
+
+    res = res + stringify_term(child, child_parenthesis);
+    if (parenthesis) {
+        return "(" + res + ")";
+    }
+    return res;
+}
+
+/**
+ * Output assertions in human readable format.
+ *
+ * */
+void Solver::print_assertions() const
+{
+    for (auto& t : this->s.getAssertions()) {
+        info(stringify_term(t));
+    }
+}
 }; // namespace smt_solver