<commit_before>/* dlvhex -- Answer-Set Programming with external interfaces.
 * Copyright (C) 2005, 2006, 2007 <NAME>
 * Copyright (C) 2006, 2007, 2008, 2009, 2010 <NAME>
 * Copyright (C) 2009, 2010 <NAME>
 * Copyright (C) 2011, 2012, 2013 <NAME>
 * 
 * This file is part of dlvhex.
 *
 * dlvhex is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License as
 * published by the Free Software Foundation; either version 2.1 of
 * the License, or (at your option) any later version.
 *
 * dlvhex is distributed in the hope that it will be useful, but
 * WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with dlvhex; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
 * 02110-1301 USA.
 */

/**
 * @file NogoodGrounder.cpp
 * @author <NAME>
 *
 * @brief Implements a grounder for nonground nogoods.
 */

#define DLVHEX_BENCHMARK

#include "dlvhex2/NogoodGrounder.h"
#include "dlvhex2/Logger.h"
#include "dlvhex2/Registry.h"
#include "dlvhex2/Printer.h"
#include "dlvhex2/Benchmarking.h"
#include "dlvhex2/Nogood.h"

#include <bm/bmalgo.h>

#include <boost/foreach.hpp>

DLVHEX_NAMESPACE_BEGIN

NogoodGrounder::NogoodGrounder(RegistryPtr reg, SimpleNogoodContainerPtr watched, SimpleNogoodContainerPtr destination, AnnotatedGroundProgram& agp) :
	reg(reg), watched(watched), destination(destination), agp(agp){
}

void NogoodGrounder::resetWatched(SimpleNogoodContainerPtr watched){
	this->watched = watched;
}

ImmediateNogoodGrounder::ImmediateNogoodGrounder(RegistryPtr reg, SimpleNogoodContainerPtr watched, SimpleNogoodContainerPtr destination, AnnotatedGroundProgram& agp) :
	NogoodGrounder(reg, watched, destination, agp), instantiatedNongroundNogoodsIndex(0){
}

