From 8d0860b1ff0ee53d38a8c48f1cde447c83bf70cd Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 14 Mar 2024 08:06:16 +0000 Subject: [PATCH 1/6] Made cvc5 external project. No manual installation --- .../smt_verification/CMakeLists.txt | 34 +++++++++++++------ 1 file changed, 23 insertions(+), 11 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt index ad7ed03dd4a..431354b5802 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt +++ b/barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt @@ -1,14 +1,26 @@ -barretenberg_module(smt_verification common proof_system stdlib_primitives stdlib_sha256 cvc5 circuit_checker) +include(ExternalProject) -set(CVC5_INCLUDE $ENV{HOME}/cvc5/tmp-lib/include) -set(CVC5_LIB $ENV{HOME}/cvc5/tmp-lib/lib) +# External project: Download cvc5 from GitHub +set(CVC5_PREFIX "${CMAKE_BINARY_DIR}/_deps/cvc5") +set(CVC5_BUILD "${CVC5_PREFIX}/src/cvc5-build") -target_include_directories(smt_verification PUBLIC ${CVC5_INCLUDE}) -target_include_directories(smt_verification_objects PUBLIC ${CVC5_INCLUDE}) -target_include_directories(smt_verification_tests PUBLIC ${CVC5_INCLUDE}) -target_include_directories(smt_verification_test_objects PUBLIC ${CVC5_INCLUDE}) +ExternalProject_Add( + cvc5-download + PREFIX ${CVC5_PREFIX} + GIT_REPOSITORY "https://github.com/cvc5/cvc5.git" + GIT_TAG main + BUILD_IN_SOURCE YES + CONFIGURE_COMMAND ${SHELL} ./configure.sh production --auto-download --cocoa --cryptominisat --kissat -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ --prefix=${CVC5_BUILD} + BUILD_COMMAND make -C build + INSTALL_COMMAND make -C build install + UPDATE_COMMAND "" # No update step +) -target_link_directories(smt_verification PUBLIC ${CVC5_LIB}) -target_link_directories(smt_verification_objects PUBLIC ${CVC5_LIB}) -target_link_directories(smt_verification_tests PUBLIC ${CVC5_LIB}) -target_link_directories(smt_verification_test_objects PUBLIC ${CVC5_LIB}) +set(CVC5_INCLUDE "${CVC5_BUILD}/include") +set(CVC5_LIB "${CVC5_BUILD}/lib/libcvc5.so") + +include_directories(${CVC5_INCLUDE}) +add_library(cvc5 SHARED IMPORTED) +set_target_properties(cvc5 PROPERTIES IMPORTED_LOCATION ${CVC5_LIB}) + +barretenberg_module(smt_verification common proof_system stdlib_primitives stdlib_sha256 circuit_checker cvc5) \ No newline at end of file From 491b651846b671983d87444170ecaf736db7bb8c Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 14 Mar 2024 08:06:54 +0000 Subject: [PATCH 2/6] I have no idea how did it pass here --- .../cpp/src/barretenberg/smt_verification/circuit/circuit.hpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp index d2bce23aab6..910310a6684 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/circuit/circuit.hpp @@ -468,7 +468,7 @@ template size_t Circuit::prepare_gates(size_t cursor) // Handles the case when we have univariate polynomial as constraint // by simply finding the roots via quadratic formula(or linear) // There're 7 possibilities of that, which are present below - bool univariate_flag = true; + bool univariate_flag = false; univariate_flag |= (w_l == w_r) && (w_r == w_o); univariate_flag |= (w_l == w_r) && (q_3 == 0); univariate_flag |= (w_l == w_o) && (q_2 == 0) && (q_m == 0); From 99541081d1835189f3c4075e26f634df4a5090ef Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 14 Mar 2024 08:08:40 +0000 Subject: [PATCH 3/6] CVC5 api was updated --- .../smt_verification/solver/solver.hpp | 5 ++- .../smt_verification/terms/ffiterm.cpp | 42 +++++++++---------- .../smt_verification/terms/ffiterm.hpp | 10 ++--- .../smt_verification/terms/ffterm.cpp | 28 ++++++------- .../smt_verification/terms/ffterm.hpp | 4 +- 5 files changed, 45 insertions(+), 44 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp index e2bc854c67f..e79cdc6893e 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -37,6 +37,7 @@ const SolverConfiguration default_solver_config = { true, 0, 0, false, "" }; */ class Solver { public: + cvc5::TermManager tm; cvc5::Solver s; cvc5::Sort fp; std::string modulus; // modulus in base 10 @@ -46,9 +47,9 @@ class Solver { explicit Solver(const std::string& modulus, const SolverConfiguration& config = default_solver_config, - uint32_t base = 16) + uint32_t base = 16):s(tm) { - this->fp = s.mkFiniteFieldSort(modulus, base); + this->fp = tm.mkFiniteFieldSort(modulus, base); this->modulus = fp.getFiniteFieldSize(); if (config.produce_models) { s.setOption("produce-models", "true"); diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp index d1e7330ad13..dccce0e0071 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp @@ -29,64 +29,64 @@ FFITerm FFITerm::Const(const std::string& val, Solver* slv, uint32_t base) FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) : solver(slv) - , modulus(slv->s.mkInteger(slv->modulus)) + , modulus(slv->tm.mkInteger(slv->modulus)) { if (!isconst) { - this->term = slv->s.mkConst(slv->s.getIntegerSort(), t); - cvc5::Term ge = slv->s.mkTerm(cvc5::Kind::GEQ, { this->term, slv->s.mkInteger(0) }); - cvc5::Term lt = slv->s.mkTerm(cvc5::Kind::LT, { this->term, this->modulus }); + this->term = slv->tm.mkConst(slv->tm.getIntegerSort(), t); + cvc5::Term ge = slv->tm.mkTerm(cvc5::Kind::GEQ, { this->term, slv->tm.mkInteger(0) }); + cvc5::Term lt = slv->tm.mkTerm(cvc5::Kind::LT, { this->term, this->modulus }); slv->s.assertFormula(ge); slv->s.assertFormula(lt); } else { // TODO(alex): CVC5 doesn't provide integer initialization from hex. Yet. - std::string strvalue = slv->s.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); - this->term = slv->s.mkInteger(strvalue); + std::string strvalue = slv->tm.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); + this->term = slv->tm.mkInteger(strvalue); this->mod(); } } void FFITerm::mod() { - this->term = this->solver->s.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); } FFITerm FFITerm::operator+(const FFITerm& other) const { - cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); + cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); return { res, this->solver }; } void FFITerm::operator+=(const FFITerm& other) { - this->term = this->solver->s.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); } FFITerm FFITerm::operator-(const FFITerm& other) const { - cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); + cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); return { res, this->solver }; } void FFITerm::operator-=(const FFITerm& other) { - this->term = this->solver->s.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); } FFITerm FFITerm::operator-() const { - cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::NEG, { this->term }); + cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::NEG, { this->term }); return { res, this->solver }; } FFITerm FFITerm::operator*(const FFITerm& other) const { - cvc5::Term res = solver->s.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); + cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); return { res, this->solver }; } void FFITerm::operator*=(const FFITerm& other) { - this->term = this->solver->s.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); } /** @@ -133,7 +133,7 @@ void FFITerm::operator==(const FFITerm& other) const if (tmp2.term.getNumChildren() > 1) { tmp2.mod(); } - cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); + cvc5::Term eq = this->solver->tm.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); this->solver->s.assertFormula(eq); } @@ -151,8 +151,8 @@ void FFITerm::operator!=(const FFITerm& other) const if (tmp2.term.getNumChildren() > 1) { tmp2.mod(); } - cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); - eq = this->solver->s.mkTerm(cvc5::Kind::NOT, { eq }); + cvc5::Term eq = this->solver->tm.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); + eq = this->solver->tm.mkTerm(cvc5::Kind::NOT, { eq }); this->solver->s.assertFormula(eq); } @@ -193,22 +193,22 @@ void operator!=(const bb::fr& lhs, const FFITerm& rhs) void FFITerm::operator<(const bb::fr& other) const { - cvc5::Term lt = this->solver->s.mkTerm(cvc5::Kind::LT, { this->term, FFITerm(other, this->solver) }); + cvc5::Term lt = this->solver->tm.mkTerm(cvc5::Kind::LT, { this->term, FFITerm(other, this->solver) }); this->solver->s.assertFormula(lt); } void FFITerm::operator<=(const bb::fr& other) const { - cvc5::Term le = this->solver->s.mkTerm(cvc5::Kind::LEQ, { this->term, FFITerm(other, this->solver) }); + cvc5::Term le = this->solver->tm.mkTerm(cvc5::Kind::LEQ, { this->term, FFITerm(other, this->solver) }); this->solver->s.assertFormula(le); } void FFITerm::operator>(const bb::fr& other) const { - cvc5::Term gt = this->solver->s.mkTerm(cvc5::Kind::GT, { this->term, FFITerm(other, this->solver) }); + cvc5::Term gt = this->solver->tm.mkTerm(cvc5::Kind::GT, { this->term, FFITerm(other, this->solver) }); this->solver->s.assertFormula(gt); } void FFITerm::operator>=(const bb::fr& other) const { - cvc5::Term ge = this->solver->s.mkTerm(cvc5::Kind::GEQ, { this->term, FFITerm(other, this->solver) }); + cvc5::Term ge = this->solver->tm.mkTerm(cvc5::Kind::GEQ, { this->term, FFITerm(other, this->solver) }); this->solver->s.assertFormula(ge); } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp index 6b7a53a4531..6d180f680b5 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp @@ -30,7 +30,7 @@ class FFITerm { FFITerm(cvc5::Term& term, Solver* s) : solver(s) , term(term) - , modulus(s->s.mkInteger(s->modulus)) + , modulus(s->tm.mkInteger(s->modulus)) {} explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16); @@ -91,8 +91,8 @@ class FFITerm { { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = slv->s.mkTerm(cvc5::Kind::ADD, terms); - res = slv->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); + cvc5::Term res = slv->tm.mkTerm(cvc5::Kind::ADD, terms); + res = slv->tm.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); return { res, slv }; } @@ -100,8 +100,8 @@ class FFITerm { { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = slv->s.mkTerm(cvc5::Kind::MULT, terms); - res = slv->s.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); + cvc5::Term res = slv->tm.mkTerm(cvc5::Kind::MULT, terms); + res = slv->tm.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); return { res, slv }; } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index af31f5833d8..ec981d99a5f 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -31,51 +31,51 @@ FFTerm::FFTerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) : solver(slv) { if (!isconst) { - this->term = slv->s.mkConst(slv->fp, t); + this->term = slv->tm.mkConst(slv->fp, t); } else { - this->term = slv->s.mkFiniteFieldElem(t, slv->fp, base); + this->term = slv->tm.mkFiniteFieldElem(t, slv->fp, base); } } FFTerm FFTerm::operator+(const FFTerm& other) const { - cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); + cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); return { res, this->solver }; } void FFTerm::operator+=(const FFTerm& other) { - this->term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); } FFTerm FFTerm::operator-(const FFTerm& other) const { - cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); - res = solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, res }); + cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); + res = solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, res }); return { res, this->solver }; } FFTerm FFTerm::operator-() const { - cvc5::Term res = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { this->term }); + cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { this->term }); return { res, this->solver }; } void FFTerm::operator-=(const FFTerm& other) { - cvc5::Term tmp_term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); - this->term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, tmp_term }); + cvc5::Term tmp_term = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, tmp_term }); } FFTerm FFTerm::operator*(const FFTerm& other) const { - cvc5::Term res = solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); + cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); return { res, this->solver }; } void FFTerm::operator*=(const FFTerm& other) { - this->term = this->solver->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); } /** @@ -114,7 +114,7 @@ void FFTerm::operator/=(const FFTerm& other) */ void FFTerm::operator==(const FFTerm& other) const { - cvc5::Term eq = this->solver->s.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + cvc5::Term eq = this->solver->tm.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); this->solver->s.assertFormula(eq); } @@ -124,8 +124,8 @@ 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::NOT, { eq }); + cvc5::Term eq = this->solver->tm.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + eq = this->solver->tm.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 2be142d4960..478f39a9802 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -87,7 +87,7 @@ class FFTerm { { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = slv->s.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, terms); + cvc5::Term res = slv->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, terms); return { res, slv }; } @@ -95,7 +95,7 @@ class FFTerm { { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = slv->s.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, terms); + cvc5::Term res = slv->tm.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, terms); return { res, slv }; } From bf793374ba4f3cf8e2adca85fc05e6afc02eb673 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 14 Mar 2024 08:08:54 +0000 Subject: [PATCH 4/6] Updated Bool class - CVC5 api now uses TermManager instead of Solver to manage terms - I have no recollection of making Bool to have only pure cvc5::Solver, fixed it --- .../smt_verification/terms/bool.cpp | 16 +++++----- .../smt_verification/terms/bool.hpp | 29 +++++++++---------- 2 files changed, 21 insertions(+), 24 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp index 535e9a2002a..b64e3ab2992 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp @@ -4,43 +4,43 @@ namespace smt_terms { Bool Bool::operator|(const Bool& other) const { - cvc5::Term res = solver->mkTerm(cvc5::Kind::OR, { this->term, other.term }); + cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::OR, { this->term, other.term }); ; return { res, this->solver }; } void Bool::operator|=(const Bool& other) { - this->term = this->solver->mkTerm(cvc5::Kind::OR, { this->term, other.term }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::OR, { this->term, other.term }); } Bool Bool::operator&(const Bool& other) const { - cvc5::Term res = solver->mkTerm(cvc5::Kind::AND, { this->term, other.term }); + cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::AND, { this->term, other.term }); return { res, this->solver }; } void Bool::operator&=(const Bool& other) { - this->term = this->solver->mkTerm(cvc5::Kind::AND, { this->term, other.term }); + this->term = this->solver->tm.mkTerm(cvc5::Kind::AND, { this->term, other.term }); } Bool Bool::operator==(const Bool& other) const { - cvc5::Term res = solver->mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); return { res, this->solver }; } Bool Bool::operator!=(const Bool& other) const { - cvc5::Term res = solver->mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); - res = solver->mkTerm(cvc5::Kind::NOT, { res }); + cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + res = solver->tm.mkTerm(cvc5::Kind::NOT, { res }); return { res, this->solver }; } Bool Bool::operator!() const { - cvc5::Term res = solver->mkTerm(cvc5::Kind::NOT, { this->term }); + cvc5::Term res = solver->tm.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 2c6a4b9691d..f2cf73faf00 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp @@ -14,29 +14,26 @@ using namespace smt_solver; */ class Bool { public: - cvc5::Solver* solver; + Solver* solver; cvc5::Term term; bool asserted = false; - explicit Bool(const cvc5::Term& t, Solver& slv) - : solver(&slv.s) + Bool(const cvc5::Term& t, Solver* slv) + : solver(slv) , term(t){}; explicit Bool(const FFTerm& t) - : solver(&t.solver->s) + : solver(t.solver) , term(t.term){}; explicit Bool(const FFITerm& t) - : solver(&t.solver->s) + : solver(t.solver) , term(t.term){}; - explicit Bool(bool t, Solver& slv) - : solver(&slv.s) + explicit Bool(bool t, Solver* slv) + : solver(slv) { - term = solver->mkBoolean(t); + term = solver->tm.mkBoolean(t); } - Bool(const cvc5::Term& term, cvc5::Solver* s) - : solver(s) - , term(term){}; Bool(const Bool& other) = default; Bool(Bool&& other) = default; @@ -46,7 +43,7 @@ class Bool { void assert_term() { if (!asserted) { - solver->assertFormula(term); + solver->s.assertFormula(term); asserted = true; } } @@ -71,17 +68,17 @@ class Bool { friend Bool batch_or(const std::vector& children) { - cvc5::Solver* s = children[0].solver; + Solver* s = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = s->mkTerm(cvc5::Kind::OR, terms); + cvc5::Term res = s->tm.mkTerm(cvc5::Kind::OR, terms); return { res, s }; } friend Bool batch_and(const std::vector& children) { - cvc5::Solver* s = children[0].solver; + Solver* s = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = s->mkTerm(cvc5::Kind::AND, terms); + cvc5::Term res = s->tm.mkTerm(cvc5::Kind::AND, terms); return { res, s }; } From 3d4d7d091572341117918f8730e5c83f111cf3c7 Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 14 Mar 2024 10:59:52 +0000 Subject: [PATCH 5/6] Renamed members of a Solver class and added placeholders --- .../smt_verification/solver/solver.cpp | 8 ++-- .../smt_verification/solver/solver.hpp | 39 +++++++++++-------- .../smt_verification/solver/solver.test.cpp | 2 +- 3 files changed, 27 insertions(+), 22 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp index 6a3a369a4e9..4090cce9352 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.cpp @@ -10,7 +10,7 @@ namespace smt_solver { * */ bool Solver::check() { - cvc5::Result result = this->s.checkSat(); + cvc5::Result result = this->solver.checkSat(); this->checked = true; this->cvc_result = result; @@ -41,7 +41,7 @@ std::unordered_map Solver::model(std::unordered_map resulting_model; for (auto& term : terms) { - cvc5::Term val = this->s.getValue(term.second); + cvc5::Term val = this->solver.getValue(term.second); std::string str_val; if (val.isIntegerValue()) { str_val = val.getIntegerValue(); @@ -76,7 +76,7 @@ std::unordered_map Solver::model(std::vector resulting_model; for (auto& term : terms) { - cvc5::Term val = this->s.getValue(term); + cvc5::Term val = this->solver.getValue(term); std::string str_val; if (val.isIntegerValue()) { str_val = val.getIntegerValue(); @@ -199,7 +199,7 @@ std::string stringify_term(const cvc5::Term& term, bool parenthesis) * */ void Solver::print_assertions() const { - for (auto& t : this->s.getAssertions()) { + for (auto& t : this->solver.getAssertions()) { info(stringify_term(t)); } } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp index e79cdc6893e..21e66826609 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.hpp @@ -37,9 +37,9 @@ const SolverConfiguration default_solver_config = { true, 0, 0, false, "" }; */ class Solver { public: - cvc5::TermManager tm; - cvc5::Solver s; - cvc5::Sort fp; + cvc5::TermManager term_manager; + cvc5::Solver solver; + cvc5::Sort ff_sort; std::string modulus; // modulus in base 10 bool res = false; cvc5::Result cvc_result; @@ -47,25 +47,26 @@ class Solver { explicit Solver(const std::string& modulus, const SolverConfiguration& config = default_solver_config, - uint32_t base = 16):s(tm) + uint32_t base = 16) + : solver(term_manager) { - this->fp = tm.mkFiniteFieldSort(modulus, base); - this->modulus = fp.getFiniteFieldSize(); + this->ff_sort = term_manager.mkFiniteFieldSort(modulus, base); + this->modulus = ff_sort.getFiniteFieldSize(); if (config.produce_models) { - s.setOption("produce-models", "true"); + solver.setOption("produce-models", "true"); } if (config.timeout > 0) { - s.setOption("tlimit-per", std::to_string(config.timeout)); + solver.setOption("tlimit-per", std::to_string(config.timeout)); } if (config.debug >= 1) { - s.setOption("verbosity", "5"); + solver.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"); + solver.setOption("output", "learned-lits"); + solver.setOption("output", "subs"); + solver.setOption("output", "post-asserts"); + solver.setOption("output", "trusted-proof-steps"); + solver.setOption("output", "deep-restart"); } // Can be useful when split-gb is used as ff-solver. @@ -73,7 +74,7 @@ class Solver { // 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"); + solver.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 @@ -81,10 +82,10 @@ class Solver { // 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); + solver.setOption("ff-solver", config.ff_solver); } - s.setOption("output", "incomplete"); + solver.setOption("output", "incomplete"); } Solver(const Solver& other) = delete; @@ -92,6 +93,10 @@ class Solver { Solver& operator=(const Solver& other) = delete; Solver& operator=(Solver&& other) = delete; + void assertFormula(const cvc5::Term& term) const { this->solver.assertFormula(term); } + + cvc5::Term getValue(const cvc5::Term& term) const { return this->solver.getValue(term); } + bool check(); [[nodiscard]] const char* getResult() const diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.test.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.test.cpp index d2ac6e04c2f..78e5a8833af 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/solver/solver.test.cpp @@ -51,7 +51,7 @@ TEST(Solver, FFITerm_use_case) info("+"); info(vvars["y"]); info("="); - info(s.s.getValue(FFITerm(a, &s).term)); + info(s.getValue(FFITerm(a, &s).term)); } TEST(Solver, human_readable_constraints_FFTerm) From 52fde3c9e6ec85fa64e44611636d191ebd841fdd Mon Sep 17 00:00:00 2001 From: Sarkoxed Date: Thu, 14 Mar 2024 11:01:31 +0000 Subject: [PATCH 6/6] Meet new api syntax --- .../smt_verification/terms/bool.cpp | 16 ++--- .../smt_verification/terms/bool.hpp | 8 +-- .../smt_verification/terms/ffiterm.cpp | 58 +++++++++---------- .../smt_verification/terms/ffiterm.hpp | 10 ++-- .../smt_verification/terms/ffiterm.test.cpp | 16 ++--- .../smt_verification/terms/ffterm.cpp | 32 +++++----- .../smt_verification/terms/ffterm.hpp | 4 +- .../smt_verification/terms/ffterm.test.cpp | 16 ++--- 8 files changed, 80 insertions(+), 80 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp index b64e3ab2992..b9173e61a72 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.cpp @@ -4,43 +4,43 @@ namespace smt_terms { Bool Bool::operator|(const Bool& other) const { - cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::OR, { this->term, other.term }); + cvc5::Term res = solver->term_manager.mkTerm(cvc5::Kind::OR, { this->term, other.term }); ; return { res, this->solver }; } void Bool::operator|=(const Bool& other) { - this->term = this->solver->tm.mkTerm(cvc5::Kind::OR, { this->term, other.term }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::OR, { this->term, other.term }); } Bool Bool::operator&(const Bool& other) const { - cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::AND, { this->term, other.term }); + cvc5::Term res = solver->term_manager.mkTerm(cvc5::Kind::AND, { this->term, other.term }); return { res, this->solver }; } void Bool::operator&=(const Bool& other) { - this->term = this->solver->tm.mkTerm(cvc5::Kind::AND, { this->term, other.term }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::AND, { this->term, other.term }); } Bool Bool::operator==(const Bool& other) const { - cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + cvc5::Term res = solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); return { res, this->solver }; } Bool Bool::operator!=(const Bool& other) const { - cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); - res = solver->tm.mkTerm(cvc5::Kind::NOT, { res }); + cvc5::Term res = solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + res = solver->term_manager.mkTerm(cvc5::Kind::NOT, { res }); return { res, this->solver }; } Bool Bool::operator!() const { - cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::NOT, { this->term }); + cvc5::Term res = solver->term_manager.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 f2cf73faf00..306b4359fad 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/bool.hpp @@ -32,7 +32,7 @@ class Bool { explicit Bool(bool t, Solver* slv) : solver(slv) { - term = solver->tm.mkBoolean(t); + term = solver->term_manager.mkBoolean(t); } Bool(const Bool& other) = default; Bool(Bool&& other) = default; @@ -43,7 +43,7 @@ class Bool { void assert_term() { if (!asserted) { - solver->s.assertFormula(term); + solver->assertFormula(term); asserted = true; } } @@ -70,7 +70,7 @@ class Bool { { Solver* s = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = s->tm.mkTerm(cvc5::Kind::OR, terms); + cvc5::Term res = s->term_manager.mkTerm(cvc5::Kind::OR, terms); return { res, s }; } @@ -78,7 +78,7 @@ class Bool { { Solver* s = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = s->tm.mkTerm(cvc5::Kind::AND, terms); + cvc5::Term res = s->term_manager.mkTerm(cvc5::Kind::AND, terms); return { res, s }; } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp index dccce0e0071..f70802397e4 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.cpp @@ -29,64 +29,64 @@ FFITerm FFITerm::Const(const std::string& val, Solver* slv, uint32_t base) FFITerm::FFITerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) : solver(slv) - , modulus(slv->tm.mkInteger(slv->modulus)) + , modulus(slv->term_manager.mkInteger(slv->modulus)) { if (!isconst) { - this->term = slv->tm.mkConst(slv->tm.getIntegerSort(), t); - cvc5::Term ge = slv->tm.mkTerm(cvc5::Kind::GEQ, { this->term, slv->tm.mkInteger(0) }); - cvc5::Term lt = slv->tm.mkTerm(cvc5::Kind::LT, { this->term, this->modulus }); - slv->s.assertFormula(ge); - slv->s.assertFormula(lt); + this->term = slv->term_manager.mkConst(slv->term_manager.getIntegerSort(), t); + cvc5::Term ge = slv->term_manager.mkTerm(cvc5::Kind::GEQ, { this->term, slv->term_manager.mkInteger(0) }); + cvc5::Term lt = slv->term_manager.mkTerm(cvc5::Kind::LT, { this->term, this->modulus }); + slv->assertFormula(ge); + slv->assertFormula(lt); } else { // TODO(alex): CVC5 doesn't provide integer initialization from hex. Yet. - std::string strvalue = slv->tm.mkFiniteFieldElem(t, slv->fp, base).getFiniteFieldValue(); - this->term = slv->tm.mkInteger(strvalue); + std::string strvalue = slv->term_manager.mkFiniteFieldElem(t, slv->ff_sort, base).getFiniteFieldValue(); + this->term = slv->term_manager.mkInteger(strvalue); this->mod(); } } void FFITerm::mod() { - this->term = this->solver->tm.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::INTS_MODULUS, { this->term, this->modulus }); } FFITerm FFITerm::operator+(const FFITerm& other) const { - cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); + cvc5::Term res = this->solver->term_manager.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); return { res, this->solver }; } void FFITerm::operator+=(const FFITerm& other) { - this->term = this->solver->tm.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::ADD, { this->term, other.term }); } FFITerm FFITerm::operator-(const FFITerm& other) const { - cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); + cvc5::Term res = this->solver->term_manager.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); return { res, this->solver }; } void FFITerm::operator-=(const FFITerm& other) { - this->term = this->solver->tm.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::SUB, { this->term, other.term }); } FFITerm FFITerm::operator-() const { - cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::NEG, { this->term }); + cvc5::Term res = this->solver->term_manager.mkTerm(cvc5::Kind::NEG, { this->term }); return { res, this->solver }; } FFITerm FFITerm::operator*(const FFITerm& other) const { - cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); + cvc5::Term res = solver->term_manager.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); return { res, this->solver }; } void FFITerm::operator*=(const FFITerm& other) { - this->term = this->solver->tm.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::MULT, { this->term, other.term }); } /** @@ -133,8 +133,8 @@ void FFITerm::operator==(const FFITerm& other) const if (tmp2.term.getNumChildren() > 1) { tmp2.mod(); } - cvc5::Term eq = this->solver->tm.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); - this->solver->s.assertFormula(eq); + cvc5::Term eq = this->solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); + this->solver->assertFormula(eq); } /** @@ -151,9 +151,9 @@ void FFITerm::operator!=(const FFITerm& other) const if (tmp2.term.getNumChildren() > 1) { tmp2.mod(); } - cvc5::Term eq = this->solver->tm.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); - eq = this->solver->tm.mkTerm(cvc5::Kind::NOT, { eq }); - this->solver->s.assertFormula(eq); + cvc5::Term eq = this->solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { tmp1.term, tmp2.term }); + eq = this->solver->term_manager.mkTerm(cvc5::Kind::NOT, { eq }); + this->solver->assertFormula(eq); } FFITerm operator+(const bb::fr& lhs, const FFITerm& rhs) @@ -193,23 +193,23 @@ void operator!=(const bb::fr& lhs, const FFITerm& rhs) void FFITerm::operator<(const bb::fr& other) const { - cvc5::Term lt = this->solver->tm.mkTerm(cvc5::Kind::LT, { this->term, FFITerm(other, this->solver) }); - this->solver->s.assertFormula(lt); + cvc5::Term lt = this->solver->term_manager.mkTerm(cvc5::Kind::LT, { this->term, FFITerm(other, this->solver) }); + this->solver->assertFormula(lt); } void FFITerm::operator<=(const bb::fr& other) const { - cvc5::Term le = this->solver->tm.mkTerm(cvc5::Kind::LEQ, { this->term, FFITerm(other, this->solver) }); - this->solver->s.assertFormula(le); + cvc5::Term le = this->solver->term_manager.mkTerm(cvc5::Kind::LEQ, { this->term, FFITerm(other, this->solver) }); + this->solver->assertFormula(le); } void FFITerm::operator>(const bb::fr& other) const { - cvc5::Term gt = this->solver->tm.mkTerm(cvc5::Kind::GT, { this->term, FFITerm(other, this->solver) }); - this->solver->s.assertFormula(gt); + cvc5::Term gt = this->solver->term_manager.mkTerm(cvc5::Kind::GT, { this->term, FFITerm(other, this->solver) }); + this->solver->assertFormula(gt); } void FFITerm::operator>=(const bb::fr& other) const { - cvc5::Term ge = this->solver->tm.mkTerm(cvc5::Kind::GEQ, { this->term, FFITerm(other, this->solver) }); - this->solver->s.assertFormula(ge); + cvc5::Term ge = this->solver->term_manager.mkTerm(cvc5::Kind::GEQ, { this->term, FFITerm(other, this->solver) }); + this->solver->assertFormula(ge); } } // namespace smt_terms diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp index 6d180f680b5..e7c6c1afc5c 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.hpp @@ -30,7 +30,7 @@ class FFITerm { FFITerm(cvc5::Term& term, Solver* s) : solver(s) , term(term) - , modulus(s->tm.mkInteger(s->modulus)) + , modulus(s->term_manager.mkInteger(s->modulus)) {} explicit FFITerm(const std::string& t, Solver* slv, bool isconst = false, uint32_t base = 16); @@ -91,8 +91,8 @@ class FFITerm { { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = slv->tm.mkTerm(cvc5::Kind::ADD, terms); - res = slv->tm.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); + cvc5::Term res = slv->term_manager.mkTerm(cvc5::Kind::ADD, terms); + res = slv->term_manager.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); return { res, slv }; } @@ -100,8 +100,8 @@ class FFITerm { { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = slv->tm.mkTerm(cvc5::Kind::MULT, terms); - res = slv->tm.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); + cvc5::Term res = slv->term_manager.mkTerm(cvc5::Kind::MULT, terms); + res = slv->term_manager.mkTerm(cvc5::Kind::INTS_MODULUS, { res, children[0].modulus }); return { res, slv }; } 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 1538b5ce585..7949ffde76c 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffiterm.test.cpp @@ -26,8 +26,8 @@ TEST(FFITerm, addition) x == a; ASSERT_TRUE(s.check()); - std::string yvals = s.s.getValue(y.term).getIntegerValue(); - std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + std::string yvals = s.getValue(y.term).getIntegerValue(); + std::string bvals = s.getValue(bval.term).getIntegerValue(); ASSERT_EQ(bvals, yvals); } @@ -47,8 +47,8 @@ TEST(FFITerm, subtraction) x == a; ASSERT_TRUE(s.check()); - std::string yvals = s.s.getValue(y.term).getIntegerValue(); - std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + std::string yvals = s.getValue(y.term).getIntegerValue(); + std::string bvals = s.getValue(bval.term).getIntegerValue(); ASSERT_EQ(bvals, yvals); } @@ -68,8 +68,8 @@ TEST(FFITerm, multiplication) x == a; ASSERT_TRUE(s.check()); - std::string yvals = s.s.getValue(y.term).getIntegerValue(); - std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + std::string yvals = s.getValue(y.term).getIntegerValue(); + std::string bvals = s.getValue(bval.term).getIntegerValue(); ASSERT_EQ(bvals, yvals); } @@ -89,7 +89,7 @@ TEST(FFITerm, division) x == a; ASSERT_TRUE(s.check()); - std::string yvals = s.s.getValue(y.term).getIntegerValue(); - std::string bvals = s.s.getValue(bval.term).getIntegerValue(); + std::string yvals = s.getValue(y.term).getIntegerValue(); + std::string bvals = s.getValue(bval.term).getIntegerValue(); ASSERT_EQ(bvals, yvals); } diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp index ec981d99a5f..0761954680f 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.cpp @@ -31,51 +31,51 @@ FFTerm::FFTerm(const std::string& t, Solver* slv, bool isconst, uint32_t base) : solver(slv) { if (!isconst) { - this->term = slv->tm.mkConst(slv->fp, t); + this->term = slv->term_manager.mkConst(slv->ff_sort, t); } else { - this->term = slv->tm.mkFiniteFieldElem(t, slv->fp, base); + this->term = slv->term_manager.mkFiniteFieldElem(t, slv->ff_sort, base); } } FFTerm FFTerm::operator+(const FFTerm& other) const { - cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); + cvc5::Term res = this->solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); return { res, this->solver }; } void FFTerm::operator+=(const FFTerm& other) { - this->term = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, other.term }); } FFTerm FFTerm::operator-(const FFTerm& other) const { - cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); - res = solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, res }); + cvc5::Term res = this->solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); + res = solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, res }); return { res, this->solver }; } FFTerm FFTerm::operator-() const { - cvc5::Term res = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { this->term }); + cvc5::Term res = this->solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { this->term }); return { res, this->solver }; } void FFTerm::operator-=(const FFTerm& other) { - cvc5::Term tmp_term = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); - this->term = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, tmp_term }); + cvc5::Term tmp_term = this->solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_NEG, { other.term }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, { this->term, tmp_term }); } FFTerm FFTerm::operator*(const FFTerm& other) const { - cvc5::Term res = solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); + cvc5::Term res = solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); return { res, this->solver }; } void FFTerm::operator*=(const FFTerm& other) { - this->term = this->solver->tm.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); + this->term = this->solver->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, { this->term, other.term }); } /** @@ -114,8 +114,8 @@ void FFTerm::operator/=(const FFTerm& other) */ void FFTerm::operator==(const FFTerm& other) const { - cvc5::Term eq = this->solver->tm.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); - this->solver->s.assertFormula(eq); + cvc5::Term eq = this->solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + this->solver->assertFormula(eq); } /** @@ -124,9 +124,9 @@ void FFTerm::operator==(const FFTerm& other) const */ void FFTerm::operator!=(const FFTerm& other) const { - cvc5::Term eq = this->solver->tm.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); - eq = this->solver->tm.mkTerm(cvc5::Kind::NOT, { eq }); - this->solver->s.assertFormula(eq); + cvc5::Term eq = this->solver->term_manager.mkTerm(cvc5::Kind::EQUAL, { this->term, other.term }); + eq = this->solver->term_manager.mkTerm(cvc5::Kind::NOT, { eq }); + this->solver->assertFormula(eq); } FFTerm operator+(const bb::fr& lhs, const FFTerm& rhs) diff --git a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp index 478f39a9802..4451c4befb5 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.hpp @@ -87,7 +87,7 @@ class FFTerm { { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = slv->tm.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, terms); + cvc5::Term res = slv->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_ADD, terms); return { res, slv }; } @@ -95,7 +95,7 @@ class FFTerm { { Solver* slv = children[0].solver; std::vector terms(children.begin(), children.end()); - cvc5::Term res = slv->tm.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, terms); + cvc5::Term res = slv->term_manager.mkTerm(cvc5::Kind::FINITE_FIELD_MULT, terms); return { res, slv }; } 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 3ecd54362f1..633f40a6465 100644 --- a/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp +++ b/barretenberg/cpp/src/barretenberg/smt_verification/terms/ffterm.test.cpp @@ -26,8 +26,8 @@ TEST(FFTerm, addition) x == a; ASSERT_TRUE(s.check()); - std::string yvals = s.s.getValue(y.term).getFiniteFieldValue(); - std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue(); + std::string yvals = s.getValue(y.term).getFiniteFieldValue(); + std::string bvals = s.getValue(bval.term).getFiniteFieldValue(); ASSERT_EQ(bvals, yvals); } @@ -47,8 +47,8 @@ TEST(FFTerm, subtraction) x == a; ASSERT_TRUE(s.check()); - std::string yvals = s.s.getValue(y.term).getFiniteFieldValue(); - std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue(); + std::string yvals = s.getValue(y.term).getFiniteFieldValue(); + std::string bvals = s.getValue(bval.term).getFiniteFieldValue(); ASSERT_EQ(bvals, yvals); } @@ -68,8 +68,8 @@ TEST(FFTerm, multiplication) x == a; ASSERT_TRUE(s.check()); - std::string yvals = s.s.getValue(y.term).getFiniteFieldValue(); - std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue(); + std::string yvals = s.getValue(y.term).getFiniteFieldValue(); + std::string bvals = s.getValue(bval.term).getFiniteFieldValue(); ASSERT_EQ(bvals, yvals); } @@ -89,7 +89,7 @@ TEST(FFTerm, division) x == a; ASSERT_TRUE(s.check()); - std::string yvals = s.s.getValue(y.term).getFiniteFieldValue(); - std::string bvals = s.s.getValue(bval.term).getFiniteFieldValue(); + std::string yvals = s.getValue(y.term).getFiniteFieldValue(); + std::string bvals = s.getValue(bval.term).getFiniteFieldValue(); ASSERT_EQ(bvals, yvals); } \ No newline at end of file