diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-11 12:45:16 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-11 12:45:16 +0000 |
| commit | e72fdcf6333d575e9c737a6274aa627dc9c54b47 (patch) | |
| tree | dcab5cfd03cb531201fd0c3d27d2c05dc6f42775 /src/theory/uf/theory_uf.h | |
| parent | 25e9c72dd689d3b621b901220794c652a3ba589a (diff) | |
adding disequality propagation
relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index d78504dc8..de8e70a49 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -103,6 +103,7 @@ public: { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); + d_equalityEngine.addFunctionKind(kind::EQUAL); // The boolean constants d_true = NodeManager::currentNM()->mkConst<bool>(true); |