Invalid propagator domain

Issue #411 resolved
Broes De Cat created an issue

Failed: ModelExpansion/MXsatTest.DoesMXWithCP/51 Testing /home/broes/documents/oursoftware/gidl2/tests/mx/satmx/set_reuse.idp stack trace: /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : AssertionException::AssertionException(std::string)+0x58 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : TypedFOPropagator<FOPropBDDDomainFactory, FOPropBDDDomain>::setCTOfDomain(Formula const, FOPropBDDDomain)+0x124 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : TypedFOPropagator<FOPropBDDDomainFactory, FOPropBDDDomain>::updateDomain(Formula const, FOPropDirection, bool, FOPropBDDDomain, Formula const)+0x4b4 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : TypedFOPropagator<FOPropBDDDomainFactory, FOPropBDDDomain>::visit(QuantForm const)+0x8e8 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : QuantForm::accept(TheoryVisitor) const+0x2e /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : TypedFOPropagator<FOPropBDDDomainFactory, FOPropBDDDomain>::doPropagation()+0x325 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : generateBounds(AbstractTheory, AbstractStructure&, bool, bool, Vocabulary)+0x2c2 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : GroundingInference<MinisatID::Space>::ground()+0x594 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : GroundingInference<MinisatID::Space>::doGrounding(AbstractTheory, AbstractStructure, Term, TraceMonitor, bool, MinisatID::Space, Vocabulary)+0x26b /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : ModelExpansion::expand() const+0xeb /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : ModelExpansion::doModelExpansion(AbstractTheory, AbstractStructure, Vocabulary, TraceMonitor)+0x62 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : ModelExpandInference::execute(std::__debug::vector<InternalArgument, std::allocator<InternalArgument> > const&) const+0x98 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : LuaConnection::InternalProcedure::operator()(lua_State) const+0x11a /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : LuaConnection::internalCall(lua_State)+0x64a /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/lib/lua/src/liblua.so.5 : ()+0x13f7f /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/lib/lua/src/liblua.so.5 : ()+0x2b77a /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/lib/lua/src/liblua.so.5 : ()+0x14251 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/lib/lua/src/liblua.so.5 : ()+0x96b2 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/lib/lua/src/liblua.so.5 : ()+0x1318e /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/lib/lua/src/liblua.so.5 : ()+0x1467d /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/lib/lua/src/liblua.so.5 : lua_pcall(lua_State, int, int, int)+0xa8 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : LuaConnection::execute(std::string const&)+0x61 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : Insert::exec(std::string const&)+0x18 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/src/libidp.so : handleAndRun(void)+0x29 /export/home1/NoCsBack/dtai/broes/gidlbuilds/debug/lib/tinythread/source/libtinythread.so : tthread::thread::wrapper_function(void*)+0x29 /lib/x86_64-linux-gnu/libpthread.so.0 : ()+0x7e9a /lib/x86_64-linux-gnu/libc.so.6 : clone()+0x6d Error: ASSERT FAILED: getFactory()->isValidAsDomainFor(d,f) @ /home/broes/documents/oursoftware/gidl2/src/inferences/propagation/Propagator.hpp (162)

Comments (2)

  1. Bart Bogaerts

    Eerste idee: die vrije variabele wordt niet goed inrekening gebracht en komt niet voor in hot domain van de subformule of zo

    Ik zal er eens naar kijken! (maar nog niet vandaag)

  2. Bart Bogaerts

    Added an extra quantification in propagator

    This extra quantifications avoid faulty behavior in case a formula does not depend on one of the higher quantified variables. This fixes #411

    → <<cset e9c04b203ab2>>

  3. Log in to comment