smt_terms Namespace Reference

Classes
class	Bool
	Bool element class. More...
class	STerm
	Symbolic term element class. More...
class	STuple
	sym Tuple class More...
class	SymArray
	symbolic Array class More...
class	SymSet
	symbolic Set class More...

Concepts
concept	ConstructibleFromTerm

Enumerations
enum class	TermType {   FFTerm , FFITerm , BVTerm , ITerm ,   SBool , STuple , SymArray , 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	OpType : int32_t {   ADD , SUB , MUL , DIV ,   NEG , XOR , AND , OR ,   GT , GE , LT , LE ,   MOD , RSH , LSH , ROTR ,   ROTL , NOT , EXTRACT , BITVEC_PAD ,   BIT_SUM }

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

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

Enumeration Type Documentation

OpType

enum class smt_terms::OpType : int32_t

strong

Enumerator
ADD
SUB
MUL
DIV
NEG
XOR
AND
OR
GT
GE
LT
LE
MOD
RSH
LSH
ROTR
ROTL
NOT
EXTRACT
BITVEC_PAD
BIT_SUM

Definition at line 18 of file term.hpp.

TermType

enum class smt_terms::TermType

strong

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.

Enumerator
FFTerm
FFITerm
BVTerm
ITerm
SBool
STuple
SymArray
SymSet

Definition at line 15 of file term.hpp.

Function Documentation

BVConst() [1/2]

STerm smt_terms::BVConst	(	const bb::fr &	val,
		Solver *	slv
	)

Definition at line 625 of file term.cpp.

BVConst() [2/2]

STerm smt_terms::BVConst	(	const std::string &	val,
		Solver *	slv,
		uint32_t	base
	)

Definition at line 620 of file term.cpp.

BVVar()

STerm smt_terms::BVVar	(	const std::string &	name,
		Solver *	slv
	)

Definition at line 615 of file term.cpp.

FFConst() [1/2]

STerm smt_terms::FFConst	(	const bb::fr &	val,
		Solver *	slv
	)

Definition at line 580 of file term.cpp.

FFConst() [2/2]

STerm smt_terms::FFConst	(	const std::string &	val,
		Solver *	slv,
		uint32_t	base
	)

Definition at line 575 of file term.cpp.

FFIConst() [1/2]

STerm smt_terms::FFIConst	(	const bb::fr &	val,
		Solver *	slv
	)

Definition at line 595 of file term.cpp.

FFIConst() [2/2]

STerm smt_terms::FFIConst	(	const std::string &	val,
		Solver *	slv,
		uint32_t	base
	)

Definition at line 590 of file term.cpp.

FFIVar()

STerm smt_terms::FFIVar	(	const std::string &	name,
		Solver *	slv
	)

Definition at line 585 of file term.cpp.

FFVar()

STerm smt_terms::FFVar	(	const std::string &	name,
		Solver *	slv
	)

Definition at line 570 of file term.cpp.

IConst() [1/2]

STerm smt_terms::IConst	(	const bb::fr &	val,
		Solver *	slv
	)

Definition at line 610 of file term.cpp.

IConst() [2/2]

STerm smt_terms::IConst	(	const std::string &	val,
		Solver *	slv,
		uint32_t	base
	)

Definition at line 605 of file term.cpp.

IVar()

STerm smt_terms::IVar	(	const std::string &	name,
		Solver *	slv
	)

Definition at line 600 of file term.cpp.

operator!=()

void smt_terms::operator!=	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 531 of file term.cpp.

operator&()

STerm smt_terms::operator&	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 511 of file term.cpp.

operator*()

STerm smt_terms::operator*	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 501 of file term.cpp.

operator+()

STerm smt_terms::operator+	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 491 of file term.cpp.

operator-()

STerm smt_terms::operator-	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 496 of file term.cpp.

operator/()

STerm smt_terms::operator/	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 521 of file term.cpp.

operator<<()

std::ostream & smt_terms::operator<<	(	std::ostream &	os,
		const TermType	type
	)

Definition at line 536 of file term.cpp.

operator==()

void smt_terms::operator==	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 526 of file term.cpp.

operator^()

STerm smt_terms::operator^	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 506 of file term.cpp.

operator|()

STerm smt_terms::operator|	(	const bb::fr &	lhs,
		const STerm &	rhs
	)

Definition at line 516 of file term.cpp.

Variable Documentation

typed_operations

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

Definition at line 47 of file term.hpp.