|
barretenberg
|
Class for the solver. More...
#include <solver.hpp>
Public Member Functions | |
| Solver (const std::string &modulus, const SolverConfiguration &config={ false, 0 }, uint32_t base=16) | |
| Solver (const Solver &other)=delete | |
| Solver (Solver &&other)=delete | |
| Solver & | operator= (const Solver &other)=delete |
| Solver & | operator= (Solver &&other)=delete |
| bool | check () |
| std::string | getResult () const |
| std::unordered_map< std::string, std::string > | model (std::unordered_map< std::string, cvc5::Term > &terms) const |
Public Attributes | |
| cvc5::Solver | s |
| cvc5::Sort | fp |
| std::string | modulus |
| bool | res = false |
| bool | checked = false |
Class for the solver.
Solver class that can be used to create a solver, finite field terms and the circuit. Check the satisfability of a system and get it's model.
| bool smt_solver::Solver::check | ( | ) |
Check if the system is solvable.
| std::unordered_map< std::string, std::string > smt_solver::Solver::model | ( | std::unordered_map< std::string, cvc5::Term > & | terms | ) | const |
If the system is solvable, extract the values for the given symbolic variables.
| terms | A map containing pairs (name, symbolic term). |
1.9.6