/* * File: AIGBasedSkolem.hpp * Author: Ajith John * * Created on 15 April, 2014 */ #ifndef AIGBASEDSKOLEM_HPP #define AIGBASEDSKOLEM_HPP #include "helper.hpp" #include "ExpressionManager.h" #include "HashTable_WithStandardKeys.h" #include "LogManager.h" #include #include #include #include #include #include using namespace std; class AIGBasedSkolem { public: // pointer to aig manager Aig_Man_t* pub_aig_manager; 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 factors map FactorMatrix; // factor index ---> factor // matrix storing the skolem functions map SkolemFunctions; // var to elim index ---> skolem function // matrix storing the alpha-combined's map AlphaCombineds; // var to elim index ---> alpha combined // matrix storing the gamma-combined's map GammaCombineds; // var to elim index ---> gamma combined // Following are used when CEGAR is enabled map BadSets; // var to elim index ---> bad set vector< vector > FixedCNF; // The fixed part of the CNF to be given to the SAT-solver vector< vector > CNFForRenamedConjunctionOfFactors; // CNF for renamed conjunction of factors vector top_labels_of_skolem_functions; // top labels of cnfs of skolem functions map Connections; // subst_index + variable_index ---> dag for connection map top_labels_of_connections; // top labels of cnfs of connections map > end_locations_of_connections_sensitive_to_skolem_function; // variable index --> end locations of connections sensitive to change in skolem function for variable index map > start_locations_of_connections_skolem_function_is_sensitive_to; // variable index --> start locations of connections that the skolem function for variable index is sensitive to map > refinement_hints; // the final set of refinement hints // VARIABLE-SPECIFIC MATRICES AND SETS // THESE ARE CLEANED AFTER FINDING SKOLEM-FUNCTION FOR THE VARIABLE set FactorsWithVariable; // Matrices storing alpha, beta, gamma, delta, and cofactors // Note that the negations of cofactors are not required as the // AIG for negation is obtained by just flipping the pointer map CofactorOneMatrix; // factor index ---> co-factor 1 map CofactorZeroMatrix; // factor index ---> co-factor 0 map AlphaMatrix; // factor index ---> alpha map BetaMatrix; // factor index ---> beta map GammaMatrix; // factor index ---> gamma map DeltaMatrix; // factor index ---> delta // 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 AIGBasedSkolem(Aig_Man_t* aig_manager); ~AIGBasedSkolem(); static AIGBasedSkolem* AIGBasedSkolem_instance; static AIGBasedSkolem* getInstance(Aig_Man_t* aig_manager); /** * The factorized skolem function generator * @param factors * @param variables to be eliminated */ void factorizedSkolemFunctionGenerator(set &Factors, list &VariablesToEliminate); /** * Initializes the fields of AIGBasedSkolem class and * Decides the order in which variables are to be eliminated * @param factors * @param variables to be eliminated */ void initializeFactorizedSkolemFunctionGenerator(set &Factors, list &VariablesToEliminate); /** * 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 alpha at location [var_to_elim_index][factor_index] * @param index of the variable to be eliminated * @param index of the factor */ Aig_Obj_t* 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 */ Aig_Obj_t* 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 */ Aig_Obj_t* 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 */ Aig_Obj_t* 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 */ Aig_Obj_t* 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 */ Aig_Obj_t* 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 */ Aig_Obj_t* 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 */ Aig_Obj_t* 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(Aig_Obj_t* 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 */ Aig_Obj_t* replaceVariableByFormula(Aig_Obj_t* OriginalFormula, int var_index_to_replace, Aig_Obj_t* FormulaToSubstitute); /** * replaces the occurences of each variable in map by corresponding formula * @param original formula * @param replacement map * post-conditions: 1) return value = The result of replacing the occurences of the variables in OriginalFormula as per replacement_map */ Aig_Obj_t* replaceVariablesByFormulas(Aig_Obj_t* OriginalFormula, map &replacement_map); /** * 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 */ Aig_Obj_t* replaceVariableByConstant(Aig_Obj_t* OriginalFormula, int var_index_to_replace, int constant_to_substitute); /** * replaces the occurences of each variable in map by corresponding constant * @param original formula * @param replacement map * post-conditions: 1) return value = The result of replacing the occurences of the variables in OriginalFormula as per replacement_map */ Aig_Obj_t* replaceVariablesByConstants(Aig_Obj_t* OriginalFormula, map &replacement_map); /* Clears the variable-specific data-structures */ void clearVariableSpecificDataStructures(); /* 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 */ Aig_Obj_t* computeAlphaCombinedOrGammaCombined(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); /* functions for skolem function generation along with quantifier elimination */ Aig_Obj_t* computeSkolemFunctionUsingBadSet(int var_to_elim_index, Aig_Obj_t* &cofactor_one_of_bad_set); void updateBadSet(int var_to_elim_index, Aig_Obj_t* cofactor_one_of_bad_set); void updateFactorsWithoutComposition(int var_to_elim_index); void updateFactorsUsingQuantifierEliminatedResult(int var_to_elim_index, Aig_Obj_t* quantifier_eliminated_result); Aig_Obj_t* computeQuantifierEliminatedResultUsingCofactors(int var_to_elim_index); /* functions for skolem function generation using scope reduced Jiang */ void monolithicSkolemFunctionGeneratorWithScopeReduction(set &Factors, list &VariablesToEliminate); void updateFactorsUsingGlobalSkolemFunction(int var_to_elim_index, Aig_Obj_t* skolem_function); /* functions for generic skolem function parameters */ void computeGenericSkolemFunctionParametersInBadBased(int var_to_elim_index, Aig_Obj_t* &alpha_combined_in_bad_based); void computeGenericSkolemFunctionParametersInBddBased(int var_to_elim_index, Aig_Obj_t* &cofactor_one_in_bdd_based, Aig_Obj_t* &cofactor_zero_in_bdd_based); void updateBadSetWithGivenAlphaCombined(int var_to_elim_index, Aig_Obj_t* alpha_combined_in_bad_based); /* Functions for CEGAR */ /* function for initial abstract skolem function generation (used when enable_cegar is true) */ Aig_Obj_t* computeAbstractSkolemFunction(int var_to_elim_index); /* function for initial abstract bad set generation (used when enable_cegar is true) */ void computeAbstractBadSet(int var_to_elim_index); /* function to check if the present set of Skolem functions are exact */ bool checkIfSkolemFunctionsAreExact(map &Model_of_ExactnessCheck, map &Refinement_Hint_To_Eliminate_This_CEX); /* function to refine the present set of Skolem functions */ void refineSkolemFunctions(map &Model_of_ExactnessCheck, map &Refinement_Hint_To_Eliminate_This_CEX); bool checkIfMismatchIsGenuine(int mismatch_location, vector &XNewValues, vector &XNewLabels, map &YLabelsToYValuesMap); void findBadLocationsToRefineMismatchAtLocation(int mismatch_location, vector &BadLocations, vector & bad_locations_to_refine_mismatch_at_mismatch_location); /* function to initialize the CEGAR loop */ void initializeCEGAR(); /* function to compute alpha-combined */ Aig_Obj_t* computeAlphaCombined(int var_to_elim_index); /* function to compute alpha-combined that is sufficient for abstract skolem function generation */ Aig_Obj_t* computeAlphaCombinedForComputingAbstractSkolemFunction(int var_to_elim_index); /* function to compute gamma-combined */ Aig_Obj_t* computeGammaCombined(int var_to_elim_index); /* function to substitute connections by their dags where the connections are binary*/ void replaceConnectionsByFormulas_In_Two_Point_Connections(); /* For cegar using ABC's sat-solving routines */ void initializeCEGAR_using_ABC(); /* Functions for implementation of CEGAR scheme using replacement-based scheme */ void refineSkolemFunctions_using_ABC(map &Model_of_ExactnessCheck, map &Refinement_Hint_To_Eliminate_This_CEX); bool checkIfMismatchIsGenuine_using_ABC(int mismatch_location, vector &XNewValues, map &YValues); Aig_Obj_t* obtainFormulaWithoutConnections(Aig_Obj_t* formula); void refineSkolemFunctions_using_ABC_EvaluationBasedStrategy(map &Model_of_ExactnessCheck, map &Refinement_Hint_To_Eliminate_This_CEX); void reevaluateXValues(vector &XValues, map &YValues, int asserted_location, int asserted_value); bool obtainValueOfCi(string variable, map &variable_to_value_map); bool evaluateFormulaOfCi(Aig_Obj_t* formula, map &variable_to_value_map); bool evaluateFormulaOfCi_DFS(Aig_Obj_t* formula, map &variable_to_value_map); void evaluateBadValues(vector &XValues, map &YValues, int var_to_elim_index, vector &BadValues); void analyzeReasonBehindUnderApproximation(int index_of_variable, vector &XValues, vector &XNewValues, map &YValues); Aig_Obj_t* computeBetaCombinedForDebugging(int var_to_elim_index); Aig_Obj_t* computeDisjunctionOfGammas(int var_to_elim_index); Aig_Obj_t* computeDisjunctionOfDeltas(int var_to_elim_index); void reevaluateXValues_using_Solver(vector &XValues, map &YValues, int asserted_location, int asserted_value); void evaluateBadValues_using_Solver(vector &XValues, map &YValues, int index_of_variable, vector &BadValues); void findSkolemFunctionsToRecompute(set &skolem_functions_changed, set &skolem_functions_to_recompute); void findSensitiveSkolemFunctions(set &skolem_functions_changed, set &skolem_functions_sensitive); Aig_Obj_t* computeQuantifierEliminatedResultUsingSkolemFunction(int var_to_elim_index, Aig_Obj_t* skolem_function); /* Functions for Interpolant-based Jiang */ Aig_Obj_t* computeBetaCombined(int var_to_elim_index); Aig_Obj_t* computeSkolemFunctionAsInterpolant(int var_to_elim_index); /* Functions for implementation of CEGAR scheme using multi-point connections based scheme */ bool checkIfSkolemFunctionsAreExact_using_ABC_with_Cyclic_Two_Point_Connections(map &Model_of_ExactnessCheck, map &Refinement_Hint_To_Eliminate_This_CEX); bool checkIfSkolemFunctionsAreExact_using_ABC_with_Composes(map &Model_of_ExactnessCheck, map &Refinement_Hint_To_Eliminate_This_CEX, list &VariablesToEliminate); bool checkIfSkolemFunctionsAreExact_using_ABC_with_Multi_Point_Connections(map &Model_of_ExactnessCheck, map &Refinement_Hint_To_Eliminate_This_CEX, list &VariablesToEliminate); bool checkIfSkolemFunctionsAreExact_using_Value_Based_Scheme(map &Model_of_ExactnessCheck, map &Refinement_Hint_To_Eliminate_This_CEX, list &VariablesToEliminate); void findConnectionsToUpdate(set &connections_to_update, int variable_index, int bad_index); void obtainReplacementMapForConnection(string connection, map &replacement_map_for_connection); void findPointsInConnection(string connection, vector &points_in_connection); void findStartIndexAndEndIndexOfConnection(string connection, int &start_index_of_connection, int &end_index_of_connection); Aig_Obj_t* replaceVariablesByFormulas(Aig_Obj_t* OriginalFormula, map &replacement_map); Aig_Obj_t* replaceVariableByFormula(Aig_Obj_t* OriginalFormula, string var_to_replace, Aig_Obj_t* FormulaToSubstitute); string mergeConnections(string start_connection, string end_connection); void replaceConnectionsByFormulas_In_Multi_Point_Connections(); void sortConnectionsBasedOnStartingLocation(set &unsorted_connections_set, list &sorted_connections_list); /* Functions for supporting incremental sat-solving in multi-point connections based scheme */ string obtainZVariableString(int var_to_elim_index, int z_i_count); string obtainRVariableString(int bad_index, int variable_index); string obtainTVariableString(int connection_i_j_count, string connection); string obtainIVariableString(int connection_i_j_count, string connection); Aig_Obj_t* obtainObjectOfConnectionString(string connection_string); Aig_Obj_t* obtainObjectOfTemporaryVariableForIncrementalSolving(string temporary_variable_string); Aig_Obj_t* obtainExistingObjectOfTemporaryVariableForIncrementalSolving(string temporary_variable_string); void obtainAssumptionsInExactnessCheck(vector &positive_assumptions_in_exactness_check, vector &negative_assumptions_in_exactness_check, bool apply_uniformity, bool enable_uniformity_condition); void removeTemporaryVariablesFromModel(map &Model_of_ExactnessCheck); /* Functions for value-based scheme */ Aig_Obj_t* createAssignment(map &x_replacement_map); void analyzeReasonBehindMismatch(int bad_index, int variable_index, map &bad_to_var_replacement_map, map &below_var_replacement_map); Aig_Obj_t* createUnsatCoreBasedAssignment(map &x_replacement_map, int one_variable_index, int &number_of_literals_dropped_by_unsat_core); /* Functions for uniform witness generation */ Aig_Obj_t* createUniformityCondition(); string obtainPVariableString(int p_count); string obtainQVariableString(int p_count); Aig_Obj_t* createUniformityConditionDag(); /* Functions for graph decomposition */ void graphDecomposition(set &transition_function_factors, set &transition_function_parts, list &VariablesToEliminate, map &Output_Object_to_RHS_of_Factors, map &Output_Object_to_RHS_of_PrimaryOutputs, ABC* abcObj, Abc_Frame_t* abcFrame); void obtainSkolemFunctionsInGraphDecomposition(set &uncovered_edges_factors, list &VariablesToEliminate, map &variable_to_skolem_function_map, int iterations_of_loop); void clearAllDataStructures(); Aig_Obj_t* generateComponent(Aig_Obj_t* transition_function, map &variable_to_skolem_function_map); Aig_Obj_t* generateCoveredEdges(set &transition_function_parts, map &variable_to_skolem_function_map); /* Functions for CEGAR with generic form of Skolem functions */ Aig_Obj_t* computeInitialSkolemFunctionsAndCannotBeSets(int var_to_elim_index); void allocateStringAndObjectToCannotBeDag(int kind_of_cannot_be, Aig_Obj_t* cannot_be_dag, string &cannot_be_string, Aig_Obj_t* &cannot_be_object); bool checkIfSkolemFunctionsAreExact_using_Generic_Skolem_Functions(map &Model_of_ExactnessCheck, map &Refinement_Hint_Of_CannotBe_One_To_Eliminate_This_CEX, map &Refinement_Hint_Of_CannotBe_Zero_To_Eliminate_This_CEX, list &VariablesToEliminate); void obtainAssumptionsInExactnessCheck_using_Generic_Skolem_Functions(vector &positive_assumptions_in_exactness_check); void refineSkolemFunctions_using_Generic_Skolem_Functions(map &Model_of_ExactnessCheck, map &Refinement_Hint_Of_CannotBe_One_To_Eliminate_This_CEX, map &Refinement_Hint_Of_CannotBe_Zero_To_Eliminate_This_CEX); Aig_Obj_t* obtain_initial_mu(int origin, map &cannot_be_object_to_value_map, int &number_of_cannot_be_one_elements, int &number_of_cannot_be_zero_elements, int &size_of_initial_mu); Aig_Obj_t* obtain_disjunction_of_true_cannot_be_zero_dags(int destination, map &cannot_be_object_to_value_map, Aig_Obj_t* cofactor_of_mu, int &number_of_cannot_be_zero_elements_that_are_true_selected); Aig_Obj_t* obtain_disjunction_of_true_cannot_be_one_dags(int destination, map &cannot_be_object_to_value_map, Aig_Obj_t* cofactor_of_mu, int &number_of_cannot_be_one_elements_that_are_true_selected); void show_present_refinement_hint(map &Refinement_Hint_Of_CannotBe_One_To_Eliminate_This_CEX, map &Refinement_Hint_Of_CannotBe_Zero_To_Eliminate_This_CEX); /* Functions for benchmark generation */ void benchmarkGeneration(set &transition_function_factors, map &output_string_to_transition_function_parts, list &VariablesToEliminate); /* Functions for CEGAR with mu-based scheme with optimizations */ Aig_Obj_t* computeInitialSkolemFunctionsBadSetsAndCannotBeSets(int var_to_elim_index); bool checkIfSkolemFunctionAtGivenIndexIsExact_using_Mu_Based_Scheme_With_Optimizations(int correction_index, map &Model_of_ExactnessCheck, map &Refinement_Hint_Of_CannotBe_One_To_Eliminate_This_CEX, map &Refinement_Hint_Of_CannotBe_Zero_To_Eliminate_This_CEX, list &VariablesToEliminate); void refineSkolemFunctions_using_Mu_Based_Scheme_With_Optimizations(int correction_index, map &Model_of_ExactnessCheck, map &Refinement_Hint_Of_CannotBe_One_To_Eliminate_This_CEX, map &Refinement_Hint_Of_CannotBe_Zero_To_Eliminate_This_CEX); bool evaluateMu(Aig_Obj_t* mu, map &XValues, map &YValues, int destination, int value_at_destination); Aig_Obj_t* createSkolemFunction_In_Mu_Based_Scheme_With_Optimizations(int destination); Aig_Obj_t* optimizeCannotBeOneDagThroughInterpolation(Aig_Obj_t* original_cannot_be_one_dag, int destination); Aig_Obj_t* createDontCarePart_In_Mu_Based_Scheme_With_Optimizations(int destination); string obtainDVariableString(int var_to_elim_index, int d_i_count); string obtainSVariableString(int var_to_elim_index, int s_i_count); void obtainAssumptionsInExactnessCheck_using_Generic_Skolem_Functions_And_Dontcare_Optimization(vector &positive_assumptions_in_exactness_check, vector &negative_assumptions_in_exactness_check); Aig_Obj_t* obtainExtraCannotBeOneDagAtDestination(map &XValues, map &YValues, int destination, int &number_of_variables_dropped_in_generalization); void obtainGeneralizedModelByIncrementalSolvingInObtainingExtraCannotBeOneDagAtDestination(map &XValues, map &YValues, int destination, set &variables_avoided); /* Functions for enabling incremental solving in CEGAR with mu-based scheme with optimizations */ bool checkIfSkolemFunctionAtGivenIndexIsExact_using_Mu_Based_Scheme_With_Optimizations_With_Incremental_Solving(int correction_index, map &Model_of_ExactnessCheck, map &Refinement_Hint_Of_CannotBe_One_To_Eliminate_This_CEX, map &Refinement_Hint_Of_CannotBe_Zero_To_Eliminate_This_CEX, list &VariablesToEliminate); void obtainAssumptionsInExactnessCheck_using_Generic_Skolem_Functions_With_Incremental_Solving(int correction_index, vector &positive_assumptions_in_exactness_check, vector &negative_assumptions_in_exactness_check); string obtainYVariableString(int var_to_elim_index, int y_i_count); void skolemFunctionGeneratorUsingBloqqer(set &Factors_new, list &VariablesToEliminate); //New functions for comparison with Jiang's Aig_Obj_t* computeCofactorOneOrNegCofactorZero(int var_to_elim_index); // New functions for unified CEGAR bool checkIfSkolemFunctionAtGivenIndexIsExact_using_Mu_Based_Scheme_With_Optimizations_With_Unified_Code_And_Incremental_Solving(int correction_index, map &Model_of_ExactnessCheck, map &Refinement_Hint_Of_CannotBe_One_To_Eliminate_This_CEX, map &Refinement_Hint_Of_CannotBe_Zero_To_Eliminate_This_CEX, list &VariablesToEliminate); void obtainAssumptionsInExactnessCheck_using_Generic_Skolem_Functions_With_Unified_Code_And_Incremental_Solving(int correction_index, vector &positive_assumptions_in_exactness_check, vector &negative_assumptions_in_exactness_check); /* Functions for supporting game benchmarks */ void generateSkolemFunctionsForGameBenchmarks(set &original_factors, vector< list > &VariablesToEliminateForGameBenchmarks, char TypeOfInnerQuantifier); void obtainSkolemFunctionsInGameBenchmarks(set &Factors, list &VariablesToEliminate, map &variable_to_skolem_function_map, int quantifier_block, char TypeOfQuantifier); void recreateCiMaps(list &VariablesToEliminate); /* Functions to generate satisfiable benchmarks */ void satisfiableBenchmarkGeneration(set &transition_function_factors, map &output_string_to_transition_function_parts, list &VariablesToEliminate); }; #endif /* AIGBASEDSKOLEM_HPP */