#include <cassert>
#include <gmp.h>
#include <mathsat_conv.h>
#include <sstream>
#include <string>
#include <util/lang/c_types.h>
#include <util/expr/expr_util.h>

Include dependency graph for mathsat_conv.cpp:

Macros
#define	new_ast new_solver_ast<mathsat_smt_ast>

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

Variables
static const char *	mathsat_config

Macro Definition Documentation

◆ new_ast

#define new_ast new_solver_ast<mathsat_smt_ast>

Function Documentation

◆ create_new_mathsat_solver()

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

Variable Documentation

◆ mathsat_config

const char* mathsat_config

static

Initial value:

=
  "preprocessor.toplevel_propagation = true\n"
  "preprocessor.simplification = 1\n"
  "dpll.branching_random_frequency = 0.01\n"
  "dpll.branching_random_invalidate_phase_cache = true\n"
  "dpll.restart_strategy = 3\n"
  "dpll.glucose_var_activity = true\n"
  "dpll.glucose_learnt_minimization = true\n"
  "dpll.preprocessor.mode = 1\n"
  "theory.bv.eager = true\n"
  "theory.bv.bit_blast_mode = 2\n"
  "theory.bv.delay_propagated_eqs = true\n"
  "theory.la.enabled = false\n"
  "theory.fp.mode = 1\n"
  "theory.fp.bit_blast_mode = 2\n"
  "theory.fp.bv_combination_enabled = true\n"
  "theory.arr.enable_witness = true"

Macros