1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 |
|
* Rewriting based on learned literals |
14 |
|
*/ |
15 |
|
#include "cvc5_private.h" |
16 |
|
|
17 |
|
#ifndef CVC5__PREPROCESSING__PASSES__LEARNED_REWRITE_H |
18 |
|
#define CVC5__PREPROCESSING__PASSES__LEARNED_REWRITE_H |
19 |
|
|
20 |
|
#include "preprocessing/preprocessing_pass.h" |
21 |
|
#include "preprocessing/preprocessing_pass_context.h" |
22 |
|
#include "theory/arith/bound_inference.h" |
23 |
|
#include "util/statistics_stats.h" |
24 |
|
|
25 |
|
#include <iosfwd> |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace preprocessing { |
29 |
|
namespace passes { |
30 |
|
|
31 |
|
/** |
32 |
|
* Learned rewrites in the pass below. |
33 |
|
*/ |
34 |
|
enum class LearnedRewriteId |
35 |
|
{ |
36 |
|
// Elimination of division, int division, int modulus due to non-zero |
37 |
|
// denominator. e.g. (not (= y 0)) => (div x y) ---> (div_total x y) |
38 |
|
NON_ZERO_DEN, |
39 |
|
// Elimination of int modulus due to range. |
40 |
|
// e.g. (and (<= 0 x) (< x n)) => (mod x n) ---> x |
41 |
|
INT_MOD_RANGE, |
42 |
|
// e.g. (>= c 0) => (>= p 0) ---> true where c is inferred const lower bound |
43 |
|
PRED_POS_LB, |
44 |
|
// e.g. (= c 0) => (>= p 0) ---> true where c is inferred const lower bound |
45 |
|
PRED_ZERO_LB, |
46 |
|
// e.g. (> c 0) => (>= p 0) ---> false where c is inferred const upper bound |
47 |
|
PRED_NEG_UB, |
48 |
|
|
49 |
|
//-------------------------------------- NONE |
50 |
|
NONE |
51 |
|
}; |
52 |
|
|
53 |
|
/** |
54 |
|
* Converts an learned rewrite id to a string. |
55 |
|
* |
56 |
|
* @param i The learned rewrite identifier |
57 |
|
* @return The name of the learned rewrite identifier |
58 |
|
*/ |
59 |
|
const char* toString(LearnedRewriteId i); |
60 |
|
|
61 |
|
/** |
62 |
|
* Writes an learned rewrite identifier to a stream. |
63 |
|
* |
64 |
|
* @param out The stream to write to |
65 |
|
* @param i The learned rewrite identifier to write to the stream |
66 |
|
* @return The stream |
67 |
|
*/ |
68 |
|
std::ostream& operator<<(std::ostream& out, LearnedRewriteId i); |
69 |
|
|
70 |
|
/** |
71 |
|
* Applies learned rewriting. This rewrites the input based on learned literals. |
72 |
|
* This in particular does rewriting that goes beyond what is done in |
73 |
|
* non-clausal simplification, where equality substitutions + constant |
74 |
|
* propagations are performed. In particular, this pass applies rewriting |
75 |
|
* based on e.g. bound inference for arithmetic. |
76 |
|
*/ |
77 |
19706 |
class LearnedRewrite : public PreprocessingPass |
78 |
|
{ |
79 |
|
public: |
80 |
|
LearnedRewrite(PreprocessingPassContext* preprocContext); |
81 |
|
|
82 |
|
protected: |
83 |
|
PreprocessingPassResult applyInternal( |
84 |
|
AssertionPipeline* assertionsToPreprocess) override; |
85 |
|
/** |
86 |
|
* Apply rewrite with learned literals, traverses n. |
87 |
|
*/ |
88 |
|
Node rewriteLearnedRec(Node n, |
89 |
|
theory::arith::BoundInference& binfer, |
90 |
|
std::unordered_set<Node>& lems, |
91 |
|
std::unordered_map<TNode, Node>& visited); |
92 |
|
/** |
93 |
|
* Learned rewrite to n, single step. |
94 |
|
*/ |
95 |
|
Node rewriteLearned(Node n, |
96 |
|
theory::arith::BoundInference& binfer, |
97 |
|
std::unordered_set<Node>& lems); |
98 |
|
/** Return learned rewrite */ |
99 |
|
Node returnRewriteLearned(Node n, Node nr, LearnedRewriteId id); |
100 |
|
/** Counts number of applications of learned rewrites */ |
101 |
|
HistogramStat<LearnedRewriteId> d_lrewCount; |
102 |
|
}; |
103 |
|
|
104 |
|
} // namespace passes |
105 |
|
} // namespace preprocessing |
106 |
|
} // namespace cvc5 |
107 |
|
|
108 |
|
#endif /* CVC5__PREPROCESSING__PASSES__LEARNED_REWRITE_H */ |