From f24ecde35c29b46706f736f5f29982d4016fb74a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 1 Dec 2022 09:31:52 +0900
Subject: [PATCH] wip - fixes to simplifiers
---
src/ast/simplifiers/elim_term_ite.h | 6 +---
src/ast/simplifiers/elim_unconstrained.cpp | 4 +++
src/ast/simplifiers/flatten_clauses.h | 36 +++++++++++++++++-----
src/ast/simplifiers/push_ite.h | 1 -
src/sat/sat_solver/sat_smt_solver.cpp | 2 +-
5 files changed, 34 insertions(+), 15 deletions(-)
diff --git a/src/ast/simplifiers/elim_term_ite.h b/src/ast/simplifiers/elim_term_ite.h
index 6455db321..5b6ef38fa 100644
--- a/src/ast/simplifiers/elim_term_ite.h
+++ b/src/ast/simplifiers/elim_term_ite.h
@@ -15,7 +15,7 @@ Author:
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
-#include "ast/normal_forms/elim_term_ite.h""
+#include "ast/normal_forms/elim_term_ite.h"
class elim_term_ite_simplifier : public dependent_expr_simplifier {
@@ -32,13 +32,9 @@ public:
char const* name() const override { return "elim-term-ite"; }
void reduce() override {
- if (!m_fmls.has_quantifiers())
- return;
expr_ref r(m);
for (unsigned idx : indices()) {
auto const& d = m_fmls[idx];
- if (!has_quantifiers(d.fml()))
- continue;
m_rewriter(d.fml(), r);
m_fmls.update(idx, dependent_expr(m, r, d.dep()));
}
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index d9fe5d480..713d7941c 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -130,6 +130,7 @@ void elim_unconstrained::init_nodes() {
m_trail.append(terms);
m_heap.reset();
m_root.reset();
+ m_nodes.reset();
// initialize nodes for terms in the original goal
init_terms(terms);
@@ -159,6 +160,7 @@ void elim_unconstrained::init_terms(expr_ref_vector const& terms) {
n.m_orig = e;
n.m_term = e;
n.m_refcount = 0;
+
if (is_uninterp_const(e))
m_heap.insert(root(e));
if (is_quantifier(e)) {
@@ -250,6 +252,8 @@ void elim_unconstrained::assert_normalized(vector<dependent_expr>& old_fmls) {
void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<dependent_expr> const& old_fmls) {
auto& trail = m_fmls.model_trail();
+ // fresh declarations are added first since
+ // model reconstruction proceeds in reverse order of stack.
for (auto const& entry : mc.entries()) {
switch (entry.m_instruction) {
case generic_model_converter::instruction::HIDE:
diff --git a/src/ast/simplifiers/flatten_clauses.h b/src/ast/simplifiers/flatten_clauses.h
index 02444f093..aa81024ef 100644
--- a/src/ast/simplifiers/flatten_clauses.h
+++ b/src/ast/simplifiers/flatten_clauses.h
@@ -28,7 +28,11 @@ class flatten_clauses : public dependent_expr_simplifier {
bool is_literal(expr* a) {
m.is_not(a, a);
- return !is_app(a) || to_app(a)->get_num_args() == 0;
+ if (m.is_eq(a) && !m.is_iff(a))
+ return true;
+ if (!is_app(a))
+ return true;
+ return to_app(a)->get_family_id() != m.get_basic_family_id();
}
bool is_reducible(expr* a, expr* b) {
@@ -49,14 +53,14 @@ public:
}
void reduce() override {
- bool change = true;
-
- while (change) {
- change = false;
+ unsigned nf = m_num_flat + 1;
+ while (nf != m_num_flat) {
+ nf = m_num_flat;
for (unsigned idx : indices()) {
auto de = m_fmls[idx];
expr* f = de.fml(), *a, *b, *c;
bool decomposed = false;
+ // (or a (not (or b_i)) => and_i (or a (not b_i))
if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && is_reducible(a, b))
decomposed = true;
else if (m.is_or(f, b, a) && m.is_not(b, b) && m.is_or(b) && is_reducible(a, b))
@@ -65,10 +69,10 @@ public:
for (expr* arg : *to_app(b))
m_fmls.add(dependent_expr(m, m.mk_or(a, mk_not(m, arg)), de.dep()));
m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
- change = true;
++m_num_flat;
continue;
}
+ // (or a (and b_i)) => and_i (or a b_i)
if (m.is_or(f, a, b) && m.is_and(b) && is_reducible(a, b))
decomposed = true;
else if (m.is_or(f, b, a) && m.is_and(b) && is_reducible(a, b))
@@ -77,7 +81,24 @@ public:
for (expr * arg : *to_app(b))
m_fmls.add(dependent_expr(m, m.mk_or(a, arg), de.dep()));
m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
- change = true;
+ ++m_num_flat;
+ continue;
+ }
+ // not (and a (or b_i)) => and_i (not a) or (not b_i)
+ if (m.is_not(f, c) && m.is_and(c, a, b) && m.is_or(b) && is_reducible(a, b))
+ decomposed = true;
+ else if (m.is_not(f, c) && m.is_and(c, b, a) && m.is_or(b) && is_reducible(a, b))
+ decomposed = true;
+ if (decomposed) {
+ expr* na = mk_not(m, a);
+ for (expr* arg : *to_app(b))
+ m_fmls.add(dependent_expr(m, m.mk_or(na, arg), de.dep()));
+ m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
+ ++m_num_flat;
+ continue;
+ }
+ if (m.is_implies(f, a, b)) {
+ m_fmls.update(idx, dependent_expr(m, m.mk_or(mk_not(m, a), b), de.dep()));
++m_num_flat;
continue;
}
@@ -85,7 +106,6 @@ public:
m_fmls.add(dependent_expr(m, m.mk_or(mk_not(m, a), b), de.dep()));
m_fmls.add(dependent_expr(m, m.mk_or(a, c), de.dep()));
m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
- change = true;
++m_num_flat;
continue;
}
diff --git a/src/ast/simplifiers/push_ite.h b/src/ast/simplifiers/push_ite.h
index e2acdbdb0..e26070a7e 100644
--- a/src/ast/simplifiers/push_ite.h
+++ b/src/ast/simplifiers/push_ite.h
@@ -38,7 +38,6 @@ public:
m_fmls.update(idx, dependent_expr(m, r, d.dep()));
}
}
-
};
diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp
index c544df6fa..3fd3a0080 100644
--- a/src/sat/sat_solver/sat_smt_solver.cpp
+++ b/src/sat/sat_solver/sat_smt_solver.cpp
@@ -63,7 +63,7 @@ class sat_smt_solver : public solver {
std::ostream& display(std::ostream& out) const override {
unsigned i = 0;
for (auto const& d : s.m_fmls) {
- if (i == qhead())
+ if (i > 0 && i == qhead())
out << "---- head ---\n";
out << d << "\n";
++i;