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