From 51b9c07af2001e961911e59f3e7e80728c88550a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Oct 2020 16:15:16 -0500
Subject: (proof-new) Fixes for theory preprocessing proofs (#5171)

This fixes several subtle issues with theory preprocessing.

The main fix is to ensure proofs are correct for cases where the theory preprocessor applies either with or without theory preprocessing (calling Theory::ppRewrite on subterms) enabled, see argument doTheoryPreprocess of preprocess. If disabled, it applies term formula removal and rewriting only. This is required for processing lemmas that are marked as "do not preprocess", which is an optimization, but is also necessary since theory combination may e.g. split on equality that was solved during ppRewrite. The solution is to use 2 separate term conversion sequences for these 2 cases.

It also fixes an issue where preprocessing is term-context-sensitive: terms underneath quantifiers are treated differently. This is now handled by a new TermContext callback "InQuantTermContext".
---
 src/expr/term_context.cpp | 16 ++++++++++++++++
 src/expr/term_context.h   | 18 ++++++++++++++++++
 2 files changed, 34 insertions(+)

(limited to 'src/expr')

diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
index 6974e2114..67da6d842 100644
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -69,6 +69,22 @@ bool RtfTermContext::hasNestedTermChildren(TNode t)
          && k != kind::BITVECTOR_EAGER_ATOM;
 }
 
+uint32_t InQuantTermContext::initialValue() const { return 0; }
+
+uint32_t InQuantTermContext::computeValue(TNode t,
+                                          uint32_t tval,
+                                          size_t index) const
+{
+  return t.isClosure() ? 1 : tval;
+}
+
+uint32_t InQuantTermContext::getValue(bool inQuant) { return inQuant ? 1 : 0; }
+
+bool InQuantTermContext::inQuant(uint32_t val, bool& inQuant)
+{
+  return val == 1;
+}
+
 uint32_t PolarityTermContext::initialValue() const
 {
   // by default, we have true polarity
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index ec7b488f9..b0ce03e48 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -92,6 +92,24 @@ class RtfTermContext : public TermContext
   static bool hasNestedTermChildren(TNode t);
 };
 
+/**
+ * Simpler version of above that only computes whether we are inside a
+ * quantifier.
+ */
+class InQuantTermContext : public TermContext
+{
+ public:
+  InQuantTermContext() {}
+  /** The initial value: not beneath a quantifier. */
+  uint32_t initialValue() const override;
+  /** Compute the value of the index^th child of t whose hash is tval */
+  uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
+  /** get hash value from the flags */
+  static uint32_t getValue(bool inQuant);
+  /** get flags from the hash value */
+  static bool inQuant(uint32_t val, bool& inQuant);
+};
+
 /**
  * Polarity term context.
  *
-- 
cgit v1.2.3