From a4d9642cf2d9bec78288b53e2af33003e21c5a04 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 Dec 2015 09:46:18 -0800 Subject: [PATCH 1/3] parsing of SMT 2.5 style string literals Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2scanner.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index 18d40d48f..bc62c2646 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -171,11 +171,17 @@ namespace smt2 { throw scanner_exception("unexpected end of string", m_line, m_spos); if (c == '\"') { next(); - m_string.push_back(0); - return STRING_TOKEN; + if (curr() == '\"') { + m_string.push_back(c); + } + else { + m_string.push_back(0); + return STRING_TOKEN; + } } - if (c == '\n') + else if (c == '\n') { new_line(); + } else if (c == '\\') { next(); c = curr(); From 3f02beb8203bb4bf68e39a168254fc97e8f75338 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 Dec 2015 10:18:40 -0800 Subject: [PATCH 2/3] reset-assertions resets everything (also declarations, and we take scopes) when global-declarations is false. v2.5 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f863393fb..02b2b6525 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1493,6 +1493,11 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions } void cmd_context::reset_assertions() { + if (!m_global_decls) { + reset(false); + return; + } + if (m_opt) { m_opt = 0; } From 4bbe1d4674bf2ca5eefb2dc2f44659d7a0762079 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Dec 2015 09:23:36 -0800 Subject: [PATCH 3/3] remove unused min-aggregate Signed-off-by: Nikolaj Bjorner --- src/ast/dl_decl_plugin.cpp | 65 +----------------------------------- src/ast/dl_decl_plugin.h | 58 -------------------------------- src/muz/base/dl_rule.h | 7 ---- src/muz/base/dl_rule_set.cpp | 44 +----------------------- src/muz/base/dl_rule_set.h | 1 - src/muz/rel/dl_compiler.cpp | 45 +------------------------ src/muz/rel/dl_compiler.h | 15 --------- 7 files changed, 3 insertions(+), 232 deletions(-) diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 305ac1779..13416c086 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -44,8 +44,7 @@ namespace datalog { m_num_sym("N"), m_lt_sym("<"), m_le_sym("<="), - m_rule_sym("R"), - m_min_sym("min") + m_rule_sym("R") { } @@ -491,65 +490,6 @@ namespace datalog { return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info); } - /** - In SMT2 syntax, we can write \c ((_ min R N) v_0 v_1 ... v_k)) where 0 <= N <= k, - R is a relation of sort V_0 x V_1 x ... x V_k and each v_i is a zero-arity function - (also known as a "constant" in SMT2 parlance) whose range is of sort V_i. - - Example: - - (define-sort number_t () (_ BitVec 2)) - (declare-rel numbers (number_t number_t)) - (declare-rel is_min (number_t number_t)) - - (declare-var x number_t) - (declare-var y number_t) - - (rule (numbers #b00 #b11)) - (rule (numbers #b00 #b01)) - - (rule (=> (and (numbers x y) ((_ min numbers 1) x y)) (is_min x y))) - - This says that we want to find the mininum y grouped by x. - */ - func_decl * dl_decl_plugin::mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters) { - if (num_parameters < 2) { - m_manager->raise_exception("invalid min aggregate definition due to missing parameters"); - return 0; - } - - parameter const & relation_parameter = parameters[0]; - if (!relation_parameter.is_ast() || !is_func_decl(relation_parameter.get_ast())) { - m_manager->raise_exception("invalid min aggregate definition, first parameter is not a function declaration"); - return 0; - } - - func_decl* f = to_func_decl(relation_parameter.get_ast()); - if (!m_manager->is_bool(f->get_range())) { - m_manager->raise_exception("invalid min aggregate definition, first paramater must be a predicate"); - return 0; - } - - parameter const & min_col_parameter = parameters[1]; - if (!min_col_parameter.is_int()) { - m_manager->raise_exception("invalid min aggregate definition, second parameter must be an integer"); - return 0; - } - - if (min_col_parameter.get_int() < 0) { - m_manager->raise_exception("invalid min aggregate definition, second parameter must be non-negative"); - return 0; - } - - if ((unsigned)min_col_parameter.get_int() >= f->get_arity()) { - m_manager->raise_exception("invalid min aggregate definition, second parameter exceeds the arity of the relation"); - return 0; - } - - func_decl_info info(m_family_id, k, num_parameters, parameters); - SASSERT(f->get_info() == 0); - return m_manager->mk_func_decl(m_min_sym, f->get_arity(), f->get_domain(), f->get_range(), info); - } func_decl * dl_decl_plugin::mk_func_decl( decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -678,8 +618,6 @@ namespace datalog { break; } - case OP_DL_MIN: - return mk_min(k, num_parameters, parameters); default: m_manager->raise_exception("operator not recognized"); @@ -691,7 +629,6 @@ namespace datalog { } void dl_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - op_names.push_back(builtin_name(m_min_sym.bare_str(), OP_DL_MIN)); } void dl_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index 4491fe180..66ce45c3c 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -50,7 +50,6 @@ namespace datalog { OP_DL_LT, OP_DL_REP, OP_DL_ABS, - OP_DL_MIN, LAST_RA_OP }; @@ -72,7 +71,6 @@ namespace datalog { symbol m_lt_sym; symbol m_le_sym; symbol m_rule_sym; - symbol m_min_sym; bool check_bounds(char const* msg, unsigned low, unsigned up, unsigned val) const; bool check_domain(unsigned low, unsigned up, unsigned val) const; @@ -96,68 +94,12 @@ namespace datalog { func_decl * mk_compare(decl_kind k, symbol const& sym, sort*const* domain); func_decl * mk_clone(sort* r); func_decl * mk_rule(unsigned arity); - func_decl * mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters); sort * mk_finite_sort(unsigned num_params, parameter const* params); sort * mk_relation_sort(unsigned num_params, parameter const* params); sort * mk_rule_sort(); public: - /** - Is \c decl a min aggregation function? - */ - static bool is_aggregate(const func_decl* const decl) - { - return decl->get_decl_kind() == OP_DL_MIN; - } - - /** - \pre: is_aggregate(aggregate) - - \returns function declaration of predicate which is subject to min aggregation function - */ - static func_decl * min_func_decl(const func_decl* const aggregate) - { - SASSERT(is_aggregate(aggregate)); - parameter const & relation_parameter = aggregate->get_parameter(0); - return to_func_decl(relation_parameter.get_ast()); - } - - /** - \pre: is_aggregate(aggregate) - - \returns column identifier (starting at zero) which is minimized by aggregation function - */ - static unsigned min_col(const func_decl* const aggregate) - { - SASSERT(is_aggregate(aggregate)); - return (unsigned)aggregate->get_parameter(1).get_int(); - } - - /** - \pre: is_aggregate(aggregate) - - \returns column identifiers for the "group by" in the given min aggregation function - */ - static unsigned_vector group_by_cols(const func_decl* const aggregate) - { - SASSERT(is_aggregate(aggregate)); - unsigned _min_col = min_col(aggregate); - if (aggregate->get_arity() == 0U) - return unsigned_vector(); - - unsigned col_num = 0; - unsigned_vector cols(aggregate->get_arity() - 1U); - for (unsigned i = 0; i < cols.size(); ++i, ++col_num) - { - if (col_num == _min_col) - ++col_num; - - cols[i] = col_num; - } - - return cols; - } dl_decl_plugin(); virtual ~dl_decl_plugin() {} diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 34cbffcb7..2261a7a00 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -346,13 +346,6 @@ namespace datalog { bool is_neg_tail(unsigned i) const { SASSERT(i < m_tail_size); return GET_TAG(m_tail[i]) == 1; } - /** - A predicate P(Xj) can be annotated by adding an interpreted predicate of the form ((_ min P N) ...) - where N is the column number that should be used for the min aggregation function. - Such an interpreted predicate is an example for which this function returns true. - */ - bool is_min_tail(unsigned i) const { return dl_decl_plugin::is_aggregate(get_tail(i)->get_decl()); } - /** Check whether predicate p is in the interpreted tail. diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index 4f558a535..5eb8e5f7e 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -400,7 +400,7 @@ namespace datalog { SASSERT(!is_closed()); //the rule_set is not already closed m_deps.populate(*this); m_stratifier = alloc(rule_stratifier, m_deps); - if (!stratified_negation() || !check_min()) { + if (!stratified_negation()) { m_stratifier = 0; m_deps.reset(); return false; @@ -441,48 +441,6 @@ namespace datalog { return true; } - bool rule_set::check_min() { - // For now, we check the following: - // - // if a min aggregation function occurs in an SCC, is this SCC - // free of any other non-monotonic functions, e.g. negation? - const unsigned NEG_BIT = 1U << 0; - const unsigned MIN_BIT = 1U << 1; - - ptr_vector::const_iterator it = m_rules.c_ptr(); - ptr_vector::const_iterator end = m_rules.c_ptr() + m_rules.size(); - unsigned_vector component_status(m_stratifier->get_strats().size()); - - for (; it != end; it++) { - rule * r = *it; - // app * head = r->get_head(); - // func_decl * head_decl = head->get_decl(); - // unsigned head_strat = get_predicate_strat(head_decl); - unsigned n = r->get_tail_size(); - for (unsigned i = 0; i < n; i++) { - func_decl * tail_decl = r->get_tail(i)->get_decl(); - unsigned strat = get_predicate_strat(tail_decl); - - if (r->is_neg_tail(i)) { - SASSERT(strat < component_status.size()); - component_status[strat] |= NEG_BIT; - } - - if (r->is_min_tail(i)) { - SASSERT(strat < component_status.size()); - component_status[strat] |= MIN_BIT; - } - } - } - - const unsigned CONFLICT = NEG_BIT | MIN_BIT; - for (unsigned k = 0; k < component_status.size(); ++k) { - if (component_status[k] == CONFLICT) - return false; - } - - return true; - } void rule_set::replace_rules(const rule_set & src) { if (this != &src) { diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h index b6735aba9..2e7401fea 100644 --- a/src/muz/base/dl_rule_set.h +++ b/src/muz/base/dl_rule_set.h @@ -179,7 +179,6 @@ namespace datalog { void compute_deps(); void compute_tc_deps(); bool stratified_negation(); - bool check_min(); public: rule_set(context & ctx); rule_set(const rule_set & rs); diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index c35985e98..7b26f19c7 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -73,12 +73,6 @@ namespace datalog { vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result)); } - void compiler::make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols, - const unsigned min_col, instruction_block & acc) { - target = get_register(m_reg_signatures[source], true, source); - acc.push_back(instruction::mk_min(source, target, group_by_cols, min_col)); - } - void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond, const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc) { SASSERT(!removed_cols.empty()); @@ -446,29 +440,7 @@ namespace datalog { get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res); } - void compiler::find_min_aggregates(const rule * r, ptr_vector& min_aggregates) { - unsigned ut_len = r->get_uninterpreted_tail_size(); - unsigned ft_len = r->get_tail_size(); // full tail - func_decl * aggregate; - for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { - aggregate = r->get_tail(tail_index)->get_decl(); - if (dl_decl_plugin::is_aggregate(aggregate)) { - min_aggregates.push_back(aggregate); - } - } - } - bool compiler::prepare_min_aggregate(const func_decl * decl, const ptr_vector& min_aggregates, - unsigned_vector & group_by_cols, unsigned & min_col) { - for (unsigned i = 0; i < min_aggregates.size(); ++i) { - if (dl_decl_plugin::min_func_decl(min_aggregates[i]) == decl) { - group_by_cols = dl_decl_plugin::group_by_cols(min_aggregates[i]); - min_col = dl_decl_plugin::min_col(min_aggregates[i]); - return true; - } - } - return false; - } void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, reg_idx delta_reg, bool use_widening, instruction_block & acc) { @@ -496,10 +468,7 @@ namespace datalog { bool dealloc = true; // setup information for min aggregation - ptr_vector min_aggregates; - find_min_aggregates(r, min_aggregates); unsigned_vector group_by_cols; - unsigned min_col; if(pt_len == 2) { reg_idx t1_reg=tail_regs[0]; @@ -509,14 +478,6 @@ namespace datalog { SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args()); SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args()); - if (prepare_min_aggregate(a1->get_decl(), min_aggregates, group_by_cols, min_col)) { - make_min(t1_reg, single_res, group_by_cols, min_col, acc); - } - - if (prepare_min_aggregate(a2->get_decl(), min_aggregates, group_by_cols, min_col)) { - make_min(t2_reg, single_res, group_by_cols, min_col, acc); - } - variable_intersection a1a2(m_context.get_manager()); a1a2.populate(a1,a2); @@ -558,9 +519,6 @@ namespace datalog { single_res = tail_regs[0]; dealloc = false; - if (prepare_min_aggregate(a->get_decl(), min_aggregates, group_by_cols, min_col)) { - make_min(single_res, single_res, group_by_cols, min_col, acc); - } SASSERT(m_reg_signatures[single_res].size() == a->get_num_args()); @@ -645,8 +603,7 @@ namespace datalog { unsigned ft_len = r->get_tail_size(); // full tail ptr_vector tail; for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { - if (!r->is_min_tail(tail_index)) - tail.push_back(r->get_tail(tail_index)); + tail.push_back(r->get_tail(tail_index)); } expr_ref_vector binding(m); diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h index 51be65d01..4126833d1 100644 --- a/src/muz/rel/dl_compiler.h +++ b/src/muz/rel/dl_compiler.h @@ -120,21 +120,6 @@ namespace datalog { instruction_observer m_instruction_observer; expr_free_vars m_free_vars; - /** - \brief Finds all the min aggregation functions in the premise of a given rule. - */ - static void find_min_aggregates(const rule * r, ptr_vector& min_aggregates); - - /** - \brief Decides whether a predicate is subject to a min aggregation function. - - If \c decl is subject to a min aggregation function, the output parameters are written - with the neccessary information. - - \returns true if the output paramaters have been written - */ - static bool prepare_min_aggregate(const func_decl * decl, const ptr_vector& min_aggregates, - unsigned_vector & group_by_cols, unsigned & min_col); /** If true, the union operation on the underlying structure only provides the information