smt_terms::FFITerm Class Reference

Integer Modulo element class. More...

#include <ffiterm.hpp>

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

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

Public Attributes
Solver *	solver
cvc5::Term	term
cvc5::Term	modulus

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

Detailed Description

Integer Modulo element class.

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

Todo:

TODO(alex): mayb.. Have to patch cvc5 to create integers from hex...

Member Function Documentation

Const()

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

static

Create an integer mod 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::FFITerm::operator!=

(

const FFITerm &

other

)

const

Create an inequality constraint between two integer mod elements.

operator/()

FFITerm smt_terms::FFITerm::operator/

(

const FFITerm &

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

FFITerm

operator==()

void smt_terms::FFITerm::operator==

(

const FFITerm &

other

)

const

Create an equality constraint between two integer mod elements.

Var()

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

static

Create an integer mod 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/ffiterm.hpp
• src/barretenberg/smt_verification/terms/ffiterm.cpp