1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Abdalrhman Mohamed, Andrew Reynolds |
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 |
|
* Reconstruct Type Info class implementation. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/sygus/rcons_type_info.h" |
17 |
|
|
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
#include "smt/env.h" |
20 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
21 |
|
#include "theory/quantifiers/sygus/rcons_obligation.h" |
22 |
|
#include "theory/quantifiers/sygus_sampler.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace quantifiers { |
27 |
|
|
28 |
57 |
void RConsTypeInfo::initialize(Env& env, |
29 |
|
TermDbSygus* tds, |
30 |
|
SygusStatistics& s, |
31 |
|
TypeNode stn, |
32 |
|
const std::vector<Node>& builtinVars) |
33 |
|
{ |
34 |
57 |
NodeManager* nm = NodeManager::currentNM(); |
35 |
57 |
SkolemManager* sm = nm->getSkolemManager(); |
36 |
|
|
37 |
57 |
d_enumerator.reset(new SygusEnumerator(tds, nullptr, &s, true)); |
38 |
57 |
d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn)); |
39 |
57 |
d_crd.reset(new CandidateRewriteDatabase(env, true, false, true, false)); |
40 |
|
// since initial samples are not always useful for equivalence checks, set |
41 |
|
// their number to 0 |
42 |
57 |
d_sygusSampler.reset(new SygusSampler(env)); |
43 |
57 |
d_sygusSampler->initialize(stn, builtinVars, 0); |
44 |
57 |
d_crd->initialize(builtinVars, d_sygusSampler.get()); |
45 |
57 |
} |
46 |
|
|
47 |
11688 |
Node RConsTypeInfo::nextEnum() |
48 |
|
{ |
49 |
11688 |
if (!d_enumerator->increment()) |
50 |
|
{ |
51 |
656 |
Trace("sygus-rcons") << "no increment" << std::endl; |
52 |
656 |
return Node::null(); |
53 |
|
} |
54 |
|
|
55 |
22064 |
Node sz = d_enumerator->getCurrent(); |
56 |
|
|
57 |
22064 |
Trace("sygus-rcons") << (sz == Node::null() |
58 |
22064 |
? sz |
59 |
11032 |
: datatypes::utils::sygusToBuiltin(sz)) |
60 |
11032 |
<< std::endl; |
61 |
|
|
62 |
11032 |
return sz; |
63 |
|
} |
64 |
|
|
65 |
794 |
Node RConsTypeInfo::addTerm(Node n) |
66 |
|
{ |
67 |
1588 |
std::stringstream out; |
68 |
1588 |
return d_crd->addTerm(n, false, out); |
69 |
|
} |
70 |
|
|
71 |
721 |
void RConsTypeInfo::setBuiltinToOb(Node t, RConsObligation* ob) |
72 |
|
{ |
73 |
721 |
d_ob.emplace(t, ob); |
74 |
721 |
} |
75 |
|
|
76 |
15878 |
RConsObligation* RConsTypeInfo::builtinToOb(Node t) |
77 |
|
{ |
78 |
15878 |
auto it = d_ob.find(t); |
79 |
15878 |
if (it != d_ob.cend()) |
80 |
|
{ |
81 |
15186 |
return it->second; |
82 |
|
} |
83 |
692 |
return nullptr; |
84 |
|
} |
85 |
|
|
86 |
|
} // namespace quantifiers |
87 |
|
} // namespace theory |
88 |
31125 |
} // namespace cvc5 |