diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-27 09:27:19 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-27 09:27:29 -0500 |
| commit | e277b4d220a1d15ac32f6e4fc5f06e88f55b7f68 (patch) | |
| tree | 2a56691dea81453e5f9ba42e859fdc6783fa1545 /src/theory/quantifiers_engine.cpp | |
| parent | ccd1ca4c32e8a3eac8b18911a7b2d32b55203707 (diff) | |
Add new symmetry breaking technique for finite model finding. Improvements to bounded integer quantifier instantiation.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rwxr-xr-x[-rw-r--r--] | src/theory/quantifiers_engine.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e5cc8a1fb..0fe50aad6 100644..100755 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -29,6 +29,7 @@ #include "theory/rewriterules/rr_trigger.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/rewrite_engine.h" +#include "theory/uf/options.h" using namespace std; using namespace CVC4; @@ -632,6 +633,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, }else{ int sortId = 0; if( optInternalRepSortInference() ){ + //if( options::ufssSymBreak() ){ sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] ); } if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){ |