-
Notifications
You must be signed in to change notification settings - Fork 87
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: creating an SMT verification module #712
Conversation
@@ -187,6 +193,99 @@ template <typename Arithmetization> class CircuitBuilderBase { | |||
real_variable_tags.emplace_back(DUMMY_TAG); | |||
return index; | |||
} | |||
|
|||
/** | |||
* Assign a name to a variable(equivalence calss). Should be one name per equivalence class. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Typo ("Calss")
msgpack::sbuffer buffer; | ||
msgpack::pack(buffer, cir); | ||
return buffer; | ||
// info("Buffer size: ", buffer.size()); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Commented out code
barretenberg_module(smt_verification common ${CMAKE_SOURCE_DIR}/src/cvc5/tmp-lib/lib/libcvc5.so.1) | ||
|
||
barretenberg_module(smt_examples common proof_system stdlib_primitives smt_verification) | ||
#barretenberg_module(smt_polynomials common proof_system stdlib_primitives smt_verification) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Commented out code
|
||
1. First you need to import the circuit from the saved file or from the buffer: | ||
|
||
- `smt_circuit::CircuitSchema c_info = smt_circuit::unpack_from_file(str fname);` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you provide instructions without storing the circuit on disk?
@@ -0,0 +1,111 @@ | |||
# TODO how exactly ref works | |||
import cvc5 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This file is not documented at all
#include "circuit.hpp" | ||
namespace smt_circuit { | ||
|
||
Circuit::Circuit(CircuitSchema& circuit_info, Solver* solver, const std::string& tag) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This file has very few comments
This became a monorepo PR |
Description
Please provide a paragraph or two giving a summary of the change, including relevant motivation and context.
Checklist:
@brief
describing the intended functionality.include
directives have been added.