Eliminate use of subtyping from results of quantifier elimination (#7885)

Fixes #7870.

Notice this node converter is potentially unnecessary if we ever get rid of arithmetic subtyping.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index e00e938e038bfc8ba03fb62bc629e00ab10b1876..b65909403eb7d75e7407dd56409dfb8e60c75a4c 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -60,6 +60,8 @@ libcvc5_add_sources(
   node_visitor.h
   skolem_manager.cpp
   skolem_manager.h
+  subtype_elim_node_converter.cpp
+  subtype_elim_node_converter.h
   symbol_manager.cpp
   symbol_manager.h
   symbol_table.cpp

diff --git a/src/expr/subtype_elim_node_converter.cpp b/src/expr/subtype_elim_node_converter.cpp
new file mode 100644 (file)
index 0000000..fd888a0
--- /dev/null
+++ b/src/expr/subtype_elim_node_converter.cpp
@@ -0,0 +1,65 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of subtype elimination node conversion
+ */
+
+#include "expr/subtype_elim_node_converter.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+
+SubtypeElimNodeConverter::SubtypeElimNodeConverter() {}
+
+bool SubtypeElimNodeConverter::isRealTypeStrict(TypeNode tn)
+{
+  return tn.isReal() && !tn.isInteger();
+}
+
+Node SubtypeElimNodeConverter::postConvert(Node n)
+{
+  Kind k = n.getKind();
+  bool convertToRealChildren = false;
+  if (k == PLUS || k == MULT || k == NONLINEAR_MULT)
+  {
+    convertToRealChildren = isRealTypeStrict(n.getType());
+  }
+  else if (k == EQUAL || k == GEQ)
+  {
+    convertToRealChildren =
+        isRealTypeStrict(n[0].getType()) || isRealTypeStrict(n[1].getType());
+  }
+  if (convertToRealChildren)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    std::vector<Node> children;
+    for (const Node& nc : n)
+    {
+      if (nc.getType().isInteger())
+      {
+        // we use CAST_TO_REAL for constants, so that e.g. 5 is printed as
+        // 5.0 not (to_real 5)
+        Kind nk = nc.isConst() ? CAST_TO_REAL : TO_REAL;
+        children.push_back(nm->mkNode(nk, nc));
+      }
+      else
+      {
+        children.push_back(nc);
+      }
+    }
+    return nm->mkNode(k, children);
+  }
+  return n;
+}
+
+}  // namespace cvc5

diff --git a/src/expr/subtype_elim_node_converter.h b/src/expr/subtype_elim_node_converter.h
new file mode 100644 (file)
index 0000000..f0a84c8
--- /dev/null
+++ b/src/expr/subtype_elim_node_converter.h
@@ -0,0 +1,48 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of subtype elimination node conversion
+ */
+#include "cvc5_private.h"
+
+#ifndef CVC4__PROOF__EXPR__SUBTYPE_ELIM_NODE_CONVERTER_H
+#define CVC4__PROOF__EXPR__SUBTYPE_ELIM_NODE_CONVERTER_H
+
+#include <iostream>
+#include <map>
+
+#include "expr/node.h"
+#include "expr/node_converter.h"
+#include "expr/type_node.h"
+
+namespace cvc5 {
+
+/**
+ * This converts a node into one that does not involve (arithmetic) subtyping.
+ * In particular, all applications of arithmetic symbols that involve at least
+ * one (strict) Real child are such that all children are cast to real.
+ */
+class SubtypeElimNodeConverter : public NodeConverter
+{
+ public:
+  SubtypeElimNodeConverter();
+  ~SubtypeElimNodeConverter() {}
+  /** convert node n as described above during post-order traversal */
+  Node postConvert(Node n) override;
+ private:
+  /** Is real type (not integer)? */
+  static bool isRealTypeStrict(TypeNode tn);
+};
+
+}  // namespace cvc5
+
+#endif

diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 9193685124a477c3f32dcf976443cbbead2c432d..1b84e0c74594e428bcf2024b34da042a2a0c4220 100644 (file)
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 #include "util/string.h"
+#include "expr/subtype_elim_node_converter.h"
 
 using namespace cvc5::theory;
 using namespace cvc5::kind;
@@ -132,6 +133,9 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     {
       ret = SkolemManager::getOriginalForm(ret);
     }
+    // make so that the returned formula does not involve arithmetic subtyping
+    SubtypeElimNodeConverter senc;
+    ret = senc.convert(ret);
     return ret;
   }
   // otherwise, just true/false

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9183d24e723437406127104b75949815070282aa..96c34638f79854ab31c29fac52edb1672e4d1b48 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2093,8 +2093,9 @@ set(regress_1_tests
   regress1/quantifiers/qbv-test-urem-rewrite.smt2
   regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2
   regress1/quantifiers/qcft-smtlib3dbc51.smt2
-  regress1/quantifiers/qe-partial.smt2
   regress1/quantifiers/qe.smt2
+  regress1/quantifiers/qe-partial.smt2
+  regress1/quantifiers/qe-subtypes.smt2
   regress1/quantifiers/qid.smt2
   regress1/quantifiers/qid-debug-inst.smt2
   regress1/quantifiers/quant-wf-int-ind.smt2

diff --git a/test/regress/regress1/quantifiers/qe-subtypes.smt2 b/test/regress/regress1/quantifiers/qe-subtypes.smt2
new file mode 100644 (file)
index 0000000..081ee43
--- /dev/null
+++ b/test/regress/regress1/quantifiers/qe-subtypes.smt2
@@ -0,0 +1,6 @@
+; EXPECT: (>= (* (- 1.0) x) (- 100.0))
+(set-logic LRA)  
+(declare-fun x () Real)
+(get-qe
+ (exists ((Y Bool)) (>= (* (- 1.0) x) (- 100.0))
+))