diff --git a/vertexy/src/private/constraints/ReachabilityConstraint.cpp b/vertexy/src/private/constraints/ReachabilityConstraint.cpp index 9bf001f..6fe2a6d 100644 --- a/vertexy/src/private/constraints/ReachabilityConstraint.cpp +++ b/vertexy/src/private/constraints/ReachabilityConstraint.cpp @@ -58,680 +58,43 @@ ReachabilityConstraint::ReachabilityConstraint( const ValueSet& requireReachableMask, const shared_ptr>& edgeGraphData, const ValueSet& edgeBlockedMask) - : IBacktrackingSolverConstraint(params) //ApplyGraphRelation(Params, SourceGraphData, EdgeGraphData)) - , m_edgeWatcher(*this) - , m_sourceGraphData(sourceGraphData) - , m_sourceGraph(sourceGraphData->getSource()) - , m_edgeGraphData(edgeGraphData) - , m_edgeGraph(edgeGraphData->getSource()->getImplementation()) - , m_minGraph(make_shared()) - , m_maxGraph(make_shared()) - , m_explanationGraph(make_shared()) - , m_sourceMask(sourceMask) - , m_requireReachableMask(requireReachableMask) - , m_edgeBlockedMask(edgeBlockedMask) + : TopologyConnectionConstraint(params, sourceGraphData, sourceMask, requireReachableMask, edgeGraphData, edgeBlockedMask) { - m_notSourceMask = sourceMask.inverted(); - m_notReachableMask = requireReachableMask.inverted(); - m_edgeOpenMask = edgeBlockedMask.inverted(); - for (int i = 0; i < m_sourceGraph->getNumVertices(); ++i) - { - VarID var = sourceGraphData->get(i); - if (var.isValid()) - { - m_variableToSourceVertexIndex[var] = i; - } - } - - vxy_assert(m_edgeGraph->getSource() == m_sourceGraph); - for (int i = 0; i < m_edgeGraph->getNumVertices(); ++i) - { - VarID var = edgeGraphData->get(i); - if (var.isValid()) - { - m_variableToSourceEdgeIndex[var] = i; - } - } -} - -bool ReachabilityConstraint::getGraphRelations(const vector& literals, ConstraintGraphRelationInfo& outRelations) const -{ - // First search through all provided literals to find the minimum graph vertex. - // Note: some vertices will be edges, some will be tiles. - int minGraphVertex = m_sourceGraph->getNumVertices(); - - vector vertices; - vector isEdgeNode; - - vertices.reserve(literals.size()); - isEdgeNode.reserve(literals.size()); - - for (auto& lit : literals) - { - int graphVertex = m_sourceGraphData->indexOf(lit.variable); - if (graphVertex < 0) - { - int edgeNode = m_edgeGraphData->indexOf(lit.variable); - vxy_assert(edgeNode >= 0); - - vertices.push_back(edgeNode); - isEdgeNode.push_back(true); - - int edgeFrom, edgeTo; - bool bidirectional; - m_edgeGraph->getSourceEdgeForVertex(edgeNode, edgeFrom, edgeTo, bidirectional); - - graphVertex = min(edgeFrom, edgeTo); - } - else - { - vertices.push_back(graphVertex); - isEdgeNode.push_back(false); - } - vxy_assert(graphVertex >= 0); - minGraphVertex = min(graphVertex, minGraphVertex); - } - - // We always provide relations in terms of the source graph. - // Relations are anchored to the minimum vertex ID found (maps to top-leftmost in a grid graph). - outRelations.reset(m_sourceGraph, minGraphVertex); - - // create the relations! - outRelations.reserve(literals.size()); - for (int i = 0; i != literals.size(); ++i) - { - bool isEdge = isEdgeNode[i]; - - if (!isEdge) - { - int vertex = vertices[i]; - if (vertex != minGraphVertex) - { - TopologyLink link; - if (!m_sourceGraph->getTopologyLink(minGraphVertex, vertex, link)) - { - // no path specified in graph - // TODO: assert? - outRelations.clear(); - return false; - } - - auto linkRel = make_shared>(m_sourceGraphData, link); - outRelations.addRelation(m_sourceGraphData->get(vertex), linkRel); - } - else - { - auto selfRel = make_shared>(m_sourceGraphData); - outRelations.addRelation(m_sourceGraphData->get(vertex), selfRel); - } - } - else - { - int edgeNode = vertices[i]; - - // edge variable: get the source node if the edge - int edgeOrigin, edgeDestination; - bool bidirectional; - m_edgeGraph->getSourceEdgeForVertex(edgeNode, edgeOrigin, edgeDestination, bidirectional); - - int nodeEdgeIndex = -1; - for (int e = 0; e < m_sourceGraph->getNumOutgoing(edgeOrigin); ++e) - { - if (int testDest; m_sourceGraph->getOutgoingDestination(edgeOrigin, e, testDest) && testDest == edgeDestination) - { - nodeEdgeIndex = e; - break; - } - } - if (nodeEdgeIndex < 0) - { - vxy_assert_msg(false, "Edge node %d has source graph node origin %d, but can't find edgeIndex in source graph!", edgeNode, edgeOrigin); - outRelations.clear(); - return false; - } - - auto nodeToEdgeNodeRel = make_shared>(m_sourceGraph, m_edgeGraph, nodeEdgeIndex); - auto nodeToEdgeVarRel = nodeToEdgeNodeRel->map(make_shared>(m_edgeGraphData)); - - if (edgeOrigin != minGraphVertex) - { - TopologyLink link; - if (!m_sourceGraph->getTopologyLink(minGraphVertex, edgeOrigin, link)) - { - vxy_assert_msg(false, "expected link between vertices %d -> %d", minGraphVertex, edgeOrigin); - outRelations.clear(); - return false; - } - - auto linkRel = make_shared(m_sourceGraph, link); - outRelations.addRelation(m_edgeGraphData->get(edgeNode), linkRel->map(nodeToEdgeVarRel)); - } - else - { - outRelations.addRelation(m_edgeGraphData->get(edgeNode), nodeToEdgeVarRel); - } - } - } - - vxy_assert(outRelations.relations.size() == literals.size()); - return true; -} - -bool ReachabilityConstraint::initialize(IVariableDatabase* db) -{ - // Add all vertices to min/max graphs - for (int vertexIndex = 0; vertexIndex < m_sourceGraph->getNumVertices(); ++vertexIndex) - { - VarID vertexVar = m_sourceGraphData->get(vertexIndex); - - int addedIdx = m_maxGraph->addVertex(); - vxy_assert(addedIdx == vertexIndex); - - addedIdx = m_minGraph->addVertex(); - vxy_assert(addedIdx == vertexIndex); - - addedIdx = m_explanationGraph->addVertex(); - vxy_assert(addedIdx == vertexIndex); - - if (vertexVar.isValid()) - { - m_vertexWatchHandles[vertexVar] = db->addVariableWatch(vertexVar, EVariableWatchType::WatchModification, this); - } - } - - hash_map> edgeCapacities; - - m_totalNumEdges = 0; - - // Add all definitely-open edges to the min graph, and all possibly-open edges to the max graph - m_reachabilityEdgeLookup.resize(m_sourceGraph->getNumVertices()); - for (int sourceVertex = 0; sourceVertex < m_sourceGraph->getNumVertices(); ++sourceVertex) - { - auto foundVertexEdges = edgeCapacities.find(sourceVertex); - if (foundVertexEdges == edgeCapacities.end()) - { - foundVertexEdges = edgeCapacities.insert(sourceVertex).first; - } - - m_reachabilityEdgeLookup[sourceVertex].reserve(m_sourceGraph->getNumOutgoing(sourceVertex)); - for (int edgeIndex = 0; edgeIndex < m_sourceGraph->getNumOutgoing(sourceVertex); ++edgeIndex) - { - int destVertex; - if (m_sourceGraph->getOutgoingDestination(sourceVertex, edgeIndex, destVertex)) - { - m_reachabilityEdgeLookup[sourceVertex].push_back(make_tuple(destVertex, m_totalNumEdges)); - ++m_totalNumEdges; - - int edgeNode = m_edgeGraph->getVertexForSourceEdge(sourceVertex, destVertex); - vxy_assert(edgeNode >= 0); - VarID edgeVar = m_edgeGraphData->get(edgeNode); - - bool edgeIsClosed = true; - if (edgeVar.isValid()) - { - if (definitelyOpenEdge(db, edgeVar)) - { - edgeIsClosed = false; - - m_minGraph->initEdge(sourceVertex, destVertex); - m_maxGraph->initEdge(sourceVertex, destVertex); - m_explanationGraph->initEdge(sourceVertex, destVertex); - } - else if (possiblyOpenEdge(db, edgeVar)) - { - edgeIsClosed = false; - - if (m_edgeWatchHandles.find(edgeVar) == m_edgeWatchHandles.end()) - { - m_edgeWatchHandles[edgeVar] = db->addVariableWatch(edgeVar, EVariableWatchType::WatchModification, &m_edgeWatcher); - } - m_maxGraph->initEdge(sourceVertex, destVertex); - m_explanationGraph->initEdge(sourceVertex, destVertex); - } - } - else - { - edgeIsClosed = false; - - // No variable for this edge, so should always exist - m_minGraph->initEdge(sourceVertex, destVertex); - m_maxGraph->initEdge(sourceVertex, destVertex); - m_explanationGraph->initEdge(sourceVertex, destVertex); - } - - foundVertexEdges->second[destVertex] = edgeIsClosed ? CLOSED_EDGE_FLOW : OPEN_EDGE_FLOW; - - if (!m_sourceGraph->hasEdge(destVertex, sourceVertex)) - { - auto foundDestVertexEdges = edgeCapacities.find(destVertex); - if (foundDestVertexEdges == edgeCapacities.end()) - { - foundDestVertexEdges = edgeCapacities.insert(destVertex).first; - } - foundDestVertexEdges->second[sourceVertex] = 0; - } - } - } - } - - // Build flow graph edges flat list and lookup map - m_flowGraphEdges.reserve(m_totalNumEdges); - m_flowGraphLookup.reserve(m_sourceGraph->getNumVertices()); - for (int sourceVertex = 0; sourceVertex < m_sourceGraph->getNumVertices(); ++sourceVertex) - { - m_flowGraphLookup.emplace_back(m_flowGraphEdges.size(), m_flowGraphEdges.size() + edgeCapacities[sourceVertex].size()); - for (auto it = edgeCapacities[sourceVertex].begin(), itEnd = edgeCapacities[sourceVertex].end(); it != itEnd; ++it) - { - m_flowGraphEdges.push_back({it->first, -1, it->second}); - } - } - - // Fill in the ReverseEdgeIndex for each vertex - for (int sourceVertex = 0; sourceVertex < m_sourceGraph->getNumVertices(); ++sourceVertex) - { - for (int i = get<0>(m_flowGraphLookup[sourceVertex]); i < get<1>(m_flowGraphLookup[sourceVertex]); ++i) - { - if (m_flowGraphEdges[i].reverseEdgeIndex < 0) - { - int destVertex = m_flowGraphEdges[i].endVertex; - bool foundReverse = false; - for (int j = get<0>(m_flowGraphLookup[destVertex]); j < get<1>(m_flowGraphLookup[destVertex]); ++j) - { - if (m_flowGraphEdges[j].endVertex == sourceVertex) - { - m_flowGraphEdges[i].reverseEdgeIndex = j; - vxy_assert(m_flowGraphEdges[j].reverseEdgeIndex < 0); - m_flowGraphEdges[j].reverseEdgeIndex = i; - - foundReverse = true; - break; - } - } - vxy_assert(foundReverse); - } - } - } - - // Register for callback when edges are added/removed from ExplanationGraph, in order to update capacities - m_explanationGraph->getEdgeChangeListener().add([&](bool edgeWasAdded, int from, int to) - { - onExplanationGraphEdgeChange(edgeWasAdded, from, to); - }); - - // Create reachability structures for all variables that are possibly reachability sources - for (int vertex = 0; vertex < m_sourceGraph->getNumVertices(); ++vertex) - { - VarID vertexVar = m_sourceGraphData->get(vertex); - if (vertexVar.isValid() && possiblyIsSource(db, vertexVar)) - { - addSource(vertexVar); - m_initialPotentialSources.push_back(vertexVar); - } - } - - // Constrain all variables that are definitely reachable by any definite reachability source to reachable - // Constrain all variables that are not reachable by all potential reachability sources to unreachable - for (int vertex = 0; vertex < m_sourceGraph->getNumVertices(); ++vertex) - { - VarID vertexVar = m_sourceGraphData->get(vertex); - if (vertexVar.isValid()) - { - EReachabilityDetermination determination = determineReachability(db, vertex); - - if (determination == EReachabilityDetermination::DefinitelyUnreachable) - { - if (!db->constrainToValues(vertexVar, m_notReachableMask, this)) - { - return false; - } - } - else if (determination == EReachabilityDetermination::DefinitelyReachable) - { - if (!db->constrainToValues(vertexVar, m_requireReachableMask, this)) - { - return false; - } - } - } - } - - return true; } -void ReachabilityConstraint::reset(IVariableDatabase* db) +shared_ptr> ReachabilityConstraint::makeTopology(const shared_ptr& graph) const { - for (auto it = m_vertexWatchHandles.begin(), itEnd = m_vertexWatchHandles.end(); it != itEnd; ++it) - { - db->removeVariableWatch(it->first, it->second, this); - } - m_vertexWatchHandles.clear(); - - for (auto it = m_edgeWatchHandles.begin(), itEnd = m_edgeWatchHandles.end(); it != itEnd; ++it) - { - db->removeVariableWatch(it->first, it->second, &m_edgeWatcher); - } - m_edgeWatchHandles.clear(); -} - -bool ReachabilityConstraint::onVariableNarrowed(IVariableDatabase* db, VarID variable, const ValueSet& prevValue, bool& removeWatch) -{ - const ValueSet& newValue = db->getPotentialValues(variable); - - if ((prevValue.anyPossible(m_sourceMask) && !newValue.anyPossible(m_sourceMask)) || - (prevValue.anyPossible(m_notReachableMask) && !newValue.anyPossible(m_notReachableMask))) - { - if (!contains(m_vertexProcessList.begin(), m_vertexProcessList.end(), variable)) - { - m_vertexProcessList.push_back(variable); - } - db->queueConstraintPropagation(this); - } - return true; -} - -bool ReachabilityConstraint::EdgeWatcher::onVariableNarrowed(IVariableDatabase* db, VarID var, const ValueSet& prevValue, bool& removeHandle) -{ - const ValueSet& newValue = db->getPotentialValues(var); - if ((prevValue.anyPossible(m_parent.m_edgeBlockedMask) && !newValue.anyPossible(m_parent.m_edgeBlockedMask)) || - (prevValue.anyPossible(m_parent.m_edgeOpenMask) && !newValue.anyPossible(m_parent.m_edgeOpenMask))) - { - m_parent.m_edgeProcessList.push_back(var); - db->queueConstraintPropagation(&m_parent); - } - return true; -} - -bool ReachabilityConstraint::propagate(IVariableDatabase* db) -{ - vxy_assert(!m_edgeChangeFailure); - ValueGuard guardEdgeChangeFailure(m_edgeChangeFailure, false); - - // Process edges first, adding/removing edges from the Min/Max graph, respectively - for (VarID edgeVar : m_edgeProcessList) - { - updateGraphsForEdgeChange(db, edgeVar); - if (m_edgeChangeFailure) - { - return false; - } - } - m_edgeProcessList.clear(); - - #if REACHABILITY_USE_RAMAL_REPS - // Batch-update reachability for all edge changes. This will trigger OnReachabilityChanged callbacks. - { - vxy_assert(!m_edgeChangeFailure); - ValueGuard guardEdgeChange(m_inEdgeChange, true); - ValueGuard guardDb(m_edgeChangeDb, db); - - for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) - { - it->second.maxReachability->refresh(); - if (m_edgeChangeFailure) - { - return false; - } - - it->second.minReachability->refresh(); - if (m_edgeChangeFailure) - { - return false; - } - } - } - #endif - - vxy_assert(!m_edgeChangeFailure); - - // Now that reachability info is up to date, process vertices - for (VarID vertexVar : m_vertexProcessList) - { - if (!processVertexVariableChange(db, vertexVar)) - { - return false; - } - } - m_vertexProcessList.clear(); - - return true; + return make_shared(graph, USE_RAMAL_REPS_BATCHING, true, false); } -bool ReachabilityConstraint::processVertexVariableChange(IVariableDatabase* db, VarID variable) -{ - if (!db->anyPossible(variable, m_sourceMask)) - { - if (!removeSource(db, variable)) - { - return false; - } - } - - // If this now requires reachability... - if (!db->anyPossible(variable, m_notReachableMask)) - { - int vertex = m_variableToSourceVertexIndex[variable]; - int numReachableSources = 0; - VarID lastReachableSource = VarID::INVALID; - for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) - { - if (it->second.maxReachability->isReachable(vertex)) - { - ++numReachableSources; - lastReachableSource = it->first; - if (numReachableSources > 1) - { - break; - } - } - } - - // If not reachable by any source, then fail - if (numReachableSources == 0) - { - bool success = db->constrainToValues(variable, m_notReachableMask, this, [&](auto params) { return explainNoReachability(params); }); - vxy_assert(!success); - return false; - } - // If reachable by a single potential source, that single source must be definite - else if (numReachableSources == 1) - { - if (!db->constrainToValues(lastReachableSource, m_sourceMask, this, [&](auto params) { return explainRequiredSource(params); })) - { - return false; - } - } - } - - return true; -} - -void ReachabilityConstraint::addSource(VarID source) +EventListenerHandle ReachabilityConstraint::addMinCallback(RamalRepsType& minReachable, const IVariableDatabase* db, VarID source) { - int vertex = m_variableToSourceVertexIndex[source]; - - #if REACHABILITY_USE_RAMAL_REPS - auto minReachable = make_shared(m_minGraph, USE_RAMAL_REPS_BATCHING, true, false); - auto maxReachable = make_shared(m_maxGraph, USE_RAMAL_REPS_BATCHING, true, false); - #else - auto minReachable = make_shared(m_minGraph); - auto maxReachable = make_shared(m_maxGraph); - #endif - - minReachable->initialize(vertex, &m_reachabilityEdgeLookup, m_totalNumEdges); - maxReachable->initialize(vertex, &m_reachabilityEdgeLookup, m_totalNumEdges); - - // Listen for when reachability changes on the conservative/optimistic graphs - EventListenerHandle minDelHandle = minReachable->onReachabilityChanged.add([this, source](int changedVertex, bool isReachable) + return minReachable.onReachabilityChanged.add([this, source](int changedVertex, bool isReachable) { if (!m_backtracking && !m_explainingSourceRequirement) { vxy_assert(isReachable); - onReachabilityChanged(changedVertex, source, true); + onVertexChanged(changedVertex, source, true); } }); +} - EventListenerHandle maxDelHandle = maxReachable->onReachabilityChanged.add([this, source](int changedVertex, bool isReachable) +EventListenerHandle ReachabilityConstraint::addMaxCallback(RamalRepsType& maxReachable, const IVariableDatabase* db, VarID source) +{ + return maxReachable.onReachabilityChanged.add([this, source](int changedVertex, bool isReachable) { if (!m_backtracking && !m_explainingSourceRequirement) { vxy_assert(!isReachable); - onReachabilityChanged(changedVertex, source, false); + onVertexChanged(changedVertex, source, false); } }); - - m_reachabilitySources[source] = {minReachable, maxReachable, minDelHandle, maxDelHandle}; } -bool ReachabilityConstraint::removeSource(IVariableDatabase* db, VarID source) -{ - if (m_reachabilitySources.find(source) == m_reachabilitySources.end()) - { - return true; - } - - vxy_assert(m_backtrackData.empty() || m_backtrackData.back().level <= db->getDecisionLevel()); - if (m_backtrackData.empty() || m_backtrackData.back().level != db->getDecisionLevel()) - { - m_backtrackData.push_back({db->getDecisionLevel()}); - } - - vxy_assert(m_backtrackData.back().level == db->getDecisionLevel()); - vxy_sanity(!contains(m_backtrackData.back().reachabilitySourcesRemoved.begin(), m_backtrackData.back().reachabilitySourcesRemoved.end(), source)); - m_backtrackData.back().reachabilitySourcesRemoved.push_back(source); - - ReachabilitySourceData sourceData = m_reachabilitySources[source]; - m_reachabilitySources.erase(source); - - sourceData.minReachability->onReachabilityChanged.remove(sourceData.minReachabilityChangedHandle); - sourceData.maxReachability->onReachabilityChanged.remove(sourceData.maxReachabilityChangedHandle); - - int sourceVertex = m_variableToSourceVertexIndex[source]; - - // Look through all vertices that were reachable from this old source. If any are now definitely unreachable, - // mark them as such. - bool failure = false; - auto checkReachability = [&](int vertex, int parent) - { - if (sourceData.maxReachability->isReachable(vertex)) - { - // This vertex is no longer reachable from the removed source, so might be definitely unreachable now - VarID vertexVar = m_sourceGraphData->get(vertex); - if (vertexVar.isValid() && db->anyPossible(vertexVar, m_requireReachableMask)) - { - EReachabilityDetermination determination = determineReachability(db, vertex); - - if (determination == EReachabilityDetermination::DefinitelyUnreachable) - { - sanityCheckUnreachable(db, vertex); - if (!db->constrainToValues(vertexVar, m_notReachableMask, this, [&](auto params) { return explainNoReachability(params); })) - { - failure = true; - return ETopologySearchResponse::Abort; - } - } - else if (determination == EReachabilityDetermination::PossiblyReachable && !db->anyPossible(vertexVar, m_notReachableMask)) - { - // The vertex is marked definitely reachable, but only possibly reachable in the graph. - // If there is only a single potential source that reaches this vertex, then it must now definitely be a source. - VarID lastReachableSource = VarID::INVALID; - int numReachableSources = 0; - for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) - { - if (it->second.maxReachability->isReachable(vertex)) - { - ++numReachableSources; - lastReachableSource = it->first; - if (numReachableSources > 1) - { - break; - } - } - } - - vxy_assert(numReachableSources >= 1); - if (numReachableSources == 1) - { - if (!db->constrainToValues(lastReachableSource, m_sourceMask, this, [&, source](auto params) { return explainRequiredSource(params, source); })) - { - failure = true; - return ETopologySearchResponse::Abort; - } - } - } - } - return ETopologySearchResponse::Continue; - } - else - { - return ETopologySearchResponse::Skip; - } - }; - m_dfs.search(*m_sourceGraph.get(), sourceVertex, checkReachability); - - return !failure; -} - -void ReachabilityConstraint::updateGraphsForEdgeChange(IVariableDatabase* db, VarID variable) -{ - vxy_assert(!m_inEdgeChange); - vxy_assert(!m_edgeChangeFailure); - vxy_assert(m_edgeChangeDb == nullptr); - - ValueGuard guardEdgeChange(m_inEdgeChange, true); - ValueGuard guardDb(m_edgeChangeDb, db); - - int nodeIndex = m_variableToSourceEdgeIndex[variable]; - - // - // If an edge becomes definitely unblocked, add it to the min graph. - // If an edge becomes definitely blocked, remove it from the max graph. - // - // Sources listen to edge changes and call OnReachabilityChanged for any nodes that become (un)reachable from - // that source. The variables will attempt to be constrained based on their (un)reachability; if they cannot, - // then the bEdgeChangeFailure flag is set. - // - - if (db->anyPossible(variable, m_edgeOpenMask) && !db->anyPossible(variable, m_edgeBlockedMask)) - { - int from, to; - bool bidirectional; - m_edgeGraph->getSourceEdgeForVertex(nodeIndex, from, to, bidirectional); - if (!m_minGraph->hasEdge(from, to)) - { - m_minGraph->addEdge(from, to, db->getTimestamp()); - if (bidirectional) - { - m_minGraph->addEdge(to, from, db->getTimestamp()); - } - } - } - else if (db->anyPossible(variable, m_edgeBlockedMask) && !db->anyPossible(variable, m_edgeOpenMask)) - { - int from, to; - bool bidirectional; - m_edgeGraph->getSourceEdgeForVertex(nodeIndex, from, to, bidirectional); - - if (m_maxGraph->hasEdge(from, to)) - { - // Remove from the explanation graph first, so that we can sync to correct time. - m_explanationGraph->removeEdge(from, to, db->getTimestamp()); - if (bidirectional) - { - m_explanationGraph->removeEdge(to, from, db->getTimestamp()); - } - - m_maxGraph->removeEdge(from, to, db->getTimestamp()); - if (bidirectional) - { - m_maxGraph->removeEdge(to, from, db->getTimestamp()); - } - } - } -} - -void ReachabilityConstraint::onReachabilityChanged(int vertexIndex, VarID sourceVar, bool inMinGraph) +//determine if it's still within the required range +void ReachabilityConstraint::onVertexChanged(int vertexIndex, VarID sourceVar, bool inMinGraph) { vxy_assert(!m_backtracking); vxy_assert(!m_explainingSourceRequirement); @@ -748,10 +111,10 @@ void ReachabilityConstraint::onReachabilityChanged(int vertexIndex, VarID source if (inMinGraph) { // See if this vertex is definitely reachable by any source now - if (determineReachability(m_edgeChangeDb, vertexIndex) == EReachabilityDetermination::DefinitelyReachable) + if (determineValidity(m_edgeChangeDb, vertexIndex) == EValidityDetermination::DefinitelyValid) { VarID var = m_sourceGraphData->get(vertexIndex); - if (var.isValid() && !m_edgeChangeDb->constrainToValues(var, m_requireReachableMask, this)) + if (var.isValid() && !m_edgeChangeDb->constrainToValues(var, m_requireValidMask, this)) { m_edgeChangeFailure = true; } @@ -760,380 +123,16 @@ void ReachabilityConstraint::onReachabilityChanged(int vertexIndex, VarID source else { // vertexIndex became unreachable in the max graph - if (determineReachability(m_edgeChangeDb, vertexIndex) == EReachabilityDetermination::DefinitelyUnreachable) + if (determineValidity(m_edgeChangeDb, vertexIndex) == EValidityDetermination::DefinitelyUnreachable) { VarID var = m_sourceGraphData->get(vertexIndex); sanityCheckUnreachable(m_edgeChangeDb, vertexIndex); - if (var.isValid() && !m_edgeChangeDb->constrainToValues(var, m_notReachableMask, this, [&](auto params) { return explainNoReachability(params); })) + if (var.isValid() && !m_edgeChangeDb->constrainToValues(var, m_invalidMask, this, [&](auto params) { return explainNoReachability(params); })) { m_edgeChangeFailure = true; } } } } - -void ReachabilityConstraint::backtrack(const IVariableDatabase* db, SolverDecisionLevel level) -{ - vxy_assert(!m_edgeChangeFailure); - m_edgeProcessList.clear(); - m_vertexProcessList.clear(); - - ValueGuard backtrackGuard(m_backtracking, true); - - while (!m_backtrackData.empty() && m_backtrackData.back().level > level) - { - for (VarID sourceVar : m_backtrackData.back().reachabilitySourcesRemoved) - { - addSource(sourceVar); - } - m_backtrackData.pop_back(); - } - - // Backtrack any edges added/removed after this point - m_minGraph->backtrackUntil(db->getTimestamp()); - m_maxGraph->backtrackUntil(db->getTimestamp()); - m_explanationGraph->backtrackUntil(db->getTimestamp()); - - #if REACHABILITY_USE_RAMAL_REPS - // Batch-update reachability for all edge changes - { - for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) - { - it->second.maxReachability->refresh(); - it->second.minReachability->refresh(); - } - vxy_assert(!m_edgeChangeFailure); - } - #endif -} - -ReachabilityConstraint::EReachabilityDetermination ReachabilityConstraint::determineReachability(const IVariableDatabase* db, int vertexIndex) -{ - VarID vertexVar = m_sourceGraphData->get(vertexIndex); - for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) - { - if (it->first == vertexVar) - { - // Don't treat reachability as reflective. If a vertex is marked both needing reachability and is a - // reachability source, it needs to be reachable from a DIFFERENT source. - continue; - } - - if (it->second.minReachability->isReachable(vertexIndex)) - { - if (definitelyIsSource(db, it->first)) - { - return EReachabilityDetermination::DefinitelyReachable; - } - else - { - return EReachabilityDetermination::PossiblyReachable; - } - } - else if (it->second.maxReachability->isReachable(vertexIndex)) - { - return EReachabilityDetermination::PossiblyReachable; - } - } - - return EReachabilityDetermination::DefinitelyUnreachable; -} - -// Called whenever an edge is added or removed from the explanation graph, including during backtracking -void ReachabilityConstraint::onExplanationGraphEdgeChange(bool edgeWasAdded, int from, int to) -{ - // Keep the edge capacities in sync. - for (int i = get<0>(m_flowGraphLookup[from]); i < get<1>(m_flowGraphLookup[from]); ++i) - { - if (m_flowGraphEdges[i].endVertex == to) - { - m_flowGraphEdges[i].capacity = edgeWasAdded ? OPEN_EDGE_FLOW : CLOSED_EDGE_FLOW; - return; - } - } - vxy_fail(); -} - -vector ReachabilityConstraint::explainNoReachability(const NarrowingExplanationParams& params) const -{ - // return FSolverVariableDatabase::DefaultExplainer(Params); - - vxy_assert_msg(m_variableToSourceVertexIndex.find(params.propagatedVariable) != m_variableToSourceVertexIndex.end(), "Not a vertex variable?"); - - auto db = params.database; - int conflictVertex = m_variableToSourceVertexIndex.find(params.propagatedVariable)->second; - - vector lits; - lits.push_back(Literal(params.propagatedVariable, m_notReachableMask)); - - static hash_set edgeVarsRecorded; - edgeVarsRecorded.clear(); - - ValueSet visited; - visited.init(m_initialPotentialSources.size(), false); - - // For each source that could possibly exist... - for (int potentialSrcIndex = 0; potentialSrcIndex < m_initialPotentialSources.size(); ++potentialSrcIndex) - { - if (visited[potentialSrcIndex]) - { - continue; - } - visited[potentialSrcIndex] = true; - - VarID potentialSource = m_initialPotentialSources[potentialSrcIndex]; - - int sourceVertex = m_variableToSourceVertexIndex.find(potentialSource)->second; - if (sourceVertex == conflictVertex) - { - // Reachability sources cannot provide reachability to themselves - continue; - } - - // If this is currently a potential source... - if (db->getPotentialValues(potentialSource).anyPossible(m_sourceMask)) - { - // - // Find the minimum cut of edges that would make this reachable - // - - // Temporarily rewind the explanation graph to this time. - // This will trigger OnExplanationGraphEdgeChange() for any edges re-added, so that FlowGraphEdges - // will be the same state as when we processed the input variable. - - m_explanationGraph->rewindUntil(params.timestamp); - - vxy_sanity(!TopologySearchAlgorithm::canReach(m_explanationGraph, sourceVertex, conflictVertex)); - - // Find the minimum cut in the maximum flow graph. This will correspond to edges that are disabled, because - // A) we know that sourceVertex can't reach conflictVertex without going through a disabled edge - // B) blocked edges are set to a flow capacity of 1, and blocked edges have infinite flow - vector> cutEdges; - m_maxFlowAlgo.getMaxFlow(*m_sourceGraph.get(), sourceVertex, conflictVertex, m_flowGraphEdges, m_flowGraphLookup, &cutEdges); - vxy_assert(!cutEdges.empty()); - - // Now that we've found the cut, bring the explanation graph back to current state. - m_explanationGraph->fastForward(); - - for (tuple& edge : cutEdges) - { - int edgeNode = m_edgeGraph->getVertexForSourceEdge(get<0>(edge), get<1>(edge)); - VarID edgeVar = m_edgeGraphData->get(edgeNode); - if (edgeVarsRecorded.find(edgeVar) == edgeVarsRecorded.end()) - { - edgeVarsRecorded.insert(edgeVar); - - vxy_assert(!db->anyPossible(edgeVar, m_edgeOpenMask)); - lits.push_back(Literal(edgeVar, m_edgeOpenMask)); - } - } - - // For every other potential source, see if this graph also holds. It holds if the other source is on the - // same side as this source, hence would have to cross the same edge boundary. - for (int j = potentialSrcIndex + 1; j < m_initialPotentialSources.size(); ++j) - { - if (visited[j]) - { - continue; - } - - int vertex = m_variableToSourceVertexIndex.find(potentialSource)->second; - if (vertex == conflictVertex) - { - continue; - } - - if (db->getPotentialValues(m_initialPotentialSources[j]).anyPossible(m_sourceMask)) - { - if (!m_maxFlowAlgo.onSinkSide(vertex, m_flowGraphEdges, m_flowGraphLookup)) - { - visited[j] = true; - } - } - } - } - // Not currently a potential source. For now, the conservative explanation is that we'd be able to reach if it - // was. - else - { - lits.push_back(Literal(potentialSource, m_sourceMask)); - } - } - - return lits; -} - -vector ReachabilityConstraint::explainRequiredSource(const NarrowingExplanationParams& params, VarID removedSource) -{ - vxy_assert(!m_explainingSourceRequirement); - ValueGuard guard(m_explainingSourceRequirement, true); - - VarID sourceVar = params.propagatedVariable; - int sourceVertex = m_variableToSourceVertexIndex[sourceVar]; - - auto db = params.database; - - vector lits; - lits.push_back(Literal(sourceVar, m_sourceMask)); - - m_maxGraph->rewindUntil(params.timestamp); - - #if REACHABILITY_USE_RAMAL_REPS - { - // Batch-update to rewound graph state - for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) - { - it->second.maxReachability->refresh(); - } - } - #endif - - // Create any sources that might've gotten removed since this happened. - // (We'll clean them up after) - vector tempSources; - for (VarID potentialSource : m_initialPotentialSources) - { - if (db->anyPossible(potentialSource, m_sourceMask)) - { - if (m_reachabilitySources.find(potentialSource) == m_reachabilitySources.end()) - { - tempSources.push_back(potentialSource); - - int vertexIndex = m_variableToSourceVertexIndex[potentialSource]; - - ReachabilitySourceData data; - #if REACHABILITY_USE_RAMAL_REPS - data.maxReachability = make_shared(m_maxGraph, false, false, false); - #else - Data.maxReachability = make_shared(MaxGraph); - #endif - data.maxReachability->initialize(vertexIndex, &m_reachabilityEdgeLookup, m_totalNumEdges); - - m_reachabilitySources[potentialSource] = data; - } - } - else if (potentialSource != sourceVar) - { - lits.push_back(Literal(potentialSource, m_sourceMask)); - } - } - - int removedSourceLitIdx = -1; - if (removedSource.isValid()) - { - // This became a required source because RemovedSource was removed, and some definitely-reachable vertices were - // only reachable by this source. - vxy_assert(!db->anyPossible(removedSource, m_sourceMask)); - removedSourceLitIdx = indexOfPredicate(lits.begin(), lits.end(), [&](auto& lit) { return lit.variable == removedSource; }); - vxy_assert(removedSourceLitIdx >= 0); - } - - // - // This became a required source because some variable(s) were marked as required, and we are the only - // source that can reach them. Find those variables. - // - bool foundSupports = false; - auto& ourReachability = m_reachabilitySources[sourceVar].maxReachability; - auto searchCallback = [&](int vertex, int parent, int edgeIndex) - { - if (ourReachability->isReachable(vertex)) - { - VarID vertexVar = m_sourceGraphData->get(vertex); - if (!db->anyPossible(vertexVar, m_notReachableMask)) - { - bool reachableFromAnotherSource = false; - for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) - { - if (it->first != sourceVar && it->first != vertexVar && it->second.maxReachability->isReachable(vertex)) - { - reachableFromAnotherSource = true; - break; - } - } - - if (!reachableFromAnotherSource) - { - vxy_assert(m_reachabilitySources[sourceVar].maxReachability->isReachable(vertex)); - // make sure we don't add the same literal twice! - auto found = find_if(lits.begin(), lits.end(), [&](auto& lit) { return lit.variable == vertexVar; }); - if (found != lits.end()) - { - vxy_assert(found->variable == vertexVar); - found->values.include(m_notReachableMask); - } - else - { - lits.push_back(Literal(vertexVar, m_notReachableMask)); - } - foundSupports = true; - } - } - return ETopologySearchResponse::Continue; - } - else - { - return ETopologySearchResponse::Skip; - } - }; - m_dfs.search(*m_sourceGraph.get(), m_variableToSourceVertexIndex[sourceVar], searchCallback); - vxy_assert(foundSupports); - - for (VarID tempSource : tempSources) - { - m_reachabilitySources.erase(tempSource); - } - - m_maxGraph->fastForward(); - return lits; -} - - -void ReachabilityConstraint::sanityCheckUnreachable(IVariableDatabase* db, int vertexIndex) -{ - #if SANITY_CHECKS - // For each source that could possibly exist... - for (VarID potentialSource : m_initialPotentialSources) - { - int sourceVertex = m_variableToSourceVertexIndex[potentialSource]; - // If this is currently a potential source... - if (db->getPotentialValues(potentialSource).anyPossible(m_sourceMask)) - { - vxy_assert(!TopologySearchAlgorithm::canReach(m_maxGraph, sourceVertex, vertexIndex)); - } - } - #endif -} - - -vector ReachabilityConstraint::getConstrainingVariables() const -{ - vector out; - for (int i = 0; i < m_sourceGraph->getNumVertices(); ++i) - { - VarID var = m_sourceGraphData->get(i); - if (var.isValid()) - { - out.push_back(var); - } - } - - for (int i = 0; i < m_edgeGraph->getNumVertices(); ++i) - { - VarID var = m_edgeGraphData->get(i); - if (var.isValid()) - { - out.push_back(var); - } - } - - return out; -} - -bool ReachabilityConstraint::checkConflicting(IVariableDatabase* db) const -{ - // TODO - return false; -} - #undef SANITY_CHECKS diff --git a/vertexy/src/private/constraints/ShortestPathConstraint.cpp b/vertexy/src/private/constraints/ShortestPathConstraint.cpp new file mode 100644 index 0000000..3a696ac --- /dev/null +++ b/vertexy/src/private/constraints/ShortestPathConstraint.cpp @@ -0,0 +1,605 @@ +// Copyright Proletariat, Inc. All Rights Reserved. +#include "constraints/ShortestPathConstraint.h" + +#include "variable/IVariableDatabase.h" +#include "topology/GraphRelations.h" + +using namespace Vertexy; + +#define SANITY_CHECKS VERTEXY_SANITY_CHECKS + +static constexpr int OPEN_EDGE_FLOW = INT_MAX >> 1; +static constexpr int CLOSED_EDGE_FLOW = 1; +static constexpr bool USE_RAMAL_REPS_BATCHING = true; + +ShortestPathConstraint* ShortestPathConstraint::ShortestPathFactory::construct( + const ConstraintFactoryParams& params, + const shared_ptr>& vertexData, + const vector& sourceValues, + const vector& needReachableValues, + const shared_ptr>& edgeData, + const vector& edgeBlockedValues, + EConstraintOperator op, + int distance) +{ + // Get an example graph variable + VarID graphVar; + for (int i = 0; i < vertexData->getSource()->getNumVertices(); ++i) + { + if (vertexData->get(i).isValid()) + { + graphVar = vertexData->get(i); + break; + } + } + vxy_assert(graphVar.isValid()); + + // Get an example edge variable + VarID edgeVar; + for (int i = 0; i < edgeData->getSource()->getNumVertices(); ++i) + { + if (edgeData->get(i).isValid()) + { + edgeVar = edgeData->get(i); + break; + } + } + vxy_assert(edgeVar.isValid()); + + ValueSet sourceMask = params.valuesToInternal(graphVar, sourceValues); + ValueSet needReachableMask = params.valuesToInternal(graphVar, needReachableValues); + ValueSet edgeBlockedMask = params.valuesToInternal(edgeVar, edgeBlockedValues); + + return new ShortestPathConstraint(params, vertexData, sourceMask, needReachableMask, edgeData, edgeBlockedMask, op, distance); +} + +ShortestPathConstraint::ShortestPathConstraint( + const ConstraintFactoryParams& params, + const shared_ptr>& sourceGraphData, + const ValueSet& sourceMask, + const ValueSet& requireReachableMask, + const shared_ptr>& edgeGraphData, + const ValueSet& edgeBlockedMask, + EConstraintOperator op, + int distance) + : TopologyConnectionConstraint(params, sourceGraphData, sourceMask, requireReachableMask, edgeGraphData, edgeBlockedMask) + , m_op(op) + , m_distance(distance) +{ + vxy_assert(m_op != EConstraintOperator::NotEqual); //NotEqual not supported + if (m_op == EConstraintOperator::GreaterThan || m_op == EConstraintOperator::GreaterThanEq) + { + this->m_explanationMinGraph = make_shared(); + } +} + +void ShortestPathConstraint::onInitialArcConsistency(IVariableDatabase* db) +{ + m_lastValidTimestamp.clear(); +} + +bool ShortestPathConstraint::isValidDistance(const IVariableDatabase* db, int dist) const +{ + switch (m_op) + { + case EConstraintOperator::GreaterThan: + return dist > m_distance; + case EConstraintOperator::GreaterThanEq: + return dist >= m_distance; + case EConstraintOperator::LessThan: + return dist < m_distance; + case EConstraintOperator::LessThanEq: + return dist <= m_distance; + } + + vxy_assert(false); //NotEqual not supported + return false; +} + +//is possibly reachable +bool ShortestPathConstraint::isPossiblyValid(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex) +{ + // we do not need to check for reachability here because we always call isPossiblyReachable before calling this + if (m_op == EConstraintOperator::GreaterThan || m_op == EConstraintOperator::GreaterThanEq) + { + if (src.minReachability->isReachable(vertex)) + { + if (!isValidDistance(db, src.minReachability->getDistance(vertex))) + { + // the shortest path is too short, so our vertex is definitely unreachable (ie it cannot be a target) + removeTimestampToCommit(db, src.vertex, vertex); + return false; + } + else + { + addTimestampToCommit(db, src.vertex, vertex); + return true; + } + } + else if (src.maxReachability->isReachable(vertex)) + { + return true; + } + } + else + { + if (src.minReachability->isReachable(vertex) && isValidDistance(db, src.minReachability->getDistance(vertex))) + { + return true; + } + else if (src.maxReachability->isReachable(vertex)) + { + if (!isValidDistance(db, src.maxReachability->getDistance(vertex))) + { + removeTimestampToCommit(db, src.vertex, vertex); + return false; + } + + addTimestampToCommit(db, src.vertex, vertex); + return true; + } + } + return false; +} + +TopologyConnectionConstraint::EValidityDetermination ShortestPathConstraint::determineValidityHelper( + const IVariableDatabase* db, + const ReachabilitySourceData& src, + int vertex, + VarID srcVertex) +{ + if (m_op == EConstraintOperator::GreaterThan || m_op == EConstraintOperator::GreaterThanEq) + { + if (src.minReachability->isReachable(vertex)) + { + if (!isValidDistance(db, src.minReachability->getDistance(vertex))) + { + // the shortest path is too short, so our vertex is definitely unreachable (ie it cannot be a target) + removeTimestampToCommit(db, src.vertex, vertex); + return EValidityDetermination::DefinitelyInvalid; + } + + addTimestampToCommit(db, src.vertex, vertex); + if (definitelyIsSource(db, srcVertex)) + { + return EValidityDetermination::DefinitelyValid; + } + else + { + return EValidityDetermination::PossiblyValid; + } + } + else if (src.maxReachability->isReachable(vertex)) + { + return EValidityDetermination::PossiblyValid; + } + } + else + { + if (src.minReachability->isReachable(vertex) && isValidDistance(db, src.minReachability->getDistance(vertex))) + { + if (definitelyIsSource(db, srcVertex)) + { + return EValidityDetermination::DefinitelyValid; + } + else + { + return EValidityDetermination::PossiblyValid; + } + } + else if (src.maxReachability->isReachable(vertex)) + { + if (!isValidDistance(db, src.maxReachability->getDistance(vertex))) + { + // undo any changes we have made during the current timestamp while processing all changes + removeTimestampToCommit(db, src.vertex, vertex); + return EValidityDetermination::DefinitelyInvalid; + } + + addTimestampToCommit(db, src.vertex, vertex); + return EValidityDetermination::PossiblyValid; + } + } + + return EValidityDetermination::DefinitelyUnreachable; +} + +shared_ptr> ShortestPathConstraint::makeTopology(const shared_ptr& graph) const +{ + return make_shared(graph, USE_RAMAL_REPS_BATCHING, false, true); +} + +EventListenerHandle ShortestPathConstraint::addMinCallback(RamalRepsType& minReachable, const IVariableDatabase* db, VarID source) +{ + return minReachable.onDistanceChanged.add([&](int changedVertex, int distance) + { + if (!m_backtracking && !m_explainingSourceRequirement) + { + onVertexChanged(changedVertex, source, true); + } + }); +} + +EventListenerHandle ShortestPathConstraint::addMaxCallback(RamalRepsType& maxReachable, const IVariableDatabase* db, VarID source) +{ + return maxReachable.onDistanceChanged.add([&](int changedVertex, int distance) + { + if (!m_backtracking && !m_explainingSourceRequirement) + { + onVertexChanged(changedVertex, source, false); + } + }); +} + +vector Vertexy::ShortestPathConstraint::explainInvalid(const NarrowingExplanationParams& params) +{ + // if we are here, it means that the path was reachable, but we marked it as invalid because of the distance constraint + vxy_sanity_msg(m_variableToSourceVertexIndex.find(params.propagatedVariable) != m_variableToSourceVertexIndex.end(), "Not a vertex variable?"); + + auto db = params.database; + int conflictVertex = m_variableToSourceVertexIndex.find(params.propagatedVariable)->second; + + vector lits; + lits.push_back(Literal(params.propagatedVariable, m_invalidMask)); + + static hash_set edgeVarsRecorded; + edgeVarsRecorded.clear(); + + ValueSet visited; + visited.init(m_initialPotentialSources.size(), false); + + const bool isGreaterOp = m_op == EConstraintOperator::GreaterThan || m_op == EConstraintOperator::GreaterThanEq; + { + bool hasAnyTimestamp = false; + auto foundLastTimestamp = m_lastValidTimestamp.find(conflictVertex); + if (foundLastTimestamp != m_lastValidTimestamp.end()) + { + for (auto& it : foundLastTimestamp->second) + { + if (it.second.hasValue()) + { + hasAnyTimestamp = true; + break; + } + } + } + + if (!hasAnyTimestamp) + { + // there was never a point where this vertex was valid + // the best explanation is that this edge is too far away / too close from any sources + for (int potentialSrcIndex = 0; potentialSrcIndex < m_initialPotentialSources.size(); ++potentialSrcIndex) + { + VarID potentialSource = m_initialPotentialSources[potentialSrcIndex]; + int sourceVertex = m_variableToSourceVertexIndex.find(potentialSource)->second; + if (sourceVertex == conflictVertex) + { + continue; + } + + if (!db->getPotentialValues(potentialSource).anyPossible(m_sourceMask)) + { + // best explanation is that any source that isn't a source currently would make it reachable + lits.push_back(Literal(potentialSource, m_sourceMask)); + } + } + return lits; + } + } + + bool foundAny = false; + bool hasUnprocessedSources = false; + if (isGreaterOp) + { + m_explanationMinGraph->rewindUntil(params.timestamp); + } + // For each source that could possibly exist... + for (int potentialSrcIndex = 0; potentialSrcIndex < m_initialPotentialSources.size(); ++potentialSrcIndex) + { + VarID potentialSource = m_initialPotentialSources[potentialSrcIndex]; + + int sourceVertex = m_variableToSourceVertexIndex.find(potentialSource)->second; + if (sourceVertex == conflictVertex) + { + // Reachability sources cannot provide reachability to themselves + continue; + } + + // check if it's reachable + auto reachabilitySource = m_reachabilitySources.find(potentialSource); + SolverTimestamp valueToRewind = -1; + { + auto& lastValid = m_lastValidTimestamp[conflictVertex].find(sourceVertex); + if (lastValid == m_lastValidTimestamp[conflictVertex].end() || !lastValid->second.hasValue()) + { + // there was never a possible path for the source + // ignore this when running shortest path + visited[potentialSrcIndex] = true; + continue; + } + valueToRewind = lastValid->second.getTimestamp(); + } + + if (db->getPotentialValues(potentialSource).anyPossible(m_sourceMask) || reachabilitySource != m_reachabilitySources.end()) + { + vector path; + // so this is a bit confusing, bear with me: + auto timestampToCheck = isGreaterOp ? valueToRewind : params.timestamp; + if (isGreaterOp) + { + // if this is a greater than op, the only possibility for it to be invalid is if the min graph has a path that is lower + // than our constraint. In that case, we want to find the path that is too short currently (on the timestamp of the triggered + // explanation), and compare each edge against the last valid version of it + // any edge that was blocked but now is not will get into the explanation + if (!m_shortestPathAlgo.find(*m_explanationMinGraph, sourceVertex, conflictVertex, path)) + { + // it's actually unreachable right now, so let's let the reachability explainer kick in (by not setting visited = true) + hasUnprocessedSources = true; + continue; + } + } + else + { + // in case this is a less than op, the only possibility for it to be invalid is if the max graph has a path that is too long + // so, in that case, what we want to do is rewind our explanation max graph to the last time it was valid, and get the shortest + // path at that point. Then, we can compare each edge against the timestamp of the conflict, and set to open any edge that + // is now blocked + m_explanationMaxGraph->rewindUntil(valueToRewind); + auto found = m_shortestPathAlgo.find(*m_explanationMaxGraph, sourceVertex, conflictVertex, path); + vxy_assert(found); + // TODO optimize: we can sort the values to rewind in such a way that we can do many partial rewinds instead of rewinding, + // and then fast forwarding every time + m_explanationMaxGraph->fastForward(); + vxy_assert(isValidDistance(db, path.size() - 1)); + } + + foundAny = true; + visited[potentialSrcIndex] = true; + + auto& targetMask = isGreaterOp ? m_edgeBlockedMask : m_edgeOpenMask; + bool changedEdge = false; + for (int i = 0; i < (path.size() - 1); ++i) + { + // mark all edges that don't currently have the targetMask + int edge = m_edgeGraph->getVertexForSourceEdge(path[i], path[i + 1]); + auto edgeVar = m_edgeGraphData->get(edge); + if (edgeVarsRecorded.find(edgeVar) == edgeVarsRecorded.end()) + { + if (!db->getValueBefore(edgeVar, timestampToCheck).anyPossible(targetMask)) + { + edgeVarsRecorded.insert(edgeVar); + lits.push_back(Literal(edgeVar, targetMask)); + changedEdge = true; + } + } + else + { + changedEdge = true; + } + } + vxy_assert(changedEdge); + } + else + { + // Not currently a potential source. It's safe to assume that it would be valid in case that was a potention source + // because we are only at this point if valueToRewind was set (so there was a moment in time where this source was a valid + // source for the target) + lits.push_back(Literal(potentialSource, m_sourceMask)); + visited[potentialSrcIndex] = true; + foundAny = true; + } + } + vxy_assert(foundAny); + if (isGreaterOp) + { + m_explanationMinGraph->fastForward(); + } + + if (hasUnprocessedSources) + { + // for all other sources, run the reachability explainer + auto otherLits = explainNoReachability(params, &visited); + // we can skip the first one since it's always the propagatedVariable + for (int i = 1; i < otherLits.size(); i++) + { + const auto& lit = otherLits[i]; + if (edgeVarsRecorded.find(lit.variable) == edgeVarsRecorded.end()) + { + // we don't need to add that edge to the edgeVarsRecorded because it was already deduped + lits.push_back(lit); + } + } + } + + return lits; +} + +void Vertexy::ShortestPathConstraint::sanityCheckInvalid(IVariableDatabase* db, int vertexIndex) +{ + #if SANITY_CHECKS + // For each source that could possibly exist... + bool foundInvalid = false; + for (VarID potentialSource : m_initialPotentialSources) + { + int sourceVertex = m_variableToSourceVertexIndex[potentialSource]; + // If this is currently a potential source... + if (db->getPotentialValues(potentialSource).anyPossible(m_sourceMask) || m_reachabilitySources.find(potentialSource) != m_reachabilitySources.end()) + { + vector path; + if (m_op == EConstraintOperator::GreaterThan || m_op == EConstraintOperator::GreaterThanEq) + { + if (m_shortestPathAlgo.find(*m_explanationMinGraph, sourceVertex, vertexIndex, path)) + { + foundInvalid = true; + vxy_assert(!isValidDistance(db, path.size() - 1)); + } + } + else + { + if (m_shortestPathAlgo.find(*m_explanationMaxGraph, sourceVertex, vertexIndex, path)) + { + foundInvalid = true; + vxy_assert(!isValidDistance(db, path.size() - 1)); + } + } + } + } + vxy_assert(foundInvalid); + #endif +} + +void Vertexy::ShortestPathConstraint::createTempSourceData(ReachabilitySourceData& data, int vertexIndex) const +{ + TopologyConnectionConstraint::createTempSourceData(data, vertexIndex); +#if REACHABILITY_USE_RAMAL_REPS + data.minReachability = make_shared(m_minGraph, false, false, false); +#else + Data.minReachability = make_shared(MinGraph); +#endif + data.minReachability->initialize(vertexIndex, &m_reachabilityEdgeLookup, m_totalNumEdges); +} + +void ShortestPathConstraint::onVertexChanged(int vertexIndex, VarID sourceVar, bool inMinGraph) +{ + vxy_assert(!m_backtracking); + vxy_assert(!m_explainingSourceRequirement); + + vxy_assert(m_edgeChangeDb != nullptr); + vxy_assert(m_inEdgeChange); + + if (m_edgeChangeFailure) + { + // We already failed - avoid further failures that could confuse the conflict analyzer + return; + } + + m_processingVertices = true; + m_queuedVertexChanges.insert(vertexIndex); + auto reachability = determineValidity(m_edgeChangeDb, vertexIndex); + + if (reachability == EValidityDetermination::DefinitelyUnreachable) + { + // vertexIndex became unreachable in the max graph + VarID var = m_sourceGraphData->get(vertexIndex); + // we cannot sanity check now because not all RamalReps have been updated - see processQueuedVertexChanges + sanityCheckUnreachable(m_edgeChangeDb, vertexIndex); + + if (var.isValid() && !m_edgeChangeDb->constrainToValues(var, m_invalidMask, this, [&](auto params) { return explainNoReachability(params); })) + { + m_edgeChangeFailure = true; + } + } + m_processingVertices = false; +} + +void ShortestPathConstraint::backtrack(const IVariableDatabase* db, SolverDecisionLevel level) +{ + auto stamp = db->getTimestamp(); + TopologyConnectionConstraint::backtrack(db, level); + + // TODO optimize: make a better data structure so we don't need to touch all vertices just to backtrack the ones that can be backtracked + for (auto& vertexData : m_lastValidTimestamp) + { + for (auto& srcData : vertexData.second) + { + srcData.second.backtrackUntil(stamp); + } + } +} + +void ShortestPathConstraint::commitValidTimestamps(const IVariableDatabase* db) +{ + for (auto& toCommitDest : m_validTimestampsToCommit) + { + auto& found = m_lastValidTimestamp.find(toCommitDest.first); + auto validTimestamp = m_lastValidTimestamp.insert(toCommitDest.first).first; + for (auto& value : toCommitDest.second) + { + validTimestamp->second.insert(value.first).first->second.set(value.second, value.second); + } + } +} + +void ShortestPathConstraint::onEdgeChangeFailure(const IVariableDatabase* db) +{ + m_queuedVertexChanges.clear(); + m_validTimestampsToCommit.clear(); +} + +void ShortestPathConstraint::onEdgeChangeSuccess(const IVariableDatabase* db) +{ + commitValidTimestamps(db); + m_validTimestampsToCommit.clear(); +} + +void ShortestPathConstraint::addTimestampToCommit(const IVariableDatabase* db, int sourceVertex, int destVertex) +{ + if (m_explainingSourceRequirement || m_processingVertices) + { + return; + } + + #if VERTEXY_SANITY_CHECKS + auto timestamp = db->getTimestamp(); + if (m_lastValidTimestamp.find(destVertex) != m_lastValidTimestamp.end() && + m_lastValidTimestamp[destVertex].find(sourceVertex) != m_lastValidTimestamp[destVertex].end()) + { + auto& val = m_lastValidTimestamp[destVertex][sourceVertex]; + if (val.hasValue()) + { + vxy_assert(val.getTimestamp() <= timestamp); + } + } + #endif + + if (m_validTimestampsToCommit.find(destVertex) == m_validTimestampsToCommit.end()) + { + m_validTimestampsToCommit[destVertex] = hash_map(); + } + + m_validTimestampsToCommit[destVertex][sourceVertex] = timestamp; +} + +void ShortestPathConstraint::removeTimestampToCommit(const IVariableDatabase* db, int sourceVertex, int destVertex) +{ + m_validTimestampsToCommit.erase(sourceVertex); +} + +void Vertexy::ShortestPathConstraint::processQueuedVertexChanges(IVariableDatabase* db) +{ + m_validTimestampsToCommit.clear(); + vxy_assert(m_processingVertices == false); + for (auto vertexIndex : m_queuedVertexChanges) + { + // we need to run determineValidity again for all these vertices so we can update our valid timestamps + auto validity = determineValidity(db, vertexIndex); + if (validity == EValidityDetermination::DefinitelyValid) + { + // vertexIndex became unreachable in the max graph + VarID var = m_sourceGraphData->get(vertexIndex); + + if (var.isValid() && !db->constrainToValues(var, m_requireValidMask, this)) + { + m_edgeChangeFailure = true; + break; + } + } + else if (validity == EValidityDetermination::DefinitelyInvalid) + { + // vertexIndex became unreachable in the max graph + VarID var = m_sourceGraphData->get(vertexIndex); + // we cannot sanity check now because not all RamalReps have been updated - see processQueuedVertexChanges + sanityCheckInvalid(db, vertexIndex); + + if (var.isValid() && !db->constrainToValues(var, m_invalidMask, this, [&](auto params) { return explainInvalid(params); })) + { + m_edgeChangeFailure = true; + break; + } + } + } + m_queuedVertexChanges.clear(); +} + + +#undef SANITY_CHECKS diff --git a/vertexy/src/private/constraints/TopologyConnectionConstraint.cpp b/vertexy/src/private/constraints/TopologyConnectionConstraint.cpp new file mode 100644 index 0000000..ade2ba5 --- /dev/null +++ b/vertexy/src/private/constraints/TopologyConnectionConstraint.cpp @@ -0,0 +1,1143 @@ +// Copyright Proletariat, Inc. All Rights Reserved. +#include "constraints/TopologyConnectionConstraint.h" + +#include "variable/IVariableDatabase.h" +#include "topology/GraphRelations.h" + +using namespace Vertexy; + +#define SANITY_CHECKS VERTEXY_SANITY_CHECKS + +static constexpr int OPEN_EDGE_FLOW = INT_MAX >> 1; +static constexpr int CLOSED_EDGE_FLOW = 1; +static constexpr bool USE_RAMAL_REPS_BATCHING = true; + +TopologyConnectionConstraint::TopologyConnectionConstraint( + const ConstraintFactoryParams& params, + const shared_ptr>& sourceGraphData, + const ValueSet& sourceMask, + const ValueSet& requireReachableMask, + const shared_ptr>& edgeGraphData, + const ValueSet& edgeBlockedMask) + : IBacktrackingSolverConstraint(params) //ApplyGraphRelation(Params, SourceGraphData, EdgeGraphData)) + , m_edgeWatcher(*this) + , m_sourceGraphData(sourceGraphData) + , m_sourceGraph(sourceGraphData->getSource()) + , m_edgeGraphData(edgeGraphData) + , m_edgeGraph(edgeGraphData->getSource()->getImplementation()) + , m_minGraph(make_shared()) + , m_maxGraph(make_shared()) + , m_explanationMaxGraph(make_shared()) + , m_explanationMinGraph(nullptr) + , m_sourceMask(sourceMask) + , m_requireValidMask(requireReachableMask) + , m_edgeBlockedMask(edgeBlockedMask) +{ + m_notSourceMask = sourceMask.inverted(); + m_invalidMask = requireReachableMask.inverted(); + m_edgeOpenMask = edgeBlockedMask.inverted(); + + for (int i = 0; i < m_sourceGraph->getNumVertices(); ++i) + { + VarID var = sourceGraphData->get(i); + if (var.isValid()) + { + m_variableToSourceVertexIndex[var] = i; + } + } + + vxy_assert(m_edgeGraph->getSource() == m_sourceGraph); + for (int i = 0; i < m_edgeGraph->getNumVertices(); ++i) + { + VarID var = edgeGraphData->get(i); + if (var.isValid()) + { + m_variableToSourceEdgeIndex[var] = i; + } + } +} + +bool TopologyConnectionConstraint::getGraphRelations(const vector& literals, ConstraintGraphRelationInfo& outRelations) const +{ + // First search through all provided literals to find the minimum graph vertex. + // Note: some vertices will be edges, some will be tiles. + int minGraphVertex = m_sourceGraph->getNumVertices(); + + vector vertices; + vector isEdgeNode; + + vertices.reserve(literals.size()); + isEdgeNode.reserve(literals.size()); + + for (auto& lit : literals) + { + int graphVertex = m_sourceGraphData->indexOf(lit.variable); + if (graphVertex < 0) + { + int edgeNode = m_edgeGraphData->indexOf(lit.variable); + vxy_assert(edgeNode >= 0); + + vertices.push_back(edgeNode); + isEdgeNode.push_back(true); + + int edgeFrom, edgeTo; + bool bidirectional; + m_edgeGraph->getSourceEdgeForVertex(edgeNode, edgeFrom, edgeTo, bidirectional); + + graphVertex = min(edgeFrom, edgeTo); + } + else + { + vertices.push_back(graphVertex); + isEdgeNode.push_back(false); + } + vxy_assert(graphVertex >= 0); + minGraphVertex = min(graphVertex, minGraphVertex); + } + + // We always provide relations in terms of the source graph. + // Relations are anchored to the minimum vertex ID found (maps to top-leftmost in a grid graph). + outRelations.reset(m_sourceGraph, minGraphVertex); + + // create the relations! + outRelations.reserve(literals.size()); + for (int i = 0; i != literals.size(); ++i) + { + bool isEdge = isEdgeNode[i]; + + if (!isEdge) + { + int vertex = vertices[i]; + if (vertex != minGraphVertex) + { + TopologyLink link; + if (!m_sourceGraph->getTopologyLink(minGraphVertex, vertex, link)) + { + // no path specified in graph + // TODO: assert? + outRelations.clear(); + return false; + } + + auto linkRel = make_shared>(m_sourceGraphData, link); + outRelations.addRelation(m_sourceGraphData->get(vertex), linkRel); + } + else + { + auto selfRel = make_shared>(m_sourceGraphData); + outRelations.addRelation(m_sourceGraphData->get(vertex), selfRel); + } + } + else + { + int edgeNode = vertices[i]; + + // edge variable: get the source node if the edge + int edgeOrigin, edgeDestination; + bool bidirectional; + m_edgeGraph->getSourceEdgeForVertex(edgeNode, edgeOrigin, edgeDestination, bidirectional); + + int nodeEdgeIndex = -1; + for (int e = 0; e < m_sourceGraph->getNumOutgoing(edgeOrigin); ++e) + { + if (int testDest; m_sourceGraph->getOutgoingDestination(edgeOrigin, e, testDest) && testDest == edgeDestination) + { + nodeEdgeIndex = e; + break; + } + } + if (nodeEdgeIndex < 0) + { + vxy_assert_msg(false, "Edge node %d has source graph node origin %d, but can't find edgeIndex in source graph!", edgeNode, edgeOrigin); + outRelations.clear(); + return false; + } + + auto nodeToEdgeNodeRel = make_shared>(m_sourceGraph, m_edgeGraph, nodeEdgeIndex); + auto nodeToEdgeVarRel = nodeToEdgeNodeRel->map(make_shared>(m_edgeGraphData)); + + if (edgeOrigin != minGraphVertex) + { + TopologyLink link; + if (!m_sourceGraph->getTopologyLink(minGraphVertex, edgeOrigin, link)) + { + vxy_assert_msg(false, "expected link between vertices %d -> %d", minGraphVertex, edgeOrigin); + outRelations.clear(); + return false; + } + + auto linkRel = make_shared(m_sourceGraph, link); + outRelations.addRelation(m_edgeGraphData->get(edgeNode), linkRel->map(nodeToEdgeVarRel)); + } + else + { + outRelations.addRelation(m_edgeGraphData->get(edgeNode), nodeToEdgeVarRel); + } + } + } + + vxy_assert(outRelations.relations.size() == literals.size()); + return true; +} + +bool TopologyConnectionConstraint::initialize(IVariableDatabase* db) +{ + // Add all vertices to min/max graphs + for (int vertexIndex = 0; vertexIndex < m_sourceGraph->getNumVertices(); ++vertexIndex) + { + VarID vertexVar = m_sourceGraphData->get(vertexIndex); + + int addedIdx = m_maxGraph->addVertex(); + vxy_assert(addedIdx == vertexIndex); + + addedIdx = m_minGraph->addVertex(); + vxy_assert(addedIdx == vertexIndex); + + addedIdx = m_explanationMaxGraph->addVertex(); + vxy_assert(addedIdx == vertexIndex); + + if (m_explanationMinGraph) + { + addedIdx = m_explanationMinGraph->addVertex(); + vxy_assert(addedIdx == vertexIndex); + } + if (vertexVar.isValid()) + { + m_vertexWatchHandles[vertexVar] = db->addVariableWatch(vertexVar, EVariableWatchType::WatchModification, this); + } + } + + hash_map> edgeCapacities; + + m_totalNumEdges = 0; + + // Add all definitely-open edges to the min graph, and all possibly-open edges to the max graph + m_reachabilityEdgeLookup.resize(m_sourceGraph->getNumVertices()); + for (int sourceVertex = 0; sourceVertex < m_sourceGraph->getNumVertices(); ++sourceVertex) + { + auto foundVertexEdges = edgeCapacities.find(sourceVertex); + if (foundVertexEdges == edgeCapacities.end()) + { + foundVertexEdges = edgeCapacities.insert(sourceVertex).first; + } + + m_reachabilityEdgeLookup[sourceVertex].reserve(m_sourceGraph->getNumOutgoing(sourceVertex)); + for (int edgeIndex = 0; edgeIndex < m_sourceGraph->getNumOutgoing(sourceVertex); ++edgeIndex) + { + int destVertex; + if (m_sourceGraph->getOutgoingDestination(sourceVertex, edgeIndex, destVertex)) + { + m_reachabilityEdgeLookup[sourceVertex].push_back(make_tuple(destVertex, m_totalNumEdges)); + ++m_totalNumEdges; + + int edgeNode = m_edgeGraph->getVertexForSourceEdge(sourceVertex, destVertex); + vxy_assert(edgeNode >= 0); + VarID edgeVar = m_edgeGraphData->get(edgeNode); + + bool edgeIsClosed = true; + if (edgeVar.isValid()) + { + if (definitelyOpenEdge(db, edgeVar)) + { + edgeIsClosed = false; + + m_minGraph->initEdge(sourceVertex, destVertex); + m_maxGraph->initEdge(sourceVertex, destVertex); + m_explanationMaxGraph->initEdge(sourceVertex, destVertex); + if (m_explanationMinGraph) + { + m_explanationMinGraph->initEdge(sourceVertex, destVertex); + } + } + else if (possiblyOpenEdge(db, edgeVar)) + { + edgeIsClosed = false; + + if (m_edgeWatchHandles.find(edgeVar) == m_edgeWatchHandles.end()) + { + m_edgeWatchHandles[edgeVar] = db->addVariableWatch(edgeVar, EVariableWatchType::WatchModification, &m_edgeWatcher); + } + m_maxGraph->initEdge(sourceVertex, destVertex); + m_explanationMaxGraph->initEdge(sourceVertex, destVertex); + } + } + else + { + edgeIsClosed = false; + + // No variable for this edge, so should always exist + m_minGraph->initEdge(sourceVertex, destVertex); + m_maxGraph->initEdge(sourceVertex, destVertex); + m_explanationMaxGraph->initEdge(sourceVertex, destVertex); + if (m_explanationMinGraph) + { + m_explanationMinGraph->initEdge(sourceVertex, destVertex); + } + } + + foundVertexEdges->second[destVertex] = edgeIsClosed ? CLOSED_EDGE_FLOW : OPEN_EDGE_FLOW; + + if (!m_sourceGraph->hasEdge(destVertex, sourceVertex)) + { + auto foundDestVertexEdges = edgeCapacities.find(destVertex); + if (foundDestVertexEdges == edgeCapacities.end()) + { + foundDestVertexEdges = edgeCapacities.insert(destVertex).first; + } + foundDestVertexEdges->second[sourceVertex] = 0; + } + } + } + } + + // Build flow graph edges flat list and lookup map + m_flowGraphEdges.reserve(m_totalNumEdges); + m_flowGraphLookup.reserve(m_sourceGraph->getNumVertices()); + for (int sourceVertex = 0; sourceVertex < m_sourceGraph->getNumVertices(); ++sourceVertex) + { + m_flowGraphLookup.emplace_back(m_flowGraphEdges.size(), m_flowGraphEdges.size() + edgeCapacities[sourceVertex].size()); + for (auto it = edgeCapacities[sourceVertex].begin(), itEnd = edgeCapacities[sourceVertex].end(); it != itEnd; ++it) + { + m_flowGraphEdges.push_back({it->first, -1, it->second}); + } + } + + // Fill in the ReverseEdgeIndex for each vertex + for (int sourceVertex = 0; sourceVertex < m_sourceGraph->getNumVertices(); ++sourceVertex) + { + for (int i = get<0>(m_flowGraphLookup[sourceVertex]); i < get<1>(m_flowGraphLookup[sourceVertex]); ++i) + { + if (m_flowGraphEdges[i].reverseEdgeIndex < 0) + { + int destVertex = m_flowGraphEdges[i].endVertex; + bool foundReverse = false; + for (int j = get<0>(m_flowGraphLookup[destVertex]); j < get<1>(m_flowGraphLookup[destVertex]); ++j) + { + if (m_flowGraphEdges[j].endVertex == sourceVertex) + { + m_flowGraphEdges[i].reverseEdgeIndex = j; + vxy_assert(m_flowGraphEdges[j].reverseEdgeIndex < 0); + m_flowGraphEdges[j].reverseEdgeIndex = i; + + foundReverse = true; + break; + } + } + vxy_assert(foundReverse); + } + } + } + + // Register for callback when edges are added/removed from ExplanationGraph, in order to update capacities + m_explanationMaxGraph->getEdgeChangeListener().add([&](bool edgeWasAdded, int from, int to) + { + onExplanationMaxGraphEdgeChange(edgeWasAdded, from, to); + }); + + // Create reachability structures for all variables that are possibly reachability sources + for (int vertex = 0; vertex < m_sourceGraph->getNumVertices(); ++vertex) + { + VarID vertexVar = m_sourceGraphData->get(vertex); + if (vertexVar.isValid() && possiblyIsSource(db, vertexVar)) + { + addSource(db, vertexVar); + m_initialPotentialSources.push_back(vertexVar); + } + } + + // Constrain all variables that are definitely reachable by any definite reachability source to reachable + // Constrain all variables that are not reachable by all potential reachability sources to unreachable + for (int vertex = 0; vertex < m_sourceGraph->getNumVertices(); ++vertex) + { + VarID vertexVar = m_sourceGraphData->get(vertex); + if (vertexVar.isValid()) + { + EValidityDetermination determination = determineValidity(db, vertex); + + if (determination == EValidityDetermination::DefinitelyUnreachable) + { + if (!db->constrainToValues(vertexVar, m_invalidMask, this)) + { + onEdgeChangeFailure(db); + return false; + } + } + else if (determination == EValidityDetermination::DefinitelyValid) + { + if (!db->constrainToValues(vertexVar, m_requireValidMask, this)) + { + onEdgeChangeFailure(db); + return false; + } + } + } + } + onEdgeChangeSuccess(db); + + return true; +} + +void TopologyConnectionConstraint::reset(IVariableDatabase* db) +{ + for (auto it = m_vertexWatchHandles.begin(), itEnd = m_vertexWatchHandles.end(); it != itEnd; ++it) + { + db->removeVariableWatch(it->first, it->second, this); + } + m_vertexWatchHandles.clear(); + + for (auto it = m_edgeWatchHandles.begin(), itEnd = m_edgeWatchHandles.end(); it != itEnd; ++it) + { + db->removeVariableWatch(it->first, it->second, &m_edgeWatcher); + } + m_edgeWatchHandles.clear(); +} + +bool TopologyConnectionConstraint::onVariableNarrowed(IVariableDatabase* db, VarID variable, const ValueSet& prevValue, bool& removeWatch) +{ + const ValueSet& newValue = db->getPotentialValues(variable); + + if ((prevValue.anyPossible(m_sourceMask) && !newValue.anyPossible(m_sourceMask)) || + (prevValue.anyPossible(m_invalidMask) && !newValue.anyPossible(m_invalidMask))) + { + if (!contains(m_vertexProcessList.begin(), m_vertexProcessList.end(), variable)) + { + m_vertexProcessList.push_back(variable); + } + db->queueConstraintPropagation(this); + } + return true; +} + +bool TopologyConnectionConstraint::EdgeWatcher::onVariableNarrowed(IVariableDatabase* db, VarID var, const ValueSet& prevValue, bool& removeHandle) +{ + const ValueSet& newValue = db->getPotentialValues(var); + if ((prevValue.anyPossible(m_parent.m_edgeBlockedMask) && !newValue.anyPossible(m_parent.m_edgeBlockedMask)) || + (prevValue.anyPossible(m_parent.m_edgeOpenMask) && !newValue.anyPossible(m_parent.m_edgeOpenMask))) + { + m_parent.m_edgeProcessList.push_back(var); + db->queueConstraintPropagation(&m_parent); + } + return true; +} + +bool TopologyConnectionConstraint::propagate(IVariableDatabase* db) +{ + vxy_assert(!m_edgeChangeFailure); + ValueGuard guardEdgeChangeFailure(m_edgeChangeFailure, false); + + // Process edges first, adding/removing edges from the Min/Max graph, respectively + for (VarID edgeVar : m_edgeProcessList) + { + updateGraphsForEdgeChange(db, edgeVar); + if (m_edgeChangeFailure) + { + onEdgeChangeFailure(db); + return false; + } + } + m_edgeProcessList.clear(); + + #if REACHABILITY_USE_RAMAL_REPS + // Batch-update reachability for all edge changes. This will trigger onVertexChanged callbacks. + { + vxy_assert(!m_edgeChangeFailure); + ValueGuard guardEdgeChange(m_inEdgeChange, true); + ValueGuard guardDb(m_edgeChangeDb, db); + + for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) + { + it->second.maxReachability->refresh(); + if (m_edgeChangeFailure) + { + onEdgeChangeFailure(db); + return false; + } + + it->second.minReachability->refresh(); + if (m_edgeChangeFailure) + { + onEdgeChangeFailure(db); + return false; + } + } + } + #endif + + vxy_assert(!m_edgeChangeFailure); + + processQueuedVertexChanges(db); + if (m_edgeChangeFailure) + { + onEdgeChangeFailure(db); + return false; + } + + // Now that reachability info is up to date, process vertices + for (VarID vertexVar : m_vertexProcessList) + { + if (!processVertexVariableChange(db, vertexVar)) + { + onEdgeChangeFailure(db); + return false; + } + } + m_vertexProcessList.clear(); + onEdgeChangeSuccess(db); + + return true; +} + +bool TopologyConnectionConstraint::processVertexVariableChange(IVariableDatabase* db, VarID variable) +{ + if (!db->anyPossible(variable, m_sourceMask)) + { + if (!removeSource(db, variable)) + { + return false; + } + } + + // If this now requires reachability... + if (!db->anyPossible(variable, m_invalidMask)) + { + int vertex = m_variableToSourceVertexIndex[variable]; + + int numValidSources = 0; + VarID lastValidSource = VarID::INVALID; + bool hadAnyReachable = false; + for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) + { + bool isReachable = isPossiblyReachable(db, it->second, vertex); + hadAnyReachable |= isReachable; + if (isReachable && isPossiblyValid(db, it->second, vertex) ) + { + ++numValidSources; + lastValidSource = it->first; + if (numValidSources > 1) + { + break; + } + } + } + + // If not reachable by any source, then fail + if (numValidSources == 0) + { + bool success = db->constrainToValues(variable, m_invalidMask, this, [&,hadAnyReachable](auto params) { return hadAnyReachable ? explainInvalid(params) : explainNoReachability(params); }); + vxy_assert(!success); + return false; + } + // If reachable by a single potential source, that single source must be definite + else if (numValidSources == 1) + { + if (!db->constrainToValues(lastValidSource, m_sourceMask, this, [&](auto params) { return explainRequiredSource(params); })) + { + return false; + } + } + } + + return true; +} + +void TopologyConnectionConstraint::addSource(const IVariableDatabase* db, VarID source) +{ + int vertex = m_variableToSourceVertexIndex[source]; + + #if REACHABILITY_USE_RAMAL_REPS + auto minReachable = makeTopology(m_minGraph); + auto maxReachable = makeTopology(m_maxGraph); + #else + auto minReachable = make_shared(m_minGraph); + auto maxReachable = make_shared(m_maxGraph); + #endif + + minReachable->initialize(vertex, &m_reachabilityEdgeLookup, m_totalNumEdges); + maxReachable->initialize(vertex, &m_reachabilityEdgeLookup, m_totalNumEdges); + + EventListenerHandle minHandle = addMinCallback(*minReachable, db, source); + EventListenerHandle maxHandle = addMaxCallback(*maxReachable, db, source); + + m_reachabilitySources[source] = { minReachable, maxReachable, minHandle, maxHandle, vertex }; +} + +bool TopologyConnectionConstraint::removeSource(IVariableDatabase* db, VarID source) +{ + if (m_reachabilitySources.find(source) == m_reachabilitySources.end()) + { + return true; + } + + vxy_assert(m_backtrackData.empty() || m_backtrackData.back().level <= db->getDecisionLevel()); + if (m_backtrackData.empty() || m_backtrackData.back().level != db->getDecisionLevel()) + { + m_backtrackData.push_back({db->getDecisionLevel()}); + } + + vxy_assert(m_backtrackData.back().level == db->getDecisionLevel()); + vxy_sanity(!contains(m_backtrackData.back().reachabilitySourcesRemoved.begin(), m_backtrackData.back().reachabilitySourcesRemoved.end(), source)); + m_backtrackData.back().reachabilitySourcesRemoved.push_back(source); + + ReachabilitySourceData sourceData = m_reachabilitySources[source]; + m_reachabilitySources.erase(source); + + sourceData.minReachability->onReachabilityChanged.remove(sourceData.minRamalHandle); + sourceData.maxReachability->onReachabilityChanged.remove(sourceData.maxRamalHandle); + + int sourceVertex = m_variableToSourceVertexIndex[source]; + + // Look through all vertices that were reachable from this old source. If any are now definitely unreachable, + // mark them as such. + bool failure = false; + auto checkReachability = [&](int vertex, int parent) + { + if (isPossiblyReachable(db, sourceData, vertex) && isPossiblyValid(db, sourceData, vertex)) + { + // This vertex is no longer reachable from the removed source, so might be definitely unreachable now + VarID vertexVar = m_sourceGraphData->get(vertex); + if (vertexVar.isValid() && db->anyPossible(vertexVar, m_requireValidMask)) + { + EValidityDetermination determination = determineValidity(db, vertex); + + if (determination == EValidityDetermination::DefinitelyUnreachable) + { + sanityCheckUnreachable(db, vertex); + if (!db->constrainToValues(vertexVar, m_invalidMask, this, [&](auto params) { return explainNoReachability(params); })) + { + failure = true; + return ETopologySearchResponse::Abort; + } + } + else if (determination == EValidityDetermination::DefinitelyInvalid) + { + sanityCheckInvalid(db, vertex); + if (!db->constrainToValues(vertexVar, m_invalidMask, this, [&](auto params) { return explainInvalid(params); })) + { + failure = true; + return ETopologySearchResponse::Abort; + } + } + else if (determination == EValidityDetermination::PossiblyValid && !db->anyPossible(vertexVar, m_invalidMask)) + { + // The vertex is marked definitely reachable, but only possibly reachable in the graph. + // If there is only a single potential source that reaches this vertex, then it must now definitely be a source. + VarID lastValidSource = VarID::INVALID; + int numValidSources = 0; + for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) + { + if (isPossiblyReachable(db, it->second, vertex) && isPossiblyValid(db, it->second, vertex)) + { + ++numValidSources; + lastValidSource = it->first; + if (numValidSources > 1) + { + break; + } + } + } + + vxy_assert(numValidSources >= 1); + if (numValidSources == 1) + { + if (!db->constrainToValues(lastValidSource, m_sourceMask, this, [&, source](auto params) { return explainRequiredSource(params, source); })) + { + failure = true; + return ETopologySearchResponse::Abort; + } + } + } + } + return ETopologySearchResponse::Continue; + } + else + { + return ETopologySearchResponse::Skip; + } + }; + //source was removed. find nodes that relied on this source, check to see if they are reachable by other sources + m_dfs.search(*m_sourceGraph.get(), sourceVertex, checkReachability); + + return !failure; +} + +bool Vertexy::TopologyConnectionConstraint::isPossiblyValid(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex) +{ + // in the default implementation, it is always valid. implementors can override this for their invalid implementation + return true; +} + +TopologyConnectionConstraint::EValidityDetermination Vertexy::TopologyConnectionConstraint::determineValidityHelper( + const IVariableDatabase* db, + const ReachabilitySourceData& src, + int vertex, + VarID srcVertex) +{ + if (src.minReachability->isReachable(vertex)) + { + if (definitelyIsSource(db, srcVertex)) + { + return EValidityDetermination::DefinitelyValid; + } + else + { + return EValidityDetermination::PossiblyValid; + } + } + else if (src.maxReachability->isReachable(vertex)) + { + return EValidityDetermination::PossiblyValid; + } + + return EValidityDetermination::DefinitelyUnreachable; +} + +void Vertexy::TopologyConnectionConstraint::createTempSourceData(ReachabilitySourceData& data, int vertexIndex) const +{ +#if REACHABILITY_USE_RAMAL_REPS + data.maxReachability = make_shared(m_maxGraph, false, false, false); +#else + Data.maxReachability = make_shared(MaxGraph); +#endif + data.maxReachability->initialize(vertexIndex, &m_reachabilityEdgeLookup, m_totalNumEdges); +} + +void TopologyConnectionConstraint::updateGraphsForEdgeChange(IVariableDatabase* db, VarID variable) +{ + vxy_assert(!m_inEdgeChange); + vxy_assert(!m_edgeChangeFailure); + vxy_assert(m_edgeChangeDb == nullptr); + + ValueGuard guardEdgeChange(m_inEdgeChange, true); + ValueGuard guardDb(m_edgeChangeDb, db); + + int nodeIndex = m_variableToSourceEdgeIndex[variable]; + + // + // If an edge becomes definitely unblocked, add it to the min graph. + // If an edge becomes definitely blocked, remove it from the max graph. + // + // Sources listen to edge changes and call OnReachabilityChanged for any nodes that become (un)reachable from + // that source. The variables will attempt to be constrained based on their (un)reachability; if they cannot, + // then the bEdgeChangeFailure flag is set. + // + + if (db->anyPossible(variable, m_edgeOpenMask) && !db->anyPossible(variable, m_edgeBlockedMask)) + { + int from, to; + bool bidirectional; + m_edgeGraph->getSourceEdgeForVertex(nodeIndex, from, to, bidirectional); + if (!m_minGraph->hasEdge(from, to)) + { + m_minGraph->addEdge(from, to, db->getTimestamp()); + if (bidirectional) + { + m_minGraph->addEdge(to, from, db->getTimestamp()); + } + + if (m_explanationMinGraph) + { + m_explanationMinGraph->addEdge(from, to, db->getTimestamp()); + if (bidirectional) + { + m_explanationMinGraph->addEdge(to, from, db->getTimestamp()); + } + } + } + } + else if (db->anyPossible(variable, m_edgeBlockedMask) && !db->anyPossible(variable, m_edgeOpenMask)) + { + int from, to; + bool bidirectional; + m_edgeGraph->getSourceEdgeForVertex(nodeIndex, from, to, bidirectional); + + if (m_maxGraph->hasEdge(from, to)) + { + // Remove from the explanation graph first, so that we can sync to correct time. + m_explanationMaxGraph->removeEdge(from, to, db->getTimestamp()); + if (bidirectional) + { + m_explanationMaxGraph->removeEdge(to, from, db->getTimestamp()); + } + + m_maxGraph->removeEdge(from, to, db->getTimestamp()); + if (bidirectional) + { + m_maxGraph->removeEdge(to, from, db->getTimestamp()); + } + } + } +} + +void TopologyConnectionConstraint::backtrack(const IVariableDatabase* db, SolverDecisionLevel level) +{ + vxy_assert(!m_edgeChangeFailure); + m_edgeProcessList.clear(); + m_vertexProcessList.clear(); + + ValueGuard backtrackGuard(m_backtracking, true); + + while (!m_backtrackData.empty() && m_backtrackData.back().level > level) + { + for (VarID sourceVar : m_backtrackData.back().reachabilitySourcesRemoved) + { + addSource(db, sourceVar); + } + m_backtrackData.pop_back(); + } + + // Backtrack any edges added/removed after this point + m_minGraph->backtrackUntil(db->getTimestamp()); + m_maxGraph->backtrackUntil(db->getTimestamp()); + m_explanationMaxGraph->backtrackUntil(db->getTimestamp()); + if (m_explanationMinGraph) + { + m_explanationMinGraph->backtrackUntil(db->getTimestamp()); + } + + #if REACHABILITY_USE_RAMAL_REPS + // Batch-update reachability for all edge changes + { + for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) + { + it->second.maxReachability->refresh(); + it->second.minReachability->refresh(); + } + vxy_assert(!m_edgeChangeFailure); + } + #endif +} + +TopologyConnectionConstraint::EValidityDetermination TopologyConnectionConstraint::determineValidity(const IVariableDatabase* db, int vertexIndex) +{ + VarID vertexVar = m_sourceGraphData->get(vertexIndex); + bool hadAnyInvalid = false; + for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) + { + if (it->first == vertexVar) + { + // Don't treat reachability as reflective. If a vertex is marked both needing reachability and is a + // reachability source, it needs to be reachable from a DIFFERENT source. + continue; + } + + auto validity = determineValidityHelper(db, it->second, vertexIndex, it->first); + switch (validity) + { + case EValidityDetermination::DefinitelyInvalid: + hadAnyInvalid = true; + break; + case EValidityDetermination::DefinitelyUnreachable: + break; + default: + return validity; + } + } + + return hadAnyInvalid ? EValidityDetermination::DefinitelyInvalid : EValidityDetermination::DefinitelyUnreachable; +} + +// Called whenever an edge is added or removed from the explanation graph, including during backtracking +void TopologyConnectionConstraint::onExplanationMaxGraphEdgeChange(bool edgeWasAdded, int from, int to) +{ + // Keep the edge capacities in sync. + for (int i = get<0>(m_flowGraphLookup[from]); i < get<1>(m_flowGraphLookup[from]); ++i) + { + if (m_flowGraphEdges[i].endVertex == to) + { + m_flowGraphEdges[i].capacity = edgeWasAdded ? OPEN_EDGE_FLOW : CLOSED_EDGE_FLOW; + return; + } + } + vxy_fail(); +} + +vector TopologyConnectionConstraint::explainNoReachability(const NarrowingExplanationParams& params, ValueSet* alreadyVisitedSources) const +{ + vxy_assert_msg(m_variableToSourceVertexIndex.find(params.propagatedVariable) != m_variableToSourceVertexIndex.end(), "Not a vertex variable?"); + + auto db = params.database; + int conflictVertex = m_variableToSourceVertexIndex.find(params.propagatedVariable)->second; + + vector lits; + lits.push_back(Literal(params.propagatedVariable, m_invalidMask)); + + static hash_set edgeVarsRecorded; + edgeVarsRecorded.clear(); + + ValueSet curVisited; + curVisited.init(m_initialPotentialSources.size(), false); + ValueSet& visited = (alreadyVisitedSources != nullptr ? *alreadyVisitedSources : curVisited); + + // For each source that could possibly exist... + for (int potentialSrcIndex = 0; potentialSrcIndex < m_initialPotentialSources.size(); ++potentialSrcIndex) + { + if (visited[potentialSrcIndex]) + { + continue; + } + visited[potentialSrcIndex] = true; + + VarID potentialSource = m_initialPotentialSources[potentialSrcIndex]; + + int sourceVertex = m_variableToSourceVertexIndex.find(potentialSource)->second; + if (sourceVertex == conflictVertex) + { + // Reachability sources cannot provide reachability to themselves + continue; + } + + // If this is currently a potential source... + if (db->getPotentialValues(potentialSource).anyPossible(m_sourceMask)) + { + // + // Find the minimum cut of edges that would make this reachable + // + + // Temporarily rewind the explanation graph to this time. + // This will trigger onExplanationMaxGraphEdgeChange() for any edges re-added, so that FlowGraphEdges + // will be the same state as when we processed the input variable. + + m_explanationMaxGraph->rewindUntil(params.timestamp); + + vxy_sanity(!TopologySearchAlgorithm::canReach(m_explanationMaxGraph, sourceVertex, conflictVertex)); + + // Find the minimum cut in the maximum flow graph. This will correspond to edges that are disabled, because + // A) we know that sourceVertex can't reach conflictVertex without going through a disabled edge + // B) blocked edges are set to a flow capacity of 1, and blocked edges have infinite flow + vector> cutEdges; + // first check if the source and conflict have a common edge, since getMaxFlow doesn't work in this case + if (m_edgeGraph->getVertexForSourceEdge(sourceVertex, conflictVertex) == -1) + { + m_maxFlowAlgo.getMaxFlow(*m_sourceGraph.get(), sourceVertex, conflictVertex, m_flowGraphEdges, m_flowGraphLookup, &cutEdges); + } + else + { + cutEdges.push_back(make_tuple(sourceVertex, conflictVertex)); + } + vxy_assert(!cutEdges.empty()); + + // Now that we've found the cut, bring the explanation graph back to current state. + m_explanationMaxGraph->fastForward(); + + for (tuple& edge : cutEdges) + { + int edgeNode = m_edgeGraph->getVertexForSourceEdge(get<0>(edge), get<1>(edge)); + VarID edgeVar = m_edgeGraphData->get(edgeNode); + if (edgeVarsRecorded.find(edgeVar) == edgeVarsRecorded.end()) + { + edgeVarsRecorded.insert(edgeVar); + + vxy_assert(!db->anyPossible(edgeVar, m_edgeOpenMask)); //hits this with distance = 100, 200 + lits.push_back(Literal(edgeVar, m_edgeOpenMask)); + } + } + + // For every other potential source, see if this graph also holds. It holds if the other source is on the + // same side as this source, hence would have to cross the same edge boundary. + for (int j = potentialSrcIndex + 1; j < m_initialPotentialSources.size(); ++j) + { + if (visited[j]) + { + continue; + } + + int vertex = m_variableToSourceVertexIndex.find(potentialSource)->second; + if (vertex == conflictVertex) + { + continue; + } + + if (db->getPotentialValues(m_initialPotentialSources[j]).anyPossible(m_sourceMask)) + { + if (!m_maxFlowAlgo.onSinkSide(vertex, m_flowGraphEdges, m_flowGraphLookup)) + { + visited[j] = true; + } + } + } + } + // Not currently a potential source. For now, the conservative explanation is that we'd be able to reach if it + // was. + else + { + lits.push_back(Literal(potentialSource, m_sourceMask)); + } + } + + return lits; +} + +vector TopologyConnectionConstraint::explainRequiredSource(const NarrowingExplanationParams& params, VarID removedSource) +{ + //return IVariableDatabase::defaultExplainer(params); + + vxy_assert(!m_explainingSourceRequirement); + ValueGuard guard(m_explainingSourceRequirement, true); + + VarID sourceVar = params.propagatedVariable; + int sourceVertex = m_variableToSourceVertexIndex[sourceVar]; + + auto db = params.database; + + vector lits; + lits.push_back(Literal(sourceVar, m_sourceMask)); + + m_maxGraph->rewindUntil(params.timestamp); + +#if REACHABILITY_USE_RAMAL_REPS + { + // Batch-update to rewound graph state + for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) + { + it->second.maxReachability->refresh(); + } + } +#endif + + // Create any sources that might've gotten removed since this happened. + // (We'll clean them up after) + vector tempSources; + for (VarID potentialSource : m_initialPotentialSources) + { + if (db->anyPossible(potentialSource, m_sourceMask)) + { + if (m_reachabilitySources.find(potentialSource) == m_reachabilitySources.end()) + { + tempSources.push_back(potentialSource); + + int vertexIndex = m_variableToSourceVertexIndex[potentialSource]; + + ReachabilitySourceData data; + createTempSourceData(data, vertexIndex); + + m_reachabilitySources[potentialSource] = data; + } + } + else if (potentialSource != sourceVar) + { + lits.push_back(Literal(potentialSource, m_sourceMask)); + } + } + + int removedSourceLitIdx = -1; + if (removedSource.isValid()) + { + // This became a required source because RemovedSource was removed, and some definitely-reachable vertices were + // only reachable by this source. + vxy_assert(!db->anyPossible(removedSource, m_sourceMask)); + removedSourceLitIdx = indexOfPredicate(lits.begin(), lits.end(), [&](auto& lit) { return lit.variable == removedSource; }); + vxy_assert(removedSourceLitIdx >= 0); + } + + // + // This became a required source because some variable(s) were marked as required, and we are the only + // source that can reach them. Find those variables. + // + bool foundSupports = false; + auto& ourReachability = m_reachabilitySources[sourceVar].maxReachability; + auto searchCallback = [&](int vertex, int parent, int edgeIndex) + { + if (ourReachability->isReachable(vertex)) + { + VarID vertexVar = m_sourceGraphData->get(vertex); + if (!db->anyPossible(vertexVar, m_invalidMask)) + { + bool reachableFromAnotherSource = false; + for (auto it = m_reachabilitySources.begin(), itEnd = m_reachabilitySources.end(); it != itEnd; ++it) + { + if (it->first != sourceVar && it->first != vertexVar && isPossiblyReachable(db, it->second, vertex) && isPossiblyValid(db, it->second, vertex)) + { + reachableFromAnotherSource = true; + break; + } + } + + if (!reachableFromAnotherSource) + { + vxy_assert(m_reachabilitySources[sourceVar].maxReachability->isReachable(vertex)); + // make sure we don't add the same literal twice! + auto found = find_if(lits.begin(), lits.end(), [&](auto& lit) { return lit.variable == vertexVar; }); + if (found != lits.end()) + { + vxy_assert(found->variable == vertexVar); + found->values.include(m_invalidMask); + } + else + { + lits.push_back(Literal(vertexVar, m_invalidMask)); + } + foundSupports = true; + } + } + return ETopologySearchResponse::Continue; + } + else + { + return ETopologySearchResponse::Skip; + } + }; + m_dfs.search(*m_sourceGraph.get(), m_variableToSourceVertexIndex[sourceVar], searchCallback); + vxy_assert(foundSupports); + + for (VarID tempSource : tempSources) + { + m_reachabilitySources.erase(tempSource); + } + + m_maxGraph->fastForward(); + return lits; +} + +bool TopologyConnectionConstraint::isPossiblyReachable(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex) const +{ + return src.maxReachability->isReachable(vertex); +} + +void TopologyConnectionConstraint::sanityCheckUnreachable(IVariableDatabase* db, int vertexIndex) +{ + #if SANITY_CHECKS + // For each source that could possibly exist... + for (VarID potentialSource : m_initialPotentialSources) + { + int sourceVertex = m_variableToSourceVertexIndex[potentialSource]; + // If this is currently a potential source... + if (db->getPotentialValues(potentialSource).anyPossible(m_sourceMask)) + { + vxy_assert(!TopologySearchAlgorithm::canReach(m_maxGraph, sourceVertex, vertexIndex)); + } + } + #endif +} + + +vector TopologyConnectionConstraint::getConstrainingVariables() const +{ + vector out; + for (int i = 0; i < m_sourceGraph->getNumVertices(); ++i) + { + VarID var = m_sourceGraphData->get(i); + if (var.isValid()) + { + out.push_back(var); + } + } + + for (int i = 0; i < m_edgeGraph->getNumVertices(); ++i) + { + VarID var = m_edgeGraphData->get(i); + if (var.isValid()) + { + out.push_back(var); + } + } + + return out; +} + +bool TopologyConnectionConstraint::checkConflicting(IVariableDatabase* db) const +{ + // TODO + return false; +} + +#undef SANITY_CHECKS diff --git a/vertexy/src/private/variable/SolverVariableDatabase.cpp b/vertexy/src/private/variable/SolverVariableDatabase.cpp index 4e0c390..9704b51 100644 --- a/vertexy/src/private/variable/SolverVariableDatabase.cpp +++ b/vertexy/src/private/variable/SolverVariableDatabase.cpp @@ -9,6 +9,50 @@ using namespace Vertexy; +// +// Default explanation function for a violated constraint. This will return a true explanation, but is not necessarily +// the smallest explanation possible, especially for constraints involving more than 2 variables. +// +vector IVariableDatabase::defaultExplainer(const NarrowingExplanationParams& params) +{ + // Find all dependent variables for this constraint that were previously narrowed, and add their (inverted) value to the list. + // The clause will look like: + // (Arg1 != Arg1Values OR Arg2 != Arg2Values OR [...] OR PropagatedVariable == PropagatedValues) + const vector& constraintVars = params.solver->getVariablesForConstraint(params.constraint); + vector clauses; + clauses.reserve(constraintVars.size()); + + bool foundPropagated = false; + for (int i = 0; i < constraintVars.size(); ++i) + { + VarID arg = constraintVars[i]; + clauses.push_back(Literal(arg, params.database->getPotentialValues(arg))); + clauses.back().values.invert(); + + if (arg == params.propagatedVariable) + { + foundPropagated = true; + clauses.back().values.pad(params.propagatedValues.size(), false); + clauses.back().values.include(params.propagatedValues); + } + } + + vxy_assert(foundPropagated); + return clauses; +} + +int IVariableDatabase::getMinimumPossibleDomainValue(VarID varID) const +{ + vxy_assert(varID.isValid()); + return getSolver()->getDomain(varID).getValueForIndex(getMinimumPossibleValue(varID)); +} + +int IVariableDatabase::getMaximumPossibleDomainValue(VarID varID) const +{ + vxy_assert(varID.isValid()); + return getSolver()->getDomain(varID).getValueForIndex(getMaximumPossibleValue(varID)); +} + SolverVariableDatabase::SolverVariableDatabase(ConstraintSolver* inSolver) : IVariableDatabase() , m_solver(inSolver) diff --git a/vertexy/src/public/ConstraintTypes.h b/vertexy/src/public/ConstraintTypes.h index 99aed29..1fe6046 100644 --- a/vertexy/src/public/ConstraintTypes.h +++ b/vertexy/src/public/ConstraintTypes.h @@ -39,7 +39,8 @@ enum class EConstraintType : uint8_t Offset, Table, Reachability, - Sum + Sum, + ShortestPath }; // If set, VariableDBs will cache the state of each variable (solved/unsolved/contradiction), only updating when diff --git a/vertexy/src/public/constraints/ReachabilityConstraint.h b/vertexy/src/public/constraints/ReachabilityConstraint.h index cc9fc82..b0162ef 100644 --- a/vertexy/src/public/constraints/ReachabilityConstraint.h +++ b/vertexy/src/public/constraints/ReachabilityConstraint.h @@ -1,6 +1,7 @@ // Copyright Proletariat, Inc. All Rights Reserved. #pragma once #include "ConstraintTypes.h" +#include "TopologyConnectionConstraint.h" #include "IBacktrackingSolverConstraint.h" #include "IConstraint.h" #include "SignedClause.h" @@ -22,7 +23,7 @@ namespace Vertexy * Any variable that is definitely one of SourceValues is considered a reachability source. * Any variable that is definitely on of NeedReachableValues is considered a destination that must remain reachable from AT LEAST one source. */ -class ReachabilityConstraint : public IBacktrackingSolverConstraint +class ReachabilityConstraint : public TopologyConnectionConstraint { public: ReachabilityConstraint(const ConstraintFactoryParams& params, @@ -52,162 +53,14 @@ class ReachabilityConstraint : public IBacktrackingSolverConstraint using Factory = ReachabilityFactory; virtual EConstraintType getConstraintType() const override { return EConstraintType::Reachability; } - virtual vector getConstrainingVariables() const override; - virtual bool initialize(IVariableDatabase* db) override; - virtual void reset(IVariableDatabase* db) override; - virtual bool onVariableNarrowed(IVariableDatabase* db, VarID variable, const ValueSet& previousValue, bool& removeWatch) override; - virtual bool checkConflicting(IVariableDatabase* db) const override; - virtual bool propagate(IVariableDatabase* db) override; - virtual void backtrack(const IVariableDatabase* db, SolverDecisionLevel level) override; - virtual bool getGraphRelations(const vector& literals, ConstraintGraphRelationInfo& outRelations) const override; protected: - vector explainNoReachability(const NarrowingExplanationParams& params) const; - vector explainRequiredSource(const NarrowingExplanationParams& params, VarID removedSource = VarID::INVALID); - enum class EReachabilityDetermination : uint8_t - { - DefinitelyReachable, - // Reachable from a definite source - PossiblyReachable, - // Reachable from a possible source - DefinitelyUnreachable, - // Unreachable from any possible source - }; - - EReachabilityDetermination determineReachability(const IVariableDatabase* db, int vertex); - bool processVertexVariableChange(IVariableDatabase* db, VarID variable); - void updateGraphsForEdgeChange(IVariableDatabase* db, VarID variable); - void onReachabilityChanged(int vertexIndex, VarID sourceVar, bool inMinGraph); - void sanityCheckUnreachable(IVariableDatabase* db, int vertexIndex); - - void onExplanationGraphEdgeChange(bool edgeWasAdded, int from, int to); - - void addSource(VarID source); - bool removeSource(IVariableDatabase* db, VarID source); - - inline bool definitelyNeedsToReach(const IVariableDatabase* db, VarID var) const - { - return !db->getPotentialValues(var).anyPossible(m_notReachableMask); - } - - inline bool definitelyIsSource(const IVariableDatabase* db, VarID var) const - { - return !db->getPotentialValues(var).anyPossible(m_notSourceMask); - } - - inline bool definitelyNotSource(const IVariableDatabase* db, VarID var) const - { - return !db->getPotentialValues(var).anyPossible(m_sourceMask); - } - - inline bool possiblyIsSource(const IVariableDatabase* db, VarID var) - { - return !definitelyNotSource(db, var); - } - - inline bool possiblyOpenEdge(const IVariableDatabase* db, VarID var) const - { - return db->getPotentialValues(var).anyPossible(m_edgeOpenMask); - } - - inline bool definitelyOpenEdge(const IVariableDatabase* db, VarID var) const - { - return !db->getPotentialValues(var).anyPossible(m_edgeBlockedMask); - } - - inline bool definitelyClosedEdge(const IVariableDatabase* db, VarID var) - { - return !possiblyOpenEdge(db, var); - } - - class EdgeWatcher : public IVariableWatchSink - { - public: - EdgeWatcher(ReachabilityConstraint& parent) - : m_parent(parent) - { - } - - virtual IConstraint* asConstraint() override { return &m_parent; } - virtual bool onVariableNarrowed(IVariableDatabase* db, VarID variable, const ValueSet& previousValue, bool& removeWatch) override; - - protected: - ReachabilityConstraint& m_parent; - }; - - EdgeWatcher m_edgeWatcher; - - shared_ptr> m_sourceGraphData; - shared_ptr m_sourceGraph; - shared_ptr> m_edgeGraphData; - shared_ptr m_edgeGraph; - - // Contains edges that DEFINITELY exist. Edges are only added to this graph. - shared_ptr m_minGraph; - // Contains edges that POSSIBLY exist. Edges are only removed from this graph. - shared_ptr m_maxGraph; - // Synchronized with MaxGraph. Used during explanations where we need to temporarily rewind graph state, but we don't - // want to propagate to the source reachability trees. - shared_ptr m_explanationGraph; - - ValueSet m_sourceMask; - ValueSet m_notSourceMask; - - ValueSet m_requireReachableMask; - ValueSet m_notReachableMask; - - ValueSet m_edgeBlockedMask; - ValueSet m_edgeOpenMask; - - hash_map m_vertexWatchHandles; - hash_map m_edgeWatchHandles; - - struct BacktrackData - { - SolverDecisionLevel level; - vector reachabilitySourcesRemoved; - }; - - vector m_backtrackData; - - using ESTreeType = ESTree; - using RamalRepsType = RamalReps; - - struct ReachabilitySourceData - { - #if REACHABILITY_USE_RAMAL_REPS - shared_ptr minReachability; - shared_ptr maxReachability; - #else - shared_ptr minReachability; - shared_ptr maxReachability; - #endif - EventListenerHandle minReachabilityChangedHandle = INVALID_EVENT_LISTENER_HANDLE; - EventListenerHandle maxReachabilityChangedHandle = INVALID_EVENT_LISTENER_HANDLE; - }; - - vector m_vertexProcessList; - vector m_edgeProcessList; - - vector m_initialPotentialSources; - hash_map m_reachabilitySources; - - hash_map m_variableToSourceVertexIndex; - hash_map m_variableToSourceEdgeIndex; - - IVariableDatabase* m_edgeChangeDb = nullptr; - bool m_edgeChangeFailure = false; - bool m_inEdgeChange = false; - bool m_backtracking = false; - bool m_explainingSourceRequirement = false; - int m_totalNumEdges = 0; + virtual shared_ptr makeTopology(const shared_ptr& graph) const override; + virtual EventListenerHandle addMinCallback(RamalRepsType& minReachable, const IVariableDatabase* db, VarID source) override; + virtual EventListenerHandle addMaxCallback(RamalRepsType& maxReachable, const IVariableDatabase* db, VarID source) override; - DepthFirstSearchAlgorithm m_dfs; - mutable TMaxFlowMinCutAlgorithm m_maxFlowAlgo; - vector> m_flowGraphEdges; - FlowGraphLookupMap m_flowGraphLookup; - RamalRepsEdgeDefinitions m_reachabilityEdgeLookup; + void onVertexChanged(int vertexIndex, VarID sourceVar, bool inMinGraph); }; } // namespace Vertexy \ No newline at end of file diff --git a/vertexy/src/public/constraints/ShortestPathConstraint.h b/vertexy/src/public/constraints/ShortestPathConstraint.h new file mode 100644 index 0000000..e2ea992 --- /dev/null +++ b/vertexy/src/public/constraints/ShortestPathConstraint.h @@ -0,0 +1,102 @@ +// Copyright Proletariat, Inc. All Rights Reserved. +#pragma once +#include "ConstraintTypes.h" +#include "TopologyConnectionConstraint.h" +#include "IConstraint.h" +#include "SignedClause.h" +#include "ds/ESTree.h" +#include "ds/RamalReps.h" +#include "topology/BacktrackingDigraphTopology.h" +#include "topology/DigraphEdgeTopology.h" +#include "topology/TopologyVertexData.h" +#include "topology/algo/MaxFlowMinCut.h" +#include "topology/algo/ShortestPath.h" +#include "variable/IVariableDatabase.h" +#include "constraints/ConstraintOperator.h" +#include "ds/BacktrackableValue.h" + +#define REACHABILITY_USE_RAMAL_REPS 1 + +namespace Vertexy +{ + +/** Constraint to ensure the shortest paths between source and destination nodes + * All destination nodes must have at least 1 shortest path to at least 1 source node + * this shortest path must have a relation with 'distance' + */ +class ShortestPathConstraint : public TopologyConnectionConstraint +{ +public: + ShortestPathConstraint(const ConstraintFactoryParams& params, + const shared_ptr>& sourceGraphData, + const ValueSet& sourceMask, + const ValueSet& requireReachableMask, + const shared_ptr>& edgeGraphData, + const ValueSet& edgeBlockedMask, + EConstraintOperator op, + int distance + ); + + struct ShortestPathFactory + { + static ShortestPathConstraint* construct( + const ConstraintFactoryParams& params, + // Graph of vertices where reachability is calculated + const shared_ptr>& sourceGraphData, + // Values of vertices in SourceGraph that establish it as a reachability source + const vector& sourceValues, + // Values of vertices in SourceGraph that establish it as needing to be reachable from a source + const vector& needReachableValues, + // The variables for each edge of source graph + const shared_ptr>& edgeGraphData, + // Values of vertices in the edge graph establishing that edge as "off" + const vector& edgeBlockedValues, + // How to compare distance + EConstraintOperator op, + // The variable that stores the distance + int distance); + }; + + using Factory = ShortestPathFactory; + + virtual EConstraintType getConstraintType() const override { return EConstraintType::ShortestPath; } + virtual void onInitialArcConsistency(IVariableDatabase* db) override; + +protected: + + bool isValidDistance(const IVariableDatabase* db, int dist) const; + + virtual bool isPossiblyValid(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex) override; + virtual EValidityDetermination determineValidityHelper(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex, VarID srcVertex) override; + virtual shared_ptr makeTopology(const shared_ptr& graph) const override; + virtual EventListenerHandle addMinCallback(RamalRepsType& minReachable, const IVariableDatabase* db, VarID source) override; + virtual EventListenerHandle addMaxCallback(RamalRepsType& maxReachable, const IVariableDatabase* db, VarID source) override; + virtual vector explainInvalid(const NarrowingExplanationParams& params) override; + virtual void sanityCheckInvalid(IVariableDatabase* db, int vertexIndex) override; + virtual void createTempSourceData(ReachabilitySourceData& data, int vertexIndex) const override; + void onVertexChanged(int vertexIndex, VarID sourceVar, bool inMinGraph); + void backtrack(const IVariableDatabase* db, SolverDecisionLevel level) override; + + EConstraintOperator m_op; + int m_distance; + + // used to determine the path that is either too long or too short when explaning + ShortestPathAlgorithm m_shortestPathAlgo; + + // used when m_op is LessThan/LessThanEq and records the last timestamp in which a vertex was deemed valid + hash_map>> m_lastValidTimestamp; + hash_map> m_validTimestampsToCommit; + hash_set> m_alwaysForbiddenPaths; + + hash_set m_queuedVertexChanges; + bool m_processingVertices = false; + + void commitValidTimestamps(const IVariableDatabase* db); + void onEdgeChangeFailure(const IVariableDatabase* db) override; + void onEdgeChangeSuccess(const IVariableDatabase* db) override; + void addTimestampToCommit(const IVariableDatabase* db, int sourceVertex, int destVertex); + void removeTimestampToCommit(const IVariableDatabase* db, int sourceVertex, int destVertex); + void processQueuedVertexChanges(IVariableDatabase* db) override; +}; + +} // namespace Vertexy \ No newline at end of file diff --git a/vertexy/src/public/constraints/TopologyConnectionConstraint.h b/vertexy/src/public/constraints/TopologyConnectionConstraint.h new file mode 100644 index 0000000..3ae08e7 --- /dev/null +++ b/vertexy/src/public/constraints/TopologyConnectionConstraint.h @@ -0,0 +1,229 @@ +// Copyright Proletariat, Inc. All Rights Reserved. +#pragma once +#include "ConstraintTypes.h" +#include "IBacktrackingSolverConstraint.h" +#include "IConstraint.h" +#include "SignedClause.h" +#include "ds/ESTree.h" +#include "ds/RamalReps.h" +#include "topology/BacktrackingDigraphTopology.h" +#include "topology/DigraphEdgeTopology.h" +#include "topology/TopologyVertexData.h" +#include "topology/algo/MaxFlowMinCut.h" +#include "variable/IVariableDatabase.h" + +#define REACHABILITY_USE_RAMAL_REPS 1 + +namespace Vertexy +{ + +/** Base class for ReachabilityConstraint and ShortestPathConstraint + */ +class TopologyConnectionConstraint : public IBacktrackingSolverConstraint +{ +public: + TopologyConnectionConstraint(const ConstraintFactoryParams& params, + const shared_ptr>& sourceGraphData, + const ValueSet& sourceMask, + const ValueSet& requireReachableMask, + const shared_ptr>& edgeGraphData, + const ValueSet& edgeBlockedMask + ); + + virtual vector getConstrainingVariables() const override; + virtual bool initialize(IVariableDatabase* db) override; + virtual void reset(IVariableDatabase* db) override; + virtual bool onVariableNarrowed(IVariableDatabase* db, VarID variable, const ValueSet& previousValue, bool& removeWatch) override; + virtual bool checkConflicting(IVariableDatabase* db) const override; + virtual bool propagate(IVariableDatabase* db) override; + virtual void backtrack(const IVariableDatabase* db, SolverDecisionLevel level) override; + virtual bool getGraphRelations(const vector& literals, ConstraintGraphRelationInfo& outRelations) const override; + +protected: + vector explainNoReachability(const NarrowingExplanationParams& params, ValueSet* alreadyVisitedSources = nullptr) const; + vector explainRequiredSource(const NarrowingExplanationParams& params, VarID removedSource = VarID::INVALID); + virtual vector explainInvalid(const NarrowingExplanationParams& params) + { + vxy_fail(); // override this if using DefinitelyInvalid + return vector(); + } + + enum class EValidityDetermination : uint8_t + { + DefinitelyValid, + // Reachable from a definite source + PossiblyValid, + // Reachable from a possible source + DefinitelyUnreachable, + // Unreachable from any possible source + DefinitelyInvalid, + // Invalid from any possible source + }; + + EValidityDetermination determineValidity(const IVariableDatabase* db, int vertex); + //used by propagate, NEEDS TO CHANGE + bool processVertexVariableChange(IVariableDatabase* db, VarID variable); + //used by propagate + void updateGraphsForEdgeChange(IVariableDatabase* db, VarID variable); + void sanityCheckUnreachable(IVariableDatabase* db, int vertexIndex); + virtual void sanityCheckInvalid(IVariableDatabase* db, int vertexIndex) + { + vxy_fail(); // override me! + } + + void onExplanationMaxGraphEdgeChange(bool edgeWasAdded, int from, int to); + + void addSource(const IVariableDatabase* db, VarID source); + //used by processVertexVariableChange + bool removeSource(IVariableDatabase* db, VarID source); + + using ESTreeType = ESTree; + using RamalRepsType = RamalReps; + + struct ReachabilitySourceData; + //virtual + bool isPossiblyReachable(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex) const; + virtual bool isPossiblyValid(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex); + virtual EValidityDetermination determineValidityHelper(const IVariableDatabase* db, const ReachabilitySourceData& src, int vertex, VarID srcVertex); + virtual shared_ptr makeTopology(const shared_ptr& graph) const = 0; + virtual EventListenerHandle addMinCallback(RamalRepsType& minReachable, const IVariableDatabase* db, VarID source) = 0; + virtual EventListenerHandle addMaxCallback(RamalRepsType& maxReachable, const IVariableDatabase* db, VarID source) = 0; + virtual void createTempSourceData(ReachabilitySourceData& data, int vertexIndex) const; + virtual void onEdgeChangeFailure(const IVariableDatabase* db) + { + } + + virtual void onEdgeChangeSuccess(const IVariableDatabase* db) + { + } + + virtual void processQueuedVertexChanges(IVariableDatabase* db) + { + } + + inline bool definitelyNeedsToReach(const IVariableDatabase* db, VarID var) const + { + return !db->getPotentialValues(var).anyPossible(m_invalidMask); + } + + inline bool definitelyIsSource(const IVariableDatabase* db, VarID var) const + { + return !db->getPotentialValues(var).anyPossible(m_notSourceMask); + } + + inline bool definitelyNotSource(const IVariableDatabase* db, VarID var) const + { + return !db->getPotentialValues(var).anyPossible(m_sourceMask); + } + + inline bool possiblyIsSource(const IVariableDatabase* db, VarID var) + { + return !definitelyNotSource(db, var); + } + + inline bool possiblyOpenEdge(const IVariableDatabase* db, VarID var) const + { + return db->getPotentialValues(var).anyPossible(m_edgeOpenMask); + } + + inline bool definitelyOpenEdge(const IVariableDatabase* db, VarID var) const + { + return !db->getPotentialValues(var).anyPossible(m_edgeBlockedMask); + } + + inline bool definitelyClosedEdge(const IVariableDatabase* db, VarID var) + { + return !possiblyOpenEdge(db, var); + } + + class EdgeWatcher : public IVariableWatchSink + { + public: + EdgeWatcher(TopologyConnectionConstraint& parent) + : m_parent(parent) + { + } + + virtual IConstraint* asConstraint() override { return &m_parent; } + virtual bool onVariableNarrowed(IVariableDatabase* db, VarID variable, const ValueSet& previousValue, bool& removeWatch) override; + + protected: + TopologyConnectionConstraint& m_parent; + }; + + EdgeWatcher m_edgeWatcher; + + shared_ptr> m_sourceGraphData; + shared_ptr m_sourceGraph; + shared_ptr> m_edgeGraphData; + shared_ptr m_edgeGraph; + + // Contains edges that DEFINITELY exist. Edges are only added to this graph. + shared_ptr m_minGraph; + // Contains edges that POSSIBLY exist. Edges are only removed from this graph. + shared_ptr m_maxGraph; + // Synchronized with MaxGraph. Used during explanations where we need to temporarily rewind graph state, but we don't + // want to propagate to the source reachability trees. + shared_ptr m_explanationMaxGraph; + // Synchronized with MinGraph. Used during explanations where we need to temporarily rewind graph state, but we don't + // want to propagate to the source reachability trees. + shared_ptr m_explanationMinGraph; + + ValueSet m_sourceMask; + ValueSet m_notSourceMask; + + ValueSet m_requireValidMask; + ValueSet m_invalidMask; + + ValueSet m_edgeBlockedMask; + ValueSet m_edgeOpenMask; + + hash_map m_vertexWatchHandles; + hash_map m_edgeWatchHandles; + + struct BacktrackData + { + SolverDecisionLevel level; + vector reachabilitySourcesRemoved; + }; + + vector m_backtrackData; + + struct ReachabilitySourceData + { + #if REACHABILITY_USE_RAMAL_REPS + shared_ptr minReachability; + shared_ptr maxReachability; + #else + shared_ptr minReachability; + shared_ptr maxReachability; + #endif + EventListenerHandle minRamalHandle = INVALID_EVENT_LISTENER_HANDLE; + EventListenerHandle maxRamalHandle = INVALID_EVENT_LISTENER_HANDLE; + int vertex; + }; + + vector m_vertexProcessList; + vector m_edgeProcessList; + + vector m_initialPotentialSources; + hash_map m_reachabilitySources; + + hash_map m_variableToSourceVertexIndex; + hash_map m_variableToSourceEdgeIndex; + + IVariableDatabase* m_edgeChangeDb = nullptr; + bool m_edgeChangeFailure = false; + bool m_inEdgeChange = false; + bool m_backtracking = false; + bool m_explainingSourceRequirement = false; + int m_totalNumEdges = 0; + + DepthFirstSearchAlgorithm m_dfs; + mutable TMaxFlowMinCutAlgorithm m_maxFlowAlgo; + vector> m_flowGraphEdges; + FlowGraphLookupMap m_flowGraphLookup; + RamalRepsEdgeDefinitions m_reachabilityEdgeLookup; +}; + +} // namespace Vertexy \ No newline at end of file diff --git a/vertexy/src/public/ds/BacktrackableValue.h b/vertexy/src/public/ds/BacktrackableValue.h new file mode 100644 index 0000000..04560d1 --- /dev/null +++ b/vertexy/src/public/ds/BacktrackableValue.h @@ -0,0 +1,81 @@ +#pragma once +#include "ConstraintTypes.h" +#include "EASTL/vector.h" +#include "util/Asserts.h" + +namespace Vertexy +{ +template +struct TTimestampAndValue +{ + InElementType value; + SolverTimestamp timestamp; +}; + +template +class TBacktrackableValue +{ +public: + TBacktrackableValue() {} + + void set(SolverTimestamp timestamp, InElementType&& value) + { + vxy_assert(this->timesAndValues.size() == 0 || this->timesAndValues.back().timestamp <= timestamp); + this->timesAndValues.push_back({ move(value), timestamp }); + } + + void set(SolverTimestamp timestamp, const InElementType& value) + { + vxy_assert(this->timesAndValues.size() == 0 || this->timesAndValues.back().timestamp <= timestamp); + this->timesAndValues.push_back({ value, timestamp }); + } + + bool hasValue() + { + return this->timesAndValues.size() > 0; + } + + const InElementType& get() const + { + return this->timesAndValues.back().value; + } + + int getIndexBefore(SolverTimestamp timestamp) const + { + auto size = this->timesAndValues.size(); + while (size > 0 && this->timesAndValues[size - 1].timestamp >= timestamp) + { + size--; + } + return size - 1; + } + + const InElementType& getValueForIndex(int index) const + { + return this->timesAndValues[index].value; + } + + const InElementType& getTimestampForIndex(int index) const + { + return this->timesAndValues[index].timestamp; + } + + const SolverTimestamp getTimestamp() + { + return this->timesAndValues.back().timestamp; + } + + void backtrackUntil(SolverTimestamp timestamp) + { + auto size = this->timesAndValues.size(); + while (size > 0 && this->timesAndValues[size - 1].timestamp > timestamp) + { + size--; + this->timesAndValues.pop_back(); + } + } + +private: + vector> timesAndValues; +}; +} diff --git a/vertexy/src/public/ds/RamalReps.h b/vertexy/src/public/ds/RamalReps.h index 23b1ae1..f585338 100644 --- a/vertexy/src/public/ds/RamalReps.h +++ b/vertexy/src/public/ds/RamalReps.h @@ -234,6 +234,7 @@ class RamalReps } inline bool isReachable(int vertex) const { return m_vertexDists[vertex] != INT_MAX; } + inline int getDistance(int vertex) const { return m_vertexDists[vertex]; } protected: void addEdge(int from, int to) diff --git a/vertexy/src/public/topology/BacktrackingDigraphTopology.h b/vertexy/src/public/topology/BacktrackingDigraphTopology.h index c319186..78f3c16 100644 --- a/vertexy/src/public/topology/BacktrackingDigraphTopology.h +++ b/vertexy/src/public/topology/BacktrackingDigraphTopology.h @@ -99,7 +99,7 @@ class BacktrackingDigraphTopology : public TDigraphTopologyBase 0) || m_lastHistoryIdx < m_history.size() - 1; } protected: struct HistoryRecord diff --git a/vertexy/src/public/topology/algo/ShortestPath.h b/vertexy/src/public/topology/algo/ShortestPath.h index 4fb0d9d..ee06ca8 100644 --- a/vertexy/src/public/topology/algo/ShortestPath.h +++ b/vertexy/src/public/topology/algo/ShortestPath.h @@ -18,7 +18,7 @@ class ShortestPathAlgorithm inline bool find(const TTopology& topology, int startVertex, int endVertex, vector& outPath) { vector parentLinks; - parentLinks.resize(topology->getNumVertices(), -1); + parentLinks.resize(topology.getNumVertices(), -1); m_bfs.search(topology, startVertex, [&](int vertex, int parent) { diff --git a/vertexy/src/public/variable/IVariableDatabase.h b/vertexy/src/public/variable/IVariableDatabase.h index 369cb43..e12d097 100644 --- a/vertexy/src/public/variable/IVariableDatabase.h +++ b/vertexy/src/public/variable/IVariableDatabase.h @@ -194,6 +194,13 @@ class IVariableDatabase return getPotentialValues(varID).lastIndexOf(true); } + int getMinimumPossibleDomainValue(VarID varID) const; + int getMaximumPossibleDomainValue(VarID varID) const; + + // Default explanation for propagation. The explanation is guaranteed to be assertive (i.e. will cause backtracking) but + // is not necessarily the tightest explanation possible. (It is generally rather poor.) + static vector defaultExplainer(const NarrowingExplanationParams& params); + inline bool excludeValues(const Literal& literalToExclude, IConstraint* origin, ExplainerFunction explainer=nullptr) { return excludeValues(literalToExclude.variable, literalToExclude.values, origin, explainer); diff --git a/vertexyTestHarness/src/SolverTest.cpp b/vertexyTestHarness/src/SolverTest.cpp index 47984a9..e047671 100644 --- a/vertexyTestHarness/src/SolverTest.cpp +++ b/vertexyTestHarness/src/SolverTest.cpp @@ -251,7 +251,7 @@ int test_ruleSCCs() return nErrorCount; } -static constexpr int FORCE_SEED = 0; +static constexpr int FORCE_SEED = 42; static constexpr int NUM_TIMES = 10; static constexpr int MAZE_NUM_ROWS = 15; static constexpr int MAZE_NUM_COLS = 15; @@ -259,7 +259,7 @@ static constexpr int NQUEENS_SIZE = 25; static constexpr int SUDOKU_STARTING_HINTS = 0; static constexpr int TOWERS_NUM_DISCS = 3; static constexpr int KNIGHT_BOARD_DIM = 6; -static constexpr bool PRINT_VERBOSE = false; +static constexpr bool PRINT_VERBOSE = true; int main(int argc, char* argv[]) { @@ -267,29 +267,30 @@ int main(int argc, char* argv[]) using namespace VertexyTests; TestApplication Suite("Solver Tests", argc, argv); - Suite.AddTest("ValueBitset", test_ValueBitset); - Suite.AddTest("Digraph", test_Digraph); - Suite.AddTest("RuleSCCs", test_ruleSCCs); - Suite.AddTest("Clause-Basic", []() { return TestSolvers::solveClauseBasic(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Inequality-Basic", []() { return TestSolvers::solveInequalityBasic(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Cardinality-Basic", []() { return TestSolvers::solveCardinalityBasic(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Cardinality-Shift", []() { return TestSolvers::solveCardinalityShiftProblem(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("AllDifferent-Small", []() { return TestSolvers::solveAllDifferentSmall(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("AllDifferent-Large", []() { return TestSolvers::solveAllDifferentLarge(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Rules-BasicChoice", []() { return TestSolvers::solveRules_basicChoice(FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Rules-BasicDisjunction", []() { return TestSolvers::solveRules_basicDisjunction(FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Rules-BasicCycle", []() { return TestSolvers::solveRules_basicCycle(FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Rules-BasicIncomplete", []() { return TestSolvers::solveRules_incompleteCycle(FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Sum-Basic", []() { return TestSolvers::solveSumBasic(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("Sudoku", []() { return SudokuSolver::solve(NUM_TIMES, SUDOKU_STARTING_HINTS, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("TowersOfHanoi", []() { return TowersOfHanoiSolver::solveTowersGrid(NUM_TIMES, TOWERS_NUM_DISCS, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("TowersOfHanoi", []() { return TowersOfHanoiSolver::solveTowersDiskBased(NUM_TIMES, TOWERS_NUM_DISCS, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("TowersOfHanoi", []() { return TowersOfHanoiSolver::solverTowersDiskBasedGraph(NUM_TIMES, TOWERS_NUM_DISCS, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("KnightTourPacked", []() { return KnightTourSolver::solvePacked(NUM_TIMES, KNIGHT_BOARD_DIM, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("KnightTour", []() { return KnightTourSolver::solveAtomic(NUM_TIMES, KNIGHT_BOARD_DIM, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("NQueens-AllDifferent", []() { return NQueensSolvers::solveUsingAllDifferent(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("NQueens-Table", []() { return NQueensSolvers::solveUsingTable(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); - Suite.AddTest("NQueens-Graph", []() { return NQueensSolvers::solveUsingGraph(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("ValueBitset", test_ValueBitset); + //Suite.AddTest("Digraph", test_Digraph); + //Suite.AddTest("RuleSCCs", test_ruleSCCs); + //Suite.AddTest("Clause-Basic", []() { return TestSolvers::solveClauseBasic(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Inequality-Basic", []() { return TestSolvers::solveInequalityBasic(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Cardinality-Basic", []() { return TestSolvers::solveCardinalityBasic(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Cardinality-Shift", []() { return TestSolvers::solveCardinalityShiftProblem(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("AllDifferent-Small", []() { return TestSolvers::solveAllDifferentSmall(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("AllDifferent-Large", []() { return TestSolvers::solveAllDifferentLarge(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Rules-BasicChoice", []() { return TestSolvers::solveRules_basicChoice(FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Rules-BasicDisjunction", []() { return TestSolvers::solveRules_basicDisjunction(FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Rules-BasicCycle", []() { return TestSolvers::solveRules_basicCycle(FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Rules-BasicIncomplete", []() { return TestSolvers::solveRules_incompleteCycle(FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Sum-Basic", []() { return TestSolvers::solveSumBasic(NUM_TIMES, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("Sudoku", []() { return SudokuSolver::solve(NUM_TIMES, SUDOKU_STARTING_HINTS, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("TowersOfHanoi", []() { return TowersOfHanoiSolver::solveTowersGrid(NUM_TIMES, TOWERS_NUM_DISCS, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("TowersOfHanoi", []() { return TowersOfHanoiSolver::solveTowersDiskBased(NUM_TIMES, TOWERS_NUM_DISCS, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("TowersOfHanoi", []() { return TowersOfHanoiSolver::solverTowersDiskBasedGraph(NUM_TIMES, TOWERS_NUM_DISCS, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("NQueens-AllDifferent", []() { return NQueensSolvers::solveUsingAllDifferent(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("NQueens-Table", []() { return NQueensSolvers::solveUsingTable(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("NQueens-Graph", []() { return NQueensSolvers::solveUsingGraph(NUM_TIMES, NQUEENS_SIZE, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("KnightTourPacked", []() { return KnightTourSolver::solvePacked(NUM_TIMES, KNIGHT_BOARD_DIM, FORCE_SEED, PRINT_VERBOSE); }); + //Suite.AddTest("KnightTour", []() { return KnightTourSolver::solveAtomic(NUM_TIMES, KNIGHT_BOARD_DIM, FORCE_SEED, PRINT_VERBOSE); }); + Suite.AddTest("MazeSimple", []() { return MazeSolver::solveSimple(NUM_TIMES, MAZE_NUM_COLS, FORCE_SEED, PRINT_VERBOSE); }); Suite.AddTest("Maze", []() { return MazeSolver::solve(NUM_TIMES, MAZE_NUM_ROWS, MAZE_NUM_COLS, FORCE_SEED, PRINT_VERBOSE); }); return Suite.Run(); } diff --git a/vertexyTests/src/private/Maze.cpp b/vertexyTests/src/private/Maze.cpp index ae67dc6..1f02f92 100644 --- a/vertexyTests/src/private/Maze.cpp +++ b/vertexyTests/src/private/Maze.cpp @@ -3,6 +3,7 @@ #include "ConstraintSolver.h" #include "EATest/EATest.h" #include "constraints/ReachabilityConstraint.h" +#include "constraints/ShortestPathConstraint.h" #include "constraints/TableConstraint.h" #include "constraints/IffConstraint.h" #include "decision/LogOrderHeuristic.h" @@ -17,7 +18,9 @@ using namespace VertexyTests; // Interval of solver steps to print out current maze status. Set to 1 to see each solver step. static constexpr int MAZE_REFRESH_RATE = 0; // The number of keys/doors that should exist in the maze. -static constexpr int NUM_KEYS = 3; +static constexpr int NUM_KEYS = 1; +// Test Shortest Path constraint (slow), recommend 1 key. +static constexpr bool TEST_SHORTEST_PATH = true; // True to print edge variables in FMaze::Print static constexpr bool PRINT_EDGES = false; // Whether to write a decision log as DecisionLog.txt @@ -57,6 +60,100 @@ class DebugMazeStrategy : public ISolverDecisionHeuristic ConstraintSolver& m_solver; }; +int MazeSolver::solveSimple(int times, int numCols, int seed, bool printVerbose) +{ + int nErrorCount = 0; + + ConstraintSolver solver(TEXT("Maze"), seed); + VERTEXY_LOG("TestMaze(%d)", solver.getSeed()); + + constexpr int BLANK_IDX = 0; + constexpr int ENTRANCE_IDX = 1; + constexpr int EXIT_IDX = 2; + + // Predefined combinations of values for cells + const vector cell_Blank{ BLANK_IDX }; + const vector cell_Entrance{ ENTRANCE_IDX }; + const vector cell_Exit{ EXIT_IDX }; + + // The domain determines the range of values that each tile takes on + SolverVariableDomain tileDomain(0, 2); + + // Create the topology for the maze. + shared_ptr grid = make_shared(numCols, 1); + + // Create a variable for each tile in the maze. + auto tileData = solver.makeVariableGraph(TEXT("TileVars"), ITopology::adapt(grid), tileDomain, TEXT("Cell")); + + for (int x = 0; x < numCols; ++x) + { + uint32_t node = grid->coordinateToIndex(x, 0); + solver.setInitialValues(tileData->get(node), vector{0, 1, 2}); + } + +// +// CONSTRAINT: Exactly one entrance, one exit, +// + hash_map> globalCardinalities; + globalCardinalities[ENTRANCE_IDX] = make_tuple(1, 1); // Min = 1, Max = 1 + globalCardinalities[EXIT_IDX] = make_tuple(1, 1); // Min = 1, Max = 1 + solver.cardinality(tileData->getData(), globalCardinalities); + + // +// Define a domain for edges between tiles. Each edge is either solid or empty. +// + +// Edge graphs per step: 0 = passable, 1 = impassable + SolverVariableDomain edgeDomain(0, 1); + const vector edge_Empty{ 0 }; + const vector edge_Solid{ 1 }; + + // Create the edge topology for the maze. This creates a parallel graph where each node in Edges corresponds + // to an edge in Grid. + auto edges = make_shared(ITopology::adapt(grid), true, false); + + auto selfTile = make_shared>(tileData); + + auto stepEdgeData = solver.makeVariableGraph(TEXT("EdgeVars"), ITopology::adapt(edges), edgeDomain, TEXT("Edge")); + + auto edgeNodeToEdgeVarRel = make_shared>(stepEdgeData); + + solver.makeConstraint(tileData, cell_Entrance, cell_Exit, stepEdgeData, edge_Solid, EConstraintOperator::GreaterThan, 5); + + + // + // Solve! + // + for (int i = 0; i < times; ++i) + { + EConstraintSolverResult result = solver.startSolving(); + while (result == EConstraintSolverResult::Unsolved) + { + if (ATTEMPT_SOLUTION_AT >= 0 && solver.getStats().stepCount >= ATTEMPT_SOLUTION_AT) + { + solver.debugAttemptSolution(TEXT("MazeSolution.txt")); + } + + result = solver.step(); + // print out the maze every MAZE_REFRESH_RATE steps + if (printVerbose && MAZE_REFRESH_RATE > 0 && (solver.getStats().stepCount % MAZE_REFRESH_RATE) == 0) + { + //print(stepDatas[0], stepEdgeDatas[0], solver); + } + } + + // Print out the final maze! + if (printVerbose) + { + print(tileData, stepEdgeData, solver); + } + solver.dumpStats(printVerbose); + EATEST_VERIFY(result == EConstraintSolverResult::Solved); + } + + return nErrorCount; +} + int MazeSolver::solve(int times, int numRows, int numCols, int seed, bool printVerbose) { int nErrorCount = 0; @@ -310,6 +407,7 @@ int MazeSolver::solve(int times, int numRows, int numCols, int seed, bool printV // vector>> stepDatas; vector>> stepEdgeDatas; + vector>> stepDoorDatas; for (int step = 0; step < NUM_KEYS + 1; ++step) { // @@ -321,18 +419,57 @@ int MazeSolver::solve(int times, int numRows, int numCols, int seed, bool printV auto selfStepTile = make_shared>(stepData); - // If this tile is the entrance in the maze, constrain it to be the entrance in this step. + auto stepDoorData = solver.makeVariableGraph(stepName, ITopology::adapt(grid), stepDomain, { wstring::CtorSprintf(), TEXT("StepDoor%d-"), step }); + stepDoorDatas.push_back(stepDoorData); + auto selfStepDoorTile = make_shared>(stepDoorData); + // constraint solver.makeGraphConstraint(grid, - GraphRelationClause(selfStepTile, step_Origin), - vector{GraphRelationClause(selfTile, cell_Entrance)} + GraphRelationClause(selfStepDoorTile, step_Origin), + vector{ GraphRelationClause(selfTile, step == 0 ? cell_Entrance : vector{cell_Doors[step - 1]})} ); + // if stepDoor != reachable, tile can't be a door + solver.makeGraphConstraint(grid, ENoGood::NoGood, + GraphRelationClause(selfStepDoorTile, EClauseSign::Outside, step_Reachable), + GraphRelationClause(selfTile, step == NUM_KEYS ? cell_Exit : vector{ cell_Keys[step] }) + ); + + if (TEST_SHORTEST_PATH) + { + //if this is the most recent door, constrain it to the be the entrance in this step + //solver.makeGraphConstraint(grid, + // GraphRelationClause(selfStepTile, step_door), + // vector{ GraphRelationClause(selfTile, step == 0 ? cell_Entrance : vector{cell_Doors[step - 1]})} + //); + + solver.makeGraphConstraint(grid, + GraphRelationClause(selfStepTile, step_Origin), + vector{ GraphRelationClause(selfTile, cell_Entrance) } + ); + } + else + { + //If this tile is the entrance in the maze, constrain it to be the entrance in this step. + solver.makeGraphConstraint(grid, + GraphRelationClause(selfStepTile, step_Origin), + vector{ GraphRelationClause(selfTile, cell_Entrance) } + ); + } + // A tile can never be passable in any step if it is a wall solver.makeGraphConstraint(grid, ENoGood::NoGood, GraphRelationClause(selfStepTile, step_ReachableOrOrigin), GraphRelationClause(selfTile, cell_Wall) ); + if (TEST_SHORTEST_PATH) + { + solver.makeGraphConstraint(grid, ENoGood::NoGood, + GraphRelationClause(selfStepDoorTile, step_ReachableOrOrigin), + GraphRelationClause(selfStepTile, EClauseSign::Outside, step_ReachableOrOrigin) + ); + } + // If we don't have all the keys at this step... if (step < NUM_KEYS) { @@ -430,7 +567,15 @@ int MazeSolver::solve(int times, int numRows, int numCols, int seed, bool printV } // Ensure reachability for this step: all Step_Reachable cells must be reachable from Step_Origin cells. - solver.makeConstraint(stepData, step_Origin, step_Reachable, stepEdgeData, edge_Solid); + if (TEST_SHORTEST_PATH) + { + solver.makeConstraint(stepDoorData, step_Origin, step_Reachable, stepEdgeData, edge_Solid, EConstraintOperator::LessThan, 10); + solver.makeConstraint(stepData, step_Origin, step_Reachable, stepEdgeData, edge_Solid); + } + else + { + solver.makeConstraint(stepData, step_Origin, step_Reachable, stepEdgeData, edge_Solid); + } } // Uncomment to print out the maze every time the solver backtracks (for debugging) @@ -474,6 +619,17 @@ int MazeSolver::solve(int times, int numRows, int numCols, int seed, bool printV if (printVerbose && MAZE_REFRESH_RATE > 0 && (solver.getStats().stepCount % MAZE_REFRESH_RATE) == 0) { print(stepDatas[0], stepEdgeDatas[0], solver); + VERTEXY_LOG("step door data"); + print(stepDoorDatas[1], stepEdgeDatas[1], solver); + VERTEXY_LOG("step data"); + print(stepDatas[1], stepEdgeDatas[1], solver); + VERTEXY_LOG("start edge data"); + for (int i = 0; i < (numRows * numCols) - 1; i++) + { + auto edge = stepEdgeDatas[1]->get(i); + VERTEXY_LOG(" %s --> %s", solver.getVariableName(edge).c_str(), solver.getVariableDB()->getPotentialValues(edge).toString().c_str()); + } + VERTEXY_LOG("end edge data"); } } @@ -567,15 +723,15 @@ void MazeSolver::print(const shared_ptr>& cells, cons for (int x = 0; x < numCols; ++x) { out.append_sprintf(TEXT("%d"), x); - if (x < 10) + if (x < 9) { out += TEXT(" "); } - if (x < 100) + if (x < 99) { out += TEXT(" "); } - if (PRINT_EDGES && x < 1000) + if (PRINT_EDGES && x < 999) { out += TEXT(" "); } diff --git a/vertexyTests/src/public/Maze.h b/vertexyTests/src/public/Maze.h index a3eb6aa..c4d381c 100644 --- a/vertexyTests/src/public/Maze.h +++ b/vertexyTests/src/public/Maze.h @@ -16,6 +16,8 @@ class MazeSolver } public: + static int solveSimple(int times, int numCols, int seed, bool printVerbose = true); + static int solve(int times, int numRows, int numCols, int seed, bool printVerbose=true); static int check(const shared_ptr>& Cells, const ConstraintSolver& solver); static void print(const shared_ptr>& cells, const shared_ptr>& edges, const ConstraintSolver& solver);