mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-05 14:39:23 +00:00
parent 50c323dc74
commit 5ef7d38d72
1 changed files with 47 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

97
src/smt/smt_quantifier.cpp
View file

@ -27,7 +27,7 @@ Revision History:
#include"ast_smt2_pp.h" #include"ast_smt2_pp.h"
namespace smt { namespace smt {
quantifier_manager_plugin * mk_default_plugin(); quantifier_manager_plugin * mk_default_plugin();
struct quantifier_manager::imp { struct quantifier_manager::imp {
@ -40,7 +40,7 @@ namespace smt {
ptr_vector<quantifier> m_quantifiers; ptr_vector<quantifier> m_quantifiers;
scoped_ptr<quantifier_manager_plugin> m_plugin; scoped_ptr<quantifier_manager_plugin> m_plugin;
unsigned m_num_instances; unsigned m_num_instances;
imp(quantifier_manager & wrapper, context & ctx, smt_params & p, quantifier_manager_plugin * plugin): imp(quantifier_manager & wrapper, context & ctx, smt_params & p, quantifier_manager_plugin * plugin):
m_wrapper(wrapper), m_wrapper(wrapper),
m_context(ctx), m_context(ctx),
@ -85,7 +85,7 @@ namespace smt {
out << max_generation << " : " << max_cost << "\n"; out << max_generation << " : " << max_cost << "\n";
} }
} }
void del(quantifier * q) { void del(quantifier * q) {
if (m_params.m_qi_profile) { if (m_params.m_qi_profile) {
display_stats(verbose_stream(), q); display_stats(verbose_stream(), q);
@ -99,15 +99,15 @@ namespace smt {
} }
bool is_shared(enode * n) const { bool is_shared(enode * n) const {
return m_plugin->is_shared(n); return m_plugin->is_shared(n);
} }
bool add_instance(quantifier * q, app * pat, bool add_instance(quantifier * q, app * pat,
unsigned num_bindings, unsigned num_bindings,
enode * const * bindings, enode * const * bindings,
unsigned max_generation, unsigned max_generation,
unsigned min_top_generation, unsigned min_top_generation,
unsigned max_top_generation, unsigned max_top_generation,
ptr_vector<enode> & used_enodes) { ptr_vector<enode> & used_enodes) {
max_generation = std::max(max_generation, get_generation(q)); max_generation = std::max(max_generation, get_generation(q));
if (m_num_instances > m_params.m_qi_max_instances) if (m_num_instances > m_params.m_qi_max_instances)
@ -136,7 +136,7 @@ namespace smt {
} }
return false; return false;
} }
void init_search_eh() { void init_search_eh() {
m_num_instances = 0; m_num_instances = 0;
ptr_vector<quantifier>::iterator it2 = m_quantifiers.begin(); ptr_vector<quantifier>::iterator it2 = m_quantifiers.begin();
@ -149,7 +149,7 @@ namespace smt {
m_plugin->init_search_eh(); m_plugin->init_search_eh();
TRACE("smt_params", m_params.display(tout); ); TRACE("smt_params", m_params.display(tout); );
} }
void assign_eh(quantifier * q) { void assign_eh(quantifier * q) {
m_plugin->assign_eh(q); m_plugin->assign_eh(q);
} }
@ -175,7 +175,7 @@ namespace smt {
m_plugin->pop(num_scopes); m_plugin->pop(num_scopes);
m_qi_queue.pop_scope(num_scopes); m_qi_queue.pop_scope(num_scopes);
} }
bool can_propagate() { bool can_propagate() {
return m_qi_queue.has_work() || m_plugin->can_propagate(); return m_qi_queue.has_work() || m_plugin->can_propagate();
} }
@ -184,7 +184,7 @@ namespace smt {
m_plugin->propagate(); m_plugin->propagate();
m_qi_queue.instantiate(); m_qi_queue.instantiate();
} }
bool check_quantifier(quantifier* q) { bool check_quantifier(quantifier* q) {
return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && !m_context->get_manager().is_rec_fun_def(q); return m_context.is_relevant(q) && m_context.get_assignment(q) == l_true; // TBD: && !m_context->get_manager().is_rec_fun_def(q);
} }
@ -251,7 +251,7 @@ namespace smt {
quantifier_manager::~quantifier_manager() { quantifier_manager::~quantifier_manager() {
dealloc(m_imp); dealloc(m_imp);
} }
context & quantifier_manager::get_context() const { context & quantifier_manager::get_context() const {
return m_imp->m_context; return m_imp->m_context;
} }
@ -285,16 +285,16 @@ namespace smt {
return m_imp->get_generation(q); return m_imp->get_generation(q);
} }
bool quantifier_manager::add_instance(quantifier * q, app * pat, bool quantifier_manager::add_instance(quantifier * q, app * pat,
unsigned num_bindings, unsigned num_bindings,
enode * const * bindings, enode * const * bindings,
unsigned max_generation, unsigned max_generation,
unsigned min_top_generation, unsigned min_top_generation,
unsigned max_top_generation, unsigned max_top_generation,
ptr_vector<enode> & used_enodes) { ptr_vector<enode> & used_enodes) {
return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_generation, used_enodes); return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_generation, used_enodes);
} }
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) { bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) {
ptr_vector<enode> tmp; ptr_vector<enode> tmp;
return add_instance(q, 0, num_bindings, bindings, generation, generation, generation, tmp); return add_instance(q, 0, num_bindings, bindings, generation, generation, generation, tmp);
@ -347,7 +347,7 @@ namespace smt {
quantifier_manager::check_model_result quantifier_manager::check_model(proto_model * m, obj_map<enode, app *> const & root2value) { quantifier_manager::check_model_result quantifier_manager::check_model(proto_model * m, obj_map<enode, app *> const & root2value) {
return m_imp->check_model(m, root2value); return m_imp->check_model(m, root2value);
} }
void quantifier_manager::push() { void quantifier_manager::push() {
m_imp->push(); m_imp->push();
} }
@ -367,7 +367,7 @@ namespace smt {
plugin->set_manager(*this); plugin->set_manager(*this);
} }
} }
void quantifier_manager::display(std::ostream & out) const { void quantifier_manager::display(std::ostream & out) const {
} }
@ -382,12 +382,12 @@ namespace smt {
m_imp->display_stats(out, q); m_imp->display_stats(out, q);
} }
ptr_vector<quantifier>::const_iterator quantifier_manager::begin_quantifiers() const { ptr_vector<quantifier>::const_iterator quantifier_manager::begin_quantifiers() const {
return m_imp->m_quantifiers.begin(); return m_imp->m_quantifiers.begin();
} }
ptr_vector<quantifier>::const_iterator quantifier_manager::end_quantifiers() const { ptr_vector<quantifier>::const_iterator quantifier_manager::end_quantifiers() const {
return m_imp->m_quantifiers.end(); return m_imp->m_quantifiers.end();
} }
// The default plugin uses E-matching, MBQI and quick-checker // The default plugin uses E-matching, MBQI and quick-checker
@ -404,13 +404,13 @@ namespace smt {
bool m_active; bool m_active;
public: public:
default_qm_plugin(): default_qm_plugin():
m_qm(0), m_qm(0),
m_context(0), m_context(0),
m_new_enode_qhead(0), m_new_enode_qhead(0),
m_lazy_matching_idx(0), m_lazy_matching_idx(0),
m_active(false) { m_active(false) {
} }
virtual ~default_qm_plugin() { virtual ~default_qm_plugin() {
} }
@ -434,20 +434,18 @@ namespace smt {
virtual bool model_based() const { return m_fparams->m_mbqi; } virtual bool model_based() const { return m_fparams->m_mbqi; }
virtual bool mbqi_enabled(quantifier *q) const { virtual bool mbqi_enabled(quantifier *q) const {
if(!m_fparams->m_mbqi_id) return true; if (!m_fparams->m_mbqi_id) return true;
const symbol &s = q->get_qid(); const symbol &s = q->get_qid();
size_t len = strlen(m_fparams->m_mbqi_id); size_t len = strlen(m_fparams->m_mbqi_id);
if(s == symbol::null || s.is_numerical()) if (s == symbol::null || s.is_numerical())
return len == 0; return len == 0;
return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0; return strncmp(s.bare_str(), m_fparams->m_mbqi_id, len) == 0;
} }
/* Quantifier id's must begin with the prefix specified by /* Quantifier id's must begin with the prefix specified by parameter
parameter mbqi.id to be instantiated with MBQI. The default mbqi.id to be instantiated with MBQI. The default value is the
value is the empty string, so all quantifiers are empty string, so all quantifiers are instantiated. */
instantiated.
*/
virtual void add(quantifier * q) { virtual void add(quantifier * q) {
if (m_fparams->m_mbqi && mbqi_enabled(q)) { if (m_fparams->m_mbqi && mbqi_enabled(q)) {
m_active = true; m_active = true;
@ -455,8 +453,7 @@ namespace smt {
} }
} }
virtual void del(quantifier * q) { virtual void del(quantifier * q) { }
}
virtual void push() { virtual void push() {
m_mam->push_scope(); m_mam->push_scope();
@ -465,7 +462,7 @@ namespace smt {
m_model_finder->push_scope(); m_model_finder->push_scope();
} }
} }
virtual void pop(unsigned num_scopes) { virtual void pop(unsigned num_scopes) {
m_mam->pop_scope(num_scopes); m_mam->pop_scope(num_scopes);
m_lazy_mam->pop_scope(num_scopes); m_lazy_mam->pop_scope(num_scopes);
@ -473,7 +470,7 @@ namespace smt {
m_model_finder->pop_scope(num_scopes); m_model_finder->pop_scope(num_scopes);
} }
} }
virtual void init_search_eh() { virtual void init_search_eh() {
m_lazy_matching_idx = 0; m_lazy_matching_idx = 0;
if (m_fparams->m_mbqi) { if (m_fparams->m_mbqi) {
@ -516,7 +513,7 @@ namespace smt {
} }
} }
} }
bool use_ematching() const { bool use_ematching() const {
return m_fparams->m_ematching && !m_qm->empty(); return m_fparams->m_ematching && !m_qm->empty();
} }
@ -538,7 +535,7 @@ namespace smt {
} }
virtual void restart_eh() { virtual void restart_eh() {
if (m_fparams->m_mbqi) { if (m_fparams->m_mbqi) {
m_model_finder->restart_eh(); m_model_finder->restart_eh();
m_model_checker->restart_eh(); m_model_checker->restart_eh();
} }
@ -613,7 +610,7 @@ namespace smt {
} }
return FC_DONE; return FC_DONE;
} }
}; };
quantifier_manager_plugin * mk_default_plugin() { quantifier_manager_plugin * mk_default_plugin() {