From: Andrew Reynolds Date: Wed, 12 Jan 2022 15:58:14 +0000 (-0600) Subject: Eliminate use of subtyping from results of quantifier elimination (#7885) X-Git-Tag: cvc5-1.0.0~561 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=141c8f592c31422cc07b0d8965750db235195251;p=cvc5.git 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 e00e938e0..b65909403 100644 --- 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 index 000000000..fd888a0f2 --- /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 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 index 000000000..f0a84c86e --- /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 +#include + +#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 919368512..1b84e0c74 100644 --- 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 9183d24e7..96c34638f 100644 --- 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 index 000000000..081ee4376 --- /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)) +))