1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
/******************************************************************************
* Top contributors (to current version):
* Gereon Kremer, Mathias Preiner
*
* 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.
* ****************************************************************************
*
* Utils for indexed root predicates.
*/
#include "cvc5_public.h"
#ifndef CVC5__UTIL__INDEXED_ROOT_PREDICATE_H
#define CVC5__UTIL__INDEXED_ROOT_PREDICATE_H
namespace cvc5 {
/**
* 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 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);
inline std::ostream& operator<<(std::ostream& os,
const IndexedRootPredicate& irp)
{
return os << "k=" << irp.d_index;
}
struct IndexedRootPredicateHashFunction
{
std::size_t operator()(const IndexedRootPredicate& irp) const
{
return irp.d_index;
}
}; /* struct IndexedRootPredicateHashFunction */
} // namespace cvc5
#endif
|
