Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
Public Attributes | List of all members
smt_solver::SolverConfiguration Struct Reference

Solver configuration. More...

#include <solver.hpp>

Public Attributes

bool produce_models
 
uint64_t timeout
 
uint32_t debug
 
bool ff_elim_disjunctive_bit
 
bool ff_bitsum
 
std::string ff_solver
 
bool lookup_enabled
 

Detailed Description

Solver configuration.

Parameters
produce_modeltells solver to actually compute the values of the variables in SAT case.
timeouttells solver to stop trying after timeout msecs.
debugset verbosity of cvc5: 0, 1, 2.
ff_elim_disjunctive_bittells solver to change all ((x = 0) | (x = 1)) to x*x = x.
ff_bitsumtells solver to identify bitsums
ff_solvertells solver which finite field solver to use: "gb", "split".
lookup_enabledtells solver to enable sets when we deal with lookups

Definition at line 25 of file solver.hpp.

Member Data Documentation

◆ debug

uint32_t smt_solver::SolverConfiguration::debug

Definition at line 28 of file solver.hpp.

◆ ff_bitsum

bool smt_solver::SolverConfiguration::ff_bitsum

Definition at line 31 of file solver.hpp.

◆ ff_elim_disjunctive_bit

bool smt_solver::SolverConfiguration::ff_elim_disjunctive_bit

Definition at line 30 of file solver.hpp.

◆ ff_solver

std::string smt_solver::SolverConfiguration::ff_solver

Definition at line 32 of file solver.hpp.

◆ lookup_enabled

bool smt_solver::SolverConfiguration::lookup_enabled

Definition at line 34 of file solver.hpp.

◆ produce_models

bool smt_solver::SolverConfiguration::produce_models

Definition at line 26 of file solver.hpp.

◆ timeout

uint64_t smt_solver::SolverConfiguration::timeout

Definition at line 27 of file solver.hpp.

The documentation for this struct was generated from the following file: