summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/cegis_unif.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 83fb6f253..2b17d6d79 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -474,10 +474,6 @@ void CegisUnifEnumManager::incrementNumEnumerators()
<< " to strategy point " << ci.second.d_pt
<< "\n";
d_tds->registerEnumerator(e, ci.second.d_pt, d_parent, false, index==0 ? options::sygusUnifRepairRet() : options::sygusUnifRepairCond());
- // TODO symmetry breaking for making
- // e distinct from ei : (ci.second.d_enums[index] \ {e})
- // if its respective type has had at least
- // ci.second.d_enums[index].size() distinct values enumerated
}
}
// register the evaluation points at the new value
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback