Barretenberg
The ZK-SNARK library at the core of Aztec
Loading...
Searching...
No Matches
Public Member Functions | Static Public Member Functions | Public Attributes | Private Member Functions | Friends | List of all members
smt_terms::STerm Class Reference

Symbolic term element class. More...

#include <term.hpp>

Public Member Functions

 STerm ()
 
 STerm (const cvc5::Term &term, Solver *s, TermType type)
 
 STerm (const std::string &t, Solver *slv, bool isconst=false, uint32_t base=16, TermType type=TermType::FFTerm)
 
 STerm (const STerm &other)=default
 
 STerm (STerm &&other)=default
 
 STerm (bb::fr value, Solver *s, TermType type=TermType::FFTerm)
 
STerm & operator= (const STerm &right)=default
 
STerm & operator= (STerm &&right)=default
 
STerm operator+ (const STerm &other) const
 
void operator+= (const STerm &other)
 
STerm operator- (const STerm &other) const
 
void operator-= (const STerm &other)
 
STerm operator- () const
 
STerm operator* (const STerm &other) const
 
void operator*= (const STerm &other)
 
STerm operator/ (const STerm &other) const
 Division operation.
 
void operator/= (const STerm &other)
 
STerm operator% (const STerm &other) const
 
void operator< (const STerm &other) const
 
void operator<= (const STerm &other) const
 
void operator> (const STerm &other) const
 
void operator>= (const STerm &other) const
 
void operator== (const STerm &other) const
 
void operator!= (const STerm &other) const
 
STerm operator^ (const STerm &other) const
 
void operator^= (const STerm &other)
 
STerm operator& (const STerm &other) const
 
void operator&= (const STerm &other)
 
STerm operator| (const STerm &other) const
 
void operator|= (const STerm &other)
 
STerm operator~ () const
 
STerm truncate (const uint32_t &to_size)
 Returns last to_size bits of variable.
 
STerm extract_bit (const uint32_t &bit_index)
 Returns ith bit of variable.
 
 operator std::string () const
 
 operator cvc5::Term () const
 
 ~STerm ()=default
 
STerm operator+ (const bb::fr &other) const
 
void operator+= (const bb::fr &other)
 
STerm operator- (const bb::fr &other) const
 
void operator-= (const bb::fr &other)
 
STerm operator* (const bb::fr &other) const
 
void operator*= (const bb::fr &other)
 
STerm operator/ (const bb::fr &other) const
 
void operator/= (const bb::fr &other)
 
STerm operator% (const bb::fr &other) const
 
void operator< (const bb::fr &other) const
 
void operator<= (const bb::fr &other) const
 
void operator> (const bb::fr &other) const
 
void operator>= (const bb::fr &other) const
 
void operator== (const bb::fr &other) const
 
void operator!= (const bb::fr &other) const
 
STerm operator^ (const bb::fr &other) const
 
void operator^= (const bb::fr &other)
 
STerm operator& (const bb::fr &other) const
 
void operator&= (const bb::fr &other)
 
STerm operator| (const bb::fr &other) const
 
void operator|= (const bb::fr &other)
 
STerm operator<< (const uint32_t &n) const
 
void operator<<= (const uint32_t &n)
 
STerm operator>> (const uint32_t &n) const
 
void operator>>= (const uint32_t &n)
 
STerm rotr (const uint32_t &n) const
 
STerm rotl (const uint32_t &n) const
 

Static Public Member Functions

static STerm Var (const std::string &name, Solver *slv, TermType type=TermType::FFTerm)
 
static STerm Const (const std::string &val, Solver *slv, uint32_t base=16, TermType type=TermType::FFTerm)
 
static STerm Const (const bb::fr &val, Solver *slv, TermType type=TermType::FFTerm)
 
static STerm batch_add (const std::vector< STerm > &children)
 
static STerm batch_mul (const std::vector< STerm > &children)
 

Public Attributes

Solver * solver
 
cvc5::Term term
 
TermType type
 
std::unordered_map< OpType, cvc5::Kind > operations
 

Private Member Functions

STerm mod () const
 Reduce the term modulo circuit prime.
 
STerm normalize () const
 Reduce the integer symbolic term modulo circuit prime if needed.
 

Friends

class Bool
 
std::ostream & operator<< (std::ostream &out, const STerm &term)
 

