neurosym_conv.cpp File Reference

#include <solvers/neurosym/neurosym_conv.h>
#include <solvers/smtlib/oneshot_process.h>
#include <util/arith/mp_arith.h>
#include <util/message/message.h>
#include <algorithm>
#include <cctype>
#include <cstdio>
#include <cstdlib>

Include dependency graph for neurosym_conv.cpp:

Functions
static std::string	prog_command (const optionst &options)
static void	skip_ws (const std::string &s, size_t &pos)
static void	skip_paren_group (const std::string &s, size_t &pos)
static std::string	read_token (const std::string &s, size_t &pos)
static std::string	unescape_smtlib_name (const std::string &s)
static bool	parse_define_fun (const std::string &s, size_t &pos, std::string &name, std::string &value)
static bool	numeric_value (const std::string &v, bool is_signed, BigInt &out)
static BigInt	mask_to_width (const BigInt &val, std::size_t width)
static BigInt	to_signed (const BigInt &unsigned_val, std::size_t width)
template<typename F>
static BigInt	bitwise_bv (const BigInt &a, const BigInt &b, std::size_t width, F &&bit)
static std::optional< BigInt >	eval_bv_binop (smt_func_kind kind, const BigInt &lhs, const BigInt &rhs, std::size_t width)
static std::optional< bool >	eval_bv_compare (smt_func_kind kind, const BigInt &lhs, const BigInt &rhs, std::size_t width)
smt_solver_baset *	create_new_neurosym_solver (const optionst &options, const namespacet &ns, tuple_iface **tuple_api, array_iface **array_api, fp_convt **fp_api)

Function Documentation

bitwise_bv()

template<typename F>

BigInt bitwise_bv ( const BigInt & a, const BigInt & b, std::size_t width, F && bit )

static

create_new_neurosym_solver()

smt_solver_baset * create_new_neurosym_solver	(	const optionst &	options,
		const namespacet &	ns,
		tuple_iface **	tuple_api,
		array_iface **	array_api,
		fp_convt **	fp_api )

eval_bv_binop()

std::optional< BigInt > eval_bv_binop ( smt_func_kind kind, const BigInt & lhs, const BigInt & rhs, std::size_t width )

static

eval_bv_compare()

std::optional< bool > eval_bv_compare ( smt_func_kind kind, const BigInt & lhs, const BigInt & rhs, std::size_t width )

static

mask_to_width()

BigInt mask_to_width ( const BigInt & val, std::size_t width )

static

numeric_value()

bool numeric_value ( const std::string & v, bool is_signed, BigInt & out )

static

parse_define_fun()

bool parse_define_fun ( const std::string & s, size_t & pos, std::string & name, std::string & value )

static

prog_command()

std::string prog_command ( const optionst & options )

static

read_token()

std::string read_token ( const std::string & s, size_t & pos )

static

skip_paren_group()

void skip_paren_group ( const std::string & s, size_t & pos )

static

skip_ws()

void skip_ws ( const std::string & s, size_t & pos )

static

to_signed()

BigInt to_signed ( const BigInt & unsigned_val, std::size_t width )

static

unescape_smtlib_name()

std::string unescape_smtlib_name ( const std::string & s )

static