mirror of
https://github.com/Z3Prover/z3
synced 2025-05-08 16:25:48 +00:00
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
commit
13099b1590
87 changed files with 2187 additions and 4479 deletions
|
|
@ -184,13 +184,13 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) {
|
|||
}
|
||||
|
||||
void asserted_formulas::push_scope() {
|
||||
SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size());
|
||||
SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m_manager.canceled());
|
||||
TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout););
|
||||
m_scopes.push_back(scope());
|
||||
m_macro_manager.push_scope();
|
||||
scope & s = m_scopes.back();
|
||||
s.m_asserted_formulas_lim = m_asserted_formulas.size();
|
||||
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead);
|
||||
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m_manager.canceled());
|
||||
s.m_inconsistent_old = m_inconsistent;
|
||||
m_defined_names.push();
|
||||
m_bv_sharing.push_scope();
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
def_module_params(module_name='smt',
|
||||
def_module_params(module_name='smt',
|
||||
class_name='smt_params_helper',
|
||||
description='smt solver based on lazy smt',
|
||||
export=True,
|
||||
|
|
@ -17,7 +17,7 @@ def_module_params(module_name='smt',
|
|||
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
|
||||
('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
|
||||
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
|
||||
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
|
||||
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
|
||||
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
|
||||
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
|
||||
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
|
||||
|
|
@ -62,5 +62,6 @@ def_module_params(module_name='smt',
|
|||
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
|
||||
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
|
||||
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
|
||||
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context')
|
||||
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
|
||||
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances')
|
||||
))
|
||||
|
|
|
|||
47
src/smt/smt2_extra_cmds.cpp
Normal file
47
src/smt/smt2_extra_cmds.cpp
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
smt2_extra_cmds.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Additional SMT-specific commands.
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2017-01-16
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"cmd_context.h"
|
||||
#include"smt2parser.h"
|
||||
#include"smt2_extra_cmds.h"
|
||||
|
||||
class include_cmd : public cmd {
|
||||
char const * m_filename;
|
||||
public:
|
||||
include_cmd() : cmd("include"), m_filename(0) {}
|
||||
virtual char const * get_usage() const { return "<string>"; }
|
||||
virtual char const * get_descr(cmd_context & ctx) const { return "include a file"; }
|
||||
virtual unsigned get_arity() const { return 1; }
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_STRING; }
|
||||
virtual void set_next_arg(cmd_context & ctx, char const * val) { m_filename = val; }
|
||||
virtual void failure_cleanup(cmd_context & ctx) {}
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
std::ifstream is(m_filename);
|
||||
if (is.bad() || is.fail())
|
||||
throw cmd_exception(std::string("failed to open file '") + m_filename + "'");
|
||||
parse_smt2_commands(ctx, is, false, params_ref(), m_filename);
|
||||
is.close();
|
||||
}
|
||||
virtual void prepare(cmd_context & ctx) { reset(ctx); }
|
||||
virtual void reset(cmd_context & ctx) { m_filename = 0; }
|
||||
virtual void finalize(cmd_context & ctx) { reset(ctx); }
|
||||
};
|
||||
|
||||
void install_smt2_extra_cmds(cmd_context & ctx) {
|
||||
ctx.insert(alloc(include_cmd));
|
||||
}
|
||||
26
src/smt/smt2_extra_cmds.h
Normal file
26
src/smt/smt2_extra_cmds.h
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
smt2_extra_cmds.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Additional SMT-specific commands.
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2017-01-16
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef SMT2_EXTRA_CMDS_H_
|
||||
#define SMT2_EXTRA_CMDS_H_
|
||||
|
||||
class cmd_context;
|
||||
|
||||
void install_smt2_extra_cmds(cmd_context & ctx);
|
||||
|
||||
#endif /* SMT2_EXTRA_CMDS_H_ */
|
||||
|
|
@ -24,7 +24,9 @@ Revision History:
|
|||
namespace smt {
|
||||
|
||||
struct bool_var_data {
|
||||
private:
|
||||
b_justification m_justification;
|
||||
public:
|
||||
unsigned m_scope_lvl:24; //!< scope level of when the variable was assigned.
|
||||
unsigned m_mark:1;
|
||||
unsigned m_assumption:1;
|
||||
|
|
@ -45,6 +47,14 @@ namespace smt {
|
|||
public:
|
||||
|
||||
unsigned get_intern_level() const { return m_iscope_lvl; }
|
||||
|
||||
b_justification justification() const { return m_justification; }
|
||||
|
||||
void set_axiom() { m_justification = b_justification::mk_axiom(); }
|
||||
|
||||
void set_null_justification() { m_justification = null_b_justification; }
|
||||
|
||||
void set_justification(b_justification const& j) { m_justification = j; }
|
||||
|
||||
bool is_atom() const { return m_atom; }
|
||||
|
||||
|
|
|
|||
|
|
@ -496,13 +496,15 @@ namespace smt {
|
|||
|
||||
unsigned idx = skip_literals_above_conflict_level();
|
||||
|
||||
TRACE("conflict", m_ctx.display_literal_verbose(tout, not_l); m_ctx.display(tout << " ", conflict););
|
||||
|
||||
// save space for first uip
|
||||
m_lemma.push_back(null_literal);
|
||||
m_lemma_atoms.push_back(0);
|
||||
|
||||
unsigned num_marks = 0;
|
||||
if (not_l != null_literal) {
|
||||
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal(tout, not_l); tout << "\n";);
|
||||
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal_verbose(tout, not_l); tout << "\n";);
|
||||
process_antecedent(not_l, num_marks);
|
||||
}
|
||||
|
||||
|
|
@ -514,7 +516,7 @@ namespace smt {
|
|||
get_manager().trace_stream() << "\n";
|
||||
}
|
||||
|
||||
TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal(tout, consequent); tout << "\n";
|
||||
TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
|
||||
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
|
||||
SASSERT(js != null_b_justification);
|
||||
switch (js.get_kind()) {
|
||||
|
|
@ -1076,6 +1078,7 @@ namespace smt {
|
|||
return true;
|
||||
SASSERT(js.get_kind() != b_justification::BIN_CLAUSE);
|
||||
CTRACE("visit_b_justification_bug", js.get_kind() == b_justification::AXIOM, tout << "l: " << l << "\n"; m_ctx.display(tout););
|
||||
|
||||
if (js.get_kind() == b_justification::AXIOM)
|
||||
return true;
|
||||
SASSERT(js.get_kind() != b_justification::AXIOM);
|
||||
|
|
@ -1089,14 +1092,17 @@ namespace smt {
|
|||
i = 1;
|
||||
}
|
||||
else {
|
||||
SASSERT(cls->get_literal(1) == l);
|
||||
if (get_proof(~cls->get_literal(0)) == 0)
|
||||
visited = false;
|
||||
i = 2;
|
||||
}
|
||||
}
|
||||
for (; i < num_lits; i++)
|
||||
for (; i < num_lits; i++) {
|
||||
SASSERT(cls->get_literal(i) != l);
|
||||
if (get_proof(~cls->get_literal(i)) == 0)
|
||||
visited = false;
|
||||
}
|
||||
return visited;
|
||||
}
|
||||
else
|
||||
|
|
@ -1251,14 +1257,19 @@ namespace smt {
|
|||
}
|
||||
tout << "\n";);
|
||||
init_mk_proof();
|
||||
literal consequent = false_literal;
|
||||
if (not_l != null_literal)
|
||||
consequent = ~not_l;
|
||||
visit_b_justification(consequent, conflict);
|
||||
if (not_l != null_literal)
|
||||
literal consequent;
|
||||
if (not_l == null_literal) {
|
||||
consequent = false_literal;
|
||||
}
|
||||
else {
|
||||
consequent = ~not_l;
|
||||
m_todo_pr.push_back(tp_elem(not_l));
|
||||
}
|
||||
visit_b_justification(consequent, conflict);
|
||||
|
||||
while (!m_todo_pr.empty()) {
|
||||
tp_elem & elem = m_todo_pr.back();
|
||||
|
||||
switch (elem.m_kind) {
|
||||
case tp_elem::EQUALITY: {
|
||||
enode * lhs = elem.m_lhs;
|
||||
|
|
|
|||
|
|
@ -261,10 +261,11 @@ namespace smt {
|
|||
m_assignment[false_literal.index()] = l_false;
|
||||
if (m_manager.proofs_enabled()) {
|
||||
proof * pr = m_manager.mk_true_proof();
|
||||
m_bdata[true_bool_var].m_justification = b_justification(mk_justification(justification_proof_wrapper(*this, pr)));
|
||||
|
||||
set_justification(true_bool_var, m_bdata[true_bool_var], b_justification(mk_justification(justification_proof_wrapper(*this, pr))));
|
||||
}
|
||||
else {
|
||||
m_bdata[true_bool_var].m_justification = b_justification::mk_axiom();
|
||||
m_bdata[true_bool_var].set_axiom();
|
||||
}
|
||||
m_true_enode = mk_enode(t, true, true, false);
|
||||
// internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
|
||||
|
|
@ -292,6 +293,12 @@ namespace smt {
|
|||
std::swap(lhs, rhs);
|
||||
return m_manager.mk_eq(lhs, rhs);
|
||||
}
|
||||
|
||||
void context::set_justification(bool_var v, bool_var_data& d, b_justification const& j) {
|
||||
SASSERT(validate_justification(v, d, j));
|
||||
d.set_justification(j);
|
||||
}
|
||||
|
||||
|
||||
void context::assign_core(literal l, b_justification j, bool decision) {
|
||||
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
|
||||
|
|
@ -302,7 +309,7 @@ namespace smt {
|
|||
m_assignment[l.index()] = l_true;
|
||||
m_assignment[(~l).index()] = l_false;
|
||||
bool_var_data & d = get_bdata(l.var());
|
||||
d.m_justification = j;
|
||||
set_justification(l.var(), d, j);
|
||||
d.m_scope_lvl = m_scope_lvl;
|
||||
if (m_fparams.m_restart_adaptive && d.m_phase_available) {
|
||||
m_agility *= m_fparams.m_agility_factor;
|
||||
|
|
@ -1406,7 +1413,8 @@ namespace smt {
|
|||
else {
|
||||
TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v)););
|
||||
if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) {
|
||||
set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), ~l);
|
||||
literal n_eq = literal(l.var(), true);
|
||||
set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), n_eq);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1787,6 +1795,7 @@ namespace smt {
|
|||
|
||||
void context::set_conflict(b_justification js, literal not_l) {
|
||||
if (!inconsistent()) {
|
||||
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
|
||||
m_conflict = js;
|
||||
m_not_l = not_l;
|
||||
}
|
||||
|
|
@ -2042,7 +2051,7 @@ namespace smt {
|
|||
m_assignment[(~l).index()] = l_undef;
|
||||
bool_var v = l.var();
|
||||
bool_var_data & d = get_bdata(v);
|
||||
d.m_justification = null_b_justification;
|
||||
d.set_null_justification();
|
||||
m_case_split_queue->unassign_var_eh(v);
|
||||
}
|
||||
|
||||
|
|
@ -2593,10 +2602,10 @@ namespace smt {
|
|||
cls->set_justification(0);
|
||||
m_justifications.push_back(js);
|
||||
}
|
||||
m_bdata[v0].m_justification = b_justification(js);
|
||||
set_justification(v0, m_bdata[v0], b_justification(js));
|
||||
}
|
||||
else
|
||||
m_bdata[v0].m_justification = b_justification::mk_axiom();
|
||||
m_bdata[v0].set_axiom();
|
||||
}
|
||||
}
|
||||
del_clause(cls);
|
||||
|
|
|
|||
|
|
@ -50,9 +50,9 @@ Revision History:
|
|||
#include"statistics.h"
|
||||
#include"progress_callback.h"
|
||||
|
||||
// there is a significant space overhead with allocating 1000+ contexts in
|
||||
// there is a significant space overhead with allocating 1000+ contexts in
|
||||
// the case that each context only references a few expressions.
|
||||
// Using a map instead of a vector for the literals can compress space
|
||||
// Using a map instead of a vector for the literals can compress space
|
||||
// consumption.
|
||||
#ifdef SPARSE_MAP
|
||||
#define USE_BOOL_VAR_VECTOR 0
|
||||
|
|
@ -98,7 +98,7 @@ namespace smt {
|
|||
// Remark: boolean expressions can also be internalized as
|
||||
// enodes. Examples: boolean expression nested in an
|
||||
// uninterpreted function.
|
||||
expr_ref_vector m_e_internalized_stack; // stack of the expressions already internalized as enodes.
|
||||
expr_ref_vector m_e_internalized_stack; // stack of the expressions already internalized as enodes.
|
||||
|
||||
ptr_vector<justification> m_justifications;
|
||||
|
||||
|
|
@ -116,7 +116,7 @@ namespace smt {
|
|||
plugin_manager<theory> m_theories; // mapping from theory_id -> theory
|
||||
ptr_vector<theory> m_theory_set; // set of theories for fast traversal
|
||||
vector<enode_vector> m_decl2enodes; // decl -> enode (for decls with arity > 0)
|
||||
cg_table m_cg_table;
|
||||
cg_table m_cg_table;
|
||||
dyn_ack_manager m_dyn_ack_manager;
|
||||
struct new_eq {
|
||||
enode * m_lhs;
|
||||
|
|
@ -140,7 +140,7 @@ namespace smt {
|
|||
svector<new_th_eq> m_propagated_th_eqs;
|
||||
svector<new_th_eq> m_propagated_th_diseqs;
|
||||
svector<enode_pair> m_diseq_vector;
|
||||
#endif
|
||||
#endif
|
||||
enode * m_is_diseq_tmp; // auxiliary enode used to find congruent equality atoms.
|
||||
|
||||
tmp_enode m_tmp_enode;
|
||||
|
|
@ -161,8 +161,8 @@ namespace smt {
|
|||
vector<watch_list> m_watches; //!< per literal
|
||||
vector<clause_set> m_lit_occs; //!< index for backward subsumption
|
||||
svector<bool_var_data> m_bdata; //!< mapping bool_var -> data
|
||||
svector<double> m_activity;
|
||||
clause_vector m_aux_clauses;
|
||||
svector<double> m_activity;
|
||||
clause_vector m_aux_clauses;
|
||||
clause_vector m_lemmas;
|
||||
vector<clause_vector> m_clauses_to_reinit;
|
||||
expr_ref_vector m_units_to_reassert;
|
||||
|
|
@ -176,7 +176,7 @@ namespace smt {
|
|||
bool m_phase_cache_on;
|
||||
unsigned m_phase_counter; //!< auxiliary variable used to decide when to turn on/off phase caching
|
||||
bool m_phase_default; //!< default phase when using phase caching
|
||||
|
||||
|
||||
// A conflict is usually a single justification. That is, a justification
|
||||
// for false. If m_not_l is not null_literal, then m_conflict is a
|
||||
// justification for l, and the conflict is union of m_no_l and m_conflict;
|
||||
|
|
@ -220,10 +220,10 @@ namespace smt {
|
|||
// Unsat core extraction
|
||||
//
|
||||
// -----------------------------------
|
||||
typedef u_map<expr *> literal2assumption;
|
||||
typedef u_map<expr *> literal2assumption;
|
||||
literal_vector m_assumptions;
|
||||
literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption
|
||||
expr_ref_vector m_unsat_core;
|
||||
expr_ref_vector m_unsat_core;
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
|
|
@ -261,7 +261,7 @@ namespace smt {
|
|||
SASSERT(e_internalized(n));
|
||||
return m_app2enode[n->get_id()];
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Similar to get_enode, but returns 0 if n is to e_internalized.
|
||||
*/
|
||||
|
|
@ -323,7 +323,7 @@ namespace smt {
|
|||
literal enode2literal(enode const * n) const {
|
||||
SASSERT(n->is_bool());
|
||||
return n == m_false_enode ? false_literal : literal(enode2bool_var(n));
|
||||
}
|
||||
}
|
||||
|
||||
unsigned get_num_bool_vars() const {
|
||||
return m_b_internalized_stack.size();
|
||||
|
|
@ -336,7 +336,7 @@ namespace smt {
|
|||
bool_var_data const & get_bdata(bool_var v) const {
|
||||
return m_bdata[v];
|
||||
}
|
||||
|
||||
|
||||
lbool get_lit_assignment(unsigned lit_idx) const {
|
||||
return static_cast<lbool>(m_assignment[lit_idx]);
|
||||
}
|
||||
|
|
@ -349,8 +349,8 @@ namespace smt {
|
|||
return get_assignment(literal(v));
|
||||
}
|
||||
|
||||
literal_vector const & assigned_literals() const {
|
||||
return m_assigned_literals;
|
||||
literal_vector const & assigned_literals() const {
|
||||
return m_assigned_literals;
|
||||
}
|
||||
|
||||
lbool get_assignment(expr * n) const;
|
||||
|
|
@ -363,9 +363,11 @@ namespace smt {
|
|||
void get_assignments(expr_ref_vector& assignments);
|
||||
|
||||
b_justification get_justification(bool_var v) const {
|
||||
return get_bdata(v).m_justification;
|
||||
return get_bdata(v).justification();
|
||||
}
|
||||
|
||||
void set_justification(bool_var v, bool_var_data& d, b_justification const& j);
|
||||
|
||||
bool has_th_justification(bool_var v, theory_id th_id) const {
|
||||
b_justification js = get_justification(v);
|
||||
return js.get_kind() == b_justification::JUSTIFICATION && js.get_justification()->get_from_theory() == th_id;
|
||||
|
|
@ -423,7 +425,7 @@ namespace smt {
|
|||
unsigned get_assign_level(literal l) const {
|
||||
return get_assign_level(l.var());
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Return the scope level when v was internalized.
|
||||
*/
|
||||
|
|
@ -434,7 +436,7 @@ namespace smt {
|
|||
theory * get_theory(theory_id th_id) const {
|
||||
return m_theories.get_plugin(th_id);
|
||||
}
|
||||
|
||||
|
||||
ptr_vector<theory>::const_iterator begin_theories() const {
|
||||
return m_theories.begin();
|
||||
}
|
||||
|
|
@ -448,7 +450,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
unsigned get_base_level() const {
|
||||
return m_base_lvl;
|
||||
return m_base_lvl;
|
||||
}
|
||||
|
||||
bool at_base_level() const {
|
||||
|
|
@ -468,11 +470,11 @@ namespace smt {
|
|||
}
|
||||
|
||||
expr * bool_var2expr(bool_var v) const {
|
||||
return m_bool_var2expr[v];
|
||||
return m_bool_var2expr[v];
|
||||
}
|
||||
|
||||
|
||||
void literal2expr(literal l, expr_ref & result) const {
|
||||
if (l == true_literal)
|
||||
if (l == true_literal)
|
||||
result = m_manager.mk_true();
|
||||
else if (l == false_literal)
|
||||
result = m_manager.mk_false();
|
||||
|
|
@ -499,7 +501,7 @@ namespace smt {
|
|||
unsigned id = decl->get_decl_id();
|
||||
return id < m_decl2enodes.size() ? m_decl2enodes[id].begin() : 0;
|
||||
}
|
||||
|
||||
|
||||
enode_vector::const_iterator end_enodes_of(func_decl const * decl) const {
|
||||
unsigned id = decl->get_decl_id();
|
||||
return id < m_decl2enodes.size() ? m_decl2enodes[id].end() : 0;
|
||||
|
|
@ -589,7 +591,7 @@ namespace smt {
|
|||
void push_scope();
|
||||
|
||||
unsigned pop_scope_core(unsigned num_scopes);
|
||||
|
||||
|
||||
void pop_scope(unsigned num_scopes);
|
||||
|
||||
void undo_trail_stack(unsigned old_size);
|
||||
|
|
@ -615,13 +617,13 @@ namespace smt {
|
|||
bool is_empty_clause(clause const * c) const;
|
||||
|
||||
void cache_generation(unsigned new_scope_lvl);
|
||||
|
||||
|
||||
void cache_generation(clause const * cls, unsigned new_scope_lvl);
|
||||
|
||||
void cache_generation(unsigned num_lits, literal const * lits, unsigned new_scope_lvl);
|
||||
|
||||
void cache_generation(expr * n, unsigned new_scope_lvl);
|
||||
|
||||
|
||||
void reset_cache_generation();
|
||||
|
||||
void reinit_clauses(unsigned num_scopes, unsigned num_bool_vars);
|
||||
|
|
@ -630,14 +632,14 @@ namespace smt {
|
|||
|
||||
// -----------------------------------
|
||||
//
|
||||
// Internalization
|
||||
// Internalization
|
||||
//
|
||||
// -----------------------------------
|
||||
public:
|
||||
bool b_internalized(expr const * n) const {
|
||||
return get_bool_var_of_id_option(n->get_id()) != null_bool_var;
|
||||
}
|
||||
|
||||
|
||||
bool lit_internalized(expr const * n) const {
|
||||
return m_manager.is_false(n) || (m_manager.is_not(n) ? b_internalized(to_app(n)->get_arg(0)) : b_internalized(n));
|
||||
}
|
||||
|
|
@ -646,7 +648,7 @@ namespace smt {
|
|||
return m_app2enode.get(n->get_id(), 0) != 0;
|
||||
}
|
||||
|
||||
unsigned get_num_b_internalized() const {
|
||||
unsigned get_num_b_internalized() const {
|
||||
return m_b_internalized_stack.size();
|
||||
}
|
||||
|
||||
|
|
@ -654,7 +656,7 @@ namespace smt {
|
|||
return m_b_internalized_stack.get(idx);
|
||||
}
|
||||
|
||||
unsigned get_num_e_internalized() const {
|
||||
unsigned get_num_e_internalized() const {
|
||||
return m_e_internalized_stack.size();
|
||||
}
|
||||
|
||||
|
|
@ -691,9 +693,9 @@ namespace smt {
|
|||
void ts_visit_child(expr * n, bool gate_ctx, svector<int> & tcolors, svector<int> & fcolors, svector<expr_bool_pair> & todo, bool & visited);
|
||||
|
||||
bool ts_visit_children(expr * n, bool gate_ctx, svector<int> & tcolors, svector<int> & fcolors, svector<expr_bool_pair> & todo);
|
||||
|
||||
|
||||
void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs);
|
||||
|
||||
|
||||
void assert_default(expr * n, proof * pr);
|
||||
|
||||
void assert_distinct(app * n, proof * pr);
|
||||
|
|
@ -721,7 +723,7 @@ namespace smt {
|
|||
void internalize_term(app * n);
|
||||
|
||||
void internalize_ite_term(app * n);
|
||||
|
||||
|
||||
bool internalize_theory_term(app * n);
|
||||
|
||||
void internalize_uninterpreted(app * n);
|
||||
|
|
@ -752,7 +754,7 @@ namespace smt {
|
|||
bool simplify_aux_lemma_literals(unsigned & num_lits, literal * lits);
|
||||
|
||||
void mark_for_reinit(clause * cls, unsigned scope_lvl, bool reinternalize_atoms);
|
||||
|
||||
|
||||
unsigned get_max_iscope_lvl(unsigned num_lits, literal const * lits) const;
|
||||
|
||||
bool use_binary_clause_opt(literal l1, literal l2, bool lemma) const;
|
||||
|
|
@ -784,7 +786,7 @@ namespace smt {
|
|||
void add_and_rel_watches(app * n);
|
||||
|
||||
void add_or_rel_watches(app * n);
|
||||
|
||||
|
||||
void add_ite_rel_watches(app * n);
|
||||
|
||||
void mk_not_cnstr(app * n);
|
||||
|
|
@ -796,7 +798,7 @@ namespace smt {
|
|||
void mk_iff_cnstr(app * n);
|
||||
|
||||
void mk_ite_cnstr(app * n);
|
||||
|
||||
|
||||
bool lit_occs_enabled() const { return m_fparams.m_phase_selection==PS_OCCURRENCE; }
|
||||
|
||||
void add_lit_occs(clause * cls);
|
||||
|
|
@ -819,7 +821,7 @@ namespace smt {
|
|||
|
||||
|
||||
bool_var mk_bool_var(expr * n);
|
||||
|
||||
|
||||
enode * mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled);
|
||||
|
||||
void attach_th_var(enode * n, theory * th, theory_var v);
|
||||
|
|
@ -828,7 +830,7 @@ namespace smt {
|
|||
justification * mk_justification(Justification const & j) {
|
||||
justification * js = new (m_region) Justification(j);
|
||||
SASSERT(js->in_region());
|
||||
if (js->has_del_eh())
|
||||
if (js->has_del_eh())
|
||||
m_justifications.push_back(js);
|
||||
return js;
|
||||
}
|
||||
|
|
@ -849,10 +851,10 @@ namespace smt {
|
|||
unsigned m_num_conflicts_since_lemma_gc;
|
||||
unsigned m_restart_threshold;
|
||||
unsigned m_restart_outer_threshold;
|
||||
unsigned m_luby_idx;
|
||||
unsigned m_luby_idx;
|
||||
double m_agility;
|
||||
unsigned m_lemma_gc_threshold;
|
||||
|
||||
|
||||
void assign_core(literal l, b_justification j, bool decision = false);
|
||||
void trace_assign(literal l, b_justification j, bool decision) const;
|
||||
|
||||
|
|
@ -878,7 +880,7 @@ namespace smt {
|
|||
|
||||
friend class set_true_first_trail;
|
||||
void set_true_first_flag(bool_var v);
|
||||
|
||||
|
||||
bool try_true_first(bool_var v) const { return get_bdata(v).try_true_first(); }
|
||||
|
||||
bool assume_eq(enode * lhs, enode * rhs);
|
||||
|
|
@ -899,13 +901,13 @@ namespace smt {
|
|||
d.m_phase = phase;
|
||||
}
|
||||
|
||||
void force_phase(literal l) {
|
||||
void force_phase(literal l) {
|
||||
force_phase(l.var(), !l.sign());
|
||||
}
|
||||
|
||||
bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
|
||||
|
||||
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
|
||||
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
|
||||
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes);
|
||||
|
||||
void set_global_generation(unsigned generation) { m_generation = generation; }
|
||||
|
|
@ -958,7 +960,7 @@ namespace smt {
|
|||
|
||||
void assign_quantifier(quantifier * q);
|
||||
|
||||
void set_conflict(b_justification js, literal not_l);
|
||||
void set_conflict(b_justification js, literal not_l);
|
||||
|
||||
void set_conflict(b_justification js) {
|
||||
set_conflict(js, null_literal);
|
||||
|
|
@ -997,12 +999,12 @@ namespace smt {
|
|||
#define INV_ACTIVITY_LIMIT 1e-100
|
||||
|
||||
void rescale_bool_var_activity();
|
||||
|
||||
|
||||
public:
|
||||
void inc_bvar_activity(bool_var v) {
|
||||
double & act = m_activity[v];
|
||||
act += m_bvar_inc;
|
||||
if (act > ACTIVITY_LIMIT)
|
||||
if (act > ACTIVITY_LIMIT)
|
||||
rescale_bool_var_activity();
|
||||
m_case_split_queue->activity_increased_eh(v);
|
||||
}
|
||||
|
|
@ -1031,7 +1033,7 @@ namespace smt {
|
|||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
bool can_delete(clause * cls) const {
|
||||
if (cls->in_reinit_stack())
|
||||
return false;
|
||||
|
|
@ -1053,7 +1055,7 @@ namespace smt {
|
|||
bool validate_assumptions(unsigned num_assumptions, expr * const * assumptions);
|
||||
|
||||
void init_assumptions(unsigned num_assumptions, expr * const * assumptions);
|
||||
|
||||
|
||||
void reset_assumptions();
|
||||
|
||||
void mk_unsat_core();
|
||||
|
|
@ -1073,9 +1075,9 @@ namespace smt {
|
|||
void tick(unsigned & counter) const;
|
||||
|
||||
lbool bounded_search();
|
||||
|
||||
|
||||
final_check_status final_check();
|
||||
|
||||
|
||||
void check_proof(proof * pr);
|
||||
|
||||
void forget_phase_of_vars_in_current_level();
|
||||
|
|
@ -1102,7 +1104,7 @@ namespace smt {
|
|||
|
||||
public:
|
||||
// event handler for relevancy_propagator class
|
||||
void relevant_eh(expr * n);
|
||||
void relevant_eh(expr * n);
|
||||
|
||||
bool is_relevant(expr * n) const {
|
||||
return !relevancy() || is_relevant_core(n);
|
||||
|
|
@ -1126,9 +1128,9 @@ namespace smt {
|
|||
void mark_as_relevant(enode * n) { mark_as_relevant(n->get_owner()); }
|
||||
|
||||
void mark_as_relevant(bool_var v) { mark_as_relevant(bool_var2expr(v)); }
|
||||
|
||||
|
||||
void mark_as_relevant(literal l) { mark_as_relevant(l.var()); }
|
||||
|
||||
|
||||
template<typename Eh>
|
||||
relevancy_eh * mk_relevancy_eh(Eh const & eh) {
|
||||
return m_relevancy_propagator->mk_relevancy_eh(eh);
|
||||
|
|
@ -1149,9 +1151,9 @@ namespace smt {
|
|||
void propagate_th_eqs();
|
||||
|
||||
void propagate_th_diseqs();
|
||||
|
||||
|
||||
bool can_theories_propagate() const;
|
||||
|
||||
|
||||
bool propagate();
|
||||
|
||||
public:
|
||||
|
|
@ -1167,7 +1169,7 @@ namespace smt {
|
|||
|
||||
// -----------------------------------
|
||||
//
|
||||
// Pretty Printing
|
||||
// Pretty Printing
|
||||
//
|
||||
// -----------------------------------
|
||||
protected:
|
||||
|
|
@ -1215,7 +1217,7 @@ namespace smt {
|
|||
void display_binary_clauses(std::ostream & out) const;
|
||||
|
||||
void display_assignment(std::ostream & out) const;
|
||||
|
||||
|
||||
void display_eqc(std::ostream & out) const;
|
||||
|
||||
void display_app_enode_map(std::ostream & out) const;
|
||||
|
|
@ -1235,15 +1237,15 @@ namespace smt {
|
|||
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
|
||||
|
||||
void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
|
||||
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
|
||||
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
|
||||
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
|
||||
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
|
||||
literal consequent = false_literal, symbol const& logic = symbol::null) const;
|
||||
|
||||
void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
|
||||
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
|
||||
void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
|
||||
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
|
||||
literal consequent = false_literal, symbol const& logic = symbol::null) const;
|
||||
|
||||
void display_assignment_as_smtlib2(std::ostream& out, symbol const& logic = symbol::null) const;
|
||||
void display_assignment_as_smtlib2(std::ostream& out, symbol const& logic = symbol::null) const;
|
||||
|
||||
void display_normalized_enodes(std::ostream & out) const;
|
||||
|
||||
|
|
@ -1289,13 +1291,13 @@ namespace smt {
|
|||
bool check_invariant() const;
|
||||
|
||||
bool check_eqc_bool_assignment() const;
|
||||
|
||||
|
||||
bool check_missing_clause_propagation(clause_vector const & v) const;
|
||||
|
||||
bool check_missing_bin_clause_propagation() const;
|
||||
|
||||
bool check_missing_eq_propagation() const;
|
||||
|
||||
|
||||
bool check_missing_congruence() const;
|
||||
|
||||
bool check_missing_bool_enode_propagation() const;
|
||||
|
|
@ -1357,7 +1359,7 @@ namespace smt {
|
|||
static literal translate_literal(
|
||||
literal lit, context& src_ctx, context& dst_ctx,
|
||||
vector<bool_var> b2v, ast_translation& tr);
|
||||
|
||||
|
||||
/*
|
||||
\brief Utilities for consequence finding.
|
||||
*/
|
||||
|
|
@ -1366,7 +1368,7 @@ namespace smt {
|
|||
u_map<index_set> m_antecedents;
|
||||
void extract_fixed_consequences(literal lit, obj_map<expr, expr*>& var2val, index_set const& assumptions, expr_ref_vector& conseq);
|
||||
void extract_fixed_consequences(unsigned& idx, obj_map<expr, expr*>& var2val, index_set const& assumptions, expr_ref_vector& conseq);
|
||||
|
||||
|
||||
void display_consequence_progress(std::ostream& out, unsigned it, unsigned nv, unsigned fixed, unsigned unfixed, unsigned eq);
|
||||
|
||||
unsigned delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed);
|
||||
|
|
@ -1378,9 +1380,11 @@ namespace smt {
|
|||
|
||||
literal mk_diseq(expr* v, expr* val);
|
||||
|
||||
void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars,
|
||||
void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars,
|
||||
expr_ref_vector const& conseq, expr_ref_vector const& unfixed);
|
||||
|
||||
bool validate_justification(bool_var v, bool_var_data const& d, b_justification const& j);
|
||||
|
||||
void justify(literal lit, index_set& s);
|
||||
|
||||
void extract_cores(expr_ref_vector const& asms, vector<expr_ref_vector>& cores, unsigned& min_core_size);
|
||||
|
|
@ -1426,18 +1430,18 @@ namespace smt {
|
|||
|
||||
void pop(unsigned num_scopes);
|
||||
|
||||
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true);
|
||||
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true);
|
||||
|
||||
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);
|
||||
|
||||
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
|
||||
|
||||
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
|
||||
|
||||
|
||||
lbool setup_and_check(bool reset_cancel = true);
|
||||
|
||||
|
||||
// return 'true' if assertions are inconsistent.
|
||||
bool reduce_assertions();
|
||||
bool reduce_assertions();
|
||||
|
||||
bool resource_limits_exceeded();
|
||||
|
||||
|
|
@ -1462,15 +1466,15 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool already_internalized() const { return m_e_internalized_stack.size() > 2 || m_b_internalized_stack.size() > 1; }
|
||||
|
||||
|
||||
unsigned get_unsat_core_size() const {
|
||||
return m_unsat_core.size();
|
||||
}
|
||||
|
||||
|
||||
expr * get_unsat_core_expr(unsigned idx) const {
|
||||
return m_unsat_core.get(idx);
|
||||
}
|
||||
|
||||
|
||||
void get_model(model_ref & m) const;
|
||||
|
||||
bool update_model(bool refinalize);
|
||||
|
|
@ -1478,17 +1482,17 @@ namespace smt {
|
|||
void get_proto_model(proto_model_ref & m) const;
|
||||
|
||||
bool validate_model();
|
||||
|
||||
|
||||
unsigned get_num_asserted_formulas() const { return m_asserted_formulas.get_num_formulas(); }
|
||||
|
||||
unsigned get_asserted_formulas_last_level() const { return m_asserted_formulas.get_formulas_last_level(); }
|
||||
|
||||
expr * get_asserted_formula(unsigned idx) const { return m_asserted_formulas.get_formula(idx); }
|
||||
|
||||
|
||||
proof * get_asserted_formula_proof(unsigned idx) const { return m_asserted_formulas.get_formula_proof(idx); }
|
||||
|
||||
|
||||
expr * const * get_asserted_formulas() const { return m_asserted_formulas.get_formulas(); }
|
||||
|
||||
|
||||
proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); }
|
||||
|
||||
void get_assumptions_core(ptr_vector<expr> & result);
|
||||
|
|
@ -1500,7 +1504,7 @@ namespace smt {
|
|||
void display_unsat_core(std::ostream & out) const;
|
||||
|
||||
void collect_statistics(::statistics & st) const;
|
||||
|
||||
|
||||
void display_statistics(std::ostream & out) const;
|
||||
void display_istatistics(std::ostream & out) const;
|
||||
|
||||
|
|
|
|||
|
|
@ -402,6 +402,20 @@ namespace smt {
|
|||
|
||||
#endif
|
||||
|
||||
bool context::validate_justification(bool_var v, bool_var_data const& d, b_justification const& j) {
|
||||
if (j.get_kind() == b_justification::CLAUSE && v != true_bool_var) {
|
||||
clause* cls = j.get_clause();
|
||||
unsigned num_lits = cls->get_num_literals();
|
||||
literal l = cls->get_literal(0);
|
||||
if (l.var() != v) {
|
||||
l = cls->get_literal(1);
|
||||
}
|
||||
SASSERT(l.var() == v);
|
||||
SASSERT(m_assignment[l.index()] == l_true);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool context::validate_model() {
|
||||
if (!m_proto_model) {
|
||||
return true;
|
||||
|
|
|
|||
|
|
@ -27,6 +27,8 @@ namespace smt {
|
|||
out << "true";
|
||||
else if (*this == false_literal)
|
||||
out << "false";
|
||||
else if (*this == null_literal)
|
||||
out << "null";
|
||||
else if (sign())
|
||||
out << "(not " << mk_pp(bool_var2expr_map[var()], m) << ")";
|
||||
else
|
||||
|
|
|
|||
|
|
@ -22,42 +22,62 @@ Notes:
|
|||
#include"smt_params.h"
|
||||
#include"smt_params_helper.hpp"
|
||||
#include"mus.h"
|
||||
|
||||
#include"for_each_expr.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
#include"func_decl_dependencies.h"
|
||||
#include"dec_ref_util.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
class solver : public solver_na2as {
|
||||
smt_params m_smt_params;
|
||||
params_ref m_params;
|
||||
smt::kernel m_context;
|
||||
progress_callback * m_callback;
|
||||
symbol m_logic;
|
||||
bool m_minimizing_core;
|
||||
smt_params m_smt_params;
|
||||
params_ref m_params;
|
||||
smt::kernel m_context;
|
||||
progress_callback * m_callback;
|
||||
symbol m_logic;
|
||||
bool m_minimizing_core;
|
||||
bool m_core_extend_patterns;
|
||||
obj_map<expr, expr*> m_name2assertion;
|
||||
|
||||
public:
|
||||
solver(ast_manager & m, params_ref const & p, symbol const & l):
|
||||
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_minimizing_core(false),
|
||||
m_core_extend_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();
|
||||
}
|
||||
|
||||
virtual solver* translate(ast_manager& m, params_ref const& p) {
|
||||
solver* result = alloc(solver, m, p, m_logic);
|
||||
virtual solver * translate(ast_manager & m, params_ref const & p) {
|
||||
solver * result = alloc(solver, m, p, m_logic);
|
||||
smt::kernel::copy(m_context, result->m_context);
|
||||
|
||||
ast_translation translator(get_manager(), m);
|
||||
obj_map<expr, expr*>::iterator it = m_name2assertion.begin();
|
||||
obj_map<expr, expr*>::iterator end = m_name2assertion.end();
|
||||
for (; it != end; it++)
|
||||
result->m_name2assertion.insert(translator(it->m_key),
|
||||
translator(it->m_value));
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
|
||||
virtual ~solver() {
|
||||
dec_ref_values(get_manager(), m_name2assertion);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & 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();
|
||||
}
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
|
|
@ -81,11 +101,32 @@ namespace smt {
|
|||
m_context.assert_expr(t);
|
||||
}
|
||||
|
||||
virtual void assert_expr(expr * t, expr * a) {
|
||||
solver_na2as::assert_expr(t, a);
|
||||
SASSERT(!m_name2assertion.contains(a));
|
||||
get_manager().inc_ref(t);
|
||||
m_name2assertion.insert(a, t);
|
||||
}
|
||||
|
||||
virtual void push_core() {
|
||||
m_context.push();
|
||||
}
|
||||
|
||||
virtual void pop_core(unsigned n) {
|
||||
unsigned cur_sz = m_assumptions.size();
|
||||
if (n > 0 && cur_sz > 0) {
|
||||
unsigned lvl = m_scopes.size();
|
||||
SASSERT(n <= lvl);
|
||||
unsigned new_lvl = lvl - n;
|
||||
unsigned old_sz = m_scopes[new_lvl];
|
||||
for (unsigned i = cur_sz - 1; i >= old_sz; i--) {
|
||||
expr * key = m_assumptions[i].get();
|
||||
SASSERT(m_name2assertion.contains(key));
|
||||
expr * value = m_name2assertion.find(key);
|
||||
m.dec_ref(value);
|
||||
m_name2assertion.erase(key);
|
||||
}
|
||||
}
|
||||
m_context.pop(n);
|
||||
}
|
||||
|
||||
|
|
@ -97,7 +138,7 @@ namespace smt {
|
|||
struct scoped_minimize_core {
|
||||
solver& s;
|
||||
expr_ref_vector m_assumptions;
|
||||
scoped_minimize_core(solver& s): s(s), m_assumptions(s.m_assumptions) {
|
||||
scoped_minimize_core(solver& s) : s(s), m_assumptions(s.m_assumptions) {
|
||||
s.m_minimizing_core = true;
|
||||
s.m_assumptions.reset();
|
||||
}
|
||||
|
|
@ -114,17 +155,19 @@ namespace smt {
|
|||
r.push_back(m_context.get_unsat_core_expr(i));
|
||||
}
|
||||
|
||||
if (m_minimizing_core || smt_params_helper(m_params).core_minimize() == false) {
|
||||
return;
|
||||
}
|
||||
scoped_minimize_core scm(*this);
|
||||
mus mus(*this);
|
||||
mus.add_soft(r.size(), r.c_ptr());
|
||||
ptr_vector<expr> r2;
|
||||
if (l_true == mus.get_mus(r2)) {
|
||||
r.reset();
|
||||
r.append(r2);
|
||||
if (m_minimizing_core && smt_params_helper(m_params).core_minimize()) {
|
||||
scoped_minimize_core scm(*this);
|
||||
mus mus(*this);
|
||||
mus.add_soft(r.size(), r.c_ptr());
|
||||
ptr_vector<expr> r2;
|
||||
if (l_true == mus.get_mus(r2)) {
|
||||
r.reset();
|
||||
r.append(r2);
|
||||
}
|
||||
}
|
||||
|
||||
if (m_core_extend_patterns)
|
||||
add_pattern_literals_to_core(r);
|
||||
}
|
||||
|
||||
virtual void get_model(model_ref & m) {
|
||||
|
|
@ -149,7 +192,7 @@ namespace smt {
|
|||
r.append(tmp.size(), tmp.c_ptr());
|
||||
}
|
||||
|
||||
virtual ast_manager& get_manager() const { return m_context.m(); }
|
||||
virtual ast_manager & get_manager() const { return m_context.m(); }
|
||||
|
||||
virtual void set_progress_callback(progress_callback * callback) {
|
||||
m_callback = callback;
|
||||
|
|
@ -159,12 +202,115 @@ namespace smt {
|
|||
virtual unsigned get_num_assertions() const {
|
||||
return m_context.size();
|
||||
}
|
||||
|
||||
|
||||
virtual expr * get_assertion(unsigned idx) const {
|
||||
SASSERT(idx < get_num_assertions());
|
||||
return m_context.get_formulas()[idx];
|
||||
}
|
||||
}
|
||||
|
||||
struct collect_fds_proc {
|
||||
ast_manager & m;
|
||||
func_decl_set & m_fds;
|
||||
collect_fds_proc(ast_manager & m, func_decl_set & fds) :
|
||||
m(m), m_fds(fds) {
|
||||
}
|
||||
void operator()(var * n) {}
|
||||
void operator()(app * n) {
|
||||
func_decl * fd = n->get_decl();
|
||||
if (fd->get_family_id() == null_family_id)
|
||||
m_fds.insert_if_not_there(fd);
|
||||
}
|
||||
void operator()(quantifier * n) {}
|
||||
};
|
||||
|
||||
struct collect_pattern_fds_proc {
|
||||
ast_manager & m;
|
||||
expr_fast_mark1 m_visited;
|
||||
func_decl_set & m_fds;
|
||||
collect_pattern_fds_proc(ast_manager & m, func_decl_set & fds) :
|
||||
m(m), m_fds(fds) {
|
||||
m_visited.reset();
|
||||
}
|
||||
void operator()(var * n) {}
|
||||
void operator()(app * n) {}
|
||||
void operator()(quantifier * n) {
|
||||
collect_fds_proc p(m, m_fds);
|
||||
|
||||
unsigned sz = n->get_num_patterns();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
quick_for_each_expr(p, m_visited, n->get_pattern(i));
|
||||
|
||||
sz = n->get_num_no_patterns();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
quick_for_each_expr(p, m_visited, n->get_no_pattern(i));
|
||||
}
|
||||
};
|
||||
|
||||
void collect_pattern_func_decls(expr_ref & e, func_decl_set & fds) {
|
||||
collect_pattern_fds_proc p(get_manager(), fds);
|
||||
expr_mark visited;
|
||||
for_each_expr(p, visited, e);
|
||||
}
|
||||
|
||||
void compute_assrtn_fds(ptr_vector<expr> & core, vector<func_decl_set> & assrtn_fds) {
|
||||
assrtn_fds.resize(m_name2assertion.size());
|
||||
obj_map<expr, expr*>::iterator ait = m_name2assertion.begin();
|
||||
obj_map<expr, expr*>::iterator aend = m_name2assertion.end();
|
||||
for (unsigned i = 0; ait != aend; ait++, i++) {
|
||||
if (core.contains(ait->m_key))
|
||||
continue;
|
||||
collect_fds_proc p(m, assrtn_fds[i]);
|
||||
expr_fast_mark1 visited;
|
||||
quick_for_each_expr(p, visited, ait->m_value);
|
||||
}
|
||||
}
|
||||
|
||||
bool fds_intersect(func_decl_set & pattern_fds, func_decl_set & assrtn_fds) {
|
||||
func_decl_set::iterator it = pattern_fds.begin();
|
||||
func_decl_set::iterator end = pattern_fds.end();
|
||||
for (; it != end; it++) {
|
||||
func_decl * fd = *it;
|
||||
if (assrtn_fds.contains(fd))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void add_pattern_literals_to_core(ptr_vector<expr> & core) {
|
||||
ast_manager & m = get_manager();
|
||||
expr_ref_vector new_core_literals(m);
|
||||
|
||||
func_decl_set pattern_fds;
|
||||
vector<func_decl_set> assrtn_fds;
|
||||
|
||||
do {
|
||||
new_core_literals.reset();
|
||||
|
||||
unsigned sz = core.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
expr_ref name(core[i], m);
|
||||
SASSERT(m_name2assertion.contains(name));
|
||||
expr_ref assrtn(m_name2assertion.find(name), m);
|
||||
collect_pattern_func_decls(assrtn, pattern_fds);
|
||||
}
|
||||
|
||||
if (!pattern_fds.empty()) {
|
||||
if (assrtn_fds.empty())
|
||||
compute_assrtn_fds(core, assrtn_fds);
|
||||
|
||||
obj_map<expr, expr*>::iterator ait = m_name2assertion.begin();
|
||||
obj_map<expr, expr*>::iterator aend = m_name2assertion.end();
|
||||
for (unsigned i = 0; ait != aend; ait++, i++) {
|
||||
if (!core.contains(ait->m_key) &&
|
||||
fds_intersect(pattern_fds, assrtn_fds[i]))
|
||||
new_core_literals.push_back(ait->m_key);
|
||||
}
|
||||
}
|
||||
|
||||
core.append(new_core_literals.size(), new_core_literals.c_ptr());
|
||||
}
|
||||
while (!new_core_literals.empty());
|
||||
}
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -180,7 +180,7 @@ namespace smt {
|
|||
|
||||
final_check_status theory_wmaxsat::final_check_eh() {
|
||||
if (m_normalize) normalize();
|
||||
// std::cout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n";
|
||||
TRACE("opt", tout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n";);
|
||||
return FC_DONE;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue