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/preprocessing/passes/quantifier_macros.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/preprocessing/passes/quantifier_macros.cpp')
-rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 1d834ce60..bc2c136e4 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -18,7 +18,6 @@ #include <vector> -#include "options/quantifiers_modes.h" #include "options/quantifiers_options.h" #include "proof/proof_manager.h" #include "smt/smt_engine.h" @@ -70,7 +69,8 @@ void QuantifierMacros::clearMaps() } bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ - unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; + unsigned rmax = + options::macrosQuantMode() == options::MacrosQuantMode::ALL ? 2 : 1; for( unsigned r=0; r<rmax; r++ ){ d_ground_macros = (r==0); Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl; @@ -365,7 +365,10 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod if( !containsBadOp( n_def, op, opc, visited ) ){ Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl; //must be ground UF term if mode is GROUND_UF - if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){ + if (options::macrosQuantMode() + != options::MacrosQuantMode::GROUND_UF + || isGroundUfTerm(f, n_def)) + { Trace("macros-debug") << "...respects ground-uf constraint." << std::endl; //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where // x1 ... xn are distinct variables |