From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 30 Jul 2019 15:21:01 +0000 (-0500)
Subject: Code to activate hoelim preprocessing pass (#3129)
X-Git-Tag: cvc5-1.0.0~4066
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5e3e9c156b20031a1b0e31489477b9b337d47cae;p=cvc5.git

Code to activate hoelim preprocessing pass (#3129)
---

diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 34bae1224..36b3c6392 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -34,6 +34,7 @@
 #include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/passes/extended_rewriter_pass.h"
 #include "preprocessing/passes/global_negate.h"
+#include "preprocessing/passes/ho_elim.h"
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/ite_removal.h"
 #include "preprocessing/passes/ite_simp.h"
@@ -148,6 +149,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("quantifier-macros", callCtor<QuantifierMacros>);
   registerPassInfo("nl-ext-purify", callCtor<NlExtPurify>);
   registerPassInfo("bool-to-bv", callCtor<BoolToBV>);
+  registerPassInfo("ho-elim", callCtor<HoElim>);
 }
 
 }  // namespace preprocessing
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 560cb0599..4a8803392 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1838,6 +1838,11 @@ void SmtEngine::setDefaults() {
     if( options::mbqiMode()!=quantifiers::MBQI_NONE ){
       options::mbqiMode.set( quantifiers::MBQI_NONE );
     }
+    if (!options::hoElimStoreAx.wasSetByUser())
+    {
+      // by default, use store axioms only if --ho-elim is set
+      options::hoElimStoreAx.set(options::hoElim());
+    }
   }
   if( options::fmfFunWellDefinedRelevant() ){
     if( !options::fmfFunWellDefined.wasSetByUser() ){
@@ -3488,6 +3493,11 @@ void SmtEnginePrivate::processAssertions() {
     d_passes["apply-to-const"]->apply(&d_assertions);
   }
 
+  if (options::ufHo())
+  {
+    d_passes["ho-elim"]->apply(&d_assertions);
+  }
+
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 #ifdef CVC4_ASSERTIONS