-
Notifications
You must be signed in to change notification settings - Fork 189
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: CVC5 api update (AztecProtocol/aztec-packages#5203)
### CVC5 Recently `cvc5` updated their api and changed the way of creating and managing terms. Now `cvc5::TermManger` is responsible for this instead of `cvc5::Solver`. This pr fixes our api to meet their update. Also I made `cvc5` an external project in CMakeLists so now you don't have to install it manually. ### Bool For some reason `Bool` class had pure `cvc5::Solver` pointer as a member. Fixed that to be `smt_solver::Solver`. ### Circuit fixed `univariate_flag`. It was `true` by default, so it performed the wrong optimization. ### Solver renamed - `fp` -> `ff_sort` - `s` -> `solver` - `tm` -> `term_manager` Added placeholder methods `getValue` and `assertFormula` to avoid code like `solver->solver.assertFormula` --------- Co-authored-by: Innokentii Sennovskii <[email protected]>
- Loading branch information
Showing
97 changed files
with
1,941 additions
and
1,553 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1 @@ | ||
aa90f6ed7bfae06bdf6990816d154bbd24993689 | ||
9cc32cb5e4aaf03ea3457a8fcf3b38c1e39d3d04 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.