smtlib_conv.cpp File Reference

#include <smtlib_conv.h>
#include <smtlib.hpp>
#include <smtlib_tok.hpp>
#include <solvers/smt/tuple/smt_tuple_node.h>
#include <cinttypes>
#include <regex>
#include <sstream>
#include <unistd.h>
#include <signal.h>
#include <sys/wait.h>

Include dependency graph for smtlib_conv.cpp:

Macros
#define	__STDC_FORMAT_MACROS

Functions
int	smtlibparse (int startval)
smt_solver_baset *	create_new_smtlib_solver (const optionst &options, const namespacet &ns, tuple_iface **tuple_api, array_iface **array_api, fp_convt **fp_api)
static std::string	quote_smtlib_symbol (const std::string &name)
static BigInt	interp_numeric (const sexpr &respval)
static std::string	read_all (FILE *in)
int	smtliberror (int startsym, const std::string &error)

Variables
static const std::array	smt_func_name_table
	Mapping of SMT function IDs to their names.
int	smtlib_send_start_code
sexpr *	smtlib_output

Macro Definition Documentation

__STDC_FORMAT_MACROS

#define __STDC_FORMAT_MACROS

Function Documentation

create_new_smtlib_solver()

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

interp_numeric()

BigInt interp_numeric ( const sexpr & respval )

static

quote_smtlib_symbol()

std::string quote_smtlib_symbol ( const std::string & name )

static

read_all()

std::string read_all ( FILE * in )

static

smtliberror()

int smtliberror	(	int	startsym,
		const std::string &	error )

smtlibparse()

int smtlibparse

(

int

startval

)

Variable Documentation

smt_func_name_table

const std::array smt_func_name_table

static

Mapping of SMT function IDs to their names.

smtlib_output

sexpr* smtlib_output

extern

smtlib_send_start_code

int smtlib_send_start_code

extern