Detailed Description

Symbolic term element class.

Can be a Finite Field/Integer Mod/BitVector symbolic variable or a constant. Supports basic arithmetic operations: +, -, *, /. Additionally FFITerm and ITerm support inequalities: <, <=, >, >= and % BVTerm further supports bitwise operations: ~,^, &, |, >>, <<, ror, rol, truncate, extract_bit

Definition at line 114 of file term.hpp.

Constructor & Destructor Documentation

◆ STerm() [1/6]

smt_terms::STerm::STerm ( )
inline

Definition at line 126 of file term.hpp.

◆ STerm() [2/6]

smt_terms::STerm::STerm ( const cvc5::Term &  term,
Solver *  s,
TermType  type 
)
inline

Definition at line 131 of file term.hpp.

◆ STerm() [3/6]

smt_terms::STerm::STerm ( const std::string &  t,
Solver *  slv,
bool  isconst = false,
uint32_t  base = 16,
TermType  type = TermType::FFTerm 
)
explicit

Definition at line 54 of file term.cpp.

◆ STerm() [4/6]

smt_terms::STerm::STerm ( const STerm &  other)
default

◆ STerm() [5/6]

smt_terms::STerm::STerm ( STerm &&  other)
default

◆ STerm() [6/6]

smt_terms::STerm::STerm ( bb::fr  value,
Solver *  s,
TermType  type = TermType::FFTerm 
)
inline

Definition at line 147 of file term.hpp.

◆ ~STerm()

smt_terms::STerm::~STerm ( )
default

Member Function Documentation

◆ batch_add()

static STerm smt_terms::STerm::batch_add ( const std::vector< STerm > &  children)
inlinestatic

Definition at line 202 of file term.hpp.

◆ batch_mul()

static STerm smt_terms::STerm::batch_mul ( const std::vector< STerm > &  children)
inlinestatic

Definition at line 213 of file term.hpp.

◆ Const() [1/2]

STerm smt_terms::STerm::Const ( const bb::fr &  val,
Solver *  slv,
TermType  type = TermType::FFTerm 
)
static

Create constant symbolic variable. i.e. term with predefined constant value

Parameters
valfield value.
slvPointer to the global solver.
baseBase of the string representation. 16 by default.
typeFFTerm, FFITerm or BVTerm
Returns
numeric constant

Definition at line 44 of file term.cpp.

◆ Const() [2/2]

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

Create constant symbolic variable. i.e. term with predefined constant value

Parameters
valString representation of the value.
slvPointer to the global solver.
baseBase of the string representation. 16 by default.
typeFFTerm, FFITerm or BVTerm
Returns
numeric constant

Definition at line 29 of file term.cpp.

◆ extract_bit()

STerm smt_terms::STerm::extract_bit ( const uint32_t &  bit_index)

Returns ith bit of variable.

Parameters
bit_indexindex of bit to be extracted

Definition at line 476 of file term.cpp.

◆ mod()

STerm smt_terms::STerm::mod ( ) const
private

Reduce the term modulo circuit prime.

Returns
New Symbolic Term with reduction constraint

Definition at line 119 of file term.cpp.

◆ normalize()

STerm smt_terms::STerm::normalize ( ) const
private

Reduce the integer symbolic term modulo circuit prime if needed.

Sometimes we do not want to add extra reduction constraint due to term being already reduced.

One of the cases is FFITerm type: When we have already performed some operations with it, it needs to be reduced Otherwise it doesn't

Returns
New normalized Symbolic Term

Definition at line 140 of file term.cpp.

◆ operator cvc5::Term()

smt_terms::STerm::operator cvc5::Term ( ) const
inline

Definition at line 193 of file term.hpp.

◆ operator std::string()

smt_terms::STerm::operator std::string ( ) const
inline

Definition at line 192 of file term.hpp.

◆ operator!=() [1/2]

void smt_terms::STerm::operator!= ( const bb::fr &  other) const
inline

Definition at line 244 of file term.hpp.

◆ operator!=() [2/2]

void smt_terms::STerm::operator!= ( const STerm &  other) const

Create an inequality constraint between two symbolic variables of the same type

Definition at line 254 of file term.cpp.

◆ operator%() [1/2]

STerm smt_terms::STerm::operator% ( const bb::fr &  other) const
inline

Definition at line 236 of file term.hpp.

