mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-08-05 11:13:05 +02:00
commit b8e6a0d0dc
3 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/ast.cpp
View file

@ -1018,7 +1018,7 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) {
sort* basic_decl_plugin::join(sort* s1, sort* s2) { sort* basic_decl_plugin::join(sort* s1, sort* s2) {
if (s1 == s2) return s1; if (s1 == s2) return s1;
if (s1->get_family_id() == m_manager->m_arith_family_id && if (s1->get_family_id() == m_manager->m_arith_family_id &&
s2->get_family_id() == m_manager->m_arith_family_id) { s2->get_family_id() == m_manager->m_arith_family_id) {
if (s1->get_decl_kind() == REAL_SORT) { if (s1->get_decl_kind() == REAL_SORT) {
return s1; return s1;
@ -1030,6 +1030,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
throw ast_exception(buffer.str().c_str()); throw ast_exception(buffer.str().c_str());
} }
func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) { unsigned arity, sort * const * domain, sort * range) {
switch (static_cast<basic_op_kind>(k)) { switch (static_cast<basic_op_kind>(k)) {

4
src/sat/sat_solver.h
View file

@ -210,6 +210,7 @@ namespace sat {
public: public:
bool inconsistent() const { return m_inconsistent; } bool inconsistent() const { return m_inconsistent; }
unsigned num_vars() const { return m_level.size(); } unsigned num_vars() const { return m_level.size(); }
unsigned num_clauses() const;
bool is_external(bool_var v) const { return m_external[v] != 0; } bool is_external(bool_var v) const { return m_external[v] != 0; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; } unsigned scope_lvl() const { return m_scope_lvl; }
@ -446,8 +447,7 @@ namespace sat {
protected: protected:
void display_binary(std::ostream & out) const; void display_binary(std::ostream & out) const;
void display_units(std::ostream & out) const; void display_units(std::ostream & out) const;
unsigned num_clauses() const;
bool is_unit(clause const & c) const; bool is_unit(clause const & c) const;
bool is_empty(clause const & c) const; bool is_empty(clause const & c) const;
bool check_missed_propagation(clause_vector const & cs) const; bool check_missed_propagation(clause_vector const & cs) const;

3
src/solver/solver.h
View file

@ -139,6 +139,7 @@ public:
\brief Display the content of this solver. \brief Display the content of this solver.
*/ */
virtual void display(std::ostream & out) const; virtual void display(std::ostream & out) const;
class scoped_push { class scoped_push {
solver& s; solver& s;
bool m_nopop; bool m_nopop;
@ -147,9 +148,9 @@ public:
~scoped_push() { if (!m_nopop) s.pop(1); } ~scoped_push() { if (!m_nopop) s.pop(1); }
void disable_pop() { m_nopop = true; } void disable_pop() { m_nopop = true; }
}; };
protected: protected:
virtual void set_cancel(bool f) = 0; virtual void set_cancel(bool f) = 0;
}; };
#endif #endif