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