diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-02-24 16:37:46 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-02-24 16:37:46 -0600 |
commit | c71ec272d5ef58bfa147507bdbb370f2e288d154 (patch) | |
tree | 8bf3b84a476fa7fff798158e6b58697399c7b966 /src/theory/quantifiers/inst_match.cpp | |
parent | deb304550fbb6e19346319ec24d83e0650c64e91 (diff) |
added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index dcd7a1b79..85a96f90a 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -103,12 +103,12 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ } } -void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){ - EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery(); - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - d_map[ it->first ] = eqqe->getInternalRepresentative( it->second ); - } -} +//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){ +// EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery(); +// for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ +// d_map[ it->first ] = eqqe->getInternalRepresentative( it->second ); +// } +//} void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ |