GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_arith_instantiator.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 16 22 72.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ceg_arith_instantiator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, 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 ceg_arith_instantiator
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
18
#define CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
19
20
#include <vector>
21
#include "expr/node.h"
22
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
23
#include "theory/quantifiers/cegqi/vts_term_cache.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
/** Arithmetic instantiator
30
 *
31
 * This implements a selection function for arithmetic, which is based on
32
 * variants of:
33
 * - Loos/Weispfenning's method (virtual term substitution) for linear real
34
 *    arithmetic,
35
 * - Ferrante/Rackoff's method (interior points) for linear real arithmetic,
36
 * - Cooper's method for linear arithmetic.
37
 * For details, see Reynolds et al, "Solving Linear Arithmetic Using
38
 * Counterexample-Guided Instantiation", FMSD 2017.
39
 *
40
 * This class contains all necessary information for instantiating a single
41
 * real or integer typed variable of a single quantified formula.
42
 */
43
class ArithInstantiator : public Instantiator
44
{
45
 public:
46
  ArithInstantiator(TypeNode tn, VtsTermCache* vtc);
47
3326
  virtual ~ArithInstantiator() {}
48
  /** reset */
49
  void reset(CegInstantiator* ci,
50
             SolvedForm& sf,
51
             Node pv,
52
             CegInstEffort effort) override;
53
  /** this instantiator processes equalities */
54
  bool hasProcessEquality(CegInstantiator* ci,
55
                          SolvedForm& sf,
56
                          Node pv,
57
                          CegInstEffort effort) override;
58
  /**
59
   * Process the equality term[0]=term[1]. If this equality is equivalent to one
60
   * of the form c * pv = t, then we add the substitution c * pv -> t to sf and
61
   * recurse.
62
   */
63
  bool processEquality(CegInstantiator* ci,
64
                       SolvedForm& sf,
65
                       Node pv,
66
                       std::vector<TermProperties>& term_props,
67
                       std::vector<Node>& terms,
68
                       CegInstEffort effort) override;
69
  /** this instantiator processes assertions */
70
  bool hasProcessAssertion(CegInstantiator* ci,
71
                           SolvedForm& sf,
72
                           Node pv,
73
                           CegInstEffort effort) override;
74
  /** this instantiator processes literals lit of kinds EQUAL and GEQ */
75
  Node hasProcessAssertion(CegInstantiator* ci,
76
                           SolvedForm& sf,
77
                           Node pv,
78
                           Node lit,
79
                           CegInstEffort effort) override;
80
  /** process assertion lit
81
   *
82
   * If lit can be turned into a bound of the form c * pv <> t, then we store
83
   * information about this bound (see d_mbp_bounds).
84
   *
85
   * If cbqiModel is false (not the default), we recursively try adding the
86
   * substitution { c * pv -> t } to sf and recursing.
87
   */
88
  bool processAssertion(CegInstantiator* ci,
89
                        SolvedForm& sf,
90
                        Node pv,
91
                        Node lit,
92
                        Node alit,
93
                        CegInstEffort effort) override;
94
  /** process assertions
95
   *
96
   * This is called after processAssertion has been called on all current bounds
97
   * for pv. This method selects the "best" bound of those we have seen, which
98
   * can be one of the following:
99
   * - Maximal lower bound,
100
   * - Minimal upper bound,
101
   * - Midpoint of maximal lower and minimal upper bounds, [if pv is not Int,
102
   *   and --cbqi-midpoint]
103
   * - (+-) Infinity, [if no upper (resp. lower) bounds, and --cbqi-use-vts-inf]
104
   * - Zero, [if no bounds]
105
   * - Non-optimal bounds. [if the above bounds fail, and --cbqi-nopt]
106
   */
107
  bool processAssertions(CegInstantiator* ci,
108
                         SolvedForm& sf,
109
                         Node pv,
110
                         CegInstEffort effort) override;
111
  /**
112
   * This instantiator needs to postprocess variables that have substitutions
113
   * with coefficients, i.e. c*x -> t.
114
   */
115
  bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
116
                                                SolvedForm& sf,
117
                                                Node pv,
118
                                                CegInstEffort effort) override;
119
  /** post-process instantiation for variable
120
   *
121
   * If the solved form for integer variable pv is a substitution with
122
   * coefficients c*x -> t, this turns its solved form into x -> div(t,c), where
123
   * div is integer division.
124
   */
