(proof-new) Remove arith-snorm option. (#4591)

This option only marginally helped and will be difficult to support with the new proof infrastructure.

5 files changed, 2 insertions, 93 deletions

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index d16513cfb..0bfc26338 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -429,15 +429,6 @@ header = "options/arith_options.h"
   help       = "apply pseudo boolean rewrites"
 
 [[option]]
-  name       = "sNormInferEq"
-  category   = "regular"
-  long       = "snorm-infer-eq"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "infer equalities based on Shostak normalization"
-
-[[option]]
   name       = "nlExt"
   category   = "regular"
   long       = "nl-ext"
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 5a6bf6f31..6bfa2c705 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -21,7 +21,6 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/constraint.h"
-#include "theory/quantifiers/equality_infer.h"
 #include "options/arith_options.h"
 
 namespace CVC4 {
@@ -37,8 +36,6 @@ ArithCongruenceManager::ArithCongruenceManager(
     : d_inConflict(c),
       d_raiseConflict(raiseConflict),
       d_notify(*this),
-      d_eq_infer(),
-      d_eqi_counter(0, c),
       d_keepAlive(c),
       d_propagatations(c),
       d_explanationMap(c),
@@ -50,11 +47,6 @@ ArithCongruenceManager::ArithCongruenceManager(
   d_ee.addFunctionKind(kind::NONLINEAR_MULT);
   d_ee.addFunctionKind(kind::EXPONENTIAL);
   d_ee.addFunctionKind(kind::SINE);
-  //module to infer additional equalities based on normalization
-  if( options::sNormInferEq() ){
-    d_eq_infer.reset(new quantifiers::EqualityInference(c, true));
-    d_true = NodeManager::currentNM()->mkConst( true );
-  }
 }
 
 ArithCongruenceManager::~ArithCongruenceManager() {}
@@ -116,12 +108,10 @@ void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TN
   d_acm.propagate(t1.eqNode(t2));
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
-  d_acm.eqNotifyNewClass(t);
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPreMerge(TNode t1, TNode t2) {
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPostMerge(TNode t1, TNode t2) {
-  d_acm.eqNotifyPostMerge(t1,t2);
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 }
@@ -360,19 +350,6 @@ Node ArithCongruenceManager::explainInternal(TNode internal){
   }
 }
 
-void ArithCongruenceManager::eqNotifyNewClass(TNode t) {
-  if( d_eq_infer ){
-    d_eq_infer->eqNotifyNewClass(t);
-    fixpointInfer();
-  }
-}
-void ArithCongruenceManager::eqNotifyPostMerge(TNode t1, TNode t2) {
-  if( d_eq_infer ){
-    d_eq_infer->eqNotifyMerge(t1, t2);
-    fixpointInfer();
-  }
-}
-
 Node ArithCongruenceManager::explain(TNode external){
   Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
   Node internal = externalToInternal(external);
@@ -470,53 +447,6 @@ void ArithCongruenceManager::addSharedTerm(Node x){
   d_ee.addTriggerTerm(x, THEORY_ARITH);
 }
 
-bool ArithCongruenceManager::fixpointInfer() {
-  if( d_eq_infer ){
-    while(! inConflict() && d_eqi_counter.get()<d_eq_infer->getNumPendingMerges() ) {
-      Trace("snorm-infer-eq-debug") << "Processing " << d_eqi_counter.get() << " / " << d_eq_infer->getNumPendingMerges() << std::endl;
-      Node eq = d_eq_infer->getPendingMerge( d_eqi_counter.get() );
-      Trace("snorm-infer-eq") << "ArithCongruenceManager : Infer by normalization : " << eq << std::endl;
-      if( !d_ee.areEqual( eq[0], eq[1] ) ){
-        Node eq_exp = d_eq_infer->getPendingMergeExplanation( d_eqi_counter.get() );
-        Trace("snorm-infer-eq") << "           explanation : " << eq_exp << std::endl;
-        //regress explanation
-        std::vector<TNode> assumptions;
-        if( eq_exp.getKind()==kind::AND ){
-          for( unsigned i=0; i<eq_exp.getNumChildren(); i++ ){
-            explain( eq_exp[i], assumptions );
-          }
-        }else if( eq_exp.getKind()==kind::EQUAL ){
-          explain( eq_exp, assumptions );
-        }else{
-          //eq_exp should be true
-          Assert(eq_exp == d_true);
-        }
-        Node req_exp;
-        if( assumptions.empty() ){
-          req_exp = d_true;
-        }else{
-          std::set<TNode> assumptionSet;
-          assumptionSet.insert(assumptions.begin(), assumptions.end());
-          if( assumptionSet.size()==1 ){
-            req_exp = assumptions[0];
-          }else{
-            NodeBuilder<> conjunction(kind::AND);
-            enqueueIntoNB(assumptionSet, conjunction);
-            req_exp = conjunction;
-          }
-        }
-        Trace("snorm-infer-eq") << " regressed explanation : " << req_exp << std::endl;
-        d_ee.assertEquality( eq, true, req_exp );
-        d_keepAlive.push_back( req_exp );
-      }else{
-        Trace("snorm-infer-eq") << "...already equal." << std::endl;
-      }
-      d_eqi_counter = d_eqi_counter.get() + 1;
-    }
-  }
-  return inConflict();
-}
-
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index bccd2e943..837b7c07f 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -78,12 +78,6 @@ private:
   };
   ArithCongruenceNotify d_notify;
 
-  /** module for shostak normalization, d_eqi_counter is how many pending merges
-   * in d_eq_infer we have processed */
-  std::unique_ptr<quantifiers::EqualityInference> d_eq_infer;
-  context::CDO<unsigned> d_eqi_counter;
-  Node d_true;
-
   context::CDList<Node> d_keepAlive;
 
   /** Store the propagations. */
@@ -140,9 +134,6 @@ private:
   void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
 
   Node explainInternal(TNode internal);
-
-  void eqNotifyNewClass(TNode t);
-  void eqNotifyPostMerge(TNode t1, TNode t2);
 public:
 
   ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
@@ -176,9 +167,6 @@ public:
 
 
   void addSharedTerm(Node x);
-
-  /** process inferred equalities based on Shostak normalization */
-  bool fixpointInfer();
   
   eq::EqualityEngine * getEqualityEngine() { return &d_ee; }
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ea1021d89..69378a559 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1502,7 +1502,6 @@ set(regress_1_tests
   regress1/quantifiers/anti-sk-simp.smt2
   regress1/quantifiers/ari118-bv-2occ-x.smt2
   regress1/quantifiers/arith-rec-fun.smt2
-  regress1/quantifiers/arith-snorm.smt2
   regress1/quantifiers/array-unsat-simp3.smt2
   regress1/quantifiers/bi-artm-s.smt2
   regress1/quantifiers/bignum_quant.smt2
@@ -2420,6 +2419,8 @@ set(regression_disabled_tests
   regress1/nl/NAVIGATION2.smt2
   # sat or unknown in different builds
   regress1/nl/issue3307.smt2
+  # no longer support snorm option
+  regress1/quantifiers/arith-snorm.smt2
   # ajreynol: different error messages on production and debug:
   regress1/quantifiers/macro-subtype-param.smt2
   # times out with competition build:
diff --git a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2
index 21f26df2d..a4d04a8f4 100644
--- a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2
+++ b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2
@@ -1,7 +1,6 @@
 ; COMMAND-LINE: --quiet

 ; EXPECT: sat

 (set-logic QF_UFNRA)

-(set-option :snorm-infer-eq true)

 (set-info :status sat)

 (declare-const r0 Real)

 (declare-const r4 Real)