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