From 971b9d4081a694ad0bd5482977639a963aa53296 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jan 2023 09:32:34 -0800 Subject: [PATCH] fix #6564 fixes to simplifier command front-end --- doc/mk_tactic_doc.py | 2 +- src/api/java/Context.java | 4 +-- src/cmd_context/simplifier_cmds.cpp | 38 +++++++++++++++++------------ src/cmd_context/tactic_cmds.cpp | 21 +++++++++++----- src/cmd_context/tactic_cmds.h | 1 + src/solver/simplifier_solver.cpp | 3 +-- 6 files changed, 43 insertions(+), 26 deletions(-) diff --git a/doc/mk_tactic_doc.py b/doc/mk_tactic_doc.py index 38b9be40a..86e32aa18 100644 --- a/doc/mk_tactic_doc.py +++ b/doc/mk_tactic_doc.py @@ -55,7 +55,7 @@ def extract_tactic_doc(ous, f): generate_tactic_doc(ous, f, ins) def generate_simplifier_doc(ous, name, desc): - ous.write("## Simplifier [" + name + "](summary/#tactic-" + name + ")\n") + ous.write("## Simplifier [" + name + "](../summary/#tactic-" + name + ")\n") ous.write("### Description\n" + desc + "\n") diff --git a/src/api/java/Context.java b/src/api/java/Context.java index bb3f6fe8e..d48101235 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2110,7 +2110,7 @@ public class Context implements AutoCloseable { * Check if the string s1 is lexicographically strictly less than s2. */ - public BoolExpr MkStringLt(SeqSort s1, SeqSort s2) + public BoolExpr MkStringLt(Expr> s1, Expr> s2) { checkContextMatch(s1, s2); return new BoolExpr(this, Native.mkStrLt(nCtx(), s1.getNativeObject(), s2.getNativeObject())); @@ -2119,7 +2119,7 @@ public class Context implements AutoCloseable { /** * Check if the string s1 is lexicographically less or equal to s2. */ - public BoolExpr MkStringLe(SeqSort s1, SeqSort s2) + public BoolExpr MkStringLe(Expr> s1, Expr> s2) { checkContextMatch(s1, s2); return new BoolExpr(this, Native.mkStrLe(nCtx(), s1.getNativeObject(), s2.getNativeObject())); diff --git a/src/cmd_context/simplifier_cmds.cpp b/src/cmd_context/simplifier_cmds.cpp index 47f20f3fd..0ea88e095 100644 --- a/src/cmd_context/simplifier_cmds.cpp +++ b/src/cmd_context/simplifier_cmds.cpp @@ -14,6 +14,7 @@ Author: --*/ #include +#include #include "cmd_context/simplifier_cmds.h" #include "cmd_context/cmd_context.h" #include "cmd_context/cmd_util.h" @@ -32,15 +33,13 @@ static simplifier_factory mk_and_then(cmd_context & ctx, sexpr * n) { throw cmd_exception("invalid and-then combinator, at least one argument expected", n->get_line(), n->get_pos()); if (num_children == 2) return sexpr2simplifier(ctx, n->get_child(1)); - scoped_ptr> args = alloc(vector); + std::vector args; for (unsigned i = 1; i < num_children; i++) - args->push_back(sexpr2simplifier(ctx, n->get_child(i))); - vector* _args = args.detach(); - simplifier_factory result = [_args](ast_manager& m, const params_ref& p, dependent_expr_state& st) { + args.push_back(sexpr2simplifier(ctx, n->get_child(i))); + simplifier_factory result = [args](ast_manager& m, const params_ref& p, dependent_expr_state& st) { scoped_ptr s = alloc(seq_simplifier, m, p, st); - for (auto & simp : *_args) + for (auto & simp : args) s->add_simplifier(simp(m, p, st)); - dealloc(_args); return s.detach(); }; return result; @@ -53,15 +52,22 @@ static simplifier_factory mk_using_params(cmd_context & ctx, sexpr * n) { throw cmd_exception("invalid using-params combinator, at least one argument expected", n->get_line(), n->get_pos()); if (num_children == 2) return sexpr2simplifier(ctx, n->get_child(1)); - simplifier_factory t = sexpr2simplifier(ctx, n->get_child(1)); -#if 0 - // hoist parameter parsing code from tactic_cmds to share. + ast_manager& m = ctx.get_ast_manager(); + default_dependent_expr_state st(m); + + simplifier_factory fac = sexpr2simplifier(ctx, n->get_child(1)); + params_ref p; param_descrs descrs; - t->collect_param_descrs(descrs); - -#endif - return t; -// return using_params(t.detach(), p); + scoped_ptr s = fac(m, p, st); + s->collect_param_descrs(descrs); + params_ref params = sexpr2params(ctx, n, descrs); + simplifier_factory result = [params, fac](auto& m, auto& p, auto& s) { + params_ref pp; + pp.append(params); + pp.append(p); + return fac(m, pp, s); + }; + return result; } @@ -82,6 +88,8 @@ simplifier_factory sexpr2simplifier(cmd_context & ctx, sexpr * n) { symbol const & cmd_name = head->get_symbol(); if (cmd_name == "and-then" || cmd_name == "then") return mk_and_then(ctx, n); + else if (cmd_name == "!" || cmd_name == "using-params" || cmd_name == "with") + return mk_using_params(ctx, n); else throw cmd_exception("invalid tactic, unknown tactic combinator ", cmd_name, n->get_line(), n->get_pos()); } @@ -95,7 +103,7 @@ void help_simplifier(cmd_context & ctx) { std::ostringstream buf; buf << "combinators:\n"; buf << "- (and-then +) executes the given simplifiers sequentially.\n"; - // buf << "- (using-params *) executes the given tactic using the given attributes, where ::= . ! is a syntax sugar for using-params.\n"; + buf << "- (using-params *) executes the given simplifier using the given attributes, where ::= . ! is syntax sugar for using-params.\n"; buf << "builtin simplifiers:\n"; for (simplifier_cmd* cmd : ctx.simplifiers()) { buf << "- " << cmd->get_name() << " " << cmd->get_descr() << "\n"; diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index af030e139..4559586f3 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -481,16 +481,11 @@ static tactic * mk_repeat(cmd_context & ctx, sexpr * n) { return repeat(t, max); } -static tactic * mk_using_params(cmd_context & ctx, sexpr * n) { +params_ref sexpr2params(cmd_context& ctx, sexpr * n, param_descrs const& descrs) { SASSERT(n->is_composite()); unsigned num_children = n->get_num_children(); if (num_children < 2) throw cmd_exception("invalid using-params combinator, at least one argument expected", n->get_line(), n->get_pos()); - if (num_children == 2) - return sexpr2tactic(ctx, n->get_child(1)); - tactic_ref t = sexpr2tactic(ctx, n->get_child(1)); - param_descrs descrs; - t->collect_param_descrs(descrs); params_ref p; unsigned i = 2; while (i < num_children) { @@ -535,6 +530,20 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) { throw cmd_exception("invalid using-params combinator, unsupported parameter kind"); } } + return p; +} + +static tactic * mk_using_params(cmd_context & ctx, sexpr * n) { + SASSERT(n->is_composite()); + unsigned num_children = n->get_num_children(); + if (num_children < 2) + throw cmd_exception("invalid using-params combinator, at least one argument expected", n->get_line(), n->get_pos()); + if (num_children == 2) + return sexpr2tactic(ctx, n->get_child(1)); + tactic_ref t = sexpr2tactic(ctx, n->get_child(1)); + param_descrs descrs; + t->collect_param_descrs(descrs); + params_ref p = sexpr2params(ctx, n, descrs); return using_params(t.get(), p); } diff --git a/src/cmd_context/tactic_cmds.h b/src/cmd_context/tactic_cmds.h index be094840c..5096ae962 100644 --- a/src/cmd_context/tactic_cmds.h +++ b/src/cmd_context/tactic_cmds.h @@ -44,6 +44,7 @@ public: void install_core_tactic_cmds(cmd_context & ctx); tactic * sexpr2tactic(cmd_context & ctx, sexpr * n); +params_ref sexpr2params(cmd_context& ctx, sexpr * n, param_descrs const& descr); class probe_info { symbol m_name; diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index faaf5b28f..6cdb4cd59 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -308,9 +308,8 @@ public: void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { s->user_propagate_register_final(final_eh); } void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { s->user_propagate_register_eq(eq_eh); } void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { s->user_propagate_register_diseq(diseq_eh); } - void user_propagate_register_expr(expr* e) override { /*m_preprocess.user_propagate_register_expr(e); */ s->user_propagate_register_expr(e); } + void user_propagate_register_expr(expr* e) override { m_preprocess_state.freeze(e); s->user_propagate_register_expr(e); } void user_propagate_register_created(user_propagator::created_eh_t& r) override { s->user_propagate_register_created(r); } - // void user_propagate_clear() override { m_preprocess.user_propagate_clear(); s->user_propagate_clear(); } };