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