diff --git a/contrib/qprofdiff/Makefile b/contrib/qprofdiff/Makefile new file mode 100644 index 000000000..6b90bed51 --- /dev/null +++ b/contrib/qprofdiff/Makefile @@ -0,0 +1,7 @@ +qprofdiff: main.cpp + $(CXX) $(CXXFLAGS) main.cpp -o qprofdiff + +all: qprofdiff + +clean: + rm -f qprofdiff diff --git a/contrib/qprofdiff/main.cpp b/contrib/qprofdiff/main.cpp new file mode 100644 index 000000000..58d21b77d --- /dev/null +++ b/contrib/qprofdiff/main.cpp @@ -0,0 +1,284 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + main.cpp + +Abstract: + + Main file for qprofdiff. + +Author: + + Christoph M. Wintersteiger (cwinter) + +Revision History: +--*/ +#include +#include + +#include +#include +#include +#include +#include +#include +#include + +using namespace std; + +set options; + +// Profile format: +// [quantifier_instances] qname : num_instances : max_generation : max_cost_s +const string prefix = "[quantifier_instances]"; +unsigned prefix_len = prefix.length(); +typedef struct { unsigned num_instances, max_generation, max_cost; } map_entry; + +string trim(string str) { + size_t linx = str.find_first_not_of(' '); + size_t rinx = str.find_last_not_of(' '); + return str.substr(linx, rinx-linx+1); +} + +int parse(string const & filename, map & data) { + ifstream fs(filename.c_str()); + + if (!fs.is_open()) { + cout << "Can't open file '" << filename << "'" << endl; + return ENOENT; + } + + string qid; + string tokens[4]; + unsigned cur_token = 0; + + while (!fs.eof()) { + string line; + getline(fs, line); + + if (line.substr(0, prefix_len) == prefix) { + line = trim(line.substr(prefix_len)); + size_t from = 0, ti = 0; + for (size_t inx = line.find(':', from); + inx != string::npos; + inx = line.find(':', from)) { + tokens[ti] = trim(line.substr(from, inx-from)); + from = inx+1; + ti++; + } + if (from != line.length() && ti < 4) + tokens[ti] = trim(line.substr(from)); + + qid = tokens[0]; + + if (data.find(qid) == data.end()) { + map_entry & entry = data[qid]; + entry.num_instances = entry.max_generation = entry.max_cost = 0; + } + + map_entry & entry = data[qid]; + entry.num_instances = atoi(tokens[1].c_str()); + entry.max_generation = (unsigned)atoi(tokens[2].c_str()); + entry.max_cost = (unsigned)atoi(tokens[3].c_str()); + } + } + + fs.close(); + + return 0; +} + +void display_data(map & data) { + for (map::iterator it = data.begin(); + it != data.end(); + it++) + cout << it->first << ": " << it->second.num_instances << + ", " << it->second.max_generation << + ", " << it->second.max_cost << endl; +} + + +typedef struct { + int d_num_instances, d_max_generation, d_max_cost; + bool left_only, right_only; +} diff_entry; + +typedef struct { string qid; diff_entry e; } diff_item; + +#define DIFF_LT(X) bool diff_item_lt_ ## X (diff_item const & l, diff_item const & r) { \ + int l_lt_r = l.e.d_ ## X < r.e.d_ ## X; \ + int l_eq_r = l.e.d_ ## X == r.e.d_ ## X; \ + return \ + l.e.left_only ? (r.e.left_only ? ((l_eq_r) ? l.qid < r.qid : l_lt_r) : false) : \ + l.e.right_only ? (r.e.right_only ? ((l_eq_r) ? l.qid < r.qid : l_lt_r) : true) : \ + r.e.right_only ? false : \ + r.e.left_only ? true : \ + l_lt_r; \ +} + +DIFF_LT(num_instances) +DIFF_LT(max_generation) +DIFF_LT(max_cost) + +int indicate(diff_entry const & e, bool suppress_unchanged) { + if (e.left_only) { + cout << "< "; + return INT_MIN; + } + else if (e.right_only) { + cout << "> "; + return INT_MAX; + } + else { + int const & delta = + (options.find("-si") != options.end()) ? e.d_num_instances : + (options.find("-sg") != options.end()) ? e.d_max_generation : + (options.find("-sc") != options.end()) ? e.d_max_cost : + e.d_num_instances; + + if (delta < 0) + cout << "+ "; + else if (delta > 0) + cout << "- "; + else if (delta == 0 && !suppress_unchanged) + cout << "= "; + + return delta; + } +} + +void diff(map & left, map & right) { + map diff_data; + + for (map::const_iterator lit = left.begin(); + lit != left.end(); + lit++) { + string const & qid = lit->first; + map_entry const & lentry = lit->second; + + map::const_iterator rit = right.find(qid); + if (rit != right.end()) { + map_entry const & rentry = rit->second; + diff_entry & de = diff_data[qid]; + + de.left_only = de.right_only = false; + de.d_num_instances = lentry.num_instances - rentry.num_instances; + de.d_max_generation = lentry.max_generation - rentry.max_generation; + de.d_max_cost = lentry.max_cost - rentry.max_cost; + } + else { + diff_entry & de = diff_data[qid]; + de.left_only = true; + de.right_only = false; + de.d_num_instances = lentry.num_instances; + de.d_max_generation = lentry.max_generation; + de.d_max_cost = lentry.max_cost; + } + } + + for (map::const_iterator rit = right.begin(); + rit != right.end(); + rit++) { + string const & qid = rit->first; + map_entry const & rentry = rit->second; + + map::const_iterator lit = left.find(qid); + if (lit == left.end()) { + diff_entry & de = diff_data[qid]; + de.left_only = false; + de.right_only = true; + de.d_num_instances = -(int)rentry.num_instances; + de.d_max_generation = -(int)rentry.max_generation; + de.d_max_cost = -(int)rentry.max_cost; + } + } + + vector flat_data; + for (map::const_iterator it = diff_data.begin(); + it != diff_data.end(); + it++) { + flat_data.push_back(diff_item()); + flat_data.back().qid = it->first; + flat_data.back().e = it->second; + } + + stable_sort(flat_data.begin(), flat_data.end(), + options.find("-si") != options.end() ? diff_item_lt_num_instances: + options.find("-sg") != options.end() ? diff_item_lt_max_generation : + options.find("-sc") != options.end() ? diff_item_lt_max_cost : + diff_item_lt_num_instances); + + bool suppress_unchanged = options.find("-n") != options.end(); + + for (vector::const_iterator it = flat_data.begin(); + it != flat_data.end(); + it++) { + diff_item const & d = *it; + string const & qid = d.qid; + diff_entry const & e = d.e; + + int delta = indicate(e, suppress_unchanged); + + if (!(delta == 0 && suppress_unchanged)) + cout << qid << " (" << + (e.d_num_instances > 0 ? "" : "+") << -e.d_num_instances << " inst., " << + (e.d_max_generation > 0 ? "" : "+") << -e.d_max_generation << " max. gen., " << + (e.d_max_cost > 0 ? "" : "+") << -e.d_max_cost << " max. cost)" << + endl; + } +} + +void display_usage() { + cout << "Usage: qprofdiff [options] " << endl; + cout << "Options:" << endl; + cout << " -n Suppress unchanged items" << endl; + cout << " -si Sort by difference in number of instances" << endl; + cout << " -sg Sort by difference in max. generation" << endl; + cout << " -sc Sort by difference in max. cost" << endl; +} + +int main(int argc, char ** argv) { + char * filename1 = 0; + char * filename2 = 0; + + for (int i = 1; i < argc; i++) { + int len = string(argv[i]).length(); + if (len > 1 && argv[i][0] == '-') { + options.insert(string(argv[i])); + } + else if (filename1 == 0) + filename1 = argv[i]; + else if (filename2 == 0) + filename2 = argv[i]; + else { + cout << "Invalid argument: " << argv[i] << endl << endl; + display_usage(); + return EINVAL; + } + } + + if (filename1 == 0 || filename2 == 0) { + cout << "Two filenames required." << endl << endl; + display_usage(); + return EINVAL; + } + + + cout << "Comparing " << filename1 << " to " << filename2 << endl; + + map data1, data2; + + int r = parse(filename1, data1); + if (r != 0) return r; + r = parse(filename2, data2); + if (r != 0) return r; + + // display_data(data1); + // display_data(data2); + + diff(data1, data2); + + return 0; +} diff --git a/contrib/qprofdiff/qprofdiff.vcxproj b/contrib/qprofdiff/qprofdiff.vcxproj new file mode 100644 index 000000000..b6584e126 --- /dev/null +++ b/contrib/qprofdiff/qprofdiff.vcxproj @@ -0,0 +1,137 @@ + + + + + Debug + Win32 + + + Release + Win32 + + + Debug + x64 + + + Release + x64 + + + + 15.0 + {96E7E3EF-4162-474D-BD32-C702632AAF2B} + qprofdiff + 8.1 + + + + Application + true + v141 + NotSet + + + Application + false + v141 + true + MultiByte + + + Application + true + v141 + MultiByte + + + Application + false + v141 + true + MultiByte + + + + + + + + + + + + + + + + + + + + + $(IncludePath) + $(LibraryPath) + + + $(IncludePath) + $(LibraryPath) + + + + Level3 + Disabled + true + MultiThreadedDebugDLL + ..\..\src\util;%(AdditionalIncludeDirectories) + + + ProgramDatabase + + + $(LibraryPath);%(AdditionalLibraryDirectories) + + + + + Level3 + Disabled + true + ..\..\src\util;%(AdditionalIncludeDirectories) + + + + + Level3 + MaxSpeed + true + true + true + ..\..\src\util;%(AdditionalIncludeDirectories) + + + true + true + + + + + Level3 + MaxSpeed + true + true + true + ..\..\src\util;%(AdditionalIncludeDirectories) + + + true + true + + + + + + + + + \ No newline at end of file diff --git a/contrib/qprofdiff/qprofdiff.vcxproj.filters b/contrib/qprofdiff/qprofdiff.vcxproj.filters new file mode 100644 index 000000000..0d8d9e457 --- /dev/null +++ b/contrib/qprofdiff/qprofdiff.vcxproj.filters @@ -0,0 +1,22 @@ + + + + + {4FC737F1-C7A5-4376-A066-2A32D752A2FF} + cpp;c;cc;cxx;def;odl;idl;hpj;bat;asm;asmx + + + {93995380-89BD-4b04-88EB-625FBE52EBFB} + h;hh;hpp;hxx;hm;inl;inc;xsd + + + {67DA6AB6-F800-4c08-8B7A-83BB121AAD01} + rc;ico;cur;bmp;dlg;rc2;rct;bin;rgs;gif;jpg;jpeg;jpe;resx;tiff;tif;png;wav;mfcribbon-ms + + + + + Source Files + + + \ No newline at end of file diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index bf64aa571..e87b9446f 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -69,14 +69,17 @@ extern "C" { } expr * const* ps = reinterpret_cast(patterns); expr * const* no_ps = reinterpret_cast(no_patterns); - pattern_validator v(mk_c(c)->m()); - for (unsigned i = 0; i < num_patterns; i++) { - if (!v(num_decls, ps[i], 0, 0)) { - SET_ERROR_CODE(Z3_INVALID_PATTERN); - return 0; + symbol qid = to_symbol(quantifier_id); + bool is_rec = mk_c(c)->m().rec_fun_qid() == qid; + if (!is_rec) { + pattern_validator v(mk_c(c)->m()); + for (unsigned i = 0; i < num_patterns; i++) { + if (!v(num_decls, ps[i], 0, 0)) { + SET_ERROR_CODE(Z3_INVALID_PATTERN); + return 0; + } } } - sort* const* ts = reinterpret_cast(sorts); svector names; for (unsigned i = 0; i < num_decls; ++i) { @@ -88,7 +91,7 @@ extern "C" { (0 != is_forall), names.size(), ts, names.c_ptr(), to_expr(body), weight, - to_symbol(quantifier_id), + qid, to_symbol(skolem_id), num_patterns, ps, num_no_patterns, no_ps diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 16d7fbb5f..568ffe9a2 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3701,12 +3701,8 @@ def Extract(high, low, a): high = StringVal(high) if is_seq(high): s = high - offset = _py2expr(low, high.ctx) - length = _py2expr(a, high.ctx) - - if __debug__: - _z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers") - return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) + offset, length = _coerce_exprs(low, a, s.ctx) + return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) if __debug__: _z3_assert(low <= high, "First argument must be greater than or equal to second argument") _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 546f037de..1c01496cf 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -35,7 +35,7 @@ struct arith_decl_plugin::algebraic_numbers_wrapper { ~algebraic_numbers_wrapper() { } - + unsigned mk_id(algebraic_numbers::anum const & val) { SASSERT(!m_amanager.is_rational(val)); unsigned new_id = m_id_gen.mk(); @@ -121,7 +121,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { m_int_decl = m->mk_sort(symbol("Int"), sort_info(id, INT_SORT)); m->inc_ref(m_int_decl); sort * i = m_int_decl; - + sort * b = m->mk_bool_sort(); #define MK_PRED(FIELD, NAME, KIND, SORT) { \ @@ -140,7 +140,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { MK_PRED(m_i_ge_decl, ">=", OP_GE, i); MK_PRED(m_i_lt_decl, "<", OP_LT, i); MK_PRED(m_i_gt_decl, ">", OP_GT, i); - + #define MK_AC_OP(FIELD, NAME, KIND, SORT) { \ func_decl_info info(id, KIND); \ info.set_associative(); \ @@ -205,7 +205,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { MK_UNARY(m_asinh_decl, "asinh", OP_ASINH, r); MK_UNARY(m_acosh_decl, "acosh", OP_ACOSH, r); MK_UNARY(m_atanh_decl, "atanh", OP_ATANH, r); - + func_decl * pi_decl = m->mk_const_decl(symbol("pi"), r, func_decl_info(id, OP_PI)); m_pi = m->mk_const(pi_decl); m->inc_ref(m_pi); @@ -213,7 +213,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { func_decl * e_decl = m->mk_const_decl(symbol("euler"), r, func_decl_info(id, OP_E)); m_e = m->mk_const(e_decl); m->inc_ref(m_e); - + func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT)); m_0_pw_0_int = m->mk_const(z_pw_z_int); m->inc_ref(m_0_pw_0_int); @@ -221,7 +221,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL)); m_0_pw_0_real = m->mk_const(z_pw_z_real); m->inc_ref(m_0_pw_0_real); - + MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r); MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r); MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i); @@ -285,7 +285,8 @@ arith_decl_plugin::arith_decl_plugin(): m_idiv_0_decl(0), m_mod_0_decl(0), m_u_asin_decl(0), - m_u_acos_decl(0) { + m_u_acos_decl(0), + m_convert_int_numerals_to_real(false) { } arith_decl_plugin::~arith_decl_plugin() { @@ -418,7 +419,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { if (val.is_unsigned()) { unsigned u_val = val.get_unsigned(); if (u_val < MAX_SMALL_NUM_TO_CACHE) { - if (is_int) { + if (is_int && !m_convert_int_numerals_to_real) { app * r = m_small_ints.get(u_val, 0); if (r == 0) { parameter p[2] = { parameter(val), parameter(1) }; @@ -442,7 +443,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { } parameter p[2] = { parameter(val), parameter(static_cast(is_int)) }; func_decl * decl; - if (is_int) + if (is_int && !m_convert_int_numerals_to_real) decl = m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p)); else decl = m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p)); @@ -479,14 +480,14 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args } static bool is_const_op(decl_kind k) { - return - k == OP_PI || + return + k == OP_PI || k == OP_E || k == OP_0_PW_0_INT || k == OP_0_PW_0_REAL; } - -func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + +func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, arity); @@ -503,7 +504,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters } } -func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, num_args); @@ -521,9 +522,17 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters } void arith_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { - // TODO: only define Int and Real in the right logics - sort_names.push_back(builtin_name("Int", INT_SORT)); - sort_names.push_back(builtin_name("Real", REAL_SORT)); + if (logic == "NRA" || + logic == "QF_NRA" || + logic == "QF_UFNRA") { + m_convert_int_numerals_to_real = true; + sort_names.push_back(builtin_name("Real", REAL_SORT)); + } + else { + // TODO: only define Int and Real in the right logics + sort_names.push_back(builtin_name("Int", INT_SORT)); + sort_names.push_back(builtin_name("Real", REAL_SORT)); + } } void arith_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { @@ -563,16 +572,16 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con } bool arith_decl_plugin::is_value(app * e) const { - return - is_app_of(e, m_family_id, OP_NUM) || + return + is_app_of(e, m_family_id, OP_NUM) || is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) || is_app_of(e, m_family_id, OP_PI) || is_app_of(e, m_family_id, OP_E); } bool arith_decl_plugin::is_unique_value(app * e) const { - return - is_app_of(e, m_family_id, OP_NUM) || + return + is_app_of(e, m_family_id, OP_NUM) || is_app_of(e, m_family_id, OP_PI) || is_app_of(e, m_family_id, OP_E); } @@ -671,7 +680,7 @@ expr_ref arith_util::mk_mul_simplify(expr_ref_vector const& args) { } expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) { expr_ref result(m_manager); - + switch (sz) { case 0: result = mk_numeral(rational(1), true); @@ -681,7 +690,7 @@ expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) { break; default: result = mk_mul(sz, args); - break; + break; } return result; } @@ -692,7 +701,7 @@ expr_ref arith_util::mk_add_simplify(expr_ref_vector const& args) { } expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { expr_ref result(m_manager); - + switch (sz) { case 0: result = mk_numeral(rational(0), true); @@ -702,7 +711,7 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { break; default: result = mk_add(sz, args); - break; + break; } return result; } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 410c50852..668eebcc9 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -152,6 +152,8 @@ protected: ptr_vector m_small_ints; ptr_vector m_small_reals; + bool m_convert_int_numerals_to_real; + func_decl * mk_func_decl(decl_kind k, bool is_real); virtual void set_manager(ast_manager * m, family_id id); decl_kind fix_kind(decl_kind k, unsigned arity); diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index b663a9df3..773ebefc7 100644 --- a/src/ast/decl_collector.cpp +++ b/src/ast/decl_collector.cpp @@ -23,8 +23,21 @@ void decl_collector::visit_sort(sort * n) { family_id fid = n->get_family_id(); if (m().is_uninterp(n)) m_sorts.push_back(n); - if (fid == m_dt_fid) + if (fid == m_dt_fid) { m_sorts.push_back(n); + + unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n); + for (unsigned i = 0; i < num_cnstr; i++) { + func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i); + m_decls.push_back(cnstr); + ptr_vector const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr); + unsigned num_cas = cnstr_acc.size(); + for (unsigned j = 0; j < num_cas; j++) { + func_decl * accsr = cnstr_acc.get(j); + m_decls.push_back(accsr); + } + } + } } bool decl_collector::is_bool(sort * s) { @@ -38,14 +51,15 @@ void decl_collector::visit_func(func_decl * n) { m_preds.push_back(n); else m_decls.push_back(n); - } + } } decl_collector::decl_collector(ast_manager & m, bool preds): m_manager(m), - m_sep_preds(preds) { + m_sep_preds(preds), + m_dt_util(m) { m_basic_fid = m_manager.get_basic_family_id(); - m_dt_fid = m_manager.mk_family_id("datatype"); + m_dt_fid = m_dt_util.get_family_id(); } void decl_collector::visit(ast* n) { @@ -55,7 +69,7 @@ void decl_collector::visit(ast* n) { n = todo.back(); todo.pop_back(); if (!m_visited.is_marked(n)) { - m_visited.mark(n, true); + m_visited.mark(n, true); switch(n->get_kind()) { case AST_APP: { app * a = to_app(n); @@ -64,7 +78,7 @@ void decl_collector::visit(ast* n) { } todo.push_back(a->get_decl()); break; - } + } case AST_QUANTIFIER: { quantifier * q = to_quantifier(n); unsigned num_decls = q->get_num_decls(); @@ -77,7 +91,7 @@ void decl_collector::visit(ast* n) { } break; } - case AST_SORT: + case AST_SORT: visit_sort(to_sort(n)); break; case AST_FUNC_DECL: { diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index 678f3805d..0067d18eb 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -21,6 +21,7 @@ Revision History: #define SMT_DECL_COLLECTOR_H_ #include"ast.h" +#include"datatype_decl_plugin.h" class decl_collector { ast_manager & m_manager; @@ -28,9 +29,10 @@ class decl_collector { ptr_vector m_sorts; ptr_vector m_decls; ptr_vector m_preds; - ast_mark m_visited; - family_id m_basic_fid; - family_id m_dt_fid; + ast_mark m_visited; + family_id m_basic_fid; + family_id m_dt_fid; + datatype_util m_dt_util; void visit_sort(sort* n); bool is_bool(sort* s); diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index c1d9b36a5..1ac2049ac 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -28,7 +28,7 @@ struct defined_names::impl { typedef obj_map expr2proof; ast_manager & m_manager; symbol m_z3name; - + /** \brief Mapping from expressions to their names. A name is an application. If the expression does not have free variables, then the name is just a constant. @@ -38,25 +38,25 @@ struct defined_names::impl { \brief Mapping from expressions to the apply-def proof. That is, for each expression e, m_expr2proof[e] is the proof e and m_expr2name[2] are observ. equivalent. - + This mapping is not used if proof production is disabled. */ expr2proof m_expr2proof; - + /** \brief Domain of m_expr2name. It is used to keep the expressions alive and for backtracking */ - expr_ref_vector m_exprs; + expr_ref_vector m_exprs; expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive. proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive. - - + + unsigned_vector m_lims; //!< Backtracking support. - + impl(ast_manager & m, char const * prefix); virtual ~impl(); - + app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer & var_names); void cache_new_name(expr * e, app * name); void cache_new_name_intro_proof(expr * e, proof * pr); @@ -106,7 +106,7 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe for (unsigned i = 0; i < num_vars; i++) { sort * s = uv.get(i); if (s) { - domain.push_back(s); + domain.push_back(s); new_args.push_back(m_manager.mk_var(i, s)); var_sorts.push_back(s); } @@ -162,7 +162,7 @@ void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer var_names; - + n = gen_name(e, var_sorts, var_names); cache_new_name(e, n); - + TRACE("mk_definition_bug", tout << "name: " << mk_ismt2_pp(n, m_manager) << "\n";); // variables are in reverse order in quantifiers std::reverse(var_sorts.c_ptr(), var_sorts.c_ptr() + var_sorts.size()); std::reverse(var_names.c_ptr(), var_names.c_ptr() + var_names.size()); - + mk_definition(e, n, var_sorts, var_names, new_def); - + TRACE("mk_definition_bug", tout << "new_def:\n" << mk_ismt2_pp(new_def, m_manager) << "\n";); - + if (m_manager.proofs_enabled()) { new_def_pr = m_manager.mk_def_intro(new_def); pr = m_manager.mk_apply_def(e, n, new_def_pr); @@ -311,11 +311,11 @@ void defined_names::reset() { m_pos_impl->reset(); } -unsigned defined_names::get_num_names() const { +unsigned defined_names::get_num_names() const { return m_impl->get_num_names() + m_pos_impl->get_num_names(); } -func_decl * defined_names::get_name_decl(unsigned i) const { +func_decl * defined_names::get_name_decl(unsigned i) const { SASSERT(i < get_num_names()); unsigned n1 = m_impl->get_num_names(); return i < n1 ? m_impl->get_name_decl(i) : m_pos_impl->get_name_decl(i - n1); diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index 83ed94ece..aef5d8ddd 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -36,7 +36,7 @@ static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) { /** \brief Return true if \c e is of the form (not (= VAR t)) or (not (iff VAR t)) or (iff VAR t) or (iff (not VAR) t) or (VAR IDX) or (not (VAR IDX)). - The last case can be viewed + The last case can be viewed */ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { // (not (= VAR t)) and (not (iff VAR t)) cases @@ -49,7 +49,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { return false; if (!is_var(lhs, num_decls)) std::swap(lhs, rhs); - SASSERT(is_var(lhs, num_decls)); + SASSERT(is_var(lhs, num_decls)); // Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles... // if (occurs(lhs, rhs)) { // return false; @@ -67,7 +67,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { if (is_var(lhs, num_decls) || is_var(rhs, num_decls)) { if (!is_var(lhs, num_decls)) std::swap(lhs, rhs); - SASSERT(is_var(lhs, num_decls)); + SASSERT(is_var(lhs, num_decls)); // Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles... // if (occurs(lhs, rhs)) { // return false; @@ -83,11 +83,11 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { if (!is_neg_var(m_manager, lhs, num_decls)) std::swap(lhs, rhs); SASSERT(is_neg_var(m_manager, lhs, num_decls)); - expr * lhs_var = to_app(lhs)->get_arg(0); + expr * lhs_var = to_app(lhs)->get_arg(0); // Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles... // if (occurs(lhs_var, rhs)) { // return false; - // } + // } v = to_var(lhs_var); t = rhs; TRACE("der", tout << mk_pp(e, m_manager) << "\n";); @@ -134,11 +134,11 @@ void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) { pr = m_manager.mk_transitivity(pr, curr_pr); } } while (q != r && is_quantifier(r)); - + // Eliminate variables that have become unused if (reduced && is_forall(r)) { quantifier * q = to_quantifier(r); - elim_unused_vars(m_manager, q, r); + elim_unused_vars(m_manager, q, params_ref(), r); if (m_manager.proofs_enabled()) { proof * p1 = m_manager.mk_elim_unused_vars(q, r); pr = m_manager.mk_transitivity(pr, p1); @@ -153,24 +153,24 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) { r = q; return; } - + expr * e = q->get_expr(); unsigned num_decls = q->get_num_decls(); var * v = 0; - expr_ref t(m_manager); + expr_ref t(m_manager); if (m_manager.is_or(e)) { unsigned num_args = to_app(e)->get_num_args(); unsigned i = 0; unsigned diseq_count = 0; unsigned largest_vinx = 0; - + m_map.reset(); m_pos2var.reset(); m_inx2var.reset(); - + m_pos2var.reserve(num_args, -1); - + // Find all disequalities for (; i < num_args; i++) { if (is_var_diseq(to_app(e)->get_arg(i), num_decls, v, t)) { @@ -192,7 +192,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) { get_elimination_order(); SASSERT(m_order.size() <= diseq_count); // some might be missing because of cycles - if (!m_order.empty()) { + if (!m_order.empty()) { create_substitution(largest_vinx + 1); apply_substitution(q, r); } @@ -202,22 +202,22 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) { r = q; } } - // Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses. + // Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses. // So, we must perform a occurs check here. else if (is_var_diseq(e, num_decls, v, t) && !occurs(v, t)) { r = m_manager.mk_false(); } - else + else r = q; - + if (m_manager.proofs_enabled()) { pr = r == q ? 0 : m_manager.mk_der(q, r); - } + } } void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsigned_vector & order) { order.reset(); - + // eliminate self loops, and definitions containing quantifiers. bool found = false; for (unsigned i = 0; i < definitions.size(); i++) { @@ -228,7 +228,7 @@ void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsig else found = true; // found at least one candidate } - + if (!found) return; @@ -329,14 +329,14 @@ void der::get_elimination_order() { // der::top_sort ts(m_manager); der_sort_vars(m_inx2var, m_map, m_order); - TRACE("der", + TRACE("der", tout << "Elimination m_order:" << std::endl; for(unsigned i=0; iget_expr(); - unsigned num_args=to_app(e)->get_num_args(); - + unsigned num_args=to_app(e)->get_num_args(); + // get a new expression m_new_args.reset(); for(unsigned i = 0; i < num_args; i++) { int x = m_pos2var[i]; - if (x != -1 && m_map[x] != 0) + if (x != -1 && m_map[x] != 0) continue; // this is a disequality with definition (vanishes) - + m_new_args.push_back(to_app(e)->get_arg(i)); } unsigned sz = m_new_args.size(); expr_ref t(m_manager); t = (sz == 1) ? m_new_args[0] : m_manager.mk_or(sz, m_new_args.c_ptr()); - expr_ref new_e(m_manager); + expr_ref new_e(m_manager); m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e); - + // don't forget to update the quantifier patterns expr_ref_buffer new_patterns(m_manager); expr_ref_buffer new_no_patterns(m_manager); @@ -392,7 +392,7 @@ void der::apply_substitution(quantifier * q, expr_ref & r) { new_no_patterns.push_back(new_nopat); } - r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), + r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), new_no_patterns.size(), new_no_patterns.c_ptr(), new_e); } @@ -404,9 +404,9 @@ struct der_rewriter_cfg : public default_rewriter_cfg { ast_manager & m() const { return m_der.m(); } - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { diff --git a/src/ast/rewriter/rewriter_params.pyg b/src/ast/rewriter/rewriter_params.pyg index 5bd17f556..06500086a 100644 --- a/src/ast/rewriter/rewriter_params.pyg +++ b/src/ast/rewriter/rewriter_params.pyg @@ -8,5 +8,6 @@ def_module_params('rewriter', ("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."), ("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."), ("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."), - ("cache_all", BOOL, False, "cache all intermediate results."))) + ("cache_all", BOOL, False, "cache all intermediate results."), + ("ignore_patterns_on_ground_qbody", BOOL, True, "ignores patterns on quantifiers that don't mention their bound variables."))) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index a62eea6ea..3d7da43a7 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -12,6 +12,7 @@ Abstract: Author: Nikolaj Bjorner (nbjorner) 2015-12-5 + Murphy Berzish 2017-02-21 Notes: @@ -514,30 +515,56 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu bool constantPos = m_autil.is_numeral(b, pos); bool constantLen = m_autil.is_numeral(c, len); - // case 1: pos<0 or len<0 + // case 1: pos<0 or len<=0 // rewrite to "" - if ( (constantPos && pos.is_neg()) || (constantLen && len.is_neg()) ) { + if ( (constantPos && pos.is_neg()) || (constantLen && !len.is_pos()) ) { result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; } // case 1.1: pos >= length(base) // rewrite to "" - if (constantBase && constantPos && pos.get_unsigned() >= s.length()) { + if (constantBase && constantPos && pos >= rational(s.length())) { result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; } + constantPos &= pos.is_unsigned(); + constantLen &= len.is_unsigned(); + if (constantBase && constantPos && constantLen) { if (pos.get_unsigned() + len.get_unsigned() >= s.length()) { // case 2: pos+len goes past the end of the string unsigned _len = s.length() - pos.get_unsigned() + 1; result = m_util.str.mk_string(s.extract(pos.get_unsigned(), _len)); - return BR_DONE; } else { // case 3: pos+len still within string result = m_util.str.mk_string(s.extract(pos.get_unsigned(), len.get_unsigned())); - return BR_DONE; } + return BR_DONE; + } + + if (constantPos && constantLen) { + unsigned _pos = pos.get_unsigned(); + unsigned _len = len.get_unsigned(); + SASSERT(_len > 0); + expr_ref_vector as(m()), bs(m()); + m_util.str.get_concat(a, as); + for (unsigned i = 0; i < as.size() && _len > 0; ++i) { + if (m_util.str.is_unit(as[i].get())) { + if (_pos == 0) { + bs.push_back(as[i].get()); + --_len; + } + else { + --_pos; + } + } + else { + return BR_FAILED; + } + } + result = m_util.str.mk_concat(bs); + return BR_DONE; } return BR_FAILED; @@ -640,10 +667,33 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; } - if (m_util.str.is_string(a, c) && r.is_unsigned() && r < rational(c.length())) { - result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1)); + if (m_util.str.is_string(a, c)) { + if (r.is_unsigned() && r < rational(c.length())) { + result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1)); + } + else { + result = m_util.str.mk_empty(m().get_sort(a)); + } return BR_DONE; - } + } + if (r.is_unsigned()) { + len = r.get_unsigned(); + expr_ref_vector as(m()); + m_util.str.get_concat(a, as); + for (unsigned i = 0; i < as.size(); ++i) { + if (m_util.str.is_unit(as[i].get())) { + if (len == 0) { + result = as[i].get(); + return BR_DONE; + } + --len; + } + else { + return BR_FAILED; + } + } + } + } return BR_FAILED; } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 0c57ea609..b561e02fc 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -54,6 +54,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { bool m_cache_all; bool m_push_ite_arith; bool m_push_ite_bv; + bool m_ignore_patterns_on_ground_qbody; // substitution support expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions @@ -70,8 +71,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_cache_all = p.cache_all(); m_push_ite_arith = p.push_ite_arith(); m_push_ite_bv = p.push_ite_bv(); + m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody(); } - + void updt_params(params_ref const & p) { m_b_rw.updt_params(p); m_a_rw.updt_params(p); @@ -82,7 +84,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { updt_local_params(p); } - bool flat_assoc(func_decl * f) const { + bool flat_assoc(func_decl * f) const { if (!m_flat) return false; family_id fid = f->get_family_id(); if (fid == null_family_id) @@ -98,10 +100,10 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } bool rewrite_patterns() const { return false; } - + bool cache_all_results() const { return m_cache_all; } - bool max_steps_exceeded(unsigned num_steps) const { + bool max_steps_exceeded(unsigned num_steps) const { cooperate("simplifier"); if (memory::get_allocation_size() > m_max_memory) throw rewriter_exception(Z3_MAX_MEMORY_MSG); @@ -179,13 +181,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg { st = m_ar_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(args[0], args[1], result); - + if (st != BR_FAILED) return st; } if (k == OP_EQ || k == OP_IFF) { SASSERT(num == 2); - st = apply_tamagotchi(args[0], args[1], result); + st = apply_tamagotchi(args[0], args[1], result); if (st != BR_FAILED) return st; } @@ -239,13 +241,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } else { if (SWAP) { - result = m().mk_ite(ite->get_arg(0), + result = m().mk_ite(ite->get_arg(0), m().mk_app(p, value, ite->get_arg(1)), m().mk_app(p, value, ite->get_arg(2))); return BR_REWRITE2; } else { - result = m().mk_ite(ite->get_arg(0), + result = m().mk_ite(ite->get_arg(0), m().mk_app(p, ite->get_arg(1), value), m().mk_app(p, ite->get_arg(2), value)); return BR_REWRITE2; @@ -257,7 +259,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { // ite-value-tree := (ite c ) // subtree := value // | (ite c ) - // + // bool is_ite_value_tree(expr * t) { if (!m().is_ite(t)) return false; @@ -281,7 +283,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } return true; } - + br_status pull_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { if (num == 2 && m().is_bool(f->get_range()) && !m().is_bool(args[0])) { if (m().is_ite(args[0])) { @@ -325,7 +327,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (!is_app(t)) return false; family_id fid = to_app(t)->get_family_id(); - return ((fid == m_a_rw.get_fid() && m_push_ite_arith) || + return ((fid == m_a_rw.get_fid() && m_push_ite_arith) || (fid == m_bv_rw.get_fid() && m_push_ite_bv)); } @@ -349,7 +351,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } return false; } - + /** \brief Try to "unify" t1 and t2 Examples @@ -463,7 +465,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } // terms matched... bool is_int = m_a_util.is_int(t1); - if (!new_t1) + if (!new_t1) new_t1 = m_a_util.mk_numeral(rational(0), is_int); if (!new_t2) new_t2 = m_a_util.mk_numeral(rational(0), is_int); @@ -476,7 +478,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { args.push_back(arg); } SASSERT(!args.empty()); - if (args.size() == 1) + if (args.size() == 1) c = args[0]; else c = m_a_util.mk_add(args.size(), args.c_ptr()); @@ -518,7 +520,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { // Apply transformations of the form // - // (ite c (+ k1 a) (+ k2 a)) --> (+ (ite c k1 k2) a) + // (ite c (+ k1 a) (+ k2 a)) --> (+ (ite c k1 k2) a) // (ite c (* k1 a) (* k2 a)) --> (* (ite c k1 k2) a) // // These transformations are useful for bit-vector problems, since @@ -536,7 +538,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (unify(t, e, f_prime, new_t, new_e, common, first)) { if (first) result = m().mk_app(f_prime, common, m().mk_ite(c, new_t, new_e)); - else + else result = m().mk_app(f_prime, m().mk_ite(c, new_t, new_e), common); return BR_DONE; } @@ -558,7 +560,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { result_pr = 0; br_status st = reduce_app_core(f, num, args, result); if (st != BR_DONE && st != BR_FAILED) { - CTRACE("th_rewriter_step", st != BR_FAILED, + CTRACE("th_rewriter_step", st != BR_FAILED, tout << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";); @@ -576,7 +578,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { else st = pull_ite(result); } - CTRACE("th_rewriter_step", st != BR_FAILED, + CTRACE("th_rewriter_step", st != BR_FAILED, tout << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";); @@ -593,28 +595,28 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { quantifier_ref q1(m()); proof * p1 = 0; - if (is_quantifier(new_body) && + if (is_quantifier(new_body) && to_quantifier(new_body)->is_forall() == old_q->is_forall() && !old_q->has_patterns() && !to_quantifier(new_body)->has_patterns()) { - + quantifier * nested_q = to_quantifier(new_body); - + ptr_buffer sorts; - buffer names; + buffer names; sorts.append(old_q->get_num_decls(), old_q->get_decl_sorts()); names.append(old_q->get_num_decls(), old_q->get_decl_names()); sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts()); names.append(nested_q->get_num_decls(), nested_q->get_decl_names()); - + q1 = m().mk_quantifier(old_q->is_forall(), sorts.size(), sorts.c_ptr(), @@ -624,9 +626,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg { old_q->get_qid(), old_q->get_skid(), 0, 0, 0, 0); - + SASSERT(is_well_sorted(m(), q1)); - + if (m().proofs_enabled()) { SASSERT(old_q->get_expr() == new_body); p1 = m().mk_pull_quant(old_q, q1); @@ -635,24 +637,24 @@ struct th_rewriter_cfg : public default_rewriter_cfg { else { ptr_buffer new_patterns_buf; ptr_buffer new_no_patterns_buf; - + new_patterns_buf.append(old_q->get_num_patterns(), new_patterns); new_no_patterns_buf.append(old_q->get_num_no_patterns(), new_no_patterns); remove_duplicates(new_patterns_buf); remove_duplicates(new_no_patterns_buf); - - q1 = m().update_quantifier(old_q, + + q1 = m().update_quantifier(old_q, new_patterns_buf.size(), new_patterns_buf.c_ptr(), new_no_patterns_buf.size(), new_no_patterns_buf.c_ptr(), new_body); TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";); SASSERT(is_well_sorted(m(), q1)); } - - elim_unused_vars(m(), q1, result); + + elim_unused_vars(m(), q1, params_ref(), result); TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m()) << "\n";); - + result_pr = 0; if (m().proofs_enabled()) { proof * p2 = 0; @@ -758,7 +760,7 @@ unsigned th_rewriter::get_num_steps() const { void th_rewriter::cleanup() { ast_manager & m = m_imp->m(); dealloc(m_imp); - m_imp = alloc(imp, m, m_params); + m_imp = alloc(imp, m, m_params); } void th_rewriter::reset() { diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp index 37b335a9d..fd290c8fe 100644 --- a/src/ast/rewriter/var_subst.cpp +++ b/src/ast/rewriter/var_subst.cpp @@ -39,10 +39,16 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";); } +unused_vars_eliminator::unused_vars_eliminator(ast_manager & m, params_ref const & params) : + m(m), m_subst(m), m_params(params) +{ + m_ignore_patterns_on_ground_qbody = m_params.get_bool("ignore_patterns_on_ground_qbody", true); +} + void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { SASSERT(is_well_sorted(m, q)); - if (is_ground(q->get_expr())) { - // ignore patterns if the body is a ground formula. + if (m_ignore_patterns_on_ground_qbody && is_ground(q->get_expr())) { + // Ignore patterns if the body is a ground formula. result = q->get_expr(); return; } @@ -146,8 +152,8 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) { SASSERT(is_well_sorted(m, result)); } -void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) { - unused_vars_eliminator el(m); +void elim_unused_vars(ast_manager & m, quantifier * q, params_ref const & params, expr_ref & result) { + unused_vars_eliminator el(m, params); el(q, result); } diff --git a/src/ast/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h index 9d04cebe3..21aa58399 100644 --- a/src/ast/rewriter/var_subst.h +++ b/src/ast/rewriter/var_subst.h @@ -21,6 +21,7 @@ Notes: #include"rewriter.h" #include"used_vars.h" +#include"params.h" /** \brief Alias for var_shifter class. @@ -31,7 +32,7 @@ typedef var_shifter shift_vars; \brief Variable substitution functor. It substitutes variables by expressions. The expressions may contain variables. */ -class var_subst { +class var_subst { beta_reducer m_reducer; bool m_std_order; public: @@ -39,7 +40,7 @@ public: bool std_order() const { return m_std_order; } /** - When std_order() == true, + When std_order() == true, I'm using the same standard used in quantifier instantiation. (VAR 0) is stored in the last position of the array. ... @@ -55,15 +56,17 @@ public: \brief Eliminate the unused variables from \c q. Store the result in \c r. */ class unused_vars_eliminator { - ast_manager& m; - var_subst m_subst; - used_vars m_used; + ast_manager & m; + var_subst m_subst; + used_vars m_used; + params_ref m_params; + bool m_ignore_patterns_on_ground_qbody; public: - unused_vars_eliminator(ast_manager& m): m(m), m_subst(m) {} + unused_vars_eliminator(ast_manager & m, params_ref const & params); void operator()(quantifier* q, expr_ref& r); }; -void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & r); +void elim_unused_vars(ast_manager & m, quantifier * q, params_ref const & params, expr_ref & r); /** \brief Instantiate quantifier q using the given exprs. @@ -86,7 +89,7 @@ class expr_free_vars { expr_sparse_mark m_mark; ptr_vector m_sorts; ptr_vector m_todo; -public: +public: void reset(); void operator()(expr* e); void accumulate(expr* e); @@ -96,7 +99,7 @@ public: bool contains(unsigned idx) const { return idx < m_sorts.size() && m_sorts[idx] != 0; } void set_default_sort(sort* s); void reverse() { m_sorts.reverse(); } - sort*const* c_ptr() const { return m_sorts.c_ptr(); } + sort*const* c_ptr() const { return m_sorts.c_ptr(); } }; #endif diff --git a/src/ast/simplifier/distribute_forall.cpp b/src/ast/simplifier/distribute_forall.cpp index bd2af5675..78e5d5ded 100644 --- a/src/ast/simplifier/distribute_forall.cpp +++ b/src/ast/simplifier/distribute_forall.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura (leonardo) 2010-04-02. Revision History: - + Christoph Wintersteiger 2010-04-06: Added implementation. --*/ @@ -40,7 +40,7 @@ bool distribute_forall::visit_children(expr * n) { bool visited = true; unsigned j; switch(n->get_kind()) { - case AST_VAR: + case AST_VAR: break; case AST_APP: j = to_app(n)->get_num_args(); @@ -86,15 +86,15 @@ void distribute_forall::reduce1_app(app * a) { SASSERT(is_cached(a->get_arg(j))); expr * c = get_cached(a->get_arg(j)); SASSERT(c!=0); - if (c != a->get_arg(j)) + if (c != a->get_arg(j)) reduced = true; m_new_args[j] = c; - } + } if (reduced) { na = m_manager.mk_app(a->get_decl(), num_args, m_new_args.c_ptr()); } - + cache_result(a, na); } @@ -126,11 +126,11 @@ void distribute_forall::reduce1_quantifier(quantifier * q) { quantifier_ref tmp_q(m_manager); tmp_q = m_manager.update_quantifier(q, not_arg); expr_ref new_q(m_manager); - elim_unused_vars(m_manager, tmp_q, new_q); + elim_unused_vars(m_manager, tmp_q, params_ref(), new_q); new_args.push_back(new_q); } expr_ref result(m_manager); - // m_bsimp.mk_and actually constructs a (not (or ...)) formula, + // m_bsimp.mk_and actually constructs a (not (or ...)) formula, // it will also apply basic simplifications. m_bsimp.mk_and(new_args.size(), new_args.c_ptr(), result); cache_result(q, result); @@ -148,15 +148,15 @@ void distribute_forall::operator()(expr * f, expr_ref & result) { while (!m_todo.empty()) { expr * e = m_todo.back(); - if (visit_children(e)) { + if (visit_children(e)) { m_todo.pop_back(); reduce1(e); - } + } } result = get_cached(f); SASSERT(result!=0); - TRACE("distribute_forall", tout << mk_ll_pp(f, m_manager) << "======>\n" + TRACE("distribute_forall", tout << mk_ll_pp(f, m_manager) << "======>\n" << mk_ll_pp(result, m_manager);); } @@ -166,5 +166,5 @@ expr * distribute_forall::get_cached(expr * n) const { void distribute_forall::cache_result(expr * n, expr * r) { SASSERT(r != 0); - m_cache.insert(n, r); + m_cache.insert(n, r); } diff --git a/src/ast/simplifier/elim_bounds.cpp b/src/ast/simplifier/elim_bounds.cpp index a4e145e0a..7a40b8602 100644 --- a/src/ast/simplifier/elim_bounds.cpp +++ b/src/ast/simplifier/elim_bounds.cpp @@ -32,7 +32,7 @@ elim_bounds::elim_bounds(ast_manager & m): (<= x k) (<= (+ x (* -1 y)) k) - (<= (+ x (* -1 t)) k) + (<= (+ x (* -1 t)) k) (<= (+ t (* -1 x)) k) x and y are a bound variables, t is a ground term and k is a numeral @@ -65,14 +65,14 @@ bool elim_bounds::is_bound(expr * n, var * & lower, var * & upper) { if (neg) le = !le; - + if (is_var(n)) { upper = to_var(n); } else if (m_util.is_add(n) && to_app(n)->get_num_args() == 2) { expr * arg1 = to_app(n)->get_arg(0); expr * arg2 = to_app(n)->get_arg(1); - if (is_var(arg1)) + if (is_var(arg1)) upper = to_var(arg1); else if (!is_ground(arg1)) return false; @@ -95,7 +95,7 @@ bool elim_bounds::is_bound(expr * n, var * & lower, var * & upper) { if (!le) std::swap(upper, lower); - + return true; } @@ -188,7 +188,7 @@ void elim_bounds::operator()(quantifier * q, expr_ref & r) { } quantifier_ref new_q(m_manager); new_q = m_manager.update_quantifier(q, new_body); - elim_unused_vars(m_manager, new_q, r); + elim_unused_vars(m_manager, new_q, params_ref(), r); TRACE("elim_bounds", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";); } @@ -199,10 +199,10 @@ bool elim_bounds_star::visit_quantifier(quantifier * q) { visit(q->get_expr(), visited); return visited; } - + void elim_bounds_star::reduce1_quantifier(quantifier * q) { if (!q->is_forall() || q->get_num_patterns() != 0) { - cache_result(q, q, 0); + cache_result(q, q, 0); return; } quantifier_ref new_q(m); diff --git a/src/ast/simplifier/simplifier.cpp b/src/ast/simplifier/simplifier.cpp index 6f7e62fd4..498244919 100644 --- a/src/ast/simplifier/simplifier.cpp +++ b/src/ast/simplifier/simplifier.cpp @@ -33,8 +33,8 @@ simplifier::simplifier(ast_manager & m): m_ac_support(true) { } -void simplifier::register_plugin(plugin * p) { - m_plugins.register_plugin(p); +void simplifier::register_plugin(plugin * p) { + m_plugins.register_plugin(p); } simplifier::~simplifier() { @@ -46,13 +46,13 @@ void simplifier::enable_ac_support(bool flag) { ptr_vector::const_iterator it = m_plugins.begin(); ptr_vector::const_iterator end = m_plugins.end(); for (; it != end; ++it) { - if (*it != 0) + if (*it != 0) (*it)->enable_ac_support(flag); } } /** - \brief External interface for the simplifier. + \brief External interface for the simplifier. A client will invoke operator()(s, r, p) to simplify s. The result is stored in r. When proof generation is enabled, a proof for the equivalence (or equisatisfiability) @@ -69,14 +69,14 @@ void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) { proof * result_proof; switch (m.proof_mode()) { case PGM_DISABLED: // proof generation is disabled. - reduce_core(s); + reduce_core(s); // after executing reduce_core, the result of the simplification is in the cache get_cached(s, result, result_proof); r = result; p = m.mk_undef_proof(); break; case PGM_COARSE: // coarse proofs... in this case, we do not produce a step by step (fine grain) proof to show the equivalence (or equisatisfiability) of s an r. - m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst. + m_subst_proofs.reset(); // m_subst_proofs is an auxiliary vector that is used to justify substitutions. See comment on method get_subst. reduce_core(s); get_cached(s, result, result_proof); r = result; @@ -163,7 +163,7 @@ bool simplifier::visit_children(expr * n) { // The method ast_manager::mk_app is used to create the flat version of an AC operator. // In Z3 1.x, we used multi-ary operators. This creates problems for the superposition engine. // So, starting at Z3 2.x, only boolean operators can be multi-ary. - // Example: + // Example: // (and (and a b) (and c d)) --> (and a b c d) // (+ (+ a b) (+ c d)) --> (+ a (+ b (+ c d))) // Remark: The flattening is only applied if m_ac_support is true. @@ -178,7 +178,7 @@ bool simplifier::visit_children(expr * n) { } return visited; } - case AST_QUANTIFIER: + case AST_QUANTIFIER: return visit_quantifier(to_quantifier(n)); default: UNREACHABLE(); @@ -188,7 +188,7 @@ bool simplifier::visit_children(expr * n) { /** \brief Visit the children of n assuming it is an AC (associative-commutative) operator. - + For example, if n is of the form (+ (+ a b) (+ c d)), this method will return true if the nodes a, b, c and d have been already simplified. The nodes (+ a b) and (+ c d) are not really checked. @@ -216,7 +216,7 @@ bool simplifier::visit_ac(app * n) { expr * arg = n->get_arg(i); if (is_app_of(arg, decl)) todo.push_back(to_app(arg)); - else + else visit(arg, visited); } } @@ -319,7 +319,7 @@ void simplifier::reduce1_app_core(app * n) { proof * p; if (n == r) p = 0; - else if (r != s) + else if (r != s) // we use a "theory rewrite generic proof" to justify the step // s = (decl arg_0' ... arg_{n-1}') --> r p = m.mk_transitivity(p1, m.mk_rewrite(s, r)); @@ -368,7 +368,7 @@ void simplifier::reduce1_ac_app_core(app * n) { proof_ref p1(m); mk_ac_congruent_term(n, n_c, p1); TRACE("ac", tout << "expr:\n" << mk_pp(n, m) << "\ncongruent term:\n" << mk_pp(n_c, m) << "\n";); - expr_ref r(m); + expr_ref r(m); func_decl * decl = n->get_decl(); family_id fid = decl->get_family_id(); plugin * p = get_plugin(fid); @@ -415,7 +415,7 @@ void simplifier::reduce1_ac_app_core(app * n) { proof * p; if (n == r.get()) p = 0; - else if (r.get() != n_c.get()) + else if (r.get() != n_c.get()) p = m.mk_transitivity(p1, m.mk_rewrite(n_c, r)); else p = p1; @@ -434,7 +434,7 @@ void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * sprintf_s(buffer, ARRAYSIZE(buffer), "lemma_%d.smt", g_rewrite_lemma_id); #else sprintf(buffer, "rewrite_lemma_%d.smt", g_rewrite_lemma_id); -#endif +#endif ast_smt_pp pp(m); pp.set_benchmark_name("rewrite_lemma"); pp.set_status("unsat"); @@ -450,7 +450,7 @@ void simplifier::dump_rewrite_lemma(func_decl * decl, unsigned num_args, expr * /** \brief Return in \c result an expression \c e equivalent to (f args[0] ... args[num_args - 1]), and store in \c pr a proof for (= (f args[0] ... args[num_args - 1]) e) - + If e is identical to (f args[0] ... args[num_args - 1]), then pr is set to 0. */ void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args, expr_ref & result) { @@ -474,7 +474,7 @@ void simplifier::mk_app(func_decl * decl, unsigned num_args, expr * const * args //dump_rewrite_lemma(decl, num_args, args, result.get()); return; } - + result = m.mk_app(decl, num_args, args); } @@ -494,17 +494,17 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) { proof * arg_proof; get_cached(arg, new_arg, arg_proof); - CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0), + CTRACE("simplifier_bug", (arg != new_arg) != (arg_proof != 0), tout << mk_ll_pp(arg, m) << "\n---->\n" << mk_ll_pp(new_arg, m) << "\n"; tout << "#" << arg->get_id() << " #" << new_arg->get_id() << "\n"; tout << arg << " " << new_arg << "\n";); - - + + if (arg != new_arg) { has_new_args = true; proofs.push_back(arg_proof); SASSERT(arg_proof); - } + } else { SASSERT(arg_proof == 0); } @@ -526,10 +526,10 @@ void simplifier::mk_congruent_term(app * n, app_ref & r, proof_ref & p) { /** \brief Store the new arguments of \c n in result. Store in p a proof for (= n (f result[0] ... result[num_args - 1])), where f is the function symbol of n. - + If there are no new arguments or fine grain proofs are disabled, then p is set to 0. - Return true there are new arguments. + Return true there are new arguments. */ bool simplifier::get_args(app * n, ptr_vector & result, proof_ref & p) { bool has_new_args = false; @@ -565,10 +565,10 @@ bool simplifier::get_args(app * n, ptr_vector & result, proof_ref & p) { void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) { SASSERT(m_ac_support); func_decl * f = n->get_decl(); - + m_ac_cache.reset(); m_ac_pr_cache.reset(); - + ptr_buffer todo; ptr_buffer new_args; ptr_buffer new_arg_prs; @@ -621,7 +621,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) { todo.pop_back(); if (!has_new_arg) { m_ac_cache.insert(curr, curr); - if (m.fine_grain_proofs()) + if (m.fine_grain_proofs()) m_ac_pr_cache.insert(curr, 0); } else { @@ -634,7 +634,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) { } } } - + SASSERT(m_ac_cache.contains(n)); app * new_n = 0; m_ac_cache.find(n, new_n); @@ -646,7 +646,7 @@ void simplifier::mk_ac_congruent_term(app * n, app_ref & r, proof_ref & p) { } } -#define White 0 +#define White 0 #define Grey 1 #define Black 2 @@ -688,7 +688,7 @@ void simplifier::ac_top_sort(app * n, ptr_buffer & result) { while (!todo.empty()) { expr * curr = todo.back(); int color; - obj_map::obj_map_entry * entry = colors.insert_if_not_there2(curr, White); + obj_map::obj_map_entry * entry = colors.insert_if_not_there2(curr, White); SASSERT(entry); color = entry->get_data().m_value; switch (color) { @@ -731,7 +731,7 @@ void simplifier::get_ac_args(app * n, ptr_vector & args, vector ac_top_sort(n, sorted_exprs); SASSERT(!sorted_exprs.empty()); SASSERT(sorted_exprs[sorted_exprs.size()-1] == n); - + TRACE("ac", tout << mk_ll_pp(n, m, true, false) << "#" << n->get_id() << "\nsorted expressions...\n"; for (unsigned i = 0; i < sorted_exprs.size(); i++) { tout << "#" << sorted_exprs[i]->get_id() << " "; @@ -747,7 +747,7 @@ void simplifier::get_ac_args(app * n, ptr_vector & args, vector expr * curr = sorted_exprs[j]; rational mult; m_ac_mults.find(curr, mult); - SASSERT(!mult.is_zero()); + SASSERT(!mult.is_zero()); if (is_app_of(curr, decl)) { unsigned num_args = to_app(curr)->get_num_args(); for (unsigned i = 0; i < num_args; i++) { @@ -772,16 +772,16 @@ void simplifier::reduce1_quantifier(quantifier * q) { quantifier_ref q1(m); proof * p1 = 0; - - if (is_quantifier(new_body) && + + if (is_quantifier(new_body) && to_quantifier(new_body)->is_forall() == q->is_forall() && !to_quantifier(q)->has_patterns() && !to_quantifier(new_body)->has_patterns()) { - + quantifier * nested_q = to_quantifier(new_body); ptr_buffer sorts; - buffer names; + buffer names; sorts.append(q->get_num_decls(), q->get_decl_sorts()); names.append(q->get_num_decls(), q->get_decl_names()); sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts()); @@ -797,7 +797,7 @@ void simplifier::reduce1_quantifier(quantifier * q) { q->get_skid(), 0, 0, 0, 0); SASSERT(is_well_sorted(m, q1)); - + if (m.fine_grain_proofs()) { quantifier * q0 = m.update_quantifier(q, new_body); proof * p0 = q == q0 ? 0 : m.mk_quant_intro(q, q0, new_body_pr); @@ -817,13 +817,13 @@ void simplifier::reduce1_quantifier(quantifier * q) { get_cached(q->get_pattern(i), new_pattern, new_pattern_pr); if (m.is_pattern(new_pattern)) { new_patterns.push_back(new_pattern); - } + } } num = q->get_num_no_patterns(); for (unsigned i = 0; i < num; i++) { get_cached(q->get_no_pattern(i), new_pattern, new_pattern_pr); new_no_patterns.push_back(new_pattern); - } + } remove_duplicates(new_patterns); remove_duplicates(new_no_patterns); @@ -833,7 +833,7 @@ void simplifier::reduce1_quantifier(quantifier * q) { q->get_decl_sorts(), q->get_decl_names(), new_body, - q->get_weight(), + q->get_weight(), q->get_qid(), q->get_skid(), new_patterns.size(), @@ -850,10 +850,10 @@ void simplifier::reduce1_quantifier(quantifier * q) { p1 = q == q1 ? 0 : m.mk_quant_intro(q, q1, new_body_pr); } } - + expr_ref r(m); - elim_unused_vars(m, q1, r); - + elim_unused_vars(m, q1, params_ref(), r); + proof * pr = 0; if (m.fine_grain_proofs()) { proof * p2 = 0; @@ -871,7 +871,7 @@ void simplifier::reduce1_quantifier(quantifier * q) { void simplifier::borrow_plugins(simplifier const & s) { ptr_vector::const_iterator it = s.begin_plugins(); ptr_vector::const_iterator end = s.end_plugins(); - for (; it != end; ++it) + for (; it != end; ++it) register_plugin(*it); } @@ -882,7 +882,7 @@ void simplifier::enable_presimp() { enable_ac_support(false); ptr_vector::const_iterator it = begin_plugins(); ptr_vector::const_iterator end = end_plugins(); - for (; it != end; ++it) + for (; it != end; ++it) (*it)->enable_presimp(true); } @@ -905,7 +905,7 @@ bool subst_simplifier::get_subst(expr * n, expr_ref & r, proof_ref & p) { m_subst_map->get(n, _r, _p); r = _r; p = _p; - if (m.coarse_grain_proofs()) + if (m.coarse_grain_proofs()) m_subst_proofs.push_back(p); return true; } @@ -917,7 +917,7 @@ static void push_core(ast_manager & m, expr * e, proof * pr, expr_ref_vector & r TRACE("preprocessor", tout << mk_pp(e, m) << "\n"; if (pr) tout << mk_ll_pp(pr, m) << "\n\n";); - if (m.is_true(e)) + if (m.is_true(e)) return; result.push_back(e); if (m.proofs_enabled()) @@ -952,9 +952,9 @@ void push_assertion(ast_manager & m, expr * e, proof * pr, expr_ref_vector & res CTRACE("push_assertion", !(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e), tout << mk_pp(e, m) << "\n" << mk_pp(m.get_fact(pr), m) << "\n";); SASSERT(pr == 0 || m.is_undef_proof(pr) || m.get_fact(pr) == e); - if (m.is_and(e)) + if (m.is_and(e)) push_and(m, to_app(e), pr, result, result_prs); - else if (m.is_not(e) && m.is_or(to_app(e)->get_arg(0))) + else if (m.is_not(e) && m.is_or(to_app(e)->get_arg(0))) push_not_or(m, to_app(to_app(e)->get_arg(0)), pr, result, result_prs); else push_core(m, e, pr, result, result_prs); diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index d951f7710..f09d35158 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -100,13 +100,34 @@ public: ATOMIC_CMD(exit_cmd, "exit", "exit.", ctx.print_success(); throw stop_parser_exception();); -ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat command", { - if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) - throw cmd_exception("model is not available"); - model_ref m; - ctx.get_check_sat_result()->get_model(m); - ctx.display_model(m); -}); +class get_model_cmd : public cmd { + unsigned m_index; +public: + get_model_cmd(): cmd("get-model"), m_index(0) {} + virtual char const * get_usage() const { return "[]"; } + virtual char const * get_descr(cmd_context & ctx) const { + return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; + } + virtual unsigned get_arity() const { return VAR_ARITY; } + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; } + virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } + virtual void execute(cmd_context & ctx) { + if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) + throw cmd_exception("model is not available"); + model_ref m; + if (m_index > 0 && ctx.get_opt()) { + ctx.get_opt()->get_box_model(m, m_index); + } + else { + ctx.get_check_sat_result()->get_model(m); + } + ctx.display_model(m); + } + virtual void reset(cmd_context& ctx) { + m_index = 0; + } +}; + ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 8eee632dc..92943c71c 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -124,6 +124,7 @@ public: virtual bool is_pareto() = 0; virtual void set_logic(symbol const& s) = 0; virtual bool print_model() const = 0; + virtual void get_box_model(model_ref& mdl, unsigned index) = 0; virtual void updt_params(params_ref const& p) = 0; }; diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp index 94583001b..86078a13c 100644 --- a/src/cmd_context/eval_cmd.cpp +++ b/src/cmd_context/eval_cmd.cpp @@ -38,6 +38,7 @@ public: virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { model_evaluator::get_param_descrs(p); insert_timeout(p); + p.insert("model_index", CPK_UINT, "(default: 0) index of model from box optimization objective"); } virtual void prepare(cmd_context & ctx) { @@ -58,9 +59,15 @@ public: if (!ctx.is_model_available()) throw cmd_exception("model is not available"); model_ref md; + unsigned index = m_params.get_uint("model_index", 0); check_sat_result * last_result = ctx.get_check_sat_result(); SASSERT(last_result); - last_result->get_model(md); + if (index == 0 || !ctx.get_opt()) { + last_result->get_model(md); + } + else { + ctx.get_opt()->get_box_model(md, index); + } expr_ref r(ctx.m()); unsigned timeout = m_params.get_uint("timeout", UINT_MAX); unsigned rlimit = m_params.get_uint("rlimit", 0); diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 509b5ff2e..7ee1c0aeb 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -29,11 +29,12 @@ Notes: #include"bound_manager.h" #include"used_vars.h" #include"var_subst.h" +#include"gparams.h" #ifndef _EXTERNAL_RELEASE -BINARY_SYM_CMD(get_quantifier_body_cmd, - "dbg-get-qbody", +BINARY_SYM_CMD(get_quantifier_body_cmd, + "dbg-get-qbody", " ", "store the body of the quantifier in the global variable ", CPK_EXPR, @@ -43,8 +44,8 @@ BINARY_SYM_CMD(get_quantifier_body_cmd, store_expr_ref(ctx, m_sym, to_quantifier(arg)->get_expr()); }); -BINARY_SYM_CMD(set_cmd, - "dbg-set", +BINARY_SYM_CMD(set_cmd, + "dbg-set", " ", "store in the global variable ", CPK_EXPR, @@ -57,7 +58,7 @@ UNARY_CMD(pp_var_cmd, "dbg-pp-var", "", "pretty print a global variable expr * t = get_expr_ref(ctx, arg); SASSERT(t != 0); ctx.display(ctx.regular_stream(), t); - ctx.regular_stream() << std::endl; + ctx.regular_stream() << std::endl; }); BINARY_SYM_CMD(shift_vars_cmd, @@ -71,7 +72,7 @@ BINARY_SYM_CMD(shift_vars_cmd, var_shifter s(ctx.m()); s(t, arg, r); store_expr_ref(ctx, m_sym, r.get()); -}); +}); UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "", "display shared subterms of the given term", CPK_EXPR, expr *, { shared_occs s(ctx.m()); @@ -81,7 +82,7 @@ UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "", "display shared subterms of shared_occs::iterator end = s.end_shared(); for (; it != end; ++it) { expr * curr = *it; - ctx.regular_stream() << std::endl << " "; + ctx.regular_stream() << std::endl << " "; ctx.display(ctx.regular_stream(), curr, 2); } ctx.regular_stream() << ")" << std::endl; @@ -112,7 +113,7 @@ public: if (m_idx == 1) return CPK_SYMBOL_LIST; return CPK_SYMBOL; } - virtual void set_next_arg(cmd_context & ctx, symbol const & s) { + virtual void set_next_arg(cmd_context & ctx, symbol const & s) { if (m_idx == 0) { m_source = get_expr_ref(ctx, s); } @@ -146,24 +147,24 @@ UNARY_CMD(bool_rewriter_cmd, "dbg-bool-rewriter", "", "apply the Boolean r bool_rewriter_star r(ctx.m(), p); r(arg, t); ctx.display(ctx.regular_stream(), t); - ctx.regular_stream() << std::endl; + ctx.regular_stream() << std::endl; }); UNARY_CMD(bool_frewriter_cmd, "dbg-bool-flat-rewriter", "", "apply the Boolean (flattening) rewriter to the given term", CPK_EXPR, expr *, { expr_ref t(ctx.m()); - { + { params_ref p; p.set_bool("flat", true); bool_rewriter_star r(ctx.m(), p); r(arg, t); } ctx.display(ctx.regular_stream(), t); - ctx.regular_stream() << std::endl; + ctx.regular_stream() << std::endl; }); UNARY_CMD(elim_and_cmd, "dbg-elim-and", "", "apply the Boolean rewriter (eliminating AND operator and flattening) to the given term", CPK_EXPR, expr *, { expr_ref t(ctx.m()); - { + { params_ref p; p.set_bool("flat", true); p.set_bool("elim_and", true); @@ -171,7 +172,7 @@ UNARY_CMD(elim_and_cmd, "dbg-elim-and", "", "apply the Boolean rewriter (e r(arg, t); } ctx.display(ctx.regular_stream(), t); - ctx.regular_stream() << std::endl; + ctx.regular_stream() << std::endl; }); class lt_cmd : public cmd { @@ -192,7 +193,7 @@ public: } virtual void execute(cmd_context & ctx) { bool r = lt(m_t1, m_t2); - ctx.regular_stream() << (r ? "true" : "false") << std::endl; + ctx.regular_stream() << (r ? "true" : "false") << std::endl; } }; @@ -249,7 +250,7 @@ UNARY_CMD(set_next_id, "dbg-set-next-id", "", "set the next expression UNARY_CMD(used_vars_cmd, "dbg-used-vars", "", "test used_vars functor", CPK_EXPR, expr *, { used_vars proc; - if (is_quantifier(arg)) + if (is_quantifier(arg)) arg = to_quantifier(arg)->get_expr(); proc(arg); ctx.regular_stream() << "(vars"; @@ -258,7 +259,7 @@ UNARY_CMD(used_vars_cmd, "dbg-used-vars", "", "test used_vars functor", CP ctx.regular_stream() << "\n (" << std::left << std::setw(6) << i << " "; if (s != 0) ctx.display(ctx.regular_stream(), s, 10); - else + else ctx.regular_stream() << ""; ctx.regular_stream() << ")"; } @@ -271,7 +272,7 @@ UNARY_CMD(elim_unused_vars_cmd, "dbg-elim-unused-vars", "", "eliminate unu return; } expr_ref r(ctx.m()); - elim_unused_vars(ctx.m(), to_quantifier(arg), r); + elim_unused_vars(ctx.m(), to_quantifier(arg), gparams::get(), r); SASSERT(!is_quantifier(r) || !to_quantifier(r)->may_have_unused_vars()); ctx.display(ctx.regular_stream(), r); ctx.regular_stream() << std::endl; @@ -287,18 +288,18 @@ public: virtual char const * get_descr() const { return "instantiate the quantifier using the given expressions."; } virtual unsigned get_arity() const { return 2; } virtual void prepare(cmd_context & ctx) { m_q = 0; m_args.reset(); } - + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { if (m_q == 0) return CPK_EXPR; else return CPK_EXPR_LIST; } - + virtual void set_next_arg(cmd_context & ctx, expr * s) { if (!is_quantifier(s)) throw cmd_exception("invalid command, quantifier expected."); m_q = to_quantifier(s); } - + virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * ts) { if (num != m_q->get_num_decls()) throw cmd_exception("invalid command, mismatch between the number of quantified variables and the number of arguments."); @@ -331,7 +332,7 @@ public: class instantiate_nested_cmd : public instantiate_cmd_core { public: instantiate_nested_cmd():instantiate_cmd_core("dbg-instantiate-nested") {} - + virtual char const * get_descr() const { return "instantiate the quantifier nested in the outermost quantifier, this command is used to test the instantiation procedure with quantifiers that contain free variables."; } virtual void set_next_arg(cmd_context & ctx, expr * s) { diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 7ee76d4d6..35033f739 100755 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -41,8 +41,8 @@ namespace Duality { params_ref p; p.set_bool("proof", true); // this is currently useless if(models) - p.set_bool("model", true); - p.set_bool("unsat_core", true); + p.set_bool("model", true); + p.set_bool("unsat_core", true); bool mbqi = c.get_config().get().get_bool("mbqi",true); p.set_bool("mbqi",mbqi); // just to test p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants @@ -57,7 +57,7 @@ namespace Duality { m_mode = m().proof_mode(); } - expr context::constant(const std::string &name, const sort &ty){ + expr context::constant(const std::string &name, const sort &ty){ symbol s = str_symbol(name.c_str()); return cook(m().mk_const(m().mk_const_decl(s, ty))); } @@ -111,7 +111,7 @@ namespace Duality { } expr context::mki(family_id fid, ::decl_kind dk, int n, ::expr **args){ - return cook(m().mk_app(fid, dk, 0, 0, n, (::expr **)args)); + return cook(m().mk_app(fid, dk, 0, 0, n, (::expr **)args)); } expr context::make(decl_kind op, const std::vector &args){ @@ -168,9 +168,9 @@ namespace Duality { expr_abstract(m(), 0, num_bound, VEC2PTR(bound_asts), to_expr(body.raw()), abs_body); expr_ref result(m()); result = m().mk_quantifier( - op == Forall, - names.size(), VEC2PTR(types), VEC2PTR(names), abs_body.get(), - 0, + op == Forall, + names.size(), VEC2PTR(types), VEC2PTR(names), abs_body.get(), + 0, ::symbol(), ::symbol(), 0, 0, @@ -194,9 +194,9 @@ namespace Duality { } expr_ref result(m()); result = m().mk_quantifier( - op == Forall, - names.size(), VEC2PTR(types), VEC2PTR(names), to_expr(body.raw()), - 0, + op == Forall, + names.size(), VEC2PTR(types), VEC2PTR(names), to_expr(body.raw()), + 0, ::symbol(), ::symbol(), 0, 0, @@ -273,7 +273,7 @@ namespace Duality { return OtherArray; } } - + return Other; } @@ -340,7 +340,7 @@ namespace Duality { params p; return simplify(p); } - + expr context::make_var(int idx, const sort &s){ ::sort * a = to_sort(s.raw()); return cook(m().mk_var(idx,a)); @@ -348,7 +348,7 @@ namespace Duality { expr expr::qe_lite() const { - ::qe_lite qe(m()); + ::qe_lite qe(m(), params_ref()); expr_ref result(to_expr(raw()),m()); proof_ref pf(m()); qe(result,pf); @@ -356,7 +356,7 @@ namespace Duality { } expr expr::qe_lite(const std::set &idxs, bool index_of_bound) const { - ::qe_lite qe(m()); + ::qe_lite qe(m(), params_ref()); expr_ref result(to_expr(raw()),m()); proof_ref pf(m()); uint_set uis; @@ -412,16 +412,16 @@ namespace Duality { std::vector < ::sort * > _domain(domain.size()); for(unsigned i = 0; i < domain.size(); i++) _domain[i] = to_sort(domain[i].raw()); - ::func_decl* d = m().mk_fresh_func_decl(prefix, - _domain.size(), + ::func_decl* d = m().mk_fresh_func_decl(prefix, + _domain.size(), VEC2PTR(_domain), to_sort(range.raw())); return func_decl(*this,d); } func_decl context::fresh_func_decl(char const * prefix, sort const & range){ - ::func_decl* d = m().mk_fresh_func_decl(prefix, - 0, + ::func_decl* d = m().mk_fresh_func_decl(prefix, + 0, 0, to_sort(range.raw())); return func_decl(*this,d); @@ -462,30 +462,30 @@ namespace Duality { incremental, _theory.size(), VEC2PTR(_theory)); - + if(lb == Z3_L_FALSE){ interpolants.resize(_interpolants.size()); for (unsigned i = 0; i < _interpolants.size(); ++i) { interpolants[i] = expr(ctx(),_interpolants[i]); } - } - + } + if (_model) { model = iz3wrapper::model(ctx(), _model); } - + if(_labels){ labels = _labels; } - + return lb; } #endif - + static int linearize_assumptions(int num, TermTree *assumptions, - std::vector > &linear_assumptions, + std::vector > &linear_assumptions, std::vector &parents){ for(unsigned i = 0; i < assumptions->getChildren().size(); i++) num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents); @@ -501,7 +501,7 @@ namespace Duality { } static int unlinearize_interpolants(int num, - TermTree* assumptions, + TermTree* assumptions, const std::vector &interpolant, TermTree * &tree_interpolant) { @@ -522,7 +522,7 @@ namespace Duality { literals &labels, bool incremental ) - + { int size = assumptions->number(0); std::vector > linear_assumptions(size); @@ -540,36 +540,36 @@ namespace Duality { ptr_vector< ::ast> _theory(theory.size()); for(unsigned i = 0; i < theory.size(); i++) _theory[i] = theory[i]; - - + + if(!incremental){ push(); for(unsigned i = 0; i < linear_assumptions.size(); i++) for(unsigned j = 0; j < linear_assumptions[i].size(); j++) add(linear_assumptions[i][j]); } - + check_result res = unsat; if(!m_solver->get_proof()) res = check(); - + if(res == unsat){ interpolation_options_struct opts; if(weak_mode) - opts.set("weak","1"); - + opts.set("weak","1"); + ::ast *proof = m_solver->get_proof(); try { iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts); } // If there's an interpolation bug, throw a char * - // exception so duality can catch it and restart. + // exception so duality can catch it and restart. catch (const interpolation_failure &f) { throw f.msg(); } - + std::vector linearized_interpolants(_interpolants.size()); for(unsigned i = 0; i < _interpolants.size(); i++) linearized_interpolants[i] = expr(ctx(),_interpolants[i]); @@ -585,13 +585,13 @@ namespace Duality { model_ref _m; m_solver->get_model(_m); model = Duality::model(ctx(),_m.get()); - + #if 0 if(_labels){ labels = _labels; } #endif - + if(!incremental) pop(); @@ -603,7 +603,7 @@ namespace Duality { void interpolating_solver::SetWeakInterpolants(bool weak){ weak_mode = weak; } - + void interpolating_solver::SetPrintToFile(const std::string &filename){ print_filename = filename; @@ -618,14 +618,14 @@ namespace Duality { void interpolating_solver::RemoveInterpolationAxiom(const expr & t){ // theory.remove(t); } - + const char *interpolating_solver::profile(){ // return Z3_interpolation_profile(ctx()); return ""; } - + static void get_assumptions_rec(stl_ext::hash_set &memo, const proof &pf, std::vector &assumps){ if(memo.find(pf) != memo.end())return; memo.insert(pf); @@ -657,7 +657,7 @@ namespace Duality { model_smt2_pp(std::cout, m(), *m_model, 0); std::cout << std::endl; } - + void model::show_hash() const { std::ostringstream ss; model_smt2_pp(ss, m(), *m_model, 0); diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 56cc6e154..ffb964f47 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -47,14 +47,14 @@ Revision History: namespace datalog { - rule_manager::rule_manager(context& ctx) + rule_manager::rule_manager(context& ctx) : m(ctx.get_manager()), m_ctx(ctx), m_body(m), m_head(m), m_args(m), m_hnf(m), - m_qe(m), + m_qe(m, params_ref()), m_rwr(m), m_ufproc(m) {} @@ -98,7 +98,7 @@ namespace datalog { var_idx_set& rule_manager::finalize_collect_vars() { unsigned sz = m_free_vars.size(); for (unsigned i = 0; i < sz; ++i) { - if (m_free_vars[i]) m_var_idx.insert(i); + if (m_free_vars[i]) m_var_idx.insert(i); } return m_var_idx; } @@ -139,7 +139,7 @@ namespace datalog { } - void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) { + void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) { scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED); proof_ref pr(p, m); expr_ref fml1(m); @@ -147,7 +147,7 @@ namespace datalog { if (fml1 != fml && pr) { pr = m.mk_asserted(fml1); } - remove_labels(fml1, pr); + remove_labels(fml1, pr); mk_rule_core(fml1, pr, rules, name); } @@ -162,7 +162,7 @@ namespace datalog { else { is_negated.push_back(false); } - } + } } void rule_manager::mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name) { @@ -170,7 +170,7 @@ namespace datalog { proof_ref_vector prs(m); m_hnf.reset(); m_hnf.set_name(name); - + m_hnf(fml, p, fmls, prs); for (unsigned i = 0; i < m_hnf.get_fresh_predicates().size(); ++i) { m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false); @@ -181,7 +181,7 @@ namespace datalog { } void rule_manager::mk_horn_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) { - + m_body.reset(); m_neg.reset(); unsigned index = extract_horn(fml, m_body, m_head); @@ -208,13 +208,13 @@ namespace datalog { } else if (is_quantifier(fml1)) { p = m.mk_modus_ponens(p, m.mk_symmetry(m.mk_der(to_quantifier(fml1), fml))); - } + } else { p = m.mk_modus_ponens(p, m.mk_rewrite(fml, fml1)); } } - if (m_ctx.fix_unbound_vars()) { + if (m_ctx.fix_unbound_vars()) { fix_unbound_vars(r, true); } @@ -242,10 +242,10 @@ namespace datalog { for (unsigned i = 0; i < m_args.size(); ++i) { body.push_back(ensure_app(m_args[i].get())); } - } + } else { head = ensure_app(fml); - } + } return index; } @@ -262,12 +262,12 @@ namespace datalog { func_decl* rule_manager::mk_query(expr* query, rule_set& rules) { TRACE("dl", tout << mk_pp(query, m) << "\n";); - + ptr_vector vars; svector names; app_ref_vector body(m); expr_ref q(m); - + // Add implicit variables. // Remove existential prefix. bind_variables(query, false, q); @@ -278,7 +278,7 @@ namespace datalog { m_free_vars(q); vars.append(m_free_vars.size(), m_free_vars.c_ptr()); if (vars.contains(static_cast(0))) { - var_subst sub(m, false); + var_subst sub(m, false); expr_ref_vector args(m); // [s0, 0, s2, ..] // [0 -> 0, 1 -> x, 2 -> 1, ..] @@ -313,7 +313,7 @@ namespace datalog { } } - // we want outermost declared variable first to + // we want outermost declared variable first to // follow order of quantified variables so we reverse vars. while (vars.size() > names.size()) { names.push_back(symbol(names.size())); @@ -321,9 +321,9 @@ namespace datalog { vars.reverse(); names.reverse(); func_decl* qpred = m_ctx.mk_fresh_head_predicate(symbol("query"), symbol(), vars.size(), vars.c_ptr(), body_pred); - m_ctx.register_predicate(qpred, false); + m_ctx.register_predicate(qpred, false); rules.set_output_predicate(qpred); - + if (m_ctx.get_model_converter()) { filter_model_converter* mc = alloc(filter_model_converter, m); mc->insert(qpred); @@ -366,7 +366,7 @@ namespace datalog { for (unsigned i = 0; i < r.size(); ++i) { body.push_back(ensure_app(r[i].get())); } - } + } void rule_manager::hoist_compound(unsigned& num_bound, app_ref& fml, app_ref_vector& body) { @@ -440,7 +440,7 @@ namespace datalog { if (is_quantifier(e)) { q = to_quantifier(e); return q->is_forall(); - } + } return false; } @@ -454,7 +454,7 @@ namespace datalog { return app_ref(m.mk_eq(e, m.mk_true()), m); } } - + void rule_manager::check_app(expr* e) { if (!is_app(e)) { std::ostringstream out; @@ -481,7 +481,7 @@ namespace datalog { bool has_neg = false; for (unsigned i = 0; i < n; i++) { - bool is_neg = (is_negated != 0 && is_negated[i]); + bool is_neg = (is_negated != 0 && is_negated[i]); app * curr = tail[i]; if (is_neg && !m_ctx.is_predicate(curr)) { @@ -571,7 +571,7 @@ namespace datalog { case 1: fml = m.mk_implies(body[0].get(), fml); break; default: fml = m.mk_implies(m.mk_and(body.size(), body.c_ptr()), fml); break; } - + m_free_vars(fml); if (m_free_vars.empty()) { return; @@ -579,7 +579,7 @@ namespace datalog { svector names; used_symbols<> us; m_free_vars.set_default_sort(m.mk_bool_sort()); - + us(fml); m_free_vars.reverse(); for (unsigned j = 0, i = 0; i < m_free_vars.size(); ++j) { @@ -594,8 +594,8 @@ namespace datalog { ++i; } } - } - fml = m.mk_forall(m_free_vars.size(), m_free_vars.c_ptr(), names.c_ptr(), fml); + } + fml = m.mk_forall(m_free_vars.size(), m_free_vars.c_ptr(), names.c_ptr(), fml); } std::ostream& rule_manager::display_smt2(rule const& r, std::ostream & out) { @@ -749,7 +749,7 @@ namespace datalog { quant_tail = m.mk_exists(q_var_cnt, qsorts.c_ptr(), qnames.c_ptr(), unbound_tail_pre_quant); if (try_quantifier_elimination) { - TRACE("dl_rule_unbound_fix_pre_qe", + TRACE("dl_rule_unbound_fix_pre_qe", tout<<"rule: "; r->display(m_ctx, tout); tout<<"tail with unbound vars: "<display(m_ctx, tout); tout<<"tail with unbound vars: "<name(), false); - // keep old variable indices around so we can compose with substitutions. + // keep old variable indices around so we can compose with substitutions. // r->norm_vars(*this); } @@ -835,7 +835,7 @@ namespace datalog { void rule_manager::check_valid_head(expr * head) const { SASSERT(head); - + if (!m_ctx.is_predicate(head)) { std::ostringstream out; out << "Illegal head. The head predicate needs to be uninterpreted and registered (as recursive) " << mk_pp(head, m); @@ -874,14 +874,14 @@ namespace datalog { m.get_allocator().deallocate(get_obj_size(n), this); } - void rule::set_proof(ast_manager& m, proof* p) { + void rule::set_proof(ast_manager& m, proof* p) { if (p) { - m.inc_ref(p); + m.inc_ref(p); } if (m_proof) { - m.dec_ref(m_proof); + m.dec_ref(m_proof); } - m_proof = p; + m_proof = p; } bool rule::is_in_tail(const func_decl * p, bool only_positive) const { @@ -896,7 +896,7 @@ namespace datalog { // - // non-predicates may appear only in the interpreted tail, it is therefore + // non-predicates may appear only in the interpreted tail, it is therefore // sufficient only to check the tail. // bool rule_manager::has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const { @@ -911,7 +911,7 @@ namespace datalog { // - // Quantifiers may appear only in the interpreted tail, it is therefore + // Quantifiers may appear only in the interpreted tail, it is therefore // sufficient only to check the interpreted tail. // void rule_manager::has_quantifiers(rule const& r, bool& existential, bool& universal) const { @@ -945,7 +945,7 @@ namespace datalog { unsigned sz = get_tail_size(); for (unsigned i = 0; i < sz; ++i) { used.process(get_tail(i)); - } + } } void rule::get_vars(ast_manager& m, ptr_vector& sorts) const { @@ -994,13 +994,13 @@ namespace datalog { app * old_tail = get_tail(i); expr_ref new_tail_e(m); vs(old_tail, subst_vals.size(), subst_vals.c_ptr(), new_tail_e); - bool sign = is_neg_tail(i); + bool sign = is_neg_tail(i); m.inc_ref(new_tail_e); m.dec_ref(old_tail); m_tail[i] = TAG(app *, to_app(new_tail_e), sign); } } - + void rule::display(context & ctx, std::ostream & out) const { ast_manager & m = ctx.get_manager(); //out << mk_pp(m_head, m); @@ -1068,7 +1068,7 @@ namespace datalog { } - + }; diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 587488fc9..7484a77fa 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1007,7 +1007,7 @@ namespace pdr { return m_cache[l]; } - void model_search::erase_children(model_node& n, bool backtrack) { + void model_search::erase_children(model_node& n, bool backtrack) { ptr_vector todo, nodes; todo.append(n.children()); remove_goal(n); @@ -2241,7 +2241,7 @@ namespace pdr { vars.append(aux_vars.size(), aux_vars.c_ptr()); scoped_ptr rep; - qe_lite qe(m); + qe_lite qe(m, m_params.p); expr_ref phi1 = m_pm.mk_and(Phi); qe(vars, phi1); TRACE("pdr", tout << "Eliminated\n" << mk_pp(phi1, m) << "\n";); diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 0a6c4c294..35eb5d936 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -53,10 +53,10 @@ namespace tb { app* t = to_app(_t); if (m.is_value(s) && m.is_value(t)) { - IF_VERBOSE(2, verbose_stream() << "different:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << "different:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";); return l_false; } - + if (m_dt.is_constructor(s) && m_dt.is_constructor(t)) { if (s->get_decl() == t->get_decl()) { lbool state = l_true; @@ -75,7 +75,7 @@ namespace tb { return state; } else { - IF_VERBOSE(2, verbose_stream() << "different constructors:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << "different constructors:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";); return l_false; } } @@ -109,7 +109,7 @@ namespace tb { case l_false: return false; default: - conds.push_back(m.mk_eq(p, t)); + conds.push_back(m.mk_eq(p, t)); return true; } } @@ -117,7 +117,7 @@ namespace tb { public: matcher(ast_manager& m): m(m), m_dt(m) {} - + bool operator()(app* pat, app* term, substitution& s, expr_ref_vector& conds) { // top-most term to match is a predicate. The predicates should be the same. if (pat->get_decl() != term->get_decl() || @@ -149,7 +149,7 @@ namespace tb { } } return true; - } + } }; class clause { @@ -165,22 +165,22 @@ namespace tb { unsigned m_next_rule; // next rule to expand goal on unsigned m_ref; // reference count - public: - + public: + clause(ast_manager& m): m_head(m), m_predicates(m), m_constraint(m), m_seqno(0), - m_index(0), + m_index(0), m_num_vars(0), - m_predicate_index(0), + m_predicate_index(0), m_parent_rule(0), m_parent_index(0), m_next_rule(static_cast(-1)), m_ref(0) { } - + void set_seqno(unsigned seqno) { m_seqno = seqno; } unsigned get_seqno() const { return m_seqno; } unsigned get_next_rule() const { return m_next_rule; } @@ -198,10 +198,10 @@ namespace tb { void set_head(app* h) { m_head = h; } unsigned get_parent_index() const { return m_parent_index; } unsigned get_parent_rule() const { return m_parent_rule; } - void set_parent(ref& parent) { + void set_parent(ref& parent) { m_parent_index = parent->get_index(); m_parent_rule = parent->get_next_rule(); - } + } expr_ref get_body() const { ast_manager& m = get_manager(); @@ -247,7 +247,7 @@ namespace tb { } if (!vars.empty()) { body = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), body); - } + } return body; } @@ -273,18 +273,18 @@ namespace tb { reduce_equalities(); // IF_VERBOSE(1, display(verbose_stream());); } - + void inc_ref() { m_ref++; } - + void dec_ref() { --m_ref; if (m_ref == 0) { dealloc(this); } } - + void display(std::ostream& out) const { ast_manager& m = m_head.get_manager(); expr_ref_vector fmls(m); @@ -304,7 +304,7 @@ namespace tb { } out << mk_pp(fml, m) << "\n"; } - + private: ast_manager& get_manager() const { return m_head.get_manager(); } @@ -314,7 +314,7 @@ namespace tb { // - m_head - head predicate // - m_predicates - auxiliary predicates in body. // - m_constraint - side constraint - // + // void init_from_rule(datalog::rule_ref const& r) { ast_manager& m = get_manager(); expr_ref_vector fmls(m); @@ -328,7 +328,7 @@ namespace tb { m_predicates.reset(); for (unsigned i = 0; i < utsz; ++i) { m_predicates.push_back(r->get_tail(i)); - } + } bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint); } @@ -348,13 +348,13 @@ namespace tb { if (get_subst(rw, subst, i, fmls)) { fmls[i] = m.mk_true(); } - } + } subst.apply(1, delta, expr_offset(m_head, 0), tmp); m_head = to_app(tmp); for (unsigned i = 0; i < m_predicates.size(); ++i) { subst.apply(1, delta, expr_offset(m_predicates[i].get(), 0), tmp); m_predicates[i] = to_app(tmp); - } + } bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint); subst.apply(1, delta, expr_offset(m_constraint, 0), m_constraint); rw(m_constraint); @@ -404,7 +404,7 @@ namespace tb { throw non_constructor(); } } - void operator()(var* v) { } + void operator()(var* v) { } void operator()(quantifier* ) { throw non_constructor(); } @@ -421,7 +421,7 @@ namespace tb { return true; } - }; + }; // rules class rules { @@ -456,7 +456,7 @@ namespace tb { func_decl* f = g->get_decl(); map::obj_map_entry* e = m_index.insert_if_not_there2(f, unsigned_vector()); SASSERT(e); - e->get_data().m_value.push_back(idx); + e->get_data().m_value.push_back(idx); } unsigned get_num_rules(func_decl* p) const { @@ -475,14 +475,14 @@ namespace tb { for (; it != end; ++it) { decls.push_back(it->m_key); } - } + } ref get_rule(func_decl* p, unsigned idx) const { map::obj_map_entry* e = m_index.find_core(p); SASSERT(p); unsigned rule_id = e->get_data().get_value()[idx]; return m_rules[rule_id]; - } + } private: void reset() { m_rules.reset(); @@ -509,7 +509,7 @@ namespace tb { bool_rewriter m_rw; smt_params m_fparams; smt::kernel m_solver; - + public: index(ast_manager& m): m(m), @@ -520,7 +520,7 @@ namespace tb { m_matcher(m), m_refs(m), m_subst(m), - m_qe(m), + m_qe(m, params_ref()), m_rw(m), m_solver(m, m_fparams) {} @@ -544,7 +544,7 @@ namespace tb { } private: - + void setup(clause const& g) { m_preds.reset(); m_refs.reset(); @@ -569,8 +569,8 @@ namespace tb { } vs(g.get_constraint(), vars.size(), vars.c_ptr(), fml); fmls.push_back(fml); - m_precond = m.mk_and(fmls.size(), fmls.c_ptr()); - IF_VERBOSE(2, + m_precond = m.mk_and(fmls.size(), fmls.c_ptr()); + IF_VERBOSE(2, verbose_stream() << "setup-match: "; for (unsigned i = 0; i < m_preds.size(); ++i) { verbose_stream() << mk_pp(m_preds[i].get(), m) << " "; @@ -587,18 +587,18 @@ namespace tb { return true; } } - return false; + return false; } // // check that each predicate in r is matched by some predicate in premise. // for now: skip multiple matches within the same rule (incomplete). // bool match_rule(unsigned rule_index) { - clause const& g = *m_index[rule_index]; + clause const& g = *m_index[rule_index]; m_sideconds.reset(); m_subst.reset(); m_subst.reserve(2, g.get_num_vars()); - + IF_VERBOSE(2, g.display(verbose_stream() << "try-match\n");); return match_head(g); @@ -628,9 +628,9 @@ namespace tb { } verbose_stream() << mk_pp(q, m) << " = " << mk_pp(p, m) << "\n"; ); - - if (q->get_decl() == p->get_decl() && + + if (q->get_decl() == p->get_decl() && m_matcher(q, p, m_subst, m_sideconds) && match_predicates(predicate_index + 1, g)) { return true; @@ -646,7 +646,7 @@ namespace tb { expr_ref q(m), postcond(m); expr_ref_vector fmls(m_sideconds); m_subst.reset_cache(); - + for (unsigned i = 0; !m.canceled() && i < fmls.size(); ++i) { m_subst.apply(2, deltas, expr_offset(fmls[i].get(), 0), q); fmls[i] = q; @@ -680,7 +680,7 @@ namespace tb { verbose_stream() << "check: " << mk_pp(postcond, m, 7 + g.get_num_predicates()) << "\n";); if (!is_ground(postcond)) { - IF_VERBOSE(1, verbose_stream() << "TBD: non-ground\n" + IF_VERBOSE(1, verbose_stream() << "TBD: non-ground\n" << mk_pp(postcond, m) << "\n"; m_clause->display(verbose_stream()); verbose_stream() << "\n=>\n"; @@ -743,7 +743,7 @@ namespace tb { double m_weight_multiply; unsigned m_update_frequency; unsigned m_next_update; - + public: selection(datalog::context& ctx): @@ -766,7 +766,7 @@ namespace tb { scores.reset(); basic_score_predicate(p, scores); insert_score(p->get_decl(), scores); - } + } normalize_scores(rs); } @@ -783,7 +783,7 @@ namespace tb { default: return weight_select(g); - } + } } void reset() { @@ -867,8 +867,8 @@ namespace tb { } } IF_VERBOSE(1, verbose_stream() << "select:" << result << "\n";); - - return result; + + return result; } unsigned basic_weight_select(clause const& g) { @@ -957,7 +957,7 @@ namespace tb { } } - + double score_predicate(app* p) { double score = 1; if (find_score(p, score)) { @@ -1031,7 +1031,7 @@ namespace tb { } else { m_score_map.insert(f, scores); - } + } } }; @@ -1044,15 +1044,15 @@ namespace tb { expr_ref_vector m_sub1; expr_ref_vector m_sub2; public: - unifier(ast_manager& m): - m(m), + unifier(ast_manager& m): + m(m), m_unifier(m), m_S1(m), m_S2(m, false), m_rename(m), - m_sub1(m), + m_sub1(m), m_sub2(m) {} - + bool operator()(ref& tgt, unsigned idx, ref& src, bool compute_subst, ref& result) { return unify(*tgt, idx, *src, compute_subst, result); } @@ -1066,12 +1066,12 @@ namespace tb { } } - bool unify(clause const& tgt, unsigned idx, clause const& src, bool compute_subst, ref& result) { - qe_lite qe(m); + bool unify(clause const& tgt, unsigned idx, clause const& src, bool compute_subst, ref& result) { + qe_lite qe(m, params_ref()); reset(); SASSERT(tgt.get_predicate(idx)->get_decl() == src.get_decl()); unsigned var_cnt = std::max(tgt.get_num_vars(), src.get_num_vars()); - m_S1.reserve(2, var_cnt); + m_S1.reserve(2, var_cnt); if (!m_unifier(tgt.get_predicate(idx), src.get_head(), m_S1)) { return false; } @@ -1080,7 +1080,7 @@ namespace tb { app_ref head(m); result = alloc(clause, m); unsigned delta[2] = { 0, var_cnt }; - m_S1.apply(2, delta, expr_offset(tgt.get_head(), 0), tmp); + m_S1.apply(2, delta, expr_offset(tgt.get_head(), 0), tmp); head = to_app(tmp); for (unsigned i = 0; i < tgt.get_num_predicates(); ++i) { if (i != idx) { @@ -1096,7 +1096,7 @@ namespace tb { } m_S1.apply(2, delta, expr_offset(tgt.get_constraint(), 0), tmp); m_S1.apply(2, delta, expr_offset(src.get_constraint(), 1), tmp2); - constraint = m.mk_and(tmp, tmp2); + constraint = m.mk_and(tmp, tmp2); // perform trival quantifier-elimination: uint_set index_set; @@ -1114,7 +1114,7 @@ namespace tb { if (m.is_false(constraint)) { return false; } - + // initialize rule. result->init(head, predicates, constraint); ptr_vector vars; @@ -1147,10 +1147,10 @@ namespace tb { extract_subst(delta, src, 1); } // init result using head, predicates, constraint - return true; + return true; } - - + + private: void reset() { m_S1.reset(); @@ -1175,9 +1175,9 @@ namespace tb { else { insert_subst(offset, m.mk_true()); } - } + } } - + void insert_subst(unsigned offset, expr* e) { if (offset == 0) { m_sub1.push_back(e); @@ -1201,7 +1201,7 @@ namespace tb { // - // Given a clause + // Given a clause // P(s) :- P(t), Phi(x). // Compute the clauses: // acc: P(s) :- Delta(z,t), P(z), Phi(x). @@ -1237,7 +1237,7 @@ namespace tb { head = m.mk_app(delta, zszs.size(), zszs.c_ptr()); for (unsigned i = 0; i < zs.size(); ++i) { zszs[i+zs.size()] = q->get_arg(i); - } + } pred = m.mk_app(delta, zszs.size(), zszs.c_ptr()); preds.push_back(pred); for (unsigned i = 1; i < g.get_num_predicates(); ++i) { @@ -1247,28 +1247,28 @@ namespace tb { preds.push_back(m.mk_app(q->get_decl(), zs.size(), zs.c_ptr())); acc->init(p, preds, g.get_constraint()); - IF_VERBOSE(1, + IF_VERBOSE(1, delta1->display(verbose_stream() << "delta1:\n"); delta2->display(verbose_stream() << "delta2:\n"); acc->display(verbose_stream() << "acc:\n");); } - // + // // Given a sequence of clauses and inference rules // compute a super-predicate and auxiliary clauses. - // + // // P1(x) :- P2(y), R(z) // P2(y) :- P3(z), T(u) // P3(z) :- P1(x), U(v) // => // P1(x) :- P1(x), R(z), T(u), U(v) - // + // ref resolve_rules(unsigned num_clauses, clause*const* clauses, unsigned const* positions) { ref result = clauses[0]; ref tmp; unsigned offset = 0; - for (unsigned i = 0; i + 1 < num_clauses; ++i) { + for (unsigned i = 0; i + 1 < num_clauses; ++i) { clause const& cl = *clauses[i+1]; offset += positions[i]; VERIFY (m_unifier.unify(*result, offset, cl, false, tmp)); @@ -1276,7 +1276,7 @@ namespace tb { } return result; } - + private: @@ -1286,7 +1286,7 @@ namespace tb { unsigned num_vars = g.get_num_vars(); for (unsigned i = 0; i < p->get_num_args(); ++i) { result.push_back(m.mk_var(num_vars+i, m.get_sort(p->get_arg(i)))); - } + } return result; } }; @@ -1341,7 +1341,7 @@ namespace datalog { uint_set m_displayed_rules; public: imp(context& ctx): - m_ctx(ctx), + m_ctx(ctx), m(ctx.get_manager()), rm(ctx.get_rule_manager()), m_index(m), @@ -1358,7 +1358,7 @@ namespace datalog { m_fparams.m_timeout = 1000; } - ~imp() {} + ~imp() {} lbool query(expr* query) { m_ctx.ensure_opened(); @@ -1378,7 +1378,7 @@ namespace datalog { IF_VERBOSE(1, display_clause(*get_clause(), verbose_stream() << "g" << get_clause()->get_seqno() << " ");); return run(); } - + void cleanup() { m_clauses.reset(); } @@ -1400,7 +1400,7 @@ namespace datalog { expr_ref get_answer() const { switch(m_status) { - case l_undef: + case l_undef: UNREACHABLE(); return expr_ref(m.mk_false(), m); case l_true: { @@ -1415,7 +1415,7 @@ namespace datalog { return expr_ref(m.mk_true(), m); } private: - + void select_predicate() { tb::clause & g = *get_clause(); unsigned num_predicates = g.get_num_predicates(); @@ -1430,17 +1430,17 @@ namespace datalog { IF_VERBOSE(2, verbose_stream() << mk_pp(g.get_predicate(pi), m) << "\n";); } } - + void apply_rule(ref& r) { ref clause = get_clause(); - ref next_clause; + ref next_clause; if (m_unifier(clause, clause->get_predicate_index(), r, false, next_clause) && !query_is_tautology(*next_clause)) { init_clause(next_clause); unsigned subsumer = 0; - IF_VERBOSE(1, + IF_VERBOSE(1, display_rule(*clause, verbose_stream()); - display_premise(*clause, + display_premise(*clause, verbose_stream() << "g" << next_clause->get_seqno() << " "); display_clause(*next_clause, verbose_stream()); ); @@ -1462,8 +1462,8 @@ namespace datalog { m_instruction = tb::SELECT_RULE; } } - - void select_rule() { + + void select_rule() { tb::clause& g = *get_clause(); g.inc_next_rule(); unsigned pi = g.get_predicate_index(); @@ -1481,7 +1481,7 @@ namespace datalog { void backtrack() { SASSERT(!m_clauses.empty()); - m_clauses.pop_back(); + m_clauses.pop_back(); if (m_clauses.empty()) { m_instruction = tb::SATISFIABLE; } @@ -1500,16 +1500,16 @@ namespace datalog { return l_undef; } switch(m_instruction) { - case tb::SELECT_PREDICATE: - select_predicate(); + case tb::SELECT_PREDICATE: + select_predicate(); break; - case tb::SELECT_RULE: - select_rule(); + case tb::SELECT_RULE: + select_rule(); break; case tb::BACKTRACK: backtrack(); break; - case tb::SATISFIABLE: + case tb::SATISFIABLE: m_status = l_false; return l_false; case tb::UNSATISFIABLE: @@ -1522,18 +1522,18 @@ namespace datalog { return l_undef; } } - } + } bool query_is_tautology(tb::clause const& g) { expr_ref fml = g.to_formula(); fml = m.mk_not(fml); m_solver.push(); m_solver.assert_expr(fml); - lbool is_sat = m_solver.check(); + lbool is_sat = m_solver.check(); m_solver.pop(1); TRACE("dl", tout << is_sat << ":\n" << mk_pp(fml, m) << "\n";); - + return l_false == is_sat; } @@ -1560,7 +1560,7 @@ namespace datalog { void display_premise(tb::clause& p, std::ostream& out) { func_decl* f = p.get_predicate(p.get_predicate_index())->get_decl(); - out << "{g" << p.get_seqno() << " " << f->get_name() << " pos: " + out << "{g" << p.get_seqno() << " " << f->get_name() << " pos: " << p.get_predicate_index() << " rule: " << p.get_next_rule() << "}\n"; } @@ -1576,21 +1576,21 @@ namespace datalog { ref replayed_clause; replace_proof_converter pc(m); - // clause is a empty clause. + // clause is a empty clause. // Pretend it is asserted. // It gets replaced by premises. - SASSERT(clause->get_num_predicates() == 0); + SASSERT(clause->get_num_predicates() == 0); expr_ref root = clause->to_formula(); vector substs; - while (0 != clause->get_index()) { - SASSERT(clause->get_parent_index() < clause->get_index()); + while (0 != clause->get_index()) { + SASSERT(clause->get_parent_index() < clause->get_index()); unsigned p_index = clause->get_parent_index(); unsigned p_rule = clause->get_parent_rule(); ref parent = m_clauses[p_index]; unsigned pi = parent->get_predicate_index(); func_decl* pred = parent->get_predicate(pi)->get_decl(); - ref rl = m_rules.get_rule(pred, p_rule); + ref rl = m_rules.get_rule(pred, p_rule); VERIFY(m_unifier(parent, parent->get_predicate_index(), rl, true, replayed_clause)); expr_ref_vector s1(m_unifier.get_rule_subst(true)); expr_ref_vector s2(m_unifier.get_rule_subst(false)); @@ -1614,36 +1614,36 @@ namespace datalog { } expr_ref body = clause.get_body(); var_subst vs(m, false); - vs(body, subst.size(), subst.c_ptr(), body); + vs(body, subst.size(), subst.c_ptr(), body); out << mk_pp(body, m) << "\n"; } - void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2, + void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2, expr_ref_vector const& s1, expr_ref_vector const& s2, tb::clause const& res) const { unsigned idx = r1.get_predicate_index(); expr_ref fml = res.to_formula(); vector substs; svector > positions; substs.push_back(s1); - substs.push_back(s2); + substs.push_back(s2); scoped_proof _sc(m); proof_ref pr(m); proof_ref_vector premises(m); premises.push_back(m.mk_asserted(r1.to_formula())); premises.push_back(m.mk_asserted(r2.to_formula())); - positions.push_back(std::make_pair(idx+1, 0)); + positions.push_back(std::make_pair(idx+1, 0)); pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs); pc.insert(pr); - } + } }; tab::tab(context& ctx): datalog::engine_base(ctx.get_manager(),"tabulation"), - m_imp(alloc(imp, ctx)) { + m_imp(alloc(imp, ctx)) { } tab::~tab() { dealloc(m_imp); - } + } lbool tab::query(expr* query) { return m_imp->query(query); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d1b7a489e..af3c57baa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -342,6 +342,14 @@ namespace opt { fix_model(mdl); } + void context::get_box_model(model_ref& mdl, unsigned index) { + if (index >= m_box_models.size()) { + throw default_exception("index into models is out of bounds"); + } + mdl = m_box_models[index]; + fix_model(mdl); + } + lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) { if (scoped) get_solver().push(); lbool result = m_optsmt.lex(index, is_max); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index f51f75830..53bfc19c5 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -186,6 +186,7 @@ namespace opt { virtual bool print_model() const; virtual void set_model(model_ref& _m) { m_model = _m; } virtual void get_model(model_ref& _m); + virtual void get_box_model(model_ref& _m, unsigned index); virtual void fix_model(model_ref& _m); virtual void collect_statistics(statistics& stats) const; virtual proof* get_proof() { return 0; } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 2b73381a9..eccc2d0c7 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -48,8 +48,8 @@ class is_variable_test : public is_variable_proc { is_var_kind m_var_kind; public: is_variable_test(uint_set const& vars, bool index_of_bound) : - m_var_set(vars), - m_num_decls(0), + m_var_set(vars), + m_num_decls(0), m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {} is_variable_test(unsigned num_decls) : @@ -83,7 +83,7 @@ namespace eq { is_variable_proc* m_is_variable; var_subst m_subst; expr_ref_vector m_new_exprs; - + ptr_vector m_map; int_vector m_pos2var; ptr_vector m_inx2var; @@ -91,10 +91,11 @@ namespace eq { expr_ref_vector m_subst_map; expr_ref_buffer m_new_args; th_rewriter m_rewriter; - + params_ref m_params; + void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsigned_vector & order) { order.reset(); - + // eliminate self loops, and definitions containing quantifiers. bool found = false; for (unsigned i = 0; i < definitions.size(); i++) { @@ -105,18 +106,18 @@ namespace eq { else found = true; // found at least one candidate } - + if (!found) return; - + typedef std::pair frame; svector todo; - + expr_fast_mark1 visiting; expr_fast_mark2 done; - + unsigned vidx, num; - + for (unsigned i = 0; i < definitions.size(); i++) { if (definitions[i] == 0) continue; @@ -193,11 +194,11 @@ namespace eq { } } } - + bool is_variable(expr * e) const { return (*m_is_variable)(e); } - + bool is_neg_var(ast_manager & m, expr * e, var*& v) { expr* e1; if (m.is_not(e, e1) && is_variable(e1)) { @@ -208,13 +209,13 @@ namespace eq { return false; } } - - + + /** - \brief Return true if e can be viewed as a variable disequality. + \brief Return true if e can be viewed as a variable disequality. Store the variable id in v and the definition in t. For example: - + if e is (not (= (VAR 1) T)), then v assigned to 1, and t to T. if e is (iff (VAR 2) T), then v is assigned to 2, and t to (not T). (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))), @@ -225,7 +226,7 @@ namespace eq { if (m.is_not(e, e1)) { return is_var_eq(e, vs, ts); } - else if (is_var_eq(e, vs, ts) && vs.size() == 1 && m.is_bool(vs[0])) { + else if (is_var_eq(e, vs, ts) && vs.size() == 1 && m.is_bool(vs[0])) { expr_ref tmp(m); bool_rewriter(m).mk_not(ts[0].get(), tmp); ts[0] = tmp; @@ -305,7 +306,7 @@ namespace eq { todo.pop_back(); if (a.is_add(e)) { for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { - todo.push_back(std::make_pair(sign, to_app(e)->get_arg(i))); + todo.push_back(std::make_pair(sign, to_app(e)->get_arg(i))); } } else if (is_invertible_mul(is_int, e, a_val)) { @@ -322,7 +323,7 @@ namespace eq { } return false; } - + bool arith_solve(expr * lhs, expr * rhs, expr * eq, ptr_vector& vs, expr_ref_vector& ts) { return solve_arith(lhs, rhs, vs, ts); } @@ -339,7 +340,7 @@ namespace eq { TRACE("qe_lite", tout << mk_pp(eq, m) << "\n";); return true; } - + bool same_vars(ptr_vector const& vs1, ptr_vector const& vs2) const { if (vs1.size() != vs2.size()) { @@ -356,12 +357,12 @@ namespace eq { /** \brief Return true if e can be viewed as a variable equality. */ - + bool is_var_eq(expr * e, ptr_vector& vs, expr_ref_vector & ts) { expr* lhs, *rhs; var* v; - - // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases + + // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) { // (iff (not VAR) t) (iff t (not VAR)) cases if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) { @@ -384,7 +385,7 @@ namespace eq { } return false; } - + // (ite cond (= VAR t) (= VAR t2)) case expr* cond, *e2, *e3; if (m.is_ite(e, cond, e2, e3)) { @@ -400,7 +401,7 @@ namespace eq { } return false; } - + // VAR = true case if (is_variable(e)) { ts.push_back(m.mk_true()); @@ -408,7 +409,7 @@ namespace eq { TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); return true; } - + // VAR = false case if (is_neg_var(m, e, v)) { ts.push_back(m.mk_false()); @@ -416,56 +417,56 @@ namespace eq { TRACE("qe_lite", tout << mk_pp(e, m) << "\n";); return true; } - + return false; } - - + + bool is_var_def(bool check_eq, expr* e, ptr_vector& vs, expr_ref_vector& ts) { if (check_eq) { return is_var_eq(e, vs, ts); } else { return is_var_diseq(e, vs, ts); - } + } } - + void get_elimination_order() { m_order.reset(); - + TRACE("top_sort", tout << "DEFINITIONS: " << std::endl; for(unsigned i = 0; i < m_map.size(); i++) if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl; ); - + der_sort_vars(m_inx2var, m_map, m_order); - - TRACE("qe_lite", + + TRACE("qe_lite", tout << "Elimination m_order:" << std::endl; for(unsigned i=0; iget_expr(); if ((q->is_forall() && m.is_or(e)) || @@ -474,15 +475,15 @@ namespace eq { args = to_app(e)->get_args(); } } - + void apply_substitution(quantifier * q, expr_ref & r) { - + expr * e = q->get_expr(); unsigned num_args = 1; expr* const* args = &e; flatten_args(q, num_args, args); bool_rewriter rw(m); - + // get a new expression m_new_args.reset(); for(unsigned i = 0; i < num_args; i++) { @@ -495,7 +496,7 @@ namespace eq { r = q; return; } - + expr_ref t(m); if (q->is_forall()) { rw.mk_or(m_new_args.size(), m_new_args.c_ptr(), t); @@ -503,9 +504,9 @@ namespace eq { else { rw.mk_and(m_new_args.size(), m_new_args.c_ptr(), t); } - expr_ref new_e(m); + expr_ref new_e(m); m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e); - + // don't forget to update the quantifier patterns expr_ref_buffer new_patterns(m); expr_ref_buffer new_no_patterns(m); @@ -514,17 +515,17 @@ namespace eq { m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_pat); new_patterns.push_back(new_pat); } - + for (unsigned j = 0; j < q->get_num_no_patterns(); j++) { expr_ref new_nopat(m); m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_nopat); new_no_patterns.push_back(new_nopat); } - - r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), + + r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), new_no_patterns.size(), new_no_patterns.c_ptr(), new_e); } - + void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) { expr * e = q->get_expr(); is_variable_test is_v(q->get_num_decls()); @@ -532,17 +533,17 @@ namespace eq { unsigned num_args = 1; expr* const* args = &e; flatten_args(q, num_args, args); - + unsigned def_count = 0; unsigned largest_vinx = 0; - + find_definitions(num_args, args, q->is_exists(), def_count, largest_vinx); - + if (def_count > 0) { get_elimination_order(); SASSERT(m_order.size() <= def_count); // some might be missing because of cycles - - if (!m_order.empty()) { + + if (!m_order.empty()) { create_substitution(largest_vinx + 1); apply_substitution(q, r); } @@ -554,31 +555,32 @@ namespace eq { TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";); r = q; } - + if (m.proofs_enabled()) { pr = r == q ? 0 : m.mk_der(q, r); - } - } - + } + } + void elim_unused_vars(expr_ref& r, proof_ref &pr) { if (is_quantifier(r)) { quantifier * q = to_quantifier(r); - ::elim_unused_vars(m, q, r); + + ::elim_unused_vars(m, q, m_params, r); if (m.proofs_enabled()) { proof * p1 = m.mk_elim_unused_vars(q, r); pr = m.mk_transitivity(pr, p1); } } } - + void find_definitions(unsigned num_args, expr* const* args, bool is_exists, unsigned& def_count, unsigned& largest_vinx) { def_count = 0; largest_vinx = 0; m_map.reset(); m_pos2var.reset(); - m_inx2var.reset(); + m_inx2var.reset(); m_pos2var.reserve(num_args, -1); - + // Find all definitions for (unsigned i = 0; i < num_args; i++) { checkpoint(); @@ -591,12 +593,12 @@ namespace eq { unsigned idx = v->get_idx(); if (m_map.get(idx, 0) == 0) { m_map.reserve(idx + 1, 0); - m_inx2var.reserve(idx + 1, 0); + m_inx2var.reserve(idx + 1, 0); m_map[idx] = t; m_inx2var[idx] = v; m_pos2var[i] = idx; def_count++; - largest_vinx = std::max(idx, largest_vinx); + largest_vinx = std::max(idx, largest_vinx); m_new_exprs.push_back(t); } } @@ -646,10 +648,10 @@ namespace eq { tmp = m.mk_and(conjs.size(), conjs.c_ptr()); tout << "after flatten\n" << mk_pp(tmp, m) << "\n";); } - + void flatten_constructor(app* c, app* r, expr_ref_vector& conjs) { SASSERT(dt.is_constructor(c)); - + func_decl* d = c->get_decl(); if (dt.is_constructor(r->get_decl())) { @@ -661,7 +663,7 @@ namespace eq { } else { conjs.push_back(m.mk_false()); - } + } } else { func_decl* rec = dt.get_constructor_recognizer(d); @@ -683,7 +685,7 @@ namespace eq { bool remove_unconstrained(expr_ref_vector& conjs) { bool reduced = false, change = true; - expr* r, *l, *ne; + expr* r, *l, *ne; while (change) { change = false; for (unsigned i = 0; i < conjs.size(); ++i) { @@ -704,21 +706,21 @@ namespace eq { } return reduced; } - + bool reduce_var_set(expr_ref_vector& conjs) { unsigned def_count = 0; unsigned largest_vinx = 0; bool reduced = false; flatten_definitions(conjs); - + find_definitions(conjs.size(), conjs.c_ptr(), true, def_count, largest_vinx); - + if (def_count > 0) { get_elimination_order(); SASSERT(m_order.size() <= def_count); // some might be missing because of cycles - - if (!m_order.empty()) { + + if (!m_order.empty()) { expr_ref r(m), new_r(m); r = m.mk_and(conjs.size(), conjs.c_ptr()); create_substitution(largest_vinx + 1); @@ -739,35 +741,36 @@ namespace eq { void checkpoint() { cooperate("der"); - if (m.canceled()) + if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); } public: - der(ast_manager & m): - m(m), + der(ast_manager & m, params_ref const & p): + m(m), a(m), dt(m), - m_is_variable(0), - m_subst(m), - m_new_exprs(m), - m_subst_map(m), - m_new_args(m), - m_rewriter(m) {} - + m_is_variable(0), + m_subst(m), + m_new_exprs(m), + m_subst_map(m), + m_new_args(m), + m_rewriter(m), + m_params(p) {} + void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} - + void operator()(quantifier * q, expr_ref & r, proof_ref & pr) { - TRACE("qe_lite", tout << mk_pp(q, m) << "\n";); + TRACE("qe_lite", tout << mk_pp(q, m) << "\n";); pr = 0; r = q; - reduce_quantifier(q, r, pr); + reduce_quantifier(q, r, pr); if (r != q) { elim_unused_vars(r, pr); } } - - void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) { + + void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) { r = q; // Keep applying reduce_quantifier1 until r doesn't change anymore do { @@ -779,15 +782,15 @@ namespace eq { pr = m.mk_transitivity(pr, curr_pr); } } while (q != r && is_quantifier(r)); - + m_new_exprs.reset(); } - + void operator()(expr_ref_vector& r) { while (reduce_var_set(r)) ; m_new_exprs.reset(); } - + ast_manager& get_manager() const { return m; } @@ -804,7 +807,7 @@ namespace ar { is_variable_proc* m_is_variable; ptr_vector m_todo; expr_mark m_visited; - + bool is_variable(expr * e) const { return (*m_is_variable)(e); } @@ -827,7 +830,7 @@ namespace ar { Ex A. Phi[store(A,x,t)] Perhaps also: - Ex A. store(A,y,z)[x] = t & Phi where x \not\in A, t, y, z, A \not\in y z, t + Ex A. store(A,y,z)[x] = t & Phi where x \not\in A, t, y, z, A \not\in y z, t => Ex A, v . (x = y => z = t) & Phi[store(store(A,x,t),y,v)] @@ -873,7 +876,7 @@ namespace ar { bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e) { expr* e1, *e2; - return + return m.is_eq(e, e1, e2) && (solve_select(conjs, i, e1, e2) || solve_select(conjs, i, e2, e1)); @@ -887,8 +890,8 @@ namespace ar { bool solve_neq_select(expr_ref_vector& conjs, unsigned i, expr* e) { expr* e1, *a1, *a2; if (m.is_not(e, e1) && m.is_eq(e1, a1, a2)) { - if (a.is_select(a1) && - a.is_select(a2) && + if (a.is_select(a1) && + a.is_select(a2) && to_app(a1)->get_num_args() == to_app(a2)->get_num_args()) { expr* e1 = to_app(a1)->get_arg(0); expr* e2 = to_app(a2)->get_arg(0); @@ -937,7 +940,7 @@ namespace ar { void operator()(expr* e) {} void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} - + }; }; // namespace ar @@ -976,27 +979,27 @@ namespace fm { for (; it != end; ++it) it->~rational(); } - + unsigned hash() const { return hash_u(m_id); } }; - + typedef ptr_vector constraints; - + class constraint_set { - unsigned_vector m_id2pos; + unsigned_vector m_id2pos; constraints m_set; public: typedef constraints::const_iterator iterator; - - bool contains(constraint const & c) const { - if (c.m_id >= m_id2pos.size()) - return false; - return m_id2pos[c.m_id] != UINT_MAX; + + bool contains(constraint const & c) const { + if (c.m_id >= m_id2pos.size()) + return false; + return m_id2pos[c.m_id] != UINT_MAX; } - + bool empty() const { return m_set.empty(); } unsigned size() const { return m_set.size(); } - + void insert(constraint & c) { unsigned id = c.m_id; m_id2pos.reserve(id+1, UINT_MAX); @@ -1006,7 +1009,7 @@ namespace fm { m_id2pos[id] = pos; m_set.push_back(&c); } - + void erase(constraint & c) { unsigned id = c.m_id; if (id >= m_id2pos.size()) @@ -1018,27 +1021,27 @@ namespace fm { unsigned last_pos = m_set.size() - 1; if (pos != last_pos) { constraint * last_c = m_set[last_pos]; - m_set[pos] = last_c; + m_set[pos] = last_c; m_id2pos[last_c->m_id] = pos; } m_set.pop_back(); } - + constraint & erase() { SASSERT(!empty()); - constraint & c = *m_set.back(); + constraint & c = *m_set.back(); m_id2pos[c.m_id] = UINT_MAX; m_set.pop_back(); return c; } - + void reset() { m_id2pos.reset(); m_set.reset(); } void finalize() { m_id2pos.finalize(); m_set.finalize(); } - + iterator begin() const { return m_set.begin(); } iterator end() const { return m_set.end(); } }; - + class fm { ast_manager & m; is_variable_proc* m_is_variable; @@ -1068,24 +1071,24 @@ namespace fm { bool m_inconsistent; expr_dependency_ref m_inconsistent_core; constraint_set m_sub_todo; - + // --------------------------- // // OCC clause recognizer // // --------------------------- - + bool is_literal(expr * t) const { expr * atom; return is_uninterp_const(t) || (m.is_not(t, atom) && is_uninterp_const(atom)); } - + bool is_constraint(expr * t) const { return !is_literal(t); } - + bool is_var(expr * t, expr * & x) const { - + if ((*m_is_variable)(t)) { x = t; return true; @@ -1096,24 +1099,24 @@ namespace fm { } return false; } - + bool is_var(expr * t) const { expr * x; return is_var(t, x); } - + bool is_linear_mon_core(expr * t, expr * & x) const { expr * c; if (m_util.is_mul(t, c, x) && m_util.is_numeral(c) && is_var(x, x)) return true; return is_var(t, x); } - + bool is_linear_mon(expr * t) const { expr * x; return is_linear_mon_core(t, x); } - + bool is_linear_pol(expr * t) const { unsigned num_mons; expr * const * mons; @@ -1125,7 +1128,7 @@ namespace fm { num_mons = 1; mons = &t; } - + expr_fast_mark2 visited; bool all_forbidden = true; for (unsigned i = 0; i < num_mons; i++) { @@ -1141,7 +1144,7 @@ namespace fm { } return !all_forbidden; } - + bool is_linear_ineq(expr * t) const { bool result = false; m.is_not(t, t); @@ -1153,7 +1156,7 @@ namespace fm { return result; } - + bool is_occ(expr * t) { if (m_fm_occ && m.is_or(t)) { unsigned num = to_app(t)->get_num_args(); @@ -1176,7 +1179,7 @@ namespace fm { } return is_linear_ineq(t); } - + // --------------------------- // // Memory mng @@ -1195,12 +1198,12 @@ namespace fm { for (unsigned i = 0; i < sz; i++) del_constraint(cs[i]); } - + void reset_constraints() { del_constraints(m_constraints.size(), m_constraints.c_ptr()); m_constraints.reset(); } - + constraint * mk_constraint(unsigned num_lits, literal * lits, unsigned num_vars, var * xs, rational * as, rational & c, bool strict, expr_dependency * dep) { unsigned sz = constraint::get_obj_size(num_lits, num_vars); @@ -1236,15 +1239,15 @@ namespace fm { m.inc_ref(dep); return cnstr; } - + // --------------------------- // // Util // // --------------------------- - + unsigned num_vars() const { return m_is_int.size(); } - + // multiply as and c, by the lcm of their denominators void mk_int(unsigned num, rational * as, rational & c) { rational l = denominator(c); @@ -1259,7 +1262,7 @@ namespace fm { SASSERT(as[i].is_int()); } } - + void normalize_coeffs(constraint & c) { if (c.m_num_vars == 0) return; @@ -1281,7 +1284,7 @@ namespace fm { for (unsigned i = 0; i < c.m_num_vars; i++) c.m_as[i] /= g; } - + void display(std::ostream & out, constraint const & c) const { for (unsigned i = 0; i < c.m_num_lits; i++) { literal l = c.m_lits[i]; @@ -1308,10 +1311,10 @@ namespace fm { out << c.m_c; out << ")"; } - + /** \brief Return true if c1 subsumes c2 - + c1 subsumes c2 If 1) All literals of c1 are literals of c2 2) polynomial of c1 == polynomial of c2 @@ -1329,13 +1332,13 @@ namespace fm { return false; if (!c1.m_strict && c2.m_strict && c1.m_c == c2.m_c) return false; - + m_counter += c1.m_num_lits + c2.m_num_lits; - + for (unsigned i = 0; i < c1.m_num_vars; i++) { m_var2pos[c1.m_xs[i]] = i; } - + bool failed = false; for (unsigned i = 0; i < c2.m_num_vars; i++) { unsigned pos1 = m_var2pos[c2.m_xs[i]]; @@ -1344,21 +1347,21 @@ namespace fm { break; } } - + for (unsigned i = 0; i < c1.m_num_vars; i++) { m_var2pos[c1.m_xs[i]] = UINT_MAX; } - + if (failed) return false; - + for (unsigned i = 0; i < c2.m_num_lits; i++) { literal l = c2.m_lits[i]; bvar b = lit2bvar(l); SASSERT(m_bvar2sign[b] == 0); m_bvar2sign[b] = sign(l) ? -1 : 1; } - + for (unsigned i = 0; i < c1.m_num_lits; i++) { literal l = c1.m_lits[i]; bvar b = lit2bvar(l); @@ -1368,19 +1371,19 @@ namespace fm { break; } } - + for (unsigned i = 0; i < c2.m_num_lits; i++) { literal l = c2.m_lits[i]; bvar b = lit2bvar(l); m_bvar2sign[b] = 0; } - + if (failed) return false; - + return true; } - + void backward_subsumption(constraint const & c) { if (c.m_num_vars == 0) return; @@ -1422,7 +1425,7 @@ namespace fm { } cs.set_end(it2); } - + void subsume() { while (!m_sub_todo.empty()) { constraint & c = m_sub_todo.erase(); @@ -1433,13 +1436,13 @@ namespace fm { } public: - + // --------------------------- // // Initialization // // --------------------------- - + fm(ast_manager & _m): m(_m), m_is_variable(0), @@ -1453,11 +1456,11 @@ namespace fm { m_counter = 0; m_inconsistent = false; } - + ~fm() { reset_constraints(); } - + void updt_params() { m_fm_real_only = false; m_fm_limit = 5000000; @@ -1466,9 +1469,9 @@ namespace fm { m_fm_extra = 0; m_fm_occ = true; } - + private: - + struct forbidden_proc { fm & m_owner; forbidden_proc(fm & o):m_owner(o) {} @@ -1480,7 +1483,7 @@ namespace fm { void operator()(app * n) { } void operator()(quantifier * n) {} }; - + void init_forbidden_set(expr_ref_vector const & g) { m_forbidden_set.reset(); expr_fast_mark1 visited; @@ -1494,7 +1497,7 @@ namespace fm { quick_for_each_expr(proc, visited, f); } } - + void init(expr_ref_vector const & g) { m_sub_todo.reset(); m_id_gen.reset(); @@ -1517,24 +1520,24 @@ namespace fm { m_inconsistent_core = 0; init_forbidden_set(g); } - + // --------------------------- // // Internal data-structures // // --------------------------- - + static bool sign(literal l) { return l < 0; } static bvar lit2bvar(literal l) { return l < 0 ? -l : l; } - - bool is_int(var x) const { + + bool is_int(var x) const { return m_is_int[x] != 0; } - + bool is_forbidden(var x) const { return m_forbidden[x] != 0; } - + bool all_int(constraint const & c) const { for (unsigned i = 0; i < c.m_num_vars; i++) { if (!is_int(c.m_xs[i])) @@ -1542,7 +1545,7 @@ namespace fm { } return true; } - + app * to_expr(constraint const & c) { expr * ineq; if (c.m_num_vars == 0) { @@ -1577,20 +1580,20 @@ namespace fm { ineq = m_util.mk_le(lhs, rhs); } } - + if (c.m_num_lits == 0) { if (ineq) return to_app(ineq); else return m.mk_false(); } - + ptr_buffer lits; for (unsigned i = 0; i < c.m_num_lits; i++) { literal l = c.m_lits[i]; if (sign(l)) lits.push_back(m.mk_not(m_bvar2expr.get(lit2bvar(l)))); - else + else lits.push_back(m_bvar2expr.get(lit2bvar(l))); } if (ineq) @@ -1600,7 +1603,7 @@ namespace fm { else return m.mk_or(lits.size(), lits.c_ptr()); } - + var mk_var(expr * t) { SASSERT(::is_var(t)); SASSERT(m_util.is_int(t) || m_util.is_real(t)); @@ -1617,12 +1620,12 @@ namespace fm { SASSERT(m_var2expr.size() == m_is_int.size()); SASSERT(m_lowers.size() == m_is_int.size()); SASSERT(m_uppers.size() == m_is_int.size()); - SASSERT(m_forbidden.size() == m_is_int.size()); + SASSERT(m_forbidden.size() == m_is_int.size()); SASSERT(m_var2pos.size() == m_is_int.size()); TRACE("qe_lite", tout << mk_pp(t,m) << " |-> " << x << " forbidden: " << forbidden << "\n";); return x; } - + bvar mk_bvar(expr * t) { SASSERT(is_uninterp_const(t)); SASSERT(m.is_bool(t)); @@ -1634,7 +1637,7 @@ namespace fm { SASSERT(p > 0); return p; } - + var to_var(expr * t) { var x; if (!m_expr2var.find(t, x)) @@ -1644,22 +1647,22 @@ namespace fm { TRACE("qe_lite", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";); return x; } - + bvar to_bvar(expr * t) { bvar p; if (m_expr2bvar.find(t, p)) return p; return mk_bvar(t); } - + literal to_literal(expr * t) { if (m.is_not(t, t)) - return -to_bvar(t); + return -to_bvar(t); else return to_bvar(t); } - - + + void add_constraint(expr * f, expr_dependency * dep) { TRACE("qe_lite", tout << mk_pp(f, m) << "\n";); SASSERT(!m.is_or(f) || m_fm_occ); @@ -1711,7 +1714,7 @@ namespace fm { num_mons = 1; mons = &lhs; } - + bool all_int = true; for (unsigned j = 0; j < num_mons; j++) { expr * monomial = mons[j]; @@ -1740,9 +1743,9 @@ namespace fm { } } } - + TRACE("qe_lite", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";); - + constraint * new_c = mk_constraint(lits.size(), lits.c_ptr(), xs.size(), @@ -1751,15 +1754,15 @@ namespace fm { c, strict, dep); - + TRACE("qe_lite", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";); VERIFY(register_constraint(new_c)); } - + bool is_false(constraint const & c) const { return c.m_num_lits == 0 && c.m_num_vars == 0 && (c.m_c.is_neg() || (c.m_strict && c.m_c.is_zero())); } - + bool register_constraint(constraint * c) { normalize_coeffs(*c); if (is_false(*c)) { @@ -1768,20 +1771,20 @@ namespace fm { TRACE("qe_lite", tout << "is false "; display(tout, *c); tout << "\n";); return false; } - + bool r = false; - + for (unsigned i = 0; i < c->m_num_vars; i++) { var x = c->m_xs[i]; if (!is_forbidden(x)) { r = true; - if (c->m_as[i].is_neg()) + if (c->m_as[i].is_neg()) m_lowers[x].push_back(c); else m_uppers[x].push_back(c); } } - + if (r) { m_sub_todo.insert(*c); m_constraints.push_back(c); @@ -1794,7 +1797,7 @@ namespace fm { return false; } } - + void init_use_list(expr_ref_vector const & g) { unsigned sz = g.size(); for (unsigned i = 0; !m_inconsistent && i < sz; i++) { @@ -1812,13 +1815,13 @@ namespace fm { return UINT_MAX; return static_cast(r); } - + typedef std::pair x_cost; - + struct x_cost_lt { char_vector const m_is_int; x_cost_lt(char_vector & is_int):m_is_int(is_int) {} - bool operator()(x_cost const & p1, x_cost const & p2) const { + bool operator()(x_cost const & p1, x_cost const & p2) const { // Integer variables with cost 0 can be eliminated even if they depend on real variables. // Cost 0 == no lower or no upper bound. if (p1.second == 0) { @@ -1828,7 +1831,7 @@ namespace fm { if (p2.second == 0) return false; bool int1 = m_is_int[p1.first] != 0; bool int2 = m_is_int[p2.first] != 0; - return (!int1 && int2) || (int1 == int2 && p1.second < p2.second); + return (!int1 && int2) || (int1 == int2 && p1.second < p2.second); } }; @@ -1842,7 +1845,7 @@ namespace fm { } // x_cost_lt is not a total order on variables std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int)); - TRACE("qe_lite", + TRACE("qe_lite", svector::iterator it2 = x_cost_vector.begin(); svector::iterator end2 = x_cost_vector.end(); for (; it2 != end2; ++it2) { @@ -1855,7 +1858,7 @@ namespace fm { xs.push_back(it2->first); } } - + void cleanup_constraints(constraints & cs) { unsigned j = 0; unsigned sz = cs.size(); @@ -1868,7 +1871,7 @@ namespace fm { } cs.shrink(j); } - + // Set all_int = true if all variables in c are int. // Set unit_coeff = true if the coefficient of x in c is 1 or -1. // If all_int = false, then unit_coeff may not be set. @@ -1900,8 +1903,8 @@ namespace fm { unit_coeff = false; } } - - // An integer variable x may be eliminated, if + + // An integer variable x may be eliminated, if // 1- All variables in the contraints it occur are integer. // 2- The coefficient of x in all lower bounds (or all upper bounds) is unit. bool can_eliminate(var x) const { @@ -1915,7 +1918,7 @@ namespace fm { analyze(m_uppers[x], x, all_int, u_unit); return all_int && (l_unit || u_unit); } - + void copy_constraints(constraints const & s, clauses & t) { constraints::const_iterator it = s.begin(); constraints::const_iterator end = s.end(); @@ -1924,23 +1927,23 @@ namespace fm { t.push_back(c); } } - + clauses tmp_clauses; void save_constraints(var x) { } - + void mark_constraints_dead(constraints const & cs) { constraints::const_iterator it = cs.begin(); constraints::const_iterator end = cs.end(); for (; it != end; ++it) (*it)->m_dead = true; } - + void mark_constraints_dead(var x) { save_constraints(x); mark_constraints_dead(m_lowers[x]); mark_constraints_dead(m_uppers[x]); } - + void get_coeff(constraint const & c, var x, rational & a) { for (unsigned i = 0; i < c.m_num_vars; i++) { if (c.m_xs[i] == x) { @@ -1950,11 +1953,11 @@ namespace fm { } UNREACHABLE(); } - + var_vector new_xs; vector new_as; svector new_lits; - + constraint * resolve(constraint const & l, constraint const & u, var x) { m_counter += l.m_num_vars + u.m_num_vars + l.m_num_lits + u.m_num_lits; rational a, b; @@ -1963,14 +1966,14 @@ namespace fm { SASSERT(a.is_neg()); SASSERT(b.is_pos()); a.neg(); - + SASSERT(!is_int(x) || a.is_one() || b.is_one()); - + new_xs.reset(); new_as.reset(); rational new_c = l.m_c*b + u.m_c*a; bool new_strict = l.m_strict || u.m_strict; - + for (unsigned i = 0; i < l.m_num_vars; i++) { var xi = l.m_xs[i]; if (xi == x) @@ -1983,7 +1986,7 @@ namespace fm { SASSERT(new_xs[m_var2pos[xi]] == xi); SASSERT(new_xs.size() == new_as.size()); } - + for (unsigned i = 0; i < u.m_num_vars; i++) { var xi = u.m_xs[i]; if (xi == x) @@ -1997,7 +2000,7 @@ namespace fm { new_as[pos] += u.m_as[i] * a; } } - + // remove zeros and check whether all variables are int bool all_int = true; unsigned sz = new_xs.size(); @@ -2015,17 +2018,17 @@ namespace fm { } new_xs.shrink(j); new_as.shrink(j); - + if (all_int && new_strict) { new_strict = false; new_c --; } - + // reset m_var2pos for (unsigned i = 0; i < l.m_num_vars; i++) { m_var2pos[l.m_xs[i]] = UINT_MAX; } - + if (new_xs.empty() && (new_c.is_pos() || (!new_strict && new_c.is_zero()))) { // literal is true TRACE("qe_lite", tout << "resolution " << x << " consequent literal is always true: \n"; @@ -2034,7 +2037,7 @@ namespace fm { display(tout, u); tout << "\n";); return 0; // no constraint needs to be created. } - + new_lits.reset(); for (unsigned i = 0; i < l.m_num_lits; i++) { literal lit = l.m_lits[i]; @@ -2042,7 +2045,7 @@ namespace fm { m_bvar2sign[p] = sign(lit) ? -1 : 1; new_lits.push_back(lit); } - + bool tautology = false; for (unsigned i = 0; i < u.m_num_lits && !tautology; i++) { literal lit = u.m_lits[i]; @@ -2063,14 +2066,14 @@ namespace fm { UNREACHABLE(); } } - + // reset m_bvar2sign for (unsigned i = 0; i < l.m_num_lits; i++) { literal lit = l.m_lits[i]; bvar p = lit2bvar(lit); m_bvar2sign[p] = 0; } - + if (tautology) { TRACE("qe_lite", tout << "resolution " << x << " tautology: \n"; display(tout, l); @@ -2080,7 +2083,7 @@ namespace fm { } expr_dependency * new_dep = m.mk_join(l.m_dep, u.m_dep); - + if (new_lits.empty() && new_xs.empty() && (new_c.is_neg() || (new_strict && new_c.is_zero()))) { TRACE("qe_lite", tout << "resolution " << x << " inconsistent: \n"; display(tout, l); @@ -2090,7 +2093,7 @@ namespace fm { m_inconsistent_core = new_dep; return 0; } - + constraint * new_cnstr = mk_constraint(new_lits.size(), new_lits.c_ptr(), new_xs.size(), @@ -2105,45 +2108,45 @@ namespace fm { tout << "\n"; display(tout, u); tout << "\n---->\n"; - display(tout, *new_cnstr); + display(tout, *new_cnstr); tout << "\n"; tout << "new_dep: " << new_dep << "\n";); - + return new_cnstr; } - + ptr_vector new_constraints; - + bool try_eliminate(var x) { constraints & l = m_lowers[x]; constraints & u = m_uppers[x]; cleanup_constraints(l); cleanup_constraints(u); - + if (l.empty() || u.empty()) { // easy case mark_constraints_dead(x); TRACE("qe_lite", tout << "variable was eliminated (trivial case)\n";); return true; } - + unsigned num_lowers = l.size(); unsigned num_uppers = u.size(); - + if (num_lowers > m_fm_cutoff1 && num_uppers > m_fm_cutoff1) return false; - + if (num_lowers * num_uppers > m_fm_cutoff2) return false; - + if (!can_eliminate(x)) return false; - + m_counter += num_lowers * num_uppers; - + TRACE("qe_lite", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n"; display_constraints(tout, l); tout << "uppers:\n"; display_constraints(tout, u);); - + unsigned num_old_cnstrs = num_uppers + num_lowers; unsigned limit = num_old_cnstrs + m_fm_extra; unsigned num_new_cnstrs = 0; @@ -2164,13 +2167,13 @@ namespace fm { } } } - + mark_constraints_dead(x); - + unsigned sz = new_constraints.size(); - + m_counter += sz; - + for (unsigned i = 0; i < sz; i++) { constraint * c = new_constraints[i]; backward_subsumption(*c); @@ -2179,7 +2182,7 @@ namespace fm { TRACE("qe_lite", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";); return true; } - + void copy_remaining(vector & v2cs) { vector::iterator it = v2cs.begin(); vector::iterator end = v2cs.end(); @@ -2199,13 +2202,13 @@ namespace fm { } v2cs.finalize(); } - + // Copy remaining clauses to m_new_fmls void copy_remaining() { copy_remaining(m_uppers); copy_remaining(m_lowers); } - + void checkpoint() { cooperate("fm"); if (m.canceled()) @@ -2224,12 +2227,12 @@ namespace fm { } else { TRACE("qe_lite", display(tout);); - + subsume(); var_vector candidates; - sort_candidates(candidates); - unsigned eliminated = 0; - + sort_candidates(candidates); + unsigned eliminated = 0; + unsigned num = candidates.size(); for (unsigned i = 0; i < num; i++) { checkpoint(); @@ -2251,8 +2254,8 @@ namespace fm { reset_constraints(); fmls.reset(); fmls.append(m_new_fmls); - } - + } + void display_constraints(std::ostream & out, constraints const & cs) const { constraints::const_iterator it = cs.begin(); constraints::const_iterator end = cs.end(); @@ -2262,7 +2265,7 @@ namespace fm { out << "\n"; } } - + void display(std::ostream & out) const { unsigned num = num_vars(); for (var x = 0; x < num; x++) { @@ -2284,10 +2287,10 @@ public: ast_manager& m; public: elim_cfg(impl& i): m_imp(i), m(i.m) {} - - bool reduce_quantifier(quantifier * q, - expr * new_body, - expr * const * new_patterns, + + bool reduce_quantifier(quantifier * q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { @@ -2299,13 +2302,13 @@ public: for (unsigned i = 0; i < q->get_num_decls(); ++i) { indices.insert(i); } - m_imp(indices, true, result); + m_imp(indices, true, result); if (is_forall(q)) { result = push_not(result); } result = m.update_quantifier( - q, - q->get_num_patterns(), new_patterns, + q, + q->get_num_patterns(), new_patterns, q->get_num_no_patterns(), new_no_patterns, result); m_imp.m_rewriter(result); return true; @@ -2315,7 +2318,7 @@ public: class elim_star : public rewriter_tpl { elim_cfg m_cfg; public: - elim_star(impl& i): + elim_star(impl& i): rewriter_tpl(i.m, false, m_cfg), m_cfg(i) {} @@ -2346,21 +2349,21 @@ private: } public: - impl(ast_manager& m): - m(m), - m_der(m), - m_fm(m), - m_array_der(m), - m_elim_star(*this), + impl(ast_manager & m, params_ref const & p): + m(m), + m_der(m, p), + m_fm(m), + m_array_der(m), + m_elim_star(*this), m_rewriter(m) {} - + void operator()(app_ref_vector& vars, expr_ref& fml) { if (vars.empty()) { return; } expr_ref tmp(fml); quantifier_ref q(m); - proof_ref pr(m); + proof_ref pr(m); symbol qe_lite("QE"); expr_abstract(m, 0, vars.size(), (expr*const*)vars.c_ptr(), fml, tmp); ptr_vector sorts; @@ -2386,12 +2389,12 @@ public: ++j; } } - vars.resize(j); - } + vars.resize(j); + } else { fml = tmp; } - } + } void operator()(expr_ref& fml, proof_ref& pr) { expr_ref tmp(m); @@ -2438,8 +2441,8 @@ public: }; -qe_lite::qe_lite(ast_manager& m) { - m_impl = alloc(impl, m); +qe_lite::qe_lite(ast_manager & m, params_ref const & p) { + m_impl = alloc(impl, m, p); } qe_lite::~qe_lite() { @@ -2464,14 +2467,14 @@ void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_re } class qe_lite_tactic : public tactic { - + struct imp { ast_manager& m; qe_lite m_qe; - imp(ast_manager& m, params_ref const& p): + imp(ast_manager& m, params_ref const & p): m(m), - m_qe(m) + m_qe(m, p) {} void checkpoint() { @@ -2479,7 +2482,7 @@ class qe_lite_tactic : public tactic { throw tactic_exception(m.limit().get_cancel_msg()); cooperate("qe-lite"); } - + void debug_diff(expr* a, expr* b) { ptr_vector as, bs; as.push_back(a); @@ -2515,9 +2518,9 @@ class qe_lite_tactic : public tactic { } } - 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()); @@ -2540,7 +2543,7 @@ class qe_lite_tactic : public tactic { if (produce_proofs) { expr* fact = m.get_fact(new_pr); if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) { - new_pr = m.mk_modus_ponens(g->pr(i), new_pr); + new_pr = m.mk_modus_ponens(g->pr(i), new_pr); } else { new_pr = g->pr(i); @@ -2548,7 +2551,7 @@ class qe_lite_tactic : public tactic { } if (f != new_f) { TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n";); - g->update(i, new_f, new_pr, g->dep(i)); + g->update(i, new_f, new_pr, g->dep(i)); } } g->inc_depth(); @@ -2558,7 +2561,7 @@ class qe_lite_tactic : public tactic { } }; - + params_ref m_params; imp * m_imp; @@ -2567,7 +2570,7 @@ public: m_params(p) { m_imp = alloc(imp, m, p); } - + virtual ~qe_lite_tactic() { dealloc(m_imp); } @@ -2581,20 +2584,20 @@ public: // m_imp->updt_params(p); } - + virtual void collect_param_descrs(param_descrs & r) { // m_imp->collect_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) { (*m_imp)(in, result, mc, pc, core); } - + virtual void collect_statistics(statistics & st) const { // m_imp->collect_statistics(st); } @@ -2603,13 +2606,13 @@ public: // m_imp->reset_statistics(); } - + virtual void cleanup() { ast_manager & m = m_imp->m; dealloc(m_imp); m_imp = alloc(imp, m, m_params); } - + }; tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/qe/qe_lite.h b/src/qe/qe_lite.h index 48874f5cf..cff547f36 100644 --- a/src/qe/qe_lite.h +++ b/src/qe/qe_lite.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Light weight partial quantifier-elimination procedures + Light weight partial quantifier-elimination procedures Author: @@ -31,14 +31,14 @@ class qe_lite { class impl; impl * m_impl; public: - qe_lite(ast_manager& m); + qe_lite(ast_manager & m, params_ref const & p); ~qe_lite(); /** \brief - Apply light-weight quantifier elimination - on constants provided as vector of variables. + Apply light-weight quantifier elimination + on constants provided as vector of variables. Return the updated formula and updated set of variables that were not eliminated. */ @@ -66,4 +66,4 @@ tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref()) ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)") */ -#endif +#endif diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index c091f6973..7a9938cd0 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -246,13 +246,15 @@ namespace smt { simple_justification::simple_justification(region & r, unsigned num_lits, literal const * lits): m_num_literals(num_lits) { - m_literals = new (r) literal[num_lits]; - memcpy(m_literals, lits, sizeof(literal) * num_lits); + if (num_lits != 0) { + m_literals = new (r) literal[num_lits]; + memcpy(m_literals, lits, sizeof(literal) * num_lits); #ifdef Z3DEBUG - for (unsigned i = 0; i < num_lits; i++) { - SASSERT(lits[i] != null_literal); - } + for (unsigned i = 0; i < num_lits; i++) { + SASSERT(lits[i] != null_literal); + } #endif + } } void simple_justification::get_antecedents(conflict_resolution & cr) { diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index e395433f5..8cfc27950 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -34,6 +34,7 @@ class elim_small_bv_tactic : public tactic { struct rw_cfg : public default_rewriter_cfg { ast_manager & m; + params_ref m_params; bv_util m_util; simplifier m_simp; ref m_mc; @@ -47,6 +48,7 @@ class elim_small_bv_tactic : public tactic { rw_cfg(ast_manager & _m, params_ref const & p) : m(_m), + m_params(p), m_util(_m), m_simp(_m), m_bindings(_m), @@ -119,7 +121,7 @@ class elim_small_bv_tactic : public tactic { return res; } - 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) { TRACE("elim_small_bv_app", expr_ref tmp(m.mk_app(f, num, args), m); tout << "reduce " << tmp << std::endl; ); return BR_FAILED; } @@ -178,7 +180,7 @@ class elim_small_bv_tactic : public tactic { quantifier_ref new_q(m); new_q = m.update_quantifier(q, body); - unused_vars_eliminator el(m); + unused_vars_eliminator el(m, m_params); el(new_q, result); TRACE("elim_small_bv", tout << "elimination result: " << mk_ismt2_pp(result, m) << std::endl; ); @@ -203,6 +205,7 @@ class elim_small_bv_tactic : public tactic { } void updt_params(params_ref const & p) { + m_params = p; m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_max_steps = p.get_uint("max_steps", UINT_MAX); m_max_bits = p.get_uint("max_bits", 4); @@ -305,7 +308,7 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); + std::swap(d, m_imp); dealloc(d); } diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index 769f415f2..5d525a836 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -24,9 +24,9 @@ class distribute_forall_tactic : public tactic { ast_manager & m; rw_cfg(ast_manager & _m):m(_m) {} - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { @@ -34,7 +34,7 @@ class distribute_forall_tactic : public tactic { if (!old_q->is_forall()) { return false; } - + if (m.is_not(new_body) && m.is_or(to_app(new_body)->get_arg(0))) { // (forall X (not (or F1 ... Fn))) // --> @@ -50,13 +50,13 @@ class distribute_forall_tactic : public tactic { quantifier_ref tmp_q(m); tmp_q = m.update_quantifier(old_q, not_arg); expr_ref new_q(m); - elim_unused_vars(m, tmp_q, new_q); + elim_unused_vars(m, tmp_q, params_ref(), new_q); new_args.push_back(new_q); } result = m.mk_and(new_args.size(), new_args.c_ptr()); return true; } - + if (m.is_and(new_body)) { // (forall X (and F1 ... Fn)) // --> @@ -70,20 +70,20 @@ class distribute_forall_tactic : public tactic { quantifier_ref tmp_q(m); tmp_q = m.update_quantifier(old_q, arg); expr_ref new_q(m); - elim_unused_vars(m, tmp_q, new_q); + elim_unused_vars(m, tmp_q, params_ref(), new_q); new_args.push_back(new_q); } result = m.mk_and(new_args.size(), new_args.c_ptr()); return true; } - + return false; } }; struct rw : public rewriter_tpl { rw_cfg m_cfg; - + rw(ast_manager & m, bool proofs_enabled): rewriter_tpl(m, proofs_enabled, m_cfg), m_cfg(m) { @@ -99,19 +99,19 @@ public: return alloc(distribute_forall_tactic); } - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, + virtual 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()); ast_manager & m = g->m(); bool produce_proofs = g->proofs_enabled(); rw r(m, produce_proofs); - m_rw = &r; + m_rw = &r; mc = 0; pc = 0; core = 0; result.reset(); tactic_report report("distribute-forall", *g); - + expr_ref new_curr(m); proof_ref new_pr(m); unsigned size = g->size(); @@ -126,12 +126,12 @@ public: } g->update(idx, new_curr, new_pr, g->dep(idx)); } - + g->inc_depth(); result.push_back(g.get()); TRACE("distribute-forall", g->display(tout);); SASSERT(g->is_well_sorted()); - m_rw = 0; + m_rw = 0; } virtual void cleanup() {} diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp index 40fdf5e3e..f5f18d234 100644 --- a/src/tactic/ufbv/ufbv_rewriter.cpp +++ b/src/tactic/ufbv/ufbv_rewriter.cpp @@ -49,7 +49,7 @@ ufbv_rewriter::~ufbv_rewriter() { bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) const { if (e->get_kind() == AST_QUANTIFIER) { quantifier * q = to_quantifier(e); - if (q->is_forall()) { + if (q->is_forall()) { expr * qe = q->get_expr(); if ((m_manager.is_eq(qe) || m_manager.is_iff(qe))) { app * eq = to_app(q->get_expr()); @@ -61,7 +61,7 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) << mk_pp(lhs, m_manager) << "\n" << mk_pp(rhs, m_manager) << "\n" << "subset: " << subset << ", smaller: " << smaller << "\n";); - // We only track uninterpreted functions, everything else is likely too expensive. + // We only track uninterpreted functions, everything else is likely too expensive. if ((subset == +1 || subset == +2) && smaller == +1) { if (is_uninterp(rhs)) { large = rhs; @@ -78,7 +78,7 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) } #endif } - + if ((subset == -1 || subset == +2) && smaller == -1) { if (is_uninterp(lhs)) { large = lhs; @@ -113,13 +113,13 @@ bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) return false; } -class var_set_proc { +class var_set_proc { uint_set & m_set; public: var_set_proc(uint_set &s):m_set(s) {} void operator()(var * n) { m_set.insert(n->get_idx()); } void operator()(quantifier * n) {} - void operator()(app * n) {} + void operator()(app * n) {} }; int ufbv_rewriter::is_subset(expr * e1, expr * e2) const { @@ -132,10 +132,10 @@ int ufbv_rewriter::is_subset(expr * e1, expr * e2) const { for_each_expr(proc1, e1); var_set_proc proc2(ev2); for_each_expr(proc2, e2); - - return (ev1==ev2 ) ? +2 : // We return +2 if the sets are equal. - (ev1.subset_of(ev2)) ? +1 : - (ev2.subset_of(ev1)) ? -1 : + + return (ev1==ev2 ) ? +2 : // We return +2 if the sets are equal. + (ev1.subset_of(ev2)) ? +1 : + (ev2.subset_of(ev1)) ? -1 : 0 ; } @@ -154,8 +154,8 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const { else if (is_uninterp(e1) && !is_uninterp(e2)) return -1; - // two uninterpreted functions are ordered first by the number of - // arguments, then by their id. + // two uninterpreted functions are ordered first by the number of + // arguments, then by their id. if (is_uninterp(e1) && is_uninterp(e2)) { if (to_app(e1)->get_num_args() < to_app(e2)->get_num_args()) return +1; @@ -163,10 +163,10 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const { return -1; else { unsigned a = to_app(e1)->get_decl()->get_id(); - unsigned b = to_app(e2)->get_decl()->get_id(); - if (a < b) + unsigned b = to_app(e2)->get_decl()->get_id(); + if (a < b) return +1; - else if (a > b) + else if (a > b) return -1; } } @@ -185,8 +185,8 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const { default: UNREACHABLE(); } - return (sz1 == sz2) ? 0 : - (sz1 < sz2) ? +1 : + return (sz1 == sz2) ? 0 : + (sz1 < sz2) ? +1 : -1 ; } @@ -194,9 +194,9 @@ class max_var_id_proc { unsigned m_max_var_id; public: max_var_id_proc(void):m_max_var_id(0) {} - void operator()(var * n) { - if(n->get_idx() > m_max_var_id) - m_max_var_id = n->get_idx(); + void operator()(var * n) { + if(n->get_idx() > m_max_var_id) + m_max_var_id = n->get_idx(); } void operator()(quantifier * n) {} void operator()(app * n) {} @@ -206,7 +206,7 @@ public: unsigned ufbv_rewriter::max_var_id(expr * e) { max_var_id_proc proc; - for_each_expr(proc, e); + for_each_expr(proc, e); return proc.get_max(); } @@ -219,14 +219,14 @@ void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demo func_decl * fd = to_app(large)->get_decl(); fwd_idx_map::iterator it = m_fwd_idx.find_iterator(fd); - if (it == m_fwd_idx.end()) { - quantifier_set * qs = alloc(quantifier_set, 1); + if (it == m_fwd_idx.end()) { + quantifier_set * qs = alloc(quantifier_set, 1); m_fwd_idx.insert(fd, qs); it = m_fwd_idx.find_iterator(fd); } SASSERT(it->m_value); - it->m_value->insert(demodulator); + it->m_value->insert(demodulator); m_manager.inc_ref(demodulator); m_manager.inc_ref(large); @@ -238,13 +238,13 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) { TRACE("demodulator_fwd", tout << "REMOVE: " << std::hex << (size_t)demodulator << std::endl; ); fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f); - if (it != m_fwd_idx.end()) { + if (it != m_fwd_idx.end()) { demodulator2lhs_rhs::iterator fit = m_demodulator2lhs_rhs.find_iterator(demodulator); m_manager.dec_ref(fit->m_value.first); m_manager.dec_ref(fit->m_value.second); m_manager.dec_ref(demodulator); m_demodulator2lhs_rhs.erase(demodulator); - it->m_value->erase(demodulator); + it->m_value->erase(demodulator); } else { SASSERT(m_demodulator2lhs_rhs.contains(demodulator)); } @@ -281,13 +281,13 @@ void ufbv_rewriter::show_fwd_idx(std::ostream & out) { } } -bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector & m_new_args, expr_ref & np) { +bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector & m_new_args, expr_ref & np) { fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f); if (it != m_fwd_idx.end()) { TRACE("demodulator_bug", tout << "trying to rewrite: " << f->get_name() << " args:\n"; for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m_manager) << "\n"; }); quantifier_set::iterator dit = it->m_value->begin(); - quantifier_set::iterator dend = it->m_value->end(); + quantifier_set::iterator dend = it->m_value->end(); for ( ; dit != dend ; dit++ ) { quantifier * d = *dit; @@ -302,7 +302,7 @@ bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector & m_new_args, expr_ TRACE("demodulator_bug", tout << "Matching with demodulator: " << mk_pp(d, m_manager) << std::endl; ); SASSERT(large->get_decl() == f); - + if (m_match_subst(large, l_s.second, m_new_args.c_ptr(), np)) { TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(l_s.second, m_manager) << "\n===>\n" << mk_pp(np, m_manager) << "\n";); return true; @@ -331,22 +331,22 @@ void ufbv_rewriter::rewrite_cache(expr * e, expr * new_e, bool done) { } expr * ufbv_rewriter::rewrite(expr * n) { - if (m_fwd_idx.empty()) + if (m_fwd_idx.empty()) return n; TRACE("demodulator", tout << "rewrite: " << mk_pp(n, m_manager) << std::endl; ); app * a; - + SASSERT(m_rewrite_todo.empty()); m_rewrite_cache.reset(); - + m_rewrite_todo.push_back(n); while (!m_rewrite_todo.empty()) { TRACE("demodulator_stack", tout << "STACK: " << std::endl; - for ( unsigned i = 0; iget_decl(); m_new_args.reset(); @@ -389,12 +389,12 @@ expr * ufbv_rewriter::rewrite(expr * n) { // No pop. } else { if(all_untouched) { - rewrite_cache(e, actual, true); - } + rewrite_cache(e, actual, true); + } else { expr_ref na(m_manager); if (f->get_family_id() != m_manager.get_basic_family_id()) - na = m_manager.mk_app(f, m_new_args.size(), m_new_args.c_ptr()); + na = m_manager.mk_app(f, m_new_args.size(), m_new_args.c_ptr()); else m_bsimp.reduce(f, m_new_args.size(), m_new_args.c_ptr(), na); TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m_manager) << "\nnew_args: \n"; @@ -405,9 +405,9 @@ expr * ufbv_rewriter::rewrite(expr * n) { } m_rewrite_todo.pop_back(); } - } + } break; - case AST_QUANTIFIER: { + case AST_QUANTIFIER: { expr * body = to_quantifier(actual)->get_expr(); if (m_rewrite_cache.contains(body)) { const expr_bool_pair ebp = m_rewrite_cache.get(body); @@ -417,13 +417,13 @@ expr * ufbv_rewriter::rewrite(expr * n) { q = m_manager.update_quantifier(to_quantifier(actual), new_body); m_new_exprs.push_back(q); expr_ref new_q(m_manager); - elim_unused_vars(m_manager, q, new_q); + elim_unused_vars(m_manager, q, params_ref(), new_q); m_new_exprs.push_back(new_q); - rewrite_cache(e, new_q, true); + rewrite_cache(e, new_q, true); m_rewrite_todo.pop_back(); } else { m_rewrite_todo.push_back(body); - } + } break; } default: @@ -437,7 +437,7 @@ expr * ufbv_rewriter::rewrite(expr * n) { expr * r = ebp.first; TRACE("demodulator", tout << "rewrite result: " << mk_pp(r, m_manager) << std::endl; ); - + return r; } @@ -448,7 +448,7 @@ public: add_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {} void operator()(var * n) {} void operator()(quantifier * n) {} - void operator()(app * n) { + void operator()(app * n) { // We track only uninterpreted and constant functions. if (n->get_num_args()==0) return; SASSERT(m_expr && m_expr != (expr*) 0x00000003); @@ -464,7 +464,7 @@ public: m_back_idx.insert(d, e); } } - } + } }; class ufbv_rewriter::remove_back_idx_proc { @@ -473,15 +473,15 @@ class ufbv_rewriter::remove_back_idx_proc { public: remove_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {} void operator()(var * n) {} - void operator()(quantifier * n) {} - void operator()(app * n) { + void operator()(quantifier * n) {} + void operator()(app * n) { // We track only uninterpreted and constant functions. if (n->get_num_args()==0) return; func_decl * d=n->get_decl(); - if (d->get_family_id() == null_family_id) { + if (d->get_family_id() == null_family_id) { back_idx_map::iterator it = m_back_idx.find_iterator(d); if (it != m_back_idx.end()) { - SASSERT(it->m_value); + SASSERT(it->m_value); it->m_value->remove(m_expr); } } @@ -489,12 +489,12 @@ public: }; void ufbv_rewriter::reschedule_processed(func_decl * f) { - //use m_back_idx to find all formulas p in m_processed that contains f { + //use m_back_idx to find all formulas p in m_processed that contains f { back_idx_map::iterator it = m_back_idx.find_iterator(f); if (it != m_back_idx.end()) { SASSERT(it->m_value); expr_set temp; - + expr_set::iterator sit = it->m_value->begin(); expr_set::iterator send = it->m_value->end(); for ( ; sit != send ; sit++ ) { @@ -502,7 +502,7 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) { if (m_processed.contains(p)) temp.insert(p); } - + sit = temp.begin(); send = temp.end(); for ( ; sit != send; sit++) { @@ -511,7 +511,7 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) { m_processed.remove(p); remove_back_idx_proc proc(m_back_idx, p); // this could change it->m_value, thus we need the `temp' set. for_each_expr(proc, p); - // insert p into m_todo + // insert p into m_todo m_todo.push_back(p); } } @@ -529,40 +529,40 @@ bool ufbv_rewriter::can_rewrite(expr * n, expr * lhs) { while (!stack.empty()) { curr = stack.back(); - + if (visited.is_marked(curr)) { stack.pop_back(); continue; } switch(curr->get_kind()) { - case AST_VAR: + case AST_VAR: visited.mark(curr, true); stack.pop_back(); break; case AST_APP: - if (for_each_expr_args(stack, visited, to_app(curr)->get_num_args(), to_app(curr)->get_args())) { + if (for_each_expr_args(stack, visited, to_app(curr)->get_num_args(), to_app(curr)->get_args())) { if (m_match_subst(lhs, curr)) return true; visited.mark(curr, true); stack.pop_back(); } break; - + case AST_QUANTIFIER: - if (!for_each_expr_args(stack, visited, to_quantifier(curr)->get_num_patterns(), + if (!for_each_expr_args(stack, visited, to_quantifier(curr)->get_num_patterns(), to_quantifier(curr)->get_patterns())) { break; } - if (!for_each_expr_args(stack, visited, to_quantifier(curr)->get_num_no_patterns(), + if (!for_each_expr_args(stack, visited, to_quantifier(curr)->get_num_no_patterns(), to_quantifier(curr)->get_no_patterns())) { break; } if (!visited.is_marked(to_quantifier(curr)->get_expr())) { stack.push_back(to_quantifier(curr)->get_expr()); break; - } + } stack.pop_back(); break; @@ -597,7 +597,7 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { expr * occ = *esit; if (!is_quantifier(occ)) - continue; + continue; // Use the fwd idx to find out whether this is a demodulator. demodulator2lhs_rhs::iterator d2lr_it = m_demodulator2lhs_rhs.find_iterator(to_quantifier(occ)); @@ -605,22 +605,22 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { l = d2lr_it->m_value.first; quantifier_ref d(m_manager); func_decl_ref df(m_manager); - d = to_quantifier(occ); + d = to_quantifier(occ); df = to_app(l)->get_decl(); // Now we know there is an occurrence of f in d - // if n' can rewrite d { + // if n' can rewrite d { if (can_rewrite(d, lhs)) { TRACE("demodulator", tout << "Rescheduling: " << std::endl << mk_pp(d, m_manager) << std::endl; ); // remove d from m_fwd_idx remove_fwd_idx(df, d); - // remove d from m_back_idx + // remove d from m_back_idx // just remember it here, because otherwise it and/or esit might become invalid? - // to_remove.insert(d); + // to_remove.insert(d); remove_back_idx_proc proc(m_back_idx, d); for_each_expr(proc, d); // insert d into m_todo - m_todo.push_back(d); + m_todo.push_back(d); } } } @@ -629,10 +629,10 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { //for (ptr_vector::iterator it = to_remove.begin(); it != to_remove.end(); it++) { // expr * d = *it; // remove_back_idx_proc proc(m_manager, m_back_idx, d); - // for_each_expr(proc, d); + // for_each_expr(proc, d); //} } - + void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { if (m_manager.proofs_enabled()) { // Let us not waste time with proof production @@ -655,7 +655,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * m_match_subst.reserve(max_vid); - while (!m_todo.empty()) { + while (!m_todo.empty()) { // let n be the next formula in m_todo. expr_ref cur(m_manager); cur = m_todo.back(); @@ -670,21 +670,21 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * expr_ref large(m_manager), small(m_manager); if (!is_demodulator(np, large, small)) { // insert n' into m_processed - m_processed.insert(np); - // update m_back_idx (traverse n' and for each uninterpreted function declaration f in n' add the entry f->n' to m_back_idx) + m_processed.insert(np); + // update m_back_idx (traverse n' and for each uninterpreted function declaration f in n' add the entry f->n' to m_back_idx) add_back_idx_proc proc(m_back_idx, np); for_each_expr(proc, np); - } else { + } else { // np is a demodulator that allows us to replace 'large' with 'small'. TRACE("demodulator", tout << "Found demodulator: " << std::endl; - tout << mk_pp(large.get(), m_manager) << std::endl << " ---> " << + tout << mk_pp(large.get(), m_manager) << std::endl << " ---> " << std::endl << mk_pp(small.get(), m_manager) << std::endl; ); TRACE("demodulator_s", tout << "Found demodulator: " << std::endl; - tout << to_app(large)->get_decl()->get_name() << + tout << to_app(large)->get_decl()->get_name() << "[" << to_app(large)->get_depth() << "]" << " ---> "; if (is_app(small)) - tout << to_app(small)->get_decl()->get_name() << + tout << to_app(small)->get_decl()->get_name() << "[" << to_app(small)->get_depth() << "]" << std::endl; else tout << mk_pp(small.get(), m_manager) << std::endl; ); @@ -695,14 +695,14 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * reschedule_processed(f); reschedule_demodulators(f, large); - + // insert n' into m_fwd_idx insert_fwd_idx(large, small, to_quantifier(np)); // update m_back_idx add_back_idx_proc proc(m_back_idx, np); for_each_expr(proc, np); - } + } } // the result is the contents of m_processed + all demodulators in m_fwd_idx. @@ -743,10 +743,10 @@ ufbv_rewriter::match_subst::match_subst(ast_manager & m): */ struct match_args_aux_proc { substitution & m_subst; - struct no_match {}; - + struct no_match {}; + match_args_aux_proc(substitution & s):m_subst(s) {} - + void operator()(var * n) { expr_offset r; if (m_subst.find(n, 0, r)) { @@ -766,7 +766,7 @@ struct match_args_aux_proc { bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { m_cache.reset(); m_todo.reset(); - + // fill todo-list, and perform quick success/failure tests m_all_args_eq = true; unsigned num_args = lhs->get_num_args(); @@ -777,21 +777,21 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { m_all_args_eq = false; if (is_app(t_arg) && is_app(i_arg) && to_app(t_arg)->get_decl() != to_app(i_arg)->get_decl()) { // quick failure... - return false; + return false; } m_todo.push_back(expr_pair(t_arg, i_arg)); } - - if (m_all_args_eq) { + + if (m_all_args_eq) { // quick success worked... return true; } m_subst.reset(); - + while (!m_todo.empty()) { expr_pair const & p = m_todo.back(); - + if (is_var(p.first)) { expr_offset r; if (m_subst.find(to_var(p.first), 0, r)) { @@ -814,7 +814,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { SASSERT(is_app(p.first) && is_app(p.second)); - if (to_app(p.first)->is_ground() && !to_app(p.second)->is_ground()) + if (to_app(p.first)->is_ground() && !to_app(p.second)->is_ground()) return false; if (p.first == p.second && to_app(p.first)->is_ground()) { @@ -827,7 +827,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { m_todo.pop_back(); continue; } - + if (p.first == p.second) { // p.first and p.second is not ground... @@ -855,10 +855,10 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { app * n1 = to_app(p.first); app * n2 = to_app(p.second); - + if (n1->get_decl() != n2->get_decl()) return false; - + unsigned num_args1 = n1->get_num_args(); if (num_args1 != n2->get_num_args()) return false; @@ -867,7 +867,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { if (num_args1 == 0) continue; - + m_cache.insert(p); unsigned j = num_args1; while (j > 0) { @@ -886,7 +886,7 @@ bool ufbv_rewriter::match_subst::operator()(app * lhs, expr * rhs, expr * const new_rhs = rhs; return true; } - unsigned deltas[2] = { 0, 0 }; + unsigned deltas[2] = { 0, 0 }; m_subst.apply(2, deltas, expr_offset(rhs, 0), new_rhs); return true; }