Merge 4d0512f into 25ce33b

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.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<std::string, std::string> Solver::model(std::unordered_map<st
     }
     std::unordered_map<std::string, std::string> 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<std::string, std::string> Solver::model(std::vector<cvc5::Ter
     }
     std::unordered_map<std::string, std::string> 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));
     }
 }

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

@@ -37,8 +37,9 @@ const SolverConfiguration default_solver_config = { true, 0, 0, false, "" };
  */
 class Solver {
   public:
-    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,50 +48,55 @@ class Solver {
     explicit Solver(const std::string& modulus,
                     const SolverConfiguration& config = default_solver_config,
                     uint32_t base = 16)
+        : solver(term_manager)
     {
-        this->fp = s.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.
         // 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");
+            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
         // 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);
+            solver.setOption("ff-solver", config.ff_solver);
         }
 
-        s.setOption("output", "incomplete");
+        solver.setOption("output", "incomplete");
     }
 
     Solver(const Solver& other) = delete;
     Solver(Solver&& other) = delete;
     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

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)

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->term_manager.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->term_manager.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->term_manager.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->term_manager.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->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->mkTerm(cvc5::Kind::EQUAL, { this->term, other.term });
-    res = solver->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->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

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->term_manager.mkBoolean(t);
     }
-    Bool(const cvc5::Term& term, cvc5::Solver* s)
-        : solver(s)
-        , term(term){};
     Bool(const Bool& other) = default;
     Bool(Bool&& other) = default;
 
@@ -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->term_manager.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->term_manager.mkTerm(cvc5::Kind::AND, terms);
         return { res, s };
     }