mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1a859d4591
commit
77bbae65f5
|
@ -453,7 +453,8 @@ namespace datalog {
|
|||
return new_pred;
|
||||
}
|
||||
|
||||
void context::add_rule(expr* rl, symbol const& name, unsigned bound) {
|
||||
void context::add_rule(expr* rl, symbol const& name, unsigned bound) {
|
||||
SASSERT(rl);
|
||||
m_rule_fmls.push_back(rl);
|
||||
m_rule_names.push_back(name);
|
||||
m_rule_bounds.push_back(bound);
|
||||
|
|
|
@ -189,11 +189,12 @@ public:
|
|||
m_bound = bound;
|
||||
m_arg_idx++;
|
||||
}
|
||||
virtual void reset(cmd_context & ctx) { m_dl_ctx->reset(); prepare(ctx); }
|
||||
virtual void reset(cmd_context & ctx) { m_dl_ctx->reset(); prepare(ctx); m_t = nullptr; }
|
||||
virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; m_bound = UINT_MAX; }
|
||||
virtual void finalize(cmd_context & ctx) {
|
||||
}
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
if (!m_t) throw cmd_exception("invalid rule, expected formula");
|
||||
m_dl_ctx->add_rule(m_t, m_name, m_bound);
|
||||
}
|
||||
};
|
||||
|
|
|
@ -1881,6 +1881,8 @@ namespace smt2 {
|
|||
// the resultant expression is on the top of the stack
|
||||
TRACE("let_frame", tout << "let result expr: " << mk_pp(expr_stack().back(), m()) << "\n";);
|
||||
expr_ref r(m());
|
||||
if (expr_stack().empty())
|
||||
throw parser_exception("invalid let expression");
|
||||
r = expr_stack().back();
|
||||
expr_stack().pop_back();
|
||||
// remove local declarations from the stack
|
||||
|
|
Loading…
Reference in a new issue