From: Gereon Kremer <gkremer@stanford.edu>
Date: Tue, 1 Feb 2022 19:16:24 +0000 (-0800)
Subject: Add new ordering utility (#8008)
X-Git-Tag: cvc5-1.0.0~485
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7705df3f4df10c0e26bdda3f119c74801ec275d;p=cvc5.git

Add new ordering utility (#8008)

This PR provides a clean implementation of the comparators from the normal form utility, also supporting real algebraic numbers. They will be used within the refactored arithmetic rewriter.
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1715257f7..71fe64dfa 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -498,6 +498,7 @@ libcvc5_add_sources(
   theory/arith/pp_rewrite_eq.h
   theory/arith/proof_checker.cpp
   theory/arith/proof_checker.h
+  theory/arith/rewriter/ordering.h
   theory/arith/rewrites.cpp
   theory/arith/rewrites.h
   theory/arith/simplex.cpp
diff --git a/src/theory/arith/rewriter/ordering.h b/src/theory/arith/rewriter/ordering.h
new file mode 100644
index 000000000..529bd14ca
--- /dev/null
+++ b/src/theory/arith/rewriter/ordering.h
@@ -0,0 +1,112 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Comparator utilities for the arithmetic rewriter.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__ARITH__REWRITER__ORDERING_H
+#define CVC5__THEORY__ARITH__REWRITER__ORDERING_H
+
+#include "base/check.h"
+#include "expr/node.h"
+
+namespace cvc5::theory::arith::rewriter {
+
+/**
+ * Implements an ordering on arithmetic leaf nodes. We expect that values have
+ * already been combined, i.e., there shall only be a single rational and a
+ * single real algebraic number. It broadly categorizes leaf nodes into
+ * rationals, real algebraic numbers, integers, variables, and the rest.
+ * The ordering is built as follows:
+ * - rationals come first
+ * - real algebraic numbers come second
+ * - real terms come before integer terms
+ * - variables come before non-variable terms
+ * - finally, fall back to node ordering
+ */
+struct LeafNodeComparator
+{
+  /** Implements operator<(a, b) as described above */
+  bool operator()(TNode a, TNode b) const
+  {
+    if (a == b) return false;
+
+    bool aIsConst = a.isConst();
+    bool bIsConst = b.isConst();
+    if (aIsConst != bIsConst) return aIsConst;
+    Assert(!aIsConst && !bIsConst) << "Rationals should be combined";
+
+    bool aIsRAN = a.getKind() == Kind::REAL_ALGEBRAIC_NUMBER;
+    bool bIsRAN = b.getKind() == Kind::REAL_ALGEBRAIC_NUMBER;
+    if (aIsRAN != bIsRAN) return aIsRAN;
+    Assert(!aIsRAN && !bIsRAN) << "real algebraic numbers should be combined";
+
+    bool aIsInt = a.getType().isInteger();
+    bool bIsInt = b.getType().isInteger();
+    if (aIsInt != bIsInt) return !aIsInt;
+
+    bool aIsVar = a.isVar();
+    bool bIsVar = b.isVar();
+    if (aIsVar != bIsVar) return aIsVar;
+
+    return a < b;
+  }
+};
+
+/**
+ * Implements an ordering on arithmetic terms or summands. We expect these terms
+ * to be products (MULT or NONLINEAR_MULT), though products of zero or one node
+ * are not actually represented as such. For individual factors of the product,
+ * we rely on the ordering from LeafNodeComparator. Furthermore, we expect the
+ * individual factors to be sorted according to LeafNodeComparator. The ordering
+ * is built as follows:
+ * - single factors come first (everything that is MULT or NONLINEAR_MULT)
+ * - multiplications with less factors come first
+ * - multiplications are compared lexicographically
+ */
+struct TermComparator
+{
+  /** Implements operator<(a, b) as described above */
+  bool operator()(TNode a, TNode b) const
+  {
+    if (a == b) return false;
+
+    bool aIsMult = a.getKind() == Kind::MULT || a.getKind() == Kind::NONLINEAR_MULT;
+    bool bIsMult = b.getKind() == Kind::MULT || b.getKind() == Kind::NONLINEAR_MULT;
+    if (aIsMult != bIsMult) return !aIsMult;
+
+    if (!aIsMult)
+    {
+      return LeafNodeComparator()(a, b);
+    }
+
+    size_t aLen = a.getNumChildren();
+    size_t bLen = b.getNumChildren();
+    if (aLen != bLen) return aLen < bLen;
+
+    for (size_t i = 0; i < aLen; ++i)
+    {
+      if (a[i] != b[i])
+      {
+        return LeafNodeComparator()(a[i], b[i]);
+      }
+    }
+    Unreachable() << "Nodes are different, but have the same content";
+    return false;
+  }
+};
+
+}  // namespace cvc5::theory::arith::rewriter
+
+#endif