--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff