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