mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-12-14 16:55:04 -08:00
commit 1dfea1324e
22 changed files with 267 additions and 1672 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/ast_smt2_pp.cpp
View file

@ -501,7 +501,12 @@ class smt2_printer {
}
format * pp_simple_attribute(char const * attr, symbol const & s) {
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), s.str().c_str()));
std::string str;
if (is_smt2_quoted_symbol(s))
str = mk_smt2_quoted_symbol(s);
else
str = s.str();
return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str()));
}
format * pp_labels(bool is_pos, buffer<symbol> const & names, format * f) {
@ -851,7 +856,7 @@ class smt2_printer {
buf.push_back(pp_simple_attribute(":weight ", q->get_weight()));
}
if (q->get_skid() != symbol::null) {
buf.push_back(pp_simple_attribute(":skid ", q->get_skid()));
buf.push_back(pp_simple_attribute(":skolemid ", q->get_skid()));
}
if (q->get_qid() != symbol::null) {
#if 0

101
src/ast/normal_forms/defined_names.cpp
View file

@ -17,11 +17,67 @@ Revision History:
--*/
#include"defined_names.h"
#include"obj_hashtable.h"
#include"used_vars.h"
#include"var_subst.h"
#include"ast_smt2_pp.h"
#include"ast_pp.h"
struct defined_names::impl {
typedef obj_map<expr, app *> expr2name;
typedef obj_map<expr, proof *> expr2proof;
ast_manager & m_manager;
symbol m_z3name;
/**
\brief Mapping from expressions to their names. A name is an application.
If the expression does not have free variables, then the name is just a constant.
*/
expr2name m_expr2name;
/**
\brief Mapping from expressions to the apply-def proof.
That is, for each expression e, m_expr2proof[e] is the
proof e and m_expr2name[2] are observ. equivalent.
This mapping is not used if proof production is disabled.
*/
expr2proof m_expr2proof;
/**
\brief Domain of m_expr2name. It is used to keep the expressions
alive and for backtracking
*/
expr_ref_vector m_exprs;
expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
unsigned_vector m_lims; //!< Backtracking support.
impl(ast_manager & m, char const * prefix);
virtual ~impl();
app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
void cache_new_name(expr * e, app * name);
void cache_new_name_intro_proof(expr * e, proof * pr);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result);
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
void push_scope();
void pop_scope(unsigned num_scopes);
void reset();
unsigned get_num_names() const { return m_names.size(); }
func_decl * get_name_decl(unsigned i) const { return to_app(m_names.get(i))->get_decl(); }
};
struct defined_names::pos_impl : public defined_names::impl {
pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
};
defined_names::impl::impl(ast_manager & m, char const * prefix):
m_manager(m),
m_exprs(m),
@ -222,5 +278,50 @@ void defined_names::impl::reset() {
m_lims.reset();
}
defined_names::defined_names(ast_manager & m, char const * fresh_prefix) {
m_impl = alloc(impl, m, fresh_prefix);
m_pos_impl = alloc(pos_impl, m, fresh_prefix);
}
defined_names::~defined_names() {
dealloc(m_impl);
dealloc(m_pos_impl);
}
bool defined_names::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
return m_impl->mk_name(e, new_def, new_def_pr, n, pr);
}
bool defined_names::mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
return m_pos_impl->mk_name(e, new_def, new_def_pr, n, pr);
}
void defined_names::push() {
m_impl->push_scope();
m_pos_impl->push_scope();
}
void defined_names::pop(unsigned num_scopes) {
m_impl->pop_scope(num_scopes);
m_pos_impl->pop_scope(num_scopes);
}
void defined_names::reset() {
m_impl->reset();
m_pos_impl->reset();
}
unsigned defined_names::get_num_names() const {
return m_impl->get_num_names() + m_pos_impl->get_num_names();
}
func_decl * defined_names::get_name_decl(unsigned i) const {
SASSERT(i < get_num_names());
unsigned n1 = m_impl->get_num_names();
return i < n1 ? m_impl->get_name_decl(i) : m_pos_impl->get_name_decl(i - n1);
}

88
src/ast/normal_forms/defined_names.h
View file

@ -21,7 +21,6 @@ Revision History:
#define _DEFINED_NAMES_H_
#include"ast.h"
#include"obj_hashtable.h"
/**
\brief Mapping from expressions to skolem functions that are used to name them.
@ -29,62 +28,13 @@ Revision History:
The mapping supports backtracking using the methods #push_scope and #pop_scope.
*/
class defined_names {
struct impl {
typedef obj_map<expr, app *> expr2name;
typedef obj_map<expr, proof *> expr2proof;
ast_manager & m_manager;
symbol m_z3name;
/**
\brief Mapping from expressions to their names. A name is an application.
If the expression does not have free variables, then the name is just a constant.
*/
expr2name m_expr2name;
/**
\brief Mapping from expressions to the apply-def proof.
That is, for each expression e, m_expr2proof[e] is the
proof e and m_expr2name[2] are observ. equivalent.
This mapping is not used if proof production is disabled.
*/
expr2proof m_expr2proof;
/**
\brief Domain of m_expr2name. It is used to keep the expressions
alive and for backtracking
*/
expr_ref_vector m_exprs;
expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
unsigned_vector m_lims; //!< Backtracking support.
impl(ast_manager & m, char const * prefix);
virtual ~impl();
app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
void cache_new_name(expr * e, app * name);
void cache_new_name_intro_proof(expr * e, proof * pr);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result);
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
void push_scope();
void pop_scope(unsigned num_scopes);
void reset();
};
struct pos_impl : public impl {
pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
};
impl m_impl;
pos_impl m_pos_impl;
struct impl;
struct pos_impl;
impl * m_impl;
pos_impl * m_pos_impl;
public:
defined_names(ast_manager & m, char const * fresh_prefix = "z3name"):m_impl(m, fresh_prefix), m_pos_impl(m, fresh_prefix) {}
defined_names(ast_manager & m, char const * fresh_prefix = "z3name");
~defined_names();
// -----------------------------------
//
@ -113,9 +63,7 @@ public:
Remark: the definitions are closed with an universal quantifier if e contains free variables.
*/
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
return m_impl.mk_name(e, new_def, new_def_pr, n, pr);
}
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
/**
\brief Create a name for a positive occurrence of the expression \c e.
@ -127,24 +75,14 @@ public:
Remark: the definitions are closed with an universal quantifier if e contains free variables.
*/
bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
return m_pos_impl.mk_name(e, new_def, new_def_pr, n, pr);
}
bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
void push_scope() {
m_impl.push_scope();
m_pos_impl.push_scope();
}
void push();
void pop(unsigned num_scopes);
void reset();
void pop_scope(unsigned num_scopes) {
m_impl.pop_scope(num_scopes);
m_pos_impl.pop_scope(num_scopes);
}
void reset() {
m_impl.reset();
m_pos_impl.reset();
}
unsigned get_num_names() const;
func_decl * get_name_decl(unsigned i) const;
};
#endif /* _DEFINED_NAMES_H_ */

2
src/muz_qe/dl_mk_extract_quantifiers2.cpp
View file

