GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/synth_rew_rules.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

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