term.hpp File Reference

#include "barretenberg/smt_verification/solver/solver.hpp"

Go to the source code of this file.

Classes
class	smt_terms::STerm
	Symbolic term element class. More...

Namespaces
namespace	smt_terms

Enumerations
enum class	smt_terms::TermType {   smt_terms::FFTerm , smt_terms::FFITerm , smt_terms::BVTerm , smt_terms::ITerm ,   smt_terms::SBool , smt_terms::STuple , smt_terms::SymArray , smt_terms::SymSet }
	Allows to define three types of symbolic terms STerm - Symbolic Variables acting like a Finte Field elements FFITerm - Symbolic Variables acting like integers modulo prime ITerm - Symbolic Variables acting like integers BVTerm - Symbolic Variables acting like bitvectors modulo prime. More...
enum class	smt_terms::OpType : int32_t {   smt_terms::ADD , smt_terms::SUB , smt_terms::MUL , smt_terms::DIV ,   smt_terms::NEG , smt_terms::XOR , smt_terms::AND , smt_terms::OR ,   smt_terms::GT , smt_terms::GE , smt_terms::LT , smt_terms::LE ,   smt_terms::MOD , smt_terms::RSH , smt_terms::LSH , smt_terms::ROTR ,   smt_terms::ROTL , smt_terms::NOT , smt_terms::EXTRACT , smt_terms::BITVEC_PAD ,   smt_terms::BIT_SUM }

Functions
std::ostream &	smt_terms::operator<< (std::ostream &os, const TermType type)
STerm	smt_terms::operator+ (const bb::fr &lhs, const STerm &rhs)
STerm	smt_terms::operator- (const bb::fr &lhs, const STerm &rhs)
STerm	smt_terms::operator* (const bb::fr &lhs, const STerm &rhs)
STerm	smt_terms::operator/ (const bb::fr &lhs, const STerm &rhs)
void	smt_terms::operator== (const bb::fr &lhs, const STerm &rhs)
void	smt_terms::operator!= (const bb::fr &lhs, const STerm &rhs)
STerm	smt_terms::operator^ (const bb::fr &lhs, const STerm &rhs)
STerm	smt_terms::operator& (const bb::fr &lhs, const STerm &rhs)
STerm	smt_terms::operator| (const bb::fr &lhs, const STerm &rhs)
STerm	smt_terms::FFVar (const std::string &name, Solver *slv)
STerm	smt_terms::FFConst (const std::string &val, Solver *slv, uint32_t base)
STerm	smt_terms::FFConst (const bb::fr &val, Solver *slv)
STerm	smt_terms::FFIVar (const std::string &name, Solver *slv)
STerm	smt_terms::FFIConst (const std::string &val, Solver *slv, uint32_t base)
STerm	smt_terms::FFIConst (const bb::fr &val, Solver *slv)
STerm	smt_terms::IVar (const std::string &name, Solver *slv)
STerm	smt_terms::IConst (const std::string &val, Solver *slv, uint32_t base)
STerm	smt_terms::IConst (const bb::fr &val, Solver *slv)
STerm	smt_terms::BVVar (const std::string &name, Solver *slv)
STerm	smt_terms::BVConst (const std::string &val, Solver *slv, uint32_t base)
STerm	smt_terms::BVConst (const bb::fr &val, Solver *slv)

Variables
const std::unordered_map< TermType, std::unordered_map< OpType, cvc5::Kind > >	smt_terms::typed_operations
	precomputed map that contains allowed operations for each of three symbolic types