From 5a8ee19b531a86ea56658972c8aa6c77cebf3c54 Mon Sep 17 00:00:00 2001 From: Christoph Schwering Date: Sat, 26 Nov 2016 19:53:20 +1100 Subject: [PATCH] Fixed: Solver::Reduce() accidentally negated disjuncts. --- src/lela/format/output.h | 112 +++++++++++++++++++++++++-------------- src/lela/formula.h | 12 +++++ src/lela/solver.h | 8 +-- 3 files changed, 87 insertions(+), 45 deletions(-) diff --git a/src/lela/format/output.h b/src/lela/format/output.h index 02a9c4f..27a2fde 100644 --- a/src/lela/format/output.h +++ b/src/lela/format/output.h @@ -62,10 +62,7 @@ inline internal::Maybe LookupSymbol(Symbol s) { } template -std::ostream& operator<<(std::ostream& os, const std::pair p) { - os << "(" << p.first << ", " << p.second << ")"; - return os; -} +std::ostream& operator<<(std::ostream& os, const std::pair p); template std::ostream& print_sequence(std::ostream& os, @@ -79,57 +76,28 @@ template std::ostream& print_range(std::ostream& os, const Range& r, const char* pre = "[", const char* post = "]", - const char* sep = ", ") { - return print_sequence(os, r.begin(), r.end(), pre, post, sep); -} + const char* sep = ", "); template -std::ostream& operator<<(std::ostream& os, const std::vector& vec) { - print_sequence(os, vec.begin(), vec.end(), "[", "]", ", "); - return os; -} +std::ostream& operator<<(std::ostream& os, const std::vector& vec); template -std::ostream& operator<<(std::ostream& os, const std::list& list) { - os << '['; - print_sequence(os, list.begin(), list.end(), "[", "]", ", "); - os << '['; - return os; -} +std::ostream& operator<<(std::ostream& os, const std::list& list); template -std::ostream& operator<<(std::ostream& os, const std::set& set) { - print_sequence(os, set.begin(), set.end(), "{", "}", ", "); - return os; -} +std::ostream& operator<<(std::ostream& os, const std::set& set); template -std::ostream& operator<<(std::ostream& os, const std::multiset& set) { - print_sequence(os, set.begin(), set.end(), "m{", "}m", ", "); - return os; -} +std::ostream& operator<<(std::ostream& os, const std::multiset& set); template -std::ostream& operator<<(std::ostream& os, const std::map& map) { - print_sequence(os, map.begin(), map.end(), "{", "}", ", "); - return os; -} +std::ostream& operator<<(std::ostream& os, const std::map& map); template -std::ostream& operator<<(std::ostream& os, const std::multimap& map) { - print_sequence(os, map.begin(), map.end(), "m{", "}m", ", "); - return os; -} +std::ostream& operator<<(std::ostream& os, const std::multimap& map); template -std::ostream& operator<<(std::ostream& os, const internal::Maybe& m) { - if (m) { - os << "Just(" << m.val << ")"; - } else { - os << "Nothing"; - } - return os; -} +std::ostream& operator<<(std::ostream& os, const internal::Maybe& m); std::ostream& operator<<(std::ostream& os, const Symbol s) { internal::Maybe sort_name = LookupSort(s.sort()); @@ -332,6 +300,68 @@ std::ostream& print_sequence(std::ostream& os, return os; } +template +std::ostream& operator<<(std::ostream& os, const std::pair p) { + os << "(" << p.first << ", " << p.second << ")"; + return os; +} + +template +std::ostream& print_range(std::ostream& os, const Range& r, + const char* pre, + const char* post, + const char* sep) { + return print_sequence(os, r.begin(), r.end(), pre, post, sep); +} + +template +std::ostream& operator<<(std::ostream& os, const std::vector& vec) { + print_sequence(os, vec.begin(), vec.end(), "[", "]", ", "); + return os; +} + +template +std::ostream& operator<<(std::ostream& os, const std::list& list) { + os << '['; + print_sequence(os, list.begin(), list.end(), "[", "]", ", "); + os << '['; + return os; +} + +template +std::ostream& operator<<(std::ostream& os, const std::set& set) { + print_sequence(os, set.begin(), set.end(), "{", "}", ", "); + return os; +} + +template +std::ostream& operator<<(std::ostream& os, const std::multiset& set) { + print_sequence(os, set.begin(), set.end(), "m{", "}m", ", "); + return os; +} + +template +std::ostream& operator<<(std::ostream& os, const std::map& map) { + print_sequence(os, map.begin(), map.end(), "{", "}", ", "); + return os; +} + +template +std::ostream& operator<<(std::ostream& os, const std::multimap& map) { + print_sequence(os, map.begin(), map.end(), "m{", "}m", ", "); + return os; +} + +template +std::ostream& operator<<(std::ostream& os, const internal::Maybe& m) { + if (m) { + os << "Just(" << m.val << ")"; + } else { + os << "Nothing"; + } + return os; +} + } // namespace format } // namespace lela diff --git a/src/lela/formula.h b/src/lela/formula.h index 9b3fa36..fd9fde0 100644 --- a/src/lela/formula.h +++ b/src/lela/formula.h @@ -38,6 +38,14 @@ class Formula { public: enum Type { kClause, kNot, kOr, kExists }; + // XXX The implicit operator= sometimes (in cli) takes a non-const reference. Why?! + Element& operator=(const Element& e) { + type_ = e.type_; + clause_ = e.clause_; + var_ = e.var_; + return *this; + } + static Element Clause(const lela::Clause& c) { return Element(kClause, c); } static Element Not() { return Element(kNot); } static Element Or() { return Element(kOr); } @@ -231,6 +239,10 @@ class Formula { Iter end_; }; + Formula(Formula&&) = default; + Formula(const Formula&) = default; + Formula& operator=(const Formula&) = default; + static Formula Clause(const lela::Clause& c) { return Atomic(Element::Clause(c)); } static Formula Not(const Formula& phi) { return Unary(Element::Not(), phi); } static Formula Or(const Formula& phi, const Formula& psi) { return Binary(Element::Or(), phi, psi); } diff --git a/src/lela/solver.h b/src/lela/solver.h index 1640f79..e698cf1 100644 --- a/src/lela/solver.h +++ b/src/lela/solver.h @@ -266,10 +266,10 @@ class Solver { } } case Formula::Element::kOr: { - Formula left = Formula::Not(phi.left().Build()); - Formula right = Formula::Not(phi.right().Build()); - return Reduce(s, names, left.reader()) || - Reduce(s, names, right.reader()); + Formula::Reader left = phi.left(); + Formula::Reader right = phi.right(); + return Reduce(s, names, left) || + Reduce(s, names, right); } case Formula::Element::kExists: { const Term x = phi.head().var().val; -- GitLab