GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/bound_inference.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 10 30 33.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bound_inference.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 Extract bounds on variables from theory atoms.
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__BOUND_INFERENCE_H
16
#define CVC4__THEORY__ARITH__BOUND_INFERENCE_H
17
18
#include <map>
19
#include <utility>
20
#include <vector>
21
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace arith {
27
28
537216
  struct Bounds
29
  {
30
    /** The lower bound value */
31
    Node lower_value;
32
    /** Whether the lower bound is strict or weak */
33
    bool lower_strict = true;
34
    /** The lower bound as constraint */
35
    Node lower_bound;
36
    /** The origin of the lower bound */
37
    Node lower_origin;
38
    /** The upper bound value */
39
    Node upper_value;
40
    /** Whether the upper bound is strict or weak */
41
    bool upper_strict = true;
42
    /** The upper bound as constraint */
43
    Node upper_bound;
44
    /** The origin of the upper bound */
45
    Node upper_origin;
46
  };
47
48
  /** Print the current bounds. */
49
  std::ostream& operator<<(std::ostream& os, const Bounds& b);
50
51
  /**
52
   * A utility class that extracts direct bounds on arithmetic terms from theory
53
   * atoms.
54
   */
55
5852
  class BoundInference
56
  {
57
   public:
58
    void reset();
59
60
    /**
61
     * Get the current interval for lhs. Creates a new (full) interval if
62
     * necessary.
63
     */
64
    Bounds& get_or_add(const Node& lhs);
65
    /**
66
     * Get the current interval for lhs. Returns a full interval if no interval
67
     * was derived yet.
68
     */
69
    Bounds get(const Node& lhs) const;
70
71
    /** Return the current term bounds as an interval assignment. */
72
    const std::map<Node, Bounds>& get() const;
73
74
    /**
75
     * Add a new theory atom. Return true if the theory atom induces a new
76
     * term bound.
77
     * If onlyVariables is true, the left hand side needs to be a single
78
     * variable to induce a bound.
79
     */
80
    bool add(const Node& n, bool onlyVariables = true);
81
82
    /**
83
     * Post-processes a set of nodes and replaces bounds by their origins.
84
     * This utility sometimes creates new bounds, either due to tightening of
85
     * integer terms or because an equality was derived from two weak
86
     * inequalities. While the origins of these new bounds are recorded in
87
     * lower_origin and upper_origin, this method can be used to conveniently
88
     * replace these new nodes by their origins.
89
     * This can be used, for example, when constructing conflicts.
90
     */
91
    void replaceByOrigins(std::vector<Node>& nodes) const;
92
93
   private:
94
    /** The currently strictest bounds for every lhs. */
95
    std::map<Node, Bounds> d_bounds;
96
97
    /** Updates the lower bound for the given lhs */
98
    void update_lower_bound(const Node& origin,
99
                            const Node& lhs,
100
                            const Node& value,
101
                            bool strict);
102
    /** Updates the upper bound for the given lhs */
103
    void update_upper_bound(const Node& origin,
104
                            const Node& lhs,
105
                            const Node& value,
106
                            bool strict);
107
  };
108
109
/** Print the current variable bounds. */
110
std::ostream& operator<<(std::ostream& os, const BoundInference& bi);
111
112
std::map<Node, std::pair<Node,Node>> getBounds(const std::vector<Node>& assertions);
113
114
}  // namespace arith
115
}  // namespace theory
116
}  // namespace CVC4
117
118
#endif