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

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Andrew Reynolds, Tim King, Mathias Preiner
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Arithmetic instantiator.
14
 */
15
16
#include "cvc5_private.h"
17
18
#ifndef CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
19
#define CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
20
21
#include <vector>
22
#include "expr/node.h"
23
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
24
#include "theory/quantifiers/cegqi/vts_term_cache.h"
25
26
namespace cvc5 {
27
namespace theory {
28
namespace quantifiers {
29
30
/** Arithmetic instantiator
31
 *
32
 * This implements a selection function for arithmetic, which is based on
33
 * variants of:
34
 * - Loos/Weispfenning's method (virtual term substitution) for linear real
35
 *    arithmetic,
36
 * - Ferrante/Rackoff's method (interior points) for linear real arithmetic,
37
 * - Cooper's method for linear arithmetic.
38
 * For details, see Reynolds et al, "Solving Linear Arithmetic Using
39
 * Counterexample-Guided Instantiation", FMSD 2017.
40
 *
41
 * This class contains all necessary information for instantiating a single
42
 * real or integer typed variable of a single quantified formula.
43
 */
44
class ArithInstantiator : public Instantiator
45
{
46
 public:
47
  ArithInstantiator(TypeNode tn, VtsTermCache* vtc);
48
3292
  virtual ~ArithInstantiator() {}
49
  /** reset */
50
  void reset(CegInstantiator* ci,
51
             SolvedForm& sf,
52
             Node pv,
53
             CegInstEffort effort) override;
54
  /** this instantiator processes equalities */
55
  bool hasProcessEquality(CegInstantiator* ci,
56
                          SolvedForm& sf,
57
                          Node pv,
58
                          CegInstEffort effort) override;
59
  /**
60
   * Process the equality term[0]=term[1]. If this equality is equivalent to one
61
   * of the form c * pv = t, then we add the substitution c * pv -> t to sf and
62
   * recurse.
63
   */
64
  bool processEquality(CegInstantiator* ci,
65
                       SolvedForm& sf,
66
                       Node pv,
67
                       std::vector<TermProperties>& term_props,
68
                       std::vector<Node>& terms,
69
                       CegInstEffort effort) override;
70
  /** this instantiator processes assertions */
71
  bool hasProcessAssertion(CegInstantiator* ci,
72
                           SolvedForm& sf,
73
                           Node pv,
74
                           CegInstEffort effort) override;
75
  /** this instantiator processes literals lit of kinds EQUAL and GEQ */
76
  Node hasProcessAssertion(CegInstantiator* ci,
77
                           SolvedForm& sf,
78
                           Node pv,
79
                           Node lit,
80
                           CegInstEffort effort) override;
81
  /** process assertion lit
82
   *
83
   * If lit can be turned into a bound of the form c * pv <> t, then we store
84
   * information about this bound (see d_mbp_bounds).
85
   *
86
   * If cbqiModel is false (not the default), we recursively try adding the
87
   * substitution { c * pv -> t } to sf and recursing.
88
   */
89
  bool processAssertion(CegInstantiator* ci,
90
                        SolvedForm& sf,
91
                        Node pv,
92
                        Node lit,
93
                        Node alit,
94
                        CegInstEffort effort) override;
95
  /** process assertions
96
   *
97
   * This is called after processAssertion has been called on all current bounds
98
   * for pv. This method selects the "best" bound of those we have seen, which
99
   * can be one of the following:
100
   * - Maximal lower bound,
101
   * - Minimal upper bound,
102
   * - Midpoint of maximal lower and minimal upper bounds, [if pv is not Int,
103
   *   and --cbqi-midpoint]
104
   * - (+-) Infinity, [if no upper (resp. lower) bounds, and --cbqi-use-vts-inf]
105
   * - Zero, [if no bounds]
106
   * - Non-optimal bounds. [if the above bounds fail, and --cbqi-nopt]
107
   */
108
  bool processAssertions(CegInstantiator* ci,
109
                         SolvedForm& sf,
110
                         Node pv,
111
                         CegInstEffort effort) override;
112
  /**
113
   * This instantiator needs to postprocess variables that have substitutions
114
   * with coefficients, i.e. c*x -> t.
115
   */
116
  bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
117
                                                SolvedForm& sf,
118
                                                Node pv,
119
                                                CegInstEffort effort) override;
120
  /** post-process instantiation for variable
121
   *
122
   * If the solved form for integer variable pv is a substitution with
123
   * coefficients c*x -> t, this turns its solved form into x -> div(t,c), where
124
   * div is integer division.
125
   */
126
  bool postProcessInstantiationForVariable(CegInstantiator* ci,
127
                                           SolvedForm& sf,
128
                                           Node pv,
129
                                           CegInstEffort effort) override;
130
27791
  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 cvc5
214
215
#endif /* CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */