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

Merge branch 'upstream-master' into develop

Browse source 
Conflicts:
	src/smt/params/smt_params.cpp
	src/smt/params/smt_params.h
	src/smt/smt_context.cpp
	src/smt/smt_context.h
This commit is contained in:
Murphy Berzish 2017-05-01 21:33:23 -04:00
commit 0862949e66
28 changed files with 691 additions and 170 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifier/poly_simplifier_plugin.h
View file

@ -37,7 +37,7 @@ protected:
expr * mk_add(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_add(2, args); }
expr * mk_mul(unsigned num_args, expr * const * args);
expr * mk_mul(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_mul(2, args); }
expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); }
// expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); }
expr * mk_uminus(expr * arg) { return m_manager.mk_app(m_fid, m_UMINUS, arg); }
void process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer<expr> & result);

1
src/cmd_context/check_logic.cpp
View file

@ -187,6 +187,7 @@ struct check_logic::imp {
m_bvs = true;
m_uf = true;
m_ints = true;
m_nonlinear = true; // non-linear 0-1 variables may get eliminated
}
else {
m_unknown_logic = true;

1
src/muz/base/dl_util.h
View file

@ -29,6 +29,7 @@ Revision History:
#include"substitution.h"
#include"ast_counter.h"
#include"statistics.h"
#include"stopwatch.h"
#include"lbool.h"
namespace datalog {

1
src/muz/rel/dl_instruction.h
View file

@ -30,7 +30,6 @@ Revision History:
namespace datalog {
class execution_context;
class instruction_block;
class rel_context;

18
src/parsers/smt2/smt2parser.cpp
View file

@ -2219,11 +2219,27 @@ namespace smt2 {
if (m_cached_strings.empty())
throw cmd_exception("invalid get-value command, empty list of terms");
next();
unsigned index = 0;
if (curr_is_keyword() && (curr_id() == ":model-index" || curr_id() == ":model_index")) {
next();
check_int("integer index expected to indexed model evaluation");
if (!curr_numeral().is_unsigned())
throw parser_exception("expected unsigned integer index to model evaluation");
index = curr_numeral().get_unsigned();
next();
}
check_rparen("invalid get-value command, ')' expected");
if (!m_ctx.is_model_available() || m_ctx.get_check_sat_result() == 0)
throw cmd_exception("model is not available");
model_ref md;
m_ctx.get_check_sat_result()->get_model(md);
if (index == 0) {
m_ctx.get_check_sat_result()->get_model(md);
}
else {
m_ctx.get_opt()->get_box_model(md, index);
}
m_ctx.regular_stream() << "(";
expr ** expr_it = expr_stack().c_ptr() + spos;
expr ** expr_end = expr_it + m_cached_strings.size();

174
src/sat/sat_solver.cpp
View file

@ -3141,6 +3141,101 @@ namespace sat {
//
// -----------------------
static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
for (unsigned i = 0; i < lambda.size(); ++i) {
if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
lambda[i] = lambda.back();
lambda.pop_back();
--i;
}
}
}
// Algorithm 7: Corebased Algorithm with Chunking
static void back_remove(sat::literal_vector& lits, sat::literal l) {
for (unsigned i = lits.size(); i > 0; ) {
--i;
if (lits[i] == l) {
lits[i] = lits.back();
lits.pop_back();
return;
}
}
std::cout << "UNREACHABLE\n";
}
static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector<sat::literal_vector>& conseq) {
for (unsigned i = 0; i < gamma.size(); ++i) {
sat::literal nlit = ~gamma[i];
sat::literal_vector asms1(asms);
asms1.push_back(nlit);
lbool r = s.check(asms1.size(), asms1.c_ptr());
if (r == l_false) {
conseq.push_back(s.get_core());
}
}
}
static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
sat::literal_vector lambda;
for (unsigned i = 0; i < vars.size(); i++) {
lambda.push_back(sat::literal(vars[i], m[vars[i]] == l_false));
}
while (!lambda.empty()) {
IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << conseq.size() << ")\n";);
unsigned k = std::min(K, lambda.size());
sat::literal_vector gamma, omegaN;
for (unsigned i = 0; i < k; ++i) {
sat::literal l = lambda[lambda.size() - i - 1];
gamma.push_back(l);
omegaN.push_back(~l);
}
while (true) {
sat::literal_vector asms1(asms);
asms1.append(omegaN);
lbool r = s.check(asms1.size(), asms1.c_ptr());
if (r == l_true) {
IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";);
prune_unfixed(lambda, s.get_model());
break;
}
sat::literal_vector const& core = s.get_core();
sat::literal_vector occurs;
IF_VERBOSE(1, verbose_stream() << "(core " << core.size() << ")\n";);
for (unsigned i = 0; i < omegaN.size(); ++i) {
if (core.contains(omegaN[i])) {
occurs.push_back(omegaN[i]);
}
}
if (occurs.size() == 1) {
sat::literal lit = occurs.back();
sat::literal nlit = ~lit;
conseq.push_back(core);
back_remove(lambda, ~lit);
back_remove(gamma, ~lit);
s.mk_clause(1, &nlit);
}
for (unsigned i = 0; i < omegaN.size(); ++i) {
if (occurs.contains(omegaN[i])) {
omegaN[i] = omegaN.back();
omegaN.pop_back();
--i;
}
}
if (omegaN.empty() && occurs.size() > 1) {
brute_force_consequences(s, asms, gamma, conseq);
for (unsigned i = 0; i < gamma.size(); ++i) {
back_remove(lambda, gamma[i]);
}
break;
}
}
}
return l_true;
}
lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
literal_vector lits;
lbool is_sat = l_true;
@ -3163,6 +3258,9 @@ namespace sat {
default: break;
}
}
// is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
is_sat = get_consequences(asms, lits, conseq);
set_model(mdl);
return is_sat;
@ -3273,13 +3371,14 @@ namespace sat {
propagate(false);
if (check_inconsistent()) return l_false;
unsigned num_units = 0, num_iterations = 0;
extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq);
unsigned num_iterations = 0;
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
update_unfixed_literals(unfixed_lits, unfixed_vars);
while (!unfixed_lits.empty()) {
if (scope_lvl() > 1) {
pop(scope_lvl() - 1);
}
propagate(false);
++num_iterations;
checkpoint();
literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
@ -3291,6 +3390,10 @@ namespace sat {
literal lit = *it;
if (value(lit) != l_undef) {
++num_fixed;
if (lvl(lit) <= 1) {
SASSERT(value(lit) == l_true);
extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
}
continue;
}
push();
@ -3307,19 +3410,14 @@ namespace sat {
propagate(false);
++num_resolves;
}
if (scope_lvl() == 1) {
if (false && scope_lvl() == 1) {
is_sat = l_undef;
break;
}
}
if (scope_lvl() == 1) {
it = unfixed_lits.begin();
for (; it != end; ++it) {
literal lit = *it;
if (value(lit) == l_true) {
VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
}
}
}
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
if (is_sat == l_true) {
if (scope_lvl() == 1 && num_resolves > 0) {
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences backjump)\n";);
@ -3330,6 +3428,7 @@ namespace sat {
if (is_sat == l_undef) {
restart();
}
extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
}
}
if (is_sat == l_false) {
@ -3339,7 +3438,6 @@ namespace sat {
if (is_sat == l_true) {
delete_unfixed(unfixed_lits, unfixed_vars);
}
extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq);
update_unfixed_literals(unfixed_lits, unfixed_vars);
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences"
<< " iterations: " << num_iterations
@ -3391,32 +3489,47 @@ namespace sat {
SASSERT(!inconsistent());
unsigned sz = m_trail.size();
for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) {
if (!extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)) {
for (i = 0; i < sz && lvl(m_trail[i]) <= 1; ++i) {
VERIFY(extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq));
}
break;
}
extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq);
}
start = sz;
}
void solver::extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed_vars, vector<literal_vector>& conseq) {
literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
for (; it != end; ++it) {
literal lit = *it;
if (lvl(lit) <= 1) {
SASSERT(value(lit) == l_true);
extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
}
}
}
bool solver::check_domain(literal lit, literal lit2) {
return m_antecedents.contains(lit2.var());
if (!m_antecedents.contains(lit2.var())) {
SASSERT(value(lit2) == l_true);
m_todo_antecedents.push_back(lit2);
TRACE("sat", tout << "todo: " << lit2 << " " << value(lit2) << "\n";);
return false;
}
else {
return true;
}
}
bool solver::extract_assumptions(literal lit, index_set& s) {
justification js = m_justification[lit.var()];
TRACE("sat", tout << lit << " " << js << "\n";);
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
if (!check_domain(lit, js.get_literal())) return false;
if (!check_domain(lit, ~js.get_literal())) return false;
s |= m_antecedents.find(js.get_literal().var());
break;
case justification::TERNARY:
if (!check_domain(lit, js.get_literal1())) return false;
if (!check_domain(lit, js.get_literal2())) return false;
if (!check_domain(lit, ~js.get_literal1()) ||
!check_domain(lit, ~js.get_literal2())) return false;
s |= m_antecedents.find(js.get_literal1().var());
s |= m_antecedents.find(js.get_literal2().var());
break;
@ -3424,7 +3537,7 @@ namespace sat {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
for (unsigned i = 0; i < c.size(); ++i) {
if (c[i] != lit) {
if (!check_domain(lit, c[i])) return false;
if (!check_domain(lit, ~c[i])) return false;
s |= m_antecedents.find(c[i].var());
}
}
@ -3458,7 +3571,7 @@ namespace sat {
}
bool solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
index_set s;
if (m_antecedents.contains(lit.var())) {
return true;
@ -3468,6 +3581,7 @@ namespace sat {
}
else {
if (!extract_assumptions(lit, s)) {
SASSERT(!m_todo_antecedents.empty());
return false;
}
add_assumption(lit);
@ -3486,6 +3600,16 @@ namespace sat {
return true;
}
void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
SASSERT(m_todo_antecedents.empty());
m_todo_antecedents.push_back(lit);
while (!m_todo_antecedents.empty()) {
if (extract_fixed_consequences1(m_todo_antecedents.back(), assumptions, unfixed, conseq)) {
m_todo_antecedents.pop_back();
}
}
}
void solver::asymmetric_branching() {
if (scope_lvl() > 0 || inconsistent())
return;

7
src/sat/sat_solver.h
View file

@ -481,6 +481,7 @@ namespace sat {
typedef hashtable<unsigned, u_hash, u_eq> index_set;
u_map<index_set> m_antecedents;
literal_vector m_todo_antecedents;
vector<literal_vector> m_binary_clause_graph;
bool extract_assumptions(literal lit, index_set& s);
@ -497,7 +498,11 @@ namespace sat {
void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
bool extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
bool extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars);

14
src/shell/opt_frontend.cpp
View file

@ -20,12 +20,12 @@ static opt::context* g_opt = 0;
static double g_start_time = 0;
static unsigned_vector g_handles;
class stream_buffer {
class opt_stream_buffer {
std::istream & m_stream;
int m_val;
unsigned m_line;
public:
stream_buffer(std::istream & s):
opt_stream_buffer(std::istream & s):
m_stream(s),
m_line(0) {
m_val = m_stream.get();
@ -111,7 +111,7 @@ public:
class wcnf {
opt::context& opt;
ast_manager& m;
stream_buffer& in;
opt_stream_buffer& in;
app_ref read_clause(unsigned& weight) {
int parsed_lit;
@ -141,7 +141,7 @@ class wcnf {
public:
wcnf(opt::context& opt, stream_buffer& in): opt(opt), m(opt.get_manager()), in(in) {
wcnf(opt::context& opt, opt_stream_buffer& in): opt(opt), m(opt.get_manager()), in(in) {
opt.set_clausal(true);
}
@ -180,7 +180,7 @@ public:
class opb {
opt::context& opt;
ast_manager& m;
stream_buffer& in;
opt_stream_buffer& in;
arith_util arith;
app_ref parse_id() {
@ -254,7 +254,7 @@ class opb {
opt.add_hard_constraint(t);
}
public:
opb(opt::context& opt, stream_buffer& in):
opb(opt::context& opt, opt_stream_buffer& in):
opt(opt), m(opt.get_manager()),
in(in), arith(m) {}
@ -335,7 +335,7 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
g_opt = &opt;
params_ref p = gparams::get_module("opt");
opt.updt_params(p);
stream_buffer _in(in);
opt_stream_buffer _in(in);
if (is_wcnf) {
wcnf wcnf(opt, _in);
wcnf.parse();

88
src/smt/smt_context.cpp
View file

@ -63,7 +63,6 @@ namespace smt {
m_is_diseq_tmp(0),
m_units_to_reassert(m_manager),
m_qhead(0),
m_th_case_split_qhead(0),
m_simp_qhead(0),
m_simp_counter(0),
m_bvar_inc(1.0),
@ -341,7 +340,6 @@ namespace smt {
bool context::bcp() {
SASSERT(!inconsistent());
m_th_case_split_qhead = m_qhead;
while (m_qhead < m_assigned_literals.size()) {
if (get_cancel_flag()) {
return true;
@ -1777,7 +1775,7 @@ namespace smt {
unsigned qhead = m_qhead;
if (!bcp())
return false;
if (!propagate_th_case_split())
if (!propagate_th_case_split(qhead))
return false;
if (get_cancel_flag()) {
m_qhead = qhead;
@ -2977,7 +2975,6 @@ namespace smt {
public:
case_split_insert_trail(literal l):
l(l) {
}
virtual void undo(context & ctx) {
ctx.undo_th_case_split(l);
@ -2988,23 +2985,19 @@ namespace smt {
TRACE("theory_case_split", display_literals_verbose(tout << "theory case split: ", num_lits, lits); tout << std::endl;);
// If we don't use the theory case split heuristic,
// for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2)
// to enforce the condition that more than one literal can't be
// assigned 'true' simultaneously.
// to enforce the condition that at most one literal can be assigned 'true'.
if (!m_fparams.m_theory_case_split) {
for (unsigned i = 0; i < num_lits; ++i) {
for (unsigned j = i+1; j < num_lits; ++j) {
literal l1 = lits[i];
literal l2 = lits[j];
literal excl[2] = {~l1, ~l2};
justification * j_excl = 0;
mk_clause(2, excl, j_excl);
mk_clause(~l1, ~l2, (justification*) 0);
}
}
} else {
literal_vector new_case_split; // TODO is it okay to allocate this on the stack?
literal_vector new_case_split;
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
// TODO do we need to enforce this invariant? can we make undo information work without it?
SASSERT(!m_all_th_case_split_literals.contains(l.index()));
m_all_th_case_split_literals.insert(l.index());
push_trail(case_split_insert_trail(l));
@ -3020,11 +3013,11 @@ namespace smt {
m_literal2casesplitsets[l.index()].push_back(new_case_split);
}
TRACE("theory_case_split", tout << "tracking case split literal set { ";
for (unsigned i = 0; i < num_lits; ++i) {
tout << lits[i].index() << " ";
}
tout << "}" << std::endl;
);
for (unsigned i = 0; i < num_lits; ++i) {
tout << lits[i].index() << " ";
}
tout << "}" << std::endl;
);
}
}
@ -3041,7 +3034,7 @@ namespace smt {
}
}
bool context::propagate_th_case_split() {
bool context::propagate_th_case_split(unsigned qhead) {
if (m_all_th_case_split_literals.empty())
return true;
@ -3049,46 +3042,33 @@ namespace smt {
// not counting any literals that get assigned by this method
// this relies on bcp() to give us its old m_qhead and therefore
// bcp() should always be called before this method
unsigned assigned_literal_idx = m_th_case_split_qhead;
unsigned assigned_literal_end = m_assigned_literals.size();
while(assigned_literal_idx < assigned_literal_end) {
literal l = m_assigned_literals[assigned_literal_idx];
for (; qhead < assigned_literal_end; ++qhead) {
literal l = m_assigned_literals[qhead];
TRACE("theory_case_split", tout << "check literal " << l.index() << std::endl; display_literal_verbose(tout, l); tout << std::endl;);
++assigned_literal_idx;
// check if this literal participates in any theory case split
if (m_all_th_case_split_literals.contains(l.index())) {
TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;);
// now find the sets of literals which contain l
vector<literal_vector> case_split_sets = m_literal2casesplitsets.get(l.index(), vector<literal_vector>());
for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) {
literal_vector case_split_set = *it;
TRACE("theory_case_split", tout << "found case split set { ";
for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
tout << set_it->index() << " ";
}
tout << "}" << std::endl;);
for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
literal l2 = *set_it;
if (l2 != l) {
b_justification js(l);
switch (get_assignment(l2)) {
case l_false:
TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned False" << std::endl;);
break;
// TODO these next two cases can be combined. I'm doing this for debugging purposes
case l_undef:
TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is not assigned" << std::endl;);
assign(~l2, js);
break;
case l_true:
TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned True" << std::endl;);
assign(~l2, js);
break;
}
if (inconsistent()) {
TRACE("theory_case_split", tout << "conflict detected!" << std::endl;);
return false;
}
if (!m_all_th_case_split_literals.contains(l.index())) {
continue;
}
TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;);
// now find the sets of literals which contain l
vector<literal_vector> const& case_split_sets = m_literal2casesplitsets[l.index()];
for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) {
literal_vector case_split_set = *it;
TRACE("theory_case_split", tout << "found case split set { ";
for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
tout << set_it->index() << " ";
}
tout << "}" << std::endl;);
for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
literal l2 = *set_it;
if (l2 != l) {
b_justification js(l);
TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr()););
assign(~l2, js);
if (inconsistent()) {
TRACE("theory_case_split", tout << "conflict detected!" << std::endl;);
return false;
}
}
}

3
src/smt/smt_context.h
View file

@ -234,7 +234,6 @@ namespace smt {
uint_set m_all_th_case_split_literals;
vector<literal_vector> m_th_case_split_sets;
u_map< vector<literal_vector> > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in
unsigned m_th_case_split_qhead;
// -----------------------------------
//
@ -851,7 +850,7 @@ namespace smt {
// helper function for trail
void undo_th_case_split(literal l);
bool propagate_th_case_split();
bool propagate_th_case_split(unsigned qhead);
bool_var mk_bool_var(expr * n);

1
src/smt/smt_context_inv.cpp
View file

@ -405,7 +405,6 @@ namespace smt {
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);

1
src/smt/theory_arith.h
View file

@ -552,6 +552,7 @@ namespace smt {
bool is_int(theory_var v) const { return m_data[v].m_is_int; }
bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); }
bool is_real(theory_var v) const { return !is_int(v); }
bool is_real_src(theory_var v) const { return !is_int_src(v); }
bool get_implied_old_value(theory_var v, inf_numeral & r) const;
inf_numeral const & get_implied_value(theory_var v) const;
inf_numeral const & get_quasi_base_value(theory_var v) const { return get_implied_value(v); }

2
src/smt/theory_arith_core.h
View file

@ -465,7 +465,7 @@ namespace smt {
TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
tout << s_ante << "\n" << s_conseq << "\n";);
literal lits[2] = {l_ante, l_conseq};
// literal lits[2] = {l_ante, l_conseq};
mk_clause(l_ante, l_conseq, 0, 0);
if (ctx.relevancy()) {
if (l_ante == false_literal) {

38
src/smt/theory_arith_nl.h
View file

@ -444,7 +444,7 @@ namespace smt {
m_asserted_bounds.push_back(new_bound);
// copy justification to new bound
dependency2new_bound(dep, *new_bound);
TRACE("buggy_bound", new_bound->display(*this, tout); tout << "\n";);
TRACE("non_linear", new_bound->display(*this, tout); tout << "\n";);
}
/**
@ -457,8 +457,19 @@ namespace smt {
bool r = false;
if (!i.minus_infinity()) {
inf_numeral new_lower(i.get_lower_value());
if (i.is_lower_open())
new_lower += get_epsilon(v);
if (i.is_lower_open()) {
if (is_int(v)) {
if (new_lower.is_int()) {
new_lower += rational::one();
}
else {
new_lower = ceil(new_lower.get_rational());
}
}
else {
new_lower += get_epsilon(v);
}
}
bound * old_lower = lower(v);
if (old_lower == 0 || new_lower > old_lower->get_value()) {
TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << new_lower << "\n";
@ -469,8 +480,19 @@ namespace smt {
}
if (!i.plus_infinity()) {
inf_numeral new_upper(i.get_upper_value());
if (i.is_upper_open())
new_upper -= get_epsilon(v);
if (i.is_upper_open()) {
if (is_int(v)) {
if (new_upper.is_int()) {
new_upper -= rational::one();
}
else {
new_upper = floor(new_upper.get_rational());
}
}
else {
new_upper -= get_epsilon(v);
}
}
bound * old_upper = upper(v);
if (old_upper == 0 || new_upper < old_upper->get_value()) {
TRACE("non_linear", tout << "NEW upper bound for v" << v << " " << new_upper << "\n";
@ -819,6 +841,7 @@ namespace smt {
if (is_fixed(_var))
r *= lower_bound(_var).get_rational();
}
TRACE("arith", tout << mk_pp(m, get_manager()) << " " << r << "\n";);
return r;
}
@ -896,7 +919,7 @@ namespace smt {
// Assert the equality
// (= (* x_1 ... x_n) k)
TRACE("non_linear", tout << "all variables are fixed.\n";);
TRACE("non_linear", tout << "all variables are fixed, and bound is: " << k << "\n";);
new_lower = alloc(derived_bound, v, inf_numeral(k), B_LOWER);
new_upper = alloc(derived_bound, v, inf_numeral(k), B_UPPER);
}
@ -953,7 +976,8 @@ namespace smt {
new_upper->m_eqs.append(new_lower->m_eqs);
TRACE("non_linear",
tout << "lower: " << new_lower << " upper: " << new_upper << "\n";
new_lower->display(*this, tout << "lower: "); tout << "\n";
new_upper->display(*this, tout << "upper: "); tout << "\n";
for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_upper->m_lits[j]);
tout << " ";

16
src/smt/theory_bv.cpp
View file

@ -762,6 +762,21 @@ namespace smt {
TRACE("bv", tout << mk_pp(cond, get_manager()) << "\n"; tout << l << "\n";); \
}
void theory_bv::internalize_sub(app *n) {
SASSERT(!get_context().e_internalized(n));
SASSERT(n->get_num_args() == 2);
process_args(n);
ast_manager & m = get_manager();
enode * e = mk_enode(n);
expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
get_arg_bits(e, 0, arg1_bits);
get_arg_bits(e, 1, arg2_bits);
SASSERT(arg1_bits.size() == arg2_bits.size());
expr_ref carry(m);
m_bb.mk_subtracter(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits, carry);
init_bits(e, bits);
}
MK_UNARY(internalize_not, mk_not);
MK_UNARY(internalize_redand, mk_redand);
MK_UNARY(internalize_redor, mk_redor);
@ -848,6 +863,7 @@ namespace smt {
switch (term->get_decl_kind()) {
case OP_BV_NUM: internalize_num(term); return true;
case OP_BADD: internalize_add(term); return true;
case OP_BSUB: internalize_sub(term); return true;
case OP_BMUL: internalize_mul(term); return true;
case OP_BSDIV_I: internalize_sdiv(term); return true;
case OP_BUDIV_I: internalize_udiv(term); return true;

1
src/smt/theory_bv.h
View file

@ -172,6 +172,7 @@ namespace smt {
bool get_fixed_value(theory_var v, numeral & result) const;
void internalize_num(app * n);
void internalize_add(app * n);
void internalize_sub(app * n);
void internalize_mul(app * n);
void internalize_udiv(app * n);
void internalize_sdiv(app * n);

4
src/smt/theory_seq.cpp
View file

@ -3874,8 +3874,8 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
}
else if (n1 != n2 && m_util.is_re(n1->get_owner())) {
warning_msg("equality between regular expressions is not yet supported");
eautomaton* a1 = get_automaton(n1->get_owner());
eautomaton* a2 = get_automaton(n2->get_owner());
// eautomaton* a1 = get_automaton(n1->get_owner());
// eautomaton* a2 = get_automaton(n2->get_owner());
// eautomaton* b1 = mk_difference(*a1, *a2);
// eautomaton* b2 = mk_difference(*a2, *a1);
// eautomaton* c = mk_union(*b1, *b2);

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

@ -137,8 +137,10 @@ public:
SASSERT(num.is_unsigned());
expr_ref head(m);
ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range());
head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
consequences[i] = m.mk_implies(a, head);
if (enums.size() > num.get_unsigned()) {
head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
consequences[i] = m.mk_implies(a, head);
}
}
}
return r;

99
src/test/cnf_backbones.cpp
View file

@ -64,6 +64,56 @@ static void display_status(lbool r) {
}
}
static void track_clause(sat::solver& dst,
sat::literal_vector& lits,
sat::literal_vector& assumptions,
vector<sat::literal_vector>& tracking_clauses) {
sat::literal lit = sat::literal(dst.mk_var(true, false), false);
tracking_clauses.set(lit.var(), lits);
lits.push_back(~lit);
dst.mk_clause(lits.size(), lits.c_ptr());
assumptions.push_back(lit);
}
static void track_clauses(sat::solver const& src,
sat::solver& dst,
sat::literal_vector& assumptions,
vector<sat::literal_vector>& tracking_clauses) {
for (sat::bool_var v = 0; v < src.num_vars(); ++v) {
dst.mk_var(false, true);
}
sat::literal_vector lits;
sat::literal lit;
sat::clause * const * it = src.begin_clauses();
sat::clause * const * end = src.end_clauses();
svector<sat::solver::bin_clause> bin_clauses;
src.collect_bin_clauses(bin_clauses, false);
tracking_clauses.reserve(2*src.num_vars() + static_cast<unsigned>(end - it) + bin_clauses.size());
for (sat::bool_var v = 1; v < src.num_vars(); ++v) {
if (src.value(v) != l_undef) {
bool sign = src.value(v) == l_false;
lits.reset();
lits.push_back(sat::literal(v, sign));
track_clause(dst, lits, assumptions, tracking_clauses);
}
}
for (; it != end; ++it) {
lits.reset();
sat::clause& cls = *(*it);
lits.append(static_cast<unsigned>(cls.end()-cls.begin()), cls.begin());
track_clause(dst, lits, assumptions, tracking_clauses);
}
for (unsigned i = 0; i < bin_clauses.size(); ++i) {
lits.reset();
lits.push_back(bin_clauses[i].first);
lits.push_back(bin_clauses[i].second);
track_clause(dst, lits, assumptions, tracking_clauses);
}
}
static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
for (unsigned i = 0; i < lambda.size(); ++i) {
if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
@ -88,26 +138,27 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
std::cout << "UNREACHABLE\n";
}
static void brute_force_consequences(sat::solver& s, sat::literal_vector const& gamma, sat::literal_vector& backbones) {
static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, sat::literal_vector& backbones) {
for (unsigned i = 0; i < gamma.size(); ++i) {
sat::literal nlit = ~gamma[i];
lbool r = s.check(1, &nlit);
sat::literal_vector asms1(asms);
asms1.push_back(nlit);
lbool r = s.check(asms1.size(), asms1.c_ptr());
if (r == l_false) {
backbones.push_back(gamma[i]);
}
}
}
static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sat::literal_vector>& conseq, unsigned K) {
lbool r = s.check();
display_status(r);
static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
lbool r = s.check(asms.size(), asms.c_ptr());
if (r != l_true) {
return r;
}
sat::model const & m = s.get_model();
sat::literal_vector lambda, backbones;
for (unsigned i = 1; i < m.size(); i++) {
lambda.push_back(sat::literal(i, m[i] == l_false));
for (unsigned i = 0; i < vars.size(); i++) {
lambda.push_back(sat::literal(vars[i], m[vars[i]] == l_false));
}
while (!lambda.empty()) {
IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << backbones.size() << ")\n";);
@ -119,7 +170,9 @@ static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sa
omegaN.push_back(~l);
}
while (true) {
r = s.check(omegaN.size(), omegaN.c_ptr());
sat::literal_vector asms1(asms);
asms1.append(omegaN);
r = s.check(asms1.size(), asms1.c_ptr());
if (r == l_true) {
IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";);
prune_unfixed(lambda, s.get_model());
@ -149,7 +202,7 @@ static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sa
}
}
if (omegaN.empty() && occurs.size() > 1) {
brute_force_consequences(s, gamma, backbones);
brute_force_consequences(s, asms, gamma, backbones);
for (unsigned i = 0; i < gamma.size(); ++i) {
back_remove(lambda, gamma[i]);
}
@ -174,6 +227,7 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
p.set_bool("produce_models", true);
reslimit limit;
sat::solver solver(p, limit, 0);
sat::solver solver2(p, limit, 0);
g_solver = &solver;
if (file_name) {
@ -192,16 +246,22 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
vector<sat::literal_vector> conseq;
sat::bool_var_vector vars;
sat::literal_vector assumptions;
for (unsigned i = 1; i < solver.num_vars(); ++i) {
if (p.get_bool("dimacs.core", false)) {
g_solver = &solver2;
vector<sat::literal_vector> tracking_clauses;
track_clauses(solver, solver2, assumptions, tracking_clauses);
}
for (unsigned i = 1; i < g_solver->num_vars(); ++i) {
vars.push_back(i);
solver.set_external(i);
g_solver->set_external(i);
}
lbool r;
if (use_chunk) {
r = core_chunking(solver, vars, conseq, 100);
r = core_chunking(*g_solver, vars, assumptions, conseq, 100);
}
else {
r = solver.get_consequences(assumptions, vars, conseq);
r = g_solver->get_consequences(assumptions, vars, conseq);
}
std::cout << vars.size() << " " << conseq.size() << "\n";
display_status(r);
@ -209,10 +269,15 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
}
void tst_cnf_backbones(char ** argv, int argc, int& i) {
bool use_chunk = i + 1 < argc && argv[i + 1] == std::string("chunk");
if (use_chunk) ++i;
char const* file = "";
if (i + 1 < argc) {
bool use_chunk = (i + 2 < argc && argv[i + 2] == std::string("chunk"));
cnf_backbones(use_chunk, argv[i + 1]);
++i;
if (use_chunk) ++i;
file = argv[i + 1];
}
else {
file = argv[1];
}
cnf_backbones(use_chunk, file);
++i;
}

14
src/test/main.cpp
View file

@ -8,6 +8,7 @@
#include"timeit.h"
#include"warning.h"
#include "memory_manager.h"
#include"gparams.h"
//
// Unit tests fail by asserting.
@ -75,7 +76,7 @@ void display_usage() {
void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all) {
int i = 1;
while (i < argc) {
char * arg = argv[i];
char * arg = argv[i], *eq_pos = 0;
if (arg[0] == '-' || arg[0] == '/') {
char * opt_name = arg + 1;
@ -118,6 +119,17 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t
}
#endif
}
else if (arg[0] != '"' && (eq_pos = strchr(arg, '='))) {
char * key = arg;
*eq_pos = 0;
char * value = eq_pos+1;
try {
gparams::set(key, value);
}
catch (z3_exception& ex) {
std::cerr << ex.msg() << "\n";
}
}
i++;
}
}