void ImmediateNogoodGrounder::update(InterpretationConstPtr partialInterpretation, InterpretationConstPtr factWasSet, InterpretationConstPtr changed){

	// go through all nonground nogoods which have not been instantiated so far
	int max = watched->getNogoodCount();
	if (instantiatedNongroundNogoodsIndex >= max) instantiatedNongroundNogoodsIndex = 0;
	DBGLOG(DBG, "Updating nogood grounder from " << instantiatedNongroundNogoodsIndex << " to " << max);
	for (int i = instantiatedNongroundNogoodsIndex; i < max; ++i){
		Nogood ng = watched->getNogood(i);
		DBGLOG(DBG, "Checking nogood " << ng.getStringRepresentation(reg));
		if (ng.isGround()) continue;

		DBGLOG(DBG, "Searching for watched literal in nogood " << i);
		int maxBoundVariables = 0;
		ID watchedLit = ID_FAIL;
		BOOST_FOREACH (ID lit, ng){
			if (lit.isOrdinaryGroundAtom()) continue;

			const OrdinaryAtom& atom = reg->onatoms.getByID(lit);

			std::set<ID> distinctVar;
			int var = 0;
			BOOST_FOREACH (ID p, atom.tuple){
				if (p.isVariableTerm()){
					if (std::find(distinctVar.begin(), distinctVar.end(), p) == distinctVar.end()){
						distinctVar.insert(p);
						var++;
					}
				}
			}

			if (var > maxBoundVariables){
				maxBoundVariables = var;
				watchedLit = lit;
			}
		}
		assert (watchedLit != ID_FAIL);

		// watch the atom and the corresponding nogood
		DBGLOG(DBG, "Watching literal " << watchedLit << " in nogood " << i);
		const OrdinaryAtom& watchedAtom = reg->onatoms.getByAddress(watchedLit.address);

		// For each atom A of the program, check if the watched literal unifies with A
		bm::bvector<>::enumerator en = agp.getProgramMask()->getStorage().first();
		bm::bvector<>::enumerator en_end = agp.getProgramMask()->getStorage().end();

		DBGLOG(DBG, "Searching for unifying program atoms");
		while (en < en_end){

			DBGLOG(DBG, "Checking atom " << *en);

			const OrdinaryAtom& currentAtom = reg->ogatoms.getByAddress(*en);
			if (currentAtom.unifiesWith(watchedAtom, reg)){
				Nogood instantiatedNG;
				ng.match(reg, reg->ogatoms.getIDByAddress(*en), instantiatedNG);
				DBGLOG(DBG, "Instantiated " << instantiatedNG.getStringRepresentation(reg) << " from " << ng.getStringRepresentation(reg));

				// check if the instance of the nogood contains a ground literal which does not appear in the program
				bool relevant = true;
				Nogood simplifiedNG;
				BOOST_FOREACH (ID lit, instantiatedNG){
					if (lit.isOrdinaryGroundAtom() && !agp.getProgramMask()->getFact(lit.address)){
						if (!lit.isNaf()){
							// can never be true --> remove whole instance
							relevant = false;
							break;
						}else{
							// is always true --> remove literal
						}
					}else{
						// might be true --> keep literal
						simplifiedNG.insert(lit);
					}
				}

				if (relevant){
					if (simplifiedNG.isGround()){
						destination->addNogood(simplifiedNG);
					}else{
						watched->addNogood(simplifiedNG);
					}
				}
			}

			en++;
		}

	}
	instantiatedNongroundNogoodsIndex = max;
}
<commit_msg>fix a bug in nogood grounder<commit_after>/* dlvhex -- Answer-Set Programming with external interfaces.
 * Copyright (C) 2005, 2006, 2007 <NAME>
 * Copyright (C) 2006, 2007, 2008, 2009, 2010 <NAME>
 * Copyright (C) 2009, 2010 <NAME>
 * Copyright (C) 2011, 2012, 2013 <NAME>
 * 
 * This file is part of dlvhex.
 *
 * dlvhex is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License as
 * published by the Free Software Foundation; either version 2.1 of
 * the License, or (at your option) any later version.
 *
 * dlvhex is distributed in the hope that it will be useful, but
 * WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with dlvhex; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
 * 02110-1301 USA.
 */

/**
 * @file NogoodGrounder.cpp
 * @author <NAME>
 *
 * @brief Implements a grounder for nonground nogoods.
 */

#define DLVHEX_BENCHMARK

#include "dlvhex2/NogoodGrounder.h"
#include "dlvhex2/Logger.h"
#include "dlvhex2/Registry.h"
#include "dlvhex2/Printer.h"
#include "dlvhex2/Benchmarking.h"
#include "dlvhex2/Nogood.h"

#include <bm/bmalgo.h>

#include <boost/foreach.hpp>

DLVHEX_NAMESPACE_BEGIN

NogoodGrounder::NogoodGrounder(RegistryPtr reg, SimpleNogoodContainerPtr watched, SimpleNogoodContainerPtr destination, AnnotatedGroundProgram& agp) :
	reg(reg), watched(watched), destination(destination), agp(agp){
}

void NogoodGrounder::resetWatched(SimpleNogoodContainerPtr watched){
	this->watched = watched;
}

ImmediateNogoodGrounder::ImmediateNogoodGrounder(RegistryPtr reg, SimpleNogoodContainerPtr watched, SimpleNogoodContainerPtr destination, AnnotatedGroundProgram& agp) :
	NogoodGrounder(reg, watched, destination, agp), instantiatedNongroundNogoodsIndex(0){
}

