GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/icp/contraction_origins.h Lines: 0 1 0.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file contraction_origins.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 Implements a way to track the origins of ICP-style contractions.
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
16
#define CVC4__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
17
18
#include <memory>
19
#include <vector>
20
21
#include "expr/node.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace arith {
26
namespace nl {
27
namespace icp {
28
29
/**
30
 * This class tracks origins of ICP-style contractions of variable intervals.
31
 * For every variable, it holds one origin object that may recursively depend on
32
 * previous contraction origins. Initially, a immediate bound on a variable
33
 * (like x>0) yields an origin for this variable. For every contraction, we then
34
 * add a new origin that recursively holds the old origins, usually those of all
35
 * variables involved in the contraction. When generating a conflict or a lemma,
36
 * a recursive walk through this structure allow to retrieve all input theory
37
 * atoms that contributed to the new fact or the conflict.
38
 */
39
class ContractionOriginManager
40
{
41
 public:
42
  /**
43
   * Origin of one particular contraction step.
44
   * Usually, this is either a direct bound or the application of a contraction
45
   * candidate. The direct bound is stored in the candidate while origins
46
   * remains empty. The contraction candidate is stored in the candidate while
47
   * origins hold the origins of all variables used in the contraction.
48
   */
49
  struct ContractionOrigin
50
  {
51
    /** The theory atom used to do this contraction. */
52
    Node candidate;
53
    /** All origins required for this contraction. */
54
    std::vector<ContractionOrigin*> origins;
55
  };
56
57
 private:
58
  /**
59
   * Recursively walks through the data structure, collecting all theory atoms.
60
   */
61
  void getOrigins(ContractionOrigin const* const origin,
62
                  std::set<Node>& res) const;
63
64
 public:
65
  /** Return the current origins for all variables. */
66
  const std::map<Node, ContractionOrigin*>& currentOrigins() const;
67
  /**
68
   * Add a new contraction for the targetVariable.
69
   * Adds a new origin with the given candidate and origins.
70
   * If addTarget is set to true, we also add the current origin of the
71
   * targetVariable to origins. This corresponds to whether we intersected the
72
   * new interval with the previous interval, or whether the new interval was a
73
   * subset of the previous one in the first place.
74
   */
75
  void add(const Node& targetVariable,
76
           const Node& candidate,
77
           const std::vector<Node>& originVariables,
78
           bool addTarget = true);
79
80
  /**
81
   * Collect all theory atoms from the origins of the given variable.
82
   */
83
  std::vector<Node> getOrigins(const Node& variable) const;
84
85
  /** Check whether a node c is among the origins of a variable. */
86
  bool isInOrigins(const Node& variable, const Node& c) const;
87
88
 private:
89
  /** The current origins for every variable. */
90
  std::map<Node, ContractionOrigin*> d_currentOrigins;
91
  /** All allocated origins to allow for proper deallocation. */
92
  std::vector<std::unique_ptr<ContractionOrigin>> d_allocations;
93
};
94
95
/** Stream the constration origins to an ostream. */
96
std::ostream& operator<<(std::ostream& os, const ContractionOriginManager& com);
97
98
}  // namespace icp
99
}  // namespace nl
100
}  // namespace arith
101
}  // namespace theory
102
}  // namespace CVC4
103
104
#endif