diff options
Diffstat (limited to 'src')
33 files changed, 135 insertions, 22 deletions
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 683716410..b08f69b50 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -687,8 +687,9 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( return ret; } -BVGauss::BVGauss(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "bv-gauss") +BVGauss::BVGauss(PreprocessingPassContext* preprocContext, + const std::string& name) + : PreprocessingPass(preprocContext, name) { } diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index 93d61be9e..7fb23814a 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -30,7 +30,8 @@ namespace passes { class BVGauss : public PreprocessingPass { public: - BVGauss(PreprocessingPassContext* preprocContext); + BVGauss(PreprocessingPassContext* preprocContext, + const std::string& name = "bv-gauss"); protected: /** diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 8986e6894..2c748f188 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -19,6 +19,7 @@ #include "options/smt_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/arith/arith_rewriter.h" #include "theory/arith/infer_bounds.h" #include "theory/arith/theory_arith_private.h" #include "theory/ext_theory.h" @@ -53,6 +54,11 @@ TheoryArith::~TheoryArith(){ delete d_internal; } +std::unique_ptr<TheoryRewriter> TheoryArith::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new ArithRewriter()); +} + void TheoryArith::preRegisterTerm(TNode n){ d_internal->preRegisterTerm(n); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index b39ab961f..92892d2ae 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -51,6 +51,8 @@ public: Valuation valuation, const LogicInfo& logicInfo); virtual ~TheoryArith(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + /** * Does non-context dependent setup for a node connected to a theory. */ diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index dcf82e6b4..787ae84e2 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -29,6 +29,7 @@ #include "smt/command.h" #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" +#include "theory/arrays/theory_arrays_rewriter.h" #include "theory/rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" @@ -178,6 +179,11 @@ TheoryArrays::~TheoryArrays() { smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts); } +std::unique_ptr<TheoryRewriter> TheoryArrays::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheoryArraysRewriter()); +} + void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 3d6d0692e..d1f912d95 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -144,6 +144,8 @@ class TheoryArrays : public Theory { std::string name = ""); ~TheoryArrays(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; std::string identify() const override { return std::string("TheoryArrays"); } diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 8fbe83951..e670121d1 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -14,15 +14,17 @@ ** The theory of booleans. **/ -#include "theory/theory.h" #include "theory/booleans/theory_bool.h" -#include "theory/booleans/circuit_propagator.h" -#include "theory/valuation.h" -#include "smt_util/boolean_simplification.h" -#include "theory/substitutions.h" -#include <vector> #include <stack> +#include <vector> + +#include "smt_util/boolean_simplification.h" +#include "theory/booleans/circuit_propagator.h" +#include "theory/booleans/theory_bool_rewriter.h" +#include "theory/substitutions.h" +#include "theory/theory.h" +#include "theory/valuation.h" #include "util/hash.h" using namespace std; @@ -31,6 +33,11 @@ namespace CVC4 { namespace theory { namespace booleans { +std::unique_ptr<TheoryRewriter> TheoryBool::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheoryBoolRewriter()); +} + Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) { diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index abe024282..75e375ee6 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -33,6 +33,8 @@ public: : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) {} + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; //void check(Effort); diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 505aa503f..8df5a8535 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -17,6 +17,7 @@ #include "theory/builtin/theory_builtin.h" #include "expr/kind.h" +#include "theory/builtin/theory_builtin_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" @@ -35,6 +36,11 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c, { } +std::unique_ptr<TheoryRewriter> TheoryBuiltin::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheoryBuiltinRewriter()); +} + std::string TheoryBuiltin::identify() const { return std::string("TheoryBuiltin"); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 6e99ef040..d240f4f63 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -34,6 +34,8 @@ class TheoryBuiltin : public Theory Valuation valuation, const LogicInfo& logicInfo); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + std::string identify() const override; /** finish initialization */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 94fc1e34c..27718b63f 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -112,6 +112,11 @@ TheoryBV::TheoryBV(context::Context* c, TheoryBV::~TheoryBV() {} +std::unique_ptr<TheoryRewriter> TheoryBV::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheoryBVRewriter()); +} + void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { if (options::bitblastMode() == options::BitblastMode::EAGER) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 196535a19..ff1c9245a 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -72,6 +72,8 @@ public: ~TheoryBV(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; void finishInit() override; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 7fbe5bc68..15220b9dc 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -25,6 +25,7 @@ #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers_engine.h" @@ -85,6 +86,11 @@ TheoryDatatypes::~TheoryDatatypes() { } } +std::unique_ptr<TheoryRewriter> TheoryDatatypes::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new DatatypesRewriter()); +} + void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index a878647bc..7ccd04f39 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -271,6 +271,8 @@ private: const LogicInfo& logicInfo); ~TheoryDatatypes(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; /** propagate */ diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 2632a6f38..5ab285766 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -15,18 +15,18 @@ ** \todo document this file **/ - -#include "options/fp_options.h" -#include "theory/rewriter.h" -#include "theory/theory_model.h" #include "theory/fp/theory_fp.h" - #include <set> #include <stack> #include <unordered_set> #include <vector> +#include "options/fp_options.h" +#include "theory/fp/theory_fp_rewriter.h" +#include "theory/rewriter.h" +#include "theory/theory_model.h" + using namespace std; namespace CVC4 { @@ -177,6 +177,11 @@ TheoryFp::TheoryFp(context::Context *c, } /* TheoryFp::TheoryFp() */ +std::unique_ptr<TheoryRewriter> TheoryFp::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheoryFpRewriter()); +} + Node TheoryFp::minUF(Node node) { Assert(node.getKind() == kind::FLOATINGPOINT_MIN); TypeNode t(node.getType()); diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index ad093f924..802a70435 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -38,6 +38,8 @@ class TheoryFp : public Theory { TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + Node expandDefinition(LogicRequest& lr, Node node) override; void preRegisterTerm(TNode node) override; diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index dd5abd219..3c27f1b53 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -37,7 +37,6 @@ me=$(basename "$0") template=$1; shift rewriter_includes= -rewrite_init= pre_rewrite_get_cache= pre_rewrite_set_cache= @@ -140,8 +139,6 @@ function rewriter { rewriter_includes="${rewriter_includes}#include \"$header\" " - rewrite_init="${rewrite_init} d_theoryRewriters[${theory_id}].reset(new ${class}); -" pre_rewrite_attribute_ids="${pre_rewrite_attribute_ids} preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::pre_rewrite())); " post_rewrite_attribute_ids="${post_rewrite_attribute_ids} postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::post_rewrite())); @@ -257,7 +254,6 @@ for var in \ post_rewrite_get_cache \ pre_rewrite_set_cache \ post_rewrite_set_cache \ - rewrite_init \ pre_rewrite_attribute_ids \ post_rewrite_attribute_ids \ template \ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 227f4d5b5..e3e3c3824 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/ematching/instantiation_engine.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -53,6 +54,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output TheoryQuantifiers::~TheoryQuantifiers() { } +std::unique_ptr<TheoryRewriter> TheoryQuantifiers::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new QuantifiersRewriter()); +} + void TheoryQuantifiers::finishInit() { // quantifiers are not evaluated in getModelValue diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index b5b07f2e6..7efe7419c 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -39,6 +39,8 @@ class TheoryQuantifiers : public Theory { const LogicInfo& logicInfo); ~TheoryQuantifiers(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + /** finish initialization */ void finishInit() override; void preRegisterTerm(TNode n) override; diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index b3f1e23d7..54b9f319d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -96,6 +96,12 @@ Node Rewriter::rewrite(TNode node) { return getInstance().rewriteTo(theoryOf(node), node); } +void Rewriter::registerTheoryRewriter(theory::TheoryId tid, + std::unique_ptr<TheoryRewriter> trew) +{ + getInstance().d_theoryRewriters[tid] = std::move(trew); +} + void Rewriter::registerPreRewrite( Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn) { diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index f7298e1fb..8a641743b 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -63,6 +63,16 @@ class Rewriter { static void clearCaches(); /** + * Registers a theory rewriter with this rewriter. This transfers the + * ownership of the theory rewriter to the rewriter. + * + * @param tid The theory that the theory rewriter should be associated with. + * @param trew The theory rewriter to register. + */ + static void registerTheoryRewriter(theory::TheoryId tid, + std::unique_ptr<TheoryRewriter> trew); + + /** * Register a prerewrite for a given kind. * * @param k The kind to register a rewrite for. diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 1bb03e253..9f6b07389 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -63,8 +63,6 @@ ${post_rewrite_set_cache} Rewriter::Rewriter() { -${rewrite_init} - for (size_t i = 0; i < kind::LAST_KIND; ++i) { d_preRewriters[i] = nullptr; @@ -75,7 +73,6 @@ for (size_t i = 0; i < theory::THEORY_LAST; ++i) { d_preRewritersEqual[i] = nullptr; d_postRewritersEqual[i] = nullptr; - d_theoryRewriters[i]->registerRewrites(this); } } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 0b6e7a5fb..1d0ad904c 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -29,6 +29,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" +#include "theory/sep/theory_sep_rewriter.h" #include "theory/theory_model.h" #include "theory/valuation.h" @@ -64,6 +65,11 @@ TheorySep::~TheorySep() { } } +std::unique_ptr<TheoryRewriter> TheorySep::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheorySepRewriter()); +} + void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index ae044f6d7..df3294882 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -66,6 +66,8 @@ class TheorySep : public Theory { TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheorySep(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; std::string identify() const override { return std::string("TheorySep"); } diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 3b0427ec5..0b9e6d934 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -15,8 +15,10 @@ **/ #include "theory/sets/theory_sets.h" + #include "options/sets_options.h" #include "theory/sets/theory_sets_private.h" +#include "theory/sets/theory_sets_rewriter.h" #include "theory/theory_model.h" using namespace CVC4::kind; @@ -44,6 +46,11 @@ TheorySets::~TheorySets() // Do not move me to the header. See explanation in the constructor. } +std::unique_ptr<TheoryRewriter> TheorySets::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheorySetsRewriter()); +} + void TheorySets::finishInit() { TheoryModel* tm = d_valuation.getModel(); diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index ed2459b32..a55a22600 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -42,6 +42,8 @@ class TheorySets : public Theory const LogicInfo& logicInfo); ~TheorySets() override; + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + /** finish initialization */ void finishInit() override; void addSharedTerm(TNode) override; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a81c96318..f9eeb2010 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -26,6 +26,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/ext_theory.h" #include "theory/rewriter.h" +#include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/type_enumerator.h" #include "theory/strings/word.h" @@ -129,6 +130,11 @@ TheoryStrings::~TheoryStrings() { } +std::unique_ptr<TheoryRewriter> TheoryStrings::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new SequencesRewriter()); +} + bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { Assert(d_equalityEngine.hasTerm(x)); Assert(d_equalityEngine.hasTerm(y)); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 76c8f0469..0e95628bc 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -109,6 +109,8 @@ class TheoryStrings : public Theory { const LogicInfo& logicInfo); ~TheoryStrings(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; std::string identify() const override { return std::string("TheoryStrings"); } diff --git a/src/theory/theory.h b/src/theory/theory.h index d6b02e070..63ca46b41 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -42,6 +42,7 @@ #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/theory_id.h" +#include "theory/theory_rewriter.h" #include "theory/valuation.h" #include "util/statistics_registry.h" @@ -317,6 +318,11 @@ public: virtual ~Theory(); /** + * Creates a new theory rewriter for the theory. + */ + virtual std::unique_ptr<TheoryRewriter> mkTheoryRewriter() = 0; + + /** * Subclasses of Theory may add additional efforts. DO NOT CHECK * equality with one of these values (e.g. if STANDARD xxx) but * rather use range checks (or use the helper functions below). diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e665f6115..2c27c6054 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -266,7 +266,6 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, } void TheoryEngine::finishInit() { - //initialize the quantifiers engine, master equality engine, model, model builder if( d_logicInfo.isQuantified() ) { // initialize the quantifiers engine diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 840d42417..dec654e76 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -494,6 +494,8 @@ class TheoryEngine { *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo); + theory::Rewriter::registerTheoryRewriter( + theoryId, d_theoryTable[theoryId]->mkTheoryRewriter()); } void setPropEngine(prop::PropEngine* propEngine) diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3b42fa6a1..1ea5449b7 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -66,6 +66,11 @@ TheoryUF::TheoryUF(context::Context* c, TheoryUF::~TheoryUF() { } +std::unique_ptr<TheoryRewriter> TheoryUF::mkTheoryRewriter() +{ + return std::unique_ptr<TheoryRewriter>(new TheoryUfRewriter()); +} + void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 93a709fe5..623c5c64b 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -188,6 +188,8 @@ private: ~TheoryUF(); + std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; void finishInit() override; |