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