Improvements to equality inference module: add missing cases for solvable variables, do not infer equalities that are derivable by transitivity of other inferred equalities, refactor solved vars/eqc into one, option to track explanations. Handle case when equality inference in quantifiers can derive purely arithmetic ground conflicts at full effort.

1 files changed, 6 insertions, 6 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index eb92b0f70..5344c0e88 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -33,16 +33,16 @@ bool QuantArith::getMonomial( Node n, Node& c, Node& v ){
   }
 }
 bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) {
-  if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
-    if( msum.find(n[1])==msum.end() ){
-      msum[n[1]] = n[0];
-      return true;
-    }
-  }else if( n.isConst() ){
+  if( n.isConst() ){
     if( msum.find(Node::null())==msum.end() ){
       msum[Node::null()] = n;
       return true;
     }
+  }else if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
+    if( msum.find(n[1])==msum.end() ){
+      msum[n[1]] = n[0];
+      return true;
+    }
   }else{
     if( msum.find(n)==msum.end() ){
       msum[n] = Node::null();