foreign(init, c, init).
foreign(reset, c, reset).
foreign(mk_var, c, mk_var(+term, +string, [-integer])). % creates a variable; first argument is an atom of the type,
foreign(mk_bounded_var, c, mk_bounded_var(+term, +string, [-integer])).
foreign(mk_empty_set, c, mk_empty_set(+term, [-integer])).
foreign(mk_int_const, c, mk_int_const(+integer, [-integer])). % creates an int constant
foreign(mk_bool_const, c, mk_bool_const(+string, [-integer])). % creates a bool constant
foreign(mk_string_const, c, mk_string_const(+atom, [-integer])).
foreign(mk_set, c, mk_set(+term, [-integer])).
foreign(mk_sort, c, mk_sort(+atom)).
foreign(mk_sort_with_cardinality, c, mk_sort_with_cardinality(+atom,+integer)).
foreign(mk_record_const, c, mk_record_const(+term, +term, [-integer])).
foreign(mk_record_field, c, mk_record_field(+integer, +integer, +atom, [-integer])).
foreign(setup_enumerated_set, c, setup_enumerated_set(+term)).
foreign(mk_op, c, mk_op(+string, +integer, +integer, [-integer])).
foreign(mk_quantifier, c, mk_quantifier(+string, +term, +integer, [-integer])).
foreign(mk_op_arglist, c, mk_op_arglist(+string, +term, [-integer])).
foreign(smt_solve_query, c, smt_solve_query(+integer,+integer,[-atom])).
foreign(get_model_string, c, get_model_string(+integer, [-atom])).
foreign(conjoin_negated_state, c, conjoin_negated_state(+term,+integer,[-integer])).
foreign(pop_frame, c, pop_frame).
foreign(push_frame, c, push_frame).
foreign(add_interpreter_constraint, c, add_interpreter_constraint(+integer,+atom,+integer,[-term])).
foreign(mk_couple, c, mk_couple(+term,+integer,+integer,[-integer])).