summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/enum_value_manager.cpp
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2021-09-09 19:48:18 -0700
committerGitHub <noreply@github.com>2021-09-09 19:48:18 -0700
commit25597467c8df64c36e8353bfcf9d99d02fdd798b (patch)
tree9be8240f0ce11022100072bb6fb46c61ff448420 /src/theory/quantifiers/sygus/enum_value_manager.cpp
parent5fbc99c94d65b7e3fc0212e9f1e49ae8907643fe (diff)
parent5369982ff5c493f72e6f8309d8be632866314805 (diff)
Merge branch 'master' into stdAttrsstdAttrs
Diffstat (limited to 'src/theory/quantifiers/sygus/enum_value_manager.cpp')
-rw-r--r--src/theory/quantifiers/sygus/enum_value_manager.cpp8
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index 8a2d70bfa..e7b3bbaa9 100644
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -33,13 +33,15 @@ namespace cvc5 {
namespace theory {
namespace quantifiers {
-EnumValueManager::EnumValueManager(Node e,
+EnumValueManager::EnumValueManager(Env& env,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
TermRegistry& tr,
SygusStatistics& s,
+ Node e,
bool hasExamples)
- : d_enum(e),
+ : EnvObj(env),
+ d_enum(e),
d_qstate(qs),
d_qim(qim),
d_treg(tr),
@@ -108,7 +110,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
d_samplerRrV->initializeSygus(
d_tds, e, options::sygusSamples(), false);
// use the default output for the output of sygusRewVerify
- out = d_qstate.options().base.out;
+ out = options().base.out;
}
d_secd.reset(new SygusEnumeratorCallbackDefault(
e, &d_stats, d_eec.get(), d_samplerRrV.get(), out));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback