diff options
Diffstat (limited to 'src/theory/rewriterules')
| -rw-r--r-- | src/theory/rewriterules/options | 14 | ||||
| -rw-r--r-- | src/theory/rewriterules/theory_rewriterules.cpp | 6 | ||||
| -rw-r--r-- | src/theory/rewriterules/theory_rewriterules_rules.cpp | 6 |
3 files changed, 20 insertions, 6 deletions
diff --git a/src/theory/rewriterules/options b/src/theory/rewriterules/options new file mode 100644 index 000000000..285e489be --- /dev/null +++ b/src/theory/rewriterules/options @@ -0,0 +1,14 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module REWRITE_RULES "theory/rewriterules/options.h" Rewrite Rules + +option efficientEMatching --efficient-e-matching bool :default false + use efficient E-matching (only for rewrite rules) + +option rewriteRulesAsAxioms --rewrite-rules-as-axioms bool :default false + whether to convert rewrite rules to usual axioms (for debugging only) + +endmodule diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 57bc6d9cf..b4ae93653 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -23,7 +23,7 @@ #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriter.h" -#include "util/options.h" +#include "theory/rewriterules/options.h" using namespace std; @@ -292,13 +292,13 @@ Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector<Node> & pattern // Debug("rewriterules") << "createTrigger:"; getQuantifiersEngine()->registerPattern(pattern); return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern, - Options::current()->efficientEMatching? + options::efficientEMatching()? Trigger::MATCH_GEN_EFFICIENT_E_MATCH : Trigger::MATCH_GEN_DEFAULT, true, Trigger::TR_MAKE_NEW, false); - // Options::current()->smartMultiTriggers); + // options::smartMultiTriggers()); }; bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested, diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index 1ad8fdaa7..edea7a3c0 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -21,7 +21,7 @@ #include "theory/rewriterules/theory_rewriterules_params.h" #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriterules/theory_rewriterules.h" -#include "util/options.h" +#include "theory/rewriterules/options.h" #include "theory/quantifiers/term_database.h" @@ -110,7 +110,7 @@ inline void addPattern(TheoryRewriteRules & re, if (tri.getKind() == kind::NOT && tri[0].getKind() == kind::APPLY_UF) tri = tri[0]; pattern.push_back( - Options::current()->rewriteRulesAsAxioms? + options::rewriteRulesAsAxioms()? static_cast<Node>(tri): re.getQuantifiersEngine()->getTermDatabase()-> convertNodeToPattern(tri,r,vars,inst_constants)); @@ -224,7 +224,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r) //If we convert to usual axioms - if(Options::current()->rewriteRulesAsAxioms){ + if(options::rewriteRulesAsAxioms()){ NodeBuilder<> forallB(kind::FORALL); forallB << r[0]; NodeBuilder<> guardsB(kind::AND); |