yices_conv.cpp File Reference

#include <cstddef>
#include <cstdarg>
#include <cstdint>
#include <sstream>
#include <util/arith/mp_arith.h>
#include <yices_conv.h>
#include <assert.h>

Include dependency graph for yices_conv.cpp:

Macros
#define	new_ast   new_solver_ast<yices_smt_ast>

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

Macro Definition Documentation

new_ast

#define new_ast   new_solver_ast<yices_smt_ast>

Function Documentation

create_new_yices_solver()

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