From 7d57703f31e97b40812ed32424164d7c93cbc22c Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Tue, 7 Jul 2026 15:47:30 +0200 Subject: [PATCH 1/3] Fix default BoolExpr accumulator construction --- gecode/minimodel/bool-expr.cpp | 23 ++++++++++++++++---- test/int/mm-bool.cpp | 39 ++++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+), 4 deletions(-) diff --git a/gecode/minimodel/bool-expr.cpp b/gecode/minimodel/bool-expr.cpp index ce8e814c61..ae5519edb5 100755 --- a/gecode/minimodel/bool-expr.cpp +++ b/gecode/minimodel/bool-expr.cpp @@ -84,7 +84,7 @@ namespace Gecode { * */ BoolExpr::Node::Node(void) - : use(1), l(nullptr), r(nullptr), m(nullptr) {} + : use(1), same(0), t(NT_AND), l(nullptr), r(nullptr), m(nullptr) {} BoolExpr::Node::~Node(void) { delete m; @@ -125,8 +125,18 @@ namespace Gecode { n->x = x; } - BoolExpr::BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r) - : n(new Node) { + BoolExpr::BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r) { + if (((t == NT_AND) || (t == NT_OR)) && (l.n->same == 0)) { + n = r.n; + n->use++; + return; + } + if (((t == NT_AND) || (t == NT_OR)) && (r.n->same == 0)) { + n = l.n; + n->use++; + return; + } + n = new Node; int ls = ((l.n->t == t) || (l.n->t == NT_VAR)) ? l.n->same : 1; int rs = ((r.n->t == t) || (r.n->t == NT_VAR)) ? r.n->same : 1; n->same = ls+rs; @@ -140,7 +150,10 @@ namespace Gecode { BoolExpr::BoolExpr(const BoolExpr& l, NodeType t) { (void) t; assert(t == NT_NOT); - if (l.n->t == NT_NOT) { + if (l.n->same == 0) { + n = l.n; + n->use++; + } else if (l.n->t == NT_NOT) { n = l.n->l; n->use++; } else { @@ -505,6 +518,8 @@ namespace Gecode { NNF* NNF::nnf(Region& r, Node* n, bool neg) { + if (n->same == 0) + throw MiniModel::TooFewArguments("BoolExpr"); switch (n->t) { case BoolExpr::NT_VAR: case BoolExpr::NT_RLIN: diff --git a/test/int/mm-bool.cpp b/test/int/mm-bool.cpp index 6cd7fddfc2..2c7583d6f4 100644 --- a/test/int/mm-bool.cpp +++ b/test/int/mm-bool.cpp @@ -165,6 +165,41 @@ namespace Test { namespace Int { } }; + /// %Test Boolean expressions with default-constructed accumulators + class BoolExprDefaultAccumulator : public Test { + protected: + /// Boolean operation to accumulate + BoolOpcode o; + /// Whether the default expression starts on the right hand side + bool rhs; + public: + /// Create and register test + BoolExprDefaultAccumulator(BoolOpcode o0, bool rhs0) + : Test("MiniModel::BoolExpr::Default::"+ + std::string(o0 == BO_AND ? "And" : "Or")+ + (rhs0 ? "::Rhs" : "::Lhs"),3,0,1), o(o0), rhs(rhs0) {} + /// %Test whether \a x is solution + virtual bool solution(const Assignment& x) const { + int r = (o == BO_AND) ? (x[0] & x[1]) : (x[0] | x[1]); + return r == x[2]; + } + /// Post constraint on \a x + virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) { + using namespace Gecode; + Gecode::BoolExpr e; + Gecode::BoolExpr x0(channel(home,x[0])); + Gecode::BoolExpr x1(channel(home,x[1])); + if (o == BO_AND) { + e = rhs ? (x0 && e) : (e && x0); + e = e && x1; + } else { + e = rhs ? (x0 || e) : (e || x0); + e = e || x1; + } + rel(home, expr(home,e), IRT_EQ, channel(home,x[2])); + } + }; + const BoolInstr bi000[] = { {BO_AND,0,1,0},{BO_AND,2,3,1},{BO_AND,0,1,0}, {BO_HLT,0,0,0} @@ -4382,6 +4417,10 @@ namespace Test { namespace Int { (void) new BoolElement("Expr::A",0); (void) new BoolElement("Expr::B",1); (void) new BoolElement("Rel",2); + (void) new BoolExprDefaultAccumulator(BO_AND,false); + (void) new BoolExprDefaultAccumulator(BO_AND,true); + (void) new BoolExprDefaultAccumulator(BO_OR,false); + (void) new BoolExprDefaultAccumulator(BO_OR,true); } }; From 6fb859d36f47cecdeb233fd1f33071accaccffe4 Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Tue, 7 Jul 2026 16:22:23 +0200 Subject: [PATCH 2/3] Document BoolExpr accumulator fix --- changelog.in | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/changelog.in b/changelog.in index 3b5570d293..1123cd17d4 100755 --- a/changelog.in +++ b/changelog.in @@ -91,6 +91,17 @@ Rank: minor Restore the legacy GIST_STATIC_LIBS compatibility macro for static Windows clients. GECODE_STATIC_LIBS remains the preferred spelling. +[ENTRY] +Module: minimodel +What: bug +Rank: minor +Issue: 139 +Thanks: yuri@FreeBSD +[DESCRIPTION] +Fix default-constructed Boolean expressions so they can be used as +empty accumulators for conjunction and disjunction without reading +uninitialized node state. + [ENTRY] Module: float What: bug From 420234c42dd57747743fd9e8d249f221f62f82b4 Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Fri, 10 Jul 2026 13:55:07 +0200 Subject: [PATCH 3/3] minimodel: restrict empty BoolExpr accumulation --- gecode/minimodel.hh | 30 +++++++++++++-- gecode/minimodel/bool-expr.cpp | 21 ++++++----- test/int/mm-bool.cpp | 69 ++++++++++++++++++++++++++++++++++ 3 files changed, 108 insertions(+), 12 deletions(-) diff --git a/gecode/minimodel.hh b/gecode/minimodel.hh index 223aa53b9c..c406bf7c86 100755 --- a/gecode/minimodel.hh +++ b/gecode/minimodel.hh @@ -1359,8 +1359,20 @@ namespace Gecode { private: /// Pointer to node for expression Node* n; + /// Construct an expression, optionally treating an empty operand as an accumulator + BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r, + bool accumulator); + friend GECODE_MINIMODEL_EXPORT + BoolExpr operator &&(const BoolExpr&, const BoolExpr&); + friend GECODE_MINIMODEL_EXPORT + BoolExpr operator ||(const BoolExpr&, const BoolExpr&); public: - /// Default constructor + /** Default constructor + * + * Creates an empty accumulator for direct use with the public && and || + * accumulation operators. In every other context, the expression is + * invalid; materialization throws MiniModel::TooFewArguments. + */ GECODE_MINIMODEL_EXPORT BoolExpr(void); /// Copy constructor @@ -1421,10 +1433,22 @@ namespace Gecode { /// Negated Boolean expression GECODE_MINIMODEL_EXPORT BoolExpr operator !(const BoolExpr&); - /// Conjunction of Boolean expressions + /** Conjunction of Boolean expressions + * + * A default-constructed BoolExpr is treated as an empty accumulator + * only when it is a direct operand of this operator, in either operand + * position. This permits repeated accumulation; an empty expression in + * any other context remains invalid until materialization. + */ GECODE_MINIMODEL_EXPORT BoolExpr operator &&(const BoolExpr&, const BoolExpr&); - /// Disjunction of Boolean expressions + /** Disjunction of Boolean expressions + * + * A default-constructed BoolExpr is treated as an empty accumulator + * only when it is a direct operand of this operator, in either operand + * position. This permits repeated accumulation; an empty expression in + * any other context remains invalid until materialization. + */ GECODE_MINIMODEL_EXPORT BoolExpr operator ||(const BoolExpr&, const BoolExpr&); /// Exclusive-or of Boolean expressions diff --git a/gecode/minimodel/bool-expr.cpp b/gecode/minimodel/bool-expr.cpp index ae5519edb5..77ff561811 100755 --- a/gecode/minimodel/bool-expr.cpp +++ b/gecode/minimodel/bool-expr.cpp @@ -125,13 +125,19 @@ namespace Gecode { n->x = x; } - BoolExpr::BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r) { - if (((t == NT_AND) || (t == NT_OR)) && (l.n->same == 0)) { + BoolExpr::BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r) + : BoolExpr(l,t,r,false) {} + + BoolExpr::BoolExpr(const BoolExpr& l, NodeType t, const BoolExpr& r, + bool accumulator) { + if (accumulator && ((t == NT_AND) || (t == NT_OR)) && + (l.n->same == 0)) { n = r.n; n->use++; return; } - if (((t == NT_AND) || (t == NT_OR)) && (r.n->same == 0)) { + if (accumulator && ((t == NT_AND) || (t == NT_OR)) && + (r.n->same == 0)) { n = l.n; n->use++; return; @@ -150,10 +156,7 @@ namespace Gecode { BoolExpr::BoolExpr(const BoolExpr& l, NodeType t) { (void) t; assert(t == NT_NOT); - if (l.n->same == 0) { - n = l.n; - n->use++; - } else if (l.n->t == NT_NOT) { + if (l.n->t == NT_NOT) { n = l.n->l; n->use++; } else { @@ -600,11 +603,11 @@ namespace Gecode { BoolExpr operator &&(const BoolExpr& l, const BoolExpr& r) { - return BoolExpr(l,BoolExpr::NT_AND,r); + return BoolExpr(l,BoolExpr::NT_AND,r,true); } BoolExpr operator ||(const BoolExpr& l, const BoolExpr& r) { - return BoolExpr(l,BoolExpr::NT_OR,r); + return BoolExpr(l,BoolExpr::NT_OR,r,true); } BoolExpr operator ^(const BoolExpr& l, const BoolExpr& r) { diff --git a/test/int/mm-bool.cpp b/test/int/mm-bool.cpp index 2c7583d6f4..fa3b3b75d4 100644 --- a/test/int/mm-bool.cpp +++ b/test/int/mm-bool.cpp @@ -200,6 +200,64 @@ namespace Test { namespace Int { } }; + /// Invalid Boolean expressions that must fail when materialized + enum BoolExprInvalidKind { + BE_EMPTY, + BE_NOT_EMPTY, + BE_IMP_EMPTY_LHS, + BE_IMP_EMPTY_RHS, + BE_RIMP_EMPTY_LHS, + BE_RIMP_EMPTY_RHS, + BE_NOT_AND, + BE_NOT_OR, + BE_XOR_EMPTY, + BE_EQV_EMPTY, + BE_NEQ_EMPTY + }; + + /// %Test invalid Boolean expressions + class BoolExprInvalid : public Test { + protected: + /// Kind of invalid expression + BoolExprInvalidKind k; + public: + /// Create and register test + BoolExprInvalid(BoolExprInvalidKind k0, const std::string& s) + : Test("MiniModel::BoolExpr::Invalid::"+s,1,0,1), k(k0) {} + /// %Test whether an assignment is a solution + virtual bool solution(const Assignment&) const { + return false; + } + /// Post expression and check that materialization fails + virtual void post(Gecode::Space& home, Gecode::IntVarArray& x) { + using namespace Gecode; + BoolExpr empty; + BoolExpr v(channel(home,x[0])); + BoolExpr e; + switch (k) { + case BE_EMPTY: e = empty; break; + case BE_NOT_EMPTY: e = !empty; break; + case BE_IMP_EMPTY_LHS: e = empty >> v; break; + case BE_IMP_EMPTY_RHS: e = v >> empty; break; + case BE_RIMP_EMPTY_LHS: e = empty << v; break; + case BE_RIMP_EMPTY_RHS: e = v << empty; break; + case BE_NOT_AND: e = !empty && v; break; + case BE_NOT_OR: e = !empty || v; break; + case BE_XOR_EMPTY: e = empty ^ v; break; + case BE_EQV_EMPTY: e = empty == v; break; + case BE_NEQ_EMPTY: e = empty != v; break; + default: GECODE_NEVER; + } + try { + (void) expr(home,e); + } catch (MiniModel::TooFewArguments&) { + home.fail(); + return; + } + home.fail(); + } + }; + const BoolInstr bi000[] = { {BO_AND,0,1,0},{BO_AND,2,3,1},{BO_AND,0,1,0}, {BO_HLT,0,0,0} @@ -4421,6 +4479,17 @@ namespace Test { namespace Int { (void) new BoolExprDefaultAccumulator(BO_AND,true); (void) new BoolExprDefaultAccumulator(BO_OR,false); (void) new BoolExprDefaultAccumulator(BO_OR,true); + (void) new BoolExprInvalid(BE_EMPTY,"Empty"); + (void) new BoolExprInvalid(BE_NOT_EMPTY,"NotEmpty"); + (void) new BoolExprInvalid(BE_IMP_EMPTY_LHS,"Imp::EmptyLhs"); + (void) new BoolExprInvalid(BE_IMP_EMPTY_RHS,"Imp::EmptyRhs"); + (void) new BoolExprInvalid(BE_RIMP_EMPTY_LHS,"RImp::EmptyLhs"); + (void) new BoolExprInvalid(BE_RIMP_EMPTY_RHS,"RImp::EmptyRhs"); + (void) new BoolExprInvalid(BE_NOT_AND,"NotAnd"); + (void) new BoolExprInvalid(BE_NOT_OR,"NotOr"); + (void) new BoolExprInvalid(BE_XOR_EMPTY,"Xor"); + (void) new BoolExprInvalid(BE_EQV_EMPTY,"Eqv"); + (void) new BoolExprInvalid(BE_NEQ_EMPTY,"Neq"); } };