125
  bool postProcessInstantiationForVariable(CegInstantiator* ci,
126
                                           SolvedForm& sf,
127
                                           Node pv,
128
                                           CegInstEffort effort,
129
                                           std::vector<Node>& lemmas) override;
130
11804
  std::string identify() const override { return "Arith"; }
131
132
 private:
133
  /** pointer to the virtual term substitution term cache class */
134
  VtsTermCache* d_vtc;
135
  /** zero/one */
136
  Node d_zero;
137
  Node d_one;
138
  //--------------------------------------current bounds
139
  /** Virtual term symbols (vts), where 0: infinity, 1: delta. */
140
  Node d_vts_sym[2];
141
  /** Current 0:lower, 1:upper bounds for the variable to instantiate */
142
  std::vector<Node> d_mbp_bounds[2];
143
  /** Coefficients for the lower/upper bounds for the variable to instantiate */
144
  std::vector<Node> d_mbp_coeff[2];
145
  /** Coefficients for virtual terms for each bound. */
146
  std::vector<Node> d_mbp_vts_coeff[2][2];
147
  /** The source literal (explanation) for each bound. */
148
  std::vector<Node> d_mbp_lit[2];
149
  //--------------------------------------end current bounds
150
  /** solve arith
151
   *
152
   * Given variable to instantiate pv, this isolates the atom into solved form:
153
   *    veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf
154
   * where we ensure val has Int type if pv has Int type, and val does not
155
   * contain vts symbols.
156
   *
157
   * It returns a CegTermType:
158
   *   CEG_TT_INVALID if it was not possible to put atom into a solved form,
159
   *   CEG_TT_LOWER if <> in the above equation is >=,
160
   *   CEG_TT_UPPER if <> in the above equation is <=, or
161
   *   CEG_TT_EQUAL if <> in the above equation is =.
162
   */
163
  CegTermType solve_arith(CegInstantiator* ci,
164
                          Node v,
165
                          Node atom,
166
                          Node& veq_c,
167
                          Node& val,
168
                          Node& vts_coeff_inf,
169
                          Node& vts_coeff_delta);
170
  /** get model based projection value
171
   *
172
   * Given a implied (non-strict) bound:
173
   *   c*e <=/>= t + inf_coeff*INF + delta_coeff*DELTA
174
   * this method returns ret, the minimal (resp. maximal) term such that:
175
   *   c*ret <> t + inf_coeff*INF + delta_coeff*DELTA
176
   * is satisfied in the current model M, and such that the divisibilty
177
   * constraint is also satisfied:
178
   *   ret^M mod c*theta = (c*e)^M mod c*theta
179
   * where the input theta is a constant (which is assumed to be 1 if null). The
180
   * values of me and mt are the current model values of e and t respectively.
181
   *
182
   * For example, if e has Real type and:
183
   *   isLower = false, e^M = 0, t^M = 2, inf_coeff = 0, delta_coeff = 2
184
   * Then, this function returns t+2*delta.
185
   *
186
   * For example, if e has Int type and:
187
   *   isLower = true, e^M = 4, t^M = 2, theta = 3
188
   * Then, this function returns t+2, noting that (t+2)^M mod 3 = e^M mod 3 = 2.
189
   *
190
   * For example, if e has Int type and:
191
   *   isLower = false, e^M = 1, t^M = 5, theta = 3
192
   * Then, this function returns t-1, noting that (t-1)^M mod 3 = e^M mod 3 = 1.
193
   *
194
   * The value that is added or substracted from t in the return value when e
195
   * is an integer is the value of "rho" from Figure 6 of Reynolds et al,
196
   * "Solving Linear Arithmetic Using Counterexample-Guided Instantiation",
197
   * FMSD 2017.
198
   */
199
  Node getModelBasedProjectionValue(CegInstantiator* ci,
200
                                    Node e,
201
                                    Node t,
202
                                    bool isLower,
203
                                    Node c,
204
                                    Node me,
205
                                    Node mt,
206
                                    Node theta,
207
                                    Node inf_coeff,
208
                                    Node delta_coeff);
209
};
210
211
}  // namespace quantifiers
212
}  // namespace theory
213
}  // namespace CVC4
214
215
#endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */