GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/monomial_check.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file monomial_check.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer, Tim King
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 Check for some monomial lemmas
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
16
#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
17
18
#include "expr/node.h"
19
#include "theory/arith/nl/ext/monomial.h"
20
#include "theory/theory_inference.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
namespace nl {
26
27
struct ExtState;
28
29
4386
class MonomialCheck
30
{
31
 public:
32
  MonomialCheck(ExtState* data);
33
34
  void init(const std::vector<Node>& xts);
35
36
  /** check monomial sign
37
   *
38
   * Returns a set of valid theory lemmas, based on a
39
   * lemma schema which ensures that non-linear monomials
40
   * respect sign information based on their facts.
41
   * For more details, see Section 5 of "Design Theory
42
   * Solvers with Extensions" by Reynolds et al., FroCoS 2017,
43
   * Figure 5, this is the schema "Sign".
44
   *
45
   * Examples:
46
   *
47
   * x > 0 ^ y > 0 => x*y > 0
48
   * x < 0 => x*y*y < 0
49
   * x = 0 => x*y*z = 0
50
   */
51
  void checkSign();
52
53
  /** check monomial magnitude
54
   *
55
   * Returns a set of valid theory lemmas, based on a
56
   * lemma schema which ensures that comparisons between
57
   * non-linear monomials respect the magnitude of their
58
   * factors.
59
   * For more details, see Section 5 of "Design Theory
60
   * Solvers with Extensions" by Reynolds et al., FroCoS 2017,
61
   * Figure 5, this is the schema "Magnitude".
62
   *
63
   * Examples:
64
   *
65
   * |x|>|y| => |x*z|>|y*z|
66
   * |x|>|y| ^ |z|>|w| ^ |x|>=1 => |x*x*z*u|>|y*w|
67
   *
68
   * Argument c indicates the class of inferences to perform for the
69
   * (non-linear) monomials in the vector d_ms. 0 : compare non-linear monomials
70
   * against 1, 1 : compare non-linear monomials against variables, 2 : compare
71
   * non-linear monomials against other non-linear monomials.
72
   */
73
  void checkMagnitude(unsigned c);
74
75
 private:
76
  /** In the following functions, status states a relationship
77
   * between two arithmetic terms, where:
78
   * 0 : equal
79
   * 1 : greater than or equal
80
   * 2 : greater than
81
   * -X : (greater -> less)
82
   * TODO (#1287) make this an enum?
83
   */
84
  /** compute the sign of a.
85
   *
86
   * Calls to this function are such that :
87
   *    exp => ( oa = a ^ a <status> 0 )
88
   *
89
   * This function iterates over the factors of a,
90
   * where a_index is the index of the factor in a
91
   * we are currently looking at.
92
   *
93
   * This function returns a status, which indicates
94
   * a's relationship to 0.
95
   * We add lemmas to lem of the form given by the
96
   * lemma schema checkSign(...).
97
   */
98
  int compareSign(
99
      Node oa, Node a, unsigned a_index, int status, std::vector<Node>& exp);
100
  /** compare monomials a and b
101
   *
102
   * Initially, a call to this function is such that :
103
   *    exp => ( oa = a ^ ob = b )
104
   *
105
   * This function returns true if we can infer a valid
106
   * arithmetic lemma of the form :
107
   *    P => abs( a ) >= abs( b )
108
   * where P is true and abs( a ) >= abs( b ) is false in the
109
   * current model.
110
   *
111
   * This function is implemented by "processing" factors
112
   * of monomials a and b until an inference of the above
113
   * form can be made. For example, if :
114
   *   a = x*x*y and b = z*w
115
   * Assuming we are trying to show abs( a ) >= abs( c ),
116
   * then if abs( M( x ) ) >= abs( M( z ) ) where M is the current model,
117
   * then we can add abs( x ) >= abs( z ) to our explanation, and
118
   * mark one factor of x as processed in a, and
119
   * one factor of z as processed in b. The number of processed factors of a
120
   * and b are stored in a_exp_proc and b_exp_proc respectively.
121
   *
122
   * cmp_infers stores information that is helpful
123
   * in discarding redundant inferences.  For example,
124
   * we do not want to infer abs( x ) >= abs( z ) if
125
   * we have already inferred abs( x ) >= abs( y ) and
126
   * abs( y ) >= abs( z ).
127
   * It stores entries of the form (status,t1,t2)->F,
128
   * which indicates that we constructed a lemma F that
129
   * showed t1 <status> t2.
130
   *
131
   * We add lemmas to lem of the form given by the
132
   * lemma schema checkMagnitude(...).
133
   */
134
  bool compareMonomial(
135
      Node oa,
136
      Node a,
137
      NodeMultiset& a_exp_proc,
138
      Node ob,
139
      Node b,
140
      NodeMultiset& b_exp_proc,
141
      std::vector<Node>& exp,
142
      std::vector<SimpleTheoryLemma>& lem,
143
      std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
144
  /** helper function for above
145
   *
146
   * The difference is the inputs a_index and b_index, which are the indices of
147
   * children (factors) in monomials a and b which we are currently looking at.
148
   */
149
  bool compareMonomial(
150
      Node oa,
151
      Node a,
152
      unsigned a_index,
153
      NodeMultiset& a_exp_proc,
154
      Node ob,
155
      Node b,
156
      unsigned b_index,
157
      NodeMultiset& b_exp_proc,
158
      int status,
159
      std::vector<Node>& exp,
160
      std::vector<SimpleTheoryLemma>& lem,
161
      std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
162
  /** Check whether we have already inferred a relationship between monomials
163
   * x and y based on the information in cmp_infers. This computes the
164
   * transitive closure of the relation stored in cmp_infers.
165
   */
166
  bool cmp_holds(Node x,
167
                 Node y,
168
                 std::map<Node, std::map<Node, Node> >& cmp_infers,
169
                 std::vector<Node>& exp,
170
                 std::map<Node, bool>& visited);
171
  /** assign order ids */
172
  void assignOrderIds(std::vector<Node>& vars,
173
                      NodeMultiset& d_order,
174
                      bool isConcrete,
175
                      bool isAbsolute);
176
  /** Make literal */
177
  Node mkLit(Node a, Node b, int status, bool isAbsolute = false) const;
178
  /** register monomial */
179
  void setMonomialFactor(Node a, Node b, const NodeMultiset& common);
180
181
  /** Basic data that is shared with other checks */
182
  ExtState* d_data;
183
184
  std::map<Node, bool> d_ms_proc;
185
  // ordering, stores variables and 0,1,-1
186
  std::map<Node, unsigned> d_order_vars;
187
  std::vector<Node> d_order_points;
188
189
  // list of monomials with factors whose model value is non-constant in model
190
  //  e.g. y*cos( x )
191
  std::map<Node, bool> d_m_nconst_factor;
192
};
193
194
}  // namespace nl
195
}  // namespace arith
196
}  // namespace theory
197
}  // namespace CVC4
198
199
#endif