expdef:
name:Generate abductive hypotheses
info:~
This experiment definition generates abducibles for a specified abductive problem.

Results and details are published in Transactions on Computational Logic, 2014,
"Identifying efficient abductive hypotheses using multi-criteria dominance relation"
by M. Komosinski, A. Kups, D. Leszczynska-Jasion and M. Urbanski.

See also readme-abduction.txt and run-abduction.cmd.
~
code:~

global g_params;
global g_form;
global g_set;
global g_file;
global g_symbolsChart;
global g_oldSymbolsChart;

function onExpDefLoad()
{
  GenePools.clear();
  Populations.clear();
  Populations[0].clear();
 
  Math.randomize();
	
	
	var g_params = Vector.new();
	
	//Logical symbols chart including up to nine distinct variables
	g_symbolsChart = ["N", "K", "A", "C", "p", "q", "r", "s", "t", "u", "v", "w", "x"];
	
	g_form = Vector.new();
	g_set = Vector.new();
	g_file = "";	

}


function onExpInit()
{
	//Initialization of the experiment parameters loaded from file
	g_params = String.split(ExpParams.params, ";");
	if(g_params.size == 3)
	{
		//Conversion of the string characters into a numerical encoding
		var i,j;
		var splitedForm = String.split(g_params[0],"_");
		
		for(i = 0; i < splitedForm.size; i++)
		{
			g_form.add(g_symbolsChart.find(splitedForm[i]));
		}
		
		var splitedSet = String.split(g_params[1], " ");
		var splitedElt = Vector.new();
		
		for(i = 0; i < splitedSet.size; i++)
		{
			g_set.add(Vector.new());
			splitedElt = String.split(splitedSet[i], "_");	
		
			for(j = 0; j < splitedElt.size; j++)
			{
				g_set[i].add(g_symbolsChart.find(splitedElt[j]));
			}
		}
		
		g_file = g_params[2];
		
	} else
	  {
		Simulator.print("Something is not right with the experiment parameters!");
	  }
	  
}

function onStep()
{
	if(g_params.size == 3)
	{
		//Call of the main function of the experiment
		getRawHypotheses(g_set, g_form, g_file);
		Simulator.stop();
	} else
	  {
		Simulator.print("Something is wrong with experiment parameters! Stopping simulation...");
		Simulator.stop();
	  }
}

//Main function of the experiment
function getRawHypotheses(set, form, fileName)
{
		var i,j;
		//Generation of the list containg all the formulas of the problem
		var formulas = Vector.new();
		for(i = 0; i < set.size; i++)
			formulas.add(set[i]);
		
		formulas.add(form);	
		//Generation of the list containing all the subformulas of the problem
		var subformulas = Vector.new();
		for(i = 0; i < formulas.size; i++)
		{
		
			var tempSf = getSubFormulasIndexed(formulas[i]);
			for(j = 0; j < tempSf.size; j++)
			{
				if(findPlainList(subformulas, tempSf[j]) == -1)
					subformulas.add(tempSf[j]);
			}
			
		}
	
		//Generation of the list containing all the variables of the problem
		var variables = getVariablesIndexed(subformulas);
		
		//Generation of the synthetic inferences list
		var inferences = generateSyntheticInfFromSetIndexed(formulas, subformulas, variables);
		
		//Checking whether a tableau is closed
		var success = checkTableauSuccess(inferences, formulas);
		if(!success)
		{
			//Generation of the output file name
			var fileNSplit = String.split(fileName, ".");
			var  fName = fileNSplit[0] + "RawHyp.txt";
			
			//Generation and preprocessing list of the abductive hypotheses
			rawHypothesesGeneration(inferences, set, form, formulas, fName);
			
	
		} else
		  {
			//Printing out of the output if the table is closed
			var setLatex = convertIndexedSetToLatex(set);
			var infix = Vector.new();
			infix = indexesPrefixToInfix(form, infix);
			var formInfix = createInfixFormFromIndexesInfix(infix);
			var formLatex = formToLatex(formInfix);
			
			writeInfo(fileName, "#set: " + setLatex + "	form: " + formLatex + "\n");
			writeInfo(fileName, "success\n");
		  }
		  
}

