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

Line Exec Source
1
/*********************                                                        */
2
/*! \file monomial_bounds_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 monomial bound inference lemmas
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
16
#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
17
18
#include "expr/node.h"
19
#include "theory/arith/nl/ext/constraint.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace arith {
24
namespace nl {
25
26
struct ExtState;
27
28
4386
class MonomialBoundsCheck
29
{
30
 public:
31
  MonomialBoundsCheck(ExtState* data);
32
33
  void init();
34
35
  /** check monomial inferred bounds
36
   *
37
   * Returns a set of valid theory lemmas, based on a
38
   * lemma schema that infers new constraints about existing
39
   * terms based on mulitplying both sides of an existing
40
   * constraint by a term.
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 "Multiply".
44
   *
45
   * Examples:
46
   *
47
   * x > 0 ^ (y > z + w) => x*y > x*(z+w)
48
   * x < 0 ^ (y > z + w) => x*y < x*(z+w)
49
   *   ...where (y > z + w) and x*y are a constraint and term
50
   *      that occur in the current context.
51
   */
52
  void checkBounds(const std::vector<Node>& asserts,
53
                   const std::vector<Node>& false_asserts);
54
55
  /** check monomial infer resolution bounds
56
   *
57
   * Returns a set of valid theory lemmas, based on a
58
   * lemma schema which "resolves" upper bounds
59
   * of one inequality with lower bounds for another.
60
   * This schema is not enabled by default, and can
61
   * be enabled by --nl-ext-rbound.
62
   *
63
   * Examples:
64
   *
65
   *  ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
66
   *  ...where s <= x*z and x*y <= t are constraints
67
   *     that occur in the current context.
68
   */
69
  void checkResBounds();
70
71
 private:
72
  /** Basic data that is shared with other checks */
73
  ExtState* d_data;
74
75
  /** Context-independent database of constraint information */
76
  ConstraintDb d_cdb;
77
78
  // term -> coeff -> rhs -> ( status, exp, b ),
79
  //   where we have that : exp =>  ( coeff * term <status> rhs )
80
  //   b is true if degree( term ) >= degree( rhs )
81
  std::map<Node, std::map<Node, std::map<Node, Kind> > > d_ci;
82
  std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp;
83
  std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max;
84
};
85
86
}  // namespace nl
87
}  // namespace arith
88
}  // namespace theory
89
}  // namespace CVC4
90
91
#endif