diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-12-17 13:43:44 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-17 13:43:44 -0800 |
| commit | e9499c41f405df8b42fd9ae10004b1b91a869106 (patch) | |
| tree | fa1475f43a3e61b8f6ffdcb903b65919eba28661 /src/theory/quantifiers/quant_conflict_find.cpp | |
| parent | 9b2914ed9f7b14ecf535ffe9e1328d0fa042e072 (diff) | |
Generate code for options with modes. (#3561)
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index de46eee74..89f4f2989 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -17,6 +17,7 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" +#include "options/theory_options.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" @@ -652,7 +653,9 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { } //check if it is entailed Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl; - std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew ); + std::pair<bool, Node> et = + p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck( + options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew); ++(p->d_statistics.d_entailment_checks); Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl; if( !et.first ){ @@ -1901,11 +1904,11 @@ bool QuantConflictFind::needsCheck( Theory::Effort level ) { bool performCheck = false; if( options::quantConflictFind() && !d_conflict ){ if( level==Theory::EFFORT_LAST_CALL ){ - performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL; + performCheck = options::qcfWhenMode() == options::QcfWhenMode::LAST_CALL; }else if( level==Theory::EFFORT_FULL ){ - performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT; + performCheck = options::qcfWhenMode() == options::QcfWhenMode::DEFAULT; }else if( level==Theory::EFFORT_STANDARD ){ - performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD; + performCheck = options::qcfWhenMode() == options::QcfWhenMode::STD; } } return performCheck; @@ -1956,8 +1959,9 @@ inline QuantConflictFind::Effort QcfEffortStart() { // Returns the beginning of a range of efforts. The value returned is included // in the range. inline QuantConflictFind::Effort QcfEffortEnd() { - return options::qcfMode() == QCF_PROP_EQ ? QuantConflictFind::EFFORT_PROP_EQ - : QuantConflictFind::EFFORT_CONFLICT; + return options::qcfMode() == options::QcfMode::PROP_EQ + ? QuantConflictFind::EFFORT_PROP_EQ + : QuantConflictFind::EFFORT_CONFLICT; } } // namespace |