1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner |
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 |
|
* A technique for synthesizing candidate rewrites of the form t1 = t2, |
14 |
|
* where t1 and t2 are subterms of the input. |
15 |
|
*/ |
16 |
|
|
17 |
|
#ifndef CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H |
18 |
|
#define CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H |
19 |
|
|
20 |
|
#include "preprocessing/preprocessing_pass.h" |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace preprocessing { |
24 |
|
namespace passes { |
25 |
|
|
26 |
|
/** |
27 |
|
* This class rewrites the input assertions into a sygus conjecture over a |
28 |
|
* grammar whose terms are "abstractions" of the subterms of |
29 |
|
* assertionsToPreprocess. In detail, assume our input was |
30 |
|
* bvadd( bvlshr( bvadd( a, 4 ), 1 ), b ) = 1 |
31 |
|
* This class constructs this grammar: |
32 |
|
* A -> T1 | T2 | T3 | T4 | Tv |
33 |
|
* T1 -> bvadd( T2, Tv ) | x | y |
34 |
|
* T2 -> bvlshr( T3, T4 ) | x | y |
35 |
|
* T3 -> bvadd( Tv, T5 ) | x | y |
36 |
|
* T4 -> 1 | x | y |
37 |
|
* T5 -> 4 | x | y |
38 |
|
* Tv -> x | y |
39 |
|
* Notice that this grammar generates all subterms of the input where leaves |
40 |
|
* are replaced by the variables x and/or y. The number of variable constructors |
41 |
|
* (x and y in this example) used in this construction is configurable via |
42 |
|
* sygus-rr-synth-input-nvars. The default for this value is 3, the |
43 |
|
* justification is that this covers most of the interesting rewrites while |
44 |
|
* not being too inefficient. |
45 |
|
* |
46 |
|
* Also notice that currently, this grammar construction admits terms that |
47 |
|
* do not necessarily match any in the input. For example, the above grammar |
48 |
|
* admits bvlshr( x, x ), which is not matchable with a subterm of the input. |
49 |
|
* |
50 |
|
* Notice that Booleans are treated specially unless the option |
51 |
|
* --sygus-rr-synth-input-bool is enabled, since we do not by default want to |
52 |
|
* generate purely propositional rewrites. In particular, we allocate only |
53 |
|
* one Boolean variable (to ensure that no sygus type is non-empty). |
54 |
|
* |
55 |
|
* It then rewrites the input into the negated sygus conjecture |
56 |
|
* forall x : ( BV_n x BV_n ) -> BV_n. false |
57 |
|
* where x has the sygus grammar restriction A from above. This conjecture can |
58 |
|
* then be processed using --sygus-rr-synth in the standard way, which will |
59 |
|
* cause candidate rewrites to be printed on the output stream. If multiple |
60 |
|
* types are present, then we generate a conjunction of multiple synthesis |
61 |
|
* conjectures, which we enumerate terms for in parallel. |
62 |
|
*/ |
63 |
19878 |
class SynthRewRulesPass : public PreprocessingPass |
64 |
|
{ |
65 |
|
public: |
66 |
|
SynthRewRulesPass(PreprocessingPassContext* preprocContext); |
67 |
|
|
68 |
|
protected: |
69 |
|
PreprocessingPassResult applyInternal( |
70 |
|
AssertionPipeline* assertionsToPreprocess) override; |
71 |
|
}; |
72 |
|
|
73 |
|
} // namespace passes |
74 |
|
} // namespace preprocessing |
75 |
|
} // namespace cvc5 |
76 |
|
|
77 |
|
#endif /* CVC5__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ |