diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-09 15:35:40 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-09 15:35:40 -0600 |
| commit | 531f325f9f4757f68089e9600868133f7fe610f7 (patch) | |
| tree | 55cbac83898352c22b67659224eb1d20f3f38f70 /src/theory/quantifiers_engine.cpp | |
| parent | e302b6b1664d3a28c3f42de911f3c13e7b5d0605 (diff) | |
Make term database optionally SAT-context-dependent (#5877)
This makes the terms registered to the term database (those considered by E-matching) optionally stored in a SAT-context-dependent manner. The motivation is to have a more flexible/fine-grained set of terms considered by E-matching, e.g. if preregistration becomes lazier in the future.
This uncovered 2 issues:
The induction techniques in "conjecture generator" were using private interfaces, this PR removes the friend relaionship and cleans the code
The conflict-based instantiation module was accessing the signature tables for BOUND_VARIABLES when an operator of an APPLY_UF was a BOUND_VARIABLE. This is possible when options::ufHo is enabled. This makes conflict-based instantiation skip such terms.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index bdc12cdaa..33ec3cbf8 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -263,7 +263,8 @@ void QuantifiersEngine::presolve() { d_term_db->presolve(); d_presolve = false; //add all terms to database - if( options::incrementalSolving() ){ + if (options::incrementalSolving() && !options::termDbCd()) + { Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl; for (const Node& t : d_presolve_cache) { @@ -762,14 +763,16 @@ void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant) { return; } - if( options::incrementalSolving() ){ + if (options::incrementalSolving() && !options::termDbCd()) + { if( d_presolve_in.find( n )==d_presolve_in.end() ){ d_presolve_in.insert( n ); d_presolve_cache.push_back( n ); } } //only wait if we are doing incremental solving - if( !d_presolve || !options::incrementalSolving() ){ + if (!d_presolve || !options::incrementalSolving() || options::termDbCd()) + { d_term_db->addTerm(n); if (d_sygus_tdb && options::sygusEvalUnfold()) { |