◆ operator%() [2/2]

STerm smt_terms::STerm::operator% ( const STerm &  other) const

Definition at line 320 of file term.cpp.

◆ operator&() [1/2]

STerm smt_terms::STerm::operator& ( const bb::fr &  other) const
inline

Definition at line 248 of file term.hpp.

◆ operator&() [2/2]

STerm smt_terms::STerm::operator& ( const STerm &  other) const

Definition at line 349 of file term.cpp.

◆ operator&=() [1/2]

void smt_terms::STerm::operator&= ( const bb::fr &  other)
inline

Definition at line 249 of file term.hpp.

◆ operator&=() [2/2]

void smt_terms::STerm::operator&= ( const STerm &  other)

Definition at line 359 of file term.cpp.

◆ operator*() [1/2]

STerm smt_terms::STerm::operator* ( const bb::fr &  other) const
inline

Definition at line 231 of file term.hpp.

◆ operator*() [2/2]

STerm smt_terms::STerm::operator* ( const STerm &  other) const

Definition at line 176 of file term.cpp.

◆ operator*=() [1/2]

void smt_terms::STerm::operator*= ( const bb::fr &  other)
inline

Definition at line 232 of file term.hpp.

◆ operator*=() [2/2]

void smt_terms::STerm::operator*= ( const STerm &  other)

Definition at line 182 of file term.cpp.

◆ operator+() [1/2]

STerm smt_terms::STerm::operator+ ( const bb::fr &  other) const
inline

Definition at line 226 of file term.hpp.

◆ operator+() [2/2]

STerm smt_terms::STerm::operator+ ( const STerm &  other) const

Definition at line 146 of file term.cpp.

◆ operator+=() [1/2]

void smt_terms::STerm::operator+= ( const bb::fr &  other)
inline

Definition at line 227 of file term.hpp.

◆ operator+=() [2/2]

void smt_terms::STerm::operator+= ( const STerm &  other)

Definition at line 152 of file term.cpp.

◆ operator-() [1/3]

STerm smt_terms::STerm::operator- ( ) const

Definition at line 170 of file term.cpp.

◆ operator-() [2/3]

STerm smt_terms::STerm::operator- ( const bb::fr &  other) const
inline

Definition at line 228 of file term.hpp.

◆ operator-() [3/3]

STerm smt_terms::STerm::operator- ( const STerm &  other) const

Definition at line 157 of file term.cpp.

◆ operator-=() [1/2]

void smt_terms::STerm::operator-= ( const bb::fr &  other)
inline

Definition at line 229 of file term.hpp.

◆ operator-=() [2/2]

void smt_terms::STerm::operator-= ( const STerm &  other)

Definition at line 164 of file term.cpp.

◆ operator/() [1/2]

STerm smt_terms::STerm::operator/ ( const bb::fr &  other) const
inline

Definition at line 233 of file term.hpp.

◆ operator/() [2/2]