function rawHypothesesGeneration(inferences, set, form, formulas, file_name)
{
	
	var valid = checkTableValidity(inferences, formulas);
	
	//Function that gets failure inferences
	var partialTableaux = getFailures(inferences, formulas);
	var partialTableau = partialTableaux[0];
	
	//Functions that get and reduce entangled literals clauses
	var entangledLiterals = getEntangledLiterals(partialTableau, formulas);
	var entangledHuman = getFormListFromIndexes(entangledLiterals);
	var cleaned = cleanEntangledLiterals(entangledLiterals);
	var cleanedHuman = getFormListFromIndexes(cleaned);
	var cleanedSorted = sortLiteralsWithinSets(cleaned);
	var simplifiedCleanedSorted = getSymmetricalDifferences(cleanedSorted);
	var simplifiedCleanedSortedNonRep = filterOutRepeatingLiteralsLists(simplifiedCleanedSorted);
	var bhi = generateBaseHypotheses(simplifiedCleanedSortedNonRep);
	var bhiHuman = getFormListFromIndexes(bhi);
	var bhi_sorted = sortLiteralsWithinSets(bhi);
	var bhi_cons = filterOutNonConsistentLiteralsLists(bhi_sorted);
	var bhi_consHuman = getFormListFromIndexes(bhi_cons);
	var bhi_non_rep = filterOutRepeatingLiteralsLists(bhi_cons);
	var bhi_non_repHuman = getFormListFromIndexes(bhi_non_rep);
	var simplified = getSymmetricalDifferences(bhi_non_rep);
	var simpl_non_rep = filterOutRepeatingLiteralsLists(simplified);
	var simpl_non_repHuman = getFormListFromIndexes(simpl_non_rep);
	var minimalSet = removeLiteralsSupSets(simpl_non_rep);
	var minimalSetHuman = getFormListFromIndexes(minimalSet);
	 
	var baseHypotheses  = Vector.new();
	var i;
	for(i = 0; i < minimalSet.size; i++)
		baseHypotheses.add(formulaFromLiterals(minimalSet[i])); 
		
	//Functions converting	encoded literals into human readable formats
	var hypothesesAllBinary = generateBinaryCombinations(baseHypotheses.size);
	var setLatex = convertIndexedSetToLatex(set);
	var dnf = binaryToForm(hypothesesAllBinary[hypothesesAllBinary.size - 1], baseHypotheses);
	var infix = Vector.new(); 
	infix = indexesPrefixToInfix(form, infix);
	var formInfix = createInfixFormFromIndexesInfix(infix);
	var formLatex = formToLatex(formInfix);
		
	//Printing out the most important information into the specified earlier output file 	
	writeInfo(file_name, "#set: " + setLatex + "\n#form: " + formLatex  + "\n");
	writeInfo(file_name, "#tableau-validation: " + valid + "\n");
	writeInfo(file_name, "#\n");	
	writeInfo(file_name, "#base hypotheses count:\n");
	writeInfo(file_name, "#raw-size: " + entangledLiterals.size + "\n");
	writeInfo(file_name, "#cleaned-size: " + cleaned.size + "\n");
	writeInfo(file_name, "#non-filtered-raw: nf=" + entangledLiterals[0].size);
	
	for(i = 1; i <  entangledLiterals.size; i++)
		writeInfo(file_name,"*" + entangledLiterals[i].size);
		
	writeInfo(file_name, "\n#entangled-literals-raw: NA \n");
	writeInfo(file_name, "#non-filtered: nf=" + cleaned[0].size);
		
	for(i = 1; i <  cleaned.size; i++)
		writeInfo(file_name,"*" + cleaned[i].size);
		
	writeInfo(file_name, "\n");
	writeInfo(file_name, "#entangled-literals: " + cleanedHuman + "\n");
	writeInfo(file_name, "#simplify-stage-1-size: " + bhi.size + "\n");
	writeInfo(file_name, "#simplify-stage-1-hypotheses: " + bhiHuman + "\n");
	writeInfo(file_name, "#simplify-stage-1-consistent-size: " + bhi_cons.size + "\n");
	writeInfo(file_name, "#simplify-stage-1-consistent-hypotheses: " + bhi_consHuman + "\n");
	writeInfo(file_name, "#simplify-stage-1-consistent-non_repeated-size: " + bhi_non_rep.size + "\n");
	writeInfo(file_name, "#simplify-stage-1-consistent-non_repeated-hypotheses: " + bhi_non_repHuman + "\n");
	writeInfo(file_name, "#simplify-stage-2-size: " + simpl_non_rep.size + "\n");
	writeInfo(file_name, "#simplify-stage-2-hypotheses: " + simpl_non_repHuman + "\n");
	writeInfo(file_name, "#simplify-stage-3-size: " + minimalSet.size + "\n");
	writeInfo(file_name, "#simplify-stage-3-hypotheses: " + minimalSetHuman + "\n");
	writeInfo(file_name, "#number	formatChar	prefix_form	infix_form	formatHumanLatex_infix\n");
	
	
	//Generation and printing out of the base abductive hypotheses
	for(i = 0; i < hypothesesAllBinary.size; i++)
	{
		var current = binaryToForm(hypothesesAllBinary[i], baseHypotheses);
		var currentIndexed = binaryToIndex(hypothesesAllBinary[i], minimalSet);		
		writeInfo(file_name,"" + (i+1) + "	" + hypothesesAllBinary[i] + "	" + current + "	");
		
		var infix = Vector.new();
		infix = indexesPrefixToInfix(currentIndexed, infix);
		var formInfix = createInfixFormFromIndexesInfix(infix);
		var latex = formToLatex(formInfix);
		writeInfo(file_name,""  + formInfix + "	" + latex + "\n");
	}
	
}

@include "abduction_misc.inc"
@include "data_conversion.inc"
@include "formulas_processing.inc"
@include "lists_processing.inc"
@include "literals_processing.inc"
@include "synthetic_rules.inc"
@include "synthetic_tableau.inc"

~

prop:
id:params
name:Logical experiment parameters
help:See readme-abduction.txt
type:s