From 20b0feaf3f9858a1414f5d1eef9819913aae3ded Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 22 Feb 2021 17:58:47 +0100 Subject: [PATCH] (proof-new) Add new arithmetic kind INDEXED_ROOT_PREDICATE. (#5949) This PR introduces a new arithmetic kind for indexed root predicates. An indexed root predicate compares a real variable to the k'th root of a given polynomial as follows: Let IRP_k(x ~ 0, p) an indexed root predicate with k a non-negative number, x some real variable, ~ an arithmetic relation (e.g. =, <, ...), and p a polynomial over x (and possibly other variables). If p contains variables apart from x, we can only evaluate the expression over a suitable assignment for at least these variables. The evaluation of this expression is equivalent to computing the k'th real root of p in x (with all other variables evaluated over a given assignment) and comparing this real root to zero (according to the relation symbol ~). Note that we currently do not intend to use this structure for solving, but require it for representing and printing CAD proofs. --- src/printer/smt2/smt2_printer.cpp | 6 ++ src/theory/arith/kinds | 23 +++++-- src/theory/arith/theory_arith_type_rules.h | 26 ++++++++ src/util/indexed_root_predicate.h | 74 ++++++++++++++++++++++ 4 files changed, 123 insertions(+), 6 deletions(-) create mode 100644 src/util/indexed_root_predicate.h diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ccf9c4164..bc4ea16de 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -665,6 +665,12 @@ void Smt2Printer::toStream(std::ostream& out, out << "(_ divisible " << n.getOperator().getConst().k << ")"; stillNeedToPrintParams = false; break; + case kind::INDEXED_ROOT_PREDICATE_OP: + { + const IndexedRootPredicate& irp = n.getConst(); + out << "(_ root_predicate " << irp.d_index << ")"; + break; + } // arrays theory case kind::SELECT: diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index fc8f76ee4..04bdc277e 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -80,9 +80,17 @@ operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" -operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" -operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)" -operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)" +# represents an indexed root predicate. See util/indexed_root_predicate.h for more documentation. +constant INDEXED_ROOT_PREDICATE_OP \ + ::CVC4::IndexedRootPredicate \ + ::CVC4::IndexedRootPredicateHashFunction \ + "util/indexed_root_predicate.h" \ + "operator for the indexed root predicate; payload is an instance of the CVC4::IndexedRootPredicate class" +parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root predicate; first parameter is a INDEXED_ROOT_PREDICATE_OP, second is a real variable compared to zero, third is a polynomial" + +operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)" +operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)" +operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)" # CAST_TO_REAL is added to distinguish between integers casted to reals internally, and # integers casted to reals or using the API \ @@ -106,10 +114,13 @@ typerule LEQ "SimpleTypeRule" typerule GT "SimpleTypeRule" typerule GEQ "SimpleTypeRule" -typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule +typerule INDEXED_ROOT_PREDICATE_OP "SimpleTypeRule" +typerule INDEXED_ROOT_PREDICATE ::CVC4::theory::arith::IndexedRootPredicateTypeRule + +typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule typerule CAST_TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule -typerule IS_INTEGER "SimpleTypeRule" +typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule +typerule IS_INTEGER "SimpleTypeRule" typerule ABS "SimpleTypeRule" typerule INTS_DIVISION "SimpleTypeRule" diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 0aa9cd4b3..0fed2dafd 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -131,6 +131,32 @@ class IAndTypeRule } }; /* class BitVectorConversionTypeRule */ +class IndexedRootPredicateTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + if (check) + { + TypeNode t1 = n[0].getType(check); + if (!t1.isBoolean()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting boolean term as first argument"); + } + TypeNode t2 = n[1].getType(check); + if (!t2.isReal()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting polynomial as second argument"); + } + } + return nodeManager->booleanType(); + } +}; /* class IndexedRootPredicateTypeRule */ + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/util/indexed_root_predicate.h b/src/util/indexed_root_predicate.h new file mode 100644 index 000000000..2b7e36b52 --- /dev/null +++ b/src/util/indexed_root_predicate.h @@ -0,0 +1,74 @@ +/********************* */ +/*! \file indexed_root_predicate.h + ** \verbatim + ** Top contributors (to current version): + ** Gereon Kremer + ** 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 Utils for indexed root predicates. + ** + ** Some utils for indexed root predicates. + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__UTIL__INDEXED_ROOT_PREDICATE_H +#define CVC4__UTIL__INDEXED_ROOT_PREDICATE_H + +namespace CVC4 { + +/** + * The structure representing the index of a root predicate. + * An indexed root predicate has the form + * IRP_k(x ~ 0, p) + * where k is a positive integer (d_index), x is a real variable, + * ~ an arithmetic relation symbol and p a (possibly multivariate polynomial). + * The evaluation of the predicate is obtained by comparing the k'th root of p + * (as polynomial in x) to the value of x according to the relation symbol ~. + * Note that p may be multivariate: in this case we can only evaluate with + * respect to a (partial) variable assignment, that (at least) contains values + * for all variables from p except x. + * + * Some examples: + * IRP_1(x > 0, x) <=> x > 0 + * IRP_1(x < 0, x*x-1) <=> x < -1 + * IRP_2(x < 0, x*x-1) <=> x < 1 + * IRP_1(x = 0, x*x-2) <=> x = -sqrt(2) + * IRP_1(x = 0, x*x-y), y=3 <=> x = -sqrt(3) + */ +struct CVC4_PUBLIC IndexedRootPredicate +{ + /** The index of the root */ + std::uint64_t d_index; + + IndexedRootPredicate(unsigned index) : d_index(index) {} + + bool operator==(const IndexedRootPredicate& irp) const + { + return d_index == irp.d_index; + } +}; /* struct IndexedRootPredicate */ + +inline std::ostream& operator<<(std::ostream& os, + const IndexedRootPredicate& irp) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& os, + const IndexedRootPredicate& irp) +{ + return os << "k=" << irp.d_index; +} + +struct CVC4_PUBLIC IndexedRootPredicateHashFunction +{ + std::size_t operator()(const IndexedRootPredicate& irp) const + { + return irp.d_index; + } +}; /* struct IndexedRootPredicateHashFunction */ + +} // namespace CVC4 + +#endif \ No newline at end of file -- 2.30.2