summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl/icp/intersection.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nl/icp/intersection.cpp')
-rw-r--r--src/theory/arith/nl/icp/intersection.cpp224
1 files changed, 224 insertions, 0 deletions
diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp
new file mode 100644
index 000000000..148059db0
--- /dev/null
+++ b/src/theory/arith/nl/icp/intersection.cpp
@@ -0,0 +1,224 @@
+/********************* */
+/*! \file intersection.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief
+ **/
+
+#include "theory/arith/nl/icp/intersection.h"
+
+#ifdef CVC4_POLY_IMP
+
+#include <iostream>
+
+#include "base/check.h"
+#include "base/output.h"
+#include "theory/arith/nl/poly_conversion.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace icp {
+
+PropagationResult intersect_interval_with(poly::Interval& cur,
+ const poly::Interval& res,
+ std::size_t size_threshold)
+{
+ Trace("nl-icp") << cur << " := " << cur << " intersected with " << res
+ << std::endl;
+
+ if (bitsize(get_lower(res)) > size_threshold
+ || bitsize(get_upper(res)) > size_threshold)
+ {
+ Trace("nl-icp") << "Reached bitsize threshold" << std::endl;
+ return PropagationResult::NOT_CHANGED;
+ }
+
+ // Basic idea to organize this function:
+ // The bounds for res have 5 positions:
+ // 1 < 2 (lower(cur)) < 3 < 4 (upper(cur)) < 5
+
+ if (get_upper(res) < get_lower(cur))
+ {
+ // upper(res) at 1
+ Trace("nl-icp") << "res < cur -> conflict" << std::endl;
+ return PropagationResult::CONFLICT;
+ }
+ if (get_upper(res) == get_lower(cur))
+ {
+ // upper(res) at 2
+ if (get_upper_open(res) || get_lower_open(cur))
+ {
+ Trace("nl-icp") << "meet at lower, but one is open -> conflict"
+ << std::endl;
+ return PropagationResult::CONFLICT;
+ }
+ if (!is_point(cur))
+ {
+ Trace("nl-icp") << "contracts to point interval at lower" << std::endl;
+ cur = poly::Interval(get_upper(res));
+ return PropagationResult::CONTRACTED;
+ }
+ return PropagationResult::NOT_CHANGED;
+ }
+ Assert(get_upper(res) > get_lower(cur))
+ << "Comparison operator does weird stuff.";
+ if (get_upper(res) < get_upper(cur))
+ {
+ // upper(res) at 3
+ if (get_lower(res) < get_lower(cur))
+ {
+ // lower(res) at 1
+ Trace("nl-icp") << "lower(cur) .. upper(res)" << std::endl;
+ cur.set_upper(get_upper(res), get_upper_open(res));
+ return PropagationResult::CONTRACTED;
+ }
+ if (get_lower(res) == get_lower(cur))
+ {
+ // lower(res) at 2
+ Trace("nl-icp") << "meet at lower, lower(cur) .. upper(res)" << std::endl;
+ cur = poly::Interval(get_lower(cur),
+ get_lower_open(cur) || get_lower_open(res),
+ get_upper(res),
+ get_upper_open(res));
+ if (get_lower_open(cur) && !get_lower_open(res))
+ {
+ return PropagationResult::CONTRACTED;
+ }
+ return PropagationResult::CONTRACTED_WITHOUT_CURRENT;
+ }
+ Assert(get_lower(res) > get_lower(cur))
+ << "Comparison operator does weird stuff.";
+ // lower(res) at 3
+ Trace("nl-icp") << "cur covers res" << std::endl;
+ cur = res;
+ return PropagationResult::CONTRACTED_WITHOUT_CURRENT;
+ }
+ if (get_upper(res) == get_upper(cur))
+ {
+ // upper(res) at 4
+ if (get_lower(res) < get_lower(cur))
+ {
+ // lower(res) at 1
+ Trace("nl-icp") << "res covers cur but meet at upper" << std::endl;
+ if (get_upper_open(res) && !get_upper_open(cur))
+ {
+ cur.set_upper(get_upper(cur), true);
+ return PropagationResult::CONTRACTED;
+ }
+ return PropagationResult::NOT_CHANGED;
+ }
+ if (get_lower(res) == get_lower(cur))
+ {
+ // lower(res) at 2
+ Trace("nl-icp") << "same bounds but check openness" << std::endl;
+ bool changed = false;
+ if (get_lower_open(res) && !get_lower_open(cur))
+ {
+ changed = true;
+ cur.set_lower(get_lower(cur), true);
+ }
+ if (get_upper_open(res) && !get_upper_open(cur))
+ {
+ changed = true;
+ cur.set_upper(get_upper(cur), true);
+ }
+ if (changed)
+ {
+ if ((get_lower_open(res) || !get_upper_open(cur))
+ && (get_upper_open(res) || !get_upper_open(cur)))
+ {
+ return PropagationResult::CONTRACTED_WITHOUT_CURRENT;
+ }
+ return PropagationResult::CONTRACTED;
+ }
+ return PropagationResult::NOT_CHANGED;
+ }
+ Assert(get_lower(res) > get_lower(cur))
+ << "Comparison operator does weird stuff.";
+ // lower(res) at 3
+ Trace("nl-icp") << "cur covers res but meet at upper" << std::endl;
+ cur = poly::Interval(get_lower(res),
+ get_lower_open(res),
+ get_upper(res),
+ get_upper_open(cur) || get_upper_open(res));
+ if (get_upper_open(cur) && !get_upper_open(res))
+ {
+ return PropagationResult::CONTRACTED;
+ }
+ return PropagationResult::CONTRACTED_WITHOUT_CURRENT;
+ }
+
+ Assert(get_upper(res) > get_upper(cur))
+ << "Comparison operator does weird stuff.";
+ // upper(res) at 5
+
+ if (get_lower(res) < get_lower(cur))
+ {
+ // lower(res) at 1
+ Trace("nl-icp") << "res covers cur" << std::endl;
+ return PropagationResult::NOT_CHANGED;
+ }
+ if (get_lower(res) == get_lower(cur))
+ {
+ // lower(res) at 2
+ Trace("nl-icp") << "res covers cur but meet at lower" << std::endl;
+ if (get_lower_open(res) && is_point(cur))
+ {
+ return PropagationResult::CONFLICT;
+ }
+ else if (get_lower_open(res) && !get_lower_open(cur))
+ {
+ cur.set_lower(get_lower(cur), true);
+ return PropagationResult::CONTRACTED;
+ }
+ return PropagationResult::NOT_CHANGED;
+ }
+ Assert(get_lower(res) > get_lower(cur))
+ << "Comparison operator does weird stuff.";
+ if (get_lower(res) < get_upper(cur))
+ {
+ // lower(res) at 3
+ Trace("nl-icp") << "lower(res) .. upper(cur)" << std::endl;
+ cur.set_lower(get_lower(res), get_lower_open(res));
+ return PropagationResult::CONTRACTED;
+ }
+ if (get_lower(res) == get_upper(cur))
+ {
+ // lower(res) at 4
+ if (get_lower_open(res) || get_upper_open(cur))
+ {
+ Trace("nl-icp") << "meet at upper, but one is open -> conflict"
+ << std::endl;
+ return PropagationResult::CONFLICT;
+ }
+ if (!is_point(cur))
+ {
+ Trace("nl-icp") << "contracts to point interval at upper" << std::endl;
+ cur = poly::Interval(get_lower(res));
+ return PropagationResult::CONTRACTED;
+ }
+ return PropagationResult::NOT_CHANGED;
+ }
+
+ Assert(get_lower(res) > get_upper(cur));
+ // lower(res) at 5
+ Trace("nl-icp") << "res > cur -> conflict" << std::endl;
+ return PropagationResult::CONFLICT;
+}
+
+} // namespace icp
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback