GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/indexed_root_predicate.h Lines: 0 6 0.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file indexed_root_predicate.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Utils for indexed root predicates.
13
 **
14
 ** Some utils for indexed root predicates.
15
 **/
16
17
#include "cvc4_public.h"
18
19
#ifndef CVC4__UTIL__INDEXED_ROOT_PREDICATE_H
20
#define CVC4__UTIL__INDEXED_ROOT_PREDICATE_H
21
22
namespace CVC4 {
23
24
/**
25
 * The structure representing the index of a root predicate.
26
 * An indexed root predicate has the form
27
 *   IRP_k(x ~ 0, p)
28
 * where k is a positive integer (d_index), x is a real variable,
29
 * ~ an arithmetic relation symbol and p a (possibly multivariate polynomial).
30
 * The evaluation of the predicate is obtained by comparing the k'th root of p
31
 * (as polynomial in x) to the value of x according to the relation symbol ~.
32
 * Note that p may be multivariate: in this case we can only evaluate with
33
 * respect to a (partial) variable assignment, that (at least) contains values
34
 * for all variables from p except x.
35
 *
36
 * Some examples:
37
 *  IRP_1(x > 0, x)  <=>  x > 0
38
 *  IRP_1(x < 0, x*x-1)  <=>  x < -1
39
 *  IRP_2(x < 0, x*x-1)  <=>  x < 1
40
 *  IRP_1(x = 0, x*x-2)  <=>  x = -sqrt(2)
41
 *  IRP_1(x = 0, x*x-y), y=3  <=>  x = -sqrt(3)
42
 */
43
struct IndexedRootPredicate
44
{
45
  /** The index of the root */
46
  std::uint64_t d_index;
47
48
  IndexedRootPredicate(unsigned index) : d_index(index) {}
49
50
  bool operator==(const IndexedRootPredicate& irp) const
51
  {
52
    return d_index == irp.d_index;
53
  }
54
}; /* struct IndexedRootPredicate */
55
56
inline std::ostream& operator<<(std::ostream& os,
57
                                const IndexedRootPredicate& irp);
58
inline std::ostream& operator<<(std::ostream& os,
59
                                const IndexedRootPredicate& irp)
60
{
61
  return os << "k=" << irp.d_index;
62
}
63
64
struct IndexedRootPredicateHashFunction
65
{
66
  std::size_t operator()(const IndexedRootPredicate& irp) const
67
  {
68
    return irp.d_index;
69
  }
70
}; /* struct IndexedRootPredicateHashFunction */
71
72
}  // namespace CVC4
73
74
#endif