Invalid propagator domain
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)
-
-
- changed status to resolved
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>>
- Log in to comment
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)