From eaca3c11b3c2546f6ee0f840eae8e86c9d1d55ec Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 31 Oct 2019 23:37:16 -0500 Subject: [PATCH] Rename datatypes sygus solver (#3417) --- src/CMakeLists.txt | 4 +- ...atatypes_sygus.cpp => sygus_extension.cpp} | 91 +++++++++---------- .../{datatypes_sygus.h => sygus_extension.h} | 20 ++-- src/theory/datatypes/theory_datatypes.cpp | 31 ++++--- src/theory/datatypes/theory_datatypes.h | 4 +- 5 files changed, 74 insertions(+), 76 deletions(-) rename src/theory/datatypes/{datatypes_sygus.cpp => sygus_extension.cpp} (95%) rename src/theory/datatypes/{datatypes_sygus.h => sygus_extension.h} (98%) 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 similarity index 95% rename from src/theory/datatypes/datatypes_sygus.cpp rename to 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::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 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::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& lemmas) +void SygusExtension::registerSizeTerm(Node e, std::vector& lemmas) { if (d_register_st.find(e) != d_register_st.end()) { @@ -1385,7 +1384,7 @@ void SygusSymBreakNew::registerSizeTerm(Node e, std::vector& lemmas) } } -void SygusSymBreakNew::registerMeasureTerm( Node m ) { +void SygusExtension::registerMeasureTerm( Node m ) { std::map>::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>::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::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>::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>::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 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& 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& 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& 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 similarity index 98% rename from src/theory/datatypes/datatypes_sygus.h rename to 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 #include @@ -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 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 d_sygusExtension; };/* class TheoryDatatypes */ -- 2.30.2