summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/cegis.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r--src/theory/quantifiers/sygus/cegis.cpp7
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index ad45fb9b7..2e7f0cc02 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -78,7 +78,8 @@ bool Cegis::processInitialize(Node n,
// This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj)
// for each i,j. We do not do this and revert to the default behavior of
// this module instead.
- bool isVarAgnostic = options::sygusEnumVarAgnostic() && csize == 1;
+ bool isActiveGen =
+ options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1;
// initialize an enumerator for each candidate
for (unsigned i = 0; i < csize; i++)
{
@@ -101,9 +102,9 @@ bool Cegis::processInitialize(Node n,
d_tds->registerEnumerator(candidates[i],
candidates[i],
d_parent,
- isVarAgnostic,
+ isActiveGen,
do_repair_const,
- isVarAgnostic);
+ isActiveGen);
}
return true;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback