summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/cegis_unif.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.h')
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.h5
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index c32a1390c..448150d06 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -88,8 +88,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
* registerEvalPtAtSize on the output channel of d_qe.
*/
void registerEvalPts(const std::vector<Node>& eis, Node e);
- /** Retrieves active guard for enumerator */
- Node getActiveGuardForEnumerator(Node e);
private:
/** reference to quantifier engine */
@@ -102,9 +100,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
bool d_initialized;
/** null node */
Node d_null;
- /** map from condition enumerators to active guards (in case they are
- * enumerated indepedently of the return values) */
- std::map<Node, Node> d_enum_to_active_guard;
/** information per initialized type */
class StrategyPtInfo
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback