smt_bit_vector_theoryt::unsigned_greater_thant Struct Reference

#include <smt_bit_vector_theory.h>

Static Public Member Functions
static const char *	identifier ()
static smt_sortt	return_sort (const smt_termt &lhs, const smt_termt &rhs)
static void	validate (const smt_termt &lhs, const smt_termt &rhs)

Detailed Description

Definition at line 125 of file smt_bit_vector_theory.h.

Member Function Documentation

identifier()

const char * smt_bit_vector_theoryt::unsigned_greater_thant::identifier ( )

static

Definition at line 318 of file smt_bit_vector_theory.cpp.

return_sort()

smt_sortt smt_bit_vector_theoryt::unsigned_greater_thant::return_sort ( const smt_termt &  lhs, const smt_termt &  rhs  )

static

Definition at line 323 of file smt_bit_vector_theory.cpp.

validate()

void smt_bit_vector_theoryt::unsigned_greater_thant::validate ( const smt_termt &  lhs, const smt_termt &  rhs  )

static

Definition at line 330 of file smt_bit_vector_theory.cpp.

---

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

• /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/smt2_incremental/smt_bit_vector_theory.h
• /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp