diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-09 22:18:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-09 20:18:58 -0700 |
| commit | 0e09af0be57ec4df28869e4383a40d847c0a6b5a (patch) | |
| tree | 659be92f761f174f6690bd16d1d2e6b0f2301999 /src/theory | |
| parent | 3ebc297e6ff589f7b98519cd2aa23963a4e06652 (diff) | |
Rename sygus option name (#3977)
This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach).
It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 7 |
2 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index fc8dedbd3..d202648f4 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -548,7 +548,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { } void TheoryDatatypes::finishInit() { - if( getQuantifiersEngine() && options::ceGuidedInst() ){ + if (getQuantifiersEngine() && options::sygus()) + { d_sygusExtension.reset( new SygusExtension(this, getQuantifiersEngine(), getSatContext())); // do congruence on evaluation functions diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index b3ee7ad49..f6c17ebf9 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -124,7 +124,7 @@ class QuantifiersEnginePrivate modules.push_back(d_i_cbqi.get()); qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } - if (options::ceGuidedInst()) + if (options::sygus()) { d_synth_e.reset(new quantifiers::SynthEngine(qe, c)); modules.push_back(d_synth_e.get()); @@ -212,7 +212,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_util.push_back(d_term_util.get()); d_util.push_back(d_term_db.get()); - if (options::ceGuidedInst()) { + if (options::sygus()) + { d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this)); } @@ -499,7 +500,7 @@ void QuantifiersEngine::ppNotifyAssertions( theory_sep->initializeBounds(); d_qepr->finishInit(); } - if (options::ceGuidedInst()) + if (options::sygus()) { quantifiers::SynthEngine* sye = d_private->d_synth_e.get(); for (const Node& a : assertions) |