mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 10:35:33 +00:00
Code Activity

remove deprecated user-theory plugins and other unused functionality from API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-20 08:43:27 -08:00
parent e96d93ee42
commit 665af3d8b9
11 changed files with 2 additions and 2090 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_project.py
View file

@ -51,7 +51,6 @@ def init_project_def():
add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
add_lib('user_plugin', ['smt'], 'smt/user_plugin')
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
add_lib('fuzzing', ['ast'], 'test/fuzzing')
add_lib('smt_tactic', ['smt'], 'smt/tactic')
@ -78,7 +77,7 @@ def init_project_def():
add_lib('smtparser', ['portfolio'], 'parsers/smt')
add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')
API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h']
add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure', 'interp', 'opt'],
add_lib('api', ['portfolio', 'smtparser', 'realclosure', 'interp', 'opt'],
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False)

65
src/api/api_context.cpp
View file

@ -37,23 +37,6 @@ namespace api {
exit(1);
}
Z3_search_failure mk_Z3_search_failure(smt::failure f) {
switch(f) {
case smt::OK: return Z3_NO_FAILURE;
case smt::UNKNOWN: return Z3_UNKNOWN;
case smt::TIMEOUT: return Z3_TIMEOUT;
case smt::MEMOUT: return Z3_MEMOUT_WATERMARK;
case smt::CANCELED: return Z3_CANCELED;
case smt::NUM_CONFLICTS: return Z3_NUM_CONFLICTS;
case smt::THEORY: return Z3_THEORY;
case smt::QUANTIFIERS: return Z3_QUANTIFIERS;
default:
UNREACHABLE();
break;
}
return static_cast<Z3_search_failure>(f);
}
context::add_plugins::add_plugins(ast_manager & m) {
reg_decl_plugins(m);
}
@ -94,7 +77,6 @@ namespace api {
m_ast_trail(m()),
m_replay_stack() {
m_solver = 0;
m_error_code = Z3_OK;
m_print_mode = Z3_PRINT_SMTLIB_FULL;
m_searching = false;
@ -133,7 +115,6 @@ namespace api {
m_ast_trail.reset();
}
reset_parser();
dealloc(m_solver);
}
void context::interrupt() {
@ -302,52 +283,6 @@ namespace api {
}
}
// ------------------------
//
// Solver interface for backward compatibility
//
// ------------------------
smt::kernel & context::get_smt_kernel() {
if (!m_solver) {
m_fparams.updt_params(m_params);
m_solver = alloc(smt::kernel, m(), m_fparams);
}
return *m_solver;
}
void context::assert_cnstr(expr * a) {
get_smt_kernel().assert_expr(a);
}
lbool context::check(model_ref & m) {
flet<bool> searching(m_searching, true);
lbool r;
r = get_smt_kernel().check();
if (r != l_false)
get_smt_kernel().get_model(m);
return r;
}
void context::push() {
get_smt_kernel().push();
m_ast_lim.push_back(m_ast_trail.size());
m_replay_stack.push_back(0);
}
void context::pop(unsigned num_scopes) {
for (unsigned i = 0; i < num_scopes; ++i) {
unsigned sz = m_ast_lim.back();
m_ast_lim.pop_back();
dealloc(m_replay_stack.back());
m_replay_stack.pop_back();
while (m_ast_trail.size() > sz) {
m_ast_trail.pop_back();
}
}
SASSERT(num_scopes <= get_smt_kernel().get_scope_level());
get_smt_kernel().pop(num_scopes);
}
// ------------------------
//

9
src/api/api_context.h
View file

@ -44,7 +44,6 @@ namespace realclosure {
};
namespace api {
Z3_search_failure mk_Z3_search_failure(smt::failure f);
class context : public tactic_manager {
@ -62,7 +61,6 @@ namespace api {
// Support for old solver API
smt_params m_fparams;
smt::kernel * m_solver; // General purpose solver for backward compatibility
// -------------------------------
ast_ref_vector m_last_result; //!< used when m_user_ref_count == true
@ -210,13 +208,6 @@ namespace api {
//
// ------------------------
smt_params & fparams() { return m_fparams; }
bool has_solver() const { return m_solver != 0; }
smt::kernel & get_smt_kernel();
void assert_cnstr(expr * a);
lbool check(model_ref & m);
void push();
void pop(unsigned num_scopes);
unsigned get_num_scopes() const { return m_ast_lim.size(); }
// ------------------------
//

333
src/api/api_user_theory.cpp
View file

@ -1,333 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
api_user_theory.cpp
Abstract:
API for external theories
Author:
Leonardo de Moura (leonardo) 2012-02-29.
Revision History:
--*/
#include<iostream>
#include"z3.h"
#include"api_log_macros.h"
#include"api_context.h"
#include"api_util.h"
#include"user_smt_theory.h"
smt::user_theory * mk_t(Z3_theory t) {
return reinterpret_cast<smt::user_theory*>(t);
}
extern "C" {
///////////////////////////////
// Theory plugin
// No support for logging
Z3_theory Z3_mk_theory(Z3_context c, Z3_string th_name, void * ext_data) {
Z3_TRY;
RESET_ERROR_CODE();
if (mk_c(c)->get_smt_kernel().get_scope_level() > 0) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
return 0;
}
return reinterpret_cast<Z3_theory>(mk_user_theory(mk_c(c)->get_smt_kernel(), c, ext_data, th_name));
Z3_CATCH_RETURN(0);
}
void * Z3_theory_get_ext_data(Z3_theory t) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
void * r = mk_t(t)->get_ext_data();
return r;
Z3_CATCH_RETURN(0);
}
Z3_sort Z3_theory_mk_sort(Z3_context c, Z3_theory t, Z3_symbol s) {
Z3_TRY;
RESET_ERROR_CODE();
sort * r = mk_t(t)->mk_sort(to_symbol(s));
mk_c(c)->save_ast_trail(r);
return of_sort(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_theory_mk_value(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s) {
Z3_TRY;
RESET_ERROR_CODE();
func_decl * d = mk_t(t)->mk_value_decl(to_symbol(n), to_sort(s));
app * r = mk_c(c)->m().mk_const(d);
mk_c(c)->save_ast_trail(r);
return of_ast(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_theory_mk_constant(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s) {
Z3_TRY;
RESET_ERROR_CODE();
Z3_func_decl d = Z3_theory_mk_func_decl(c, t, n, 0, 0, s);
app * r = mk_c(c)->m().mk_const(to_func_decl(d));
mk_c(c)->save_ast_trail(r);
return of_ast(r);
Z3_CATCH_RETURN(0);
}
Z3_func_decl Z3_theory_mk_func_decl(Z3_context c, Z3_theory t, Z3_symbol n,
unsigned domain_size, Z3_sort const domain[],
Z3_sort range) {
Z3_TRY;
RESET_ERROR_CODE();
func_decl * r = mk_t(t)->mk_func_decl(to_symbol(n), domain_size, to_sorts(domain), to_sort(range));
mk_c(c)->save_ast_trail(r);
return of_func_decl(r);
Z3_CATCH_RETURN(0);
}
Z3_context Z3_theory_get_context(Z3_theory t) {
Z3_context c = reinterpret_cast<Z3_context>(mk_t(t)->get_ext_context());
RESET_ERROR_CODE();
return c;
}
void Z3_set_delete_callback(Z3_theory t, Z3_theory_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_delete_fptr(reinterpret_cast<smt::theory_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_reduce_app_callback(Z3_theory t, Z3_reduce_app_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_reduce_app_fptr(reinterpret_cast<reduce_app_fptr>(f));
Z3_CATCH;
}
void Z3_set_reduce_eq_callback(Z3_theory t, Z3_reduce_eq_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_reduce_eq_fptr(reinterpret_cast<reduce_eq_fptr>(f));
Z3_CATCH;
}
void Z3_set_reduce_distinct_callback(Z3_theory t, Z3_reduce_distinct_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_reduce_distinct_fptr(reinterpret_cast<reduce_distinct_fptr>(f));
Z3_CATCH;
}
void Z3_set_new_app_callback(Z3_theory t, Z3_theory_ast_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_new_app_fptr(reinterpret_cast<smt::theory_app_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_new_elem_callback(Z3_theory t, Z3_theory_ast_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_new_elem_fptr(reinterpret_cast<smt::theory_app_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_init_search_callback(Z3_theory t, Z3_theory_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_init_search_fptr(reinterpret_cast<smt::theory_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_push_callback(Z3_theory t, Z3_theory_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_push_fptr(reinterpret_cast<smt::theory_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_pop_callback(Z3_theory t, Z3_theory_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_pop_fptr(reinterpret_cast<smt::theory_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_restart_callback(Z3_theory t, Z3_theory_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_restart_fptr(reinterpret_cast<smt::theory_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_reset_callback(Z3_theory t, Z3_theory_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_reset_fptr(reinterpret_cast<smt::theory_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_final_check_callback(Z3_theory t, Z3_theory_final_check_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_final_check_fptr(reinterpret_cast<smt::theory_final_check_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_new_eq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_new_eq_fptr(reinterpret_cast<smt::theory_app_app_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_new_diseq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_new_diseq_fptr(reinterpret_cast<smt::theory_app_app_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_new_assignment_callback(Z3_theory t, Z3_theory_ast_bool_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_new_assignment_fptr(reinterpret_cast<smt::theory_app_bool_callback_fptr>(f));
Z3_CATCH;
}
void Z3_set_new_relevant_callback(Z3_theory t, Z3_theory_ast_callback_fptr f) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->set_new_relevant_fptr(reinterpret_cast<smt::theory_app_callback_fptr>(f));
Z3_CATCH;
}
void Z3_theory_assert_axiom(Z3_theory t, Z3_ast ax) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->assert_axiom(to_ast(ax));
Z3_CATCH;
}
void Z3_theory_assume_eq(Z3_theory t, Z3_ast lhs, Z3_ast rhs) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->assume_eq(to_ast(lhs), to_ast(rhs));
Z3_CATCH;
}
void Z3_theory_enable_axiom_simplification(Z3_theory t, Z3_bool flag) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
mk_t(t)->enable_axiom_simplification(flag == Z3_TRUE);
Z3_CATCH;
}
Z3_ast Z3_theory_get_eqc_root(Z3_theory t, Z3_ast n) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return of_ast(mk_t(t)->get_root(to_ast(n)));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_theory_get_eqc_next(Z3_theory t, Z3_ast n) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return of_ast(mk_t(t)->get_next(to_ast(n)));
Z3_CATCH_RETURN(0);
}
unsigned Z3_theory_get_num_parents(Z3_theory t, Z3_ast n) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return mk_t(t)->get_num_parents(to_ast(n));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_theory_get_parent(Z3_theory t, Z3_ast n, unsigned i) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return of_ast(mk_t(t)->get_parent(to_ast(n), i));
Z3_CATCH_RETURN(0);
}
unsigned Z3_theory_get_num_elems(Z3_theory t) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return mk_t(t)->get_num_asts();
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_theory_get_elem(Z3_theory t, unsigned i) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return of_ast(mk_t(t)->get_ast(i));
Z3_CATCH_RETURN(0);
}
unsigned Z3_theory_get_num_apps(Z3_theory t) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return mk_t(t)->get_num_parents();
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_theory_get_app(Z3_theory t, unsigned i) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return of_ast(mk_t(t)->get_parent(i));
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_theory_is_value(Z3_theory t, Z3_ast n) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return is_app(to_ast(n)) && mk_t(t)->get_family_id() == to_app(to_ast(n))->get_family_id();
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_theory_is_decl(Z3_theory t, Z3_func_decl d) {
Z3_context c = Z3_theory_get_context(t);
Z3_TRY;
RESET_ERROR_CODE();
return mk_t(t)->get_family_id() == to_func_decl(d)->get_family_id();
Z3_CATCH_RETURN(Z3_FALSE);
}
};

391
src/api/z3_api.h
View file

@ -24,7 +24,6 @@ Copyright (c) 2015 Microsoft Corporation
#ifdef CorML3
DEFINE_TYPE(Z3_symbol);
DEFINE_TYPE(Z3_literals);
DEFINE_TYPE(Z3_theory);
DEFINE_TYPE(Z3_config);
DEFINE_TYPE(Z3_context);
DEFINE_TYPE(Z3_sort);
@ -55,7 +54,6 @@ DEFINE_TYPE(Z3_func_entry);
DEFINE_TYPE(Z3_fixedpoint);
DEFINE_TYPE(Z3_optimize);
DEFINE_TYPE(Z3_rcf_num);
DEFINE_VOID(Z3_theory_data);
#endif
#ifndef __int64
@ -1250,7 +1248,7 @@ typedef enum {
Z3_PK_INVALID
} Z3_param_kind;
#ifdef CorML3
#if 0
/**
\mlonly {!search_failure} \endmlonly \conly \brief
The different kinds of search failure types.
@ -1345,8 +1343,6 @@ typedef enum
def_Type('LITERALS', 'Z3_literals', 'Literals')
def_Type('CONSTRUCTOR', 'Z3_constructor', 'Constructor')
def_Type('CONSTRUCTOR_LIST', 'Z3_constructor_list', 'ConstructorList')
def_Type('THEORY', 'Z3_theory', 'ctypes.c_void_p')
def_Type('THEORY_DATA', 'Z3_theory_data', 'ctypes.c_void_p')
def_Type('SOLVER', 'Z3_solver', 'SolverObj')
def_Type('GOAL', 'Z3_goal', 'GoalObj')
def_Type('TACTIC', 'Z3_tactic', 'TacticObj')
@ -5389,391 +5385,6 @@ END_MLAPI_EXCLUDE
/*@}*/
#ifdef CorML3
/**
@name External Theory Plugins
*/
/*@{*/
#ifdef Conly
//
// callbacks and void* don't work with CAMLIDL.
//
typedef Z3_bool Z3_reduce_eq_callback_fptr(Z3_theory t, Z3_ast a, Z3_ast b, Z3_ast * r);
typedef Z3_bool Z3_reduce_app_callback_fptr(Z3_theory, Z3_func_decl, unsigned, Z3_ast const [], Z3_ast *);
typedef Z3_bool Z3_reduce_distinct_callback_fptr(Z3_theory, unsigned, Z3_ast const [], Z3_ast *);
typedef void Z3_theory_callback_fptr(Z3_theory t);
typedef Z3_bool Z3_theory_final_check_callback_fptr(Z3_theory);
typedef void Z3_theory_ast_callback_fptr(Z3_theory, Z3_ast);
typedef void Z3_theory_ast_bool_callback_fptr(Z3_theory, Z3_ast, Z3_bool);
typedef void Z3_theory_ast_ast_callback_fptr(Z3_theory, Z3_ast, Z3_ast);
#endif
#ifdef Conly
/**
\brief Create a new user defined theory. The new theory will be identified by the name \c th_name.
A theory must be created before asserting any assertion to the given context.
\conly Return \c NULL in case of failure.
\conly \c data is a pointer to an external data-structure that may be used to store
\conly theory specific additional data.
*/
Z3_theory Z3_API Z3_mk_theory(Z3_context c, Z3_string th_name, Z3_theory_data data);
/**
\brief Return a pointer to the external data-structure supplied to the function #Z3_mk_theory.
\see Z3_mk_theory
*/
Z3_theory_data Z3_API Z3_theory_get_ext_data(Z3_theory t);
#endif
/**
\brief Create an interpreted theory sort.
*/
Z3_sort Z3_API Z3_theory_mk_sort(Z3_context c, Z3_theory t, Z3_symbol s);
/**
\brief Create an interpreted theory constant value. Values are assumed to be different from each other.
*/
Z3_ast Z3_API Z3_theory_mk_value(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s);
/**
\brief Create an interpreted constant for the given theory.
*/
Z3_ast Z3_API Z3_theory_mk_constant(Z3_context c, Z3_theory t, Z3_symbol n, Z3_sort s);
/**
\brief Create an interpreted function declaration for the given theory.
*/
Z3_func_decl Z3_API Z3_theory_mk_func_decl(Z3_context c, Z3_theory t, Z3_symbol n,
unsigned domain_size, Z3_sort const domain[],
Z3_sort range);
/**
\brief Return the context where the given theory is installed.
*/
Z3_context Z3_API Z3_theory_get_context(Z3_theory t);
#ifdef Conly
/**
\brief Set a callback that is invoked when theory \c t is deleted.
This callback should be used to delete external data-structures associated with the given theory.
\conly The callback has the form <tt>f(t)</tt>, where
\conly - \c t is the given theory
\see Z3_mk_theory
\conly \see Z3_theory_get_ext_data
*/
void Z3_API Z3_set_delete_callback(Z3_theory t, Z3_theory_callback_fptr f);
/**
\brief Set a callback for simplifying operators of the given theory.
The callback \c f is invoked by Z3's simplifier.
\conly It is of the form <tt>f(t, d, n, args, r)</tt>, where:
\conly - \c t is the given theory
\conly - \c d is the declaration of the theory operator
\conly - \c n is the number of arguments in the array \c args
\conly - \c args are arguments for the theory operator
\conly - \c r should contain the result: an expression equivalent to <tt>d(args[0], ..., args[n-1])</tt>.
\conly If <tt>f(t, d, n, args, r)</tt> returns false, then \c r is ignored, and Z3 assumes that no simplification was performed.
*/
void Z3_API Z3_set_reduce_app_callback(Z3_theory t, Z3_reduce_app_callback_fptr f);
/**
\brief Set a callback for simplifying the atom <tt>s_1 = s_2</tt>, when the
sort of \c s_1 and \c s_2 is an interpreted sort of the given theory.
The callback \c f is invoked by Z3's simplifier.
\conly It has the form <tt>f(t, s_1, s_2, r)</tt>, where:
\conly - \c t is the given theory
\conly - \c s_1 is the left-hand-side
\conly - \c s_2 is the right-hand-side
\conly - \c r should contain the result: an expression equivalent to <tt>s_1 = s_2</tt>.
\conly If <tt>f(t, s_1, s_2, r)</tt> returns false, then \c r is ignored, and Z3 assumes that no simplification was performed.
*/
void Z3_API Z3_set_reduce_eq_callback(Z3_theory t, Z3_reduce_eq_callback_fptr f);
/**
\brief Set a callback for simplifying the atom <tt>distinct(s_1, ..., s_n)</tt>, when the
sort of \c s_1, ..., \c s_n is an interpreted sort of the given theory.
The callback \c f is invoked by Z3's simplifier.
\conly It has the form <tt>f(t, n, args, r)</tt>, where:
\conly - \c t is the given theory
\conly - \c n is the number of arguments in the array \c args
\conly - \c args are arguments for distinct.
\conly - \c r should contain the result: an expression equivalent to <tt>distinct(s_1, ..., s_n)</tt>.
\conly If <tt>f(t, n, args, r)</tt> returns false, then \c r is ignored, and Z3 assumes that no simplification was performed.
*/
void Z3_API Z3_set_reduce_distinct_callback(Z3_theory t, Z3_reduce_distinct_callback_fptr f);
/**
\brief Set a callback that is invoked when a theory application
is finally added into the logical context. Note that, not every
application contained in an asserted expression is actually
added into the logical context because it may be simplified
during a preprocessing step.
\conly The callback has the form <tt>f(t, n)</tt>, where
\conly - \c t is the given theory
\conly - \c n is a theory application, that is, an expression of the form <tt>g(...)</tt> where \c g is a theory operator.
\remark An expression \c n added to the logical context at search level \c n,
will remain in the logical context until this level is backtracked.
*/
void Z3_API Z3_set_new_app_callback(Z3_theory t, Z3_theory_ast_callback_fptr f);
/**
\brief Set a callback that is invoked when an expression of
sort \c s, where \c s is an interpreted sort of the theory \c
t, is finally added into the logical context. Note that, not
every expression contained in an asserted expression is
actually added into the logical context because it may be
simplified during a preprocessing step.
\conly The callback has the form <tt>f(t, n)</tt>, where
\conly - \c t is the given theory
\conly - \c n is an expression of sort \c s, where \c s is an interpreted sort of \c t.
\remark An expression \c n added to the logical context at search level \c n,
will remain in the logical context until this level is backtracked.
*/
void Z3_API Z3_set_new_elem_callback(Z3_theory t, Z3_theory_ast_callback_fptr f);
/**
\brief Set a callback that is invoked when Z3 starts searching for a
satisfying assignment.
\conly The callback has the form <tt>f(t)</tt>, where
\conly - \c t is the given theory
*/
void Z3_API Z3_set_init_search_callback(Z3_theory t, Z3_theory_callback_fptr f);
/**
\brief Set a callback that is invoked when Z3 creates a
case-split (aka backtracking point).
When a case-split is created we say the search level is increased.
\conly The callback has the form <tt>f(t)</tt>, where
\conly - \c t is the given theory
*/
void Z3_API Z3_set_push_callback(Z3_theory t, Z3_theory_callback_fptr f);
/**
\brief Set a callback that is invoked when Z3 backtracks a
case-split.
When a case-split is backtracked we say the search level is decreased.
\conly The callback has the form <tt>f(t)</tt>, where
\conly - \c t is the given theory
*/
void Z3_API Z3_set_pop_callback(Z3_theory t, Z3_theory_callback_fptr f);
/**
\brief Set a callback that is invoked when Z3 restarts the
search for a satisfying assignment.
\conly The callback has the form <tt>f(t)</tt>, where
\conly - \c t is the given theory
*/
void Z3_API Z3_set_restart_callback(Z3_theory t, Z3_theory_callback_fptr f);
/**
\brief Set a callback that is invoked when the logical context
is reset by the user. This callback is useful for reseting any
data-structure maintained by the user theory solver.
\conly The callback has the form <tt>f(t)</tt>, where
\conly - \c t is the given theory
*/
void Z3_API Z3_set_reset_callback(Z3_theory t, Z3_theory_callback_fptr f);
/**
\brief Set a callback that is invoked before Z3 starts building a model.
A theory may use this callback to perform expensive operations.
\conly The callback has the form <tt>f(t)</tt>, where
\conly - \c t is the given theory
If the theory returns \mlonly \c false, \endmlonly \conly \c Z3_false,
Z3 will assume that theory is giving up,
and it will assume that it was not possible to decide if the asserted constraints
are satisfiable or not.
*/
void Z3_API Z3_set_final_check_callback(Z3_theory t, Z3_theory_final_check_callback_fptr f);
/**
\brief Set a callback that is invoked when an equality <tt>s_1 = s_2</tt>
is found by the logical context.
\conly The callback has the form <tt>f(t, s_1, s_2)</tt>, where:
\conly - \c t is the given theory
\conly - \c s_1 is the left-hand-side
\conly - \c s_2 is the right-hand-side
*/
void Z3_API Z3_set_new_eq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f);
/**
\brief Set a callback that is invoked when a disequality <tt>s_1 != s_2</tt>
is found by the logical context.
\conly The callback has the form <tt>f(t, s_1, s_2)</tt>, where:
\conly - \c t is the given theory
\conly - \c s_1 is the left-hand-side
\conly - \c s_2 is the right-hand-side
*/
void Z3_API Z3_set_new_diseq_callback(Z3_theory t, Z3_theory_ast_ast_callback_fptr f);
/**
\brief Set a callback that is invoked when a theory predicate is assigned to true/false by Z3.
\conly The callback has the form <tt>f(t, p, v)</tt>, where:
\conly - \c t is the given theory
\conly - \c p is the assigned predicate.
\conly - \c v is the value (true/false) assigned to \c p.
*/
void Z3_API Z3_set_new_assignment_callback(Z3_theory t, Z3_theory_ast_bool_callback_fptr f);
/**
\brief Set a callback that is invoked when an expression is
marked as relevant during the search. This callback is only
invoked when relevancy propagation is enabled.
\conly The callback has the form <tt>f(t, n)</tt>, where:
\conly - \c t is the given theory
\conly - \c n is the relevant expression
*/
void Z3_API Z3_set_new_relevant_callback(Z3_theory t, Z3_theory_ast_callback_fptr f);
#endif
/**
\brief Assert a theory axiom/lemmas during the search.
An axiom added at search level \c n will remain in the logical context until
level \c n is backtracked.
The callbacks for push (#Z3_set_push_callback) and pop
(#Z3_set_pop_callback) can be used to track when the search
level is increased (i.e., new case-split) and decreased (i.e.,
case-split is backtracked).
Z3 tracks the theory axioms asserted. So, multiple assertions of the same axiom are
ignored.
*/
void Z3_API Z3_theory_assert_axiom(Z3_theory t, Z3_ast ax);
/**
\brief Inform to the logical context that \c lhs and \c rhs have the same interpretation
in the model being built by theory \c t. If lhs = rhs is inconsistent with other theories,
then the logical context will backtrack.
For more information, see the paper "Model-Based Theory Combination" in the Z3 website.
*/
void Z3_API Z3_theory_assume_eq(Z3_theory t, Z3_ast lhs, Z3_ast rhs);
/**
\brief Enable/disable the simplification of theory axioms asserted using #Z3_theory_assert_axiom.
By default, the simplification of theory specific operators is disabled.
That is, the reduce theory callbacks are not invoked for theory axioms.
The default behavior is useful when asserting axioms stating properties of theory operators.
*/
void Z3_API Z3_theory_enable_axiom_simplification(Z3_theory t, Z3_bool flag);
/**
\brief Return the root of the equivalence class containing \c n.
*/
Z3_ast Z3_API Z3_theory_get_eqc_root(Z3_theory t, Z3_ast n);
/**
\brief Return the next element in the equivalence class containing \c n.
The elements in an equivalence class are organized in a circular list.
You can traverse the list by calling this function multiple times
using the result from the previous call. This is illustrated in the
code snippet below.
\code
Z3_ast curr = n;
do
curr = Z3_theory_get_eqc_next(theory, curr);
while (curr != n);
\endcode
*/
Z3_ast Z3_API Z3_theory_get_eqc_next(Z3_theory t, Z3_ast n);
/**
\brief Return the number of parents of \c n that are operators of the given theory.
*/
unsigned Z3_API Z3_theory_get_num_parents(Z3_theory t, Z3_ast n);
/**
\brief Return the i-th parent of \c n.
See #Z3_theory_get_num_parents.
*/
Z3_ast Z3_API Z3_theory_get_parent(Z3_theory t, Z3_ast n, unsigned i);
/**
\brief Return \c Z3_TRUE if \c n is an interpreted theory value.
*/
Z3_bool Z3_API Z3_theory_is_value(Z3_theory t, Z3_ast n);
/**
\brief Return \c Z3_TRUE if \c d is an interpreted theory declaration.
*/
Z3_bool Z3_API Z3_theory_is_decl(Z3_theory t, Z3_func_decl d);
/**
\brief Return the number of expressions of the given theory in
the logical context. These are the expressions notified using the
callback #Z3_set_new_elem_callback.
*/
unsigned Z3_API Z3_theory_get_num_elems(Z3_theory t);
/**
\brief Return the i-th elem of the given theory in the logical context.
\see Z3_theory_get_num_elems
*/
Z3_ast Z3_API Z3_theory_get_elem(Z3_theory t, unsigned i);
/**
\brief Return the number of theory applications in the logical
context. These are the expressions notified using the callback
#Z3_set_new_app_callback.
*/
unsigned Z3_API Z3_theory_get_num_apps(Z3_theory t);
/**
\brief Return the i-th application of the given theory in the logical context.
\see Z3_theory_get_num_apps
*/
Z3_ast Z3_API Z3_theory_get_app(Z3_theory t, unsigned i);
/*@}*/
#endif
#ifdef CorML4
/**
@name Fixedpoint facilities

97
src/smt/user_plugin/user_decl_plugin.cpp
View file

@ -1,97 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
user_decl_plugin.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2010-05-22.
Revision History:
--*/
#include"user_decl_plugin.h"
#include"warning.h"
user_decl_plugin::user_decl_plugin() {
}
void user_decl_plugin::finalize() {
m_manager->dec_array_ref(m_kind2func.size(), m_kind2func.c_ptr());
m_manager->dec_array_ref(m_kind2sort.size(), m_kind2sort.c_ptr());
}
decl_plugin * user_decl_plugin::mk_fresh() {
user_decl_plugin * p = alloc(user_decl_plugin);
// TODO copy sorts and other goodness
return p;
}
sort * user_decl_plugin::mk_sort(symbol const & name) {
unsigned kind = m_kind2sort.size();
sort * s = m_manager->mk_sort(name, sort_info(m_family_id, kind));
m_kind2sort.push_back(s);
m_manager->inc_ref(s);
if (!name.is_numerical()) {
m_sort_names.push_back(builtin_name(name.bare_str(), static_cast<decl_kind>(kind)));
}
return s;
}
func_decl * user_decl_plugin::mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) {
unsigned kind = m_kind2func.size();
func_decl * f = m_manager->mk_func_decl(name, arity, domain, range, func_decl_info(m_family_id, kind));
m_kind2func.push_back(f);
m_manager->inc_ref(f);
if (!name.is_numerical()) {
m_op_names.push_back(builtin_name(name.bare_str(), static_cast<decl_kind>(kind)));
}
return f;
}
func_decl * user_decl_plugin::mk_value_decl(symbol const & name, sort * s) {
func_decl * f = mk_func_decl(name, 0, 0, s);
m_values.insert(f);
return f;
}
sort * user_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
if (num_parameters > 0) {
throw default_exception("invalid user theory sort");
return 0;
}
return m_kind2sort.get(k, 0);
}
func_decl * user_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
func_decl * f = m_kind2func.get(k, 0);
if (num_parameters > 0 || f == 0) {
throw default_exception("invalid user theory function operator");
return 0;
}
return f;
}
bool user_decl_plugin::is_value(app * v) const {
return m_values.contains(v->get_decl());
}
bool user_decl_plugin::is_value(func_decl * f) const {
return m_values.contains(f);
}
void user_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
op_names.append(m_op_names);
}
void user_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
sort_names.append(m_sort_names);
}

62
src/smt/user_plugin/user_decl_plugin.h
View file

@ -1,62 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
user_decl_plugin.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2010-05-22.
Revision History:
--*/
#ifndef USER_DECL_PLUGIN_H_
#define USER_DECL_PLUGIN_H_
#include"ast.h"
#include"obj_hashtable.h"
class user_decl_plugin : public decl_plugin {
ptr_vector<sort> m_kind2sort;
ptr_vector<func_decl> m_kind2func;
obj_hashtable<func_decl> m_values;
svector<builtin_name> m_op_names;
svector<builtin_name> m_sort_names;
public:
user_decl_plugin();
virtual ~user_decl_plugin() {}
virtual void finalize();
virtual decl_plugin * mk_fresh();
sort * mk_sort(symbol const & name);
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range);
func_decl * mk_value_decl(symbol const & name, sort * s);
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual bool is_value(app*) const;
virtual bool is_unique_value(app * a) const { return is_value(a); }
bool is_value(func_decl *) const;
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
};
#endif /* USER_DECL_PLUGIN_H_ */

81
src/smt/user_plugin/user_simplifier_plugin.cpp
View file

@ -1,81 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
user_simplifier_plugin.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2010-05-22.
Revision History:
--*/
#include"user_simplifier_plugin.h"
#include"ast_pp.h"
#include"warning.h"
user_simplifier_plugin::user_simplifier_plugin(symbol const & fname, ast_manager & m):
simplifier_plugin(fname, m),
m_owner(0),
m_enabled(true),
m_reduce_app_fptr(0),
m_reduce_eq_fptr(0),
m_reduce_distinct_fptr(0) {
}
simplifier_plugin * user_simplifier_plugin::mk_fresh() {
ast_manager & m = get_manager();
user_simplifier_plugin * new_sp = alloc(user_simplifier_plugin, m.get_family_name(get_family_id()), m);
new_sp->m_reduce_app_fptr = m_reduce_app_fptr;
new_sp->m_reduce_eq_fptr = m_reduce_eq_fptr;
new_sp->m_reduce_distinct_fptr = m_reduce_distinct_fptr;
return new_sp;
}
bool user_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if (m_reduce_app_fptr == 0 || !m_enabled)
return false;
expr * _result = 0;
bool flag = m_reduce_app_fptr(m_owner, f, num_args, args, &_result);
if (flag) {
if (_result == 0)
throw default_exception("invalid reduce_app callback: result is null");
result = _result;
}
return flag;
}
bool user_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
if (m_reduce_eq_fptr == 0 || !m_enabled)
return false;
expr * _result = 0;
bool flag = m_reduce_eq_fptr(m_owner, lhs, rhs, &_result);
if (flag) {
if (_result == 0)
throw default_exception("invalid reduce_eq callback: result is null");
result = _result;
}
return flag;
}
bool user_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
if (m_reduce_distinct_fptr == 0 || !m_enabled)
return false;
expr * _result = 0;
bool flag = m_reduce_distinct_fptr(m_owner, num_args, args, &_result);
if (flag) {
if (_result == 0)
throw default_exception("invalid reduce_distinct callback: result is null");
result = _result;
}
return flag;
}
void user_simplifier_plugin::flush_caches() {
}

66
src/smt/user_plugin/user_simplifier_plugin.h
View file

@ -1,66 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
user_simplifier_plugin.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2010-05-22.
Revision History:
--*/
#ifndef USER_SIMPLIFIER_PLUGIN_H_
#define USER_SIMPLIFIER_PLUGIN_H_
#include"simplifier_plugin.h"
typedef bool (*reduce_app_fptr)(void *, func_decl *, unsigned, expr * const *, expr **);
typedef bool (*reduce_eq_fptr)(void *, expr *, expr *, expr **);
typedef bool (*reduce_distinct_fptr)(void *, unsigned, expr * const *, expr **);
class user_simplifier_plugin : public simplifier_plugin {
void * m_owner;
bool m_enabled;
reduce_app_fptr m_reduce_app_fptr;
reduce_eq_fptr m_reduce_eq_fptr;
reduce_distinct_fptr m_reduce_distinct_fptr;
public:
user_simplifier_plugin(symbol const & fname, ast_manager & m);
virtual simplifier_plugin * mk_fresh();
void set_reduce_app_fptr(reduce_app_fptr ptr) {
m_reduce_app_fptr = ptr;
}
void set_reduce_eq_fptr(reduce_eq_fptr ptr) {
m_reduce_eq_fptr = ptr;
}
void set_reduce_distinct_fptr(reduce_distinct_fptr ptr) {
m_reduce_distinct_fptr = ptr;
}
void enable(bool flag) { m_enabled = flag; }
void set_owner(void * ptr) { m_owner = ptr; }
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
virtual void flush_caches();
};
#endif /* USER_SIMPLIFIER_PLUGIN_H_ */

661
src/smt/user_plugin/user_smt_theory.cpp
View file

@ -1,661 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
user_smt_theory.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2010-05-22.
Revision History:
--*/
#include"smt_context.h"
#include"user_smt_theory.h"
#include"ast_pp.h"
#include"smt_model_generator.h"
#include"stats.h"
#include"warning.h"
namespace smt {
//
// value factory for user sorts.
//
// NB. This value factory for user theories
// does not address theories where model
// values are structured objects such as
// arrays, records, or data-types.
//
class user_smt_theory_factory : public simple_factory<unsigned> {
app* mk_value_core(unsigned const& val, sort* s) {
return m_manager.mk_model_value(val, s);
}
public:
user_smt_theory_factory(ast_manager& m, family_id fid):
simple_factory<unsigned>(m, fid)
{}
};
user_theory::user_theory(ast_manager & m, smt_params const& p, void * ext_context, void * ext_data, char const * name, family_id fid, user_decl_plugin * dp, user_simplifier_plugin * sp):
theory(fid),
m_params(p),
m_ext_context(ext_context),
m_ext_data(ext_data),
m_name(name),
m_simplify_axioms(false),
m_decl_plugin(dp),
m_simplifier_plugin(sp),
m_find(*this),
m_trail_stack(*this),
m_asserted_axioms(m),
m_persisted_axioms(m),
m_persisted_axioms_qhead(0),
m_delete_fptr(0),
m_new_app_fptr(0),
m_new_elem_fptr(0),
m_init_search_fptr(0),
m_push_fptr(0),
m_pop_fptr(0),
m_restart_fptr(0),
m_reset_fptr(0),
m_final_check_fptr(0),
m_new_eq_fptr(0),
m_new_diseq_fptr(0),
m_new_assignment_fptr(0),
m_new_relevant_fptr(0),
m_mk_fresh_fptr(0),
m_delete_invoking(false),
m_new_app_invoking(false),
m_new_elem_invoking(false),
m_init_search_invoking(false),
m_push_invoking(false),
m_pop_invoking(false),
m_restart_invoking(false),
m_reset_invoking(false),
m_final_check_invoking(false),
m_new_eq_invoking(false),
m_new_diseq_invoking(false),
m_new_assignment_invoking(false),
m_new_relevant_invoking(false) {
}
user_theory::~user_theory() {
if (m_delete_fptr != 0) {
flet<bool> i(m_delete_invoking, true);
m_delete_fptr(this);
}
}
theory * user_theory::mk_fresh(context * new_ctx) {
if (m_mk_fresh_fptr == 0) {
throw default_exception("The mk_fresh_ext_data callback was not set for user theory, you must use Z3_theory_set_mk_fresh_ext_data_callback");
return 0;
}
user_simplifier_plugin * new_sp = static_cast<user_simplifier_plugin*>(new_ctx->get_simplifier().get_plugin(get_family_id()));
SASSERT(new_sp != 0);
user_theory * new_th = alloc(user_theory, get_manager(), new_ctx->get_fparams(), m_ext_context, m_mk_fresh_fptr(this), get_name(), get_family_id(),
m_decl_plugin, new_sp);
new_sp->set_owner(new_th);
new_th->m_delete_fptr = m_delete_fptr;
new_th->m_new_app_fptr = m_new_app_fptr;
new_th->m_new_elem_fptr = m_new_elem_fptr;
new_th->m_init_search_fptr = m_init_search_fptr;
new_th->m_push_fptr = m_push_fptr;
new_th->m_pop_fptr = m_pop_fptr;
new_th->m_restart_fptr = m_restart_fptr;
new_th->m_reset_fptr = m_reset_fptr;
new_th->m_final_check_fptr = m_final_check_fptr;
new_th->m_new_eq_fptr = m_new_eq_fptr;
new_th->m_new_diseq_fptr = m_new_diseq_fptr;
new_th->m_new_assignment_fptr = m_new_assignment_fptr;
new_th->m_new_relevant_fptr = m_new_relevant_fptr;
new_th->m_mk_fresh_fptr = m_mk_fresh_fptr;
return new_th;
}
void user_theory::assert_axiom_core(app* a) {
if (m_asserted_axiom_set.contains(a)) {
return;
}
m_asserted_axiom_set.insert(a);
m_asserted_axioms.push_back(a);
if (m_params.m_user_theory_persist_axioms) {
m_persisted_axioms.push_back(a);
}
}
/**
TODO: discuss semantics of assert_axiom.
Should we simplify axiom of not?
*/
void user_theory::assert_axiom(ast * axiom) {
++m_stats.m_num_user_axioms;
TRACE("user_smt_theory", tout << mk_pp(axiom, get_manager()) << "\n";);
if (!is_expr(axiom)) {
throw default_exception("invalid expression");
}
if (!get_manager().is_bool(to_expr(axiom))) {
throw default_exception("invalid theory axiom: axioms must have Boolean sort");
}
if (!m_new_eq_invoking &&
!m_new_diseq_invoking &&
!m_new_assignment_invoking &&
!m_new_relevant_invoking &&
!m_final_check_invoking) {
throw default_exception("theory axioms can only be invoked during callbacks "
"for new (dis)equalities/assignments and final check");
}
context & ctx = get_context();
ast_manager & m = get_manager();
if (!is_app(axiom) || !to_app(axiom)->is_ground() ||
ctx.get_fparams().m_user_theory_preprocess_axioms) {
asserted_formulas asf(m, ctx.get_fparams());
asf.assert_expr(to_app(axiom));
asf.reduce();
unsigned sz = asf.get_num_formulas();
unsigned qhead = asf.get_qhead();
while (qhead < sz) {
expr * f = asf.get_formula(qhead);
assert_axiom_core(to_app(f));
++qhead;
}
}
else {
if (!m_simplify_axioms) {
m_simplifier_plugin->enable(false);
}
expr_ref s_axiom(m);
proof_ref pr(m);
simplifier & s = ctx.get_simplifier();
s(to_app(axiom), s_axiom, pr);
if (!is_app(s_axiom)) {
throw default_exception("invalid theory axiom: axioms must be applications");
}
axiom = s_axiom;
m_simplifier_plugin->enable(true);
assert_axiom_core(to_app(axiom));
}
}
void user_theory::assume_eq(ast * _lhs, ast * _rhs) {
if (!is_expr(_lhs) || !is_expr(_rhs)) {
throw default_exception("assume_eq must take expressions as arguments");
}
expr* lhs = to_expr(_lhs);
expr* rhs = to_expr(_rhs);
ast_manager& m = get_manager();
context& ctx = get_context();
if (m.is_true(rhs)) {
std::swap(lhs, rhs);
}
if (m.is_true(lhs)) {
theory_var v2 = mk_var(rhs);
if (v2 == null_theory_var) {
throw default_exception("invalid assume eq: lhs or rhs is not a theory term");
}
bool_var bv = ctx.get_bool_var(rhs);
ctx.set_true_first_flag(bv);
ctx.mark_as_relevant(get_enode(v2));
return;
}
if (m.is_bool(lhs)) {
throw default_exception("assume_eq on Booleans must take 'true' as one of the arguments");
}
theory_var v1 = mk_var(lhs);
theory_var v2 = mk_var(rhs);
if (v1 == null_theory_var || v2 == null_theory_var) {
throw default_exception("invalid assume eq: lhs or rhs is not a theory term");
}
ctx.assume_eq(get_enode(v1), get_enode(v2));
}
void user_theory::reset_propagation_queues() {
m_new_eqs.reset();
m_new_diseqs.reset();
m_new_assignments.reset();
m_new_relevant_apps.reset();
}
theory_var user_theory::get_var(ast * n) const {
if (!is_app(n))
return null_theory_var;
context & ctx = get_context();
if (ctx.e_internalized(to_app(n))) {
enode * e = ctx.get_enode(to_app(n));
return e->get_th_var(get_id());
}
return null_theory_var;
}
theory_var user_theory::mk_var(ast * n) {
theory_var v = get_var(n);
if (v != null_theory_var || !is_app(n)) {
return v;
}
app* a = to_app(n);
if (a->get_family_id() == get_id() &&
internalize_term(a)) {
return mk_var(get_context().get_enode(a));
}
return v;
}
ast * user_theory::get_root(ast * n) const {
theory_var v = get_var(n);
if (v != null_theory_var) {
theory_var r = m_find.find(v);
return get_ast(r);
}
return n;
}
ast * user_theory::get_next(ast * n) const {
theory_var v = get_var(n);
if (v != null_theory_var) {
theory_var r = m_find.next(v);
return get_ast(r);
}
return n;
}
void user_theory::shrink_use_list(unsigned sz) {
SASSERT(m_use_list.size() >= sz);
std::for_each(m_use_list.begin() + sz, m_use_list.end(), delete_proc<ptr_vector<app> >());
m_use_list.shrink(sz);
}
ptr_vector<app> * user_theory::get_non_null_use_list(theory_var v) {
SASSERT(v != null_theory_var);
if (m_use_list[v] == 0)
m_use_list[v] = alloc(ptr_vector<app>);
return m_use_list[v];
}
unsigned user_theory::get_num_parents(ast * n) const {
theory_var v = get_var(n);
if (v != null_theory_var && m_use_list[v] != 0)
return m_use_list[v]->size();
return 0;
}
ast * user_theory::get_parent(ast * n, unsigned i) const {
theory_var v = get_var(n);
if (v != null_theory_var && m_use_list[v] != 0)
return m_use_list[v]->get(i, 0);
return 0;
}
theory_var user_theory::mk_var(enode * n) {
if (is_attached_to_var(n))
return n->get_th_var(get_id());
theory_var r = theory::mk_var(n);
theory_var r2 = m_find.mk_var();
m_use_list.push_back(0);
SASSERT(r == r2);
get_context().attach_th_var(n, this, r);
if (m_new_elem_fptr != 0) {
flet<bool> invoking(m_new_elem_invoking, true);
m_new_elem_fptr(this, n->get_owner());
}
return r;
}
bool user_theory::internalize_atom(app * atom, bool gate_ctx) {
return internalize_term(atom);
}
bool user_theory::internalize_term(app * term) {
context & ctx = get_context();
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(term->get_arg(i), false);
// the internalization of the arguments may trigger the internalization of term.
if (ctx.e_internalized(term))
return true;
m_parents.push_back(term);
enode * e = ctx.mk_enode(term, false, get_manager().is_bool(term), true);
if (get_manager().is_bool(term)) {
bool_var bv = ctx.mk_bool_var(term);
ctx.set_var_theory(bv, get_id());
ctx.set_enode_flag(bv, true);
}
// make sure every argument is attached to a theory variable...
for (unsigned i = 0; i < num_args; i++) {
enode * arg = e->get_arg(i);
theory_var v_arg = mk_var(arg);
ptr_vector<app> * arg_use_list = get_non_null_use_list(v_arg);
arg_use_list->push_back(term);
m_trail_stack.push(push_back_trail<user_theory, app *, false>(*arg_use_list));
}
if (m_new_app_fptr != 0) {
flet<bool> invoking(m_new_app_invoking, true);
m_new_app_fptr(this, term);
}
return true;
}
void user_theory::apply_sort_cnstr(enode * n, sort * s) {
mk_var(n);
}
void user_theory::assign_eh(bool_var v, bool is_true) {
m_new_assignments.push_back(v);
}
void user_theory::new_eq_eh(theory_var v1, theory_var v2) {
m_new_eqs.push_back(var_pair(v1, v2));
}
void user_theory::new_diseq_eh(theory_var v1, theory_var v2) {
m_new_diseqs.push_back(var_pair(v1, v2));
}
void user_theory::relevant_eh(app * n) {
m_new_relevant_apps.push_back(n);
}
void user_theory::push_scope_eh() {
SASSERT(m_new_assignments.empty());
SASSERT(m_new_eqs.empty());
SASSERT(m_new_diseqs.empty());
SASSERT(m_new_relevant_apps.empty());
theory::push_scope_eh();
m_trail_stack.push_scope();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
s.m_asserted_axioms_old_sz = m_asserted_axioms.size();
s.m_parents_old_sz = m_parents.size();
if (m_push_fptr != 0) {
flet<bool> invoke(m_push_invoking, true);
m_push_fptr(this);
}
}
void user_theory::pop_scope_eh(unsigned num_scopes) {
reset_propagation_queues();
if (m_pop_fptr != 0) {
for (unsigned i = 0; i < num_scopes; i++) {
flet<bool> invoke(m_pop_invoking, true);
m_pop_fptr(this);
}
}
unsigned new_lvl = m_scopes.size() - num_scopes;
scope & s = m_scopes[new_lvl];
m_parents.shrink(s.m_parents_old_sz);
unsigned curr_sz = m_asserted_axioms.size();
unsigned old_sz = s.m_asserted_axioms_old_sz;
for (unsigned i = old_sz; i < curr_sz; i++) {
m_asserted_axiom_set.erase(m_asserted_axioms.get(i));
}
m_asserted_axioms.shrink(old_sz);
m_scopes.shrink(new_lvl);
m_trail_stack.pop_scope(num_scopes);
shrink_use_list(get_old_num_vars(num_scopes));
theory::pop_scope_eh(num_scopes);
}
void user_theory::restart_eh() {
if (m_restart_fptr != 0) {
flet<bool> invoke(m_restart_invoking, true);
m_restart_fptr(this);
}
}
void user_theory::init_search_eh() {
if (m_init_search_fptr != 0) {
flet<bool> invoke(m_init_search_invoking, true);
m_init_search_fptr(this);
}
}
final_check_status user_theory::final_check_eh() {
if (m_final_check_fptr != 0) {
unsigned old_sz = m_asserted_axioms.size();
flet<bool> invoke(m_final_check_invoking, true);
Z3_bool r = m_final_check_fptr(this);
if (old_sz != m_asserted_axioms.size()) {
assert_axioms_into_context(old_sz);
return r ? FC_CONTINUE : FC_GIVEUP;
}
return r ? FC_DONE : FC_GIVEUP;
}
return FC_DONE;
}
bool user_theory::can_propagate() {
return
(m_persisted_axioms.size() > m_persisted_axioms_qhead) ||
!m_new_eqs.empty() ||
!m_new_diseqs.empty() ||
!m_new_relevant_apps.empty() ||
!m_new_assignments.empty();
}
literal user_theory::internalize_literal(expr * arg) {
context & ctx = get_context();
ast_manager& m = get_manager();
if (is_app(arg) && m.is_not(arg)) {
expr * arg_arg = to_app(arg)->get_arg(0);
if (!ctx.b_internalized(arg_arg))
ctx.internalize(arg_arg, true);
return literal(ctx.get_bool_var(arg_arg), true);
}
else if (m.is_false(arg)) {
return false_literal;
}
else if (m.is_true(arg)) {
return true_literal;
}
else {
if (!ctx.b_internalized(arg))
ctx.internalize(arg, true);
return literal(ctx.get_bool_var(arg));
}
}
void user_theory::assert_axioms_into_context(unsigned old_sz) {
for (unsigned i = old_sz; i < m_asserted_axioms.size(); i++) {
expr * axiom = m_asserted_axioms.get(i);
assert_axiom_into_context(axiom);
}
}
void user_theory::mark_as_relevant(literal l) {
if (l == false_literal || l == true_literal) return;
get_context().mark_as_relevant(l);
}
void user_theory::assert_axiom_into_context(expr * axiom) {
TRACE("user_smt_theory", tout << mk_pp(axiom, get_manager()) << "\n";);
ast_manager & m = get_manager();
context & ctx = get_context();
if (m.is_or(axiom)) {
literal_buffer lits;
unsigned num_args = to_app(axiom)->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
lits.push_back(internalize_literal(to_app(axiom)->get_arg(i)));
mark_as_relevant(lits.back());
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
else {
literal l = internalize_literal(axiom);
mark_as_relevant(l);
ctx.mk_th_axiom(get_id(), 1, &l);
}
}
void user_theory::propagate() {
unsigned old_sz = m_asserted_axioms.size();
if (m_persisted_axioms_qhead < m_persisted_axioms.size()) {
get_context().push_trail(value_trail<context, unsigned>(m_persisted_axioms_qhead));
for (; m_persisted_axioms_qhead < m_persisted_axioms.size(); ++m_persisted_axioms_qhead) {
m_asserted_axioms.push_back(m_persisted_axioms[m_persisted_axioms_qhead].get());
}
}
do {
for (unsigned i = 0; i < m_new_eqs.size(); i++) {
var_pair & p = m_new_eqs[i];
if (m_new_eq_fptr != 0) {
++m_stats.m_num_eq;
flet<bool> invoke(m_new_eq_invoking, true);
m_new_eq_fptr(this, get_app(p.first), get_app(p.second));
}
m_find.merge(p.first, p.second);
}
m_new_eqs.reset();
if (m_new_diseq_fptr != 0) {
for (unsigned i = 0; i < m_new_diseqs.size(); i++) {
++m_stats.m_num_diseq;
var_pair & p = m_new_diseqs[i];
flet<bool> invoke(m_new_diseq_invoking, true);
m_new_diseq_fptr(this, get_app(p.first), get_app(p.second));
}
}
m_new_diseqs.reset();
if (m_new_assignment_fptr != 0) {
context & ctx = get_context();
for (unsigned i = 0; i < m_new_assignments.size(); i++) {
++m_stats.m_num_assignment;
bool_var bv = m_new_assignments[i];
lbool val = ctx.get_assignment(bv);
SASSERT(val != l_undef);
flet<bool> invoke(m_new_assignment_invoking, true);
m_new_assignment_fptr(this, to_app(ctx.bool_var2expr(bv)), val == l_true);
}
}
m_new_assignments.reset();
if (m_new_relevant_fptr != 0) {
for (unsigned i = 0; i < m_new_relevant_apps.size(); i++) {
flet<bool> invoke(m_new_relevant_invoking, true);
m_new_relevant_fptr(this, m_new_relevant_apps[i]);
}
}
m_new_relevant_apps.reset();
assert_axioms_into_context(old_sz);
old_sz = m_asserted_axioms.size();
}
while (!m_new_eqs.empty() || !m_new_diseqs.empty() || !m_new_relevant_apps.empty() || !m_new_assignments.empty());
}
void user_theory::flush_eh() {
reset(false);
}
void user_theory::reset_eh() {
reset(true);
}
void user_theory::reset(bool full_reset) {
if (m_reset_fptr != 0) {
flet<bool> invoke(m_reset_invoking, true);
m_reset_fptr(this);
}
m_trail_stack.reset();
reset_propagation_queues();
m_asserted_axioms.reset();
m_asserted_axiom_set.reset();
shrink_use_list(0);
m_parents.reset();
m_scopes.reset();
m_persisted_axioms.reset();
m_persisted_axioms_qhead = 0;
m_stats.reset();
if (full_reset)
theory::reset_eh();
}
void user_theory::display_statistics(std::ostream & out) const {
print_stat(out, "num. user eqs: ", m_stats.m_num_eq);
print_stat(out, "num. user diseq: ", m_stats.m_num_diseq);
print_stat(out, "num. assignments: ", m_stats.m_num_assignment);
print_stat(out, "num. user axioms: ", m_stats.m_num_user_axioms);
}
void user_theory::display_istatistics(std::ostream & out) const {
out << "NUM_USER_EQS " << m_stats.m_num_eq << "\n";
out << "NUM_USER_DISEQ " << m_stats.m_num_diseq << "\n";
out << "NUM_ASSIGNMENTS " << m_stats.m_num_assignment << "\n";
out << "NUM_USER_AXIOMS " << m_stats.m_num_user_axioms << "\n";
}
class user_smt_model_value_proc : public model_value_proc {
func_decl_ref m_decl;
public:
user_smt_model_value_proc(ast_manager& m, func_decl* f) : m_decl(f, m) {}
virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
ast_manager& m = mg.get_manager();
return m.mk_app(m_decl, values.size(), values.c_ptr());
}
};
bool user_theory::build_models() const {
return true;
}
void user_theory::init_model(model_generator & m) {
m.register_factory(alloc(user_smt_theory_factory, get_manager(), get_id()));
}
void user_theory::finalize_model(model_generator &) {
// No-op
}
model_value_proc * user_theory::mk_value(enode * n, model_generator & mg) {
ast_manager& m = get_manager();
func_decl* f = n->get_decl();
if (m_decl_plugin->is_value(f)) {
return alloc(user_smt_model_value_proc, m, n->get_decl());
}
else {
return mg.mk_model_value(n);
}
}
bool user_theory::get_value(enode * n, expr_ref & r) {
return false;
}
char const * user_theory::get_name() const {
return m_name.c_str();
}
void user_theory::display(std::ostream & out) const {
out << "Theory " << get_name() << ":\n";
}
user_theory * mk_user_theory(kernel & _s, void * ext_context, void * ext_data, char const * name) {
context & ctx = _s.get_context(); // HACK
symbol _name(name);
ast_manager & m = ctx.get_manager();
family_id fid = m.mk_family_id(_name);
user_decl_plugin * dp = alloc(user_decl_plugin);
m.register_plugin(fid, dp);
simplifier & s = ctx.get_simplifier();
user_simplifier_plugin * sp = alloc(user_simplifier_plugin, _name, m);
s.register_plugin(sp);
user_theory * th = alloc(user_theory, m, ctx.get_fparams(), ext_context, ext_data, name, fid, dp, sp);
ctx.register_plugin(th);
sp->set_owner(th);
return th;
}
};

324
src/smt/user_plugin/user_smt_theory.h
View file

@ -1,324 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
user_smt_theory.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2010-05-22.
Revision History:
--*/
#ifndef USER_SMT_THEORY_H_
#define USER_SMT_THEORY_H_
#include"user_decl_plugin.h"
#include"user_simplifier_plugin.h"
#include"smt_theory.h"
#include"union_find.h"
#include"smt_kernel.h"
namespace smt {
class user_theory;
typedef int Z3_bool;
typedef void (*theory_callback_fptr)(user_theory * th);
typedef Z3_bool (*theory_final_check_callback_fptr)(user_theory * th);
typedef void (*theory_app_callback_fptr)(user_theory * th, app *);
typedef void (*theory_app_bool_callback_fptr)(user_theory * th, app *, Z3_bool);
typedef void (*theory_app_app_callback_fptr)(user_theory * th, app *, app *);
typedef void * (*theory_mk_fresh_ext_data_fptr)(user_theory * th);
class user_theory : public theory {
typedef trail_stack<user_theory> th_trail_stack;
typedef union_find<user_theory> th_union_find;
typedef std::pair<theory_var, theory_var> var_pair;
smt_params const& m_params;
void * m_ext_context;
void * m_ext_data;
std::string m_name;
bool m_simplify_axioms;
user_decl_plugin * m_decl_plugin;
user_simplifier_plugin * m_simplifier_plugin;
th_union_find m_find;
th_trail_stack m_trail_stack;
svector<var_pair> m_new_eqs;
svector<var_pair> m_new_diseqs;
svector<bool_var> m_new_assignments;
ptr_vector<app> m_new_relevant_apps;
obj_hashtable<expr> m_asserted_axiom_set;
expr_ref_vector m_asserted_axioms;
ptr_vector<app> m_parents;
ptr_vector<ptr_vector<app> > m_use_list;
app_ref_vector m_persisted_axioms;
unsigned m_persisted_axioms_qhead;
struct scope {
unsigned m_asserted_axioms_old_sz;
unsigned m_parents_old_sz;
};
svector<scope> m_scopes;
theory_callback_fptr m_delete_fptr;
theory_app_callback_fptr m_new_app_fptr;
theory_app_callback_fptr m_new_elem_fptr;
theory_callback_fptr m_init_search_fptr;
theory_callback_fptr m_push_fptr;
theory_callback_fptr m_pop_fptr;
theory_callback_fptr m_restart_fptr;
theory_callback_fptr m_reset_fptr;
theory_final_check_callback_fptr m_final_check_fptr;
theory_app_app_callback_fptr m_new_eq_fptr;
theory_app_app_callback_fptr m_new_diseq_fptr;
theory_app_bool_callback_fptr m_new_assignment_fptr;
theory_app_callback_fptr m_new_relevant_fptr;
theory_mk_fresh_ext_data_fptr m_mk_fresh_fptr;
bool m_delete_invoking;
bool m_new_app_invoking;
bool m_new_elem_invoking;
bool m_init_search_invoking;
bool m_push_invoking;
bool m_pop_invoking;
bool m_restart_invoking;
bool m_reset_invoking;
bool m_final_check_invoking;
bool m_new_eq_invoking;
bool m_new_diseq_invoking;
bool m_new_assignment_invoking;
bool m_new_relevant_invoking;
struct statistics {
unsigned m_num_eq;
unsigned m_num_diseq;
unsigned m_num_assignment;
unsigned m_num_user_axioms;
statistics() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
statistics m_stats;
protected:
virtual theory_var mk_var(enode * n);
literal internalize_literal(expr * arg);
void assert_axioms_into_context(unsigned old_sz);
void assert_axiom_into_context(expr * axiom);
void reset_propagation_queues();
void shrink_use_list(unsigned sz);
ptr_vector<app> * get_non_null_use_list(theory_var v);
void mark_as_relevant(literal l);
void assert_axiom_core(app* axiom);
public:
user_theory(ast_manager & m, smt_params const& p, void * ext_context, void * ext_data, char const * name, family_id fid, user_decl_plugin * dp, user_simplifier_plugin * sp);
virtual ~user_theory();
virtual theory * mk_fresh(context * new_ctx);
void * get_ext_context() const {
return m_ext_context;
}
void * get_ext_data() {
return m_ext_data;
}
sort * mk_sort(symbol const & name) {
return m_decl_plugin->mk_sort(name);
}
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) {
return m_decl_plugin->mk_func_decl(name, arity, domain, range);
}
func_decl * mk_value_decl(symbol const & name, sort * s) {
return m_decl_plugin->mk_value_decl(name, s);
}
void assert_axiom(ast * axiom);
void assume_eq(ast * lhs, ast * rhs);
void enable_axiom_simplification(bool flag) {
m_simplify_axioms = flag;
}
void set_delete_fptr(theory_callback_fptr ptr) {
m_delete_fptr = ptr;
}
void set_reduce_app_fptr(reduce_app_fptr ptr) {
m_simplifier_plugin->set_reduce_app_fptr(ptr);
}
void set_reduce_eq_fptr(reduce_eq_fptr ptr) {
m_simplifier_plugin->set_reduce_eq_fptr(ptr);
}
void set_reduce_distinct_fptr(reduce_distinct_fptr ptr) {
m_simplifier_plugin->set_reduce_distinct_fptr(ptr);
}
void set_new_app_fptr(theory_app_callback_fptr ptr) {
m_new_app_fptr = ptr;
}
void set_new_elem_fptr(theory_app_callback_fptr ptr) {
m_new_elem_fptr = ptr;
}
void set_init_search_fptr(theory_callback_fptr ptr) {
m_init_search_fptr = ptr;
}
void set_push_fptr(theory_callback_fptr ptr) {
m_push_fptr = ptr;
}
void set_pop_fptr(theory_callback_fptr ptr) {
m_pop_fptr = ptr;
}
void set_restart_fptr(theory_callback_fptr ptr) {
m_restart_fptr = ptr;
}
void set_reset_fptr(theory_callback_fptr ptr) {
m_reset_fptr = ptr;
}
void set_final_check_fptr(theory_final_check_callback_fptr ptr) {
m_final_check_fptr = ptr;
}
void set_new_eq_fptr(theory_app_app_callback_fptr ptr) {
m_new_eq_fptr = ptr;
}
void set_new_diseq_fptr(theory_app_app_callback_fptr ptr) {
m_new_diseq_fptr = ptr;
}
void set_new_assignment_fptr(theory_app_bool_callback_fptr ptr) {
m_new_assignment_fptr = ptr;
}
void set_new_relevant_fptr(theory_app_callback_fptr ptr) {
m_new_relevant_fptr = ptr;
}
th_trail_stack & get_trail_stack() { return m_trail_stack; }
theory_var get_var(ast * n) const;
theory_var mk_var(ast * n);
ast * get_root(ast * n) const;
ast * get_next(ast * n) const;
unsigned get_num_parents(ast * n) const;
ast * get_parent(ast * n, unsigned i) const;
unsigned get_num_parents() const { return m_parents.size(); }
ast * get_parent(unsigned i) const { return m_parents[i]; }
unsigned get_num_apps() const { return get_num_vars(); }
app * get_app(unsigned i) const { return get_enode(i)->get_owner(); }
unsigned get_num_asts() const { return get_num_apps(); }
ast * get_ast(unsigned i) const { return get_app(i); }
static void merge_eh(theory_var, theory_var, theory_var, theory_var) {}
static void after_merge_eh(theory_var, theory_var, theory_var, theory_var) {}
virtual void unmerge_eh(theory_var, theory_var) {}
virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term);
virtual void apply_sort_cnstr(enode * n, sort * s);
virtual void assign_eh(bool_var v, bool is_true);
virtual void new_eq_eh(theory_var v1, theory_var v2);
virtual void new_diseq_eh(theory_var v1, theory_var v2);
virtual void relevant_eh(app * n);
virtual void push_scope_eh();
virtual void pop_scope_eh(unsigned num_scopes);
virtual void restart_eh();
virtual void init_search_eh();
virtual final_check_status final_check_eh();
virtual bool can_propagate();
virtual void propagate();
virtual void flush_eh();
virtual void reset_eh();
void reset(bool full_reset);
virtual void display_statistics(std::ostream & out) const;
virtual void display_istatistics(std::ostream & out) const;
virtual bool build_models() const;
virtual void init_model(model_generator & m);
virtual void finalize_model(model_generator & m);
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual bool get_value(enode * n, expr_ref & r);
virtual char const * get_name() const;
virtual void display(std::ostream & out) const;
};
user_theory * mk_user_theory(kernel & s, void * ext_context, void * ext_data, char const * name);
};
#endif /* USER_SMT_THEORY_H_ */