GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/instantiation_list.h Lines: 6 6 100.0 %
Date: 2021-03-23 Branches: 2 4 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file instantiation_list.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 list of instantiations
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
18
#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
19
20
#include <iosfwd>
21
#include <vector>
22
23
#include "expr/node.h"
24
25
namespace CVC4 {
26
27
/** A list of instantiations for a quantified formula */
28
7
struct InstantiationList
29
{
30
7
  InstantiationList(Node q, const std::vector<std::vector<Node> >& inst)
31
7
      : d_quant(q), d_inst(inst)
32
  {
33
7
  }
34
  /** The quantified formula */
35
  Node d_quant;
36
  /** The instantiation list */
37
  std::vector<std::vector<Node> > d_inst;
38
};
39
40
/** Print the instantiation list to stream out */
41
std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist);
42
43
/** The list of skolemization for a quantified formula */
44
7
struct SkolemList
45
{
46
7
  SkolemList(Node q, const std::vector<Node>& sks) : d_quant(q), d_sks(sks) {}
47
  /** The quantified formula */
48
  Node d_quant;
49
  /** The list of skolems for the quantified formula */
50
  std::vector<Node> d_sks;
51
};
52
53
/** Print the skolem list to stream out */
54
std::ostream& operator<<(std::ostream& out, const SkolemList& skl);
55
56
}  // namespace CVC4
57
58
#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */