Class to reduce printing of redundant candidate rewrites (#1588)

1 files changed, 114 insertions, 0 deletions

diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
new file mode 100644
index 000000000..be2ff4c78
--- /dev/null
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -0,0 +1,114 @@
+/*********************                                                        */
+/*! \file dynamic_rewriter.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 dynamic_rewriter
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#define __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+
+#include <map>
+
+#include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** DynamicRewriter
+ *
+ * This class is given a stream of equalities in calls to addRewrite(...).
+ * The goal is to show that a subset of these can be inferred from previously
+ * asserted equalities.  For example, a possible set of return values for
+ * add rewrite on successive calls is the following:
+ *
+ *   addRewrite( x, y ) ---> true
+ *   addRewrite( f( x ), f( y ) ) ---> false, since we already know x=y
+ *   addRewrite( x, z ) ---> true
+ *   addRewrite( x+y, x+z ) ---> false, since we already know y=x=z.
+ *
+ * This class can be used to filter out redundant candidate rewrite rules
+ * when using the option sygusRewSynth().
+ *
+ * Currently, this class infers that an equality is redundant using
+ * an instance of the equality engine that does congruence over all
+ * operators by mapping all operators to uninterpreted ones and doing
+ * congruence on APPLY_UF.
+ *
+ * TODO (#1591): Add more advanced technique, e.g. by theory rewriting
+ * to show when terms can already be inferred equal.
+ */
+class DynamicRewriter
+{
+ public:
+  DynamicRewriter(const std::string& name, QuantifiersEngine* qe);
+  ~DynamicRewriter() {}
+  /** inform this class that the equality a = b holds.
+   *
+   * This function returns true if this class did not already know that
+   * a = b based on the previous equalities it has seen.
+   */
+  bool addRewrite(Node a, Node b);
+
+ private:
+  /** pointer to the quantifiers engine */
+  QuantifiersEngine* d_qe;
+  /** index over argument types to function skolems
+   *
+   * The purpose of this trie is to associate a class of interpreted operator
+   * with uninterpreted symbols. It is necessary to introduce multiple
+   * uninterpreted symbols per interpreted operator since they may be
+   * polymorphic. For example, for array select, its associate trie may look
+   * like this:
+   *   d_children[array_type_1]
+   *     d_children[index_type_1] : k1
+   *     d_children[index_type_2] : k2
+   *   d_children[array_type_2]
+   *     d_children[index_type_1] : k3
+   */
+  class OpInternalSymTrie
+  {
+   public:
+    /**
+     * Get the uninterpreted function corresponding to the top-most symbol
+     * of the internal representation of term n. This will return a skolem
+     * of the same type as n.getOperator() if it has one, or of the same type
+     * as n itself otherwise.
+     */
+    Node getSymbol(Node n);
+
+   private:
+    /** the symbol at this node in the trie */
+    Node d_sym;
+    /** the children of this node in the trie */
+    std::map<TypeNode, OpInternalSymTrie> d_children;
+  };
+  /** the internal operator symbol trie for this class */
+  std::map<Node, OpInternalSymTrie> d_ois_trie;
+  /**
+   * Convert node a to its internal representation, which replaces all
+   * interpreted operators in a by a unique uninterpreted symbol.
+   */
+  Node toInternal(Node a);
+  /** cache of the above function */
+  std::map<Node, Node> d_term_to_internal;
+  /** stores congruence closure over terms given to this class. */
+  eq::EqualityEngine d_equalityEngine;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */