mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-08-16 14:33:43 -07:00
commit bb32a83c4f
8 changed files with 71 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast.cpp
View file

@ -35,7 +35,7 @@ Revision History:
parameter::~parameter() {
if (m_kind == PARAM_RATIONAL) {
m_rational.~rational();
reinterpret_cast<rational *>(m_rational)->~rational();
}
}
@ -50,14 +50,14 @@ parameter& parameter::operator=(parameter const& other) {
return *this;
}
if (m_kind == PARAM_RATIONAL) {
m_rational.~rational();
reinterpret_cast<rational *>(m_rational)->~rational();
}
m_kind = other.m_kind;
switch(other.m_kind) {
case PARAM_INT: m_int = other.get_int(); break;
case PARAM_AST: m_ast = other.get_ast(); break;
case PARAM_SYMBOL: m_symbol = other.get_symbol(); break;
case PARAM_RATIONAL: new (&m_rational) rational(other.get_rational()); break;
case PARAM_SYMBOL: new (m_symbol) symbol(other.get_symbol()); break;
case PARAM_RATIONAL: new (m_rational) rational(other.get_rational()); break;
case PARAM_DOUBLE: m_dval = other.m_dval; break;
case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
default:

24
src/ast/ast.h
View file

@ -100,12 +100,12 @@ private:
// It is not possible to use tag pointers, since symbols are already tagged.
union {
int m_int; // for PARAM_INT
ast* m_ast; // for PARAM_AST
symbol m_symbol; // for PARAM_SYMBOL
rational m_rational; // for PARAM_RATIONAL
double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
unsigned m_ext_id; // for PARAM_EXTERNAL
int m_int; // for PARAM_INT
ast* m_ast; // for PARAM_AST
char m_symbol[sizeof(symbol)]; // for PARAM_SYMBOL
char m_rational[sizeof(rational)]; // for PARAM_RATIONAL
double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
unsigned m_ext_id; // for PARAM_EXTERNAL
};
public:
@ -114,10 +114,12 @@ public:
explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {}
explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {}
explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {}
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s) {}
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(r) {}
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); }
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); }
explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(s) {}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL) {
new (m_symbol) symbol(s);
}
explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
parameter(parameter const&);
@ -154,8 +156,8 @@ public:
int get_int() const { SASSERT(is_int()); return m_int; }
ast * get_ast() const { SASSERT(is_ast()); return m_ast; }
symbol const & get_symbol() const { SASSERT(is_symbol()); return m_symbol; }
rational const & get_rational() const { SASSERT(is_rational()); return m_rational; }
symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast<const symbol *>(m_symbol)); }
rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast<const rational *>(m_rational)); }
double get_double() const { SASSERT(is_double()); return m_dval; }
unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; }

19
src/smt/asserted_formulas.cpp
View file

@ -16,31 +16,31 @@ Author:
Revision History:
--*/
#include "smt/asserted_formulas.h"
#include "util/warning.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/for_each_expr.h"
#include "ast/well_sorted.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/simplifier/array_simplifier_plugin.h"
#include "ast/simplifier/datatype_simplifier_plugin.h"
#include "ast/simplifier/fpa_simplifier_plugin.h"
#include "ast/simplifier/seq_simplifier_plugin.h"
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/for_each_expr.h"
#include "ast/well_sorted.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/simplifier/pull_ite_tree.h"
#include "ast/simplifier/push_app_ite.h"
#include "smt/elim_term_ite.h"
#include "ast/pattern/pattern_inference.h"
#include "ast/normal_forms/nnf.h"
#include "ast/simplifier/bv_elim.h"
#include "ast/simplifier/inj_axiom.h"
#include "ast/rewriter/der.h"
#include "ast/simplifier/elim_bounds.h"
#include "util/warning.h"
#include "ast/simplifier/bit2int.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/normal_forms/nnf.h"
#include "ast/pattern/pattern_inference.h"
#include "ast/rewriter/der.h"
#include "ast/rewriter/distribute_forall.h"
#include "ast/macros/quasi_macros.h"
#include "smt/asserted_formulas.h"
#include "smt/elim_term_ite.h"
asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m(m),
@ -138,6 +138,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
m_bsimp->set_eliminate_and(flag);
}
void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
if (inconsistent())
return;

19
src/smt/smt_setup.cpp
View file

@ -53,7 +53,8 @@ namespace smt {
// warning_msg("ignoring MODEL_COMPACT=true because it cannot be used with MBQI=true");
// m_params.m_model_compact = false;
// }
TRACE("setup", tout << "configuring logical context, logic: " << m_logic << "\n";);
TRACE("setup", tout << "configuring logical context, logic: " << m_logic << " " << cm << "\n";);
m_already_configured = true;
switch (cm) {
@ -202,6 +203,9 @@ namespace smt {
void setup::setup_QF_UF() {
m_params.m_relevancy_lvl = 0;
m_params.m_nnf_cnf = false;
m_params.m_restart_strategy = RS_LUBY;
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
m_params.m_random_initial_activity = IA_RANDOM;
}
void setup::setup_QF_BVRE() {
@ -210,13 +214,9 @@ namespace smt {
m_context.register_plugin(alloc(theory_seq, m_manager));
}
void setup::setup_QF_UF(static_features const & st) {
void setup::setup_QF_UF(static_features const & st) {
check_no_arithmetic(st, "QF_UF");
m_params.m_relevancy_lvl = 0;
m_params.m_nnf_cnf = false;
m_params.m_restart_strategy = RS_LUBY;
m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2;
m_params.m_random_initial_activity = IA_RANDOM;
setup_QF_UF();
TRACE("setup",
tout << "st.m_num_theories: " << st.m_num_theories << "\n";
tout << "st.m_num_uninterpreted_functions: " << st.m_num_uninterpreted_functions << "\n";);
@ -548,6 +548,7 @@ namespace smt {
}
void setup::setup_QF_BV() {
TRACE("setup", tout << "qf-bv\n";);
m_params.m_relevancy_lvl = 0;
m_params.m_arith_reflect = false;
m_params.m_bv_cc = false;
@ -877,7 +878,7 @@ namespace smt {
void setup::setup_unknown() {
static_features st(m_manager);
st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
TRACE("setup", tout << "setup_unknown\n";);
setup_arith();
setup_arrays();
setup_bv();
@ -916,7 +917,7 @@ namespace smt {
tout << "has fpa: " << st.m_has_fpa << "\n";
tout << "has arrays: " << st.m_has_arrays << "\n";);
if (st.num_non_uf_theories() == 0) {
if (st.num_non_uf_theories() == 0) {
setup_QF_UF(st);
return;
}

4
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -93,7 +93,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
return mk_qffpbv_tactic(m, p);
else if (logic=="HORN")
return mk_horn_tactic(m, p);
else if (logic == "QF_FD")
else if (logic == "QF_FD" || logic == "SAT")
return mk_solver2tactic(mk_fd_solver(m, p));
//else if (logic=="QF_UFNRA")
// return mk_qfufnra_tactic(m, p);
@ -102,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
}
static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
if (logic == "QF_FD")
if (logic == "QF_FD" || logic == "SAT")
return mk_fd_solver(m, p);
return 0;
}

51
src/util/optional.h
View file

@ -23,35 +23,32 @@ Revision History:
template<typename T>
class optional {
union {
T m_obj;
char m_dummy;
};
bool m_initialized;
char m_obj[sizeof(T)];
char m_initialized;
void construct(const T & val) {
m_initialized = true;
new (&m_obj) T(val);
m_initialized = 1;
new (reinterpret_cast<void *>(m_obj)) T(val);
}
void destroy() {
if (m_initialized) {
m_obj.~T();
if (m_initialized == 1) {
reinterpret_cast<T *>(m_obj)->~T();
}
m_initialized = false;
m_initialized = 0;
}
public:
optional():
m_initialized(false) {}
m_initialized(0) {}
explicit optional(const T & val) {
construct(val);
}
optional(const optional<T> & val):
m_initialized(false) {
if (val.m_initialized) {
m_initialized(0) {
if (val.m_initialized == 1) {
construct(*val);
}
}
@ -62,13 +59,13 @@ public:
static optional const & undef() { static optional u; return u; }
bool initialized() const { return m_initialized; }
operator bool() const { return m_initialized; }
bool operator!() const { return !m_initialized; }
bool initialized() const { return m_initialized == 1; }
operator bool() const { return m_initialized == 1; }
bool operator!() const { return m_initialized == 0; }
T * get() const {
if (m_initialized) {
return &m_obj;
if (m_initialized == 1) {
return reinterpret_cast<T *>(m_obj);
}
else {
return 0;
@ -76,29 +73,29 @@ public:
}
void set_invalid() {
if (m_initialized) {
if (m_initialized == 1) {
destroy();
}
}
T * operator->() {
SASSERT(m_initialized);
return &m_obj;
SASSERT(m_initialized==1);
return reinterpret_cast<T *>(m_obj);
}
T const * operator->() const {
SASSERT(m_initialized);
return &m_obj;
SASSERT(m_initialized==1);
return reinterpret_cast<T const *>(m_obj);
}
const T & operator*() const {
SASSERT(m_initialized);
return m_obj;
SASSERT(m_initialized==1);
return *reinterpret_cast<T const*>(m_obj);
}
T & operator*() {
SASSERT(m_initialized);
return m_obj;
SASSERT(m_initialized==1);
return *reinterpret_cast<T *>(m_obj);
}
optional & operator=(const T & val) {