From 5bc200446b4165814db47e6e3639972af31ad0a6 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 31 Oct 2015 10:00:52 +0100
Subject: Improvements to handling of mixed Int/Real quantifiers.

---
 src/theory/quantifiers/quant_util.cpp | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'src/theory/quantifiers/quant_util.cpp')

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 026293e02..0b212d696 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -137,6 +137,24 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
   return 0;
 }
 
+int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
+  Node vatom;
+  //isolate pv in the inequality
+  int ires = isolate( v, msum, vatom, k, true );
+  if( ires!=0 ){
+    val = vatom[ ires==1 ? 1 : 0 ];
+    Node pvm = vatom[ ires==1 ? 0 : 1 ];
+    //get monomial
+    if( pvm!=v ){
+      Node veq_v;
+      if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
+        Assert( veq_v==v );
+      }
+    }
+  }
+  return ires;
+}
+
 Node QuantArith::negate( Node t ) {
   Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
   tt = Rewriter::rewrite( tt );
-- 
cgit v1.2.3