(proof-new) Callbacks for term-context-sensitive terms (#4842)

Callbacks for term-context-sensitive terms.

It gives two examples of such callbacks, "remove term formula (rtf) context" to be used in the remove term formulas pass and "polarity context" which is a highly common pattern in preprocessing.

These utilities will be critical for maintain proofs for term-context-sensitive rewrites. An example user of these utilities is TermFormulaRemoval, which rewrites terms depending on whether they occur beneath quantifiers/terms. This utility currently has bugs in its proof generation since its proof cache does not consider the term context. This PR updates that class to use this utility. Its proof generator will be similarly extended in proof-new to synchronize its cache, relative to term context identifiers. Concretely, a TermContext callback will be passed to TConvProofGenerator, which will put together proof skeletons in a term-context-sensitive manner.

3 files changed, 260 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 993df2594..0092b78c6 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -61,6 +61,8 @@ libcvc4_add_sources(
   symbol_table.h
   term_canonize.cpp
   term_canonize.h
+  term_context.cpp
+  term_context.h
   term_conversion_proof_generator.cpp
   term_conversion_proof_generator.h
   type.cpp
diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
new file mode 100644
index 000000000..6dcdc25ee
--- /dev/null
+++ b/src/expr/term_context.cpp
@@ -0,0 +1,113 @@
+/*********************                                                        */
+/*! \file term_context.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of term context utilities.
+ **/
+
+#include "expr/term_context.h"
+
+namespace CVC4 {
+
+uint32_t RtfTermContext::initialValue() const
+{
+  // by default, not in a term context or a quantifier
+  return 0;
+}
+
+uint32_t RtfTermContext::computeValue(TNode t,
+                                      uint32_t tval,
+                                      size_t child) const
+{
+  if (t.isClosure())
+  {
+    if (tval % 2 == 0)
+    {
+      return tval + 1;
+    }
+  }
+  else if (hasNestedTermChildren(t))
+  {
+    if (tval < 2)
+    {
+      return tval + 2;
+    }
+  }
+  return tval;
+}
+
+uint32_t RtfTermContext::getValue(bool inQuant, bool inTerm)
+{
+  return (inQuant ? 1 : 0) + 2 * (inTerm ? 1 : 0);
+}
+
+void RtfTermContext::getFlags(uint32_t val, bool& inQuant, bool& inTerm)
+{
+  inQuant = val % 2 == 1;
+  inTerm = val >= 2;
+}
+
+bool RtfTermContext::hasNestedTermChildren(TNode t)
+{
+  Kind k = t.getKind();
+  // dont' worry about FORALL or EXISTS, these are part of inQuant.
+  return theory::kindToTheoryId(k) != theory::THEORY_BOOL && k != kind::EQUAL
+         && k != kind::SEP_STAR && k != kind::SEP_WAND && k != kind::SEP_LABEL
+         && k != kind::BITVECTOR_EAGER_ATOM;
+}
+
+uint32_t PolarityTermContext::initialValue() const
+{
+  // by default, we have true polarity
+  return 2;
+}
+
+uint32_t PolarityTermContext::computeValue(TNode t,
+                                           uint32_t tval,
+                                           size_t index) const
+{
+  switch (t.getKind())
+  {
+    case kind::AND:
+    case kind::OR:
+    case kind::SEP_STAR:
+      // polarity preserved
+      return tval;
+    case kind::IMPLIES:
+      // first child reverses, otherwise we preserve
+      return index == 0 ? (tval == 0 ? 0 : (3 - tval)) : tval;
+    case kind::NOT:
+      // polarity reversed
+      return tval == 0 ? 0 : (3 - tval);
+    case kind::ITE:
+      // head has no polarity, branches preserve
+      return index == 0 ? 0 : tval;
+    case kind::FORALL:
+      // body preserves, others have no polarity.
+      return index == 1 ? tval : 0;
+    default:
+      // no polarity
+      break;
+  }
+  return 0;
+}
+
+uint32_t PolarityTermContext::getValue(bool hasPol, bool pol)
+{
+  return hasPol ? (pol ? 2 : 1) : 0;
+}
+
+void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol)
+{
+  hasPol = val == 0;
+  pol = val == 2;
+}
+
+}  // namespace CVC4
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
new file mode 100644
index 000000000..87f91f2df
--- /dev/null
+++ b/src/expr/term_context.h
@@ -0,0 +1,145 @@
+/*********************                                                        */
+/*! \file term_context.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Term context utilities.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__TERM_CONTEXT_H
+#define CVC4__EXPR__TERM_CONTEXT_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+
+/**
+ * This is an abstract class for computing "term context identifiers". A term
+ * context identifier is a hash value that identifies some property of the
+ * context in which a term occurs. Common examples of the implementation of
+ * such a mapping are implemented in the subclasses below.
+ *
+ * A term context identifier is intended to be information that can be locally
+ * computed from the parent's hash, and hence does not rely on maintaining
+ * paths.
+ *
+ * In the below documentation, we write t @ [p] to a term at a given position,
+ * where p is a list of indices. For example, the atomic subterms of:
+ *   (and P (not Q))
+ * are P @ [0] and Q @ [1,0].
+ */
+class TermContext
+{
+ public:
+  TermContext() {}
+  virtual ~TermContext() {}
+  /** The default initial value of root terms. */
+  virtual uint32_t initialValue() const = 0;
+  /**
+   * Returns the term context identifier of the index^th child of t, where tval
+   * is the term context identifier of t.
+   */
+  virtual uint32_t computeValue(TNode t, uint32_t tval, size_t index) const = 0;
+};
+
+/**
+ * Remove term formulas (rtf) term context.
+ *
+ * Computes whether we are inside a term (as opposed to being part of Boolean
+ * skeleton) and whether we are inside a quantifier. For example, for:
+ *   (and (= a b) (forall ((x Int)) (P x)))
+ * we have the following mappings (term -> inTerm,inQuant)
+ *   (= a b) @ [0] -> false, false
+ *   a @ [0,1] -> true, false
+ *   (P x) @ [1,1] -> false, true
+ *    x @ [1,1,0] -> true, true
+ * Notice that the hash of a child can be computed from the parent's hash only,
+ * and hence this can be implemented as an instance of the abstract class.
+ */
+class RtfTermContext : public TermContext
+{
+ public:
+  RtfTermContext() {}
+  /** The initial value: not in a term context or 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, bool inTerm);
+  /** get flags from the hash value */
+  static void getFlags(uint32_t val, bool& inQuant, bool& inTerm);
+
+ private:
+  /**
+   * Returns true if the children of t should be considered in a "term" context,
+   * which is any context beneath a symbol that does not belong to the Boolean
+   * theory as well as other exceptions like equality, separation logic
+   * connectives and bit-vector eager atoms.
+   */
+  static bool hasNestedTermChildren(TNode t);
+};
+
+/**
+ * Polarity term context.
+ *
+ * This class computes the polarity of a term-context-sensitive term, which is
+ * one of {true, false, none}. This corresponds to the value that can be
+ * assigned to that term while preservering satisfiability of the overall
+ * formula, or none if such a value does not exist. If not "none", this
+ * typically corresponds to whether the number of NOT the formula is beneath is
+ * even, although special cases exist (e.g. the first child of IMPLIES).
+ *
+ * For example, given the formula:
+ *   (and P (not (= (f x) 0)))
+ * assuming the root of this formula has true polarity, we have that:
+ *   P @ [0] -> true
+ *   (not (= (f x) 0)) @ [1] -> true
+ *   (= (f x) 0) @ [1,0] -> false
+ *   (f x) @ [1,0,0]), x @ [1,0,0,0]), 0 @ [1,0,1] -> none
+ *
+ * Notice that a term-context-sensitive Node is not one-to-one with Node.
+ * In particular, given the formula:
+ *   (and P (not P))
+ * We have that the P at path [0] has polarity true and the P at path [1,0] has
+ * polarity false.
+ *
+ * Finally, notice that polarity does not correspond to a value that the
+ * formula entails. Thus, for the formula:
+ *   (or P Q)
+ * we have that
+ *   P @ [0] -> true
+ *   Q @ [1] -> true
+ * although neither is entailed.
+ *
+ * Notice that the hash of a child can be computed from the parent's hash only.
+ */
+class PolarityTermContext : public TermContext
+{
+ public:
+  PolarityTermContext() {}
+  /** The initial value: true polarity. */
+  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, where hasPol false means no polarity.
+   */
+  static uint32_t getValue(bool hasPol, bool pol);
+  /**
+   * get flags from the hash value. If we have no polarity, both hasPol and pol
+   * are set to false.
+   */
+  static void getFlags(uint32_t val, bool& hasPol, bool& pol);
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */