diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-02 12:01:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-02 12:01:27 -0500 |
commit | daeab65ac6c6715a3e0c2f6fc0e61b1a7925b932 (patch) | |
tree | 43b2604fa62cc67d15bc8afdfe74f956fb6cc174 /src/theory/quantifiers/instantiate.cpp | |
parent | 613bf2cc56a80af66f2cad9e55374136c5a346f8 (diff) |
Throw option exception when track inst lemmas is not used (#3145)
Diffstat (limited to 'src/theory/quantifiers/instantiate.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 50 |
1 files changed, 27 insertions, 23 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 8bd39c241..7ecf9866a 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -644,42 +644,46 @@ void Instantiate::getExplanationForInstLemmas( std::map<Node, Node>& quant, std::map<Node, std::vector<Node> >& tvec) { - if (options::trackInstLemmas()) + if (!options::trackInstLemmas()) { - if (options::incrementalSolving()) + std::stringstream msg; + msg << "Cannot get explanation for instantiations when --track-inst-lemmas " + "is false."; + throw OptionException(msg.str()); + } + if (options::incrementalSolving()) + { + for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie) { - for (std::pair<const Node, inst::CDInstMatchTrie*>& t : - d_c_inst_match_trie) - { - t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec); - } + t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec); } - else + } + else + { + for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie) { - for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie) - { - t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec); - } + t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec); } + } #ifdef CVC4_ASSERTIONS - for (unsigned j = 0; j < lems.size(); j++) - { - Assert(quant.find(lems[j]) != quant.end()); - Assert(tvec.find(lems[j]) != tvec.end()); - } -#endif + for (unsigned j = 0; j < lems.size(); j++) + { + Assert(quant.find(lems[j]) != quant.end()); + Assert(tvec.find(lems[j]) != tvec.end()); } - Assert(false); +#endif } void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts) { - bool useUnsatCore = false; - std::vector<Node> active_lemmas; - if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas)) + if (!options::trackInstLemmas()) { - useUnsatCore = true; + std::stringstream msg; + msg << "Cannot get instantiations when --track-inst-lemmas is false."; + throw OptionException(msg.str()); } + std::vector<Node> active_lemmas; + bool useUnsatCore = getUnsatCoreLemmas(active_lemmas); if (options::incrementalSolving()) { |