STerm smt_terms::STerm::operator/ ( const STerm &  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
STerm

Definition at line 197 of file term.cpp.

◆ operator/=() [1/2]

void smt_terms::STerm::operator/= ( const bb::fr &  other)
inline

Definition at line 234 of file term.hpp.

◆ operator/=() [2/2]

void smt_terms::STerm::operator/= ( const STerm &  other)

Definition at line 217 of file term.cpp.

◆ operator<() [1/2]

void smt_terms::STerm::operator< ( const bb::fr &  other) const
inline

Definition at line 238 of file term.hpp.

◆ operator<() [2/2]

void smt_terms::STerm::operator< ( const STerm &  other) const

Definition at line 264 of file term.cpp.

◆ operator<<()

STerm smt_terms::STerm::operator<< ( const uint32_t &  n) const

Definition at line 397 of file term.cpp.

◆ operator<<=()

void smt_terms::STerm::operator<<= ( const uint32_t &  n)

Definition at line 408 of file term.cpp.

◆ operator<=() [1/2]

void smt_terms::STerm::operator<= ( const bb::fr &  other) const
inline

Definition at line 239 of file term.hpp.

◆ operator<=() [2/2]

void smt_terms::STerm::operator<= ( const STerm &  other) const

Definition at line 278 of file term.cpp.

◆ operator=() [1/2]

STerm & smt_terms::STerm::operator= ( const STerm &  right)
default

◆ operator=() [2/2]

STerm & smt_terms::STerm::operator= ( STerm &&  right)
default

◆ operator==() [1/2]

void smt_terms::STerm::operator== ( const bb::fr &  other) const
inline

Definition at line 243 of file term.hpp.

◆ operator==() [2/2]

void smt_terms::STerm::operator== ( const STerm &  other) const

Create an equality constraint between two symbolic variables of the same type

Definition at line 241 of file term.cpp.

◆ operator>() [1/2]

void smt_terms::STerm::operator> ( const bb::fr &  other) const
inline

Definition at line 240 of file term.hpp.

◆ operator>() [2/2]

void smt_terms::STerm::operator> ( const STerm &  other) const

Definition at line 292 of file term.cpp.

◆ operator>=() [1/2]

void smt_terms::STerm::operator>= ( const bb::fr &  other) const
inline

Definition at line 241 of file term.hpp.

◆ operator>=() [2/2]

void smt_terms::STerm::operator>= ( const STerm &  other) const

Definition at line 306 of file term.cpp.

◆ operator>>()

STerm smt_terms::STerm::operator>> ( const uint32_t &  n) const

Definition at line 418 of file term.cpp.

◆ operator>>=()

void smt_terms::STerm::operator>>= ( const uint32_t &  n)

Definition at line 429 of file term.cpp.

◆ operator^() [1/2]

STerm smt_terms::STerm::operator^ ( const bb::fr &  other) const
inline

Definition at line 246 of file term.hpp.

◆ operator^() [2/2]

STerm smt_terms::STerm::operator^ ( const STerm &  other) const

Definition at line 330 of file term.cpp.

◆ operator^=() [1/2]

void smt_terms::STerm::operator^= ( const bb::fr &  other)
inline

Definition at line 247 of file term.hpp.

◆ operator^=() [2/2]

void smt_terms::STerm::operator^= ( const STerm &  other)

Definition at line 340 of file term.cpp.

◆ operator|() [1/2]

STerm smt_terms::STerm::operator| ( const bb::fr &  other) const
inline

Definition at line 250 of file term.hpp.

◆ operator|() [2/2]

STerm smt_terms::STerm::operator| ( const STerm &  other) const

Definition at line 368 of file term.cpp.

◆ operator|=() [1/2]

void smt_terms::STerm::operator|= ( const bb::fr &  other)
inline

Definition at line 251 of file term.hpp.

◆ operator|=() [2/2]

void smt_terms::STerm::operator|= ( const STerm &  other)

Definition at line 378 of file term.cpp.

◆ operator~()

STerm smt_terms::STerm::operator~ ( ) const

Definition at line 387 of file term.cpp.

◆ rotl()

STerm smt_terms::STerm::rotl ( const uint32_t &  n) const

Definition at line 450 of file term.cpp.

◆ rotr()

STerm smt_terms::STerm::rotr ( const uint32_t &  n) const

Definition at line 439 of file term.cpp.

◆ truncate()

STerm smt_terms::STerm::truncate ( const uint32_t &  to_size)

Returns last to_size bits of variable.

Parameters
to_sizenumber of bits to be extracted

Definition at line 461 of file term.cpp.

◆ Var()

STerm smt_terms::STerm::Var ( const std::string &  name,
Solver *  slv,
TermType  type = TermType::FFTerm 
)
static

Create a symbolic variable.

Parameters
nameName of the variable. Should be unique per variable
slvPointer to the global solver
typeFFTerm, FFITerm or BVTerm
Returns
symbolic variable

Definition at line 14 of file term.cpp.

Friends And Related Symbol Documentation

◆ Bool

friend class Bool
friend

Definition at line 261 of file term.hpp.

◆ operator<<

std::ostream & operator<< ( std::ostream &  out,
const STerm &  term 
)
friend

Definition at line 197 of file term.hpp.

Member Data Documentation

◆ operations

std::unordered_map<OpType, cvc5::Kind> smt_terms::STerm::operations

Definition at line 124 of file term.hpp.

◆ solver

Solver* smt_terms::STerm::solver

Definition at line 120 of file term.hpp.

◆ term

cvc5::Term smt_terms::STerm::term

Definition at line 121 of file term.hpp.

◆ type

TermType smt_terms::STerm::type

Definition at line 123 of file term.hpp.

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