smt_terms::FFTerm Class Reference

Finite Field element class. More...

#include <ffterm.hpp>

Public Member Functions
	FFTerm (const std::string &t, Solver *slv, bool isconst=false, uint32_t base=16)
	FFTerm (cvc5::Term &term, Solver *s)
	FFTerm (const FFTerm &other)=default
	FFTerm (FFTerm &&other)=default
FFTerm &	operator= (const FFTerm &right)=default
FFTerm &	operator= (FFTerm &&right)=default
FFTerm	operator+ (const FFTerm &other) const
void	operator+= (const FFTerm &other)
FFTerm	operator- (const FFTerm &other) const
void	operator-= (const FFTerm &other)
FFTerm	operator* (const FFTerm &other) const
void	operator*= (const FFTerm &other)
FFTerm	operator/ (const FFTerm &other) const
	Division operation.
void	operator/= (const FFTerm &other)
void	operator== (const FFTerm &other) const
void	operator!= (const FFTerm &other) const
	operator std::string () const
	operator cvc5::Term () const

Static Public Member Functions
static FFTerm	Var (const std::string &name, Solver *slv)
static FFTerm	Const (const std::string &val, Solver *slv, uint32_t base=16)

Public Attributes
Solver *	solver
cvc5::Term	term

Friends
std::ostream &	operator<< (std::ostream &out, const FFTerm &k)
FFTerm	batch_add (const std::vector< FFTerm > &children)
FFTerm	batch_mul (const std::vector< FFTerm > &children)

Detailed Description

Finite Field element class.

Can be a finite field symbolic variable or a constant. Both of them support basic arithmetic operations: +, -, *, /. Check the satisfability of a system and get it's model.

Member Function Documentation

Const()

FFTerm smt_terms::FFTerm::Const ( const std::string &  val, Solver *  slv, uint32_t  base = 16  )

static

Create a finite field numeric member.

Parameters

val	String representation of the value.
slv	Pointer to the global solver.
base	Base of the string representation. 16 by default.

Returns

Finite field constant.

operator!=()

void smt_terms::FFTerm::operator!=

(

const FFTerm &

other

)

const

Create an inequality constraint between two finite field elements.

operator/()

FFTerm smt_terms::FFTerm::operator/

(

const FFTerm &

other

)

const

Division operation.

Returns a result of the division by creating a new symbolic variable and adding a new constraint to the solver.

Parameters

other

Returns

FFTerm

operator==()

void smt_terms::FFTerm::operator==

(

const FFTerm &

other

)

const

Create an equality constraint between two finite field elements.

Var()

FFTerm smt_terms::FFTerm::Var ( const std::string &  name, Solver *  slv  )

static

Create a finite field symbolic variable.

Parameters

name	Name of the variable. Should be unique per variable.
slv	Pointer to the global solver.

Returns

Finite field symbolic variable.

---

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

• src/barretenberg/smt_verification/terms/ffterm.hpp
• src/barretenberg/smt_verification/terms/ffterm.cpp