GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_match_generator_multi_linear.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 multi-linear inst match generator class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
18
#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "theory/quantifiers/ematching/inst_match_generator.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace inst {
28
29
/** InstMatchGeneratorMultiLinear class
30
 *
31
 * This is the default implementation of multi-triggers.
32
 *
33
 * Handling multi-triggers using this class is done by constructing a linked
34
 * list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one
35
 * InstMatchGeneratorMultiLinear at the head and a list of trailing
36
 * InstMatchGenerators.
37
 *
38
 * CVC4 employs techniques that ensure that the number of instantiations
39
 * is worst-case polynomial wrt the number of ground terms, where this class
40
 * lifts this policy to multi-triggers. In particular consider
41
 *
42
 *  multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) }
43
 *
44
 * For this multi-trigger, we insist that for each i=1...4, and each ground term
45
 * t, there is at most 1 instantiation added as a result of matching
46
 *    ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
47
 * against ground terms of the form
48
 *    ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4.
49
 * Meaning we add instantiations for the multi-trigger
50
 * ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against:
51
 *   ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) )
52
 *   ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) )
53
 *   ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) )
54
 * Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l.
55
 *
56
 * For example, we disallow adding instantiations based on matching against both
57
 * ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and
58
 * ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) )
59
 * against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched
60
 * against f( x1 ) twice.
61
 *
62
 * This policy can be disabled by --no-multi-trigger-linear.
63
 *
64
 */
65
2450
class InstMatchGeneratorMultiLinear : public InstMatchGenerator
66
{
67
  friend class InstMatchGenerator;
68
69
 public:
70
  /** Reset. */
71
  bool reset(Node eqc) override;
72
  /** Get the next match. */
73
  int getNextMatch(Node q, InstMatch& m) override;
74
75
 protected:
76
  /** reset the children of this generator */
77
  int resetChildren();
78
  /** constructor */
79
  InstMatchGeneratorMultiLinear(Trigger* tparent,
80
                                Node q,
81
                                std::vector<Node>& pats);
82
};
83
84
}  // namespace inst
85
}  // namespace theory
86
}  // namespace CVC4
87
88
#endif