void ImmediateNogoodGrounder::update(InterpretationConstPtr partialInterpretation, InterpretationConstPtr factWasSet, InterpretationConstPtr changed){

	// go through all nonground nogoods which have not been instantiated so far
	int max = watched->getNogoodCount();
	if (instantiatedNongroundNogoodsIndex >= max) instantiatedNongroundNogoodsIndex = 0;
	DBGLOG(DBG, "Updating nogood grounder from " << instantiatedNongroundNogoodsIndex << " to " << max);
	for (int i = instantiatedNongroundNogoodsIndex; i < max; ++i){
		Nogood ng = watched->getNogood(i);
		DBGLOG(DBG, "Checking nogood " << ng.getStringRepresentation(reg));
		if (ng.isGround()) continue;

		DBGLOG(DBG, "Searching for watched literal in nogood " << i);
		int maxBoundVariables = 0;
		ID watchedLit = ID_FAIL;
		BOOST_FOREACH (ID lit, ng){
			if (lit.isOrdinaryGroundAtom()) continue;

			const OrdinaryAtom& atom = reg->onatoms.getByID(lit);

			std::set<ID> distinctVar;
			int var = 0;
			BOOST_FOREACH (ID p, atom.tuple){
				if (p.isVariableTerm()){
					if (std::find(distinctVar.begin(), distinctVar.end(), p) == distinctVar.end()){
						distinctVar.insert(p);
						var++;
					}
				}
			}

			if (var > maxBoundVariables){
				maxBoundVariables = var;
				watchedLit = lit;
			}
		}
		assert (watchedLit != ID_FAIL);

		// watch the atom and the corresponding nogood
		DBGLOG(DBG, "Watching literal " << watchedLit << " in nogood " << i);
		const OrdinaryAtom& watchedAtom = reg->onatoms.getByAddress(watchedLit.address);

		// For each atom A of the program, check if the watched literal unifies with A
		bm::bvector<>::enumerator en = agp.getProgramMask()->getStorage().first();
		bm::bvector<>::enumerator en_end = agp.getProgramMask()->getStorage().end();

		DBGLOG(DBG, "Searching for unifying program atoms");
		while (en < en_end){

			DBGLOG(DBG, "Checking atom " << *en);

			const OrdinaryAtom& currentAtom = reg->ogatoms.getByAddress(*en);
			if (currentAtom.unifiesWith(watchedAtom, reg)){
				Nogood instantiatedNG;
				ng.match(reg, reg->ogatoms.getIDByAddress(*en), instantiatedNG);
				DBGLOG(DBG, "Instantiated " << instantiatedNG.getStringRepresentation(reg) << " from " << ng.getStringRepresentation(reg));

				// check if the instance of the nogood contains a ground literal which does not appear in the program
				bool relevant = true;
				Nogood simplifiedNG;
				BOOST_FOREACH (ID lit, instantiatedNG){
					if (lit.isOrdinaryGroundAtom() && !reg->ogatoms.getIDByAddress(lit.address).isAuxiliary() && !agp.getProgramMask()->getFact(lit.address)){
						if (!lit.isNaf()){
							// can never be true --> remove whole instance
							relevant = false;
							break;
						}else{
							// is always true --> remove literal
						}
					}else{
						// might be true --> keep literal
						simplifiedNG.insert(lit);
					}
				}

				if (relevant){
					if (simplifiedNG.isGround()){
						destination->addNogood(simplifiedNG);
					}else{
						watched->addNogood(simplifiedNG);
					}
				}
			}

			en++;
		}

	}
	DBGLOG(DBG, "Finished updating");
	instantiatedNongroundNogoodsIndex = max;
}

{'fraction_non_alphanumeric': 0.11520600731153048, 'fraction_numerical': 0.014820669894279222, 'mean_word_length': 4.185450819672131, 'pattern_counts': {'":': 0, '<': 75, '<?xml version=': 0, '>': 58, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2061867', 'n_tokens_mistral': 3862, 'n_tokens_neox': 3264, 'n_words': 909}