diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp index 1f1abe570e2f..330340e3505e 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_bigfield.test.cpp +++ b/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 circuit(circuit_info, &s); std::vector 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> cs = unique_witness(circuit_info, diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp index ae74b2681bc5..e62f94195e11 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/smt_examples.test.cpp @@ -35,7 +35,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 circuit(circuit_info, &s); smt_terms::FFTerm a1 = circuit["a"]; smt_terms::FFTerm b1 = circuit["b"]; @@ -66,7 +66,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 circuit(circuit_info, &s); smt_terms::FFTerm a1 = circuit["a"]; smt_terms::FFTerm b1 = circuit["b"]; @@ -97,7 +97,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 circuit(circuit_info, &s); smt_terms::FFTerm a1 = circuit["a"]; @@ -140,7 +140,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> cirs = smt_circuit::unique_witness(circuit_info, &s, { "ev" }, { "z" }); @@ -157,7 +157,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); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/smt_intmod.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/smt_intmod.test.cpp deleted file mode 100644 index 7c98768ea895..000000000000 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_intmod.test.cpp +++ /dev/null @@ -1,21 +0,0 @@ -#include "barretenberg/smt_verification/circuit/circuit.hpp" -#include -#include - -// TODO(alex): more tests - -TEST(integer_mod, basic_arithmetic) -{ - smt_solver::Solver s("101", { true, 0 }, 10); - - smt_terms::FFITerm x = smt_terms::FFITerm::Var("x", &s); - smt_terms::FFITerm y = smt_terms::FFITerm::Var("y", &s); - smt_terms::FFITerm z = smt_terms::FFITerm::Const("79", &s); - - (x * y) == z; - info(s.check()); - - std::string xval = s.s.getValue(x.term).getIntegerValue(); - std::string yval = s.s.getValue(y.term).getIntegerValue(); - info(xval, " ", yval); -} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp index 3e15583a71ae..b19e52089385 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/smt_polynomials.test.cpp +++ b/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 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 circuit(circuit_info, &s); FFTerm ev = polynomial_evaluation(circuit, n, false); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp index 4eca2d5c3ce1..6a3a369a4e93 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp +++ b/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 Solver::model(std::unordered_map 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 symbolic 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 Solver::model(std::vector& 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 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 bool_res = { "false", "true" }; + return bool_res[static_cast(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 diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp index 1126a896794a..e2bc854c67fa 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -5,22 +5,29 @@ #include #include "barretenberg/ecc/curves/bn254/fr.hpp" - namespace smt_solver { /** * @brief Solver configuration * - * @param produce_model tells the solver to actually compute the values of the variables in SAT case. - * @param timeout tells the solver to stop trying after `timeout` msecs. + * @param produce_model tells solver to actually compute the values of the variables in SAT case. + * @param timeout tells solver to stop trying after `timeout` msecs. + * @param debug set verbosity of cvc5: 0, 1, 2. * - * @todo TODO(alex): more cvc5 options. + * @param ff_disjunctive_bit tells solver to change all ((x = 0) | (x = 1)) to x*x = x. + * @param ff_solver tells solver which finite field solver to use: "gb", "split". */ struct SolverConfiguration { - bool produce_model; + bool produce_models; uint64_t timeout; + uint32_t debug; + + bool ff_disjunctive_bit; + std::string ff_solver; }; +const SolverConfiguration default_solver_config = { true, 0, 0, false, "" }; + /** * @brief Class for the solver. * @@ -34,18 +41,49 @@ class Solver { cvc5::Sort fp; std::string modulus; // modulus in base 10 bool res = false; + cvc5::Result cvc_result; bool checked = false; - explicit Solver(const std::string& modulus, const SolverConfiguration& config = { false, 0 }, uint32_t base = 16) + explicit Solver(const std::string& modulus, + const SolverConfiguration& config = default_solver_config, + uint32_t base = 16) { this->fp = s.mkFiniteFieldSort(modulus, base); this->modulus = fp.getFiniteFieldSize(); - if (config.produce_model) { + if (config.produce_models) { s.setOption("produce-models", "true"); } if (config.timeout > 0) { s.setOption("tlimit-per", std::to_string(config.timeout)); } + if (config.debug >= 1) { + s.setOption("verbosity", "5"); + } + if (config.debug >= 2) { + s.setOption("output", "learned-lits"); + s.setOption("output", "subs"); + s.setOption("output", "post-asserts"); + s.setOption("output", "trusted-proof-steps"); + s.setOption("output", "deep-restart"); + } + + // Can be useful when split-gb is used as ff-solver. + // Cause bit constraints are part of the split-gb optimization + // and without them it will probably perform less efficient + // TODO(alex): test this `probably` after finishing the pr sequence + if (config.ff_disjunctive_bit) { + s.setOption("ff-disjunctive-bit", "true"); + } + // split-gb is an updated version of gb ff-solver + // It basically SPLITS the polynomials in the system into subsets + // and computes a Groebner basis for each of them. + // According to the benchmarks, the new decision process in split-gb + // brings a significant boost in solver performance + if (!config.ff_solver.empty()) { + s.setOption("ff-solver", config.ff_solver); + } + + s.setOption("output", "incomplete"); } Solver(const Solver& other) = delete; @@ -55,7 +93,7 @@ class Solver { bool check(); - [[nodiscard]] std::string getResult() const + [[nodiscard]] const char* getResult() const { if (!checked) { return "No result, yet"; @@ -64,6 +102,13 @@ class Solver { } std::unordered_map model(std::unordered_map& terms) const; + std::unordered_map model(std::vector& terms) const; + + void print_assertions() const; + ~Solver() = default; }; + +std::string stringify_term(const cvc5::Term& term, bool parenthesis = false); + }; // namespace smt_solver diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.test.cpp new file mode 100644 index 000000000000..d2ac6e04c2f0 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.test.cpp @@ -0,0 +1,83 @@ +#include "solver.hpp" +#include "barretenberg/smt_verification/terms/ffiterm.hpp" +#include "barretenberg/smt_verification/terms/ffterm.hpp" + +#include + +using namespace smt_terms; + +// Find a point of order 3 on y^2 = x^3 + 2 mod 101 curve +// Terrible when using ffiterm +TEST(Solver, FFTerm_use_case) +{ + Solver s("101", default_solver_config, 10); + FFTerm x = FFTerm::Var("x", &s); + FFTerm y = FFTerm::Var("y", &s); + + y* y == x* x* x + bb::fr(2); + FFTerm l = (3 * x * x) / (bb::fr(2) * y); + FFTerm xr = l * l - x - x; + FFTerm yr = l * (x - xr) - y; + x == xr; + y == -yr; + bool res = s.check(); + ASSERT_TRUE(res); + + std::unordered_map vars = { { "Gx", x }, { "Gy", y } }; + std::unordered_map mvars = s.model(vars); + + std::vector terms = { x, y }; + std::unordered_map vvars = s.model(terms); + ASSERT_EQ(mvars["Gx"], vvars["x"]); + ASSERT_EQ(mvars["Gy"], vvars["y"]); +} + +TEST(Solver, FFITerm_use_case) +{ + Solver s("bce4e33b636e0cf38d13a55c3"); + FFITerm x = FFITerm::Var("x", &s); + FFITerm y = FFITerm::Var("y", &s); + + bb::fr a = bb::fr::random_element(); + x <= bb::fr(2).pow(32); + x >= bb::fr(2).pow(10); + (x + y) == a; + bool res = s.check(); + ASSERT_TRUE(res); + + std::vector terms = { x, y }; + std::unordered_map vvars = s.model(terms); + info(vvars["x"]); + info("+"); + info(vvars["y"]); + info("="); + info(s.s.getValue(FFITerm(a, &s).term)); +} + +TEST(Solver, human_readable_constraints_FFTerm) +{ + Solver s("101", default_solver_config, 10); + FFTerm x = FFTerm::Var("x", &s); + FFTerm y = FFTerm::Var("y", &s); + y* y == x* x* x + bb::fr(2); + FFTerm l = (3 * x * x) / (bb::fr(2) * y); + FFTerm xr = l * l - x - x; + FFTerm yr = l * (x - xr) - y; + x == xr; + y == -yr; + s.print_assertions(); +} + +TEST(Solver, human_readable_constraints_FFITerm) +{ + Solver s("101", default_solver_config, 10); + FFITerm x = FFITerm::Var("x", &s); + FFITerm y = FFITerm::Var("y", &s); + y* y == x* x* x + bb::fr(2); + FFITerm l = (3 * x * x) / (bb::fr(2) * y); + FFITerm xr = l * l - x - x; + FFITerm yr = l * (x - xr) - y; + x == xr; + y == -yr; + s.print_assertions(); +} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp index e7e85d8da86a..535e9a2002ae 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp @@ -34,7 +34,13 @@ Bool Bool::operator==(const Bool& other) const Bool Bool::operator!=(const Bool& other) const { cvc5::Term res = solver->mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); - res = solver->mkTerm(cvc5::Kind::EQUAL, { res, this->solver->mkBoolean(false) }); + res = solver->mkTerm(cvc5::Kind::NOT, { res }); + return { res, this->solver }; +} + +Bool Bool::operator!() const +{ + cvc5::Term res = solver->mkTerm(cvc5::Kind::NOT, { this->term }); return { res, this->solver }; } }; // namespace smt_terms \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp index ff67f22be4d7..2c6a4b9691d2 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp @@ -61,6 +61,8 @@ class Bool { Bool operator&(const bool& other) const; void operator&=(const bool& other); + Bool operator!() const; + Bool operator==(const Bool& other) const; Bool operator!=(const Bool& other) const; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp index 130fa36f5ea9..d1e7330ad13e 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp @@ -152,21 +152,10 @@ void FFITerm::operator!=(const FFITerm& other) const tmp2.mod(); } cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); - eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { eq, this->solver->s.mkBoolean(false) }); + eq = this->solver->s.mkTerm(cvc5::Kind::NOT, { eq }); this->solver->s.assertFormula(eq); } -FFITerm FFITerm::operator^(const FFITerm& other) const -{ - cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::XOR, { this->term, other.term }); - return { res, this->solver }; -} - -void FFITerm::operator^=(const FFITerm& other) -{ - this->term = this->solver->s.mkTerm(cvc5::Kind::XOR, { this->term, other.term }); -} - FFITerm operator+(const bb::fr& lhs, const FFITerm& rhs) { return rhs + lhs; @@ -187,9 +176,10 @@ FFITerm operator/(const bb::fr& lhs, const FFITerm& rhs) return FFITerm(lhs, rhs.solver) / rhs; } -FFITerm operator^(const bb::fr& lhs, const FFITerm& rhs) +FFITerm operator^(__attribute__((unused)) const bb::fr& lhs, __attribute__((unused)) const FFITerm& rhs) { - return rhs ^ lhs; + info("Not compatible with Integers"); + return {}; } void operator==(const bb::fr& lhs, const FFITerm& rhs) { diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp index 3bc465f3e531..e37310e3ea67 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp @@ -67,12 +67,16 @@ class FFITerm { void operator==(const FFITerm& other) const; void operator!=(const FFITerm& other) const; - FFITerm operator^(const FFITerm& other) const; - void operator^=(const FFITerm& other); + FFITerm operator^(__attribute__((unused)) const FFITerm& other) const + { + info("Not compatible with Integers"); + return {}; + } + void operator^=(__attribute__((unused)) const FFITerm& other) { info("Not compatible with Integers"); }; void mod(); - operator std::string() const { return term.isIntegerValue() ? term.getIntegerValue() : term.toString(); }; + operator std::string() const { return smt_solver::stringify_term(term); }; operator cvc5::Term() const { return term; }; ~FFITerm() = default; @@ -113,8 +117,14 @@ class FFITerm { void operator==(const bb::fr& other) const { *this == FFITerm(other, this->solver); } void operator!=(const bb::fr& other) const { *this != FFITerm(other, this->solver); } - FFITerm operator^(const bb::fr& other) const { return *this ^ FFITerm(other, this->solver); } - void operator^=(const bb::fr& other) { *this ^= FFITerm(other, this->solver); } + + FFITerm operator^(__attribute__((unused)) const bb::fr& other) const + { + info("Not compatible with Integers"); + return {}; + } + void operator^=(__attribute__((unused)) const bb::fr& other) { info("Not compatible with Finite Field"); } + void operator<(const bb::fr& other) const; void operator<=(const bb::fr& other) const; void operator>(const bb::fr& other) const; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp index 7fc5e3edbf35..1538b5ce5858 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp @@ -15,7 +15,7 @@ TEST(FFITerm, addition) bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); bb::fr c = a + b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); FFITerm x = FFITerm::Var("x", &s); FFITerm y = FFITerm::Var("y", &s); @@ -36,7 +36,7 @@ TEST(FFITerm, subtraction) bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); bb::fr c = a - b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); FFITerm x = FFITerm::Var("x", &s); FFITerm y = FFITerm::Var("y", &s); @@ -57,7 +57,7 @@ TEST(FFITerm, multiplication) bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); bb::fr c = a * b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); FFITerm x = FFITerm::Var("x", &s); FFITerm y = FFITerm::Var("y", &s); @@ -78,7 +78,7 @@ TEST(FFITerm, division) bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); bb::fr c = a / b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); FFITerm x = FFITerm::Var("x", &s); FFITerm y = FFITerm::Var("y", &s); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index 2dfc0904afdc..af31f5833d86 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -125,7 +125,7 @@ void FFTerm::operator==(const FFTerm& other) const void FFTerm::operator!=(const FFTerm& other) const { cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); - eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { eq, this->solver->s.mkBoolean(false) }); + eq = this->solver->s.mkTerm(cvc5::Kind::NOT, { eq }); this->solver->s.assertFormula(eq); } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp index e847daea07fb..c777fd6bbefa 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -72,7 +72,7 @@ class FFTerm { void mod(){}; - operator std::string() const { return term.isFiniteFieldValue() ? term.getFiniteFieldValue() : term.toString(); }; + operator std::string() const { return smt_solver::stringify_term(term); }; operator cvc5::Term() const { return term; }; ~FFTerm() = default; diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp index 08c987114b09..3ecd54362f1d 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp @@ -15,7 +15,7 @@ TEST(FFTerm, addition) bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); bb::fr c = a + b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); FFTerm x = FFTerm::Var("x", &s); FFTerm y = FFTerm::Var("y", &s); @@ -36,7 +36,7 @@ TEST(FFTerm, subtraction) bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); bb::fr c = a - b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); FFTerm x = FFTerm::Var("x", &s); FFTerm y = FFTerm::Var("y", &s); @@ -57,7 +57,7 @@ TEST(FFTerm, multiplication) bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); bb::fr c = a * b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); FFTerm x = FFTerm::Var("x", &s); FFTerm y = FFTerm::Var("y", &s); @@ -78,7 +78,7 @@ TEST(FFTerm, division) bb::fr a = bb::fr::random_element(); bb::fr b = bb::fr::random_element(); bb::fr c = a / b; - Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001", { true, 0 }, 16); + Solver s("30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001"); FFTerm x = FFTerm::Var("x", &s); FFTerm y = FFTerm::Var("y", &s);