From: Andrew Reynolds Date: Thu, 11 Jun 2020 00:10:06 +0000 (-0500) Subject: (proof-new) Remove arith-snorm option. (#4591) X-Git-Tag: cvc5-1.0.0~3229 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f30f5dc342fa19b42842d744034f53a1dee3f43;p=cvc5.git (proof-new) Remove arith-snorm option. (#4591) This option only marginally helped and will be difficult to support with the new proof infrastructure. --- 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 @@ -428,15 +428,6 @@ header = "options/arith_options.h" read_only = true 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" 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()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 assumptions; - if( eq_exp.getKind()==kind::AND ){ - for( unsigned i=0; i 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 d_eq_infer; - context::CDO d_eqi_counter; - Node d_true; - context::CDList d_keepAlive; /** Store the propagations. */ @@ -140,9 +134,6 @@ private: void enqueueIntoNB(const std::set 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)