diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-10 19:10:06 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-10 19:10:06 -0500 |
commit | 2f30f5dc342fa19b42842d744034f53a1dee3f43 (patch) | |
tree | 10aa6d491a8d337bbbda3af456b96f0ed989bfb0 /src/theory | |
parent | 356647c4b7eb2420f6c6b350f0622bb4c863b0a5 (diff) |
(proof-new) Remove arith-snorm option. (#4591)
This option only marginally helped and will be difficult to support with the new proof infrastructure.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 70 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.h | 12 |
2 files changed, 0 insertions, 82 deletions
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; } |