smt_util.hpp File Reference

#include <fstream>
#include "barretenberg/circuit_checker/circuit_checker.hpp"
#include "barretenberg/smt_verification/circuit/circuit_base.hpp"

Go to the source code of this file.

Macros
#define	RED   "\033[31m"
#define	RESET   "\033[0m"

Functions
std::vector< std::vector< bb::fr > >	default_model (const std::vector< std::string > &special, smt_circuit::CircuitBase &c1, smt_circuit::CircuitBase &c2, const std::string &fname="witness.out", bool pack=true)
	Get pretty formatted result of the solver work.
std::vector< bb::fr >	default_model_single (const std::vector< std::string > &special, smt_circuit::CircuitBase &c, const std::string &fname="witness.out", bool pack=true)
	Get pretty formatted result of the solver work.
bool	smt_timer (smt_solver::Solver *s)
	Get the solver result and amount of time that it took to solve.
std::pair< std::vector< bb::fr >, std::vector< bb::fr > >	base4 (uint32_t el)
	base4 decomposition with accumulators
void	fix_range_lists (bb::UltraCircuitBuilder &builder)
	Fix the triples from range_lists in the witness.
bb::fr	string_to_fr (const std::string &number, int base, bool is_signed=true, size_t step=0)
	Converts a string of an arbitrary base to fr. Note: there should be no prefix.
std::vector< std::vector< bb::fr > >	import_witness (const std::string &fname)
	Import witness, obtained by solver, from file.
std::vector< bb::fr >	import_witness_single (const std::string &fname)
	Import witness, obtained by solver, from file.

Macro Definition Documentation

RED

#define RED   "\033[31m"

Definition at line 7 of file smt_util.hpp.

RESET

#define RESET   "\033[0m"

Definition at line 8 of file smt_util.hpp.

Function Documentation

base4()

std::pair< std::vector< bb::fr >, std::vector< bb::fr > > base4

(

uint32_t

el

)

base4 decomposition with accumulators

Parameters

el

Returns

base decomposition, accumulators

Definition at line 315 of file smt_util.cpp.

default_model()

std::vector< std::vector< bb::fr > > default_model	(	const std::vector< std::string > &	special,
		smt_circuit::CircuitBase &	c1,
		smt_circuit::CircuitBase &	c2,
		const std::string &	fname,
		bool	pack
	)

Get pretty formatted result of the solver work.

Having two circuits and defined constraint system inside the solver get the pretty formatted output. The whole witness will be saved in c-like array format. Special variables will be printed to stdout. e.g. a_1, a_2 = val_a_1, val_a_2;

Parameters

special	The list of variables that you need to see in stdout
c1	first circuit
c2	the copy of the first circuit with changed tag
s	solver
fname	file to store the resulting witness if succeded
pack	flags out to pack the resulting witness using msgpack

Definition at line 62 of file smt_util.cpp.

default_model_single()

std::vector< bb::fr > default_model_single	(	const std::vector< std::string > &	special,
		smt_circuit::CircuitBase &	c,
		const std::string &	fname,
		bool	pack
	)

Get pretty formatted result of the solver work.

Having a circuit and defined constraint system inside the solver get the pretty formatted output. The whole witness will be saved in c-like array format. Special variables will be printed to stdout. e.g. a = val_a;

Parameters

special	The list of variables that you need to see in stdout
c	first circuit
s	solver
fname	file to store the resulting witness if succeded
pack	flags out to pack the resulting witness using msgpack

Definition at line 162 of file smt_util.cpp.

fix_range_lists()

void fix_range_lists

(

bb::UltraCircuitBuilder &

builder

)

Fix the triples from range_lists in the witness.

Since we are not using the part of the witness, that contains range lists, they are set to 0 by the solver. We need to overwrite them to check the witness obtained by the solver.

Parameters

builder

Definition at line 344 of file smt_util.cpp.

import_witness()

std::vector< std::vector< bb::fr > > import_witness

(

const std::string &

fname

)

Import witness, obtained by solver, from file.

Imports the witness, that was packed by default_model function

Parameters

fname

Returns

std::vector<std::vector<bb::fr>>

Definition at line 241 of file smt_util.cpp.

import_witness_single()

std::vector< bb::fr > import_witness_single

(

const std::string &

fname

)

Import witness, obtained by solver, from file.

Imports the witness, that was packed by default_model_single function

Parameters

fname

Returns

std::vector<std::vector<bb::fr>>

Definition at line 269 of file smt_util.cpp.

smt_timer()

bool smt_timer

(

smt_solver::Solver *

s

)

Get the solver result and amount of time that it took to solve.

Parameters

s

Returns

bool is system satisfiable?

Definition at line 297 of file smt_util.cpp.

string_to_fr()

bb::fr string_to_fr	(	const std::string &	number,
		int	base,
		bool	is_signed,
		size_t	step
	)

Converts a string of an arbitrary base to fr. Note: there should be no prefix.

Parameters

number	string to be converted
base	base representation of the string
is_signed	indicates whether we treat numbers in base 2 as signed or unsigned
step	power n such that base^n <= 2^64. If base = 2, 10, 16. May remain undeclared.

Returns

bb::fr

Definition at line 13 of file smt_util.cpp.