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 'unstable' into interp

Browse source
This commit is contained in:
Ken McMillan 2013-11-05 12:28:13 -08:00
commit a785a5a4b8
33 changed files with 1995 additions and 1628 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/api_ast.cpp
View file

@ -31,7 +31,7 @@ Revision History:
#include"ast_smt2_pp.h"
#include"th_rewriter.h"
#include"var_subst.h"
#include"expr_substitution.h"
#include"expr_safe_replace.h"
#include"pp.h"
#include"scoped_ctrl_c.h"
#include"cancel_eh.h"
@ -787,17 +787,12 @@ extern "C" {
RETURN_Z3(of_expr(0));
}
}
expr_substitution subst(m);
expr_safe_replace subst(m);
for (unsigned i = 0; i < num_exprs; i++) {
subst.insert(from[i], to[i]);
}
th_rewriter m_rw(m);
m_rw.set_substitution(&subst);
expr_ref new_a(m);
proof_ref pr(m);
m_rw(a, new_a, pr);
subst(a, new_a);
mk_c(c)->save_ast_trail(new_a);
r = new_a.get();
RETURN_Z3(of_expr(r));

6
src/api/python/z3.py
View file

@ -6449,7 +6449,7 @@ class Tactic:
def _to_goal(a):
if isinstance(a, BoolRef):
goal = Goal()
goal = Goal(ctx = a.ctx)
goal.add(a)
return goal
else:
@ -6932,10 +6932,10 @@ def substitute(t, *m):
>>> x = Int('x')
>>> y = Int('y')
>>> substitute(x + 1, (x, y + 1))
2 + y
y + 1 + 1
>>> f = Function('f', IntSort(), IntSort())
>>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
2
1 + 1
"""
if isinstance(m, tuple):
m1 = _get_args(m)

67
src/ast/float_decl_plugin.cpp
View file

@ -85,6 +85,24 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
m_fm.set(val, m_values[to_app(n)->get_decl()->get_parameter(0).get_ext_id()]);
return true;
}
else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_INF)) {
unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
m_fm.mk_ninf(ebits, sbits, val);
return true;
}
else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_INF)) {
unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
m_fm.mk_pinf(ebits, sbits, val);
return true;
}
else if (is_app_of(n, m_family_id, OP_FLOAT_NAN)) {
unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
m_fm.mk_nan(ebits, sbits, val);
return true;
}
return false;
}
@ -457,6 +475,7 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("plusInfinity", OP_FLOAT_PLUS_INF));
op_names.push_back(builtin_name("minusInfinity", OP_FLOAT_MINUS_INF));
op_names.push_back(builtin_name("NaN", OP_FLOAT_NAN));
op_names.push_back(builtin_name("roundNearestTiesToEven", OP_RM_NEAREST_TIES_TO_EVEN));
op_names.push_back(builtin_name("roundNearestTiesToAway", OP_RM_NEAREST_TIES_TO_AWAY));
op_names.push_back(builtin_name("roundTowardPositive", OP_RM_TOWARD_POSITIVE));
@ -468,7 +487,7 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("/", OP_FLOAT_DIV));
op_names.push_back(builtin_name("*", OP_FLOAT_MUL));
op_names.push_back(builtin_name("abs", OP_FLOAT_ABS));
op_names.push_back(builtin_name("abs", OP_FLOAT_ABS));
op_names.push_back(builtin_name("remainder", OP_FLOAT_REM));
op_names.push_back(builtin_name("fusedMA", OP_FLOAT_FUSED_MA));
op_names.push_back(builtin_name("squareRoot", OP_FLOAT_SQRT));
@ -497,6 +516,49 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
if (m_bv_plugin)
op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV));
// We also support draft version 3
op_names.push_back(builtin_name("fp", OP_TO_FLOAT));
op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN));
op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY));
op_names.push_back(builtin_name("RTP", OP_RM_TOWARD_POSITIVE));
op_names.push_back(builtin_name("RTN", OP_RM_TOWARD_NEGATIVE));
op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO));
op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS));
op_names.push_back(builtin_name("fp.neg", OP_FLOAT_UMINUS));
op_names.push_back(builtin_name("fp.add", OP_FLOAT_ADD));
op_names.push_back(builtin_name("fp.sub", OP_FLOAT_SUB));
op_names.push_back(builtin_name("fp.mul", OP_FLOAT_MUL));
op_names.push_back(builtin_name("fp.div", OP_FLOAT_DIV));
op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FUSED_MA));
op_names.push_back(builtin_name("fp.sqrt", OP_FLOAT_SQRT));
op_names.push_back(builtin_name("fp.rem", OP_FLOAT_REM));
op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ));
op_names.push_back(builtin_name("fp.leq", OP_FLOAT_LE));
op_names.push_back(builtin_name("fp.lt", OP_FLOAT_LT));
op_names.push_back(builtin_name("fp.geq", OP_FLOAT_GE));
op_names.push_back(builtin_name("fp.gt", OP_FLOAT_GT));
op_names.push_back(builtin_name("fp.isNormal", OP_FLOAT_IS_NORMAL));
op_names.push_back(builtin_name("fp.isSubnormal", OP_FLOAT_IS_SUBNORMAL));
op_names.push_back(builtin_name("fp.isZero", OP_FLOAT_IS_ZERO));
op_names.push_back(builtin_name("fp.isInfinite", OP_FLOAT_IS_INF));
op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN));
op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));
op_names.push_back(builtin_name("fp.convert", OP_TO_FLOAT));
if (m_bv_plugin) {
// op_names.push_back(builtin_name("fp.fromBv", OP_TO_FLOAT));
// op_names.push_back(builtin_name("fp.fromUBv", OP_TO_FLOAT));
// op_names.push_back(builtin_name("fp.fromSBv", OP_TO_FLOAT));
// op_names.push_back(builtin_name("fp.toUBv", OP_TO_IEEE_BV));
// op_names.push_back(builtin_name("fp.toSBv", OP_TO_IEEE_BV));
}
op_names.push_back(builtin_name("fp.fromReal", OP_TO_FLOAT));
// op_names.push_back(builtin_name("fp.toReal", ?));
}
void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
@ -523,6 +585,9 @@ bool float_decl_plugin::is_value(app * e) const {
case OP_RM_TOWARD_NEGATIVE:
case OP_RM_TOWARD_ZERO:
case OP_FLOAT_VALUE:
case OP_FLOAT_PLUS_INF:
case OP_FLOAT_MINUS_INF:
case OP_FLOAT_NAN:
return true;
case OP_TO_FLOAT:
return m_manager->is_value(e->get_arg(0));

10
src/ast/rewriter/float_rewriter.cpp
View file

@ -354,7 +354,7 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
if (m_util.is_minus_inf(arg1)) {
// -oo < arg2 --> not(arg2 = -oo) and not(arg2 = NaN)
result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2));
return BR_REWRITE2;
return BR_REWRITE3;
}
if (m_util.is_minus_inf(arg2)) {
// arg1 < -oo --> false
@ -369,7 +369,7 @@ br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
if (m_util.is_plus_inf(arg2)) {
// arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN)
result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1));
return BR_REWRITE2;
return BR_REWRITE3;
}
scoped_mpf v1(m_util.fm()), v2(m_util.fm());
@ -490,7 +490,11 @@ br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
scoped_mpf v1(m_util.fm()), v2(m_util.fm());
if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) {
result = (v1 == v2) ? m().mk_true() : m().mk_false();
// Note: == is the floats-equality, here we need normal equality.
result = (m_fm.is_nan(v1) && m_fm.is_nan(v2)) ? m().mk_true() :
(m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1)!=m_fm.sgn(v2)) ? m().mk_false() :
(v1 == v2) ? m().mk_true() :
m().mk_false();
return BR_DONE;
}

2
src/muz/base/dl_context.cpp
View file

@ -581,7 +581,7 @@ namespace datalog {
void context::check_uninterpreted_free(rule_ref& r) {
func_decl* f = 0;
if (r->has_uninterpreted_non_predicates(f)) {
if (r->has_uninterpreted_non_predicates(m, f)) {
std::stringstream stm;
stm << "Uninterpreted '"
<< f->get_name()

19
src/muz/base/dl_rule.cpp
View file

@ -43,6 +43,7 @@ Revision History:
#include"expr_safe_replace.h"
#include"filter_model_converter.h"
#include"scoped_proof.h"
#include"datatype_decl_plugin.h"
namespace datalog {
@ -881,9 +882,12 @@ namespace datalog {
}
struct uninterpreted_function_finder_proc {
ast_manager& m;
datatype_util m_dt;
bool m_found;
func_decl* m_func;
uninterpreted_function_finder_proc() : m_found(false), m_func(0) {}
uninterpreted_function_finder_proc(ast_manager& m):
m(m), m_dt(m), m_found(false), m_func(0) {}
void operator()(var * n) { }
void operator()(quantifier * n) { }
void operator()(app * n) {
@ -891,6 +895,14 @@ namespace datalog {
m_found = true;
m_func = n->get_decl();
}
else if (m_dt.is_accessor(n)) {
sort* s = m.get_sort(n->get_arg(0));
SASSERT(m_dt.is_datatype(s));
if (m_dt.get_datatype_constructors(s)->size() > 1) {
m_found = true;
m_func = n->get_decl();
}
}
}
bool found(func_decl*& f) const { f = m_func; return m_found; }
@ -900,9 +912,9 @@ namespace datalog {
// non-predicates may appear only in the interpreted tail, it is therefore
// sufficient only to check the tail.
//
bool rule::has_uninterpreted_non_predicates(func_decl*& f) const {
bool rule::has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const {
unsigned sz = get_tail_size();
uninterpreted_function_finder_proc proc;
uninterpreted_function_finder_proc proc(m);
expr_mark visited;
for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
for_each_expr(proc, visited, get_tail(i));
@ -910,6 +922,7 @@ namespace datalog {
return proc.found(f);
}
struct quantifier_finder_proc {
bool m_exist;
bool m_univ;

2
src/muz/base/dl_rule.h
View file

@ -293,7 +293,7 @@ namespace datalog {
*/
bool is_in_tail(const func_decl * p, bool only_positive=false) const;
bool has_uninterpreted_non_predicates(func_decl*& f) const;
bool has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const;
void has_quantifiers(bool& existential, bool& universal) const;
bool has_quantifiers() const;
bool has_negation() const;

4
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -1448,6 +1448,10 @@ namespace datalog {
transformer.register_plugin(slice);
m_ctx.transform_rules(transformer);
}
if (m_ctx.get_rules().get_output_predicates().empty()) {
return l_false;
}
m_query_pred = m_ctx.get_rules().get_output_predicate();
m_rules.replace_rules(m_ctx.get_rules());
m_rules.close();

3
src/muz/clp/clp_context.cpp
View file

@ -70,6 +70,9 @@ namespace datalog {
m_goals.reset();
rm.mk_query(query, m_ctx.get_rules());
apply_default_transformation(m_ctx);
if (m_ctx.get_rules().get_output_predicates().empty()) {
return l_false;
}
func_decl* head_decl = m_ctx.get_rules().get_output_predicate();
rule_set& rules = m_ctx.get_rules();
rule_vector const& rv = rules.get_predicate_rules(head_decl);

4
src/muz/pdr/pdr_context.cpp
View file

@ -1123,9 +1123,7 @@ namespace pdr {
n->mk_instantiate(r0, r1, binding);
proof_ref p1(m), p2(m);
p1 = r0->get_proof();
if (!p1) {
r0->display(dctx, std::cout);
}
IF_VERBOSE(0, if (!p1) r0->display(dctx, verbose_stream()););
SASSERT(p1);
pfs[0] = p1;
rls[0] = r1;

18
src/muz/pdr/pdr_util.cpp
View file

@ -112,8 +112,8 @@ namespace pdr {
set_value(e, val);
}
else {
IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";);
TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";);
IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
set_x(e);
}
}
@ -672,7 +672,19 @@ namespace pdr {
eval_array_eq(e, arg1, arg2);
}
else if (is_x(arg1) || is_x(arg2)) {
set_x(e);
expr_ref eq(m), vl(m);
eq = m.mk_eq(arg1, arg2);
m_model->eval(eq, vl);
if (m.is_true(vl)) {
set_bool(e, true);
}
else if (m.is_false(vl)) {
set_bool(e, false);
}
else {
TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) << "\n";);
set_x(e);
}
}
else if (m.is_bool(arg1)) {
bool val = is_true(arg1) == is_true(arg2);

145
src/muz/rel/dl_mk_simple_joins.cpp
View file

@ -47,9 +47,9 @@ namespace datalog {
being notified about it, it will surely see the decrease from length 3 to 2 which
the threshold for rule being counted in this counter.
*/
unsigned m_consumers;
bool m_stratified;
unsigned m_src_stratum;
unsigned m_consumers;
bool m_stratified;
unsigned m_src_stratum;
public:
var_idx_set m_all_nonlocal_vars;
rule_vector m_rules;
@ -57,16 +57,13 @@ namespace datalog {
pair_info() : m_consumers(0), m_stratified(true), m_src_stratum(0) {}
bool can_be_joined() const {
return m_consumers>0;
return m_consumers > 0;
}
cost get_cost() const {
/*if(m_instantiated) {
return std::numeric_limits<cost>::min();
}*/
SASSERT(m_consumers>0);
SASSERT(m_consumers > 0);
cost amortized = m_total_cost/m_consumers;
if(m_stratified) {
if (m_stratified) {
return amortized * ( (amortized>0) ? (1/16.0f) : 16.0f);
}
else {
@ -81,19 +78,20 @@ namespace datalog {
by the time of a call to this function
*/
void add_rule(join_planner & pl, app * t1, app * t2, rule * r,
const var_idx_set & non_local_vars_normalized) {
if(m_rules.empty()) {
m_total_cost = pl.compute_cost(t1, t2);
const var_idx_set & non_local_vars_normalized,
const var_idx_set & non_local_vars) {
if (m_rules.empty()) {
m_total_cost = pl.compute_cost(t1, t2, non_local_vars);
m_src_stratum = std::max(pl.get_stratum(t1->get_decl()), pl.get_stratum(t2->get_decl()));
}
m_rules.push_back(r);
if(pl.m_rules_content.find_core(r)->get_data().m_value.size()>2) {
if (pl.m_rules_content.find(r).size()>2) {
m_consumers++;
}
if(m_stratified) {
if (m_stratified) {
unsigned head_stratum = pl.get_stratum(r->get_decl());
SASSERT(head_stratum>=m_src_stratum);
if(head_stratum==m_src_stratum) {
if (head_stratum==m_src_stratum) {
m_stratified = false;
}
}
@ -105,7 +103,7 @@ namespace datalog {
*/
bool remove_rule(rule * r, unsigned original_length) {
TRUSTME( remove_from_vector(m_rules, r) );
if(original_length>2) {
if (original_length>2) {
SASSERT(m_consumers>0);
m_consumers--;
}
@ -165,7 +163,7 @@ namespace datalog {
SASSERT(is_var(t->get_arg(i)));
var * v = to_var(t->get_arg(i));
unsigned var_idx = v->get_idx();
if(result[res_ofs-var_idx]==0) {
if (result[res_ofs-var_idx]==0) {
result[res_ofs-var_idx]=m.mk_var(next_var, v->get_sort());
next_var++;
}
@ -174,7 +172,7 @@ namespace datalog {
void get_normalizer(app * t1, app * t2, expr_ref_vector & result) const {
SASSERT(result.empty());
if(t1->get_num_args()==0 && t2->get_num_args()==0) {
if (t1->get_num_args()==0 && t2->get_num_args()==0) {
return; //nothing to normalize
}
SASSERT(!t1->is_ground() || !t2->is_ground());
@ -186,14 +184,14 @@ namespace datalog {
var_idx_set::iterator ovend = orig_var_set.end();
for(; ovit!=ovend; ++ovit) {
unsigned var_idx = *ovit;
if(var_idx>max_var_idx) {
if (var_idx>max_var_idx) {
max_var_idx = var_idx;
}
}
}
if(t1->get_decl()!=t2->get_decl()) {
if(t1->get_decl()->get_id()<t2->get_decl()->get_id()) {
if (t1->get_decl()!=t2->get_decl()) {
if (t1->get_decl()->get_id()<t2->get_decl()->get_id()) {
std::swap(t1, t2);
}
}
@ -207,9 +205,9 @@ namespace datalog {
//so the only literals which appear in pairs are the ones that contain only variables.
var * v1 = to_var(t1->get_arg(i));
var * v2 = to_var(t2->get_arg(i));
if(v1->get_sort()!=v2->get_sort()) {
if (v1->get_sort()!=v2->get_sort()) {
//different sorts mean we can distinguish the two terms
if(v1->get_sort()->get_id()<v2->get_sort()->get_id()) {
if (v1->get_sort()->get_id()<v2->get_sort()->get_id()) {
std::swap(t1, t2);
}
break;
@ -221,9 +219,9 @@ namespace datalog {
SASSERT(norm1[v1_idx]==-1);
SASSERT(norm2[v2_idx]==-1);
if(norm2[v1_idx]!=norm1[v2_idx]) {
if (norm2[v1_idx]!=norm1[v2_idx]) {
//now we can distinguish the two terms
if(norm2[v1_idx]<norm1[v2_idx]) {
if (norm2[v1_idx]<norm1[v2_idx]) {
std::swap(t1, t2);
}
break;
@ -250,7 +248,7 @@ namespace datalog {
m_var_subst(t2, norm_subst.size(), norm_subst.c_ptr(), t2n_ref);
app * t1n = to_app(t1n_ref);
app * t2n = to_app(t2n_ref);
if(t1n>t2n) {
if (t1n>t2n) {
std::swap(t1n, t2n);
}
m_pinned.push_back(t1n);
@ -274,12 +272,10 @@ namespace datalog {
by the time of a call to this function
*/
void register_pair(app * t1, app * t2, rule * r, const var_idx_set & non_local_vars) {
TRACE("dl", tout << mk_pp(t1, m) << " " << mk_pp(t2, m) << "\n";
r->display(m_context, tout); tout << "\n";);
SASSERT(t1!=t2);
cost_map::entry * e = m_costs.insert_if_not_there2(get_key(t1, t2), 0);
pair_info * & ptr_inf = e->get_data().m_value;
if(ptr_inf==0) {
if (ptr_inf==0) {
ptr_inf = alloc(pair_info);
}
pair_info & inf = *ptr_inf;
@ -288,25 +284,30 @@ namespace datalog {
get_normalizer(t1, t2, normalizer);
unsigned norm_ofs = normalizer.size()-1;
var_idx_set normalized_vars;
var_idx_set::iterator vit = non_local_vars.begin();
var_idx_set::iterator vit = non_local_vars.begin();
var_idx_set::iterator vend = non_local_vars.end();
for(; vit!=vend; ++vit) {
unsigned norm_var = to_var(normalizer.get(norm_ofs-*vit))->get_idx();
normalized_vars.insert(norm_var);
}
inf.add_rule(*this, t1, t2, r, normalized_vars);
inf.add_rule(*this, t1, t2, r, normalized_vars, non_local_vars);
TRACE("dl", tout << mk_pp(t1, m) << " " << mk_pp(t2, m) << " ";
vit = non_local_vars.begin();
for (; vit != vend; ++vit) tout << *vit << " ";
tout << "\n";
r->display(m_context, tout);
if (inf.can_be_joined()) tout << "cost: " << inf.get_cost() << "\n";);
}
pair_info & get_pair(app_pair key) const {
cost_map::entry * e = m_costs.find_core(key);
SASSERT(e);
return *e->get_data().m_value;
return *m_costs.find(key);
}
void remove_rule_from_pair(app_pair key, rule * r, unsigned original_len) {
pair_info * ptr = &get_pair(key);
if(ptr->remove_rule(r, original_len)) {
if (ptr->remove_rule(r, original_len)) {
SASSERT(ptr->m_rules.empty());
m_costs.remove(key);
dealloc(ptr);
@ -349,7 +350,7 @@ namespace datalog {
unsigned n=t->get_num_args();
for(unsigned i=0; i<n; i++) {
var * v=to_var(t->get_arg(i));
if(v->get_idx()==var_idx) {
if (v->get_idx()==var_idx) {
args.push_back(v);
domain.push_back(m.get_sort(v));
return true;
@ -375,7 +376,7 @@ namespace datalog {
unsigned var_idx=*ovit;
bool found=extract_argument_info(var_idx, t1, args, domain);
if(!found) {
if (!found) {
found=extract_argument_info(var_idx, t2, args, domain);
}
SASSERT(found);
@ -389,7 +390,7 @@ namespace datalog {
func_decl* parent_head = one_parent->get_decl();
const char * one_parent_name = parent_head->get_name().bare_str();
std::string parent_name;
if(inf.m_rules.size()>1) {
if (inf.m_rules.size()>1) {
parent_name = one_parent_name + std::string("_and_") + to_string(inf.m_rules.size()-1);
}
else {
@ -443,7 +444,7 @@ namespace datalog {
}
//remove edges between surviving tails and removed tails
for(unsigned i=0; i<len; i++) {
if(added_tails.contains(rule_content[i])) {
if (added_tails.contains(rule_content[i])) {
continue;
}
for(unsigned ri=0; ri<rt_sz; ri++) {
@ -452,7 +453,7 @@ namespace datalog {
}
}
if(len==1) {
if (len==1) {
return;
}
@ -480,7 +481,7 @@ namespace datalog {
for(unsigned i=0; i<len; i++) {
app * o_tail = rule_content[i]; //other tail
if(added_tails.contains(o_tail)) {
if (added_tails.contains(o_tail)) {
//this avoids adding edges between new tails twice
continue;
}
@ -503,9 +504,9 @@ namespace datalog {
void apply_binary_rule(rule * r, app_pair pair_key, app * t_new) {
app * t1 = pair_key.first;
app * t2 = pair_key.second;
ptr_vector<app> & rule_content = m_rules_content.find_core(r)->get_data().m_value;
ptr_vector<app> & rule_content = m_rules_content.find(r);
unsigned len = rule_content.size();
if(len==1) {
if (len==1) {
return;
}
@ -515,16 +516,16 @@ namespace datalog {
ptr_vector<app> added_tails;
for(unsigned i1=0; i1<len; i1++) {
app * rt1 = rule_content[i1];
if(rt1->get_decl()!=t1_pred) {
if (rt1->get_decl()!=t1_pred) {
continue;
}
unsigned i2start = (t1_pred==t2_pred) ? (i1+1) : 0;
for(unsigned i2=i2start; i2<len; i2++) {
app * rt2 = rule_content[i2];
if(i1==i2 || rt2->get_decl()!=t2_pred) {
if (i1==i2 || rt2->get_decl()!=t2_pred) {
continue;
}
if(get_key(rt1, rt2)!=pair_key) {
if (get_key(rt1, rt2)!=pair_key) {
continue;
}
expr_ref_vector normalizer(m);
@ -558,7 +559,7 @@ namespace datalog {
relation_sort sort = pred->get_domain(arg_index);
return static_cast<cost>(m_context.get_sort_size_estimate(sort));
//unsigned sz;
//if(!m_context.get_sort_size(sort, sz)) {
//if (!m_context.get_sort_size(sort, sz)) {
// sz=UINT_MAX;
//}
//return static_cast<cost>(sz);
@ -576,15 +577,15 @@ namespace datalog {
return cost(1);
}
relation_manager& rm = rel->get_rmanager();
if( (m_context.saturation_was_run() && rm.try_get_relation(pred))
if ( (m_context.saturation_was_run() && rm.try_get_relation(pred))
|| rm.is_saturated(pred)) {
SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist
unsigned rel_size_int = rel->get_relation(pred).get_size_estimate_rows();
if(rel_size_int!=0) {
if (rel_size_int!=0) {
cost rel_size = static_cast<cost>(rel_size_int);
cost curr_size = rel_size;
for(unsigned i=0; i<n; i++) {
if(!is_var(t->get_arg(i))) {
if (!is_var(t->get_arg(i))) {
curr_size /= get_domain_size(pred, i);
}
}
@ -593,40 +594,58 @@ namespace datalog {
}
cost res = 1;
for(unsigned i=0; i<n; i++) {
if(is_var(t->get_arg(i))) {
if (is_var(t->get_arg(i))) {
res *= get_domain_size(pred, i);
}
}
return res;
}
cost compute_cost(app * t1, app * t2) const {
cost compute_cost(app * t1, app * t2, const var_idx_set & non_local_vars) const {
func_decl * t1_pred = t1->get_decl();
func_decl * t2_pred = t2->get_decl();
cost inters_size = 1;
variable_intersection vi(m_context.get_manager());
vi.populate(t1, t2);
unsigned n = vi.size();
// remove contributions from joined columns.
for(unsigned i=0; i<n; i++) {
unsigned arg_index1, arg_index2;
vi.get(i, arg_index1, arg_index2);
inters_size *= get_domain_size(t1_pred, arg_index1);
SASSERT(is_var(t1->get_arg(arg_index1)));
if (non_local_vars.contains(to_var(t1->get_arg(arg_index1))->get_idx())) {
inters_size *= get_domain_size(t1_pred, arg_index1);
}
//joined arguments must have the same domain
SASSERT(get_domain_size(t1_pred, arg_index1)==get_domain_size(t2_pred, arg_index2));
}
cost res = estimate_size(t1)*estimate_size(t2)/(inters_size*inters_size);
// remove contributions from projected columns.
for (unsigned i = 0; i < t1->get_num_args(); ++i) {
if (is_var(t1->get_arg(i)) &&
!non_local_vars.contains(to_var(t1->get_arg(i))->get_idx())) {
inters_size *= get_domain_size(t1_pred, i);
}
}
for (unsigned i = 0; i < t2->get_num_args(); ++i) {
if (is_var(t2->get_arg(i)) &&
!non_local_vars.contains(to_var(t2->get_arg(i))->get_idx())) {
inters_size *= get_domain_size(t2_pred, i);
}
}
cost res = estimate_size(t1)*estimate_size(t2)/ inters_size; // (inters_size*inters_size);
//cost res = -inters_size;
/*unsigned t1_strat = get_stratum(t1_pred);
SASSERT(t1_strat<=m_head_stratum);
if(t1_strat<m_head_stratum) {
if (t1_strat<m_head_stratum) {
unsigned t2_strat = get_stratum(t2_pred);
SASSERT(t2_strat<=m_head_stratum);
if(t2_strat<m_head_stratum) {
if (t2_strat<m_head_stratum) {
//the rule of this predicates would depend on predicates
//in lower stratum than the head, which is a good thing, since
//then the rule code will not need to appear in a loop
if(res>0) {
if (res>0) {
res /= 2;
}
else {
@ -653,17 +672,17 @@ namespace datalog {
for(; it!=end; ++it) {
app_pair key = it->m_key;
pair_info & inf = *it->m_value;
if(!inf.can_be_joined()) {
if (!inf.can_be_joined()) {
continue;
}
cost c = inf.get_cost();
if(!found || c<best_cost) {
if (!found || c<best_cost) {
found = true;
best_cost = c;
best = key;
}
}
if(!found) {
if (!found) {
return false;
}
p=best;
@ -684,7 +703,7 @@ namespace datalog {
join_pair(selected);
}
if(m_modified_rules.empty()) {
if (m_modified_rules.empty()) {
return 0;
}
rule_set * result = alloc(rule_set, m_context);
@ -694,7 +713,7 @@ namespace datalog {
rule * orig_r = rcit->m_key;
ptr_vector<app> content = rcit->m_value;
SASSERT(content.size()<=2);
if(content.size()==orig_r->get_positive_tail_size()) {
if (content.size()==orig_r->get_positive_tail_size()) {
//rule did not change
result->add_rule(orig_r);
continue;
@ -728,7 +747,7 @@ namespace datalog {
rule_set * mk_simple_joins::operator()(rule_set const & source) {
rule_set rs_aux_copy(m_context);
rs_aux_copy.replace_rules(source);
if(!rs_aux_copy.is_closed()) {
if (!rs_aux_copy.is_closed()) {
rs_aux_copy.close();
}

127
src/muz/transforms/dl_mk_array_blast.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include "dl_mk_array_blast.h"
#include "qe_util.h"
#include "scoped_proof.h"
namespace datalog {
@ -31,7 +32,6 @@ namespace datalog {
rm(ctx.get_rule_manager()),
m_rewriter(m, m_params),
m_simplifier(ctx),
m_sub(m),
m_next_var(0) {
m_params.set_bool("expand_select_store",true);
m_rewriter.updt_params(m_params);
@ -82,7 +82,6 @@ namespace datalog {
return false;
}
if (v) {
m_sub.insert(e, v);
m_defs.insert(e, to_var(v));
}
else {
@ -92,71 +91,113 @@ namespace datalog {
m_next_var = vars.size() + 1;
}
v = m.mk_var(m_next_var, m.get_sort(e));
m_sub.insert(e, v);
m_defs.insert(e, v);
++m_next_var;
}
return true;
}
bool mk_array_blast::is_select_eq_var(expr* e, app*& s, var*& v) const {
expr* x, *y;
if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) {
if (a.is_select(y)) {
std::swap(x,y);
}
if (a.is_select(x) && is_var(y)) {
s = to_app(x);
v = to_var(y);
return true;
}
}
return false;
}
bool mk_array_blast::ackermanize(rule const& r, expr_ref& body, expr_ref& head) {
expr_ref_vector conjs(m);
expr_ref_vector conjs(m), trail(m);
qe::flatten_and(body, conjs);
m_defs.reset();
m_sub.reset();
m_next_var = 0;
ptr_vector<expr> todo;
todo.push_back(head);
obj_map<expr, expr*> cache;
ptr_vector<expr> args;
app_ref e1(m);
app* s;
var* v;
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
expr* x, *y;
if (m.is_eq(e, x, y) || m.is_iff(e, x, y)) {
if (a.is_select(y)) {
std::swap(x,y);
}
if (a.is_select(x) && is_var(y)) {
if (!insert_def(r, to_app(x), to_var(y))) {
return false;
}
}
if (is_select_eq_var(e, s, v)) {
todo.append(s->get_num_args(), s->get_args());
}
if (a.is_select(e) && !insert_def(r, to_app(e), 0)) {
return false;
else {
todo.push_back(e);
}
todo.push_back(e);
}
// now make sure to cover all occurrences.
ast_mark mark;
while (!todo.empty()) {
expr* e = todo.back();
todo.pop_back();
if (mark.is_marked(e)) {
if (cache.contains(e)) {
todo.pop_back();
continue;
}
mark.mark(e, true);
if (is_var(e)) {
cache.insert(e, e);
todo.pop_back();
continue;
}
if (!is_app(e)) {
return false;
}
app* ap = to_app(e);
if (a.is_select(ap) && !m_defs.contains(ap)) {
if (!insert_def(r, ap, 0)) {
return false;
bool valid = true;
args.reset();
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
expr* arg;
if (cache.find(ap->get_arg(i), arg)) {
args.push_back(arg);
}
else {
todo.push_back(ap->get_arg(i));
valid = false;
}
}
if (a.is_select(e)) {
get_select_args(e, todo);
continue;
if (valid) {
todo.pop_back();
e1 = m.mk_app(ap->get_decl(), args.size(), args.c_ptr());
trail.push_back(e1);
if (a.is_select(ap)) {
if (m_defs.find(e1, v)) {
cache.insert(e, v);
}
else if (!insert_def(r, e1, 0)) {
return false;
}
else {
cache.insert(e, m_defs.find(e1));
}
}
else {
cache.insert(e, e1);
}
}
}
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
if (is_select_eq_var(e, s, v)) {
args.reset();
for (unsigned j = 0; j < s->get_num_args(); ++j) {
args.push_back(cache.find(s->get_arg(j)));
}
e1 = m.mk_app(s->get_decl(), args.size(), args.c_ptr());
if (!m_defs.contains(e1) && !insert_def(r, e1, v)) {
return false;
}
conjs[i] = m.mk_eq(v, m_defs.find(e1));
}
for (unsigned i = 0; i < ap->get_num_args(); ++i) {
todo.push_back(ap->get_arg(i));
else {
conjs[i] = cache.find(e);
}
}
m_sub(body);
m_sub(head);
conjs.reset();
// perform the Ackermann reduction by creating implications
// i1 = i2 => val1 = val2 for each equality pair:
@ -171,6 +212,7 @@ namespace datalog {
for (; it2 != end; ++it2) {
app* a2 = it2->m_key;
var* v2 = it2->m_value;
TRACE("dl", tout << mk_pp(a1, m) << " " << mk_pp(a2, m) << "\n";);
if (get_select(a1) != get_select(a2)) {
continue;
}
@ -184,10 +226,7 @@ namespace datalog {
conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.c_ptr()), m.mk_eq(v1, v2)));
}
}
if (!conjs.empty()) {
conjs.push_back(body);
body = m.mk_and(conjs.size(), conjs.c_ptr());
}
body = m.mk_and(conjs.size(), conjs.c_ptr());
m_rewriter(body);
return true;
}
@ -232,7 +271,7 @@ namespace datalog {
}
}
expr_ref fml2(m), body(m), head(m);
expr_ref fml1(m), fml2(m), body(m), head(m);
body = m.mk_and(new_conjs.size(), new_conjs.c_ptr());
head = r.get_head();
sub(body);
@ -249,9 +288,17 @@ namespace datalog {
proof_ref p(m);
rule_set new_rules(m_ctx);
rm.mk_rule(fml2, p, new_rules, r.name());
rule_ref new_rule(rm);
if (m_simplifier.transform_rule(new_rules.last(), new_rule)) {
if (r.get_proof()) {
scoped_proof _sc(m);
r.to_formula(fml1);
p = m.mk_rewrite(fml1, fml2);
p = m.mk_modus_ponens(r.get_proof(), p);
new_rule->set_proof(m, p);
}
rules.add_rule(new_rule.get());
rm.mk_rule_rewrite_proof(r, *new_rule.get());
TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n"););

3
src/muz/transforms/dl_mk_array_blast.h
View file

@ -44,7 +44,6 @@ namespace datalog {
mk_interp_tail_simplifier m_simplifier;
defs_t m_defs;
expr_safe_replace m_sub;
unsigned m_next_var;
bool blast(rule& r, rule_set& new_rules);
@ -59,6 +58,8 @@ namespace datalog {
bool insert_def(rule const& r, app* e, var* v);
bool is_select_eq_var(expr* e, app*& s, var*& v) const;
public:
/**
\brief Create rule transformer that removes array stores and selects by ackermannization.

4
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "filter_model_converter.h"
#include "dl_mk_interp_tail_simplifier.h"
#include "fixedpoint_params.hpp"
#include "scoped_proof.h"
namespace datalog {
@ -268,7 +269,8 @@ namespace datalog {
r->to_formula(fml);
if (blast(r, fml)) {
proof_ref pr(m);
if (m_context.generate_proof_trace()) {
if (r->get_proof()) {
scoped_proof _sc(m);
pr = m.mk_asserted(fml); // loses original proof of r.
}
// TODO add logic for pc:

1
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -341,7 +341,6 @@ namespace datalog {
}
head = mk_head(source, *result, r.get_head(), cnt);
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head);
rule_ref_vector added_rules(rm);
proof_ref pr(m);
rm.mk_rule(fml, pr, *result);
TRACE("dl", result->last()->display(m_ctx, tout););

144
src/sat/sat_simplifier.cpp
View file

@ -9,7 +9,7 @@ Abstract:
SAT simplification procedures that use a "full" occurrence list:
Subsumption, Blocked Clause Removal, Variable Elimination, ...
Author:
@ -54,21 +54,21 @@ namespace sat {
m_use_list[l2.index()].erase(c);
}
}
simplifier::simplifier(solver & _s, params_ref const & p):
s(_s),
m_num_calls(0) {
updt_params(p);
reset_statistics();
}
simplifier::~simplifier() {
}
inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
inline watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); }
inline bool simplifier::is_external(bool_var v) const { return s.is_external(v); }
inline bool simplifier::was_eliminated(bool_var v) const { return s.was_eliminated(v); }
@ -78,7 +78,7 @@ namespace sat {
lbool simplifier::value(literal l) const { return s.value(l); }
inline void simplifier::checkpoint() { s.checkpoint(); }
void simplifier::register_clauses(clause_vector & cs) {
std::stable_sort(cs.begin(), cs.end(), size_lt());
clause_vector::iterator it = cs.begin();
@ -117,7 +117,7 @@ namespace sat {
SASSERT(s.get_wlist(~l1).contains(watched(l2, learned)));
s.get_wlist(~l1).erase(watched(l2, learned));
}
void simplifier::init_visited() {
m_visited.reset();
m_visited.resize(2*s.num_vars(), false);
@ -155,7 +155,7 @@ namespace sat {
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
elim_blocked_clauses();
if (!learned)
m_num_calls++;
@ -180,6 +180,7 @@ namespace sat {
bool vars_eliminated = m_num_elim_vars > old_num_elim_vars;
if (!m_need_cleanup) {
TRACE("after_simplifier", tout << "skipping cleanup...\n";);
if (vars_eliminated) {
// must remove learned clauses with eliminated variables
cleanup_clauses(s.m_learned, true, true, learned_in_use_lists);
@ -189,6 +190,7 @@ namespace sat {
free_memory();
return;
}
TRACE("after_simplifier", tout << "cleanning watches...\n";);
cleanup_watches();
cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists);
cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
@ -234,7 +236,7 @@ namespace sat {
s.del_clause(c);
continue;
}
if (learned && vars_eliminated) {
unsigned sz = c.size();
unsigned i;
@ -293,7 +295,7 @@ namespace sat {
mark_visited(c[i]);
}
}
void simplifier::unmark_all(clause const & c) {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++)
@ -325,7 +327,7 @@ namespace sat {
*/
bool simplifier::subsumes1(clause const & c1, clause const & c2, literal & l) {
unsigned sz2 = c2.size();
for (unsigned i = 0; i < sz2; i++)
for (unsigned i = 0; i < sz2; i++)
mark_visited(c2[i]);
bool r = true;
@ -344,7 +346,7 @@ namespace sat {
}
}
for (unsigned i = 0; i < sz2; i++)
for (unsigned i = 0; i < sz2; i++)
unmark_visited(c2[i]);
return r;
}
@ -353,7 +355,7 @@ namespace sat {
\brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1.
The collections is populated using the use list of target.
*/
void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits,
void simplifier::collect_subsumed1_core(clause const & c1, clause_vector & out, literal_vector & out_lits,
literal target) {
clause_use_list const & cs = m_use_list.get(target);
clause_use_list::iterator it = cs.mk_iterator();
@ -362,7 +364,7 @@ namespace sat {
CTRACE("resolution_bug", c2.was_removed(), tout << "clause has been removed:\n" << c2 << "\n";);
SASSERT(!c2.was_removed());
if (&c2 != &c1 &&
c1.size() <= c2.size() &&
c1.size() <= c2.size() &&
approx_subset(c1.approx(), c2.approx())) {
m_sub_counter -= c1.size() + c2.size();
literal l;
@ -373,7 +375,7 @@ namespace sat {
}
it.next();
}
}
}
/**
\brief Return the clauses subsumed by c1 and the clauses that can be subsumed resolved using c1.
@ -400,12 +402,12 @@ namespace sat {
if (*l_it == null_literal) {
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_learned();
c1.unset_learned();
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
remove_clause(c2);
m_num_subsumed++;
}
else {
else if (!c2.was_removed()) {
// subsumption resolution
TRACE("subsumption_resolution", tout << c1 << " sub-ref(" << *l_it << ") " << c2 << "\n";);
elim_lit(c2, *l_it);
@ -447,9 +449,9 @@ namespace sat {
*/
bool simplifier::subsumes0(clause const & c1, clause const & c2) {
unsigned sz2 = c2.size();
for (unsigned i = 0; i < sz2; i++)
for (unsigned i = 0; i < sz2; i++)
mark_visited(c2[i]);
bool r = true;
unsigned sz1 = c1.size();
for (unsigned i = 0; i < sz1; i++) {
@ -459,12 +461,12 @@ namespace sat {
}
}
for (unsigned i = 0; i < sz2; i++)
for (unsigned i = 0; i < sz2; i++)
unmark_visited(c2[i]);
return r;
}
/**
\brief Collect the clauses subsumed by c1 (using the occurrence list of target).
*/
@ -475,7 +477,7 @@ namespace sat {
clause & c2 = it.curr();
SASSERT(!c2.was_removed());
if (&c2 != &c1 &&
c1.size() <= c2.size() &&
c1.size() <= c2.size() &&
approx_subset(c1.approx(), c2.approx())) {
m_sub_counter -= c1.size() + c2.size();
if (subsumes0(c1, c2)) {
@ -485,7 +487,7 @@ namespace sat {
it.next();
}
}
/**
\brief Collect the clauses subsumed by c1
*/
@ -493,8 +495,8 @@ namespace sat {
literal l = get_min_occ_var0(c1);
collect_subsumed0_core(c1, out, l);
}
/**
\brief Perform backward subsumption using c1.
*/
@ -507,16 +509,16 @@ namespace sat {
clause & c2 = *(*it);
// c2 was subsumed
if (c1.is_learned() && !c2.is_learned())
c1.unset_learned();
c1.unset_learned();
TRACE("subsumption", tout << c1 << " subsumed " << c2 << "\n";);
remove_clause(c2);
m_num_subsumed++;
}
}
/**
\brief Eliminate false literals from c, and update occurrence lists
Return true if the clause is satisfied
*/
bool simplifier::cleanup_clause(clause & c, bool in_use_list) {
@ -666,7 +668,7 @@ namespace sat {
back_subsumption1(c);
if (w.is_learned() && !c.is_learned()) {
SASSERT(wlist[j] == w);
TRACE("mark_not_learned_bug",
TRACE("mark_not_learned_bug",
tout << "marking as not learned: " << l2 << " " << wlist[j].is_learned() << "\n";);
wlist[j].mark_not_learned();
mark_as_not_learned_core(get_wlist(~l2), l);
@ -735,7 +737,7 @@ namespace sat {
continue;
}
if (it2->get_literal() == last_lit) {
TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx)
TRACE("subsumption", tout << "eliminating: " << ~to_literal(l_idx)
<< " " << it2->get_literal() << "\n";);
elim++;
}
@ -762,12 +764,12 @@ namespace sat {
m_num_sub_res(s.m_num_sub_res) {
m_watch.start();
}
~subsumption_report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
IF_VERBOSE(SAT_VB_LVL,
verbose_stream() << " (sat-subsumer :subsumed "
<< (m_simplifier.m_num_subsumed - m_num_subsumed)
<< (m_simplifier.m_num_subsumed - m_num_subsumed)
<< " :subsumption-resolution " << (m_simplifier.m_num_sub_res - m_num_sub_res)
<< " :threshold " << m_simplifier.m_sub_counter
<< mem_stat()
@ -847,12 +849,12 @@ namespace sat {
vector<watch_list> const & m_watches;
public:
literal_lt(use_list const & l, vector<watch_list> const & ws):m_use_list(l), m_watches(ws) {}
unsigned weight(unsigned l_idx) const {
return 2*m_use_list.get(~to_literal(l_idx)).size() + m_watches[l_idx].size();
}
bool operator()(unsigned l_idx1, unsigned l_idx2) const {
bool operator()(unsigned l_idx1, unsigned l_idx2) const {
return weight(l_idx1) < weight(l_idx2);
}
};
@ -861,9 +863,9 @@ namespace sat {
heap<literal_lt> m_queue;
public:
queue(use_list const & l, vector<watch_list> const & ws):m_queue(128, literal_lt(l, ws)) {}
void insert(literal l) {
void insert(literal l) {
unsigned idx = l.index();
m_queue.reserve(idx + 1);
m_queue.reserve(idx + 1);
SASSERT(!m_queue.contains(idx));
m_queue.insert(idx);
}
@ -877,14 +879,14 @@ namespace sat {
literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
bool empty() const { return m_queue.empty(); }
};
simplifier & s;
int m_counter;
model_converter & mc;
queue m_queue;
clause_vector m_to_remove;
blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l,
blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l,
vector<watch_list> & wlist):
s(_s),
m_counter(limit),
@ -946,7 +948,7 @@ namespace sat {
clause_vector::iterator it = m_to_remove.begin();
clause_vector::iterator end = m_to_remove.end();
for (; it != end; ++it) {
s.remove_clause(*(*it));
s.remove_clause(*(*it));
}
}
{
@ -1025,12 +1027,12 @@ namespace sat {
m_num_blocked_clauses(s.m_num_blocked_clauses) {
m_watch.start();
}
~blocked_cls_report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
IF_VERBOSE(SAT_VB_LVL,
verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses "
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
<< mem_stat()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
}
@ -1062,8 +1064,8 @@ namespace sat {
unsigned num_neg = m_use_list.get(neg_l).size();
unsigned num_bin_pos = get_num_non_learned_bin(pos_l);
unsigned num_bin_neg = get_num_non_learned_bin(neg_l);
unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos;
CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos
unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos;
CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos
<< " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";);
return cost;
}
@ -1071,7 +1073,7 @@ namespace sat {
typedef std::pair<bool_var, unsigned> bool_var_and_cost;
struct bool_var_and_cost_lt {
bool operator()(bool_var_and_cost const & p1, bool_var_and_cost const & p2) const { return p1.second < p2.second; }
bool operator()(bool_var_and_cost const & p1, bool_var_and_cost const & p2) const { return p1.second < p2.second; }
};
void simplifier::order_vars_for_elim(bool_var_vector & r) {
@ -1104,7 +1106,7 @@ namespace sat {
r.push_back(it2->first);
}
}
/**
\brief Collect clauses and binary clauses containing l.
*/
@ -1116,7 +1118,7 @@ namespace sat {
SASSERT(r.back().size() == it.curr().size());
it.next();
}
watch_list & wlist = get_wlist(~l);
watch_list::iterator it2 = wlist.begin();
watch_list::iterator end2 = wlist.end();
@ -1129,7 +1131,7 @@ namespace sat {
}
/**
\brief Resolve clauses c1 and c2.
\brief Resolve clauses c1 and c2.
c1 must contain l.
c2 must contain ~l.
Store result in r.
@ -1149,7 +1151,7 @@ namespace sat {
m_visited[l2.index()] = true;
r.push_back(l2);
}
literal not_l = ~l;
sz = c2.size();
m_elim_counter -= sz;
@ -1164,7 +1166,7 @@ namespace sat {
if (!m_visited[l2.index()])
r.push_back(l2);
}
sz = c1.size();
for (unsigned i = 0; i < sz; i++) {
literal l2 = c1[i];
@ -1200,7 +1202,7 @@ namespace sat {
break;
}
}
CTRACE("resolve_bug", it2 == end2,
CTRACE("resolve_bug", it2 == end2,
tout << ~l1 << " -> ";
display(tout, s.m_cls_allocator, wlist1); tout << "\n" << ~l2 << " -> ";
display(tout, s.m_cls_allocator, wlist2); tout << "\n";);
@ -1262,7 +1264,7 @@ namespace sat {
TRACE("resolution_bug", tout << "processing: " << v << "\n";);
if (value(v) != l_undef)
return false;
literal pos_l(v, false);
literal neg_l(v, true);
unsigned num_bin_pos = get_num_non_learned_bin(pos_l);
@ -1274,12 +1276,12 @@ namespace sat {
m_elim_counter -= num_pos + num_neg;
TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
if (num_pos >= m_res_occ_cutoff && num_neg >= m_res_occ_cutoff)
return false;
unsigned before_lits = num_bin_pos*2 + num_bin_neg*2;
{
clause_use_list::iterator it = pos_occs.mk_iterator();
while (!it.at_end()) {
@ -1287,7 +1289,7 @@ namespace sat {
it.next();
}
}
{
clause_use_list::iterator it2 = neg_occs.mk_iterator();
while (!it2.at_end()) {
@ -1297,23 +1299,23 @@ namespace sat {
}
TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << " before_lits: " << before_lits << "\n";);
if (num_pos >= m_res_occ_cutoff3 && num_neg >= m_res_occ_cutoff3 && before_lits > m_res_lit_cutoff3 && s.m_clauses.size() > m_res_cls_cutoff2)
return false;
if (num_pos >= m_res_occ_cutoff2 && num_neg >= m_res_occ_cutoff2 && before_lits > m_res_lit_cutoff2 &&
if (num_pos >= m_res_occ_cutoff2 && num_neg >= m_res_occ_cutoff2 && before_lits > m_res_lit_cutoff2 &&
s.m_clauses.size() > m_res_cls_cutoff1 && s.m_clauses.size() <= m_res_cls_cutoff2)
return false;
if (num_pos >= m_res_occ_cutoff1 && num_neg >= m_res_occ_cutoff1 && before_lits > m_res_lit_cutoff1 &&
if (num_pos >= m_res_occ_cutoff1 && num_neg >= m_res_occ_cutoff1 && before_lits > m_res_lit_cutoff1 &&
s.m_clauses.size() <= m_res_cls_cutoff1)
return false;
m_pos_cls.reset();
m_neg_cls.reset();
collect_clauses(pos_l, m_pos_cls);
collect_clauses(neg_l, m_neg_cls);
m_elim_counter -= num_pos * num_neg + before_lits;
TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
unsigned before_clauses = num_pos + num_neg;
unsigned after_clauses = 0;
@ -1350,7 +1352,7 @@ namespace sat {
neg_occs.reset();
m_elim_counter -= num_pos * num_neg + before_lits;
it1 = m_pos_cls.begin();
end1 = m_pos_cls.end();
for (; it1 != end1; ++it1) {
@ -1393,7 +1395,7 @@ namespace sat {
return true;
}
}
return true;
}
@ -1406,10 +1408,10 @@ namespace sat {
m_num_elim_vars(s.m_num_elim_vars) {
m_watch.start();
}
~elim_var_report() {
m_watch.stop();
IF_VERBOSE(SAT_VB_LVL,
IF_VERBOSE(SAT_VB_LVL,
verbose_stream() << " (sat-resolution :elim-bool-vars "
<< (m_simplifier.m_num_elim_vars - m_num_elim_vars)
<< " :threshold " << m_simplifier.m_elim_counter
@ -1417,12 +1419,12 @@ namespace sat {
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
}
};
void simplifier::elim_vars() {
elim_var_report rpt(*this);
bool_var_vector vars;
order_vars_for_elim(vars);
bool_var_vector::iterator it = vars.begin();
bool_var_vector::iterator end = vars.end();
for (; it != end; ++it) {
@ -1463,7 +1465,7 @@ namespace sat {
void simplifier::collect_param_descrs(param_descrs & r) {
sat_simplifier_params::collect_param_descrs(r);
}
void simplifier::collect_statistics(statistics & st) {
st.update("subsumed", m_num_subsumed);
st.update("subsumption resolution", m_num_sub_res);
@ -1471,7 +1473,7 @@ namespace sat {
st.update("elim bool vars", m_num_elim_vars);
st.update("elim blocked clauses", m_num_blocked_clauses);
}
void simplifier::reset_statistics() {
m_num_blocked_clauses = 0;
m_num_subsumed = 0;

227
src/sat/sat_solver.cpp
View file

@ -27,7 +27,7 @@ Revision History:
// define to create a copy of the solver before starting the search
// useful for checking models
// #define CLONE_BEFORE_SOLVING
namespace sat {
solver::solver(params_ref const & p, extension * ext):
@ -103,7 +103,7 @@ namespace sat {
}
}
}
// -----------------------
//
// Variable & Clause creation
@ -312,7 +312,7 @@ namespace sat {
/**
\brief Select a watch literal starting the search at the given position.
This method is only used for clauses created during the search.
I use the following rules to select a watch literal.
1- select a literal l in idx >= starting_at such that value(l) = l_true,
@ -329,7 +329,7 @@ namespace sat {
lvl(l) >= lvl(l')
Without rule 3, boolean propagation is incomplete, that is, it may miss possible propagations.
\remark The method select_lemma_watch_lit is used to select the watch literal for regular learned clauses.
*/
unsigned solver::select_watch_lit(clause const & cls, unsigned starting_at) const {
@ -443,7 +443,7 @@ namespace sat {
erase_clause_watch(get_wlist(~c[0]), cls_off);
erase_clause_watch(get_wlist(~c[1]), cls_off);
}
void solver::dettach_ter_clause(clause & c) {
erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
@ -498,10 +498,10 @@ namespace sat {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
switch (value(c[i])) {
case l_true:
case l_true:
return l_true;
case l_undef:
found_undef = true;
case l_undef:
found_undef = true;
break;
default:
break;
@ -515,7 +515,7 @@ namespace sat {
// Propagation
//
// -----------------------
bool solver::propagate_core(bool update) {
if (m_inconsistent)
return false;
@ -545,7 +545,7 @@ namespace sat {
}
for (; it != end; ++it) {
switch (it->get_kind()) {
case watched::BINARY:
case watched::BINARY:
l1 = it->get_literal();
switch (value(l1)) {
case l_false:
@ -585,15 +585,30 @@ namespace sat {
break;
case watched::CLAUSE: {
if (value(it->get_blocked_literal()) == l_true) {
TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n";
clause_offset cls_off = it->get_clause_offset();
clause & c = *(m_cls_allocator.get_clause(cls_off));
tout << c << "\n";);
*it2 = *it;
it2++;
break;
}
clause_offset cls_off = it->get_clause_offset();
clause & c = *(m_cls_allocator.get_clause(cls_off));
TRACE("propagate_clause_bug", tout << "processing... " << c << "\nwas_removed: " << c.was_removed() << "\n";);
if (c[0] == not_l)
std::swap(c[0], c[1]);
CTRACE("propagate_bug", c[1] != not_l, tout << "l: " << l << " " << c << "\n";);
if (c.was_removed() || c[1] != not_l) {
// Remark: this method may be invoked when the watch lists are not in a consistent state,
// and may contain dead/removed clauses, or clauses with removed literals.
// See: method propagate_unit at sat_simplifier.cpp
// So, we must check whether the clause was marked for deletion, or
// c[1] != not_l
*it2 = *it;
it2++;
break;
}
SASSERT(c[1] == not_l);
if (value(c[0]) == l_true) {
it2->set_clause(c[0], cls_off);
@ -693,7 +708,7 @@ namespace sat {
m_conflicts_since_restart = 0;
m_restart_threshold = m_config.m_restart_initial;
}
// iff3_finder(*this)();
simplify_problem();
@ -704,10 +719,10 @@ namespace sat {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = 0\"\n";);
return l_undef;
}
while (true) {
SASSERT(!inconsistent());
lbool r = bounded_search();
if (r != l_undef)
return r;
@ -716,7 +731,7 @@ namespace sat {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"abort: max-conflicts = " << m_conflicts << "\"\n";);
return l_undef;
}
restart();
if (m_conflicts >= m_next_simplify) {
simplify_problem();
@ -734,7 +749,7 @@ namespace sat {
bool_var solver::next_var() {
bool_var next;
if (m_rand() < static_cast<int>(m_config.m_random_freq * random_gen::max_value())) {
if (num_vars() == 0)
return null_bool_var;
@ -743,16 +758,16 @@ namespace sat {
if (value(next) == l_undef && !was_eliminated(next))
return next;
}
while (!m_case_split_queue.empty()) {
next = m_case_split_queue.next_var();
if (value(next) == l_undef && !was_eliminated(next))
return next;
}
return null_bool_var;
}
bool solver::decide() {
bool_var next = next_var();
if (next == null_bool_var)
@ -760,7 +775,7 @@ namespace sat {
push();
m_stats.m_decision++;
lbool phase = m_ext ? m_ext->get_phase(next) : l_undef;
if (phase == l_undef) {
switch (m_config.m_phase) {
case PS_ALWAYS_TRUE:
@ -784,7 +799,7 @@ namespace sat {
break;
}
}
SASSERT(phase != l_undef);
literal next_lit(next, phase == l_false);
assign(next_lit, justification());
@ -807,23 +822,23 @@ namespace sat {
return l_undef;
if (scope_lvl() == 0) {
cleanup(); // cleaner may propagate frozen clauses
if (inconsistent())
if (inconsistent())
return l_false;
gc();
}
}
gc();
if (!decide()) {
if (m_ext) {
switch (m_ext->check()) {
case CR_DONE:
case CR_DONE:
mk_model();
return l_true;
case CR_CONTINUE:
case CR_CONTINUE:
break;
case CR_GIVEUP:
case CR_GIVEUP:
throw abort_solver();
}
}
@ -849,23 +864,23 @@ namespace sat {
m_stopwatch.reset();
m_stopwatch.start();
}
/**
\brief Apply all simplifications.
*/
void solver::simplify_problem() {
SASSERT(scope_lvl() == 0);
m_cleaner();
CASSERT("sat_simplify_bug", check_invariant());
m_scc();
CASSERT("sat_simplify_bug", check_invariant());
m_simplifier(false);
m_simplifier(false);
CASSERT("sat_simplify_bug", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
if (!m_learned.empty()) {
m_simplifier(true);
CASSERT("sat_missed_prop", check_missed_propagation());
@ -878,11 +893,11 @@ namespace sat {
m_probing();
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
m_asymm_branch();
CASSERT("sat_missed_prop", check_missed_propagation());
CASSERT("sat_simplify_bug", check_invariant());
if (m_ext) {
m_ext->clauses_modifed();
m_ext->simplify();
@ -956,7 +971,7 @@ namespace sat {
}
}
}
if (!m_mc.check_model(m))
if (!m_mc.check_model(m))
ok = false;
CTRACE("sat_model_bug", !ok, tout << m << "\n";);
return ok;
@ -964,9 +979,9 @@ namespace sat {
void solver::restart() {
m_stats.m_restart++;
IF_VERBOSE(1,
IF_VERBOSE(1,
verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
<< " :restarts " << m_stats.m_restart << mk_stat(*this)
<< " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
IF_VERBOSE(30, display_status(verbose_stream()););
pop(scope_lvl());
@ -991,9 +1006,9 @@ namespace sat {
// GC
//
// -----------------------
void solver::gc() {
if (m_conflicts_since_gc <= m_gc_threshold)
if (m_conflicts_since_gc <= m_gc_threshold)
return;
CASSERT("sat_gc_bug", check_invariant());
switch (m_config.m_gc_strategy) {
@ -1073,7 +1088,7 @@ namespace sat {
std::stable_sort(m_learned.begin(), m_learned.end(), glue_lt());
gc_half("glue");
}
void solver::gc_psm() {
save_psm();
std::stable_sort(m_learned.begin(), m_learned.end(), psm_lt());
@ -1134,8 +1149,8 @@ namespace sat {
void solver::gc_dyn_psm() {
// To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact
// that I may miss some propagations for reactivated clauses.
SASSERT(scope_lvl() == 0);
// compute
SASSERT(scope_lvl() == 0);
// compute
// d_tk
unsigned h = 0;
unsigned V_tk = 0;
@ -1152,7 +1167,7 @@ namespace sat {
double d_tk = V_tk == 0 ? static_cast<double>(num_vars() + 1) : static_cast<double>(h)/static_cast<double>(V_tk);
if (d_tk < m_min_d_tk)
m_min_d_tk = d_tk;
TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";);
TRACE("sat_frozen", tout << "m_min_d_tk: " << m_min_d_tk << "\n";);
unsigned frozen = 0;
unsigned deleted = 0;
unsigned activated = 0;
@ -1218,15 +1233,15 @@ namespace sat {
++it2;
}
m_learned.set_end(it2);
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk <<
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :d_tk " << d_tk << " :min-d_tk " << m_min_d_tk <<
" :frozen " << frozen << " :activated " << activated << " :deleted " << deleted << ")\n";);
}
// return true if should keep the clause, and false if we should delete it.
bool solver::activate_frozen_clause(clause & c) {
bool solver::activate_frozen_clause(clause & c) {
TRACE("sat_gc", tout << "reactivating:\n" << c << "\n";);
SASSERT(scope_lvl() == 0);
// do some cleanup
// do some cleanup
unsigned sz = c.size();
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
@ -1290,13 +1305,13 @@ namespace sat {
bool solver::resolve_conflict() {
while (true) {
bool r = resolve_conflict_core();
CASSERT("sat_check_marks", check_marks());
// after pop, clauses are reinitialized, this may trigger another conflict.
if (!r)
if (!r)
return false;
if (!inconsistent())
return true;
}
CASSERT("sat_check_marks", check_marks());
}
bool solver::resolve_conflict_core() {
@ -1311,7 +1326,7 @@ namespace sat {
if (m_conflict_lvl == 0)
return false;
m_lemma.reset();
forget_phase_of_vars(m_conflict_lvl);
unsigned idx = skip_literals_above_conflict_level();
@ -1323,10 +1338,10 @@ namespace sat {
TRACE("sat_conflict", tout << "not_l: " << m_not_l << "\n";);
process_antecedent(m_not_l, num_marks);
}
literal consequent = m_not_l;
justification js = m_conflict;
do {
TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);
@ -1362,7 +1377,7 @@ namespace sat {
fill_ext_antecedents(consequent, js);
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it)
for (; it != end; ++it)
process_antecedent(*it, num_marks);
break;
}
@ -1370,10 +1385,10 @@ namespace sat {
UNREACHABLE();
break;
}
while (true) {
literal l = m_trail[idx];
if (is_marked(l.var()))
if (is_marked(l.var()))
break;
SASSERT(idx > 0);
idx--;
@ -1386,9 +1401,9 @@ namespace sat {
idx--;
num_marks--;
reset_mark(c_var);
}
}
while (num_marks > 0);
m_lemma[0] = ~consequent;
TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
@ -1399,7 +1414,9 @@ namespace sat {
dyn_sub_res();
TRACE("sat_lemma", tout << "new lemma (after minimization) size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
}
else
reset_lemma_var_marks();
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
unsigned new_scope_lvl = 0;
@ -1430,10 +1447,10 @@ namespace sat {
return 0;
unsigned r = 0;
if (consequent != null_literal)
r = lvl(consequent);
switch (js.get_kind()) {
case justification::NONE:
break;
@ -1466,7 +1483,7 @@ namespace sat {
fill_ext_antecedents(consequent, js);
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it)
for (; it != end; ++it)
r = std::max(r, lvl(*it));
break;
}
@ -1495,7 +1512,7 @@ namespace sat {
}
return idx;
}
void solver::process_antecedent(literal antecedent, unsigned & num_marks) {
bool_var var = antecedent.var();
unsigned var_lvl = lvl(var);
@ -1509,7 +1526,7 @@ namespace sat {
m_lemma.push_back(~antecedent);
}
}
/**
\brief js is an external justification. Collect its antecedents and store at m_ext_antecedents.
*/
@ -1576,7 +1593,7 @@ namespace sat {
unsigned var_lvl = lvl(var);
if (!is_marked(var) && var_lvl > 0) {
if (m_lvl_set.may_contain(var_lvl)) {
mark(var);
mark(var);
m_unmark.push_back(var);
m_lemma_min_stack.push_back(var);
}
@ -1588,17 +1605,17 @@ namespace sat {
}
/**
\brief Return true if lit is implied by other marked literals
and/or literals assigned at the base level.
The set lvl_set is used as an optimization.
\brief Return true if lit is implied by other marked literals
and/or literals assigned at the base level.
The set lvl_set is used as an optimization.
The idea is to stop the recursive search with a failure
as soon as we find a literal assigned in a level that is not in lvl_set.
as soon as we find a literal assigned in a level that is not in lvl_set.
*/
bool solver::implied_by_marked(literal lit) {
m_lemma_min_stack.reset(); // avoid recursive function
m_lemma_min_stack.push_back(lit.var());
unsigned old_size = m_unmark.size();
while (!m_lemma_min_stack.empty()) {
bool_var var = m_lemma_min_stack.back();
m_lemma_min_stack.pop_back();
@ -1699,7 +1716,7 @@ namespace sat {
void solver::minimize_lemma() {
m_unmark.reset();
updt_lemma_lvl_set();
unsigned sz = m_lemma.size();
unsigned i = 1; // the first literal is the FUIP
unsigned j = 1;
@ -1715,12 +1732,12 @@ namespace sat {
j++;
}
}
reset_unmark(0);
m_lemma.shrink(j);
m_stats.m_minimized_lits += sz - j;
}
/**
\brief Reset the mark of the variables in the current lemma.
*/
@ -1740,17 +1757,17 @@ namespace sat {
Only binary and ternary clauses are used.
*/
void solver::dyn_sub_res() {
unsigned sz = m_lemma.size();
unsigned sz = m_lemma.size();
for (unsigned i = 0; i < sz; i++) {
mark_lit(m_lemma[i]);
}
literal l0 = m_lemma[0];
// l0 is the FUIP, and we never remove the FUIP.
//
//
// In the following loop, we use unmark_lit(l) to remove a
// literal from m_lemma.
for (unsigned i = 0; i < sz; i++) {
literal l = m_lemma[i];
if (!is_marked_lit(l))
@ -1762,8 +1779,8 @@ namespace sat {
for (; it != end; ++it) {
// In this for-loop, the conditions l0 != ~l2 and l0 != ~l3
// are not really needed if the solver does not miss unit propagations.
// However, we add them anyway because we don't want to rely on this
// property of the propagator.
// However, we add them anyway because we don't want to rely on this
// property of the propagator.
// For example, if this property is relaxed in the future, then the code
// without the conditions l0 != ~l2 and l0 != ~l3 may remove the FUIP
if (it->is_binary_clause()) {
@ -1809,10 +1826,10 @@ namespace sat {
// p1 \/ ~p2
// p2 \/ ~p3
// p3 \/ ~p4
// q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ~q1 \/ q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ~q1 \/ ~q2 \/ p1 \/ p2 \/ p3 \/ p4 \/ l2
// ...
//
// 2. Now suppose we learned the lemma
@ -1823,15 +1840,15 @@ namespace sat {
// That is, l \/ l2 is an implied clause. Note that probing does not add
// this clause to the clause database (there are too many).
//
// 4. Lemma (*) is deleted (garbage collected).
// 4. Lemma (*) is deleted (garbage collected).
//
// 5. l is decided to be false, p1, p2, p3 and p4 are propagated using BCP,
// but l2 is not since the lemma (*) was deleted.
//
//
// Probing module still "knows" that l \/ l2 is valid binary clause
//
//
// 6. A new lemma is created where ~l2 is the FUIP and the lemma also contains l.
// If we remove l0 != ~l2 may try to delete the FUIP.
// If we remove l0 != ~l2 may try to delete the FUIP.
if (is_marked_lit(~l2) && l0 != ~l2) {
// eliminate ~l2 from lemma because we have the clause l \/ l2
unmark_lit(~l2);
@ -1842,7 +1859,7 @@ namespace sat {
// can't eliminat FUIP
SASSERT(is_marked_lit(m_lemma[0]));
unsigned j = 0;
for (unsigned i = 0; i < sz; i++) {
literal l = m_lemma[i];
@ -1854,7 +1871,7 @@ namespace sat {
}
m_stats.m_dyn_sub_res += sz - j;
SASSERT(j >= 1);
m_lemma.shrink(j);
}
@ -1947,7 +1964,7 @@ namespace sat {
// Misc
//
// -----------------------
void solver::updt_params(params_ref const & p) {
m_params = p;
m_config.updt_params(p);
@ -1969,7 +1986,7 @@ namespace sat {
void solver::set_cancel(bool f) {
m_cancel = f;
}
void solver::collect_statistics(statistics & st) {
m_stats.collect_statistics(st);
m_cleaner.collect_statistics(st);
@ -2065,7 +2082,7 @@ namespace sat {
}
}
}
void solver::display_units(std::ostream & out) const {
unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
for (unsigned i = 0; i < end; i++) {
@ -2219,26 +2236,26 @@ namespace sat {
// Simplification
//
// -----------------------
void solver::cleanup() {
if (scope_lvl() > 0 || inconsistent())
return;
void solver::cleanup() {
if (scope_lvl() > 0 || inconsistent())
return;
if (m_cleaner() && m_ext)
m_ext->clauses_modifed();
}
void solver::simplify(bool learned) {
if (scope_lvl() > 0 || inconsistent())
return;
m_simplifier(learned);
m_simplifier.free_memory();
void solver::simplify(bool learned) {
if (scope_lvl() > 0 || inconsistent())
return;
m_simplifier(learned);
m_simplifier.free_memory();
if (m_ext)
m_ext->clauses_modifed();
}
unsigned solver::scc_bin() {
if (scope_lvl() > 0 || inconsistent())
return 0;
unsigned r = m_scc();
unsigned solver::scc_bin() {
if (scope_lvl() > 0 || inconsistent())
return 0;
unsigned r = m_scc();
if (r > 0 && m_ext)
m_ext->clauses_modifed();
return r;
@ -2312,10 +2329,10 @@ namespace sat {
out << " :inconsistent " << (m_inconsistent ? "true" : "false") << "\n";
out << " :vars " << num_vars() << "\n";
out << " :elim-vars " << num_elim << "\n";
out << " :lits " << num_lits << "\n";
out << " :lits " << num_lits << "\n";
out << " :assigned " << m_trail.size() << "\n";
out << " :binary-clauses " << num_bin << "\n";
out << " :ternary-clauses " << num_ter << "\n";
out << " :binary-clauses " << num_bin << "\n";
out << " :ternary-clauses " << num_ter << "\n";
out << " :clauses " << num_cls << "\n";
out << " :del-clause " << m_stats.m_del_clause << "\n";
out << " :avg-clause-size " << (total_cls == 0 ? 0.0 : static_cast<double>(num_lits) / static_cast<double>(total_cls)) << "\n";

7
src/smt/diff_logic.h
View file

@ -820,6 +820,7 @@ public:
}
}
private:
// Update the assignment of variable v, that is,
// m_assignment[v] += inc
// This method also stores the old value of v in the assignment stack.
@ -829,6 +830,12 @@ public:
m_assignment[v] += inc;
}
public:
void inc_assignment(dl_var v, numeral const& inc) {
m_assignment[v] += inc;
}
struct every_var_proc {
bool operator()(dl_var v) const {

3
src/smt/proto_model/value_factory.h
View file

@ -189,11 +189,12 @@ public:
max_size = Number(usz);
has_max = true;
}
Number start = set->m_next;
Number & next = set->m_next;
while (!is_new) {
result = mk_value(next, s, is_new);
next++;
if (has_max && next > max_size + set->m_next) {
if (has_max && next > max_size + start) {
return 0;
}
}

8
src/smt/smt_model_finder.cpp
View file

@ -975,9 +975,11 @@ namespace smt {
// Moreover, a model assigns an arbitrary intepretation to these sorts using "model_values" a model value.
// If these module values "leak" inside the logical context, they may affect satisfiability.
//
// n->insert(m_model->get_some_value(n->get_sort()), 0);
// TODO: we can use get_some_value if the sort n->get_sort() does not depend on any uninterpreted sorts.
n->insert(m_manager.mk_fresh_const("elem", n->get_sort()), 0);
sort * ns = n->get_sort();
if (m_manager.is_fully_interp(ns))
n->insert(m_model->get_some_value(ns), 0);
else
n->insert(m_manager.mk_fresh_const("elem", ns), 0);
}
}
}

31
src/smt/theory_bv.cpp
View file

@ -581,10 +581,13 @@ namespace smt {
void theory_bv::assert_int2bv_axiom(app* n) {
//
// create the axiom:
// bv2int(n) = e mod 2^bit_width
//
// bv2int(n) = e mod 2^bit_width
// where n = int2bv(e)
//
// Create the axioms:
// bit2bool(i,n) == ((e div 2^i) mod 2 != 0)
// for i = 0,.., sz-1
//
SASSERT(get_context().e_internalized(n));
SASSERT(m_util.is_int2bv(n));
ast_manager & m = get_manager();
@ -592,10 +595,12 @@ namespace smt {
parameter param(m_autil.mk_int());
expr* n_expr = n;
expr* lhs = m.mk_app(get_id(), OP_BV2INT, 1, &param, 1, &n_expr);
expr* e = n->get_arg(0);
expr_ref lhs(m), rhs(m);
lhs = m.mk_app(get_id(), OP_BV2INT, 1, &param, 1, &n_expr);
unsigned sz = m_util.get_bv_size(n);
numeral mod = power(numeral(2), sz);
expr* rhs = m_autil.mk_mod(n->get_arg(0), m_autil.mk_numeral(mod, true));
rhs = m_autil.mk_mod(e, m_autil.mk_numeral(mod, true));
literal l(mk_eq(lhs, rhs, false));
ctx.mark_as_relevant(l);
@ -605,6 +610,24 @@ namespace smt {
tout << mk_pp(lhs, m) << " == \n";
tout << mk_pp(rhs, m) << "\n";
);
expr_ref_vector n_bits(m);
enode * n_enode = mk_enode(n);
get_bits(n_enode, n_bits);
for (unsigned i = 0; i < sz; ++i) {
numeral div = power(numeral(2), i);
mod = numeral(2);
rhs = m_autil.mk_idiv(e, m_autil.mk_numeral(div,true));
rhs = m_autil.mk_mod(rhs, m_autil.mk_numeral(mod, true));
rhs = m.mk_eq(rhs, m_autil.mk_numeral(rational(1), true));
lhs = n_bits.get(i);
TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";);
l = literal(mk_eq(lhs, rhs, false));
ctx.mark_as_relevant(l);
ctx.mk_th_axiom(get_id(), 1, &l);
}
}

3
src/smt/theory_utvpi_def.h
View file

@ -752,7 +752,8 @@ namespace smt {
for (unsigned j = 0; j < zero_v.size(); ++j) {
int v = zero_v[j];
m_graph.acc_assignment(v, numeral(-1));
m_graph.inc_assignment(v, numeral(-1));
th_var k = from_var(v);
if (!is_parity_ok(k)) {
todo.push_back(k);

58
src/tactic/arith/factor_tactic.cpp
View file

@ -50,7 +50,7 @@ class factor_tactic : public tactic {
return args[0];
return m_util.mk_mul(sz, args);
}
expr * mk_zero_for(expr * arg) {
return m_util.mk_numeral(rational(0), m_util.is_int(arg));
}
@ -92,10 +92,10 @@ class factor_tactic : public tactic {
return k;
}
}
// p1^{2*k1} * p2^{2*k2 + 1} >=< 0
// -->
// (p1^2)*p2 >=<0
// (p1^2)*p2 >=<0
void mk_comp(decl_kind k, polynomial::factors const & fs, expr_ref & result) {
SASSERT(k == OP_LT || k == OP_GT || k == OP_LE || k == OP_GE);
expr_ref_buffer args(m);
@ -127,7 +127,7 @@ class factor_tactic : public tactic {
}
}
}
// Strict case
// p1^{2*k1} * p2^{2*k2 + 1} >< 0
// -->
@ -158,11 +158,11 @@ class factor_tactic : public tactic {
args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.c_ptr()), mk_zero_for(odd_factors[0])));
}
SASSERT(!args.empty());
if (args.size() == 1)
if (args.size() == 1)
result = args[0];
else if (strict)
result = m.mk_and(args.size(), args.c_ptr());
else
else
result = m.mk_or(args.size(), args.c_ptr());
}
@ -173,7 +173,7 @@ class factor_tactic : public tactic {
scoped_mpz d2(m_qm);
m_expr2poly.to_polynomial(lhs, p1, d1);
m_expr2poly.to_polynomial(rhs, p2, d2);
TRACE("factor_tactic_bug",
TRACE("factor_tactic_bug",
tout << "lhs: " << mk_ismt2_pp(lhs, m) << "\n";
tout << "p1: " << p1 << "\n";
tout << "d1: " << d1 << "\n";
@ -195,18 +195,18 @@ class factor_tactic : public tactic {
SASSERT(fs.distinct_factors() > 0);
TRACE("factor_tactic_bug", tout << "factors:\n"; fs.display(tout); tout << "\n";);
if (fs.distinct_factors() == 1 && fs.get_degree(0) == 1)
return BR_FAILED;
return BR_FAILED;
if (m.is_eq(f)) {
if (m_split_factors)
mk_split_eq(fs, result);
else
else
mk_eq(fs, result);
}
else {
decl_kind k = f->get_decl_kind();
if (m_qm.is_neg(fs.get_constant()))
k = flip(k);
if (m_split_factors)
mk_split_comp(k, fs, result);
else
@ -215,10 +215,10 @@ class factor_tactic : public tactic {
return BR_DONE;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
if (num != 2)
return BR_FAILED;
if (m.is_eq(f) && (m_util.is_arith_expr(args[0]) || m_util.is_arith_expr(args[1])))
if (m.is_eq(f) && (m_util.is_arith_expr(args[0]) || m_util.is_arith_expr(args[1])) && (!m.is_bool(args[0])))
return factor(f, args[0], args[1], result);
if (f->get_family_id() != m_util.get_family_id())
return BR_FAILED;
@ -232,10 +232,10 @@ class factor_tactic : public tactic {
return BR_FAILED;
}
};
struct rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg;
rw(ast_manager & m, params_ref const & p):
rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, p) {
@ -245,24 +245,24 @@ class factor_tactic : public tactic {
struct imp {
ast_manager & m;
rw m_rw;
imp(ast_manager & _m, params_ref const & p):
m(_m),
m_rw(m, p) {
}
void set_cancel(bool f) {
m_rw.set_cancel(f);
m_rw.cfg().m_pm.set_cancel(f);
}
void updt_params(params_ref const & p) {
m_rw.cfg().updt_params(p);
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
@ -288,7 +288,7 @@ class factor_tactic : public tactic {
SASSERT(g->is_well_sorted());
}
};
imp * m_imp;
params_ref m_params;
public:
@ -300,7 +300,7 @@ public:
virtual tactic * translate(ast_manager & m) {
return alloc(factor_tactic, m, m_params);
}
virtual ~factor_tactic() {
dealloc(m_imp);
}
@ -311,14 +311,14 @@ public:
}
virtual void collect_param_descrs(param_descrs & r) {
r.insert("split_factors", CPK_BOOL,
r.insert("split_factors", CPK_BOOL,
"(default: true) apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).");
polynomial::factor_params::get_param_descrs(r);
}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
@ -331,7 +331,7 @@ public:
throw tactic_exception(ex.msg());
}
}
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;

1
src/tactic/core/elim_uncnstr_tactic.cpp
View file

@ -38,7 +38,6 @@ class elim_uncnstr_tactic : public tactic {
typedef std::pair<expr *, unsigned> frame;
svector<frame> m_stack;
ptr_vector<app> m_vars;
expr_sparse_mark m_uncnstr_vars;
bool visit(expr * t) {
if (m_visited.is_marked(t)) {

620
src/tactic/sls/sls_evaluator.h Normal file
View file

@ -0,0 +1,620 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
sls_evaluator.h
Abstract:
SLS Evaluator
Author:
Christoph (cwinter) 2012-02-29
Notes:
--*/
#ifndef _SLS_EVALUATOR_H_
#define _SLS_EVALUATOR_H_
#include"sls_powers.h"
#include"sls_tracker.h"
class sls_evaluator {
ast_manager & m_manager;
bv_util & m_bv_util;
family_id m_basic_fid;
family_id m_bv_fid;
sls_tracker & m_tracker;
unsynch_mpz_manager & m_mpz_manager;
mpz m_zero, m_one, m_two;
powers & m_powers;
expr_ref_buffer m_temp_exprs;
vector<ptr_vector<expr> > m_traversal_stack;
public:
sls_evaluator(ast_manager & m, bv_util & bvu, sls_tracker & t, unsynch_mpz_manager & mm, powers & p) :
m_manager(m),
m_bv_util(bvu),
m_tracker(t),
m_mpz_manager(mm),
m_zero(m_mpz_manager.mk_z(0)),
m_one(m_mpz_manager.mk_z(1)),
m_two(m_mpz_manager.mk_z(2)),
m_powers(p),
m_temp_exprs(m) {
m_bv_fid = m_bv_util.get_family_id();
m_basic_fid = m_manager.get_basic_family_id();
}
~sls_evaluator() {
m_mpz_manager.del(m_zero);
m_mpz_manager.del(m_one);
m_mpz_manager.del(m_two);
}
void operator()(app * n, mpz & result) {
family_id nfid = n->get_family_id();
func_decl * fd = n->get_decl();
unsigned n_args = n->get_num_args();
if (n_args == 0) {
m_mpz_manager.set(result, m_tracker.get_value(n));
return;
}
expr * const * args = n->get_args();
m_mpz_manager.set(result, m_zero);
if (nfid == m_basic_fid) {
switch (n->get_decl_kind()) {
case OP_AND: {
m_mpz_manager.set(result, m_one);
for (unsigned i = 0; i < n_args; i++)
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
m_mpz_manager.set(result, m_zero);
break;
}
break;
}
case OP_OR: {
for (unsigned i = 0; i < n_args; i++)
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), result)) {
m_mpz_manager.set(result, m_one);
break;
}
break;
}
case OP_NOT: {
SASSERT(n_args == 1);
const mpz & child = m_tracker.get_value(args[0]);
SASSERT(m_mpz_manager.is_one(child) || m_mpz_manager.is_zero(child));
m_mpz_manager.set(result, (m_mpz_manager.is_zero(child)) ? m_one : m_zero);
break;
}
case OP_EQ: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_one);
const mpz & first = m_tracker.get_value(args[0]);
for (unsigned i = 1; i < n_args; i++)
if (m_mpz_manager.neq(m_tracker.get_value(args[i]), first)) {
m_mpz_manager.set(result, m_zero);
break;
}
break;
}
case OP_DISTINCT: {
m_mpz_manager.set(result, m_one);
for (unsigned i = 0; i < n_args && m_mpz_manager.is_one(result); i++) {
for (unsigned j = i+1; j < n_args && m_mpz_manager.is_one(result); j++) {
if (m_mpz_manager.eq(m_tracker.get_value(args[i]), m_tracker.get_value(args[j])))
m_mpz_manager.set(result, m_zero);
}
}
break;
}
default:
NOT_IMPLEMENTED_YET();
}
}
else if (nfid == m_bv_fid) {
bv_op_kind k = static_cast<bv_op_kind>(fd->get_decl_kind());
switch(k) {
case OP_CONCAT: {
SASSERT(n_args >= 2);
for (unsigned i = 0; i < n_args; i++) {
if (i != 0) {
const mpz & p = m_powers(m_bv_util.get_bv_size(args[i]));
m_mpz_manager.mul(result, p, result);
}
m_mpz_manager.add(result, m_tracker.get_value(args[i]), result);
}
break;
}
case OP_EXTRACT: {
SASSERT(n_args == 1);
const mpz & child = m_tracker.get_value(args[0]);
unsigned h = m_bv_util.get_extract_high(n);
unsigned l = m_bv_util.get_extract_low(n);
m_mpz_manager.rem(child, m_powers(h+1), result); // result = [h:0] of child
m_mpz_manager.machine_div2k(result, l, result);
break;
}
case OP_BADD: {
SASSERT(n_args >= 2);
for (unsigned i = 0; i < n_args; i++) {
const mpz & next = m_tracker.get_value(args[i]);
m_mpz_manager.add(result, next, result);
}
const mpz & p = m_powers(m_bv_util.get_bv_size(n));
m_mpz_manager.rem(result, p, result);
break;
}
case OP_BSUB: {
SASSERT(n_args == 2);
const mpz & p = m_powers(m_bv_util.get_bv_size(n));
mpz temp;
m_mpz_manager.sub(m_tracker.get_value(args[0]), m_tracker.get_value(args[1]), temp);
m_mpz_manager.mod(temp, p, result);
m_mpz_manager.del(temp);
break;
}
case OP_BMUL: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++) {
const mpz & next = m_tracker.get_value(args[i]);
m_mpz_manager.mul(result, next, result);
}
const mpz & p = m_powers(m_bv_util.get_bv_size(n));
m_mpz_manager.rem(result, p, result);
break;
}
case OP_BNEG: { // 2's complement unary minus
SASSERT(n_args == 1);
const mpz & child = m_tracker.get_value(args[0]);
if (m_mpz_manager.is_zero(child)) {
m_mpz_manager.set(result, m_zero);
}
else {
unsigned bv_sz = m_bv_util.get_bv_size(n);
m_mpz_manager.bitwise_not(bv_sz, child, result);
m_mpz_manager.inc(result); // can't overflow
}
break;
}
case OP_BSDIV:
case OP_BSDIV0:
case OP_BSDIV_I: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
SASSERT(m_mpz_manager.is_nonneg(x) && m_mpz_manager.is_nonneg(y));
unsigned bv_sz = m_bv_util.get_bv_size(args[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if (m_mpz_manager.is_zero(y)) {
if (m_mpz_manager.is_neg(x))
m_mpz_manager.set(result, m_one);
else {
m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n)));
m_mpz_manager.dec(result);
}
}
else {
m_mpz_manager.machine_div(x, y, result);
}
if (m_mpz_manager.is_neg(result))
m_mpz_manager.add(result, p, result);
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BUDIV:
case OP_BUDIV0:
case OP_BUDIV_I: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
if (m_mpz_manager.is_zero(y)) {
m_mpz_manager.set(result, m_powers(m_bv_util.get_bv_size(n)));
m_mpz_manager.dec(result);
}
else {
m_mpz_manager.machine_div(x, y, result);
}
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BSREM:
case OP_BSREM0:
case OP_BSREM_I: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
unsigned bv_sz = m_bv_util.get_bv_size(args[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if (m_mpz_manager.is_zero(y)) {
m_mpz_manager.set(result, x);
}
else {
m_mpz_manager.rem(x, y, result);
}
if (m_mpz_manager.is_neg(result))
m_mpz_manager.add(result, p, result);
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BUREM:
case OP_BUREM0:
case OP_BUREM_I: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
if (m_mpz_manager.is_zero(y)) {
m_mpz_manager.set(result, x);
}
else {
m_mpz_manager.mod(x, y, result);
}
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BSMOD:
case OP_BSMOD0:
case OP_BSMOD_I:{
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
unsigned bv_sz = m_bv_util.get_bv_size(args[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if (m_mpz_manager.is_zero(y))
m_mpz_manager.set(result, x);
else {
bool neg_x = m_mpz_manager.is_neg(x);
bool neg_y = m_mpz_manager.is_neg(y);
mpz abs_x, abs_y;
m_mpz_manager.set(abs_x, x);
m_mpz_manager.set(abs_y, y);
if (neg_x) m_mpz_manager.neg(abs_x);
if (neg_y) m_mpz_manager.neg(abs_y);
SASSERT(m_mpz_manager.is_nonneg(abs_x) && m_mpz_manager.is_nonneg(abs_y));
m_mpz_manager.mod(abs_x, abs_y, result);
if (m_mpz_manager.is_zero(result) || (!neg_x && !neg_y)) {
/* Nothing */
}
else if (neg_x && !neg_y) {
m_mpz_manager.neg(result);
m_mpz_manager.add(result, y, result);
}
else if (!neg_x && neg_y) {
m_mpz_manager.add(result, y, result);
}
else {
m_mpz_manager.neg(result);
}
m_mpz_manager.del(abs_x);
m_mpz_manager.del(abs_y);
}
if (m_mpz_manager.is_neg(result))
m_mpz_manager.add(result, p, result);
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BAND: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++)
m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), result);
break;
}
case OP_BOR: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++) {
m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), result);
}
break;
}
case OP_BXOR: {
SASSERT(n_args >= 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++)
m_mpz_manager.bitwise_xor(result, m_tracker.get_value(args[i]), result);
break;
}
case OP_BNAND: {
SASSERT(n_args >= 2);
mpz temp;
unsigned bv_sz = m_bv_util.get_bv_size(n);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++) {
m_mpz_manager.bitwise_and(result, m_tracker.get_value(args[i]), temp);
m_mpz_manager.bitwise_not(bv_sz, temp, result);
}
m_mpz_manager.del(temp);
break;
}
case OP_BNOR: {
SASSERT(n_args >= 2);
mpz temp;
unsigned bv_sz = m_bv_util.get_bv_size(n);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
for (unsigned i = 1; i < n_args; i++) {
m_mpz_manager.bitwise_or(result, m_tracker.get_value(args[i]), temp);
m_mpz_manager.bitwise_not(bv_sz, temp, result);
}
m_mpz_manager.del(temp);
break;
}
case OP_BNOT: {
SASSERT(n_args == 1);
m_mpz_manager.bitwise_not(m_bv_util.get_bv_size(args[0]), m_tracker.get_value(args[0]), result);
break;
}
case OP_ULT:
case OP_ULEQ:
case OP_UGT:
case OP_UGEQ: {
SASSERT(n_args == 2);
const mpz & x = m_tracker.get_value(args[0]);
const mpz & y = m_tracker.get_value(args[1]);
if ((k == OP_ULT && m_mpz_manager.lt(x, y)) ||
(k == OP_ULEQ && m_mpz_manager.le(x, y)) ||
(k == OP_UGT && m_mpz_manager.gt(x, y)) ||
(k == OP_UGEQ && m_mpz_manager.ge(x, y)))
m_mpz_manager.set(result, m_one);
break;
}
case OP_SLT:
case OP_SLEQ:
case OP_SGT:
case OP_SGEQ: {
SASSERT(n_args == 2);
mpz x; m_mpz_manager.set(x, m_tracker.get_value(args[0]));
mpz y; m_mpz_manager.set(y, m_tracker.get_value(args[1]));
unsigned bv_sz = m_bv_util.get_bv_size(args[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if ((k == OP_SLT && m_mpz_manager.lt(x, y)) ||
(k == OP_SLEQ && m_mpz_manager.le(x, y)) ||
(k == OP_SGT && m_mpz_manager.gt(x, y)) ||
(k == OP_SGEQ && m_mpz_manager.ge(x, y)))
m_mpz_manager.set(result, m_one);
m_mpz_manager.del(x);
m_mpz_manager.del(y);
break;
}
case OP_BIT2BOOL: {
SASSERT(n_args == 1);
const mpz & child = m_tracker.get_value(args[0]);
m_mpz_manager.set(result, child);
break;
}
case OP_BASHR: {
SASSERT(n_args == 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
mpz first;
const mpz & p = m_powers(m_bv_util.get_bv_size(args[0])-1);
m_mpz_manager.bitwise_and(result, p, first);
mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1]));
mpz temp;
while (!m_mpz_manager.is_zero(shift)) {
m_mpz_manager.machine_div(result, m_two, temp);
m_mpz_manager.add(temp, first, result);
m_mpz_manager.dec(shift);
}
m_mpz_manager.del(first);
m_mpz_manager.del(shift);
m_mpz_manager.del(temp);
break;
}
case OP_BLSHR: {
SASSERT(n_args == 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1]));
while (!m_mpz_manager.is_zero(shift)) {
m_mpz_manager.machine_div(result, m_two, result);
m_mpz_manager.dec(shift);
}
m_mpz_manager.del(shift);
break;
}
case OP_BSHL: {
SASSERT(n_args == 2);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
mpz shift; m_mpz_manager.set(shift, m_tracker.get_value(args[1]));
while (!m_mpz_manager.is_zero(shift)) {
m_mpz_manager.mul(result, m_two, result);
m_mpz_manager.dec(shift);
}
const mpz & p = m_powers(m_bv_util.get_bv_size(n));
m_mpz_manager.rem(result, p, result);
m_mpz_manager.del(shift);
break;
}
case OP_SIGN_EXT: {
SASSERT(n_args == 1);
m_mpz_manager.set(result, m_tracker.get_value(args[0]));
break;
}
default:
NOT_IMPLEMENTED_YET();
}
}
else {
NOT_IMPLEMENTED_YET();
}
TRACE("sls_eval", tout << "(" << fd->get_name();
for (unsigned i = 0; i < n_args; i++)
tout << " " << m_mpz_manager.to_string(m_tracker.get_value(args[i]));
tout << ") ---> " << m_mpz_manager.to_string(result);
if (m_manager.is_bool(fd->get_range())) tout << " [Boolean]";
else tout << " [vector size: " << m_bv_util.get_bv_size(fd->get_range()) << "]";
tout << std::endl; );
SASSERT(m_mpz_manager.is_nonneg(result));
}
void eval_checked(expr * n, mpz & result) {
switch(n->get_kind()) {
case AST_APP: {
app * a = to_app(n);
(*this)(a, result);
unsigned n_args = a->get_num_args();
m_temp_exprs.reset();
for (unsigned i = 0; i < n_args; i++) {
expr * arg = a->get_arg(i);
const mpz & v = m_tracker.get_value(arg);
m_temp_exprs.push_back(m_tracker.mpz2value(m_manager.get_sort(arg), v));
}
expr_ref q(m_manager), temp(m_manager);
q = m_manager.mk_app(a->get_decl(), m_temp_exprs.size(), m_temp_exprs.c_ptr());
model dummy_model(m_manager);
model_evaluator evaluator(dummy_model);
evaluator(q, temp);
mpz check_res;
m_tracker.value2mpz(temp, check_res);
CTRACE("sls", !m_mpz_manager.eq(check_res, result),
tout << "EVAL BUG: IS " << m_mpz_manager.to_string(result) <<
" SHOULD BE " << m_mpz_manager.to_string(check_res) << std::endl; );
SASSERT(m_mpz_manager.eq(check_res, result));
m_mpz_manager.del(check_res);
break;
}
default:
NOT_IMPLEMENTED_YET();
}
}
void run_update(unsigned cur_depth) {
// precondition: m_traversal_stack contains the entry point(s)
expr_fast_mark1 visited;
mpz new_value;
SASSERT(cur_depth < m_traversal_stack.size());
while (cur_depth != static_cast<unsigned>(-1)) {
ptr_vector<expr> & cur_depth_exprs = m_traversal_stack[cur_depth];
for (unsigned i = 0; i < cur_depth_exprs.size(); i++) {
expr * cur = cur_depth_exprs[i];
(*this)(to_app(cur), new_value);
m_tracker.set_value(cur, new_value);
m_tracker.set_score(cur, m_tracker.score(cur));
if (m_tracker.has_uplinks(cur)) {
ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
for (unsigned j = 0; j < ups.size(); j++) {
expr * next = ups[j];
unsigned next_d = m_tracker.get_distance(next);
SASSERT(next_d < cur_depth);
if (!visited.is_marked(next)) {
m_traversal_stack[next_d].push_back(next);
visited.mark(next);
}
}
}
}
cur_depth_exprs.reset();
cur_depth--;
}
m_mpz_manager.del(new_value);
}
void update_all() {
unsigned max_depth = 0;
sls_tracker::entry_point_type::iterator start = m_tracker.get_entry_points().begin();
sls_tracker::entry_point_type::iterator end = m_tracker.get_entry_points().end();
for (sls_tracker::entry_point_type::iterator it = start; it != end; it++) {
expr * ep = m_tracker.get_entry_point(it->m_key);
unsigned cur_depth = m_tracker.get_distance(ep);
if (m_traversal_stack.size() <= cur_depth)
m_traversal_stack.resize(cur_depth+1);
m_traversal_stack[cur_depth].push_back(ep);
if (cur_depth > max_depth) max_depth = cur_depth;
}
run_update(max_depth);
}
void update(func_decl * fd, const mpz & new_value) {
m_tracker.set_value(fd, new_value);
expr * ep = m_tracker.get_entry_point(fd);
unsigned cur_depth = m_tracker.get_distance(ep);
if (m_traversal_stack.size() <= cur_depth)
m_traversal_stack.resize(cur_depth+1);
m_traversal_stack[cur_depth].push_back(ep);
run_update(cur_depth);
}
void randomize_local(goal_ref const & g) {
ptr_vector<func_decl> & unsat_constants = m_tracker.get_unsat_constants(g);
// Randomize _all_ candidates:
//// bool did_something = false;
//for (unsigned i = 0; i < unsat_constants.size(); i++) {
// func_decl * fd = unsat_constants[i];
// mpz temp = m_tracker.get_random(fd->get_range());
// // if (m_mpz_manager.neq(temp, m_tracker.get_value(fd))) {
// // did_something = true;
// // }
// update(fd, temp);
// m_mpz_manager.del(temp);
//}
// Randomize _one_ candidate:
unsigned r = m_tracker.get_random_uint(16) % unsat_constants.size();
func_decl * fd = unsat_constants[r];
mpz temp = m_tracker.get_random(fd->get_range());
update(fd, temp);
m_mpz_manager.del(temp);
TRACE("sls", /*tout << "Randomization candidates: ";
for (unsigned i = 0; i < unsat_constants.size(); i++)
tout << unsat_constants[i]->get_name() << ", ";
tout << std::endl;*/
tout << "Randomization candidate: " << unsat_constants[r]->get_name() << std::endl;
tout << "Locally randomized model: " << std::endl;
m_tracker.show_model(tout); );
}
};
#endif

8
src/tactic/sls/sls_params.pyg Normal file
View file

@ -0,0 +1,8 @@
def_module_params('sls',
export=True,
description='Experimental Stochastic Local Search Solver (for QFBV only).',
params=(max_memory_param(),
('restarts', UINT, UINT_MAX, '(max) number of restarts'),
('plateau_limit', UINT, 10, 'pleateau limit'),
('random_seed', UINT, 0, 'random seed')
))

49
src/tactic/sls/sls_powers.h Normal file
View file

@ -0,0 +1,49 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
sls_powers.h
Abstract:
Power-of-2 module for SLS
Author:
Christoph (cwinter) 2012-02-29
Notes:
--*/
#ifndef _SLS_POWERS_H_
#define _SLS_POWERS_H_
#include"mpz.h"
class powers : public u_map<mpz*> {
unsynch_mpz_manager & m;
public:
powers(unsynch_mpz_manager & m) : m(m) {}
~powers() {
for (iterator it = begin(); it != end(); it++) {
m.del(*it->m_value);
dealloc(it->m_value);
}
}
const mpz & operator()(unsigned n) {
u_map<mpz*>::iterator it = find_iterator(n);
if (it != end())
return *it->m_value;
else {
mpz * new_obj = alloc(mpz);
m.mul2k(m.mk_z(1), n, *new_obj);
insert(n, new_obj);
return *new_obj;
}
}
};
#endif

1304
src/tactic/sls/sls_tactic.cpp
View file

File diff suppressed because it is too large Load diff

675
src/tactic/sls/sls_tracker.h Normal file
View file

@ -0,0 +1,675 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
sls_score_tracker.h
Abstract:
Score and value tracking module for SLS
Author:
Christoph (cwinter) 2012-02-29
Notes:
--*/
#ifndef _SLS_TRACKER_H_
#define _SLS_TRACKER_H_
class sls_tracker {
ast_manager & m_manager;
unsynch_mpz_manager & m_mpz_manager;
bv_util & m_bv_util;
powers & m_powers;
random_gen m_rng;
unsigned m_random_bits;
unsigned m_random_bits_cnt;
mpz m_zero, m_one, m_two;
struct value_score {
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), distance(0) { };
~value_score() { if (m) m->del(value); }
unsynch_mpz_manager * m;
mpz value;
double score;
unsigned distance; // max distance from any root
value_score & operator=(const value_score & other) {
SASSERT(m == 0 || m == other.m);
if (m) m->set(value, 0); else m = other.m;
m->set(value, other.value);
score = other.score;
distance = other.distance;
return *this;
}
};
public:
typedef obj_map<func_decl, expr* > entry_point_type;
private:
typedef obj_map<expr, value_score> scores_type;
typedef obj_map<expr, ptr_vector<expr> > uplinks_type;
typedef obj_map<expr, ptr_vector<func_decl> > occ_type;
scores_type m_scores;
uplinks_type m_uplinks;
entry_point_type m_entry_points;
ptr_vector<func_decl> m_constants;
ptr_vector<func_decl> m_temp_constants;
occ_type m_constants_occ;
public:
sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) :
m_manager(m),
m_mpz_manager(mm),
m_bv_util(bvu),
m_powers(p),
m_random_bits_cnt(0),
m_zero(m_mpz_manager.mk_z(0)),
m_one(m_mpz_manager.mk_z(1)),
m_two(m_mpz_manager.mk_z(2)) {
}
~sls_tracker() {
m_mpz_manager.del(m_zero);
m_mpz_manager.del(m_one);
m_mpz_manager.del(m_two);
}
inline void set_value(expr * n, const mpz & r) {
SASSERT(m_scores.contains(n));
m_mpz_manager.set(m_scores.find(n).value, r);
}
inline void set_value(func_decl * fd, const mpz & r) {
SASSERT(m_entry_points.contains(fd));
expr * ep = get_entry_point(fd);
set_value(ep, r);
}
inline mpz & get_value(expr * n) {
SASSERT(m_scores.contains(n));
return m_scores.find(n).value;
}
inline mpz & get_value(func_decl * fd) {
SASSERT(m_entry_points.contains(fd));
expr * ep = get_entry_point(fd);
return get_value(ep);
}
inline void set_score(expr * n, double score) {
SASSERT(m_scores.contains(n));
m_scores.find(n).score = score;
}
inline void set_score(func_decl * fd, double score) {
SASSERT(m_entry_points.contains(fd));
expr * ep = get_entry_point(fd);
set_score(ep, score);
}
inline double & get_score(expr * n) {
SASSERT(m_scores.contains(n));
return m_scores.find(n).score;
}
inline double & get_score(func_decl * fd) {
SASSERT(m_entry_points.contains(fd));
expr * ep = get_entry_point(fd);
return get_score(ep);
}
inline unsigned get_distance(expr * n) {
SASSERT(m_scores.contains(n));
return m_scores.find(n).distance;
}
inline void set_distance(expr * n, unsigned d) {
SASSERT(m_scores.contains(n));
m_scores.find(n).distance = d;
}
inline expr * get_entry_point(func_decl * fd) {
SASSERT(m_entry_points.contains(fd));
return m_entry_points.find(fd);
}
inline entry_point_type const & get_entry_points() {
return m_entry_points;
}
inline bool has_uplinks(expr * n) {
return m_uplinks.contains(n);
}
inline ptr_vector<expr> & get_uplinks(expr * n) {
SASSERT(m_uplinks.contains(n));
return m_uplinks.find(n);
}
void initialize(app * n) {
// Build score table
if (!m_scores.contains(n)) {
value_score vs;
vs.m = & m_mpz_manager;
m_scores.insert(n, vs);
}
// Update uplinks
unsigned na = n->get_num_args();
for (unsigned i = 0; i < na; i++) {
expr * c = n->get_arg(i);
uplinks_type::obj_map_entry * entry = m_uplinks.insert_if_not_there2(c, ptr_vector<expr>());
entry->get_data().m_value.push_back(n);
}
func_decl * d = n->get_decl();
if (n->get_num_args() == 0) {
if (d->get_family_id() != null_family_id) {
// Interpreted constant
mpz t;
value2mpz(n, t);
set_value(n, t);
m_mpz_manager.del(t);
}
else {
// Uninterpreted constant
m_entry_points.insert_if_not_there(d, n);
m_constants.push_back(d);
}
}
}
struct init_proc {
ast_manager & m_manager;
sls_tracker & m_tracker;
init_proc(ast_manager & m, sls_tracker & tracker):
m_manager(m),
m_tracker(tracker) {
}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
m_tracker.initialize(n);
}
};
struct find_func_decls_proc {
ast_manager & m_manager;
ptr_vector<func_decl> & m_occs;
find_func_decls_proc (ast_manager & m, ptr_vector<func_decl> & occs):
m_manager(m),
m_occs(occs) {
}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
if (n->get_num_args() != 0)
return;
func_decl * d = n->get_decl();
if (d->get_family_id() != null_family_id)
return;
m_occs.push_back(d);
}
};
void calculate_expr_distances(goal_ref const & g) {
// precondition: m_scores is set up.
unsigned sz = g->size();
ptr_vector<app> stack;
for (unsigned i = 0; i < sz; i++)
stack.push_back(to_app(g->form(i)));
while (!stack.empty()) {
app * cur = stack.back();
stack.pop_back();
unsigned d = get_distance(cur);
for (unsigned i = 0; i < cur->get_num_args(); i++) {
app * child = to_app(cur->get_arg(i));
unsigned d_child = get_distance(child);
if (d >= d_child) {
set_distance(child, d+1);
stack.push_back(child);
}
}
}
}
void initialize(goal_ref const & g) {
init_proc proc(m_manager, *this);
expr_mark visited;
unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
for_each_expr(proc, visited, e);
}
visited.reset();
for (unsigned i = 0; i < sz; i++) {
expr * e = g->form(i);
ptr_vector<func_decl> t;
m_constants_occ.insert_if_not_there(e, t);
find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e));
expr_fast_mark1 visited;
quick_for_each_expr(ffd_proc, visited, e);
}
calculate_expr_distances(g);
TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); );
}
void show_model(std::ostream & out) {
unsigned sz = get_num_constants();
for (unsigned i = 0; i < sz; i++) {
func_decl * fd = get_constant(i);
out << fd->get_name() << " = " << m_mpz_manager.to_string(get_value(fd)) << std::endl;
}
}
model_ref get_model() {
model_ref res = alloc(model, m_manager);
unsigned sz = get_num_constants();
for (unsigned i = 0; i < sz; i++) {
func_decl * fd = get_constant(i);
res->register_decl(fd, mpz2value(fd->get_range(), get_value(fd)));
}
return res;
}
unsigned get_num_constants() {
return m_constants.size();
}
ptr_vector<func_decl> & get_constants() {
return m_constants;
}
func_decl * get_constant(unsigned i) {
return m_constants[i];
}
void set_random_seed(unsigned s) {
m_rng.set_seed(s);
}
mpz get_random_bv(sort * s) {
SASSERT(m_bv_util.is_bv_sort(s));
unsigned bv_size = m_bv_util.get_bv_size(s);
mpz r; m_mpz_manager.set(r, 0);
mpz temp;
do
{
m_mpz_manager.mul(r, m_two, temp);
m_mpz_manager.add(temp, get_random_bool(), r);
} while (--bv_size > 0);
m_mpz_manager.del(temp);
return r;
}
mpz & get_random_bool() {
if (m_random_bits_cnt == 0) {
m_random_bits = m_rng();
m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness.
}
bool val = (m_random_bits & 0x01) != 0;
m_random_bits = m_random_bits >> 1;
m_random_bits_cnt--;
return (val) ? m_one : m_zero;
}
unsigned get_random_uint(unsigned bits) {
if (m_random_bits_cnt == 0) {
m_random_bits = m_rng();
m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness.
}
unsigned val = 0;
while (bits-- > 0) {
if ((m_random_bits & 0x01) != 0) val++;
val <<= 1;
m_random_bits >>= 1;
m_random_bits_cnt--;
if (m_random_bits_cnt == 0) {
m_random_bits = m_rng();
m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness.
}
}
return val;
}
mpz get_random(sort * s) {
if (m_bv_util.is_bv_sort(s))
return get_random_bv(s);
else if (m_manager.is_bool(s))
return get_random_bool();
else
NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
}
void randomize() {
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
func_decl * fd = it->m_key;
sort * s = fd->get_range();
mpz temp = get_random(s);
set_value(it->m_value, temp);
m_mpz_manager.del(temp);
}
TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); );
}
#define _SCORE_AND_MIN
double score_bool(expr * n, bool negated = false) {
TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; );
double res = 0.0;
if (is_uninterp_const(n)) {
const mpz & r = get_value(n);
if (negated)
res = (m_mpz_manager.is_one(r)) ? 0.0 : 1.0;
else
res = (m_mpz_manager.is_one(r)) ? 1.0 : 0.0;
}
else if (m_manager.is_and(n)) {
SASSERT(!negated);
app * a = to_app(n);
expr * const * args = a->get_args();
#ifdef _SCORE_AND_MIN
double min = 1.0;
for (unsigned i = 0; i < a->get_num_args(); i++) {
double cur = get_score(args[i]);
if (cur < min) min = cur;
}
res = min;
#else
double sum = 0.0;
for (unsigned i = 0; i < a->get_num_args(); i++)
sum += get_score(args[i]);
res = sum / (double) a->get_num_args();
#endif
}
else if (m_manager.is_or(n)) {
SASSERT(!negated);
app * a = to_app(n);
expr * const * args = a->get_args();
double max = 0.0;
for (unsigned i = 0; i < a->get_num_args(); i++) {
double cur = get_score(args[i]);
if (cur > max) max = cur;
}
res = max;
}
else if (m_manager.is_ite(n)) {
SASSERT(!negated);
app * a = to_app(n);
SASSERT(a->get_num_args() == 3);
const mpz & cond = get_value(a->get_arg(0));
double s_t = get_score(a->get_arg(1));
double s_f = get_score(a->get_arg(2));
res = (m_mpz_manager.is_one(cond)) ? s_t : s_f;
}
else if (m_manager.is_eq(n) || m_manager.is_iff(n)) {
app * a = to_app(n);
SASSERT(a->get_num_args() == 2);
expr * arg0 = a->get_arg(0);
expr * arg1 = a->get_arg(1);
const mpz & v0 = get_value(arg0);
const mpz & v1 = get_value(arg1);
if (negated) {
res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0;
TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " <<
m_mpz_manager.to_string(v1) << std::endl; );
}
else if (m_manager.is_bool(arg0)) {
res = m_mpz_manager.eq(v0, v1) ? 1.0 : 0.0;
TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " <<
m_mpz_manager.to_string(v1) << std::endl; );
}
else if (m_bv_util.is_bv(arg0)) {
mpz diff, diff_m1;
m_mpz_manager.bitwise_xor(v0, v1, diff);
unsigned hamming_distance = 0;
unsigned bv_sz = m_bv_util.get_bv_size(arg0);
#if 1 // unweighted hamming distance
while (!m_mpz_manager.is_zero(diff)) {
//m_mpz_manager.set(diff_m1, diff);
//m_mpz_manager.dec(diff_m1);
//m_mpz_manager.bitwise_and(diff, diff_m1, diff);
//hamming_distance++;
if (!m_mpz_manager.is_even(diff)) {
hamming_distance++;
}
m_mpz_manager.machine_div(diff, m_two, diff);
}
res = 1.0 - (hamming_distance / (double) bv_sz);
#else
rational r(diff);
r /= m_powers(bv_sz);
double dbl = r.get_double();
res = (dbl < 0.0) ? 1.0 : (dbl > 1.0) ? 0.0 : 1.0 - dbl;
#endif
TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " <<
m_mpz_manager.to_string(v1) << " ; HD = " << hamming_distance <<
" ; SZ = " << bv_sz << std::endl; );
m_mpz_manager.del(diff);
m_mpz_manager.del(diff_m1);
}
else
NOT_IMPLEMENTED_YET();
}
else if (m_bv_util.is_bv_ule(n)) { // x <= y
app * a = to_app(n);
SASSERT(a->get_num_args() == 2);
const mpz & x = get_value(a->get_arg(0));
const mpz & y = get_value(a->get_arg(1));
unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]);
if (negated) {
if (m_mpz_manager.gt(x, y))
res = 1.0;
else {
mpz diff;
m_mpz_manager.sub(y, x, diff);
m_mpz_manager.inc(diff);
rational n(diff);
n /= rational(m_powers(bv_sz));
double dbl = n.get_double();
// In extreme cases, n is 0.9999 but to_double returns something > 1.0
res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
m_mpz_manager.del(diff);
}
}
else {
if (m_mpz_manager.le(x, y))
res = 1.0;
else {
mpz diff;
m_mpz_manager.sub(x, y, diff);
rational n(diff);
n /= rational(m_powers(bv_sz));
double dbl = n.get_double();
res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl;
m_mpz_manager.del(diff);
}
}
TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " <<
m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; );
}
else if (m_bv_util.is_bv_sle(n)) { // x <= y
app * a = to_app(n);
SASSERT(a->get_num_args() == 2);
mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0)));
mpz y; m_mpz_manager.set(y, get_value(a->get_arg(1)));
unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]);
const mpz & p = m_powers(bv_sz);
const mpz & p_half = m_powers(bv_sz-1);
if (x >= p_half) { m_mpz_manager.sub(x, p, x); }
if (y >= p_half) { m_mpz_manager.sub(y, p, y); }
if (negated) {
if (x > y)
res = 1.0;
else {
mpz diff;
m_mpz_manager.sub(y, x, diff);
m_mpz_manager.inc(diff);
rational n(diff);
n /= p;
double dbl = n.get_double();
res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
m_mpz_manager.del(diff);
}
TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " <<
m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; );
}
else {
if (x <= y)
res = 1.0;
else {
mpz diff;
m_mpz_manager.sub(x, y, diff);
rational n(diff);
n /= p;
double dbl = n.get_double();
res = (dbl > 1.0) ? 1.0 : (dbl < 0.0) ? 0.0 : dbl;
m_mpz_manager.del(diff);
}
TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " <<
m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; );
}
m_mpz_manager.del(x);
m_mpz_manager.del(y);
}
else if (m_manager.is_not(n)) {
SASSERT(!negated);
app * a = to_app(n);
SASSERT(a->get_num_args() == 1);
expr * child = a->get_arg(0);
if (m_manager.is_and(child) || m_manager.is_or(child)) // Precondition: Assertion set is in NNF.
NOT_IMPLEMENTED_YET();
res = score_bool(child, true);
}
else if (m_manager.is_distinct(n)) {
app * a = to_app(n);
unsigned pairs = 0, distinct_pairs = 0;
unsigned sz = a->get_num_args();
for (unsigned i = 0; i < sz; i++) {
for (unsigned j = i+1; j < sz; j++) {
// pair i/j
const mpz & v0 = get_value(a->get_arg(0));
const mpz & v1 = get_value(a->get_arg(1));
pairs++;
if (v0 != v1)
distinct_pairs++;
}
}
res = (distinct_pairs/(double)pairs);
if (negated) res = 1.0 - res;
}
else
NOT_IMPLEMENTED_YET();
SASSERT(res >= 0.0 && res <= 1.0);
TRACE("sls_score", tout << "SCORE = " << res << std::endl; );
return res;
}
double score_bv(expr * n) {
return 0.0; // a bv-expr is always scored as 0.0; we won't use those scores.
}
void value2mpz(expr * n, mpz & result) {
m_mpz_manager.set(result, m_zero);
if (m_manager.is_bool(n)) {
m_mpz_manager.set(result, m_manager.is_true(n) ? m_one : m_zero);
}
else if (m_bv_util.is_bv(n)) {
unsigned bv_sz = m_bv_util.get_bv_size(n);
rational q;
if (!m_bv_util.is_numeral(n, q, bv_sz))
NOT_IMPLEMENTED_YET();
mpq temp = q.to_mpq();
SASSERT(m_mpz_manager.is_one(temp.denominator()));
m_mpz_manager.set(result, temp.numerator());
}
else
NOT_IMPLEMENTED_YET();
}
expr_ref mpz2value(sort * s, const mpz & r) {
expr_ref res(m_manager);
if (m_manager.is_bool(s))
res = (m_mpz_manager.is_zero(r)) ? m_manager.mk_false() : m_manager.mk_true();
else if (m_bv_util.is_bv_sort(s)) {
rational rat(r);
res = m_bv_util.mk_numeral(rat, s);
}
else
NOT_IMPLEMENTED_YET();
return res;
}
double score(expr * n) {
if (m_manager.is_bool(n))
return score_bool(n);
else if (m_bv_util.is_bv(n))
return score_bv(n);
else
NOT_IMPLEMENTED_YET();
}
ptr_vector<func_decl> & get_unsat_constants(goal_ref const & g) {
unsigned sz = g->size();
if (sz == 1) {
return get_constants();
}
else {
m_temp_constants.reset();
for (unsigned i = 0; i < sz; i++) {
expr * q = g->form(i);
if (m_mpz_manager.eq(get_value(q), m_one))
continue;
ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q);
unsigned sz2 = this_decls.size();
for (unsigned j = 0; j < sz2; j++) {
func_decl * fd = this_decls[j];
if (!m_temp_constants.contains(fd))
m_temp_constants.push_back(fd);
}
}
return m_temp_constants;
}
}
};
#endif

2
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -43,6 +43,8 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
simp2_p.set_bool("push_ite_bv", false);
simp2_p.set_bool("local_ctx", true);
simp2_p.set_uint("local_ctx_limit", 10000000);
simp2_p.set_bool("flat", true); // required by som
simp2_p.set_bool("hoist_mul", false); // required by som
params_ref local_ctx_p = p;
local_ctx_p.set_bool("local_ctx", true);

56
src/test/expr_substitution.cpp Normal file
View file

@ -0,0 +1,56 @@
#include "expr_substitution.h"
#include "smt_params.h"
#include "substitution.h"
#include "unifier.h"
#include "bv_decl_plugin.h"
#include "ast_pp.h"
#include "arith_decl_plugin.h"
#include "reg_decl_plugins.h"
#include "th_rewriter.h"
expr* mk_bv_xor(bv_util& bv, expr* a, expr* b) {
expr* args[2];
args[0] = a;
args[1] = b;
return bv.mk_bv_xor(2, args);
}
expr* mk_bv_and(bv_util& bv, expr* a, expr* b) {
expr* args[2];
args[0] = a;
args[1] = b;
ast_manager& m = bv.get_manager();
return m.mk_app(bv.get_family_id(), OP_BAND, 2, args);
}
void tst_expr_substitution() {
memory::initialize(0);
ast_manager m;
reg_decl_plugins(m);
bv_util bv(m);
expr_ref a(m), b(m), c(m), d(m);
expr_ref x(m);
expr_ref new_a(m);
proof_ref pr(m);
x = m.mk_const(symbol("x"), bv.mk_sort(8));
a = mk_bv_and(bv, mk_bv_xor(bv, x,bv.mk_numeral(8,8)), mk_bv_xor(bv,x,x));
b = x;
c = bv.mk_bv_sub(x, bv.mk_numeral(4, 8));
expr_substitution subst(m);
th_rewriter rw(m);
// normalizing c does not help.
rw(c, d, pr);
subst.insert(b, d);
rw.set_substitution(&subst);
enable_trace("th_rewriter_step");
rw(a, new_a, pr);
std::cout << mk_pp(new_a, m) << "\n";
}

1
src/test/main.cpp
View file

@ -215,6 +215,7 @@ int main(int argc, char ** argv) {
TST(rcf);
TST(polynorm);
TST(qe_arith);
TST(expr_substitution);
}
void initialize_mam() {}