diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-31 14:36:25 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-31 14:36:25 -0500 |
commit | ccc9cd5aad5248b4a2c86b617d76bc98063a7ea2 (patch) | |
tree | cd710b7174eb3724d1b08c3261f69c7e4745a4d0 /src/theory/quantifiers/equality_infer.cpp | |
parent | 2abcda1cfcb0c6388c00d65f8a6b3e63de9d96df (diff) |
Improvements to trigger selection, min triggers by default. Optimizations for E-matching. Minor work to equality infer.
Diffstat (limited to 'src/theory/quantifiers/equality_infer.cpp')
-rw-r--r-- | src/theory/quantifiers/equality_infer.cpp | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index fc3a274ac..f1dbb32fa 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -26,11 +26,12 @@ using namespace std; namespace CVC4 { -EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ) { +EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ), d_rep_exp(c) { } -EqualityInference::EqualityInference( context::Context* c ) : d_c( c ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ){ +EqualityInference::EqualityInference( context::Context* c, bool trackExp ) : +d_c( c ), d_trackExplain( trackExp ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ), d_pending_merge_exp( c ){ d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); } @@ -127,6 +128,10 @@ void EqualityInference::setEqcRep( Node t, Node r, EqcInfo * eqci ) { Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl; Trace("eq-infer") << " since they both normalize to : " << r << std::endl; d_pending_merges.push_back( t.eqNode( t2 ) ); + if( d_trackExplain ){ + //TODO + d_pending_merge_exp.push_back( t.eqNode( t2 ) ); + } } } } @@ -232,4 +237,9 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { } } +Node EqualityInference::getPendingMergeExplanation( unsigned i ) { + Assert( d_trackExplain ); + return d_pending_merge_exp[i]; +} + } |