@ -333,7 +333,7 @@ namespace datalog {
smt::quantifier_manager* qm = ctx.get_quantifier_manager();
qm->get_plugin()->set_instance_plugin(alloc(instance_plugin, *this));
#endif
lbool res = solver.check();
solver.check();
for (unsigned i = 0; i < m_bindings.size(); ++i) {
expr_ref_vector& binding = m_bindings[i];

37
src/nlsat/nlsat_explain.cpp
View file

@ -981,6 +981,14 @@ namespace nlsat {
bool atom_val = a->get_kind() == atom::EQ;
bool lit_val = l.sign() ? !atom_val : atom_val;
new_lit = lit_val ? true_literal : false_literal;
if (!info.m_lc_const) {
// We have essentially shown the current factor must be zero If the leading coefficient is not zero.
// Note that, if the current factor is zero, then the whole polynomial is zero.
// The atom is true if it is an equality, and false otherwise.
// The sign of the leading coefficient (info.m_lc) of info.m_eq doesn't matter.
// However, we have to store the fact it is not zero.
info.add_lc_diseq();
}
return;
}
else if (s == -1 && !is_even) {
@ -1341,3 +1349,32 @@ namespace nlsat {
}
};
#ifdef Z3DEBUG
void pp(nlsat::explain::imp & ex, unsigned num, nlsat::literal const * ls) {
ex.display(std::cout, num, ls);
}
void pp(nlsat::explain::imp & ex, nlsat::scoped_literal_vector & ls) {
ex.display(std::cout, ls);
}
void pp(nlsat::explain::imp & ex, polynomial_ref const & p) {
ex.display(std::cout, p);
std::cout << std::endl;
}
void pp(nlsat::explain::imp & ex, polynomial::polynomial * p) {
polynomial_ref _p(p, ex.m_pm);
ex.display(std::cout, _p);
std::cout << std::endl;
}
void pp(nlsat::explain::imp & ex, polynomial_ref_vector const & ps) {
ex.display(std::cout, ps);
}
void pp_var(nlsat::explain::imp & ex, nlsat::var x) {
ex.display(std::cout, x);
std::cout << std::endl;
}
void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
ex.display(std::cout, l);
std::cout << std::endl;
}
#endif

2
src/nlsat/nlsat_explain.h
View file

@ -27,7 +27,9 @@ namespace nlsat {
class evaluator;
class explain {
public:
struct imp;
private:
imp * m_imp;
public:
explain(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,

4
src/smt/asserted_formulas.cpp
View file

@ -189,7 +189,7 @@ void asserted_formulas::push_scope() {
s.m_asserted_formulas_lim = m_asserted_formulas.size();
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead);
s.m_inconsistent_old = m_inconsistent;
m_defined_names.push_scope();
m_defined_names.push();
m_bv_sharing.push_scope();
commit();
}
@ -201,7 +201,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
unsigned new_lvl = m_scopes.size() - num_scopes;
scope & s = m_scopes[new_lvl];
m_inconsistent = s.m_inconsistent_old;
m_defined_names.pop_scope(num_scopes);
m_defined_names.pop(num_scopes);
m_asserted_formulas.shrink(s.m_asserted_formulas_lim);
if (m_manager.proofs_enabled())
m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim);

5
src/smt/params/qi_params.h
View file

@ -52,8 +52,6 @@ struct qi_params {
bool m_mbqi_trace;
unsigned m_mbqi_force_template;
bool m_instgen;
qi_params(params_ref const & p = params_ref()):
/*
The "weight 0" performance bug
@ -99,8 +97,7 @@ struct qi_params {
m_mbqi_max_cexs_incr(1),
m_mbqi_max_iterations(1000),
m_mbqi_trace(false),
m_mbqi_force_template(10),
m_instgen(false) {
m_mbqi_force_template(10) {
updt_params(p);
}

4
src/smt/params/smt_params.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include"smt_params.h"
#include"smt_params_helper.hpp"
#include"model_params.hpp"
void smt_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
@ -33,6 +34,8 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
m_soft_timeout = p.soft_timeout();
model_params mp(_p);
m_model_compact = mp.compact();
if (_p.get_bool("arith.greatest_error_pivot", false))
m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
else if (_p.get_bool("arith.least_error_pivot", false))
@ -50,5 +53,4 @@ void smt_params::updt_params(params_ref const & p) {
void smt_params::updt_params(context_params const & p) {
m_auto_config = p.m_auto_config;
m_model = p.m_model;
m_model_validate = p.m_model_validate;
}

2
src/smt/params/smt_params.h
View file

@ -177,7 +177,6 @@ struct smt_params : public preprocessor_params,
// -----------------------------------
bool m_model;
bool m_model_compact;
bool m_model_validate;
bool m_model_on_timeout;
bool m_model_on_final_check;
@ -264,7 +263,6 @@ struct smt_params : public preprocessor_params,
m_abort_after_preproc(false),
m_model(true),
m_model_compact(false),
m_model_validate(false),
m_model_on_timeout(false),
m_model_on_final_check(false),
m_progress_sampling_freq(0),

6
src/smt/smt_internalizer.cpp
View file

@ -23,7 +23,6 @@ Revision History:
#include"ast_smt2_pp.h"
#include"smt_model_finder.h"
#include"for_each_expr.h"
#include"theory_instgen.h"
namespace smt {
@ -530,11 +529,6 @@ namespace smt {
SASSERT(!b_internalized(q));
SASSERT(q->is_forall());
SASSERT(check_patterns(q));
if (m_fparams.m_instgen) {
theory* th = m_theories.get_plugin(m_manager.get_family_id("inst_gen"));
static_cast<theory_instgen*>(th)->internalize_quantifier(q);
return;
}
bool_var v = mk_bool_var(q);
unsigned generation = m_generation;
unsigned _generation;

7
src/smt/smt_setup.cpp
View file

@ -28,7 +28,6 @@ Revision History:
#include"theory_datatype.h"
#include"theory_dummy.h"
#include"theory_dl.h"
#include"theory_instgen.h"
#include"theory_seq_empty.h"
namespace smt {
@ -772,11 +771,6 @@ namespace smt {
void setup::setup_seq() {
m_context.register_plugin(alloc(theory_seq_empty, m_manager));
}
void setup::setup_instgen() {
if (m_params.m_instgen) {
m_context.register_plugin(mk_theory_instgen(m_manager, m_params));
}
}
void setup::setup_unknown() {
setup_arith();
@ -784,7 +778,6 @@ namespace smt {
setup_bv();
setup_datatypes();
setup_dl();
setup_instgen();
setup_seq();
}

1494
src/smt/theory_instgen.cpp
View file

File diff suppressed because it is too large Load diff

45
src/smt/theory_instgen.h
View file

@ -1,45 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
theory_instgen.h
Abstract:
InstGen (iProver) style theory solver.
It provides an instantiation based engine
based on InstGen methods together with
unit propagation.
Author:
Krystof Hoder (t-khoder)
Nikolaj Bjorner (nbjorner) 2011-10-6
Revision History:
--*/
#ifndef _THEORY_INST_GEN_H_
#define _THEORY_INST_GEN_H_
#include "smt_theory.h"
#include "smt_params.h"
namespace smt {
class theory_instgen : public theory {
public:
theory_instgen(family_id fid) : theory(fid) {}
virtual ~theory_instgen() {}
virtual void internalize_quantifier(quantifier* q) = 0;
virtual char const * get_name() const { return "instgen"; }
};
theory_instgen* mk_theory_instgen(ast_manager& m, smt_params& p);
};
#endif /* _THEORY_INST_GEN_H_ */

4
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -18,7 +18,7 @@ Notes:
--*/
#include"ctx_simplify_tactic.h"
#include"mk_simplified_app.h"
#include"num_occurs_goal.h"
#include"goal_num_occurs.h"
#include"cooperate.h"
#include"ast_ll_pp.h"
#include"ast_smt2_pp.h"
@ -51,7 +51,7 @@ struct ctx_simplify_tactic::imp {
unsigned m_scope_lvl;
unsigned m_depth;
unsigned m_num_steps;
num_occurs_goal m_occs;
goal_num_occurs m_occs;
mk_simplified_app m_mk_app;
unsigned long long m_max_memory;
unsigned m_max_depth;

8
src/tactic/core/nnf_tactic.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include"nnf.h"
#include"tactical.h"
#include"filter_model_converter.h"
class nnf_tactic : public tactic {
params_ref m_params;
@ -100,6 +101,13 @@ public:
}
g->inc_depth();
result.push_back(g.get());
unsigned num_extra_names = dnames.get_num_names();
if (num_extra_names > 0) {
filter_model_converter * fmc = alloc(filter_model_converter, m);
mc = fmc;
for (unsigned i = 0; i < num_extra_names; i++)
fmc->insert(dnames.get_name_decl(i));
}
TRACE("nnf", g->display(tout););
SASSERT(g->is_well_sorted());
}

6
src/tactic/num_occurs_goal.cpp → src/tactic/goal_num_occurs.cpp
View file

@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
num_occurs_goal.cpp
goal_num_occurs.cpp
Abstract:
@ -15,10 +15,10 @@ Author:
Revision History:
--*/
#include"num_occurs_goal.h"
#include"goal_num_occurs.h"
#include"goal.h"
void num_occurs_goal::operator()(goal const & g) {
void goal_num_occurs::operator()(goal const & g) {
expr_fast_mark1 visited;
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {

10
src/tactic/num_occurs_goal.h → src/tactic/goal_num_occurs.h
View file

@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
Module Name:
num_occurs_goal.h
goal_num_occurs.h
Abstract:
@ -15,16 +15,16 @@ Author:
Revision History:
--*/
#ifndef _NUM_OCCURS_GOAL_H_
#define _NUM_OCCURS_GOAL_H_
#ifndef _GOAL_NUM_OCCURS_H_
#define _GOAL_NUM_OCCURS_H_
#include"num_occurs.h"
class goal;
class num_occurs_goal : public num_occurs {
class goal_num_occurs : public num_occurs {
public:
num_occurs_goal(bool ignore_ref_count1 = false, bool ignore_quantifiers = false):
goal_num_occurs(bool ignore_ref_count1 = false, bool ignore_quantifiers = false):
num_occurs(ignore_ref_count1, ignore_quantifiers) {
}