GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/sygus_datatype.cpp Lines: 43 43 100.0 %
Date: 2021-03-22 Branches: 39 126 31.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_datatype.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa
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 class for constructing SyGuS datatypes.
13
 **/
14
15
#include "expr/sygus_datatype.h"
16
17
#include <sstream>
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
23
2007
SygusDatatype::SygusDatatype(const std::string& name) : d_dt(DType(name)) {}
24
25
92
std::string SygusDatatype::getName() const { return d_dt.getName(); }
26
27
12160
void SygusDatatype::addConstructor(Node op,
28
                                   const std::string& name,
29
                                   const std::vector<TypeNode>& argTypes,
30
                                   int weight)
31
{
32
12160
  d_cons.push_back(SygusDatatypeConstructor());
33
12160
  d_cons.back().d_op = op;
34
12160
  d_cons.back().d_name = name;
35
12160
  d_cons.back().d_argTypes = argTypes;
36
12160
  d_cons.back().d_weight = weight;
37
12160
}
38
39
64
void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
40
{
41
  // add an "any constant" proxy variable
42
128
  Node av = NodeManager::currentNM()->mkSkolem("_any_constant", tn);
43
  // mark that it represents any constant
44
  SygusAnyConstAttribute saca;
45
64
  av.setAttribute(saca, true);
46
128
  std::stringstream ss;
47
64
  ss << getName() << "_any_constant";
48
128
  std::string cname(ss.str());
49
128
  std::vector<TypeNode> builtinArg;
50
64
  builtinArg.push_back(tn);
51
64
  addConstructor(
52
      av, cname, builtinArg, 0);
53
64
}
54
22
void SygusDatatype::addConstructor(Kind k,
55
                                   const std::vector<TypeNode>& argTypes,
56
                                   int weight)
57
{
58
22
  NodeManager* nm = NodeManager::currentNM();
59
22
  addConstructor(nm->operatorOf(k), kindToString(k), argTypes, weight);
60
22
}
61
62
1220
size_t SygusDatatype::getNumConstructors() const { return d_cons.size(); }
63
64
66
const SygusDatatypeConstructor& SygusDatatype::getConstructor(unsigned i) const
65
{
66
66
  Assert(i < d_cons.size());
67
66
  return d_cons[i];
68
}
69
70
2007
void SygusDatatype::initializeDatatype(TypeNode sygusType,
71
                                       Node sygusVars,
72
                                       bool allowConst,
73
                                       bool allowAll)
74
{
75
  // should not have initialized (set sygus) yet
76
2007
  Assert(!isInitialized());
77
  // should have added a constructor
78
2007
  Assert(!d_cons.empty());
79
  /* Use the sygus type to not lose reference to the original types (Bool,
80
   * Int, etc) */
81
2007
  d_dt.setSygus(sygusType, sygusVars, allowConst, allowAll);
82
14167
  for (unsigned i = 0, ncons = d_cons.size(); i < ncons; ++i)
83
  {
84
    // add (sygus) constructor
85
48640
    d_dt.addSygusConstructor(d_cons[i].d_op,
86
12160
                             d_cons[i].d_name,
87
12160
                             d_cons[i].d_argTypes,
88
12160
                             d_cons[i].d_weight);
89
  }
90
2007
  Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
91
2007
}
92
93
3976
const DType& SygusDatatype::getDatatype() const
94
{
95
  // should have initialized by this point
96
3976
  Assert(isInitialized());
97
3976
  return d_dt;
98
}
99
100
5983
bool SygusDatatype::isInitialized() const { return d_dt.isSygus(); }
101
102
26676
}  // namespace CVC4