Rename datatypes sygus solver (#3417)

5 files changed, 74 insertions, 76 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index dd2b7eaea..f2ccbd765 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -401,8 +401,8 @@ libcvc4_add_sources(
   theory/care_graph.h
   theory/datatypes/datatypes_rewriter.cpp
   theory/datatypes/datatypes_rewriter.h
-  theory/datatypes/datatypes_sygus.cpp
-  theory/datatypes/datatypes_sygus.h
+  theory/datatypes/sygus_extension.cpp
+  theory/datatypes/sygus_extension.h
   theory/datatypes/sygus_simple_sym.cpp
   theory/datatypes/sygus_simple_sym.h
   theory/datatypes/theory_datatypes.cpp
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/sygus_extension.cpp
index 4cc9e4640..7e5a3ae98 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1,20 +1,18 @@
 /*********************                                                        */
-/*! \file datatypes_sygus.cpp
+/*! \file sygus_extension.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Morgan Deters
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Implementation of sygus utilities for theory of datatypes
- **
- ** Implementation of sygus utilities for theory of datatypes
+ ** \brief Implementation of the sygus extension of the theory of datatypes.
  **/
 
-#include "theory/datatypes/datatypes_sygus.h"
+#include "theory/datatypes/sygus_extension.h"
 
 #include "expr/node_manager.h"
 #include "options/base_options.h"
@@ -35,7 +33,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
-SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
+SygusExtension::SygusExtension(TheoryDatatypes* td,
                                    QuantifiersEngine* qe,
                                    context::Context* c)
     : d_td(td),
@@ -50,12 +48,12 @@ SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
   d_true = NodeManager::currentNM()->mkConst(true);
 }
 
-SygusSymBreakNew::~SygusSymBreakNew() {
+SygusExtension::~SygusExtension() {
 
 }
 
 /** add tester */
-void SygusSymBreakNew::assertTester( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) {
+void SygusExtension::assertTester( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) {
   registerTerm( n, lemmas );
   // check if this is a relevant (sygus) term
   if( d_term_to_anchor.find( n )!=d_term_to_anchor.end() ){
@@ -100,7 +98,7 @@ void SygusSymBreakNew::assertTester( int tindex, TNode n, Node exp, std::vector<
   }
 }
 
-void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& lemmas ) {
+void SygusExtension::assertFact( Node n, bool polarity, std::vector< Node >& lemmas ) {
   if (n.getKind() == kind::DT_SYGUS_BOUND)
   {
     Node m = n[0];
@@ -125,7 +123,7 @@ void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& l
   }
 }
 
-Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) {
+Node SygusExtension::getTermOrderPredicate( Node n1, Node n2 ) {
   NodeManager* nm = NodeManager::currentNM();
   std::vector< Node > comm_disj;
   // (1) size of left is greater than size of right
@@ -163,7 +161,7 @@ Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) {
   return nm->mkNode(kind::OR, comm_disj);
 }
 
-void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) {
+void SygusExtension::registerTerm( Node n, std::vector< Node >& lemmas ) {
   if( d_is_top_level.find( n )==d_is_top_level.end() ){
     d_is_top_level[n] = false;
     TypeNode tn = n.getType();
@@ -205,7 +203,7 @@ void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) {
   }
 }
 
-bool SygusSymBreakNew::computeTopLevel( TypeNode tn, Node n ){
+bool SygusExtension::computeTopLevel( TypeNode tn, Node n ){
   if( n.getType()==tn ){
     return false;
   }else if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
@@ -215,7 +213,7 @@ bool SygusSymBreakNew::computeTopLevel( TypeNode tn, Node n ){
   }
 }
 
-void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) {
+void SygusExtension::assertTesterInternal( int tindex, TNode n, Node exp, std::vector< Node >& lemmas ) {
   TypeNode ntn = n.getType();
   if (!ntn.isDatatype())
   {
@@ -379,7 +377,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   }
 }
 
-Node SygusSymBreakNew::getRelevancyCondition( Node n ) {
+Node SygusExtension::getRelevancyCondition( Node n ) {
   std::map< Node, Node >::iterator itr = d_rlv_cond.find( n );
   if( itr==d_rlv_cond.end() ){
     Node cond;
@@ -427,7 +425,7 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) {
   }
 }
 
-Node SygusSymBreakNew::getTraversalPredicate(TypeNode tn, Node n, bool isPre)
+Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre)
 {
   unsigned index = isPre ? 0 : 1;
   std::map<Node, Node>::iterator itt = d_traversal_pred[index][tn].find(n);
@@ -444,7 +442,7 @@ Node SygusSymBreakNew::getTraversalPredicate(TypeNode tn, Node n, bool isPre)
   return pred;
 }
 
-Node SygusSymBreakNew::eliminateTraversalPredicates(Node n)
+Node SygusExtension::eliminateTraversalPredicates(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
@@ -520,7 +518,7 @@ Node SygusSymBreakNew::eliminateTraversalPredicates(Node n)
   return visited[n];
 }
 
-Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
+Node SygusExtension::getSimpleSymBreakPred(Node e,
                                              TypeNode tn,
                                              int tindex,
                                              unsigned depth,
@@ -939,11 +937,11 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e,
   return sb_pred;
 }
 
-TNode SygusSymBreakNew::getFreeVar( TypeNode tn ) {
+TNode SygusExtension::getFreeVar( TypeNode tn ) {
   return d_tds->getFreeVar(tn, 0);
 }
 
-void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ) {
+void SygusExtension::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ) {
   //register this term
   std::unordered_map<Node, Node, NodeHashFunction>::iterator ita =
       d_term_to_anchor.find(n);
@@ -959,7 +957,7 @@ void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool
   }
 }
 
-Node SygusSymBreakNew::registerSearchValue(Node a,
+Node SygusExtension::registerSearchValue(Node a,
                                            Node n,
                                            Node nv,
                                            unsigned d,
@@ -1167,7 +1165,7 @@ Node SygusSymBreakNew::registerSearchValue(Node a,
   return nv;
 }
 
-void SygusSymBreakNew::registerSymBreakLemmaForValue(
+void SygusExtension::registerSymBreakLemmaForValue(
     Node a,
     Node val,
     quantifiers::SygusInvarianceTest& et,
@@ -1188,7 +1186,7 @@ void SygusSymBreakNew::registerSymBreakLemmaForValue(
   registerSymBreakLemma(tn, lem, sz, a, lemmas);
 }
 
-void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz, Node a, std::vector< Node >& lemmas ) {
+void SygusExtension::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz, Node a, std::vector< Node >& lemmas ) {
   // lem holds for all terms of type tn, and is applicable to terms of size sz
   Trace("sygus-sb-debug") << "  register sym break lemma : " << lem
                           << std::endl;
@@ -1221,13 +1219,14 @@ void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz
     }
   }
 }
-void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, std::vector< Node >& lemmas ) {
+
+void SygusExtension::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, std::vector< Node >& lemmas ) {
   Assert(d_term_to_anchor.find(t) != d_term_to_anchor.end());
   Node a = d_term_to_anchor[t];
   addSymBreakLemmasFor( tn, t, d, a, lemmas );
 }
 
-void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, Node a, std::vector< Node >& lemmas ) {
+void SygusExtension::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, Node a, std::vector< Node >& lemmas ) {
   Assert(t.getType() == tn);
   Assert(!a.isNull());
   Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d
@@ -1262,14 +1261,14 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No
   Trace("sygus-sb-debug2") << "...finished." << std::endl;
 }
 
-void SygusSymBreakNew::preRegisterTerm( TNode n, std::vector< Node >& lemmas  ) {
+void SygusExtension::preRegisterTerm( TNode n, std::vector< Node >& lemmas  ) {
   if( n.isVar() ){
     Trace("sygus-sb-debug") << "Pre-register variable : " << n << std::endl;
     registerSizeTerm( n, lemmas );
   }
 }
 
-void SygusSymBreakNew::registerSizeTerm(Node e, std::vector<Node>& lemmas)
+void SygusExtension::registerSizeTerm(Node e, std::vector<Node>& lemmas)
 {
   if (d_register_st.find(e) != d_register_st.end())
   {
@@ -1385,7 +1384,7 @@ void SygusSymBreakNew::registerSizeTerm(Node e, std::vector<Node>& lemmas)
   }
 }
 
-void SygusSymBreakNew::registerMeasureTerm( Node m ) {
+void SygusExtension::registerMeasureTerm( Node m ) {
   std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator it =
       d_szinfo.find(m);
   if( it==d_szinfo.end() ){
@@ -1398,7 +1397,7 @@ void SygusSymBreakNew::registerMeasureTerm( Node m ) {
   }
 }
 
-void SygusSymBreakNew::notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ) {
+void SygusExtension::notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ) {
   std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
       d_szinfo.find(m);
   Assert(its != d_szinfo.end());
@@ -1408,7 +1407,7 @@ void SygusSymBreakNew::notifySearchSize( Node m, unsigned s, Node exp, std::vect
     Assert(s == 0
            || its->second->d_search_size.find(s - 1)
                   != its->second->d_search_size.end());
-    Trace("sygus-fair") << "SygusSymBreakNew:: now considering term measure : " << s << " for " << m << std::endl;
+    Trace("sygus-fair") << "SygusExtension:: now considering term measure : " << s << " for " << m << std::endl;
     Assert(s >= its->second->d_curr_search_size);
     while( s>its->second->d_curr_search_size ){
       incrementCurrentSearchSize( m, lemmas );
@@ -1427,7 +1426,7 @@ void SygusSymBreakNew::notifySearchSize( Node m, unsigned s, Node exp, std::vect
   }
 }
 
-unsigned SygusSymBreakNew::getSearchSizeFor( Node n ) {
+unsigned SygusExtension::getSearchSizeFor( Node n ) {
   Trace("sygus-sb-debug2") << "get search size for term : " << n << std::endl;
   std::unordered_map<Node, Node, NodeHashFunction>::iterator ita =
       d_term_to_anchor.find(n);
@@ -1435,14 +1434,14 @@ unsigned SygusSymBreakNew::getSearchSizeFor( Node n ) {
   return getSearchSizeForAnchor( ita->second );
 }
 
-unsigned SygusSymBreakNew::getSearchSizeForAnchor( Node a ) {
+unsigned SygusExtension::getSearchSizeForAnchor( Node a ) {
   Trace("sygus-sb-debug2") << "get search size for anchor : " << a << std::endl;
   std::map< Node, Node >::iterator it = d_anchor_to_measure_term.find( a );
   Assert(it != d_anchor_to_measure_term.end());
   return getSearchSizeForMeasureTerm(it->second);
 }
 
-unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m)
+unsigned SygusExtension::getSearchSizeForMeasureTerm(Node m)
 {
   Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl;
   std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
@@ -1451,7 +1450,7 @@ unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m)
   return its->second->d_curr_search_size;
 }
   
-void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ) {
+void SygusExtension::incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ) {
   std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator itsz =
       d_szinfo.find(m);
   Assert(itsz != d_szinfo.end());
@@ -1496,8 +1495,8 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >&
   }
 }
 
-void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
-  Trace("sygus-sb") << "SygusSymBreakNew::check" << std::endl;
+void SygusExtension::check( std::vector< Node >& lemmas ) {
+  Trace("sygus-sb") << "SygusExtension::check" << std::endl;
 
   // check for externally registered symmetry breaking lemmas
   std::vector<Node> anchors;
@@ -1605,7 +1604,7 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
           if (rsv.isNull())
           {
             isExc = true;
-            Trace("sygus-sb") << "  SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
+            Trace("sygus-sb") << "  SygusExtension::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
           }
           else
           {
@@ -1617,10 +1616,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
       prog.setAttribute(ssbo, !isExc);
     }
   }
-  Trace("sygus-sb") << "SygusSymBreakNew::check: finished." << std::endl;
+  Trace("sygus-sb") << "SygusExtension::check: finished." << std::endl;
   if (needsRecheck)
   {
-    Trace("sygus-sb") << " SygusSymBreakNew::rechecking..." << std::endl;
+    Trace("sygus-sb") << " SygusExtension::rechecking..." << std::endl;
     return check(lemmas);
   }
 
@@ -1649,7 +1648,7 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
   }
 }
 
-bool SygusSymBreakNew::checkValue(Node n,
+bool SygusExtension::checkValue(Node n,
                                   Node vn,
                                   int ind,
                                   std::vector<Node>& lemmas)
@@ -1693,7 +1692,7 @@ bool SygusSymBreakNew::checkValue(Node n,
       // This should not happen generally, it is caused by a sygus term not
       // being assigned a tester.
       Node split = utils::mkSplit(n, dt);
-      Trace("sygus-sb") << "  SygusSymBreakNew::check: ...WARNING: considered "
+      Trace("sygus-sb") << "  SygusExtension::check: ...WARNING: considered "
                            "missing split for "
                         << n << "." << std::endl;
       Assert(!split.isNull());
@@ -1714,7 +1713,7 @@ bool SygusSymBreakNew::checkValue(Node n,
   return true;
 }
 
-Node SygusSymBreakNew::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ) {
+Node SygusExtension::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ) {
   if( d_active_terms.find( n )!=d_active_terms.end() ){
     TypeNode tn = n.getType();
     IntMap::const_iterator it = d_testers.find( n );
@@ -1736,7 +1735,7 @@ Node SygusSymBreakNew::getCurrentTemplate( Node n, std::map< TypeNode, int >& va
   }
 }
 
-Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkMeasureValue(
+Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue(
     std::vector<Node>& lemmas)
 {
   if (d_measure_value.isNull())
@@ -1751,7 +1750,7 @@ Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkMeasureValue(
   return d_measure_value;
 }
 
-Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
+Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
     std::vector<Node>& lemmas, bool mkNew)
 {
   if (mkNew)
@@ -1769,7 +1768,7 @@ Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
   return d_measure_value_active;
 }
 
-Node SygusSymBreakNew::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
+Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
 {
   if (options::sygusFair() == SYGUS_FAIR_NONE)
   {
@@ -1790,7 +1789,7 @@ Node SygusSymBreakNew::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
   return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s)));
 }
 
-int SygusSymBreakNew::getGuardStatus( Node g ) {
+int SygusExtension::getGuardStatus( Node g ) {
   bool value;
   if( d_td->getValuation().hasSatValue( g, value ) ) {
     if( value ){
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/sygus_extension.h
index 95c259f2b..631f11040 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/sygus_extension.h
@@ -1,23 +1,21 @@
 /*********************                                                        */
-/*! \file datatypes_sygus.h
+/*! \file sygus_extension.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Dejan Jovanovic
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Sygus utilities for theory of datatypes
- **
- ** Theory of datatypes.
+ ** \brief The sygus extension of the theory of datatypes.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_NEW_H
-#define CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_NEW_H
+#ifndef CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H
+#define CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H
 
 #include <iostream>
 #include <map>
@@ -64,7 +62,7 @@ class TheoryDatatypes;
  * We prioritize decisions of form (1) before (2). Both kinds of decision are
  * critical for solution completeness, which is enforced by DecisionManager.
  */
-class SygusSymBreakNew
+class SygusExtension
 {
   typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
@@ -72,10 +70,10 @@ class SygusSymBreakNew
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  SygusSymBreakNew(TheoryDatatypes* td,
+  SygusExtension(TheoryDatatypes* td,
                    QuantifiersEngine* qe,
                    context::Context* c);
-  ~SygusSymBreakNew();
+  ~SygusExtension();
   /**
    * Notify this class that tester for constructor tindex has been asserted for
    * n. Exp is the literal corresponding to this tester. This method may add
@@ -571,7 +569,7 @@ private:
      */
     std::map< unsigned, Node > d_search_size_exp;
     /**
-     * For each size, whether we have called SygusSymBreakNew::notifySearchSize.
+     * For each size, whether we have called SygusExtension::notifySearchSize.
      */
     std::map< unsigned, bool > d_search_size;
     /**
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 8a34d8056..2d6aeae60 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -59,7 +59,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c,
       d_collectTermsCacheU(u),
       d_functionTerms(c),
       d_singleton_eq(u),
-      d_lemmas_produced_c(u)
+      d_lemmas_produced_c(u),
+      d_sygusExtension(nullptr)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -72,8 +73,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c,
   d_true = NodeManager::currentNM()->mkConst( true );
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
   d_dtfCounter = 0;
-
-  d_sygus_sym_break = NULL;
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -83,7 +82,6 @@ TheoryDatatypes::~TheoryDatatypes() {
     Assert(current != NULL);
     delete current;
   }
-  delete d_sygus_sym_break;
 }
 
 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -142,9 +140,9 @@ void TheoryDatatypes::check(Effort e) {
   d_addedLemma = false;
   
   if( e == EFFORT_LAST_CALL ){
-    Assert(d_sygus_sym_break);
+    Assert(d_sygusExtension != nullptr);
     std::vector< Node > lemmas;
-    d_sygus_sym_break->check( lemmas );
+    d_sygusExtension->check(lemmas);
     doSendLemmas( lemmas );
     return;
   }
@@ -376,7 +374,7 @@ void TheoryDatatypes::check(Effort e) {
 }
 
 bool TheoryDatatypes::needsCheckLastEffort() {
-  return d_sygus_sym_break!=NULL;
+  return d_sygusExtension != nullptr;
 }
 
 void TheoryDatatypes::flushPendingFacts(){
@@ -483,9 +481,10 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
   }
   doPendingMerges();
   // could be sygus-specific
-  if( d_sygus_sym_break ){
+  if (d_sygusExtension)
+  {
     std::vector< Node > lemmas;
-    d_sygus_sym_break->assertFact( atom, polarity, lemmas );
+    d_sygusExtension->assertFact(atom, polarity, lemmas);
     doSendLemmas( lemmas );
   }
   //add to tester if applicable
@@ -502,11 +501,12 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
     doPendingMerges();
     Trace("dt-tester") << "Done pending merges." << std::endl;
     if( !d_conflict && polarity ){
-      if( d_sygus_sym_break ){
+      if (d_sygusExtension)
+      {
         Trace("dt-tester") << "Assert tester to sygus : " << atom << std::endl;
         //Assert( !d_sygus_util->d_conflict );
         std::vector< Node > lemmas;
-        d_sygus_sym_break->assertTester( tindex, t_arg, atom, lemmas );
+        d_sygusExtension->assertTester(tindex, t_arg, atom, lemmas);
         Trace("dt-tester") << "Done assert tester to sygus." << std::endl;
         doSendLemmas( lemmas );
       }
@@ -532,9 +532,10 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
   default:
     // Function applications/predicates
     d_equalityEngine.addTerm(n);
-    if( d_sygus_sym_break ){
+    if (d_sygusExtension)
+    {
       std::vector< Node > lemmas;
-      d_sygus_sym_break->preRegisterTerm(n, lemmas);
+      d_sygusExtension->preRegisterTerm(n, lemmas);
       doSendLemmas( lemmas );
     }
     //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES);
@@ -545,8 +546,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
 
 void TheoryDatatypes::finishInit() {
   if( getQuantifiersEngine() && options::ceGuidedInst() ){
-    d_sygus_sym_break =
-        new SygusSymBreakNew(this, getQuantifiersEngine(), getSatContext());
+    d_sygusExtension.reset(
+        new SygusExtension(this, getQuantifiersEngine(), getSatContext()));
     // do congruence on evaluation functions
     d_equalityEngine.addFunctionKind(kind::DT_SYGUS_EVAL);
   }
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index e14a78df2..ba09ce89e 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -26,7 +26,7 @@
 #include "expr/attribute.h"
 #include "expr/datatype.h"
 #include "expr/node_trie.h"
-#include "theory/datatypes/datatypes_sygus.h"
+#include "theory/datatypes/sygus_extension.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "util/hash.h"
@@ -370,7 +370,7 @@ private:
   TNode getRepresentative( TNode a );
 private:
  /** sygus symmetry breaking utility */
- SygusSymBreakNew* d_sygus_sym_break;
+ std::unique_ptr<SygusExtension> d_sygusExtension;
 
 };/* class TheoryDatatypes */