GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp Lines: 1 17 5.9 %
Date: 2021-03-22 Branches: 2 42 4.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_enumerator_basic.cpp
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 Implementation of sygus basic enumerator
13
 **/
14
#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
15
16
#include "options/datatypes_options.h"
17
18
using namespace CVC4::kind;
19
using namespace std;
20
21
namespace CVC4 {
22
namespace theory {
23
namespace quantifiers {
24
25
EnumValGeneratorBasic::EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn)
26
    : d_tds(tds), d_te(tn)
27
{
28
}
29
30
bool EnumValGeneratorBasic::increment()
31
{
32
  ++d_te;
33
  if (d_te.isFinished())
34
  {
35
    d_currTerm = Node::null();
36
    return false;
37
  }
38
  d_currTerm = *d_te;
39
  if (options::sygusSymBreakDynamic())
40
  {
41
    Node nextb = d_tds->sygusToBuiltin(d_currTerm);
42
    nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
43
    if (d_cache.find(nextb) == d_cache.end())
44
    {
45
      d_cache.insert(nextb);
46
      // only return the current term if not unique
47
    }
48
    else
49
    {
50
      d_currTerm = Node::null();
51
    }
52
  }
53
  return true;
54
}
55
56
}  // namespace quantifiers
57
}  // namespace theory
58
26676
} /* namespace CVC4 */