GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/tangent_plane_check.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 3 4 75.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file tangent_plane_check.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 Check for tangent_plane lemma
13
 **/
14
15
#ifndef CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
16
#define CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
17
18
#include <map>
19
20
#include "expr/node.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
namespace nl {
26
27
struct ExtState;
28
29
4388
class TangentPlaneCheck
30
{
31
 public:
32
  TangentPlaneCheck(ExtState* data);
33
34
  /** check tangent planes
35
   *
36
   * Returns a set of valid theory lemmas, based on an
37
   * "incremental linearization" of non-linear monomials.
38
   * This linearization is accomplished by adding constraints
39
   * corresponding to "tangent planes" at the current
40
   * model value of each non-linear monomial. In particular
41
   * consider the definition for constants a,b :
42
   *   T_{a,b}( x*y ) = b*x + a*y - a*b.
43
   * The lemmas added by this function are of the form :
44
   *  ( ( x>a ^ y<b) ^ (x<a ^ y>b) ) => x*y < T_{a,b}( x*y )
45
   *  ( ( x>a ^ y>b) ^ (x<a ^ y<b) ) => x*y > T_{a,b}( x*y )
46
   * It is inspired by "Invariant Checking of NRA Transition
47
   * Systems via Incremental Reduction to LRA with EUF" by
48
   * Cimatti et al., TACAS 2017.
49
   * This schema is not terminating in general.
50
   * It is not enabled by default, and can
51
   * be enabled by --nl-ext-tplanes.
52
   *
53
   * Examples:
54
   *
55
   * ( ( x>2 ^ y>5) ^ (x<2 ^ y<5) ) => x*y > 5*x + 2*y - 10
56
   * ( ( x>2 ^ y<5) ^ (x<2 ^ y>5) ) => x*y < 5*x + 2*y - 10
57
   */
58
  void check(bool asWaitingLemmas);
59
60
 private:
61
  /** Basic data that is shared with other checks */
62
  ExtState* d_data;
63
  /** tangent plane bounds */
64
  std::map<Node, std::map<Node, Node> > d_tangent_val_bound[4];
65
};
66
67
}  // namespace nl
68
}  // namespace arith
69
}  // namespace theory
70
}  // namespace CVC4
71
72
#endif