diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-01 21:37:03 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-02 03:37:03 +0000 |
| commit | 4132e91fdb2f8912a89a101e96c86bf5076b327a (patch) | |
| tree | 9d773b3a36aa68bda3d7b7839d9d8cd72a4061ef /src/theory/quantifiers/sygus | |
| parent | b5073e16ea49ce9214fcc5318ce080724719c809 (diff) | |
Introduce quantifiers term registry (#5983)
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 6 |
2 files changed, 3 insertions, 13 deletions
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index f393601ad..275e9a27f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -21,14 +21,11 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" -#include "theory/arith/arith_msum.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace CVC4::kind; @@ -49,11 +46,8 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r) return os; } -TermDbSygus::TermDbSygus(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : d_quantEngine(qe), - d_qstate(qs), +TermDbSygus::TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim) + : d_qstate(qs), d_qim(qim), d_syexp(new SygusExplain(this)), d_ext_rw(new ExtendedRewriter(true)), diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index ba09c723f..013922c94 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -54,9 +54,7 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r); // TODO :issue #1235 split and document this class class TermDbSygus { public: - TermDbSygus(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantifiersInferenceManager& qim); + TermDbSygus(QuantifiersState& qs, QuantifiersInferenceManager& qim); ~TermDbSygus() {} /** Reset this utility */ bool reset(Theory::Effort e); @@ -316,8 +314,6 @@ class TermDbSygus { static void toStreamSygus(std::ostream& out, Node n); private: - /** reference to the quantifiers engine */ - QuantifiersEngine* d_quantEngine; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; /** The quantifiers inference manager */ |