From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Mar 2017 15:58:03 +0000 (-0500)
Subject: Minor fix for bounded integers.
X-Git-Tag: cvc5-1.0.0~5877
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=478251bcea8c25596eaab1664ac18c7ddd15c445;p=cvc5.git

Minor fix for bounded integers.
---

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 6b53612d7..3d5066c08 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -797,6 +797,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
       Node l, u;
       getBoundValues( q, v, rsi, l, u );
       if( l.isNull() || u.isNull() ){
+        Trace("bound-int-warn") << "WARNING: Could not find integer bounds in model for " << v << " in " << q << std::endl;
         //failed, abort the iterator
         return false;
       }else{
@@ -824,6 +825,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
     }else if( bvt==BOUND_SET_MEMBER  ){ 
       Node srv = getSetRangeValue( q, v, rsi );
       if( srv.isNull() ){
+        Trace("bound-int-warn") << "WARNING: Could not find set bound in model for " << v << " in " << q << std::endl;
         return false;
       }else{
         Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 88b5f5fb1..b1cc9ed19 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -70,6 +70,7 @@ Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) {
   }
 }
 
+//AJR : FIXME : this function is only used by bounded integers, can likely be removed.
 Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
   std::vector< Node > children;
   if( n.getNumChildren()>0 ){
@@ -92,7 +93,8 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
       return nn;
     }
   }else{
-    return getRepresentative(n);
+    //return getRepresentative(n);
+    return getValue(n);
   }
 }
 
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index ec5255db7..be2a274b2 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -68,7 +68,8 @@ TESTS =	\
 	cons-sets-bounds.smt2 \
 	bug651.smt2 \
 	bug652.smt2 \
-	bug782.smt2
+	bug782.smt2 \
+	quant_real_univ.cvc
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc b/test/regress/regress0/fmf/quant_real_univ.cvc
new file mode 100644
index 000000000..c3cefd767
--- /dev/null
+++ b/test/regress/regress0/fmf/quant_real_univ.cvc
@@ -0,0 +1,14 @@
+% EXPECT: sat
+OPTION "fmf-bound";
+Atom : TYPE;
+REAL_UNIVERSE : SET OF [REAL];
+ATOM_UNIVERSE : SET OF [Atom];
+ASSERT REAL_UNIVERSE = UNIVERSE :: SET OF [REAL];
+ASSERT ATOM_UNIVERSE = UNIVERSE :: SET OF [Atom];
+
+levelVal : SET OF [Atom, REAL];
+ASSERT FORALL (s : Atom, v1, v2 : REAL) : 
+			(TUPLE(s) IS_IN ATOM_UNIVERSE AND TUPLE(v1) IS_IN REAL_UNIVERSE AND TUPLE(v2) IS_IN REAL_UNIVERSE) 
+			=> (((s, v1) IS_IN levelVal AND (s, v2) IS_IN levelVal) => (v1 = v2));
+
+CHECKSAT;