/* * File: Skolem.hpp * Author: Ajith John * * Created on 27 December, 2013 */ #ifndef SKOLEM_HPP #define SKOLEM_HPP #include "helper.hpp" #include "ExpressionManager.h" #include "HashTable_WithStandardKeys.h" #include "LogManager.h" #include #include #include #include #include #include using namespace std; class Skolem { public: // pointer to expression manager t_ExpressionManager* pub_em; int number_of_factors; // number of factors in the original problem int number_of_vars_to_elim; // number of variables to eliminate in the original problem // GLOBAL MATRICES AND SETS // maps are created between names of variables to be eliminated and their indices. map var_name_to_var_index_map; // name --> index map map var_index_to_var_name_map; // index --> name map // matrix storing the skylines map > Skylines; set UnionOfSkylines; // union of all skylines // matrix storing factors map FactorMatrix; // factor index ---> factor // var to elim index ---> delta combined with the variables up to subst_index substituted (used when ompute_delta_combined_as_individual_factors is false) map DeltaCombinedMatrix; // version of DeltaCombinedMatrix stored factor-wise (used when compute_delta_combined_as_individual_factors is true) map > FactorWiseDeltaCombinedMatrix; // var to elim index ---> index of the variable up to which substitution is made in delta combined map DeltaCombinedSubstMatrix; // matrix storing skolemfunctions map SkolemFunctions; // var to elim index ---> skolem function // abstracted ---> un-abstracted functions map AbstractedTounabstractedFunctionsMap; // VARIABLE-SPECIFIC MATRICES AND SETS // THESE ARE CLEANED AFTER FINDING SKOLEM-FUNCTION FOR THE VARIABLE set FactorsWithVariable; // matrices storing alpha, beta, gamma, delta, cofactors, and their negations map CofactorOneMatrix; // factor index ---> co-factor 1 map CofactorZeroMatrix; // factor index ---> co-factor 0 map NegatedCofactorOneMatrix; // factor index ---> not(co-factor 1) map NegatedCofactorZeroMatrix; // factor index ---> not(co-factor 0) map AlphaMatrix; // factor index ---> alpha map BetaMatrix; // factor index ---> beta map GammaMatrix; // factor index ---> gamma map DeltaMatrix; // factor index ---> delta // CACHES FOR REPLACING VARIABLE TO BE ELIMINATED BY ZERO AND BY ONE t_HashTable pub_cofactor_zero_cache; t_HashTable pub_cofactor_one_cache; // GLOBAL MATRICES AND SETS FOR RECORD-KEEPING #ifdef RECORD_KEEP map original_factor_sizes; // sizes of original factors map abstracted_factor_sizes; // sizes of factors after abstraction - replacement by UFs map original_factor_support_sizes; // sizes of supports of original factors map original_factor_varstoelim_sizes; // number of variables to eliminate in original factors int original_support_size; // size of support of factor_1 \wedge ... \wedge factor_n int NumberOfFactors; // number of factors containing the var to elim int SkylineSize; // size of skyline unsigned long long int SkolemFunctionGenTime; // time to generate skolem function unsigned long long int AlphaCombGenTime; // time to generate alpha combined unsigned long long int SkylineGenTime; // time to generate skyline unsigned long long int DeltaPartGenTime; // time to generate delta part unsigned long long int DeltaCombGenTime; // time to generate delta combined unsigned long long int NextFactorGenTime; // time to generate next factor unsigned long long int CorrectionPartGenTime; // time to generate correction part int SkolemFunctionSize; // size of skolem function int AlphaPartSize; // size of alpha \or gamma part int DeltaPartSize; // size of delta part int DeltaCombinedSize; // size of delta combined int CorrectionPartSize; // size of correction part int number_of_compose_operations_for_variable; #endif list FactorsAffectingSkolemFunction; // list of factors which affect the skolem function of the variable list sizes_of_factors_affecting_variable; // sizes of factors which affect the skolem function of the variable list sizes_of_conflict_conjuncts_affecting_variable; // sizes of conjunctions of conflicts which affect the skolem function of the variable list sizes_of_cofactors_affecting_variable; // sizes of cofactors which affect the skolem function of the variable unsigned long long int total_time_in_ordering_for_the_variable; // ordering time for the present variable #ifdef DETAILED_RECORD_KEEP list sizes_of_factors_with_variable; unsigned long long int ComposeTime; // total time consumed in compose unsigned long long int FactorFindingTime; // total time consumed in support-finding set PreviousFactorsWithVariable; // factors with variable for the variable just eliminated #endif // Constructor, desctructor Skolem(t_ExpressionManager* em); ~Skolem(); static Skolem* Skolem_instance; static Skolem* getInstance(t_ExpressionManager* em); /** * The factorized skolem function generator * @param factors * @param variables to be eliminated */ void factorizedSkolemFunctionGenerator(set &Factors, list &VariablesToEliminate); /** * Initializes the fields of Skolem class and * Decides the order in which variables are to be eliminated * when disable_factorization=false * @param factors * @param variables to be eliminated */ void initializeFactorizedSkolemFunctionGenerator(set &Factors, list &VariablesToEliminate); /** * Computes skolem function for a given variable * @param index of the variable to be eliminated * @param alpha_combined_or_gamma_combined computed inside */ t_Expression* computeSkolemFunction(int var_to_elim_index, t_Expression* &alpha_combined_or_gamma_combined); /** * Computes the set of factors with the given variable in support * @param index of the variable to be eliminated */ void findFactorsWithVariable(int var_to_elim_index); /** * Computes delta combined for the variable at delta_combined_index with * the variables at delta_combined_index+1 to var_to_elim_index-1 replaced by their skolem functions * and the variable at var_to_elim_index replaced by 0 */ t_Expression* computeDeltaCombinedWithSubstitutions(int delta_combined_index, int var_to_elim_index); /** * Computes delta combined for the variable at delta_combined_index with * the variables at delta_combined_index+1 to subst_index replaced by their skolem functions */ t_Expression* computeDeltaCombinedWithSkolemFunctionsSubstituted(int delta_combined_index, int subst_index); /** * Computes alpha combined for a given variable * @param index of the variable to be eliminated */ t_Expression* computeAlphaCombined(int var_to_elim_index); /** * Computes delta combined for a given variable * @param index of the variable to be eliminated * Note that 1) Only pair-wise conflicts are considered; single conflicts are not considered. * 2) returns false if all factors are free of the variable. * Note that as per defn. of delta, result should be \neg(conjunction of factors)) in this case; * but returning false should serve the purpose here. */ t_Expression* computeDeltaCombined(int var_to_elim_index); t_Expression* computeDeltaCombined(int var_to_elim_index, t_Expression* local_skolem_function); /** * Updates the factor matrix after skolem function of a variable is computed * using the local skolem functions * @param index of the variable whose skolem function is just computed */ void updateFactors(int var_to_elim_index); /** * Computes alpha at location [var_to_elim_index][factor_index] * @param index of the variable to be eliminated * @param index of the factor */ t_Expression* computeAlpha(int var_to_elim_index, int factor_index); /** * Computes beta at location [var_to_elim_index][factor_index] * @param index of the variable to be eliminated * @param index of the factor */ t_Expression* computeBeta(int var_to_elim_index, int factor_index); /** * Computes gamma at location [var_to_elim_index][factor_index] * @param index of the variable to be eliminated * @param index of the factor */ t_Expression* computeGamma(int var_to_elim_index, int factor_index); /** * Computes delta at location [var_to_elim_index][factor_index] * @param index of the variable to be eliminated * @param index of the factor */ t_Expression* computeDelta(int var_to_elim_index, int factor_index); /** * Computes cofactor-1 at location [var_to_elim_index][factor_index] * Takes (computes) factor at location [var_to_elim_index][factor_index], and * replaces occurences of variable at var_to_elim_index by 1. * @param index of the variable to be eliminated * @param index of the factor */ t_Expression* computeCofactorOne(int var_to_elim_index, int factor_index); /** * Computes the negation of cofactor-1 at location [var_to_elim_index][factor_index] * Takes (computes) cofactor-1 at location [var_to_elim_index][factor_index], and negates it. * @param index of the variable to be eliminated * @param index of the factor */ t_Expression* computeNegatedCofactorOne(int var_to_elim_index, int factor_index); /** * Computes cofactor-0 at location [var_to_elim_index][factor_index] * Takes (computes) factor at location [var_to_elim_index][factor_index], and * replaces occurences of variable at var_to_elim_index by 0. * @param index of the variable to be eliminated * @param index of the factor */ t_Expression* computeCofactorZero(int var_to_elim_index, int factor_index); /** * Computes the negation of cofactor-0 at location [var_to_elim_index][factor_index] * Takes (computes) cofactor-0 at location [var_to_elim_index][factor_index], and negates it. * @param index of the variable to be eliminated * @param index of the factor */ t_Expression* computeNegatedCofactorZero(int var_to_elim_index, int factor_index); /** * Checks if a formula is free of a variable * @param formula * @param index of variable * post-conditions: return value = true if formula is free of a variable; false otherwise * Note that the circuit pointed to by formula is not changed by this function */ bool formulaFreeOfVariable(t_Expression* formula, int var_index); /** * replaces the occurences of a variable in a formula by another formula * @param original formula * @param index of the variable to be replaced * @param formula to substitute in place of the variable * post-conditions: 1) return value = The result of replacing the occurences of the variable in OriginalFormula by FormulaToSubstitute */ t_Expression* replaceVariableByFormula(t_Expression* OriginalFormula, int var_index_to_replace, t_Expression* FormulaToSubstitute); /** * Version of replaceVariableByFormula which uses the same cache across multiple calls */ t_Expression* replaceVariableByFormula(t_Expression* OriginalFormula, int var_index_to_replace, t_Expression* FormulaToSubstitute, t_HashTable &cache); /** * replaces the occurences of a variable in a formula by constant_to_substitute * @param original formula * @param index of the variable to be replaced * @param constant to substitute in place of the variable * post-conditions: 1) return value = The result of replacing the occurences of the variable in OriginalFormula by constant_to_substitute */ t_Expression* replaceVariableByConstant(t_Expression* OriginalFormula, int var_index_to_replace, int constant_to_substitute); /** * Version of replaceVariableByConstant which uses the same cache across multiple calls */ t_Expression* replaceVariableByConstant(t_Expression* OriginalFormula, int var_index_to_replace, int constant_to_substitute, t_HashTable &cache); /* Initializes the set of skyline variables for a given variable in the trivial way * i.e. each variable before the variable at var_to_elim_index are considered as a skyline variable */ void initializeSkylineVariablesTrivially(int var_to_elim_index, set &SkylineVariables); /* Computes the set of skyline variables for a given variable */ void obtainSkylineOfVariableUsingLemmas(int var_to_elim_index, set &SkylineVariables); /* Computes the set of skyline variables for all the variables to be eliminated using dynamic programming NB: Do not use this function!!Does not compute skyline correctly in all the cases */ void obtainSkylineUsingLemmas(); /* Computes the support of a formula */ void computeSupport(t_Expression* formula, set &support); /* Clears the variable-specific data-structures */ void clearVariableSpecificDataStructures(); /** * Initializes the fields of Skolem class and * Decides the order in which variables are to be eliminated * when disable_factorization=true * @param factors * @param variables to be eliminated */ void initializeMonolithicSkolemFunctionGenerator(set &Factors, list &VariablesToEliminate); /** * The monolithic skolem function generator * @param factors * @param variables to be eliminated */ void monolithicSkolemFunctionGenerator(set &Factors, list &VariablesToEliminate); /* performs reverse-substitution of skolem functions after their generation to make them order-independent */ void performReverseSubstitutionOfSkolemFunctions(); /** * Computes alpha combined \vee gamma combined for a given variable * @param index of the variable to be eliminated */ t_Expression* computeAlphaCombinedOrGammaCombined(int var_to_elim_index); /* returns size of formula (dynamic pgming enabled) */ int computeSize(t_Expression* formula); /* version of findFactorsWithVariable which takes var_to_elim and factors_with_var_to_elim as parameters */ void findFactorsWithVariable(string &var_to_elim, set &factors_with_var_to_elim); /* version of formulaFreeOfVariable which takes var_to_elim string as parameter */ bool formulaFreeOfVariable(t_Expression* formula, string &var_string); /* function to choose the next variable to be eliminated in the least-cost-first strategy */ void getNextVariableToEliminate(string &var_to_elim_selected, unsigned long long int &var_to_elim_selected_cost, int var_to_elim_index_of_last_ordered_variable); /* function to compute the skyline in the least-cost-first strategy */ set computeSkylineInLeastCostFirst(string &var_to_elim, bool upate_eqclasses); /* function to compute the strongly-connected-components of factor-graph */ void findStronglyConnectedComponentsInFactorGraph(); /* function to merge the equivalence classes in the least-cost-first strategy */ void mergeEquivalenceClasses(set &Neighbours, set &merged_equivalence_class, int &location_of_merged_equivalence_class); /* function to merge the equivalence classes while finding the strongly-connected-components of factor-graph */ void mergeStronglyConnectedComponents(set &Neighbours, set &merged_scc, int &location_of_merged_scc); /* function to check if the \delta-combined of var_to_elim will be needed by the proceeding variables in the least-cost-first strategy */ bool checkIfDeltaIsNeeded(string &var_to_elim); /* function to update the top-variables of factors in the least-cost-first strategy */ void updateTopVariablesOfFactors(string &var_to_elim); /* function to display the relevant data-structures in the least-cost-first strategy */ void showDataStructuresForLeastCostOrdering(); /* Clears all the data-structures */ void clearAllDataStructures(); /* function to compute the correction part */ t_Expression* computeCorrectionPart(int var_to_elim_index); /* function to print the factor graph */ void printFactorGraph(set &Final_VariablesToEliminate_Set); /* function to print the factor graph as .dat file */ void printFactorGraphAsData(set &Final_VariablesToEliminate_Set); /* Version of monolithic skolem function generator's initializer with scope reduction */ void initializeMonolithicSkolemFunctionGeneratorWithScopeReduction(set &Factors, list &VariablesToEliminate); /* Version of monolithic skolem function generator with scope reduction */ void monolithicSkolemFunctionGeneratorWithScopeReduction(set &Factors, list &VariablesToEliminate); /** * Updates the factor matrix after skolem function of a variable is computed * using the global skolem functions * @param index of the variable whose skolem function is just computed */ void updateFactorsUsingGlobalSkolemFunction(int var_to_elim_index, t_Expression* skolem_function); /** * Computes the set of factors with the given variable as the top-variable * @param index of the variable to be eliminated */ void findTopFactorsWithVariable(int var_to_elim_index); /** * Version of findTopFactorsWithVariable which takes var_to_elim and factors_with_var_to_elim as parameters */ void findTopFactorsWithVariable(string &var_to_elim, set &factors_with_var_to_elim); /* Variant of computeDeltaCombined which computes delta-combined as factors implicitly conjoined */ void computeDeltaCombined(int var_to_elim_index, t_Expression* local_skolem_function, map &factor_wise_delta_combined); /* Variant of computeDeltaCombinedWithSkolemFunctionsSubstituted which internally keeps delta-combined as factors implicitly conjoined */ t_Expression* computeDeltaCombinedWithSkolemFunctionsSubstitutedKeepingFactorsIndividual(int delta_combined_index, int subst_index); /* function to find the size of delta_combined represented as factors implicitly conjoined */ int computeCostOfFactorWiseDeltaCombined(map& factor_wise_delta_combined); /* functions for skolem function generation along with quantifier elimination */ t_Expression* computeSkolemFunctionUsingBadSet(int var_to_elim_index, t_Expression* &cofactor_one_of_bad_set); void updateBadSet(int var_to_elim_index, t_Expression* cofactor_one_of_bad_set); void updateFactorsWithoutComposition(int var_to_elim_index); /* functions for skolem function generation along with quantifier elimination when quantifier eliminated result is added as a factor in the factor-graph */ void updateFactorsUsingQuantifierEliminatedResult(int var_to_elim_index, t_Expression* quantifier_eliminated_result); t_Expression* computeQuantifierEliminatedResultUsingCofactors(int var_to_elim_index); }; #endif /* SKOLEM_HPP */