From 478251bcea8c25596eaab1664ac18c7ddd15c445 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 22 Mar 2017 10:58:03 -0500 Subject: [PATCH] Minor fix for bounded integers. --- src/theory/quantifiers/bounded_integers.cpp | 2 ++ src/theory/quantifiers/first_order_model.cpp | 4 +++- test/regress/regress0/fmf/Makefile.am | 3 ++- test/regress/regress0/fmf/quant_real_univ.cvc | 14 ++++++++++++++ 4 files changed, 21 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/fmf/quant_real_univ.cvc 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; -- 2.30.2