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

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-04-30 10:23:05 -07:00
commit 5fcbf55216
31 changed files with 1029 additions and 185 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/z3_api.h
View file

@ -1500,7 +1500,7 @@ extern "C" {
All main interaction with Z3 happens in the context of a \c Z3_context.
In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
are determined by the scope level of #Z3_push and #Z3_pop.
are determined by the scope level of #Z3_solver_push and #Z3_solver_pop.
In other words, a Z3_ast object remains valid until there is a
call to Z3_pop that takes the current scope below the level where
the object was created.
@ -3091,8 +3091,8 @@ extern "C" {
\brief Create a numeral of a given sort.
\param c logical context.
\param numeral A string representing the numeral value in decimal notation. The string may be of the form \code{[num]*[.[num]*][E[+|-][num]+]}.
If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}.
\param numeral A string representing the numeral value in decimal notation. The string may be of the form `[num]*[.[num]*][E[+|-][num]+]`.
If the given sort is a real, then the numeral can be a rational, that is, a string of the form `[num]* / [num]*` .
\param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.
\sa Z3_mk_int
@ -3306,7 +3306,7 @@ extern "C" {
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
/**
\brief Retrieve from \s the unit sequence positioned at position \c index.
\brief Retrieve from \c s the unit sequence positioned at position \c index.
def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
*/

1
src/ast/ast.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include<sstream>
#include<cstring>
#include"ast.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"

3
src/ast/ast.h
View file

@ -117,6 +117,9 @@ public:
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); }
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); }
explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL) {
new (m_symbol) symbol(s);
}
explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
parameter(parameter const&);

72
src/ast/rewriter/seq_rewriter.cpp
View file

@ -329,7 +329,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
switch(f->get_decl_kind()) {
case OP_SEQ_UNIT:
return BR_FAILED;
SASSERT(num_args == 1);
return mk_seq_unit(args[0], result);
case OP_SEQ_EMPTY:
return BR_FAILED;
case OP_RE_PLUS:
@ -351,7 +352,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
SASSERT(num_args == 2);
return mk_re_union(args[0], args[1], result);
case OP_RE_RANGE:
return BR_FAILED;
SASSERT(num_args == 2);
return mk_re_range(args[0], args[1], result);
case OP_RE_INTERSECT:
SASSERT(num_args == 2);
return mk_re_inter(args[0], args[1], result);
@ -434,6 +436,33 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
return BR_FAILED;
}
/*
* (seq.unit (_ BitVector 8)) ==> String constant
*/
br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
sort * s = m().get_sort(e);
bv_util bvu(m());
if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) {
// specifically we want (_ BitVector 8)
rational n_val;
unsigned int n_size;
if (bvu.is_numeral(e, n_val, n_size)) {
if (n_size == 8) {
// convert to string constant
char ch = (char)n_val.get_int32();
TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;);
char s_tmp[2] = {ch, '\0'};
symbol s(s_tmp);
result = m_util.str.mk_string(s);
return BR_DONE;
}
}
}
return BR_FAILED;
}
/*
string + string = string
a + (b + c) = (a + b) + c
@ -1401,6 +1430,39 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
return BR_FAILED;
}
/*
* (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
*/
br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
zstring str_lo, str_hi;
if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {
if (str_lo.length() == 1 && str_hi.length() == 1) {
unsigned int c1 = str_lo[0];
unsigned int c2 = str_hi[0];
if (c1 > c2) {
// exchange c1 and c2
unsigned int tmp = c1;
c2 = c1;
c1 = tmp;
}
zstring s(c1);
expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m());
for (unsigned int ch = c1 + 1; ch <= c2; ++ch) {
zstring s_ch(ch);
expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m());
acc = m_util.re.mk_union(acc, acc2);
}
result = acc;
return BR_REWRITE2;
} else {
m().raise_exception("string constants in re.range must have length 1");
}
}
return BR_FAILED;
}
/*
emp+ = emp
all+ = all
@ -1430,9 +1492,9 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
return BR_DONE;
}
return BR_FAILED;
// result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
// return BR_REWRITE2;
//return BR_FAILED;
result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
return BR_REWRITE2;
}
br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {

2
src/ast/rewriter/seq_rewriter.h
View file

@ -98,6 +98,7 @@ class seq_rewriter {
re2automaton m_re2aut;
expr_ref_vector m_es, m_lhs, m_rhs;
br_status mk_seq_unit(expr* e, expr_ref& result);
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
br_status mk_seq_length(expr* a, expr_ref& result);
br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result);
@ -119,6 +120,7 @@ class seq_rewriter {
br_status mk_re_plus(expr* a, expr_ref& result);
br_status mk_re_opt(expr* a, expr_ref& result);
br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result);
br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r,

2
src/ast/seq_decl_plugin.cpp
View file

@ -831,7 +831,9 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
init();
sort_names.push_back(builtin_name("Seq", SEQ_SORT));
sort_names.push_back(builtin_name("RegEx", RE_SORT));
// SMT-LIB 2.5 compatibility
sort_names.push_back(builtin_name("String", _STRING_SORT));
sort_names.push_back(builtin_name("StringSequence", _STRING_SORT));
}
app* seq_decl_plugin::mk_string(symbol const& s) {

9
src/ast/seq_decl_plugin.h
View file

@ -273,6 +273,15 @@ public:
bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
bool is_string_term(expr const * n) const {
sort * s = get_sort(n);
return u.is_string(s);
}
bool is_non_string_sequence(expr const * n) const {
sort * s = get_sort(n);
return (u.is_seq(s) && !u.is_string(s));
}
MATCH_BINARY(is_concat);
MATCH_UNARY(is_length);

8
src/ast/static_features.cpp
View file

@ -25,6 +25,7 @@ static_features::static_features(ast_manager & m):
m_bvutil(m),
m_arrayutil(m),
m_fpautil(m),
m_sequtil(m),
m_bfid(m.get_basic_family_id()),
m_afid(m.mk_family_id("arith")),
m_lfid(m.mk_family_id("label")),
@ -77,6 +78,8 @@ void static_features::reset() {
m_has_real = false;
m_has_bv = false;
m_has_fpa = false;
m_has_str = false;
m_has_seq_non_str = false;
m_has_arrays = false;
m_arith_k_sum .reset();
m_num_arith_terms = 0;
@ -279,6 +282,11 @@ void static_features::update_core(expr * e) {
m_has_fpa = true;
if (!m_has_arrays && m_arrayutil.is_array(e))
m_has_arrays = true;
if (!m_has_str && m_sequtil.str.is_string_term(e))
m_has_str = true;
if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) {
m_has_seq_non_str = true;
}
if (is_app(e)) {
family_id fid = to_app(e)->get_family_id();
mark_theory(fid);

4
src/ast/static_features.h
View file

@ -24,6 +24,7 @@ Revision History:
#include"bv_decl_plugin.h"
#include"array_decl_plugin.h"
#include"fpa_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"map.h"
struct static_features {
@ -32,6 +33,7 @@ struct static_features {
bv_util m_bvutil;
array_util m_arrayutil;
fpa_util m_fpautil;
seq_util m_sequtil;
family_id m_bfid;
family_id m_afid;
family_id m_lfid;
@ -77,6 +79,8 @@ struct static_features {
bool m_has_real; //
bool m_has_bv; //
bool m_has_fpa; //
bool m_has_str; // has String-typed terms
bool m_has_seq_non_str; // has non-String-typed Sequence terms
bool m_has_arrays; //
rational m_arith_k_sum; // sum of the numerals in arith atoms.
unsigned m_num_arith_terms;

7
src/cmd_context/cmd_context.cpp
View file

@ -249,6 +249,7 @@ protected:
array_util m_arutil;
fpa_util m_futil;
seq_util m_sutil;
datalog::dl_decl_util m_dlutil;
format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) {
@ -277,6 +278,7 @@ public:
virtual array_util & get_arutil() { return m_arutil; }
virtual fpa_util & get_futil() { return m_futil; }
virtual seq_util & get_sutil() { return m_sutil; }
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
virtual bool uses(symbol const & s) const {
return
@ -527,6 +529,9 @@ bool cmd_context::logic_has_fpa() const {
return !has_logic() || smt_logics::logic_has_fpa(m_logic);
}
bool cmd_context::logic_has_str() const {
return !has_logic() || m_logic == "QF_S";
}
bool cmd_context::logic_has_array() const {
return !has_logic() || smt_logics::logic_has_array(m_logic);
@ -568,7 +573,6 @@ void cmd_context::init_manager_core(bool new_manager) {
load_plugin(symbol("seq"), logic_has_seq(), fids);
load_plugin(symbol("fpa"), logic_has_fpa(), fids);
load_plugin(symbol("pb"), logic_has_pb(), fids);
svector<family_id>::iterator it = fids.begin();
svector<family_id>::iterator end = fids.end();
for (; it != end; ++it) {
@ -616,7 +620,6 @@ void cmd_context::init_external_manager() {
init_manager_core(false);
}
bool cmd_context::set_logic(symbol const & s) {
if (has_logic())
throw cmd_exception("the logic has already been set");

1
src/cmd_context/cmd_context.h
View file

@ -257,6 +257,7 @@ protected:
bool logic_has_array() const;
bool logic_has_datatype() const;
bool logic_has_fpa() const;
bool logic_has_str() const;
void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;}

100
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(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;
@ -3310,7 +3408,7 @@ namespace sat {
propagate(false);
++num_resolves;
}
if (scope_lvl() == 1) {
if (false && scope_lvl() == 1) {
break;
}
}

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 << " ";

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);

81
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,18 +138,20 @@ 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();
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());
display_status(r);
if (r != l_true) {
return r;
@ -119,7 +171,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 +203,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 +228,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 +247,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);

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++;
}
}