smt_solver::Solver Class Reference

Class for the solver. More...

#include <solver.hpp>

Public Member Functions
	Solver (const std::string &modulus, const SolverConfiguration &config=default_solver_config, uint32_t base=16, uint32_t bvsize=254)
	Solver (const Solver &other)=delete
	Solver (Solver &&other)=delete
Solver &	operator= (const Solver &other)=delete
Solver &	operator= (Solver &&other)=delete
void	assertFormula (const cvc5::Term &term) const
bool	check ()
const char *	getResult () const
cvc5::Term	get_symbolic_value (const cvc5::Term &term) const
std::string	get (const cvc5::Term &term) const
	Returns.
std::string	operator[] (const cvc5::Term &term) const
std::unordered_map< std::string, std::string >	model (std::unordered_map< std::string, cvc5::Term > &terms) const
std::unordered_map< std::string, std::string >	model (std::vector< cvc5::Term > &terms) const
void	print_assertions ()
std::string	stringify_term (const cvc5::Term &term, bool parenthesis=false)
std::string	get_array_name (const cvc5::Term &term)
	recover the array name from the nested assigments
std::pair< std::string, size_t >	print_array_trace (const cvc5::Term &term, bool is_head=true)
	print the trace of array assigments up to previously printed ones
std::string	get_set_name (const cvc5::Term &term)
	recover the set name from the nested assigments
std::pair< std::string, size_t >	print_set_trace (const cvc5::Term &term, bool is_head=true)
	print the trace of SET insertions up to previously printed ones
	~Solver ()=default

Public Attributes
cvc5::TermManager	term_manager
cvc5::Solver	solver
cvc5::Sort	ff_sort
cvc5::Sort	bv_sort
std::string	modulus
bool	res = false
cvc5::Result	cvc_result
bool	checked = false
bool	lookup_enabled = false
std::unordered_map< std::string, size_t >	cached_array_traces
std::unordered_map< std::string, size_t >	cached_set_traces

Detailed Description

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.

Definition at line 80 of file solver.hpp.

Constructor & Destructor Documentation

Solver() [1/3]

smt_solver::Solver::Solver ( const std::string &  modulus, const SolverConfiguration &  config = default_solver_config, uint32_t  base = 16, uint32_t  bvsize = 254  )

inlineexplicit

Definition at line 92 of file solver.hpp.

Solver() [2/3]

smt_solver::Solver::Solver ( const Solver &  other )

delete

Solver() [3/3]

smt_solver::Solver::Solver ( Solver &&  other )

delete

~Solver()

smt_solver::Solver::~Solver ( )

default

Member Function Documentation

assertFormula()

void smt_solver::Solver::assertFormula ( const cvc5::Term &  term ) const

inline

Definition at line 158 of file solver.hpp.

check()

bool smt_solver::Solver::check

(

)

Check if the system is solvable.

Returns

true if the system is solvable.

Definition at line 11 of file solver.cpp.

get()

std::string smt_solver::Solver::get

(

const cvc5::Term &

term

)

const

Returns.

• string value, if term is constant
• string value, if term is a variable and the model is ready

Parameters

term

Returns

string value of the term

Definition at line 32 of file solver.cpp.

get_array_name()

std::string smt_solver::Solver::get_array_name

(

const cvc5::Term &

term

)

recover the array name from the nested assigments

Parameters

term	array term

Returns

std::string array name

Definition at line 147 of file solver.cpp.

get_set_name()

std::string smt_solver::Solver::get_set_name

(

const cvc5::Term &

term

)

recover the set name from the nested assigments

Parameters

term

set term

Returns

std::string array name

Definition at line 210 of file solver.cpp.

get_symbolic_value()

cvc5::Term smt_solver::Solver::get_symbolic_value ( const cvc5::Term &  term ) const

inline

Definition at line 170 of file solver.hpp.

getResult()

const char * smt_solver::Solver::getResult ( ) const

inline

Definition at line 162 of file solver.hpp.

model() [1/2]

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. Specify the map to retrieve the values you need using the keys that are convenient for you.

e.g. {"a": a}, where a is a symbolic term with the name "var78". The return map will be {"a", value_of_a}

Parameters

terms

A map containing pairs (name, symbolic term).

Returns

A map containing pairs (name, value).

Definition at line 80 of file solver.cpp.

model() [2/2]

std::unordered_map< std::string, std::string > smt_solver::Solver::model

(

std::vector< cvc5::Term > &

terms

)

const

If the system is solvable, extract the values for the given symbolic variables. The return map will contain the resulting values, which are available by the names of the corresponding symbolic variable.

e.g. if the input vector is {a} and a it is a term with name var78, it will return {"var78": value_of_var78}

Parameters

terms

A vector containing symbolic terms.

Returns

A map containing pairs (variable name, value).

Definition at line 100 of file solver.cpp.

operator=() [1/2]

Solver & smt_solver::Solver::operator= ( const Solver &  other )

delete

operator=() [2/2]

Solver & smt_solver::Solver::operator= ( Solver &&  other )

delete

operator[]()

std::string smt_solver::Solver::operator[] ( const cvc5::Term &  term ) const

inline

Definition at line 173 of file solver.hpp.

print_array_trace()

std::pair< std::string, size_t > smt_solver::Solver::print_array_trace	(	const cvc5::Term &	term,
		bool	is_head = true
	)

print the trace of array assigments up to previously printed ones

Parameters

term	array term
is_head	end of the recursion indicator

Returns

std::pair<std::string, size_t> pair: array_name, current_depth

Definition at line 116 of file solver.cpp.

print_assertions()

void smt_solver::Solver::print_assertions

(

)

Output assertions in human readable format.

Definition at line 421 of file solver.cpp.

print_set_trace()

std::pair< std::string, size_t > smt_solver::Solver::print_set_trace	(	const cvc5::Term &	term,
		bool	is_head = true
	)

print the trace of SET insertions up to previously printed ones

Parameters

term	set term
is_head	end of the recursion indicator

Returns

std::pair<std::string, size_t> pair: set_name, current_depth

Definition at line 168 of file solver.cpp.

stringify_term()

std::string smt_solver::Solver::stringify_term	(	const cvc5::Term &	term,
		bool	parenthesis = false
	)

A simple recursive function that converts native smt language to somewhat readable by humans.

e.g. converts (or (= a0 b0000000000) (= a0 b0000000001)) to ((a0 == 0) || (a0 == 1)) (= (* (+ a b) c) 10) to ((a + b) * c) == 10

Parameters

term	cvc5 term.

Returns

Parsed term.

Definition at line 235 of file solver.cpp.

Member Data Documentation

bv_sort

cvc5::Sort smt_solver::Solver::bv_sort

Definition at line 85 of file solver.hpp.

cached_array_traces

std::unordered_map<std::string, size_t> smt_solver::Solver::cached_array_traces

Definition at line 184 of file solver.hpp.

cached_set_traces

std::unordered_map<std::string, size_t> smt_solver::Solver::cached_set_traces

Definition at line 189 of file solver.hpp.

checked

bool smt_solver::Solver::checked = false

Definition at line 89 of file solver.hpp.

cvc_result

cvc5::Result smt_solver::Solver::cvc_result

Definition at line 88 of file solver.hpp.

ff_sort

cvc5::Sort smt_solver::Solver::ff_sort

Definition at line 84 of file solver.hpp.

lookup_enabled

bool smt_solver::Solver::lookup_enabled = false

Definition at line 90 of file solver.hpp.

modulus

std::string smt_solver::Solver::modulus

Definition at line 86 of file solver.hpp.

res

bool smt_solver::Solver::res = false

Definition at line 87 of file solver.hpp.

solver

cvc5::Solver smt_solver::Solver::solver

Definition at line 83 of file solver.hpp.

term_manager

cvc5::TermManager smt_solver::Solver::term_manager

Definition at line 82 of file solver.hpp.

---

The documentation for this class was generated from the following files:

• src/barretenberg/smt_verification/solver/solver.hpp
• src/barretenberg/smt_verification/solver/solver.cpp