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

Merge branch 'develop' of github.com:/mtrberzi/z3 into develop

Browse source
This commit is contained in:
Murphy Berzish 2017-11-09 13:33:47 -05:00
parent 30f958f291 975368e16a
commit 3e53d00f81
34 changed files with 637 additions and 403 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
scripts/mk_project.py
View file

@ -37,13 +37,13 @@ def init_project_def():
add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
add_lib('aig_tactic', ['tactic'], 'tactic/aig')
add_lib('solver', ['model', 'tactic'])
add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
add_lib('solver', ['model', 'tactic', 'proofs'])
add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
add_lib('interp', ['solver'])
add_lib('cmd_context', ['solver', 'rewriter', 'interp'])
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
add_lib('bit_blaster', ['rewriter', 'rewriter'], 'ast/rewriter/bit_blaster')

29
scripts/mk_util.py
View file

@ -72,6 +72,7 @@ IS_FREEBSD=False
IS_OPENBSD=False
IS_CYGWIN=False
IS_CYGWIN_MINGW=False
IS_MSYS2=False
VERBOSE=True
DEBUG_MODE=False
SHOW_CPPS = True
@ -152,6 +153,9 @@ def is_cygwin():
def is_cygwin_mingw():
return IS_CYGWIN_MINGW
def is_msys2():
return IS_MSYS2
def norm_path(p):
return os.path.expanduser(os.path.normpath(p))
@ -227,7 +231,7 @@ def rmf(fname):
def exec_compiler_cmd(cmd):
r = exec_cmd(cmd)
if is_windows() or is_cygwin_mingw():
if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2():
rmf('a.exe')
else:
rmf('a.out')
@ -606,6 +610,13 @@ elif os.name == 'posix':
IS_CYGWIN=True
if (CC != None and "mingw" in CC):
IS_CYGWIN_MINGW=True
elif os.uname()[0].startswith('MSYS_NT') or os.uname()[0].startswith('MINGW'):
IS_MSYS2=True
if os.uname()[4] == 'x86_64':
LINUX_X64=True
else:
LINUX_X64=False
def display_help(exit_code):
print("mk_make.py: Z3 Makefile generator\n")
@ -1229,7 +1240,7 @@ def get_so_ext():
sysname = os.uname()[0]
if sysname == 'Darwin':
return 'dylib'
elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
return 'so'
elif sysname == 'CYGWIN':
return 'dll'
@ -1783,6 +1794,8 @@ class JavaDLLComponent(Component):
t = t.replace('PLATFORM', 'openbsd')
elif IS_CYGWIN:
t = t.replace('PLATFORM', 'cygwin')
elif IS_MSYS2:
t = t.replace('PLATFORM', 'win32')
else:
t = t.replace('PLATFORM', 'win32')
out.write(t)
@ -1875,7 +1888,6 @@ class MLComponent(Component):
def _init_ocamlfind_paths(self):
"""
Initialises self.destdir and self.ldconf
Do not call this from the MLComponent constructor because OCAMLFIND
has not been checked at that point
"""
@ -2446,7 +2458,7 @@ def mk_config():
if sysname == 'Darwin':
SO_EXT = '.dylib'
SLIBFLAGS = '-dynamiclib'
elif sysname == 'Linux':
elif sysname == 'Linux' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS
OS_DEFINES = '-D_LINUX_'
SO_EXT = '.so'
@ -2466,10 +2478,10 @@ def mk_config():
SO_EXT = '.so'
SLIBFLAGS = '-shared'
elif sysname[:6] == 'CYGWIN':
CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS
OS_DEFINES = '-D_CYGWIN'
SO_EXT = '.dll'
SLIBFLAGS = '-shared'
SO_EXT = '.dll'
SLIBFLAGS = '-shared'
else:
raise MKException('Unsupported platform: %s' % sysname)
if is64():
@ -3160,7 +3172,6 @@ class MakeRuleCmd(object):
"""
These class methods provide a convenient way to emit frequently
needed commands used in Makefile rules
Note that several of the method are meant for use during ``make
install`` and ``make uninstall``. These methods correctly use
``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferrable
@ -3336,10 +3347,8 @@ def configure_file(template_file_path, output_file_path, substitutions):
Read a template file ``template_file_path``, perform substitutions
found in the ``substitutions`` dictionary and write the result to
the output file ``output_file_path``.
The template file should contain zero or more template strings of the
form ``@NAME@``.
The substitutions dictionary maps old strings (without the ``@``
symbols) to their replacements.
"""

58
src/ast/ast.cpp
View file

@ -1683,7 +1683,7 @@ ast * ast_manager::register_node_core(ast * n) {
bool contains = m_ast_table.contains(n);
CASSERT("nondet_bug", contains || slow_not_contains(n));
#endif
#if 0
static unsigned counter = 0;
counter++;
@ -1719,12 +1719,6 @@ ast * ast_manager::register_node_core(ast * n) {
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
static unsigned count = 0;
if (n->m_id == 404) {
++count;
//if (count == 2) SASSERT(false);
}
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
// increment reference counters
@ -2626,7 +2620,7 @@ bool ast_manager::is_fully_interp(sort * s) const {
proof * ast_manager::mk_proof(family_id fid, decl_kind k, unsigned num_args, expr * const * args) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(fid, k, num_args, args);
}
@ -2842,23 +2836,20 @@ proof * ast_manager::mk_distributivity(expr * s, expr * r) {
}
proof * ast_manager::mk_rewrite(expr * s, expr * t) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t));
}
proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(m_basic_family_id, PR_REWRITE, mk_oeq(s, t));
}
proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.push_back(mk_eq(s, t));
@ -2866,44 +2857,38 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr
}
proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
}
proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
}
proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(m_basic_family_id, PR_PUSH_QUANT, mk_iff(q, e));
}
proof * ast_manager::mk_elim_unused_vars(quantifier * q, expr * e) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e));
}
proof * ast_manager::mk_der(quantifier * q, expr * e) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(m_basic_family_id, PR_DER, mk_iff(q, e));
}
proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
vector<parameter> params;
for (unsigned i = 0; i < num_bind; ++i) {
params.push_back(parameter(binding[i]));
@ -2937,9 +2922,8 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
}
proof * ast_manager::mk_def_axiom(expr * ax) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return nullptr;
return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax);
}
@ -3077,7 +3061,7 @@ proof * ast_manager::mk_def_intro(expr * new_def) {
proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, proof * const * proofs) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.push_back(mk_oeq(n, def));
@ -3110,7 +3094,7 @@ bool ast_manager::check_nnf_proof_parents(unsigned num_proofs, proof * const * p
proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
check_nnf_proof_parents(num_proofs, proofs);
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
@ -3120,7 +3104,7 @@ proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof *
proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
check_nnf_proof_parents(num_proofs, proofs);
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
@ -3130,7 +3114,7 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.push_back(mk_oeq(s, t));
@ -3139,7 +3123,7 @@ proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof
proof * ast_manager::mk_skolemization(expr * q, expr * e) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
SASSERT(is_bool(q));
SASSERT(is_bool(e));
return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e));
@ -3147,7 +3131,7 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.push_back(mk_oeq(s, t));
@ -3156,7 +3140,7 @@ proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof
proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
SASSERT(has_fact(p));
SASSERT(is_and(get_fact(p)));
CTRACE("mk_and_elim", i >= to_app(get_fact(p))->get_num_args(), tout << "i: " << i << "\n" << mk_pp(get_fact(p), *this) << "\n";);
@ -3167,7 +3151,7 @@ proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) {
if (proofs_disabled())
return m_undef_proof;
return nullptr;
SASSERT(has_fact(p));
SASSERT(is_not(get_fact(p)));
SASSERT(is_or(to_app(get_fact(p))->get_arg(0)));
@ -3190,7 +3174,7 @@ proof * ast_manager::mk_th_lemma(
)
{
if (proofs_disabled())
return m_undef_proof;
return nullptr;
ptr_buffer<expr> args;
vector<parameter> parameters;

1
src/ast/ast_smt2_pp.cpp
View file

@ -44,6 +44,7 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len) co
return mk_string(m, str.c_str());
}
else if (!s.bare_str()) {
len = 4;
return mk_string(m, "null");
}
else {

3
src/ast/rewriter/rewriter_def.h
View file

@ -351,7 +351,6 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
if (is_ground(def)) {
m_r = def;
if (ProofGen) {
SASSERT(def_pr);
m_pr = m().mk_transitivity(m_pr, def_pr);
}
}
@ -510,7 +509,7 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
new_no_pats = q->get_no_patterns();
}
if (ProofGen) {
quantifier * new_q = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body);
quantifier_ref new_q(m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body), m());
m_pr = q == new_q ? 0 : m().mk_quant_intro(q, new_q, result_pr_stack().get(fr.m_spos));
m_r = new_q;
proof_ref pr2(m());

94
src/duality/duality_rpfp.cpp
View file

@ -1575,6 +1575,7 @@ namespace Duality {
*/
int RPFP::SubtermTruth(hash_map<ast, int> &memo, const Term &f) {
TRACE("duality", tout << f << "\n";);
if (memo.find(f) != memo.end()) {
return memo[f];
}
@ -1657,83 +1658,6 @@ namespace Duality {
ands and, or, not. Returns result in memo.
*/
#if 0
int RPFP::GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos){
if(memo[labpos].find(f) != memo[labpos].end()){
return memo[labpos][f];
}
int res;
if(f.is_app()){
int nargs = f.num_args();
decl_kind k = f.decl().get_decl_kind();
if(k == Implies){
res = GetLabelsRec(memo,f.arg(1) || !f.arg(0), labels, labpos);
goto done;
}
if(k == And) {
res = 1;
for(int i = 0; i < nargs; i++){
int ar = GetLabelsRec(memo,f.arg(i), labels, labpos);
if(ar == 0){
res = 0;
goto done;
}
if(ar == 2)res = 2;
}
goto done;
}
else if(k == Or) {
res = 0;
for(int i = 0; i < nargs; i++){
int ar = GetLabelsRec(memo,f.arg(i), labels, labpos);
if(ar == 1){
res = 1;
goto done;
}
if(ar == 2)res = 2;
}
goto done;
}
else if(k == Not) {
int ar = GetLabelsRec(memo,f.arg(0), labels, !labpos);
res = (ar == 0) ? 1 : ((ar == 1) ? 0 : 2);
goto done;
}
}
{
bool pos; std::vector<symbol> names;
if(f.is_label(pos,names)){
res = GetLabelsRec(memo,f.arg(0), labels, labpos);
if(pos == labpos && res == (pos ? 1 : 0))
for(unsigned i = 0; i < names.size(); i++)
labels.push_back(names[i]);
goto done;
}
}
{
expr bv = dualModel.eval(f);
if(bv.is_app() && bv.decl().get_decl_kind() == Equal &&
bv.arg(0).is_array()){
bv = EvalArrayEquality(bv);
}
// Hack!!!! array equalities can occur negatively!
if(bv.is_app() && bv.decl().get_decl_kind() == Not &&
bv.arg(0).decl().get_decl_kind() == Equal &&
bv.arg(0).arg(0).is_array()){
bv = dualModel.eval(!EvalArrayEquality(bv.arg(0)));
}
if(eq(bv,ctx.bool_val(true)))
res = 1;
else if(eq(bv,ctx.bool_val(false)))
res = 0;
else
res = 2;
}
done:
memo[labpos][f] = res;
return res;
}
#endif
void RPFP::GetLabelsRec(hash_map<ast, int> &memo, const Term &f, std::vector<symbol> &labels,
hash_set<ast> *done, bool truth) {
@ -1748,8 +1672,13 @@ namespace Duality {
}
if (k == Iff) {
int b = SubtermTruth(memo, f.arg(0));
if (b == 2)
throw "disaster in GetLabelsRec";
if (b == 2) {
goto done;
// bypass error
std::ostringstream os;
os << "disaster in SubtermTruth processing " << f;
throw default_exception(os.str());
}
GetLabelsRec(memo, f.arg(1), labels, done, truth ? b : !b);
goto done;
}
@ -1825,8 +1754,11 @@ namespace Duality {
}
if (k == Iff) {
int b = SubtermTruth(memo, f.arg(0));
if (b == 2)
throw "disaster in ImplicantRed";
if (b == 2) {
std::ostringstream os;
os << "disaster in SubtermTruth processing " << f;
throw default_exception(os.str());
}
ImplicantRed(memo, f.arg(1), lits, done, truth ? b : !b, dont_cares);
goto done;
}

74
src/muz/dataflow/dataflow.h
View file

@ -62,8 +62,7 @@ namespace datalog {
rule_set::decl2rules m_body2rules;
void init_bottom_up() {
for (rule_set::iterator it = m_rules.begin(); it != m_rules.end(); ++it) {
rule* cur = *it;
for (rule* cur : m_rules) {
for (unsigned i = 0; i < cur->get_uninterpreted_tail_size(); ++i) {
func_decl *d = cur->get_decl(i);
rule_set::decl2rules::obj_map_entry *e = m_body2rules.insert_if_not_there2(d, 0);
@ -83,31 +82,25 @@ namespace datalog {
}
void init_top_down() {
const func_decl_set& output_preds = m_rules.get_output_predicates();
for (func_decl_set::iterator I = output_preds.begin(),
E = output_preds.end(); I != E; ++I) {
func_decl* sym = *I;
for (func_decl* sym : m_rules.get_output_predicates()) {
TRACE("dl", tout << sym->get_name() << "\n";);
const rule_vector& output_rules = m_rules.get_predicate_rules(sym);
for (unsigned i = 0; i < output_rules.size(); ++i) {
m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, output_rules[i]);
for (rule* r : output_rules) {
m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, r);
m_todo[m_todo_idx].insert(sym);
}
}
}
void step_bottom_up() {
for(todo_set::iterator I = m_todo[m_todo_idx].begin(),
E = m_todo[m_todo_idx].end(); I!=E; ++I) {
for (func_decl* f : m_todo[m_todo_idx]) {
ptr_vector<rule> * rules;
if (!m_body2rules.find(*I, rules))
if (!m_body2rules.find(f, rules))
continue;
for (ptr_vector<rule>::iterator I2 = rules->begin(),
E2 = rules->end(); I2 != E2; ++I2) {
func_decl* head_sym = (*I2)->get_head()->get_decl();
fact_reader<Fact> tail_facts(m_facts, *I2);
bool new_info = m_facts.insert_if_not_there2(head_sym, Fact())->get_data().m_value.propagate_up(m_context, *I2, tail_facts);
for (rule* r : *rules) {
func_decl* head_sym = r->get_head()->get_decl();
fact_reader<Fact> tail_facts(m_facts, r);
bool new_info = m_facts.insert_if_not_there2(head_sym, Fact())->get_data().m_value.propagate_up(m_context, r, tail_facts);
if (new_info) {
m_todo[!m_todo_idx].insert(head_sym);
}
@ -119,15 +112,11 @@ namespace datalog {
}
void step_top_down() {
for(todo_set::iterator I = m_todo[m_todo_idx].begin(),
E = m_todo[m_todo_idx].end(); I!=E; ++I) {
func_decl* head_sym = *I;
for (func_decl* head_sym : m_todo[m_todo_idx]) {
// We can't use a reference here because we are changing the map while using the reference
const Fact head_fact = m_facts.get(head_sym, Fact::null_fact);
const rule_vector& deps = m_rules.get_predicate_rules(head_sym);
const unsigned deps_size = deps.size();
for (unsigned i = 0; i < deps_size; ++i) {
rule *trg_rule = deps[i];
for (rule* trg_rule : deps) {
fact_writer<Fact> writer(m_facts, trg_rule, m_todo[!m_todo_idx]);
// Generate new facts
head_fact.propagate_down(m_context, trg_rule, writer);
@ -146,16 +135,13 @@ namespace datalog {
dataflow_engine(typename Fact::ctx_t& ctx, const rule_set& rules) : m_rules(rules), m_todo_idx(0), m_context(ctx) {}
~dataflow_engine() {
for (rule_set::decl2rules::iterator it = m_body2rules.begin(); it != m_body2rules.end(); ++it) {
dealloc(it->m_value);
}
for (auto & kv : m_body2rules)
dealloc(kv.m_value);
}
void dump(std::ostream& outp) {
obj_hashtable<func_decl> visited;
for (rule_set::iterator I = m_rules.begin(),
E = m_rules.end(); I != E; ++I) {
const rule* r = *I;
for (rule const* r : m_rules) {
func_decl* head_decl = r->get_decl();
obj_hashtable<func_decl>::entry *dummy;
if (visited.insert_if_not_there_core(head_decl, dummy)) {
@ -194,30 +180,30 @@ namespace datalog {
iterator end() const { return m_facts.end(); }
void join(const dataflow_engine<Fact>& oth) {
for (typename fact_db::iterator I = oth.m_facts.begin(),
E = oth.m_facts.end(); I != E; ++I) {
for (auto const& kv : oth.m_facts) {
typename fact_db::entry* entry;
if (m_facts.insert_if_not_there_core(I->m_key, entry)) {
entry->get_data().m_value = I->m_value;
} else {
entry->get_data().m_value.join(m_context, I->m_value);
if (m_facts.insert_if_not_there_core(kv.m_key, entry)) {
entry->get_data().m_value = kv.m_value;
}
else {
entry->get_data().m_value.join(m_context, kv.m_value);
}
}
}
void intersect(const dataflow_engine<Fact>& oth) {
vector<func_decl*> to_delete;
for (typename fact_db::iterator I = m_facts.begin(),
E = m_facts.end(); I != E; ++I) {
ptr_vector<func_decl> to_delete;
for (auto const& kv : m_facts) {
if (typename fact_db::entry *entry = oth.m_facts.find_core(I->m_key)) {
I->m_value.intersect(m_context, entry->get_data().m_value);
} else {
to_delete.push_back(I->m_key);
if (typename fact_db::entry *entry = oth.m_facts.find_core(kv.m_key)) {
kv.m_value.intersect(m_context, entry->get_data().m_value);
}
else {
to_delete.push_back(kv.m_key);
}
}
for (unsigned i = 0; i < to_delete.size(); ++i) {
m_facts.erase(to_delete[i]);
for (func_decl* f : to_delete) {
m_facts.erase(f);
}
}
};

4
src/muz/spacer/spacer_itp_solver.h
View file

@ -134,8 +134,8 @@ public:
{return m_solver.get_num_assumptions();}
virtual expr * get_assumption(unsigned idx) const
{return m_solver.get_assumption(idx);}
virtual std::ostream &display(std::ostream &out) const
{ return m_solver.display(out); }
virtual std::ostream &display(std::ostream &out, unsigned n, expr* const* es) const
{ return m_solver.display(out, n, es); }
/* check_sat_result interface */

9
src/muz/spacer/spacer_util.h
View file

@ -74,15 +74,6 @@ inline std::ostream& operator<<(std::ostream& out, pp_level const& p)
}
struct scoped_watch {
stopwatch &m_sw;
scoped_watch (stopwatch &sw, bool reset=false): m_sw(sw)
{
if(reset) { m_sw.reset(); }
m_sw.start ();
}
~scoped_watch () {m_sw.stop ();}
};
typedef ptr_vector<app> app_vector;

9
src/muz/spacer/spacer_virtual_solver.cpp
View file

@ -189,15 +189,16 @@ void virtual_solver::push_core()
m_context.push();
}
}
void virtual_solver::pop_core(unsigned n)
{
void virtual_solver::pop_core(unsigned n) {
SASSERT(!m_pushed || get_scope_level() > 0);
if (m_pushed) {
SASSERT(!m_in_delay_scope);
m_context.pop(n);
m_pushed = get_scope_level() - n > 0;
} else
{ m_in_delay_scope = get_scope_level() - n > 0; }
}
else {
m_in_delay_scope = get_scope_level() - n > 0;
}
}
void virtual_solver::get_unsat_core(ptr_vector<expr> &r)

60
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -21,6 +21,7 @@ Author:
#include "muz/dataflow/dataflow.h"
#include "muz/dataflow/reachability.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "tactic/extension_model_converter.h"
namespace datalog {
@ -33,20 +34,28 @@ namespace datalog {
rule_set * mk_coi_filter::bottom_up(rule_set const & source) {
dataflow_engine<reachability_info> engine(source.get_manager(), source);
engine.run_bottom_up();
func_decl_set unreachable;
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
res->inherit_predicates(source);
for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
rule * r = *it;
for (rule* r : source) {
bool new_tail = false;
bool contained = true;
m_new_tail.reset();
m_new_tail_neg.reset();
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
if (m_context.has_facts(r->get_decl(i))) {
func_decl* decl_i = r->get_decl(i);
if (m_context.has_facts(decl_i)) {
return 0;
}
bool reachable = engine.get_fact(decl_i).is_reachable();
if (!reachable) {
unreachable.insert(decl_i);
}
if (r->is_neg_tail(i)) {
if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
if (!reachable) {
if (!new_tail) {
for (unsigned j = 0; j < i; ++j) {
m_new_tail.push_back(r->get_tail(j));
@ -60,10 +69,9 @@ namespace datalog {
m_new_tail_neg.push_back(true);
}
}
else {
SASSERT(!new_tail);
if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
if (!reachable) {
contained = false;
break;
}
@ -78,24 +86,26 @@ namespace datalog {
res->add_rule(r);
}
}
m_new_tail.reset();
m_new_tail_neg.reset();
}
if (res->get_num_rules() == source.get_num_rules()) {
TRACE("dl", tout << "No transformation\n";);
res = 0;
} else {
}
else {
res->close();
}
// set to false each unreached predicate
if (m_context.get_model_converter()) {
if (res && m_context.get_model_converter()) {
extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (dataflow_engine<reachability_info>::iterator it = engine.begin(); it != engine.end(); it++) {
if (!it->m_value.is_reachable()) {
mc0->insert(it->m_key, m.mk_false());
for (auto const& kv : engine) {
if (!kv.m_value.is_reachable()) {
mc0->insert(kv.m_key, m.mk_false());
}
}
for (func_decl* f : unreachable) {
mc0->insert(f, m.mk_false());
}
m_context.add_model_converter(mc0);
}
CTRACE("dl", 0 != res, res->display(tout););
@ -109,9 +119,7 @@ namespace datalog {
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
res->inherit_predicates(source);
rule_set::iterator rend = source.end();
for (rule_set::iterator rit = source.begin(); rit != rend; ++rit) {
rule * r = *rit;
for (rule * r : source) {
func_decl * pred = r->get_decl();
if (engine.get_fact(pred).is_reachable()) {
res->add_rule(r);
@ -125,14 +133,12 @@ namespace datalog {
res = 0;
}
if (res && m_context.get_model_converter()) {
func_decl_set::iterator end = pruned_preds.end();
func_decl_set::iterator it = pruned_preds.begin();
extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (; it != end; ++it) {
const rule_vector& rules = source.get_predicate_rules(*it);
for (func_decl* f : pruned_preds) {
const rule_vector& rules = source.get_predicate_rules(f);
expr_ref_vector fmls(m);
for (unsigned i = 0; i < rules.size(); ++i) {
app* head = rules[i]->get_head();
for (rule * r : rules) {
app* head = r->get_head();
expr_ref_vector conj(m);
for (unsigned j = 0; j < head->get_num_args(); ++j) {
expr* arg = head->get_arg(j);
@ -140,11 +146,9 @@ namespace datalog {
conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg));
}
}
fmls.push_back(m.mk_and(conj.size(), conj.c_ptr()));
fmls.push_back(mk_and(conj));
}
expr_ref fml(m);
fml = m.mk_or(fmls.size(), fmls.c_ptr());
mc0->insert(*it, fml);
mc0->insert(f, mk_or(fmls));
}
m_context.add_model_converter(mc0);
}

3
src/opt/opt_solver.cpp
View file

@ -47,8 +47,9 @@ namespace opt {
m_dump_benchmarks(false),
m_first(true),
m_was_unknown(false) {
solver::updt_params(p);
m_params.updt_params(p);
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
m_params.m_relevancy_lvl = 0;
}
// m_params.m_auto_config = false;

6
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -69,7 +69,7 @@ class inc_sat_solver : public solver {
public:
inc_sat_solver(ast_manager& m, params_ref const& p):
m(m), m_solver(p, m.limit(), 0),
m_params(p), m_optimize_model(false),
m_optimize_model(false),
m_fmls(m),
m_asmsf(m),
m_fmls_head(0),
@ -79,7 +79,7 @@ public:
m_dep_core(m),
m_unknown("no reason given") {
m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params);
updt_params(p);
init_preprocess();
}
@ -237,7 +237,7 @@ public:
sat::solver::collect_param_descrs(r);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
solver::updt_params(p);
m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params);
m_optimize_model = m_params.get_bool("optimize_model", false);

9
src/smt/asserted_formulas.cpp
View file

@ -511,11 +511,14 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) {
}
TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
}
if (m.is_not(n, n1)) {
m_scoped_substitution.insert(n1, m.mk_false(), m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr);
proof_ref pr1(m);
if (m.is_not(n, n1)) {
pr1 = m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr;
m_scoped_substitution.insert(n1, m.mk_false(), pr1);
}
else {
m_scoped_substitution.insert(n, m.mk_true(), m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr);
pr1 = m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr;
m_scoped_substitution.insert(n, m.mk_true(), pr1);
}
}

3
src/smt/smt_context.cpp
View file

@ -4389,7 +4389,8 @@ namespace smt {
subst.push_back(arg);
}
expr_ref bodyr(m);
var_subst sub(m, false);
var_subst sub(m, true);
TRACE("context", tout << expr_ref(q, m) << " " << subst << "\n";);
sub(body, subst.size(), subst.c_ptr(), bodyr);
func_decl* f = to_app(fn)->get_decl();
func_interp* fi = alloc(func_interp, m, f->get_arity());

41
src/smt/smt_solver.cpp
View file

@ -29,9 +29,8 @@ Notes:
namespace smt {
class solver : public solver_na2as {
class smt_solver : public solver_na2as {
smt_params m_smt_params;
params_ref m_params;
smt::kernel m_context;
progress_callback * m_callback;
symbol m_logic;
@ -42,28 +41,24 @@ namespace smt {
obj_map<expr, expr*> m_name2assertion;
public:
solver(ast_manager & m, params_ref const & p, symbol const & l) :
smt_solver(ast_manager & m, params_ref const & p, symbol const & l) :
solver_na2as(m),
m_smt_params(p),
m_params(p),
m_context(m, m_smt_params),
m_minimizing_core(false),
m_core_extend_patterns(false),
m_core_extend_patterns_max_distance(UINT_MAX),
m_core_extend_nonlocal_patterns(false) {
m_core_extend_nonlocal_patterns(false) {
m_logic = l;
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
smt_params_helper smth(p);
m_core_extend_patterns = smth.core_extend_patterns();
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns();
updt_params(p);
}
virtual solver * translate(ast_manager & m, params_ref const & p) {
ast_translation translator(get_manager(), m);
solver * result = alloc(solver, m, p, m_logic);
smt_solver * result = alloc(smt_solver, m, p, m_logic);
smt::kernel::copy(m_context, result->m_context);
for (auto & kv : m_name2assertion)
@ -73,13 +68,13 @@ namespace smt {
return result;
}
virtual ~solver() {
virtual ~smt_solver() {
dec_ref_values(get_manager(), m_name2assertion);
}
virtual void updt_params(params_ref const & p) {
solver::updt_params(p);
m_smt_params.updt_params(p);
m_params.copy(p);
m_context.updt_params(p);
smt_params_helper smth(p);
m_core_extend_patterns = smth.core_extend_patterns();
@ -146,9 +141,9 @@ namespace smt {
}
struct scoped_minimize_core {
solver& s;
smt_solver& s;
expr_ref_vector m_assumptions;
scoped_minimize_core(solver& s) : s(s), m_assumptions(s.m_assumptions) {
scoped_minimize_core(smt_solver& s) : s(s), m_assumptions(s.m_assumptions) {
s.m_minimizing_core = true;
s.m_assumptions.reset();
}
@ -165,7 +160,7 @@ namespace smt {
r.push_back(m_context.get_unsat_core_expr(i));
}
if (m_minimizing_core && smt_params_helper(m_params).core_minimize()) {
if (m_minimizing_core && smt_params_helper(get_params()).core_minimize()) {
scoped_minimize_core scm(*this);
mus mus(*this);
mus.add_soft(r.size(), r.c_ptr());
@ -346,22 +341,16 @@ namespace smt {
void add_nonlocal_pattern_literals_to_core(ptr_vector<expr> & core) {
ast_manager & m = get_manager();
obj_map<expr, expr*>::iterator it = m_name2assertion.begin();
obj_map<expr, expr*>::iterator end = m_name2assertion.end();
for (unsigned i = 0; it != end; it++, i++) {
expr_ref name(it->m_key, m);
expr_ref assrtn(it->m_value, m);
for (auto const& kv : m_name2assertion) {
expr_ref name(kv.m_key, m);
expr_ref assrtn(kv.m_value, m);
if (!core.contains(name)) {
func_decl_set pattern_fds, body_fds;
collect_pattern_fds(assrtn, pattern_fds);
collect_body_func_decls(assrtn, body_fds);
func_decl_set::iterator pit = pattern_fds.begin();
func_decl_set::iterator pend= pattern_fds.end();
for (; pit != pend; pit++) {
func_decl * fd = *pit;
for (func_decl *fd : pattern_fds) {
if (!body_fds.contains(fd)) {
core.insert(name);
break;
@ -374,7 +363,7 @@ namespace smt {
};
solver * mk_smt_solver(ast_manager & m, params_ref const & p, symbol const & logic) {
return alloc(smt::solver, m, p, logic);
return alloc(smt::smt_solver, m, p, logic);
}
class smt_solver_factory : public solver_factory {

4
src/smt/theory_diff_logic_def.h
View file

@ -683,7 +683,9 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
vector<parameter> params;
if (get_manager().proofs_enabled()) {
params.push_back(parameter(symbol("farkas")));
params.resize(lits.size()+1, parameter(rational(1)));
for (unsigned i = 0; i <= lits.size(); ++i) {
params.push_back(parameter(rational(1)));
}
}
ctx.set_conflict(

156
src/smt/theory_str.cpp
View file

@ -166,14 +166,18 @@ namespace smt {
}
}
void theory_str::assert_axiom(expr * e) {
void theory_str::assert_axiom(expr * _e) {
if (opt_VerifyFinalCheckProgress) {
finalCheckProgressIndicator = true;
}
if (get_manager().is_true(e)) return;
TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;);
if (get_manager().is_true(_e)) return;
context & ctx = get_context();
ast_manager& m = get_manager();
TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;);
expr_ref e(_e, m);
//th_rewriter rw(m);
//rw(e);
if (!ctx.b_internalized(e)) {
ctx.internalize(e, false);
}
@ -1422,104 +1426,6 @@ namespace smt {
assert_axiom(finalAxiom);
}
void theory_str::instantiate_axiom_Substr(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("str", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;);
expr_ref substrBase(expr->get_arg(0), m);
expr_ref substrPos(expr->get_arg(1), m);
expr_ref substrLen(expr->get_arg(2), m);
SASSERT(substrBase);
SASSERT(substrPos);
SASSERT(substrLen);
expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m);
expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m);
SASSERT(zero);
SASSERT(minusOne);
expr_ref_vector argumentsValid_terms(m);
// pos >= 0
argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
// pos < strlen(base)
// --> pos + -1*strlen(base) < 0
argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
zero)));
// len >= 0
argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
expr_ref argumentsValid(mk_and(argumentsValid_terms), m);
SASSERT(argumentsValid);
ctx.internalize(argumentsValid, false);
// (pos+len) >= strlen(base)
// --> pos + len + -1*strlen(base) >= 0
expr_ref lenOutOfBounds(m_autil.mk_ge(
m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))),
zero), m);
SASSERT(lenOutOfBounds);
ctx.internalize(argumentsValid, false);
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
// ==> (Substr ...) = ""
expr_ref case1_premise(mk_not(m, argumentsValid), m);
SASSERT(case1_premise);
ctx.internalize(case1_premise, false);
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
SASSERT(case1_conclusion);
ctx.internalize(case1_conclusion, false);
expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m);
SASSERT(case1);
// Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base)
// ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1
expr_ref t0(mk_str_var("t0"), m);
expr_ref t1(mk_str_var("t1"), m);
expr_ref case2_conclusion(m.mk_and(
ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)),
ctx.mk_eq_atom(mk_strlen(t0), substrPos),
ctx.mk_eq_atom(expr, t1)), m);
expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m);
SASSERT(case2);
// Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
// ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
expr_ref t2(mk_str_var("t2"), m);
expr_ref t3(mk_str_var("t3"), m);
expr_ref t4(mk_str_var("t4"), m);
expr_ref_vector case3_conclusion_terms(m);
case3_conclusion_terms.push_back(ctx.mk_eq_atom(substrBase, mk_concat(t2, mk_concat(t3, t4))));
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t2), substrPos));
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
SASSERT(case3);
ctx.internalize(case1, false);
ctx.internalize(case2, false);
ctx.internalize(case3, false);
expr_ref finalAxiom(m.mk_and(case1, case2, case3), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
}
#if 0
// rewrite
// requires to add th_rewriter to assert_axiom to enforce normal form.
void theory_str::instantiate_axiom_Substr(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
@ -1551,6 +1457,7 @@ namespace smt {
argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
zero)));
// len >= 0
argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
@ -1564,7 +1471,7 @@ namespace smt {
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
// ==> (Substr ...) = ""
expr_ref case1_premise(mk_not(m, argumentsValid), m);
expr_ref case1_premise(m.mk_not(argumentsValid), m);
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m);
@ -1580,6 +1487,7 @@ namespace smt {
// Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
// ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
expr_ref t2(mk_str_var("t2"), m);
expr_ref t3(mk_str_var("t3"), m);
expr_ref t4(mk_str_var("t4"), m);
@ -1589,13 +1497,24 @@ namespace smt {
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
assert_axiom(case1);
assert_axiom(case2);
assert_axiom(case3);
{
th_rewriter rw(m);
expr_ref case1_rw(case1, m);
rw(case1_rw);
assert_axiom(case1_rw);
expr_ref case2_rw(case2, m);
rw(case2_rw);
assert_axiom(case2_rw);
expr_ref case3_rw(case3, m);
rw(case3_rw);
assert_axiom(case3_rw);
}
}
#endif
void theory_str::instantiate_axiom_Replace(enode * e) {
context & ctx = get_context();
@ -1636,13 +1555,17 @@ namespace smt {
// false branch
expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
th_rewriter rw(m);
expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
assert_axiom(breakdownAssert);
SASSERT(breakdownAssert);
expr_ref breakdownAssert_rw(breakdownAssert, m);
rw(breakdownAssert_rw);
assert_axiom(breakdownAssert_rw);
expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
assert_axiom(reduceToResult);
expr_ref reduceToResult_rw(reduceToResult, m);
rw(reduceToResult_rw);
assert_axiom(reduceToResult_rw);
}
void theory_str::instantiate_axiom_str_to_int(enode * e) {
@ -4752,12 +4675,10 @@ namespace smt {
bool theory_str::get_arith_value(expr* e, rational& val) const {
context& ctx = get_context();
ast_manager & m = get_manager();
// safety
if (!ctx.e_internalized(e)) {
// safety
if (!ctx.e_internalized(e)) {
return false;
}
}
// if an integer constant exists in the eqc, it should be the root
enode * en_e = ctx.get_enode(e);
enode * root_e = en_e->get_root();
@ -10509,6 +10430,9 @@ namespace smt {
// iterate parents
if (standAlone) {
// I hope this works!
if (!ctx.e_internalized(freeVar)) {
ctx.internalize(freeVar, false);
}
enode * e_freeVar = ctx.get_enode(freeVar);
enode_vector::iterator it = e_freeVar->begin_parents();
for (; it != e_freeVar->end_parents(); ++it) {

1
src/solver/CMakeLists.txt
View file

@ -6,6 +6,7 @@ z3_add_component(solver
smt_logics.cpp
solver.cpp
solver_na2as.cpp
solver_pool.cpp
solver2tactic.cpp
tactic2solver.cpp
COMPONENT_DEPENDENCIES

5
src/solver/combined_solver.cpp
View file

@ -147,6 +147,7 @@ public:
}
virtual void updt_params(params_ref const & p) {
solver::updt_params(p);
m_solver1->updt_params(p);
m_solver2->updt_params(p);
updt_local_params(p);
@ -280,8 +281,8 @@ public:
return m_solver2->get_assumption(idx - c1);
}
virtual std::ostream& display(std::ostream & out) const {
return m_solver1->display(out);
virtual std::ostream& display(std::ostream & out, unsigned n, expr* const* es) const {
return m_solver1->display(out, n, es);
}
virtual void collect_statistics(statistics & st) const {

3
src/solver/solver.cpp
View file

@ -34,11 +34,12 @@ expr * solver::get_assertion(unsigned idx) const {
return 0;
}
std::ostream& solver::display(std::ostream & out) const {
std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assumptions) const {
expr_ref_vector fmls(get_manager());
get_assertions(fmls);
ast_pp_util visitor(get_manager());
visitor.collect(fmls);
visitor.collect(n, assumptions);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
return out;

10
src/solver/solver.h
View file

@ -43,6 +43,7 @@ public:
- results based on check_sat_result API
*/
class solver : public check_sat_result {
params_ref m_params;
public:
virtual ~solver() {}
@ -54,7 +55,12 @@ public:
/**
\brief Update the solver internal settings.
*/
virtual void updt_params(params_ref const & p) { }
virtual void updt_params(params_ref const & p) { m_params.copy(p); }
/**
\brief Retrieve set of parameters set on solver.
*/
virtual params_ref const& get_params() { return m_params; }
/**
\brief Store in \c r a description of the configuration
@ -175,7 +181,7 @@ public:
/**
\brief Display the content of this solver.
*/
virtual std::ostream& display(std::ostream & out) const;
virtual std::ostream& display(std::ostream & out, unsigned n = 0, expr* const* assumptions = nullptr) const;
class scoped_push {
solver& s;

320
src/solver/solver_pool.cpp Normal file
View file

@ -0,0 +1,320 @@
/**
Copyright (c) 2017 Microsoft Corporation
Module Name:
solver_pool.cpp
Abstract:
Maintain a pool of solvers
Author:
Nikolaj Bjorner
Notes:
--*/
#include "solver/solver_pool.h"
#include "solver/solver_na2as.h"
#include "ast/proofs/proof_utils.h"
#include "ast/ast_util.h"
class pool_solver : public solver_na2as {
solver_pool& m_pool;
app_ref m_pred;
proof_ref m_proof;
ref<solver> m_base;
expr_ref_vector m_assertions;
unsigned m_head;
expr_ref_vector m_flat;
bool m_pushed;
bool m_in_delayed_scope;
unsigned m_dump_counter;
bool is_virtual() const { return !m.is_true(m_pred); }
public:
pool_solver(solver* b, solver_pool& pool, app_ref& pred):
solver_na2as(pred.get_manager()),
m_pool(pool),
m_pred(pred),
m_proof(m),
m_base(b),
m_assertions(m),
m_head(0),
m_flat(m),
m_pushed(false),
m_in_delayed_scope(false),
m_dump_counter(0) {
if (is_virtual()) {
solver_na2as::assert_expr(m.mk_true(), pred);
}
}
virtual ~pool_solver() {
if (m_pushed) pop(get_scope_level());
if (is_virtual()) {
m_pred = m.mk_not(m_pred);
m_base->assert_expr(m_pred);
}
}
solver* base_solver() { return m_base.get(); }
virtual solver* translate(ast_manager& m, params_ref const& p) { UNREACHABLE(); return nullptr; }
virtual void updt_params(params_ref const& p) { solver::updt_params(p); m_base->updt_params(p); }
virtual void collect_param_descrs(param_descrs & r) { m_base->collect_param_descrs(r); }
virtual void collect_statistics(statistics & st) const { m_base->collect_statistics(st); }
virtual void get_unsat_core(ptr_vector<expr> & r) {
m_base->get_unsat_core(r);
unsigned j = 0;
for (unsigned i = 0; i < r.size(); ++i)
if (m_pred != r[i])
r[j++] = r[i];
r.shrink(j);
}
virtual unsigned get_num_assumptions() const {
unsigned sz = solver_na2as::get_num_assumptions();
return is_virtual() ? sz - 1 : sz;
}
virtual proof * get_proof() {
scoped_watch _t_(m_pool.m_proof_watch);
if (!m_proof.get()) {
elim_aux_assertions pc(m_pred);
m_proof = m_base->get_proof();
pc(m, m_proof, m_proof);
}
return m_proof;
}
void internalize_assertions() {
SASSERT(!m_pushed || m_head == m_assertions.size());
for (unsigned sz = m_assertions.size(); m_head < sz; ++m_head) {
expr_ref f(m);
f = m.mk_implies(m_pred, (m_assertions.get(m_head)));
m_base->assert_expr(f);
}
}
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
SASSERT(!m_pushed || get_scope_level() > 0);
m_proof.reset();
scoped_watch _t_(m_pool.m_check_watch);
m_pool.m_stats.m_num_checks++;
stopwatch sw;
sw.start();
internalize_assertions();
lbool res = m_base->check_sat(num_assumptions, assumptions);
sw.stop();
switch (res) {
case l_true:
m_pool.m_check_sat_watch.add(sw);
m_pool.m_stats.m_num_sat_checks++;
break;
case l_undef:
m_pool.m_check_undef_watch.add(sw);
m_pool.m_stats.m_num_undef_checks++;
break;
default:
break;
}
set_status(res);
if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) {
std::stringstream file_name;
file_name << "virt_solver";
if (is_virtual()) { file_name << "_" << m_pred->get_decl()->get_name(); }
file_name << "_" << (m_dump_counter++) << ".smt2";
std::ofstream out(file_name.str().c_str());
if (!out) { verbose_stream() << "could not open file " << file_name.str() << " for output\n"; }
out << "(set-info :status ";
switch (res) {
case l_true: out << "sat"; break;
case l_false: out << "unsat"; break;
case l_undef: out << "unknown"; break;
}
out << ")\n";
m_base->display(out, num_assumptions, assumptions);
bool first = true;
out << "(check-sat";
for (unsigned i = 0; i < num_assumptions; ++i) {
out << " " << mk_pp(assumptions[i], m);
}
out << ")";
out << "(exit)\n";
::statistics st;
m_base->collect_statistics(st);
st.update("time", sw.get_seconds());
st.display_smt2(out);
out.close();
}
return res;
}
virtual void push_core() {
SASSERT(!m_pushed || get_scope_level() > 0);
if (m_in_delayed_scope) {
// second push
internalize_assertions();
m_base->push();
m_pushed = true;
m_in_delayed_scope = false;
}
if (!m_pushed) {
m_in_delayed_scope = true;
}
else {
SASSERT(m_pushed);
SASSERT(!m_in_delayed_scope);
m_base->push();
}
}
virtual void pop_core(unsigned n) {
SASSERT(!m_pushed || get_scope_level() > 0);
if (m_pushed) {
SASSERT(!m_in_delayed_scope);
m_base->pop(n);
m_pushed = get_scope_level() - n > 0;
}
else {
m_in_delayed_scope = get_scope_level() - n > 0;
}
}
virtual void assert_expr(expr * e) {
SASSERT(!m_pushed || get_scope_level() > 0);
if (m.is_true(e)) return;
if (m_in_delayed_scope) {
internalize_assertions();
m_base->push();
m_pushed = true;
m_in_delayed_scope = false;
}
if (m_pushed) {
m_base->assert_expr(e);
}
else {
m_flat.push_back(e);
flatten_and(m_flat);
m_assertions.append(m_flat);
m_flat.reset();
}
}
virtual void get_model(model_ref & _m) { m_base->get_model(_m); }
virtual expr * get_assumption(unsigned idx) const {
return solver_na2as::get_assumption(idx + is_virtual());
}
virtual std::string reason_unknown() const { return m_base->reason_unknown(); }
virtual void set_reason_unknown(char const* msg) { return m_base->set_reason_unknown(msg); }
virtual void get_labels(svector<symbol> & r) { return m_base->get_labels(r); }
virtual void set_progress_callback(progress_callback * callback) { m_base->set_progress_callback(callback); }
virtual ast_manager& get_manager() const { return m_base->get_manager(); }
void refresh(solver* new_base) {
SASSERT(!m_pushed);
m_head = 0;
m_base = new_base;
}
void reset() {
SASSERT(!m_pushed);
m_head = 0;
m_assertions.reset();
m_pool.refresh(m_base.get());
}
};
solver_pool::solver_pool(solver* base_solver, unsigned num_solvers_per_pool):
m_base_solver(base_solver),
m_num_solvers_per_pool(num_solvers_per_pool),
m_num_solvers_in_last_pool(0)
{}
ptr_vector<solver> solver_pool::get_base_solvers() const {
ptr_vector<solver> solvers;
for (solver* s0 : m_solvers) {
pool_solver* s = dynamic_cast<pool_solver*>(s0);
if (!solvers.contains(s->base_solver())) {
solvers.push_back(s->base_solver());
}
}
return solvers;
}
void solver_pool::collect_statistics(statistics &st) const {
ptr_vector<solver> solvers = get_base_solvers();
for (solver* s : solvers) s->collect_statistics(st);
st.update("time.pool_solver.smt.total", m_check_watch.get_seconds());
st.update("time.pool_solver.smt.total.sat", m_check_sat_watch.get_seconds());
st.update("time.pool_solver.smt.total.undef", m_check_undef_watch.get_seconds());
st.update("time.pool_solver.proof", m_proof_watch.get_seconds());
st.update("pool_solver.checks", m_stats.m_num_checks);
st.update("pool_solver.checks.sat", m_stats.m_num_sat_checks);
st.update("pool_solver.checks.undef", m_stats.m_num_undef_checks);
}
void solver_pool::reset_statistics() {
#if 0
ptr_vector<solver> solvers = get_base_solvers();
for (solver* s : solvers) {
s->reset_statistics();
}
#endif
m_stats.reset();
m_check_sat_watch.reset();
m_check_undef_watch.reset();
m_check_watch.reset();
m_proof_watch.reset();
}
solver* solver_pool::mk_solver() {
ref<solver> base_solver;
ast_manager& m = m_base_solver->get_manager();
if (m_solvers.empty() || m_num_solvers_in_last_pool == m_num_solvers_per_pool) {
base_solver = m_base_solver->translate(m, m_base_solver->get_params());
m_num_solvers_in_last_pool = 0;
}
else {
base_solver = dynamic_cast<pool_solver*>(m_solvers.back())->base_solver();
}
m_num_solvers_in_last_pool++;
std::stringstream name;
name << "vsolver#" << m_solvers.size();
app_ref pred(m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()), m);
pool_solver* solver = alloc(pool_solver, base_solver.get(), *this, pred);
m_solvers.push_back(solver);
return solver;
}
void solver_pool::reset_solver(solver* s) {
pool_solver* ps = dynamic_cast<pool_solver*>(s);
SASSERT(ps);
if (ps) ps->reset();
}
void solver_pool::refresh(solver* base_solver) {
ast_manager& m = m_base_solver->get_manager();
ref<solver> new_base = m_base_solver->translate(m, m_base_solver->get_params());
for (solver* s0 : m_solvers) {
pool_solver* s = dynamic_cast<pool_solver*>(s0);
if (base_solver == s->base_solver()) {
s->refresh(new_base.get());
}
}
}

69
src/solver/solver_pool.h Normal file
View file

@ -0,0 +1,69 @@
/**
Copyright (c) 2017 Microsoft Corporation
Module Name:
solver_pool.h
Abstract:
Maintain a pool of solvers
Author:
Nikolaj Bjorner
Arie Gurfinkel
Notes:
This is a revision of spacer_virtual_solver by Arie Gurfinkel
--*/
#ifndef SOLVER_POOL_H_
#define SOLVER_POOL_H_
#include "solver/solver.h"
#include "util/stopwatch.h"
class pool_solver;
class solver_pool {
friend class pool_solver;
struct stats {
unsigned m_num_checks;
unsigned m_num_sat_checks;
unsigned m_num_undef_checks;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
ref<solver> m_base_solver;
unsigned m_num_solvers_per_pool;
unsigned m_num_solvers_in_last_pool;
sref_vector<solver> m_solvers;
stats m_stats;
stopwatch m_check_watch;
stopwatch m_check_sat_watch;
stopwatch m_check_undef_watch;
stopwatch m_proof_watch;
void refresh(solver* s);
ptr_vector<solver> get_base_solvers() const;
public:
solver_pool(solver* base_solver, unsigned num_solvers_per_pool);
void collect_statistics(statistics &st) const;
void reset_statistics();
solver* mk_solver();
void reset_solver(solver* s);
};
#endif

7
src/solver/tactic2solver.cpp
View file

@ -37,7 +37,6 @@ class tactic2solver : public solver_na2as {
ref<simple_check_sat_result> m_result;
tactic_ref m_tactic;
symbol m_logic;
params_ref m_params;
bool m_produce_models;
bool m_produce_proofs;
bool m_produce_unsat_cores;
@ -85,7 +84,7 @@ tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p,
m_tactic = t;
m_logic = logic;
m_params = p;
solver::updt_params(p);
m_produce_models = produce_models;
m_produce_proofs = produce_proofs;
@ -96,7 +95,7 @@ tactic2solver::~tactic2solver() {
}
void tactic2solver::updt_params(params_ref const & p) {
m_params.append(p);
solver::updt_params(p);
}
void tactic2solver::collect_param_descrs(param_descrs & r) {
@ -129,7 +128,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
m_result = alloc(simple_check_sat_result, m);
m_tactic->cleanup();
m_tactic->set_logic(m_logic);
m_tactic->updt_params(m_params); // parameters are allowed to overwrite logic.
m_tactic->updt_params(get_params()); // parameters are allowed to overwrite logic.
goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
unsigned sz = m_assertions.size();

6
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -399,8 +399,8 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g,
void bv_size_reduction_tactic::cleanup() {
imp * d = alloc(imp, m_imp->m);
std::swap(d, m_imp);
dealloc(d);
ast_manager & m = m_imp->m;
m_imp->~imp();
new (m_imp) imp(m);
}

7
src/tactic/bv/max_bv_sharing_tactic.cpp
View file

@ -307,9 +307,10 @@ public:
}
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m(), m_params);
std::swap(d, m_imp);
dealloc(d);
ast_manager & m = m_imp->m();
params_ref p = std::move(m_params);
m_imp->~imp();
new (m_imp) imp(m, p);
}
};

5
src/tactic/core/propagate_values_tactic.cpp
View file

@ -255,8 +255,9 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
params_ref p = std::move(m_params);
m_imp->~imp();
new (m_imp) imp(m, p);
}
};

6
src/tactic/core/simplify_tactic.cpp
View file

@ -111,9 +111,9 @@ void simplify_tactic::operator()(goal_ref const & in,
void simplify_tactic::cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
std::swap(d, m_imp);
dealloc(d);
params_ref p = std::move(m_params);
m_imp->~imp();
new (m_imp) imp(m, p);
}
unsigned simplify_tactic::get_num_steps() const {

5
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -33,7 +33,6 @@ Notes:
class bounded_int2bv_solver : public solver_na2as {
ast_manager& m;
params_ref m_params;
mutable bv_util m_bv;
mutable arith_util m_arith;
mutable expr_ref_vector m_assertions;
@ -53,7 +52,6 @@ public:
bounded_int2bv_solver(ast_manager& m, params_ref const& p, solver* s):
solver_na2as(m),
m(m),
m_params(p),
m_bv(m),
m_arith(m),
m_assertions(m),
@ -63,6 +61,7 @@ public:
m_rewriter_ctx(m, p),
m_rewriter(m, m_rewriter_ctx)
{
solver::updt_params(p);
m_bounds.push_back(alloc(bound_manager, m));
}
@ -131,7 +130,7 @@ public:
return m_solver->check_sat(num_assumptions, assumptions);
}
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); }
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }

5
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -33,7 +33,6 @@ Notes:
class enum2bv_solver : public solver_na2as {
ast_manager& m;
params_ref m_params;
ref<solver> m_solver;
enum2bv_rewriter m_rewriter;
@ -42,10 +41,10 @@ public:
enum2bv_solver(ast_manager& m, params_ref const& p, solver* s):
solver_na2as(m),
m(m),
m_params(p),
m_solver(s),
m_rewriter(m, p)
{
solver::updt_params(p);
}
virtual ~enum2bv_solver() {}
@ -78,7 +77,7 @@ public:
return m_solver->check_sat(num_assumptions, assumptions);
}
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); }
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }

5
src/tactic/portfolio/pb2bv_solver.cpp
View file

@ -26,7 +26,6 @@ Notes:
class pb2bv_solver : public solver_na2as {
ast_manager& m;
params_ref m_params;
mutable expr_ref_vector m_assertions;
mutable ref<solver> m_solver;
mutable pb2bv_rewriter m_rewriter;
@ -36,11 +35,11 @@ public:
pb2bv_solver(ast_manager& m, params_ref const& p, solver* s):
solver_na2as(m),
m(m),
m_params(p),
m_assertions(m),
m_solver(s),
m_rewriter(m, p)
{
solver::updt_params(p);
}
virtual ~pb2bv_solver() {}
@ -70,7 +69,7 @@ public:
return m_solver->check_sat(num_assumptions, assumptions);
}
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); }
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }

8
src/tactic/smtlogics/qfufbv_tactic.cpp
View file

@ -70,8 +70,8 @@ public:
const unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
scoped_ptr<solver> uffree_solver = setup_sat();
scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, uffree_solver.get());
const lbool o = imp->operator()();
lackr imp(m, m_p, m_st, flas, uffree_solver.get());
const lbool o = imp.operator()();
flas.reset();
// report result
goal_ref resg(alloc(goal, *g, true));
@ -79,8 +79,8 @@ public:
if (o != l_undef) result.push_back(resg.get());
// report model
if (g->models_enabled() && (o == l_true)) {
model_ref abstr_model = imp->get_model();
mc = mk_qfufbv_ackr_model_converter(m, imp->get_info(), abstr_model);
model_ref abstr_model = imp.get_model();
mc = mk_qfufbv_ackr_model_converter(m, imp.get_info(), abstr_model);
}
}

11
src/util/stopwatch.h
View file

@ -185,4 +185,15 @@ public:
#endif
struct scoped_watch {
stopwatch &m_sw;
scoped_watch (stopwatch &sw, bool reset=false): m_sw(sw) {
if (reset) m_sw.reset();
m_sw.start();
}
~scoped_watch() {
m_sw.stop ();
}
};
#endif