Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 27371eac3..388c0edf0 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -41,6 +41,7 @@
 #include "util/hash.h"
 #include "util/cache.h"
 #include "util/cvc4_assert.h"
+#include "util/sort_inference.h"
 #include "theory/ite_simplifier.h"
 #include "theory/unconstrained_simplifier.h"
 #include "theory/uf/equality_engine.h"
@@ -422,6 +423,9 @@ class TheoryEngine {
 
   RemoveITE& d_iteRemover;
 
+  /** sort inference module */
+  SortInference d_sortInfer;
+
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
 
@@ -732,6 +736,7 @@ public:
 
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
 
+  SortInference* getSortInference() { return &d_sortInfer; }
 private:
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 public: