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.
out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")";
stillNeedToPrintParams = false;
break;
+ case kind::INDEXED_ROOT_PREDICATE_OP:
+ {
+ const IndexedRootPredicate& irp = n.getConst<IndexedRootPredicate>();
+ out << "(_ root_predicate " << irp.d_index << ")";
+ break;
+ }
// arrays theory
case kind::SELECT:
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 \
typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
-typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule INDEXED_ROOT_PREDICATE_OP "SimpleTypeRule<RBuiltinOperator>"
+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<RBool, AReal>"
+typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
typerule ABS "SimpleTypeRule<RInteger, AInteger>"
typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"
}
}; /* 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 */
--- /dev/null
+/********************* */
+/*! \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
projects / cvc5.git / commitdiff