GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_enumerator_basic.h Lines: 0 4 0.0 %
Date: 2021-03-23 Branches: 0 2 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_enumerator_basic.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 Basic sygus enumerator class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
19
20
#include <map>
21
#include <unordered_set>
22
#include "expr/node.h"
23
#include "expr/type_node.h"
24
#include "theory/quantifiers/sygus/synth_conjecture.h"
25
#include "theory/quantifiers/sygus/term_database_sygus.h"
26
#include "theory/type_enumerator.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
/** A basic sygus value generator
33
 *
34
 * This class is a "naive" term generator for sygus conjectures, which invokes
35
 * the type enumerator to generate a stream of (all) sygus terms of a given
36
 * type.
37
 */
38
class EnumValGeneratorBasic : public EnumValGenerator
39
{
40
 public:
41
  EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn);
42
  ~EnumValGeneratorBasic() {}
43
  /** initialize (do nothing) */
44
  void initialize(Node e) override {}
45
  /** initialize (do nothing) */
46
  void addValue(Node v) override { d_currTerm = *d_te; }
47
  /**
48
   * Get next returns the next (T-rewriter-unique) value based on the type
49
   * enumerator.
50
   */
51
  bool increment() override;
52
  /** get the current term */
53
  Node getCurrent() override { return d_currTerm; }
54
55
 private:
56
  /** pointer to term database sygus */
57
  TermDbSygus* d_tds;
58
  /** the type enumerator */
59
  TypeEnumerator d_te;
60
  /** the current term */
61
  Node d_currTerm;
62
  /** cache of (enumerated) builtin values we have enumerated so far */
63
  std::unordered_set<Node, NodeHashFunction> d_cache;
64
};
65
66
}  // namespace quantifiers
67
}  // namespace theory
68
}  // namespace CVC4
69
70
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */