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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief multilinear 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 multitriggers. 
32 

* 
33 

* Handling multitriggers 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 worstcase polynomial wrt the number of ground terms, where this class 
40 

* lifts this policy to multitriggers. In particular consider 
41 

* 
42 

* multitrigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) } 
43 

* 
44 

* For this multitrigger, 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 multitrigger 
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 nomultitriggerlinear. 
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 