fix: CVC5 api update

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)

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

@@ -468,7 +468,7 @@ template <typename FF> size_t Circuit<FF>::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);

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");

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

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<Bool>& children)
     {
-        cvc5::Solver* s = children[0].solver;
+        Solver* s = children[0].solver;
         std::vector<cvc5::Term> 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<Bool>& children)
     {
-        cvc5::Solver* s = children[0].solver;
+        Solver* s = children[0].solver;
         std::vector<cvc5::Term> 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 };
     }
 

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);
 }
 

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,17 +91,17 @@ class FFITerm {
     {
         Solver* slv = children[0].solver;
         std::vector<cvc5::Term> 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 };
     }
 
     friend FFITerm batch_mul(const std::vector<FFITerm>& children)
     {
         Solver* slv = children[0].solver;
         std::vector<cvc5::Term> 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 };
     }