mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-11-05 14:35:48 +00:00
parent 69853ba6fc
commit 50c323dc74
1 changed files with 17 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/smt/smt_quantifier.h
View file

@ -37,7 +37,7 @@ namespace smt {
public: public:
quantifier_manager(context & ctx, smt_params & fp, params_ref const & p); quantifier_manager(context & ctx, smt_params & fp, params_ref const & p);
~quantifier_manager(); ~quantifier_manager();
context & get_context() const; context & get_context() const;
void set_plugin(quantifier_manager_plugin * plugin); void set_plugin(quantifier_manager_plugin * plugin);
@ -51,12 +51,12 @@ namespace smt {
quantifier_stat * get_stat(quantifier * q) const; quantifier_stat * get_stat(quantifier * q) const;
unsigned get_generation(quantifier * q) const; unsigned get_generation(quantifier * q) const;
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);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0); bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
@ -78,11 +78,11 @@ namespace smt {
bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
void adjust_model(proto_model * m); void adjust_model(proto_model * m);
check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value); check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
void push(); void push();
void pop(unsigned num_scopes); void pop(unsigned num_scopes);
void reset(); void reset();
void display(std::ostream & out) const; void display(std::ostream & out) const;
void display_stats(std::ostream & out, quantifier * q) const; void display_stats(std::ostream & out, quantifier * q) const;
@ -97,7 +97,7 @@ namespace smt {
public: public:
quantifier_manager_plugin() {} quantifier_manager_plugin() {}
virtual ~quantifier_manager_plugin() {} virtual ~quantifier_manager_plugin() {}
virtual void set_manager(quantifier_manager & qm) = 0; virtual void set_manager(quantifier_manager & qm) = 0;
virtual quantifier_manager_plugin * mk_fresh() = 0; virtual quantifier_manager_plugin * mk_fresh() = 0;
@ -106,7 +106,7 @@ namespace smt {
virtual void del(quantifier * q) = 0; virtual void del(quantifier * q) = 0;
virtual bool is_shared(enode * n) const = 0; virtual bool is_shared(enode * n) const = 0;
/** /**
\brief This method is invoked whenever q is assigned to true. \brief This method is invoked whenever q is assigned to true.
*/ */
@ -131,9 +131,9 @@ namespace smt {
\brief This method is invoked whenever the solver restarts. \brief This method is invoked whenever the solver restarts.
*/ */
virtual void restart_eh() = 0; virtual void restart_eh() = 0;
/** /**
\brief Return true if the quantifier_manager can propagate information \brief Return true if the quantifier_manager can propagate information
information back into the core. information back into the core.
*/ */
virtual bool can_propagate() const = 0; virtual bool can_propagate() const = 0;
@ -143,11 +143,11 @@ namespace smt {
\brief Return true if the plugin is "model based" \brief Return true if the plugin is "model based"
*/ */
virtual bool model_based() const = 0; virtual bool model_based() const = 0;
/** /**
\brief Is "model based" instantiate allowed to instantiate this quantifier? \brief Is "model based" instantiate allowed to instantiate this quantifier?
*/ */
virtual bool mbqi_enabled(quantifier *q) const {return true;} virtual bool mbqi_enabled(quantifier *q) const {return true;}
/** /**
\brief Give a change to the plugin to adjust the interpretation of unintepreted functions. \brief Give a change to the plugin to adjust the interpretation of unintepreted functions.
@ -161,10 +161,10 @@ namespace smt {
It also provides a mapping from enodes to their interpretations. It also provides a mapping from enodes to their interpretations.
*/ */
virtual quantifier_manager::check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value) = 0; virtual quantifier_manager::check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value) = 0;
virtual void push() = 0; virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0; virtual void pop(unsigned num_scopes) = 0;
}; };
}; };