Module: ppl/ppl Branch: master Commit: badd595a0c22e91f4f1653ff8c7d53a3bf15ec50 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=badd595a0c22e... Author: Patricia Hill <p.m.hill@leeds.ac.uk> Date: Mon May 18 12:05:10 2009 +0100 Improved the methods refine_with_congruence[s](). Congruences can now refine the box even when the congruence is not non-relational. --- src/Box.templates.hh | 19 +--- tests/Box/Makefile.am | 7 +- tests/Box/refinewithcongruence1.cc | 194 ++++++++++++++++++++++++++++++++++++ 3 files changed, 201 insertions(+), 19 deletions(-) diff --git a/src/Box.templates.hh b/src/Box.templates.hh index 3f311fa..9918363 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -2192,23 +2192,8 @@ Box<ITV>::refine_no_check(const Congruence& cg) { } assert(cg.is_equality()); - dimension_type cg_num_vars = 0; - dimension_type cg_only_var = 0; - // Congruences that are not interval congruences are ignored. - if (!extract_interval_congruence(cg, cg_space_dim, cg_num_vars, cg_only_var)) - return; - - if (cg_num_vars == 0) { - // Dealing with a trivial congruence. - if (cg.inhomogeneous_term() != 0) - set_empty(); - return; - } - - assert(cg_num_vars == 1); - const Coefficient& n = cg.inhomogeneous_term(); - const Coefficient& d = cg.coefficient(Variable(cg_only_var)); - add_interval_constraint_no_check(cg_only_var, Constraint::EQUALITY, n, d); + Constraint c(cg); + refine_no_check(c); } template <typename ITV> diff --git a/tests/Box/Makefile.am b/tests/Box/Makefile.am index 4b53895..965ee15 100644 --- a/tests/Box/Makefile.am +++ b/tests/Box/Makefile.am @@ -100,6 +100,7 @@ propagateconstraints1 propagateconstraints2 \ relations1 relations2 relations3 relations4 \ refinewithconstraint1 refinewithconstraint2 \ refinewithconstraints1 \ +refinewithcongruence1 \ refinewithcongruences1 \ removespacedims1 \ simplifyusingcontext1 \ @@ -256,13 +257,15 @@ relations4_SOURCES = relations4.cc propagateconstraints1_SOURCES = propagateconstraints1.cc propagateconstraints2_SOURCES = propagateconstraints2.cc +refinewithcongruence1_SOURCES = refinewithcongruence1.cc + +refinewithcongruences1_SOURCES = refinewithcongruences1.cc + refinewithconstraint1_SOURCES = refinewithconstraint1.cc refinewithconstraint2_SOURCES = refinewithconstraint2.cc refinewithconstraints1_SOURCES = refinewithconstraints1.cc -refinewithcongruences1_SOURCES = refinewithcongruences1.cc - removespacedims1_SOURCES = removespacedims1.cc simplifyusingcontext1_SOURCES = simplifyusingcontext1.cc diff --git a/tests/Box/refinewithcongruence1.cc b/tests/Box/refinewithcongruence1.cc new file mode 100644 index 0000000..bba4477 --- /dev/null +++ b/tests/Box/refinewithcongruence1.cc @@ -0,0 +1,194 @@ +/* Test Box::refine_with_congruences(const Congruence_System&). + Copyright (C) 2001-2009 Roberto Bagnara <bagnara@cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +// Universe Box, zero dimensions and trivial congruence. +bool +test01() { + Congruence cg(Linear_Expression(0) %= 1); + TBox box(0); + box.refine_with_congruence(cg); + + Rational_Box known_result(0); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + +// Universe Box, 4 dimensions and refine with a proper congruence +bool +test02() { + Variable A(0); + Variable B(1); + Variable C(2); + Variable D(3); + + Congruence cg(A + B %= 0); + TBox box(4); + box.refine_with_congruence(cg); + + Rational_Box known_result(4); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + +// Universe Box in 3D and refine with an equality congruence. +bool +test03() { + Variable A(0); + Variable B(1); + Variable C(2); + + Congruence cg((A %= 7) / 0); + + TBox box(3); + box.refine_with_congruence(cg); + + Rational_Box known_result(3); + known_result.add_constraint(A == 7); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + +// Box in 1D and refine with an inconsistent proper congruence. +bool +test04() { + Variable A(0); + + Congruence cg((0*A %= 1) / 2); + + TBox box(1); + box.refine_with_congruence(cg); + + Rational_Box known_result(1, EMPTY); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + +// refine_with_congruence() +bool +test05() { + Variable A(0); + Variable B(1); + Variable C(2); + Variable D(3); + + Constraint_System cs; + cs.insert(A <= 5); + cs.insert(A >= 0); + cs.insert(B <= 5); + cs.insert(B >= 0); + cs.insert(C <= 5); + cs.insert(C >= 0); + cs.insert(D <= 5); + cs.insert(D >= 0); + TBox box(cs); + box.refine_with_congruence((1*A + 2*B + 3*C + 4*D %= 0) / 0); + + Constraint_System known_cs; + known_cs.insert(A == 0); + known_cs.insert(B == 0); + known_cs.insert(C == 0); + known_cs.insert(D == 0); + Rational_Box known_result(known_cs); + + bool ok = check_result(box, known_result); + + print_constraints(box, "*** box ***"); + + return ok; +} + + +bool +test06() { + Variable x(0); + Variable y(1); + Variable z(2); + + TBox box1(2); + + try { + // This is an invalid use of method + // Box::refine_with_congruence: it is illegal + // to refine with a congruence with bigger dimension. + box1.refine_with_congruence(x %= 0); + box1.refine_with_congruence(y - x + z %= 0); + } + catch (std::invalid_argument& e) { + nout << "std::invalid_argument: " << endl; + return true; + } + catch (...) { + } + return false; +} + +bool +test07() { + Variable y(1); + + TBox box(1); + + try { + // This is an invalid use of the method + // Box::refine_with_congruence(c): it is illegal to refine with a + // congruence that contains a variable that is not in the space + // of the box. + box.refine_with_congruence((y %= 0) / 0); + } + catch (std::invalid_argument& e) { + nout << "std::invalid_argument: " << endl; + return true; + } + catch (...) { + } + return false; +} + +} // namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); + DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test07); +END_MAIN