From f7559c879d1ebc7d4d9b9f72b0858bdf42c9ed8c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 16 Jul 2020 12:10:58 -0500 Subject: Make ExtTheory a utility and not a member of Theory (#4753) Previously, we assumed that ExtTheory, the module for doing context-dependent simplification, was one-to-one with Theory. This design is not necessary. This makes this class a utility, which can be used as needed. This makes e.g. the initialization of TheoryStrings much easier, since the ExtTheory object can be created first. --- src/theory/arith/theory_arith.cpp | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'src/theory/arith/theory_arith.cpp') diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index eb5bf3685..fcbfd1baf 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -44,16 +44,6 @@ TheoryArith::TheoryArith(context::Context* c, d_proofRecorder(nullptr) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); - // if logic is non-linear - if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) - { - setupExtTheory(); - getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT); - getExtTheory()->addFunctionKind(kind::EXPONENTIAL); - getExtTheory()->addFunctionKind(kind::SINE); - getExtTheory()->addFunctionKind(kind::PI); - getExtTheory()->addFunctionKind(kind::IAND); - } } TheoryArith::~TheoryArith(){ -- cgit v1.2.3