/******************************************************************** Developers: Ajith John, Supratik Chakraborty Last updated: July 24, 2013 *********************************************************************/ /********************************************************************* Project.cpp and Project.h contains the code for the algorithm Project described in the paper "Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors" in TACAS 2013. *********************************************************************/ #include #include "Project.h" using namespace std; /**********************************************************************/ /* Constructor, destructor */ /**********************************************************************/ t_Project::t_Project(t_HashTable &VariableList, t_HashTable &WidthTable, bool use_bvlibrary_for_layer2_computations, t_ExpressionManager* em, BVManager* bvm) { if (t_project_instance != NULL) { cerr << "Error in t_Project::t_Project: Attempt to create multiple copies of t_Project" << endl; cerr << "There should be only one copy of t_Project" << endl; assert(0); } pvt_VariableList = VariableList; pvt_WidthTable = WidthTable; pvt_use_bvlibrary_for_layer2_computations = use_bvlibrary_for_layer2_computations; pvt_em = em; pvt_bvm = bvm; t_Logger* logManager = t_Logger::getInstance(); pvt_logFile = new ofstream(); pvt_logFile->open("project.log"); logManager->LOG("project started", pvt_logFile, c_DebugLevelVerbosity); } t_Project::~t_Project() { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("project is deleted", pvt_logFile, c_DebugLevelVerbosity); pvt_logFile->close(); } t_Project* t_Project::t_project_instance = NULL; t_Project* t_Project::getInstance(t_HashTable &VariableList, t_HashTable &WidthTable, bool use_bvlibrary_for_layer2_computations, t_ExpressionManager* em, BVManager* bvm) { if(t_project_instance == NULL) { try { t_project_instance = new t_Project(VariableList, WidthTable, use_bvlibrary_for_layer2_computations, em, bvm); } catch(bad_alloc&) { cerr << "Memory allocation failure in t_Project::getInstance" << endl; assert(0); } } return t_project_instance; } /**********************************************************************/ /* Part 1: Functions related to Kappa finding */ /**********************************************************************/ // Given a "kand" node, this function finds the "eqz" node with the minimum kappa value in pivotEqzNode, // the kappa value in minKappa, and the odd part in oddPartOfMinKappa. // Returns false in case of errors; true otherwise. // Note that "eqz" node is of the form c_1.x_1 + ... +c_n.x_n = 0. Let x_i be the variable. // Let c_i be 2^{k_i}.e_i. Hence kappa = k_i and odd part = e_i. // If the equations in "kand" node are free of the variable, then minKappa = UINT_MAX. // In this case, pivotEqzNode and OddPart are not changed by the function. bool t_Project::findEquationWithMinimumKappaValue(t_Expression* kandNode, const string &variable, t_Expression* &pivotEqzNode, unsigned int &minKappa, bvatom &oddPartOfMinKappa) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::findEquationWithMinimumKappaValue", pvt_logFile, c_RunLevelVerbosity); return false; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findEquationWithMinimumKappaValue", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(kandNode); minKappa = UINT_MAX; for(int i = 0; i < Children.size(); i++) // take each "eqz" child of "kand" node { t_Expression* Child = Children[i]; assert(Child != NULL); if("eqz" != pvt_em->getLabelOfExpression(Child)) // recall that the children are ordered - "eqz" children appear first { break; } unsigned int Kappa; bvatom OddPart; // find the kappa value of Child bool KappaFound = findKappaValueAndOddPartOfEqz(Child, variable, Kappa, OddPart); if(!KappaFound)// error in findKappaValueAndOddPartOfEqz; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::findEquationWithMinimumKappaValue", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa < minKappa) { minKappa = Kappa; pivotEqzNode = Child; oddPartOfMinKappa = OddPart; } }// for ends here return true; }// else of if (!kandNode) ends here }// function ends here // Given an "eqz" node, this function finds the kappa value in Kappa, and the odd part in OddPart. // Returns false in case of errors; true otherwise // Note that "eqz" node is of the form c_1.x_1 + ... +c_n.x_n = 0. Let x_i be the variable. // Let c_i be 2^{k_i}.e_i. Hence Kappa = k_i and OddPart = e_i // If the "eqz" node is free of the variable, then Kappa = UINT_MAX and OddPart is not changed by the function // Important: Use this function only if both Kappa value and OddPart are required. // If only the Kappa value is required, use findKappaValueOfEqz. bool t_Project::findKappaValueAndOddPartOfEqz(t_Expression* eqzNode, const string &variable, unsigned int &Kappa, bvatom &OddPart) { if(eqzNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! eqzNode is NULL in function t_Project::findKappaValueAndOddPartOfEqz", pvt_logFile, c_RunLevelVerbosity); return false; } else if("eqz" != pvt_em->getLabelOfExpression(eqzNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findKappaValueAndOddPartOfEqz", pvt_logFile, c_RunLevelVerbosity); return false; } else { t_Expression* kaddNode = getIthChild(eqzNode, 0, pvt_em); // get the "kadd" node assert(kaddNode != NULL); // find the monom in the "kadd" node with the variable t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, pvt_em, pvt_VariableList); if(!MonomFound)// error in findMonomOfKaddNodeWithGivenVariable; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::findKappaValueAndOddPartOfEqz", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariable == NULL)// there's no monom in kadd node with the variable { Kappa = UINT_MAX; return true; } else { // find the kappa value and odd part of the variable in the monom bool KappaFound = findKappaValueAndOddPartOfMonom(MonomWithVariable, variable, Kappa, OddPart); if(!KappaFound)// error in findKappaValueAndOddPartOfMonom; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::findKappaValueAndOddPartOfEqz", pvt_logFile, c_RunLevelVerbosity); return false; } else { //Kappa and OddPart are found by findKappaValueAndOddPartOfMonom return true; } }//else ends here }//else ends here }// function ends here // Given an "eqz" node, this function finds the kappa value in Kappa. // Returns false in case of errors; true otherwise // Note that "eqz" node is of the form c_1.x_1 + ... +c_n.x_n = 0. Let x_i be the variable. // Let c_i be 2^{k_i}.e_i. Hence Kappa = k_i. // If the "eqz" node is free of the variable, then Kappa = UINT_MAX. // Important: Use this function if only the Kappa value is required. // If both the Kappa value and OddPart are required, use findKappaValueAndOddPartOfEqz. bool t_Project::findKappaValueOfEqz(t_Expression* eqzNode, const string &variable, unsigned int &Kappa) { if(eqzNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! eqzNode is NULL in function t_Project::findKappaValueOfEqz", pvt_logFile, c_RunLevelVerbosity); return false; } else if("eqz" != pvt_em->getLabelOfExpression(eqzNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findKappaValueOfEqz", pvt_logFile, c_RunLevelVerbosity); return false; } else { t_Expression* kaddNode = getIthChild(eqzNode, 0, pvt_em); // get the "kadd" node assert(kaddNode != NULL); // find the monom in the "kadd" node with the variable t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, pvt_em, pvt_VariableList); if(!MonomFound)// error in findMonomOfKaddNodeWithGivenVariable; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::findKappaValueOfEqz", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariable == NULL)// there's no monom in kadd node with the variable { Kappa = UINT_MAX; return true; } else { // find the kappa value of the variable in the monom bool KappaFound = findKappaValueOfMonom(MonomWithVariable, variable, Kappa); if(!KappaFound)// error in findKappaValueOfMonom; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::findKappaValueOfEqz", pvt_logFile, c_RunLevelVerbosity); return false; } else { //Kappa is found by findKappaValueOfMonom return true; } }//else ends here }//else ends here }// function ends here // Given an "diseqz" node, this function finds the kappa value in Kappa. // Returns false in case of errors; true otherwise // Note that "diseqz" node is of the form c_1.x_1 + ... +c_n.x_n != 0. Let x_i be the variable. // Let c_i be 2^{k_i}.e_i. Hence Kappa = k_i. // If the "diseqz" node is free of the variable, then Kappa = UINT_MAX. bool t_Project::findKappaValueOfDiseqz(t_Expression* DiseqzNode, const string &variable, unsigned int &Kappa) { if(DiseqzNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! DiseqzNode is NULL in function t_Project::findKappaValueOfDiseqz", pvt_logFile, c_RunLevelVerbosity); return false; } else if("diseqz" != pvt_em->getLabelOfExpression(DiseqzNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findKappaValueOfDiseqz", pvt_logFile, c_RunLevelVerbosity); return false; } else { t_Expression* kaddNode = getIthChild(DiseqzNode, 0, pvt_em); // get the "kadd" node assert(kaddNode != NULL); // find the monom in the "kadd" node with the variable t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, pvt_em, pvt_VariableList); if(!MonomFound)// error in findMonomOfKaddNodeWithGivenVariable; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::findKappaValueOfDiseqz", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariable == NULL)// there's no monom in kadd node with the variable { Kappa = UINT_MAX; return true; } else { // find the kappa value of the variable in the monom bool KappaFound = findKappaValueOfMonom(MonomWithVariable, variable, Kappa); if(!KappaFound)// error in findKappaValueOfMonom; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::findKappaValueOfDiseqz", pvt_logFile, c_RunLevelVerbosity); return false; } else { //Kappa is found by findKappaValueOfMonom return true; } }//else ends here }//else ends here }// function ends here // Given a "kadd" node, this function finds the kappa value in Kappa. // Returns false in case of errors; true otherwise // Note that "kadd" node is of the form c_1.x_1 + ... +c_n.x_n. Let x_i be the variable. // Let c_i be 2^{k_i}.e_i. Hence Kappa = k_i. // If the "kadd" node is free of the variable, then Kappa = UINT_MAX. bool t_Project::findKappaValueOfKadd(t_Expression* kaddNode, const string &variable, unsigned int &Kappa) { if(kaddNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode is NULL in function t_Project::findKappaValueOfKadd", pvt_logFile, c_RunLevelVerbosity); return false; } else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findKappaValueOfKadd", pvt_logFile, c_RunLevelVerbosity); return false; } else { // find the monom in the "kadd" node with the variable t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, pvt_em, pvt_VariableList); if(!MonomFound)// error in findMonomOfKaddNodeWithGivenVariable; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::findKappaValueOfKadd", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariable == NULL)// there's no monom in kadd node with the variable { Kappa = UINT_MAX; return true; } else { // find the kappa value of the variable in the monom bool KappaFound = findKappaValueOfMonom(MonomWithVariable, variable, Kappa); if(!KappaFound)// error in findKappaValueOfMonom; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::findKappaValueOfKadd", pvt_logFile, c_RunLevelVerbosity); return false; } else { //Kappa is found by findKappaValueOfMonom return true; } }//else ends here }//else ends here }// function ends here // Given an "leq" node, this function finds the kappa value in Kappa. // Returns false in case of errors; true otherwise // Note that "leq" node is of the form c_1.x_1 + ... +c_n.x_n <= d_1.x_1 + ... +d_n.x_n. // Let x_i be the variable. Let c_i be 2^{k_i}.e_i. Let d_i be 2^{k'_i}.e'_i. // Kappa = min(k_i, k'_i). // If the "leq" node is free of the variable, then Kappa = UINT_MAX. bool t_Project::findKappaValueOfLeq(t_Expression* LeqNode, const string &variable, unsigned int &Kappa) { if(LeqNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! LeqNode is NULL in function t_Project::findKappaValueOfLeq", pvt_logFile, c_RunLevelVerbosity); return false; } else if("leq" != pvt_em->getLabelOfExpression(LeqNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findKappaValueOfLeq", pvt_logFile, c_RunLevelVerbosity); return false; } else { t_Expression* LHSNode = getIthChild(LeqNode, 0, pvt_em); // get the LHS node t_Expression* RHSNode = getIthChild(LeqNode, 1, pvt_em); // get the RHS node assert(LHSNode != NULL); assert(RHSNode != NULL); unsigned int Kappa_LHS, Kappa_RHS; bool Kappa_LHS_Found = findKappaValueOfKadd(LHSNode, variable, Kappa_LHS); bool Kappa_RHS_Found = findKappaValueOfKadd(RHSNode, variable, Kappa_RHS); if(!Kappa_LHS_Found || !Kappa_RHS_Found)// Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::findKappaValueOfLeq", pvt_logFile, c_RunLevelVerbosity); return false; } else { Kappa = (Kappa_LHS < Kappa_RHS)? Kappa_LHS: Kappa_RHS; return true; } }//else ends here }// function ends here // Given a kand node and variable, // this function finds the kappa of the kand node for the variable,.i.e. // the minimum among the kappa values of the constraints in kand. // If all the constraints are free of the variable, "Kappa" is set as UINT_MAX. // Returns false in case of errors; true otherwise. bool t_Project::findKappaValueOfKandNode(t_Expression* kandNode, const string &variable, unsigned int &minKappa) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::findKappaValueOfKandNode", pvt_logFile, c_RunLevelVerbosity); return false; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findKappaValueOfKandNode", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(kandNode); minKappa = UINT_MAX; for(int i = 0; i < Children.size(); i++) // take each constraint { t_Expression* Constraint = Children[i]; // find the kappa value of the constraint bool KappaFound; unsigned int Kappa; if(Constraint == NULL) //Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Constraint is NULL in function t_Project::findKappaValueOfKandNode", pvt_logFile, c_RunLevelVerbosity); return false; } else if("eqz" == pvt_em->getLabelOfExpression(Constraint)) // equation { KappaFound = findKappaValueOfEqz(Constraint, variable, Kappa); } else if("diseqz" == pvt_em->getLabelOfExpression(Constraint)) // disequation { KappaFound = findKappaValueOfDiseqz(Constraint, variable, Kappa); } else if("leq" == pvt_em->getLabelOfExpression(Constraint)) // inequation { KappaFound = findKappaValueOfLeq(Constraint, variable, Kappa); } else // Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unknown constraint in function t_Project::findKappaValueOfKandNode", pvt_logFile, c_RunLevelVerbosity); return false; } if(!KappaFound)// error in kappa finding; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::findKappaValueOfKandNode", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa < minKappa) { minKappa = Kappa; } }// for ends here return true; }// else of else if("kand" != pvt_em->getLabelOfExpression(kandNode)) ends here }// function ends here // Given a set of constraints i.e. equations, disequations, and inequations, // this function finds in "minKappa", the minimum among the kappa values of // the constraints. If all the constraints are free of the variable, // "minKappa" is set as UINT_MAX. Returns false in case of errors; true otherwise. bool t_Project::findMinimumKappaValueAmongSetOfConstraints(const set &Constraints, const string &variable, unsigned int &minKappa) { minKappa = UINT_MAX; for(set::iterator it = Constraints.begin(); it != Constraints.end(); it++) // take each constraint { t_Expression* Constraint = *it; // find the kappa value of the constraint bool KappaFound; unsigned int Kappa; if(Constraint == NULL) //Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Constraint is NULL in function t_Project::findMinimumKappaValueAmongSetOfConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } else if("eqz" == pvt_em->getLabelOfExpression(Constraint)) // equation { KappaFound = findKappaValueOfEqz(Constraint, variable, Kappa); } else if("diseqz" == pvt_em->getLabelOfExpression(Constraint)) // disequation { KappaFound = findKappaValueOfDiseqz(Constraint, variable, Kappa); } else if("leq" == pvt_em->getLabelOfExpression(Constraint)) // inequation { KappaFound = findKappaValueOfLeq(Constraint, variable, Kappa); } else // Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unknown constraint in function t_Project::findMinimumKappaValueAmongSetOfConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } if(!KappaFound)// error in kappa finding; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::findMinimumKappaValueAmongSetOfConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa < minKappa) { minKappa = Kappa; } }// for ends here return true; }// function ends here // Given a monom, i.e. "bvmul" node, this function finds the kappa value and odd part // of the coefficient of the variable in the monom. In case the monom is free of the variable, // Kappa is set as UINT_MAX. Returns false in case of errors; true otherwise. bool t_Project::findKappaValueAndOddPartOfMonom(t_Expression* monom, const string &variable, unsigned int &Kappa, bvatom &OddPart) { if(monom == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom is NULL in function t_Project::findKappaValueAndOddPartOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else if("bvmul" != pvt_em->getLabelOfExpression(monom)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findKappaValueAndOddPartOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(monom); if(Children.size() != 2) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! number of children of bvmul node is not two in function t_Project::findKappaValueAndOddPartOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } t_Expression* ConstantNode = Children[0];// get the first child t_Expression* VariableNode = Children[1];// get the second child assert(ConstantNode != NULL); assert(VariableNode != NULL); if(!isBVConstant(ConstantNode, pvt_em)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! first child of bvmul node is not constant in function t_Project::findKappaValueAndOddPartOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else if(!isBVVariable(VariableNode, pvt_em)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! second child of bvmul node is not variable in function t_Project::findKappaValueAndOddPartOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else { string VariableOfMonom = pvt_em->getLabelOfExpression(VariableNode); if(VariableOfMonom != variable)// monom is free of variable { Kappa = UINT_MAX; return true; } else { string Coefficient = pvt_em->getLabelOfExpression(ConstantNode); // recall that Coefficient is a (zero-padded) binary string starting with "0b"; // hence the following code will suffice to create the bvatom Coefficient = Coefficient.substr(2); //we need characters from position 2 to end bvatom CoefficientOfMonom = pvt_bvm->getBVatom(Coefficient.size(), Coefficient); // find the kappa value and odd part of CoefficientOfMonom bool KappaFound = pvt_bvm->findKappaAndOddPart(CoefficientOfMonom, Kappa, OddPart); if(!KappaFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while computing kappa in function t_Project::findKappaValueAndOddPartOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else { return true; } }// else of monom is free of variable ends here }// else of else if(!isBVVariable(VariableNode, pvt_em)) ends here }// else of else if("bvmul" != pvt_em->getLabelOfExpression(monom)) ends here }//function ends here // Given a monom, i.e. "bvmul" node, this function finds the kappa value // of the coefficient of the variable in the monom. In case the monom is free of the variable, // Kappa is set as UINT_MAX. Returns false in case of errors; true otherwise. bool t_Project::findKappaValueOfMonom(t_Expression* monom, const string &variable, unsigned int &Kappa) { if(monom == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom is NULL in function t_Project::findKappaValueOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else if("bvmul" != pvt_em->getLabelOfExpression(monom)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::findKappaValueOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(monom); if(Children.size() != 2) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! number of children of bvmul node is not two in function t_Project::findKappaValueOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } t_Expression* ConstantNode = Children[0];// get the first child t_Expression* VariableNode = Children[1];// get the second child assert(ConstantNode != NULL); assert(VariableNode != NULL); if(!isBVConstant(ConstantNode, pvt_em)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! first child of bvmul node is not constant in function t_Project::findKappaValueOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else if(!isBVVariable(VariableNode, pvt_em)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! second child of bvmul node is not variable in function t_Project::findKappaValueOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else { string VariableOfMonom = pvt_em->getLabelOfExpression(VariableNode); if(VariableOfMonom != variable)// monom is free of variable { Kappa = UINT_MAX; return true; } else { string Coefficient = pvt_em->getLabelOfExpression(ConstantNode); // recall that Coefficient is a (zero-padded) binary string starting with "0b"; // hence the following code will suffice to create the bvatom Coefficient = Coefficient.substr(2); //we need characters from position 2 to end bvatom CoefficientOfMonom = pvt_bvm->getBVatom(Coefficient.size(), Coefficient); // find the kappa value of CoefficientOfMonom bool KappaFound = pvt_bvm->findKappa(CoefficientOfMonom, Kappa); if(!KappaFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while computing kappa in function t_Project::findKappaValueOfMonom", pvt_logFile, c_RunLevelVerbosity); return false; } else { return true; } }// else of monom is free of variable ends here }// else of else if(!isBVVariable(VariableNode, pvt_em)) ends here }// else of else if("bvmul" != pvt_em->getLabelOfExpression(monom)) ends here }//function ends here /**********************************************************************/ /* Part 2: Functions for Layer1 */ /**********************************************************************/ // Given an "eqz" node c_0 + c_1.x_1 + ... +c_n.x_n = 0, pivot variable x_i, let c_i be 2^{k_i}.e_i. // Hence "eqz" node is c_0 + c_1.x_1 + ... 2^{k_i}.e_i.x_i+ ... +c_n.x_n = 0. Hence "eqz" node // can be expressed as 2^{k_i}.x_i = MI(e_i).(-c_0) + MI(e_i).(-c_1).x_1 + ... + MI(e_i).(-c_n).x_n. // Given an "eqz" node c_0 + c_1.x_1 + ... +c_n.x_n = 0, pivot variable x_i, and odd part e_i, this // function returns MI(e_i).(-c_0) + MI(e_i).(-c_1).x_1 + ... + MI(e_i).(-c_n).x_n as // Constant = MI(e_i).(-c_0) and CoefficientMap = vector < (x_1, MI(e_i).(-c_1)), ... ,(x_n, MI(e_i).(-c_n)) > // Returns false in case of errors; true otherwise. bool t_Project::getRHSOfEquationInNormalFormAsCoefficientMap(t_Expression* eqzNode, const string &PivotVariable, const bvatom &OddPart, bvatom &Constant, vector< pair< string, bvatom > > &CoefficientMap) { if(eqzNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! eqzNode is NULL in function t_Project::getRHSOfEquationInNormalFormAsCoefficientMap", pvt_logFile, c_RunLevelVerbosity); return false; } else if("eqz" != pvt_em->getLabelOfExpression(eqzNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::getRHSOfEquationInNormalFormAsCoefficientMap", pvt_logFile, c_RunLevelVerbosity); return false; } else { t_Expression* kaddNode = getIthChild(eqzNode, 0, pvt_em); assert(kaddNode != NULL); if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::getRHSOfEquationInNormalFormAsCoefficientMap", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(kaddNode); if(Children.size() == 0) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode with no children in function t_Project::getRHSOfEquationInNormalFormAsCoefficientMap", pvt_logFile, c_RunLevelVerbosity); return false; } else { // the first child can be a constant. check it, process it. assert(Children[0] != NULL); if(isBVConstant(Children[0], pvt_em)) { if(Children.size() == 1) // kadd has only one child which is a constant { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode with only one constant child in function t_Project::getRHSOfEquationInNormalFormAsCoefficientMap", pvt_logFile, c_RunLevelVerbosity); return false; } else { // obtain the label of Children[0] as bvatom: this is the constant on LHS i.e. c_0 string ConstantString = pvt_em->getLabelOfExpression(Children[0]); ConstantString = ConstantString.substr(2); //we need characters from position 2 to end: avoiding the initial "0b" bvatom ConstantOnLHS = pvt_bvm->getBVatom(ConstantString.size(), ConstantString); // We have c_0 now // Constant = (-c_0).MI(e_i) Constant = pvt_bvm->bvmul(pvt_bvm->addInverse(ConstantOnLHS), pvt_bvm->multInverse(OddPart)); Children.erase (Children.begin()); } }// if(isBVConstant(Children[0], pvt_em)) ends here else // no constant part. we need to set Constant to zero { int WidthOfKaddNode = pvt_em->getWidth(kaddNode); string ZeroString = getZeroBinaryStringOfGivenLength(WidthOfKaddNode); Constant = pvt_bvm->getBVatom(WidthOfKaddNode, ZeroString); } // Now Children is a vector of monoms CoefficientMap.clear();// Let's clear the map any way to begin with for(int index = 0; index < Children.size(); index++) { t_Expression* Child = Children[index]; assert(Child != NULL); // find the variable and the coefficient of monom string VariableOfMonom; bvatom CoefficientOfMonom; findVariableAndCoefficientOfMonom(Child, VariableOfMonom, CoefficientOfMonom, pvt_em, pvt_bvm); //if variable of monom == pivot variable, then no need to enter it into the map if(VariableOfMonom != PivotVariable) { // we have x_j, c_j now // we need to push back (x_j, (-c_j).MI(e_i)) bvatom CoefficientInNormalForm = pvt_bvm->bvmul(pvt_bvm->addInverse(CoefficientOfMonom), pvt_bvm->multInverse(OddPart)); CoefficientMap.push_back(make_pair(VariableOfMonom, CoefficientInNormalForm)); } }// for loop ends here return true; }//else of if(Children.size() == 0) ends here }//else of if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) ends here }//else of else if("eqz" != pvt_em->getLabelOfExpression(eqzNode)) ends here }//function ends here // Given a "kand" node, variable, and PivotEquation 2^{k}.x_i = t, where // k is represented as KappaOfPivotEquation and t is represented as // ConstantOfPivotEquationInNormalForm and CoefficientMapOfPivotEquationInNormalForm, // this function, takes each constraint in the "kand" node, // (1) if the constraint is not the PivotEquation, // then recreates the constraint by replacing each occurance of 2^{k}.x_i by t, // (2) if the constraint is the PivotEquation and if layer1 eliminates the variable, // then replaces the PivotEquation by \exists x.(2^{k}.x_i = t) \equiv (2^{p-k}. t = 0), // (3) if the constraint is the PivotEquation and layer1 does not eliminate the variable, // then keeps the PivotEquation. // Recreates the "kand" node, and returns it. // Returns true node if the result is true. Returns NULL in case of errors. // Sets layer1_eliminates_variable to true / false depending on whether layer1 completely // eliminates the variable or not. t_Expression* t_Project::substituteAndSimplifyKandNodeUsingPivotEquation(t_Expression* kandNode, const string &variable, t_Expression* PivotEquation, unsigned int KappaOfPivotEquation, const bvatom &ConstantOfPivotEquationInNormalForm, const vector< pair< string, bvatom > > &CoefficientMapOfPivotEquationInNormalForm, bool &layer1_eliminates_variable) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::substituteAndSimplifyKandNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::substituteAndSimplifyKandNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { assert(PivotEquation != NULL); vector Children = pvt_em->getVectorOfOperands(kandNode); set RecreatedEqzChildren; set RecreatedDiseqzChildren; set RecreatedLeqChildren; for(int i = 0; i < Children.size(); i++)// take each child { t_Expression* Child = Children[i]; assert(Child != NULL); if("eqz" == pvt_em->getLabelOfExpression(Child))//if child is equation { if(PivotEquation != Child)//if child is not pivot equation { // get the kadd node t_Expression* kaddNode = getIthChild(Child, 0, pvt_em); assert(kaddNode != NULL); // recreate the kadd node t_Expression* RecreatedKaddNode = substituteAndSimplifyKaddNodeUsingPivotEquation(kaddNode, variable, KappaOfPivotEquation, ConstantOfPivotEquationInNormalForm, CoefficientMapOfPivotEquationInNormalForm); if(RecreatedKaddNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! recreated kadd node is NULL in function t_Project::substituteAndSimplifyKandNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { // recreate the eqz node string equation_label = "eqz"; t_Expression* RecreatedChild = CreateNode(equation_label, RecreatedKaddNode, pvt_em); assert(RecreatedChild != NULL); // insert the recreated eqz node into the set unless it is trivial if(!equationIsTrivial(RecreatedChild, pvt_em)) //eg: 0=0, i.e. "kadd" node is 0. { RecreatedEqzChildren.insert(RecreatedChild); } } }//if child is not pivot equation ends here //else : Child is the pivot equation; QE will be done later. }//if child is equation ends here else if("diseqz" == pvt_em->getLabelOfExpression(Child))// if child is disequation { // get the kadd node t_Expression* kaddNode = getIthChild(Child, 0, pvt_em); assert(kaddNode != NULL); // recreate the kadd node t_Expression* RecreatedKaddNode = substituteAndSimplifyKaddNodeUsingPivotEquation(kaddNode, variable, KappaOfPivotEquation, ConstantOfPivotEquationInNormalForm, CoefficientMapOfPivotEquationInNormalForm); if(RecreatedKaddNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! recreated kadd node is NULL in function t_Project::substituteAndSimplifyKandNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { // recreate the diseqz node string disequation_label = "diseqz"; t_Expression* RecreatedChild = CreateNode(disequation_label, RecreatedKaddNode, pvt_em); assert(RecreatedChild != NULL); // insert the recreated diseqz node into the set unless it is trivial if(!disequationIsTrivial(RecreatedChild, pvt_em)) //eg: not(7=0), i.e. "kadd" node is non-zero constant. { RecreatedDiseqzChildren.insert(RecreatedChild); } } }//if child is disequation ends here else if("leq" == pvt_em->getLabelOfExpression(Child))// if child is inequation { // get the kadd nodes vector ChildrenOfLeqNode = pvt_em->getVectorOfOperands(Child); if(ChildrenOfLeqNode.size() != 2) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! number of children of leq node is not two in function t_Project::substituteAndSimplifyKandNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } t_Expression* LHSOfLeqNode = ChildrenOfLeqNode[0];// get the first child t_Expression* RHSOfLeqNode = ChildrenOfLeqNode[1];// get the second child assert(LHSOfLeqNode != NULL); assert(RHSOfLeqNode != NULL); // recreate the kadd nodes t_Expression* RecreatedLHSOfLeqNode = substituteAndSimplifyKaddNodeUsingPivotEquation(LHSOfLeqNode, variable, KappaOfPivotEquation, ConstantOfPivotEquationInNormalForm, CoefficientMapOfPivotEquationInNormalForm); t_Expression* RecreatedRHSOfLeqNode = substituteAndSimplifyKaddNodeUsingPivotEquation(RHSOfLeqNode, variable, KappaOfPivotEquation, ConstantOfPivotEquationInNormalForm, CoefficientMapOfPivotEquationInNormalForm); if(RecreatedLHSOfLeqNode == NULL || RecreatedRHSOfLeqNode == NULL ) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! recreated kadd node is NULL in function t_Project::substituteAndSimplifyKandNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { // recreate the leq node string inequation_label = "leq"; t_Expression* RecreatedChild = CreateNode(inequation_label, RecreatedLHSOfLeqNode, RecreatedRHSOfLeqNode, pvt_em); assert(RecreatedChild != NULL); // insert the recreated leq node into the set unless it is trivial if(!inequationIsTrivial(RecreatedChild, pvt_em, pvt_bvm)) //eg: 2 <= 3, t <= 2^{p}-1 etc. { RecreatedLeqChildren.insert(RecreatedChild); } } }//if child is inequation ends here else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered as child of kand node in function t_Project::substituteAndSimplifyKandNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } }// for each child ends here // Let's process the pivot equation now // Check if the variable is eliminated by layer1 layer1_eliminates_variable = true;//initialization for(set ::iterator it = RecreatedDiseqzChildren.begin(); it != RecreatedDiseqzChildren.end() && layer1_eliminates_variable; it++) { layer1_eliminates_variable = constraintFreeOfVariable(*it, variable, pvt_em, pvt_VariableList); } for(set ::iterator it = RecreatedLeqChildren.begin(); it != RecreatedLeqChildren.end() && layer1_eliminates_variable; it++) { layer1_eliminates_variable = constraintFreeOfVariable(*it, variable, pvt_em, pvt_VariableList); } if(!layer1_eliminates_variable)// layer1 could not eliminate the variable fully. // We should not eliminate variable from PivotEquation. { RecreatedEqzChildren.insert(PivotEquation); } else// layer1 eliminated the variable fully // Recall that we have PivotEquation as 2^{k}.x_i = t mod 2^{p}. // Let's create 2^{p-k}. t = 0 and insert it into RecreatedEqzChildren { if(KappaOfPivotEquation > 0) // if k = 0 then, 2^{p-k}. t = 0 is 2^{p}. t = 0, i.e. 0 = 0, which is trivial { t_Expression* RecreatedPivotEquation; bool QEDoneFromPivotEquation = QEFromSingleEquation(variable, PivotEquation, KappaOfPivotEquation, ConstantOfPivotEquationInNormalForm, CoefficientMapOfPivotEquationInNormalForm, RecreatedPivotEquation); assert(RecreatedPivotEquation != NULL); if(!QEDoneFromPivotEquation) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in quantifier elimination from pivot equation in function t_Project::substituteAndSimplifyKandNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if(!equationIsTrivial(RecreatedPivotEquation, pvt_em)) //trivial equation such as 0=0 { //insert into set of recreated equations RecreatedEqzChildren.insert(RecreatedPivotEquation); } }// if(KappaOfPivotEquation > 0) ends here }// layer1 eliminated the variable fully ends here // recreate the kand node t_Expression* RecreatedKandNode; if(RecreatedEqzChildren.empty() && RecreatedDiseqzChildren.empty() && RecreatedLeqChildren.empty()) { // all children are trivial; hence result is true RecreatedKandNode = getTrue(pvt_em); } else { RecreatedKandNode = CreateKandNode(RecreatedEqzChildren, RecreatedDiseqzChildren, RecreatedLeqChildren, pvt_em); } // return the recreated kand node assert(RecreatedKandNode != NULL); return RecreatedKandNode; }// else of if (!kandNode) ends here }// function ends here // Given a "kadd" node, variable, and pivot equation 2^{k}.x_i = t, where // k is represented as KappaOfPivotEquation, and t is represented as // ConstantOfPivotEquationInNormalForm and CoefficientMapOfPivotEquationInNormalForm, // this function, // recreates the "kadd" node by replacing each occurance of 2^{k}.x_i by t, // and returns it. Returns NULL in case of errors. t_Expression* t_Project::substituteAndSimplifyKaddNodeUsingPivotEquation(t_Expression* kaddNode, const string &variable, unsigned int KappaOfPivotEquation, const bvatom &ConstantOfPivotEquationInNormalForm, const vector< pair< string, bvatom > > &CoefficientMapOfPivotEquationInNormalForm) { if(kaddNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode is NULL in function t_Project::substituteAndSimplifyKaddNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::substituteAndSimplifyKaddNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { //Let's find the monom containing the variable in "kadd" node t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, pvt_em, pvt_VariableList); if(!MonomFound)// error in findMonomOfKaddNodeWithGivenVariable; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::substituteAndSimplifyKaddNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if(MonomWithVariable == NULL)// there's no monom in kadd node with the variable i.e. "kadd" node is free of variable { //return the original node return kaddNode; } else //"kadd" node contains variable { // suppose the "kadd" node is of the form c_0 + c_1.x_1 + ... +c_n.x_n // let variable be x_i. // let pivot equation be 2^{k}.x_i = t, where k is KappaOfPivotEquation // Now MonomWithVariable is c_i.x_i. Let's find c_i now i.e. CoefficientOfMonom bvatom CoefficientOfMonom; bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefficientOfMonom, pvt_em, pvt_bvm); if(!CoefficientFound)// error in findCoefficientOfMonom; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in finding coefficient in function t_Project::substituteAndSimplifyKaddNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else // c_i found correctly { // let's find the kappa k_i and odd part e_i of the coefficient c_i unsigned int KappaOfMonom; bvatom OddPartOfMonom; bool KappaFound = pvt_bvm->findKappaAndOddPart(CoefficientOfMonom, KappaOfMonom, OddPartOfMonom); if(!KappaFound)// error in pvt_bvm->findKappaAndOddPart; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in finding kappa in function t_Project::substituteAndSimplifyKaddNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } // c_i = 2^{k_i}.e_i where k_i is KappaOfMonom else if(KappaOfMonom < KappaOfPivotEquation) // k_i < k { // occurence of variable in monom cannot be eliminated using // pivot equation, since, monom's kappa < pivot equation's kappa // return the original node return kaddNode; } else // k_i >= k, hence kadd node can be simplified using pivot equation { // lets obtain c_0 + c_1.x_1 + ...c_{i-1}.x_{i-1} + c_{i+1}.x_{i+1} + ... + c_n.x_n // as constant and coefficient map bvatom ConstantOfKaddNode; //this is c_0 vector< pair< string, bvatom > > CoefficientMapOfKaddNode; // this is vector < x_1--> c_1,..., x_{i-1}-->c_{i-1}, x_{i+1}-->c_{i+1},..., x_n-->c_n > set variables_to_exclude; variables_to_exclude.insert(variable); bool CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(kaddNode, variables_to_exclude, ConstantOfKaddNode, CoefficientMapOfKaddNode, pvt_em, pvt_bvm); if(!CoefficientMapFound)// error in finding coefficient map; propogate it { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! coefficient map finding error in function t_Project::substituteAndSimplifyKaddNodeUsingPivotEquation", pvt_logFile, c_RunLevelVerbosity); return NULL; } else // constant part and coefficient map of kadd node found correctly { // Now c_i.x_i = 2^{k_i}.e_i.x_i, // 2^{k}.x_i = t, // and k_i >= k. // Hence c_i.x_i = 2^{k_i}.e_i.x_i // = 2^{k}.2^{k_l}.e_i.x_i, where k_l = k_i - k // = 2^{k_l}.e_i.t // = muliplier.t, where muliplier = 2^{k_l}.e_i unsigned int KappaDifference = KappaOfMonom - KappaOfPivotEquation; //k_l = k_i - k bvatom multiplier = pvt_bvm->bvlshift(OddPartOfMonom, KappaDifference);// muliplier = 2^{k_l}.e_i assert(!(pvt_bvm->checkBVForZero(multiplier)));//multiplier should not be zero, as e_i is odd and k_l < p // let's find (muliplier.t). recall that t is represented as ConstantOfPivotEquationInNormalForm and // CoefficientMapOfPivotEquationInNormalForm // MultipliedConstantOfPivotEquationInNormalForm = multiplier.ConstantOfPivotEquationInNormalForm bvatom MultipliedConstantOfPivotEquationInNormalForm = pvt_bvm->bvmul(multiplier, ConstantOfPivotEquationInNormalForm); vector< pair< string, bvatom > > MultipliedCoefficientMapOfPivotEquationInNormalForm; // MulipliedCoefficientMapOfPivotEquationInNormalForm = multiplier.CoefficientMapOfPivotEquationInNormalForm scalarMultiplication(CoefficientMapOfPivotEquationInNormalForm, multiplier, MultipliedCoefficientMapOfPivotEquationInNormalForm, pvt_bvm); // we have found muliplier.t now // kadd node, i.e. c_0 + c_1.x_1 + ...c_i.x_i + ... +c_n.x_n now becomes // c_0 + c_1.x_1 + ...c_{i-1}.x_{i-1} + c_{i+1}.x_{i+1} + ... + c_n.x_n + muliplier.t // let's add c_0 + c_1.x_1 + ...c_{i-1}.x_{i-1} + c_{i+1}.x_{i+1} + ... + c_n.x_n with muliplier.t // final constant = constant part of muliplier.t + c_0 bvatom FinalConstant = pvt_bvm->bvadd(MultipliedConstantOfPivotEquationInNormalForm, ConstantOfKaddNode); vector< pair< string, bvatom > > FinalCoefficientMap; // final coefficient map = coefficient map part of muliplier.t + coefficient map part of kadd node addition(MultipliedCoefficientMapOfPivotEquationInNormalForm, CoefficientMapOfKaddNode, FinalCoefficientMap, pvt_bvm, pvt_VariableList); // create "kadd" node from final constant and final coefficient map, and return it int WidthOfKaddNode = pvt_em->getWidth(kaddNode); t_Expression *RecreatedKaddNode = CreateKaddNodeFromConstantAndCoefficientMap(WidthOfKaddNode, FinalConstant, FinalCoefficientMap, pvt_em, pvt_VariableList, pvt_bvm); assert(RecreatedKaddNode != NULL); return RecreatedKaddNode; }// constant part and coefficient map of kadd node found correctly ends here }// k_i >= k, hence kadd node can be simplified using pivot equation ends here }// c_i found correctly ends here }//"kadd" node contains variable ends here }//else of else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) ends here }// function ends here // We have PivotEquation as 2^{k}.x_{i} = t mod 2^{p}. // This function creates 2^{p-k}. t = 0 in RecreatedPivotEquation. // Returns false in case of errors, true otherwise. bool t_Project::QEFromSingleEquation(const string &variable, t_Expression* PivotEquation, unsigned int KappaOfPivotEquation, const bvatom &ConstantOfPivotEquationInNormalForm, const vector< pair< string, bvatom > > &CoefficientMapOfPivotEquationInNormalForm, t_Expression* &RecreatedPivotEquation) { if(PivotEquation == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! PivotEquation is NULL in function t_Project::QEFromSingleEquation", pvt_logFile, c_RunLevelVerbosity); return false; } else if("eqz" != pvt_em->getLabelOfExpression(PivotEquation)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::QEFromSingleEquation", pvt_logFile, c_RunLevelVerbosity); return false; } else { t_Expression* kaddNode = getIthChild(PivotEquation, 0, pvt_em); assert(kaddNode != NULL); if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::QEFromSingleEquation", pvt_logFile, c_RunLevelVerbosity); return false; } else { //Let's find p, i.e. width of kadd node int WidthOfKaddNode = pvt_em->getWidth(kaddNode); // Let's find KappaDifference = p - k int KappaDifference = WidthOfKaddNode - KappaOfPivotEquation; assert(KappaDifference > 0 && KappaDifference < WidthOfKaddNode); // Let's create 2^{p-k}. t = 0 in RecreatedPivotEquation // Let's just left shift by p-k, rather than multiplying bvatom MultipliedConstantOfPivotEquationInNormalForm = pvt_bvm->bvlshift(ConstantOfPivotEquationInNormalForm, KappaDifference); vector< pair< string, bvatom > > MultipliedCoefficientMapOfPivotEquationInNormalForm; leftShift(CoefficientMapOfPivotEquationInNormalForm, KappaDifference, MultipliedCoefficientMapOfPivotEquationInNormalForm, pvt_bvm); // create the equation // let's create the "kadd" node first t_Expression *RecreatedKaddNode = CreateKaddNodeFromConstantAndCoefficientMap(WidthOfKaddNode, MultipliedConstantOfPivotEquationInNormalForm, MultipliedCoefficientMapOfPivotEquationInNormalForm, pvt_em, pvt_VariableList, pvt_bvm); assert(RecreatedKaddNode != NULL); string equation_label = "eqz"; RecreatedPivotEquation = CreateNode(equation_label, RecreatedKaddNode, pvt_em); assert(RecreatedPivotEquation != NULL); return true; }//else of if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) ends here }// else of else if("eqz" != pvt_em->getLabelOfExpression(PivotEquation)) ends here }//function ends here // Given a "kand" node, this function applies layer1 to eliminate variable // Returns NULL in case of errors, true node if the result is true, and // simplified "kand" node otherwise. t_Expression* t_Project::QE1_Layer1(t_Expression* kandNode, const string &variable) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::QE1_Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::QE1_Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { // check in hash table first t_Expression* ResultFromHashTable = checkIn_QE1_Layer1_HashTable(kandNode, variable); if(ResultFromHashTable != NULL) //hash table hit { return ResultFromHashTable; } else //hash table miss { t_Expression* pivotEqzNode; unsigned int KappaOfPivotEqzNode; bvatom OddPartOfPivotEqzNode; t_Expression* SimplifiedKandNode; //result // finding the pivot equation - equation with the least kappa value for the variable bool EquationFound = findEquationWithMinimumKappaValue(kandNode, variable, pivotEqzNode, KappaOfPivotEqzNode, OddPartOfPivotEqzNode); if(!EquationFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in finding pivot equation in function t_Project::QE1_Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { if(KappaOfPivotEqzNode == UINT_MAX) { // equations in "kand" are free of variable; layer1 cannot do anything SimplifiedKandNode = kandNode; } else { bvatom ConstantOfPivotEqzNodeInNormalForm; vector< pair< string, bvatom > > CoefficientMapOfPivotEqzNodeInNormalForm; // getting rhs of pivot equation in normalized form i.e. as 2^{k}.x_i = t bool CoefficientMapFound = getRHSOfEquationInNormalFormAsCoefficientMap(pivotEqzNode, variable, OddPartOfPivotEqzNode, ConstantOfPivotEqzNodeInNormalForm, CoefficientMapOfPivotEqzNodeInNormalForm); if(!CoefficientMapFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in getting coefficient map in function t_Project::QE1_Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { // performing substitution in kandNode using pivot equation bool layer1_eliminates_variable; // for statitics collection t_Expression* kandAfterSubstitution = substituteAndSimplifyKandNodeUsingPivotEquation(kandNode, variable, pivotEqzNode, KappaOfPivotEqzNode, ConstantOfPivotEqzNodeInNormalForm, CoefficientMapOfPivotEqzNodeInNormalForm, layer1_eliminates_variable); if(kandAfterSubstitution == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in simplification of kand node using pivot equation in function t_Project::QE1_Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { SimplifiedKandNode = kandAfterSubstitution; }// else of if(kandAfterSubstitution == NULL) ends here }// else of if(!CoefficientMapFound) ends here }//else of if(KappaOfPivotEqzNode == UINT_MAX) ends here }// else of if(!EquationFound) ends here // update the hash table bool HashTable_Updated = update_QE1_Layer1_HashTable(kandNode, variable, SimplifiedKandNode); if(!HashTable_Updated) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in hash table insertion in function t_Project::QE1_Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { return SimplifiedKandNode; }// else of if(!HashTable_Updated) ends here }//hash table miss ends here }// else of else if("kand" != pvt_em->getLabelOfExpression(kandNode)) ends here }// function ends here // Checks if (InputKandNode, variable) is existing in pvt_QE1_Layer1_HashTable. // Returns the result if existing; NULL otherwise. t_Expression* t_Project::checkIn_QE1_Layer1_HashTable(t_Expression* InputKandNode, const string &variable) { assert(InputKandNode != NULL); // key = address of input kand node + variable to be eliminated string key = toString(InputKandNode); key += variable; t_HTStatusValue result_search = pvt_QE1_Layer1_HashTable.hashtable_search(key); if(result_search.success()) { return result_search.getValue(); } else { return NULL; } }//function ends here // Updates pvt_QE1_Layer1_HashTable with (InputKandNode, variable) ---> OutputKandNode. // Returns false in case of errors; true otherwise. bool t_Project::update_QE1_Layer1_HashTable(t_Expression* InputKandNode, const string &variable, t_Expression* OutputKandNode) { assert(InputKandNode != NULL); assert(OutputKandNode != NULL); // key = address of input kand node + variable to be eliminated string key = toString(InputKandNode); key += variable; t_HTStatusValue insert_result = pvt_QE1_Layer1_HashTable.hashtable_insert(key, OutputKandNode); if (insert_result.success()) { return true; } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in hash table insertion in function t_Project::update_QE1_Layer1_HashTable", pvt_logFile, c_RunLevelVerbosity); return false; } }//function ends here // Given a "kand" node, this function applies layer1 to eliminate multiple variables. // Returns NULL in case of errors, true node if the result is true, and simplified "kand" node otherwise. t_Expression* t_Project::Layer1(t_Expression* kandNode, const vector &variables) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { int var_size = variables.size(); for(int i = 0; i < var_size; i++) // take each variable to eliminate { string variable = variables[i]; t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("Calling QE1_Layer1 for eliminating variable" + variable, pvt_logFile, c_DebugLevelVerbosity); // let's eliminate variable from kandNode kandNode = QE1_Layer1(kandNode, variable); if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! result from QE1_Layer1 is NULL in function t_Project::Layer1", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if(isTrue(kandNode, pvt_em)) //kandNode == true { break; } logManager->LOG("QE1_Layer1 finished", pvt_logFile, c_DebugLevelVerbosity); }//for ends here return kandNode; }//else ends here }// function ends here /**********************************************************************/ /* Part 3: Functions for Layer2 */ /**********************************************************************/ // Given a "kand" node, this function calls the function to apply layer2 // for eliminating multiple variables in a loop. Dropping constraints involving a // variable may help in dropping constraints involving other variables. Hence we // call the function to apply layer2 for eliminating multiple variables in a loop, // until no more droppping is possible. // Returns NULL in case of errors, true node if the result is true, // and simplified "kand" node otherwise. t_Expression* t_Project::Layer2(t_Expression* kandNode, const vector &variables) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::Layer2", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::Layer2", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { t_Expression* OldKandNode; do { OldKandNode = kandNode; t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("Calling Layer2Step for eliminating variables", pvt_logFile, c_DebugLevelVerbosity); // let's eliminate variables from kandNode kandNode = Layer2Step(kandNode, variables); if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! result from t_Project::Layer2Step is NULL in function t_Project::Layer2", pvt_logFile, c_RunLevelVerbosity); return NULL; } }while(!isTrue(kandNode, pvt_em) && (kandNode != OldKandNode)); //do-while ends here return kandNode; }//else ends here }// function ends here // Given a "kand" node, this function applies layer2 for eliminating multiple // variables. // Returns NULL in case of errors, true node if the result is true, // and simplified "kand" node otherwise. t_Expression* t_Project::Layer2Step(t_Expression* kandNode, const vector &variables) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { int var_size = variables.size(); for(int i = 0; i < var_size; i++) // take each variable to eliminate { string variable = variables[i]; t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("Calling QE1_Layer2Step for eliminating variable" + variable, pvt_logFile, c_DebugLevelVerbosity); // let's eliminate variable from kandNode kandNode = QE1_Layer2Step(kandNode, variable); if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! result from t_Project::QE1_Layer2Step is NULL in function t_Project::Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if(isTrue(kandNode, pvt_em)) //kandNode == true { break; } logManager->LOG("QE1_Layer2Step finished", pvt_logFile, c_DebugLevelVerbosity); }//for ends here return kandNode; }//else ends here }// function ends here // Given a "kand" node, this function applies layer2 to eliminate a variable. // Returns NULL in case of errors, true node if the result is true, and // simplified "kand" node otherwise. t_Expression* t_Project::QE1_Layer2Step(t_Expression* kandNode, const string &variable) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { // check in hash table first t_Expression* ResultFromHashTable = checkIn_QE1_Layer2_HashTable(kandNode, variable); if(ResultFromHashTable != NULL) //hash table hit { return ResultFromHashTable; } else //hash table miss { t_Expression* SimplifiedKandNode; //result // computing result set E_x, E_neg_x; set D_x, D_neg_x; set I_x, I_neg_x; // Recall that kandNode is a conjunction of equations, disequations, and inequations. // Obtain the equations with variable in E_x, equations without variable in E_neg_x, // disequations with variable in D_x, disequations without variable in D_neg_x, // inequations with variable in I_x, inequations without variable in I_neg_x, bool ConstraintsFound = findFreeAndBoundConstraintsFromKandNode(kandNode, variable, E_x, D_x, I_x, E_neg_x, D_neg_x, I_neg_x, pvt_em, pvt_VariableList); if(!ConstraintsFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in finding free and bound constraints in t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } set E_core_x; set D_core_x; set I_core_x; // find the core constraints among E_x, D_x, and I_x in E_core_x, D_core_x, and I_core_x bool CoreFound = findCoreConstraints(E_x, D_x, I_x, variable, E_core_x, D_core_x, I_core_x); if(!CoreFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in finding core constraints in t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } if(E_core_x.size() == 1 && D_core_x.empty() && I_core_x.empty()) // layer2 eliminated all the disequations and inequations. // there's only one equation left in the scope of the quantifier. { set::iterator e_core_x_it = E_core_x.begin(); t_Expression* PivotEquation = *e_core_x_it; unsigned KappaOfPivotEquation; bvatom OddPartOfPivotEquation; bool KappaOfPivotEquation_Found = findKappaValueAndOddPartOfEqz(PivotEquation, variable, KappaOfPivotEquation, OddPartOfPivotEquation); if(!KappaOfPivotEquation_Found) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if(KappaOfPivotEquation == UINT_MAX) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! core equation free of variable in function t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } // Recall that we have PivotEquation as 2^{k}.x_i = t mod 2^{p}. // Let's create 2^{p-k}. t = 0 and replace 2^{k}.x_i = t mod 2^{p} in E_core_x by this. E_core_x.clear(); if(KappaOfPivotEquation > 0) // if k = 0 then, 2^{p-k}. t = 0 is 2^{p}. t = 0, i.e. 0 = 0, which is trivial // E_core_x is empty in this case. { bvatom ConstantOfPivotEquationInNormalForm; vector< pair< string, bvatom > > CoefficientMapOfPivotEquationInNormalForm; // getting rhs of pivot equation in normalized form i.e. as 2^{k}.x_i = t bool CoefficientMapFound = getRHSOfEquationInNormalFormAsCoefficientMap(PivotEquation, variable, OddPartOfPivotEquation, ConstantOfPivotEquationInNormalForm, CoefficientMapOfPivotEquationInNormalForm); if(!CoefficientMapFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in getting coefficient map in function t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } t_Expression* RecreatedPivotEquation; bool QEDoneFromPivotEquation = QEFromSingleEquation(variable, PivotEquation, KappaOfPivotEquation, ConstantOfPivotEquationInNormalForm, CoefficientMapOfPivotEquationInNormalForm, RecreatedPivotEquation); assert(RecreatedPivotEquation != NULL); if(!QEDoneFromPivotEquation) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in quantifier elimination from pivot equation in function t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if(!equationIsTrivial(RecreatedPivotEquation, pvt_em)) //trivial equation such as 0=0 { //insert into set of core equations E_core_x.insert(RecreatedPivotEquation); } }// if(KappaOfPivotEquation > 0) ends here }// layer2 eliminated all the disequations and inequations ends here set E; set D; set I; //find the final set of equations, disequations, and inequations in E, D, and I set_union(E_core_x.begin(), E_core_x.end(), E_neg_x.begin(), E_neg_x.end(),inserter(E, E.begin())); set_union(D_core_x.begin(), D_core_x.end(), D_neg_x.begin(), D_neg_x.end(),inserter(D, D.begin())); set_union(I_core_x.begin(), I_core_x.end(), I_neg_x.begin(), I_neg_x.end(),inserter(I, I.begin())); // recreate the kand node if(E.empty() && D.empty() && I.empty()) { // all constraints are dropped; hence result is true SimplifiedKandNode = getTrue(pvt_em); } else { SimplifiedKandNode = CreateKandNode(E, D, I, pvt_em); } assert(SimplifiedKandNode != NULL); // update the hash table bool HashTable_Updated = update_QE1_Layer2_HashTable(kandNode, variable, SimplifiedKandNode); if(!HashTable_Updated) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in hash table insertion in function t_Project::QE1_Layer2Step", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { return SimplifiedKandNode; }// else of if(!HashTable_Updated) ends here }//hash table miss ends here }// else of else if("kand" != pvt_em->getLabelOfExpression(kandNode)) ends here }// function ends here // Checks if (InputKandNode, variable) is existing in pvt_QE1_Layer2_HashTable. // Returns the result if existing; NULL otherwise. t_Expression* t_Project::checkIn_QE1_Layer2_HashTable(t_Expression* InputKandNode, const string &variable) { assert(InputKandNode != NULL); // key = address of input kand node + variable to be eliminated string key = toString(InputKandNode); key += variable; t_HTStatusValue result_search = pvt_QE1_Layer2_HashTable.hashtable_search(key); if(result_search.success()) { return result_search.getValue(); } else { return NULL; } }//function ends here // Updates pvt_QE1_Layer2_HashTable with (InputKandNode, variable) ---> OutputKandNode. // Returns false in case of errors; true otherwise. bool t_Project::update_QE1_Layer2_HashTable(t_Expression* InputKandNode, const string &variable, t_Expression* OutputKandNode) { assert(InputKandNode != NULL); assert(OutputKandNode != NULL); // key = address of input kand node + variable to be eliminated string key = toString(InputKandNode); key += variable; t_HTStatusValue insert_result = pvt_QE1_Layer2_HashTable.hashtable_insert(key, OutputKandNode); if (insert_result.success()) { return true; } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in hash table insertion in function t_Project::update_QE1_Layer2_HashTable", pvt_logFile, c_RunLevelVerbosity); return false; } }//function ends here // find the core constraints among E_x, D_x, and I_x in E_core_x, D_core_x, and I_core_x. // i.e. find E_core_x, D_core_x, and I_core_x such that // \exists x. (E_x \union D_x \union I_x) \equiv exists x. (E_core_x \union D_core_x \union I_core_x) // returns false in the case of errors; true otherwise. bool t_Project::findCoreConstraints(const set &E_x, const set &D_x, const set &I_x, const string &variable, set &E_core_x, set &D_core_x, set &I_core_x) { if(E_x.empty() && D_x.empty() && I_x.empty()) { // set core to empty set E_core_x.clear(); D_core_x.clear(); I_core_x.clear(); return true; } else { set D_neg_core_x; set I_neg_core_x; // Let us partition the constraints into core and ~core. // To start with, put all equations in core and // put all disequations and inequations in ~core. E_core_x = E_x; D_core_x.clear(); I_core_x.clear(); D_neg_core_x = D_x; I_neg_core_x = I_x; while(!D_neg_core_x.empty() || !I_neg_core_x.empty()) // repeat this as long as ~core is non-empty i.e. // as long as core does not contain all the constraints. { bool Extendable; bool isExtFound = isExt(E_core_x, D_core_x, I_core_x, D_neg_core_x, I_neg_core_x, variable, Extendable); if(!isExtFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! eta computing error in function t_Project::findCoreConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Extendable) // \exists x. (E_core_x \union D_core_x \union I_core_x \union D_neg_core_x \union I_neg_core_x) \equiv // \exists x. (E_core_x \union D_core_x \union I_core_x) // i.e. \exists x. (core \union ~core) \equiv \exists x. (core) { // core is in E_core_x, D_core_x, I_core_x return true; } else // i.e. \exists x. (core \union ~core) \notequiv \exists x. (core) // expand core and try { set D_new; set I_new; // find the least constraing constraints of ~core in new bool LeastConstrFound = getLeastConstrainingConstraints(D_neg_core_x, I_neg_core_x, variable, D_new, I_new); if(!LeastConstrFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! in finding the least constraining constraints in function t_Project::findCoreConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } // ~core := ~core - new set D_diff; set I_diff; set_difference(D_neg_core_x.begin(), D_neg_core_x.end(), D_new.begin(), D_new.end(),inserter(D_diff, D_diff.begin())); set_difference(I_neg_core_x.begin(), I_neg_core_x.end(), I_new.begin(), I_new.end(),inserter(I_diff, I_diff.begin())); D_neg_core_x = D_diff; I_neg_core_x = I_diff; // core := core \union new set_union(D_core_x.begin(), D_core_x.end(), D_new.begin(), D_new.end(),inserter(D_core_x, D_core_x.begin())); set_union(I_core_x.begin(), I_core_x.end(), I_new.begin(), I_new.end(),inserter(I_core_x, I_core_x.begin())); } //\exists x. (core \union ~core) \notequiv \exists x. (core) ends here }// while ends here // core is in E_core_x, D_core_x, I_core_x return true; }// E_x, D_x, or I_x is non-empty ends here }// function ends here // Suppose ~core = D_neg_core_x \union I_neg_core_x. // This function finds the least constraing constraints of ~core in D_new and I_new. // Least constraining constraints are those with the maximum kappa value. // Returns false in case of errors; true otherwise. bool t_Project::getLeastConstrainingConstraints(const set &D_neg_core_x, const set &I_neg_core_x, const string &variable, set &D_new, set &I_new) { D_new.clear(); I_new.clear(); unsigned KappaMax = 0; // take each Disequation in D_neg_core_x for(set::iterator it = D_neg_core_x.begin(); it != D_neg_core_x.end(); it++) { t_Expression* Disequation = *it; // find Kappa unsigned Kappa; bool KappaFound = findKappaValueOfDiseqz(Disequation, variable, Kappa); if(!KappaFound) // Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::getLeastConstrainingConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa == UINT_MAX) //Error!! Disequation free of variable; should not occure as we are working on bound constraints!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! constraint free of variable to be eliminated encountered in function t_Project::getLeastConstrainingConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa > KappaMax) //Disequation is a lesser constraining one { KappaMax = Kappa; D_new.clear(); D_new.insert(Disequation); } else if(Kappa == KappaMax) //Disequation constrains the same no: of bits as those in D_new { D_new.insert(Disequation); } }// for each disequation ends here // take each Inequation in I_neg_core_x for(set::iterator it = I_neg_core_x.begin(); it != I_neg_core_x.end(); it++) { t_Expression* Inequation = *it; // find Kappa unsigned Kappa; bool KappaFound = findKappaValueOfLeq(Inequation, variable, Kappa); if(!KappaFound) // Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::getLeastConstrainingConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa == UINT_MAX) //Error!! Inequation free of variable; should not occure as we are working on bound constraints!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! constraint free of variable to be eliminated encountered in function t_Project::getLeastConstrainingConstraints", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa > KappaMax) //Inequation is a lesser constraining one than the constraints in D_new and I_new { KappaMax = Kappa; D_new.clear(); I_new.clear(); I_new.insert(Inequation); } else if(Kappa == KappaMax) //Inequation constrains the same no: of bits as those in D_new and I_new { I_new.insert(Inequation); } }// for each inequation ends here return true; }// function ends here // Checks if // \exists x. (E_core_x \union D_core_x \union I_core_x \union D_neg_core_x \union I_neg_core_x) \equiv // \exists x. (E_core_x \union D_core_x \union I_core_x) // i.e. \exists x. (core \union ~core) \equiv \exists x. (core) // using the idea described in TACAS'13 paper // // Sets Extendable to true if yes, false otherwise. // Returns false in case of errors; true otherwise. bool t_Project::isExt(const set &E_core_x, const set &D_core_x, const set &I_core_x, const set &D_neg_core_x, const set &I_neg_core_x, const string &variable, bool &Extendable) { // Find p, i.e. width of variable int p = getWidthOfVariable(variable, pvt_WidthTable); assert(p > 0); // Find Kappa_0, i.e. minimum kappa among constraints in core unsigned int Kappa_0; if(E_core_x.empty() && D_core_x.empty() && I_core_x.empty()) // core is empty { Kappa_0 = p; } else // core is non-empty { bool Kappa_0_Found; // Let's form the core. core = E_core_x \union D_core_x \union I_core_x set core = E_core_x; set_union(D_core_x.begin(), D_core_x.end(), core.begin(), core.end(),inserter(core, core.begin())); set_union(I_core_x.begin(), I_core_x.end(), core.begin(), core.end(),inserter(core, core.begin())); // Let's find Kappa_0 Kappa_0_Found = findMinimumKappaValueAmongSetOfConstraints(core, variable, Kappa_0); if(!Kappa_0_Found) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::isExt", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa_0 == UINT_MAX) //Error!! core is non-empty and core is free of variable. { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! suspicious core in function t_Project::isExt", pvt_logFile, c_RunLevelVerbosity); return false; } assert(Kappa_0 < p); }// if core is non-empty ends here // Let's decide whether to use machine arithmetic // or bv-library for the computations. // Do computations using machine arithmetic // if pvt_use_bvlibrary_for_layer2_computations is false and // the width of variable to be eliminated is less than number of bits of t_compute. // Note that if p is the width of variable to be eliminated, // then all computations can be done using p+1 bits. if(!pvt_use_bvlibrary_for_layer2_computations && p < sizeof(t_compute)*BYTE_SIZE) { // USE MACHINE ARITHMETIC // Let's compute Mu_I (under-approximation of the number of valuations to the // most significant Kappa_0 bits of variable satisfying the inequations in I_neg_core_x) t_compute Mu_I; if(I_neg_core_x.empty()) // no inequations in core { // All 2^{Kappa_0} valuations are permitted. Mu_I = findTwosPower_UsingMachineArithmetic(Kappa_0); } else { bool Mu_I_Found = computeCombinationsPermittedByInequations_UsingMachineArithmetic(Kappa_0, I_neg_core_x, variable, p, Mu_I); if(!Mu_I_Found) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Mu_I finding error using machine arithmetic in function t_Project::isExt", pvt_logFile, c_RunLevelVerbosity); return false; } } // compute Mu_D and set Extendable = Mu_I > Mu_D bool Extendable_Found = checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingMachineArithmetic(Mu_I, D_neg_core_x, variable, p, Kappa_0, Extendable); if(!Extendable_Found) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Mu_D finding error using machine arithmetic in function t_Project::isExt", pvt_logFile, c_RunLevelVerbosity); return false; } return true; } else { // USE BV-LIBRARY // Let's compute Mu_I (under-approximation of the number of valuations to the // most significant Kappa_0 bits satisfying the inequations) bvatom Mu_I; if(I_neg_core_x.empty()) { // All 2^{Kappa_0} valuations are permitted. Mu_I = findTwosPower_UsingBVLibrary(p+1, Kappa_0); // Note that max width needed is p+1 } else { bool Mu_I_Found = computeCombinationsPermittedByInequations_UsingBVLibrary(Kappa_0, I_neg_core_x, variable, p, Mu_I); // Operations done using p+1 bits: but note that we are passing p if(!Mu_I_Found) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Mu_I finding error using bv-library in function t_Project::isExt", pvt_logFile, c_RunLevelVerbosity); return false; } } // compute Mu_D and set Extendable = Mu_I > Mu_D bool Extendable_Found = checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingBVLibrary(Mu_I, D_neg_core_x, variable, p, Kappa_0, Extendable); if(!Extendable_Found) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Mu_D finding error using bv-library in function t_Project::isExt", pvt_logFile, c_RunLevelVerbosity); return false; } return true; } }// function ends here // compute 2^{Kappa} using machine arithmetic t_compute t_Project::findTwosPower_UsingMachineArithmetic(unsigned Kappa) { t_compute result = 1; assert(Kappa < sizeof(t_compute)*BYTE_SIZE); // to avoid overflow during << result = result << Kappa; // this makes result = 2^{Kappa} return result; } // compute 2^{Kappa} using bv-library // WidthOfResult is the width (no: of bits) of the result bvatom bvatom t_Project::findTwosPower_UsingBVLibrary(unsigned WidthOfResult, unsigned Kappa) { string OneString = getOneBinaryStringOfGivenLength(WidthOfResult); bvatom result = pvt_bvm->getBVatom(WidthOfResult, OneString); // result = 1 assert(Kappa < WidthOfResult); // to avoid overflow during bvlshift result = pvt_bvm->bvlshift(result, Kappa); // this makes result = 2^{Kappa} return result; } // Using machine arithmetic, // finds Mu_D i.e. the number of valuations of the bits of variable // disallowed by the disequations in D_neg_core_x, and checks if Mu_D < Mu_I. // Sets Extendable to true if Mu_D < Mu_I, and to false if Mu_D >= Mu_I. // Returns false in the case of errors; true otherwise. bool t_Project::checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingMachineArithmetic(t_compute Mu_I, const set &D_neg_core_x, const string &variable, unsigned p, unsigned Kappa_0, bool &Extendable) { t_compute Mu_D = 0; // take each Disequation in D_neg_core_x for(set::iterator it = D_neg_core_x.begin(); it != D_neg_core_x.end(); it++) { t_Expression* Disequation = *it; assert(Disequation != NULL); // find Kappa unsigned Kappa; bool KappaFound = findKappaValueOfDiseqz(Disequation, variable, Kappa); if(!KappaFound) // Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa == UINT_MAX) //Error!! Disequation free of variable; should not occure as we are working on bound constraints!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! constraint free of variable to be eliminated encountered in function t_Project::checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa >= Kappa_0) //kappa of disequation >= kappa of equation; no dropping { Extendable = false; return true; } assert(Kappa < p); // Mu_D = Sum of 2^{Kappa} of the disequations t_compute PowerOfKappa = findTwosPower_UsingMachineArithmetic(Kappa); Mu_D = Mu_D + PowerOfKappa; if(Mu_D >= Mu_I) { Extendable = false; return true; } }// for ends here if(Mu_D >= Mu_I) { Extendable = false; } else { Extendable = true; } return true; }//function ends here // Using bv-library, // finds Mu_D i.e. the number of valuations of the bits of variable // disallowed by the disequations in D_neg_core_x, and checks if Mu_D < Mu_I. // Sets Extendable to true if Mu_D < Mu_I, and to false if Mu_D >= Mu_I. // Returns false in the case of errors; true otherwise. // Width (no: of bits) of the result bvatom is p+1. bool t_Project::checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingBVLibrary(bvatom Mu_I, const set &D_neg_core_x, const string &variable, unsigned p, unsigned Kappa_0, bool &Extendable) { unsigned WidthOfResult = p+1; string ZeroString = getZeroBinaryStringOfGivenLength(WidthOfResult); bvatom Mu_D = pvt_bvm->getBVatom(WidthOfResult, ZeroString); //Mu_D = 0 // take each Disequation in D_neg_core_x for(set::iterator it = D_neg_core_x.begin(); it != D_neg_core_x.end(); it++) { t_Expression* Disequation = *it; assert(Disequation != NULL); // find Kappa unsigned Kappa; bool KappaFound = findKappaValueOfDiseqz(Disequation, variable, Kappa); if(!KappaFound) // Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa == UINT_MAX) //Error!! Disequation free of variable; should not occure as we are working on bound constraints!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! constraint free of variable to be eliminated encountered in function t_Project::checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa >= Kappa_0) //kappa of disequation >= kappa of equation; no dropping { Extendable = false; return true; } assert(Kappa < p); // Mu_D = Sum of 2^{Kappa} of the disequations bvatom PowerOfKappa = findTwosPower_UsingBVLibrary(WidthOfResult, Kappa); Mu_D = pvt_bvm->bvadd(Mu_D, PowerOfKappa); if(pvt_bvm->checkBVGreaterThan(Mu_D, Mu_I) || pvt_bvm->checkBVEquality(Mu_D, Mu_I)) //if (Mu_D >= Mu_I) { Extendable = false; return true; } }// for ends here if(pvt_bvm->checkBVGreaterThan(Mu_D, Mu_I) || pvt_bvm->checkBVEquality(Mu_D, Mu_I)) //if (Mu_D >= Mu_I) { Extendable = false; } else { Extendable = true; } return true; }//function ends here // Using machine arithmetic, // finds Mu_I i.e. under-approximation of the number of valuations to the // most significant Kappa_0 bits of variable satisfying the inequations in I_neg_core_x. // Returns false in the case of errors; true otherwise. bool t_Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic(unsigned Kappa_0, const set &I_neg_core_x, const string &variable, unsigned p, t_compute &Mu_I) { // Let us create the map (s_j --> (u_j, v_j)), where s_j denotes a term // containing variable, u_j is the maximum among the lower bounds of s_j, and // v_j is the minimum among the upper bounds of s_j. map > BoundMap; // take each Inequation in I_neg_core_x for(set::iterator it = I_neg_core_x.begin(); it != I_neg_core_x.end(); it++) { t_Expression* Inequation = *it; assert(Inequation != NULL); // get the kadd nodes t_Expression* LHSOfLeqNode = getIthChild(Inequation, 0, pvt_em);// get the LHS t_Expression* RHSOfLeqNode = getIthChild(Inequation, 1, pvt_em);// get the RHS assert(LHSOfLeqNode != NULL); assert(RHSOfLeqNode != NULL); t_Expression* MonomWithVariableOnLHS; bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, pvt_em, pvt_VariableList); t_Expression* MonomWithVariableOnRHS; bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, pvt_em, pvt_VariableList); if(!LHSMonomFound || !RHSMonomFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariableOnLHS == NULL && MonomWithVariableOnRHS == NULL) //ERROR!!lhs is free of variable and rhs is free of variable: we are working on bound constraints { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! inequation free of variable to be eliminated in function t_Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariableOnLHS != NULL && MonomWithVariableOnRHS != NULL) //lhs contains variable and rhs contains variable: dropping not possible { Mu_I = 0; return true; } else if(MonomWithVariableOnLHS == NULL && MonomWithVariableOnRHS != NULL) //lhs is free of variable and rhs is a term containing variable { // lhs is a lower bound for rhs // Let us find the maximum possible value of lhs t_compute MaxPossibleValueOfLHS; bool MaxPossibleValueComputed = computeMaximumPossibleValueOfKadd_UsingMachineArithmetic(LHSOfLeqNode, p, MaxPossibleValueOfLHS); if(!MaxPossibleValueComputed) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! in finding maximum possible value of a term in function t_Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } // update the BoundMap using rhs and maximum possible value of lhs // check if entry already exists in BoundMap for rhs map >::iterator bmap_it = BoundMap.find(RHSOfLeqNode); if(bmap_it != BoundMap.end()) //entry exists for rhs { t_compute ExistingMaximumLowerBound = (bmap_it->second).first; // u_j is the first one in the pair // new u_j = max(maximum possible value of lhs, existing u_j) if(MaxPossibleValueOfLHS > ExistingMaximumLowerBound) { // new u_j = maximum possible value of lhs (bmap_it->second).first = MaxPossibleValueOfLHS; } }//entry exists for rhs ends here else //entry does not exist for rhs; insert a new entry { t_compute MaximumPossibleValue = findTwosPower_UsingMachineArithmetic(p)-1; //2^{p}-1 // insert (rhs --> (maximum possible value of lhs, 2^{p}-1)) in BoundMap BoundMap.insert(make_pair(RHSOfLeqNode, make_pair(MaxPossibleValueOfLHS, MaximumPossibleValue))); }//entry does not exist for rhs ends here }//lhs is free of variable and rhs contains variable ends here else if(MonomWithVariableOnLHS != NULL && MonomWithVariableOnRHS == NULL) //lhs is a term containing variable and rhs is free of variable { // rhs is an upper bound for lhs // Let us find the minimum possible value of rhs t_compute MinPossibleValueOfRHS; bool MinPossibleValueComputed = computeMinimumPossibleValueOfKadd_UsingMachineArithmetic(RHSOfLeqNode, p, MinPossibleValueOfRHS); if(!MinPossibleValueComputed) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! in finding minimum possible value of a term in function t_Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } // update the BoundMap using lhs and minimum possible value of rhs // check if entry already exists for lhs map >::iterator bmap_it = BoundMap.find(LHSOfLeqNode); if(bmap_it != BoundMap.end()) //entry exists for lhs { t_compute ExistingMinimumUpperBound = (bmap_it->second).second;// v_j is the first one in the pair // new v_j = min(minimum possible value of rhs, existing v_j) if(MinPossibleValueOfRHS < ExistingMinimumUpperBound) { // new v_j = minimum possible value of rhs (bmap_it->second).second = MinPossibleValueOfRHS; } }//entry exists for lhs ends here else //entry does not exist for lhs; insert a new entry { t_compute MinimumPossibleValue = 0; // insert (lhs --> (0, minimum possible value of rhs)) in BoundMap BoundMap.insert(make_pair(LHSOfLeqNode, make_pair(MinimumPossibleValue, MinPossibleValueOfRHS))); }//entry does not exist for lhs ends here }//lhs contains variable and rhs is free of variable else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! suspicious locatin reached in function t_Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; }// else ends here }// for each Inequation ends here // BoundMap i.e. the map (s_j --> (u_j, v_j)) is computed // Let's now create the vector of Kappa values of s_j, // sorted vector of Kappa values of s_j and Kappa_0, // and vector of delta values. vector KappaVector; vector DeltaVector; vector SortedKappaVector; // take each entry in BoundMap for(map >::iterator bmap_it = BoundMap.begin(); bmap_it != BoundMap.end(); bmap_it++) { // each entry is (s_j --> (u_j, v_j)) t_Expression* s_j = bmap_it->first; t_compute u_j = (bmap_it->second).first; t_compute v_j = (bmap_it->second).second; // compute Kappa_j unsigned int Kappa_j; bool KappaFound = findKappaValueOfKadd(s_j, variable, Kappa_j); if(!KappaFound) // Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa_j == UINT_MAX) //Error!! term free of variable; should not occure as we are working on bound constraints!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! constraint free of variable to be eliminated encountered in function t_Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa_j >= Kappa_0) //kappa of inequation >= kappa of equation; not possible to drop { Mu_I = 0; return true; } // insert Kappa_j into KappaVector and SortedKappaVector KappaVector.push_back(Kappa_j); SortedKappaVector.push_back(Kappa_j); // compute Delta_j t_compute Delta_j; if(v_j < u_j) // this means that Delta_j is zero, not possible to drop { Mu_I = 0; return true; } else { Delta_j = v_j - u_j + 1; } if(Delta_j >= findTwosPower_UsingMachineArithmetic(p)) // Delta_j >= 2^{p}. Trivial inequation!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Delta_j >= 2^{p} in Project::computeCombinationsPermittedByInequations_UsingMachineArithmetic. Occuring due to trivial inequations which should be avoided a-priori", pvt_logFile, c_RunLevelVerbosity); return false; } // insert Delta_j into DeltaVector DeltaVector.push_back(Delta_j); }// for each entry in BoundMap ends here SortedKappaVector.push_back(Kappa_0); // sort SortedKappaVector in the descending order sort(SortedKappaVector.rbegin(), SortedKappaVector.rend()); // remove duplicates from SortedKappaVector SortedKappaVector.erase(unique(SortedKappaVector.begin(), SortedKappaVector.end()), SortedKappaVector.end()); // Let's compute Mu_I from KappaVector, SortedKappaVector, and DeltaVector assert(SortedKappaVector.size() >= 2); Mu_I = 1; for(int i = 0; i < SortedKappaVector.size()-1; i++) { unsigned Omega_i = SortedKappaVector[i]; unsigned Omega_i_plus_1 = SortedKappaVector[i+1]; assert(Omega_i_plus_1 < Omega_i); t_compute W_i = 0; t_compute Pi_i = 0; for(int j = 0; j < KappaVector.size(); j++) { unsigned Kappa_j = KappaVector[j]; t_compute Delta_j = DeltaVector[j]; if(Kappa_j < Omega_i) { Pi_i++; assert(p+Kappa_j >= Omega_i); t_compute Y_ji = Delta_j >> (p-Omega_i+Kappa_j); // Y_ij = \lfloor(Delta_j / 2^(p-Omega_i+Kappa_j))\rfloor t_compute Alpha_ji; if(i == 0) { // Alpha_ji = min(2^{Omega_i - Omega_i_plus_1}, Y_ji); Alpha_ji = minimum(findTwosPower_UsingMachineArithmetic(Omega_i - Omega_i_plus_1), Y_ji); } else { // Alpha_ji = min(2^{Omega_i - Omega_i_plus_1}, max(Y_ji, 1)); Alpha_ji = minimum(findTwosPower_UsingMachineArithmetic(Omega_i - Omega_i_plus_1), maximum(Y_ji, 1)); } W_i = W_i + Alpha_ji; if(Pi_i > 1) { // Common ways = 2^{Omega_i - Omega_i_plus_1}; t_compute Common_i = findTwosPower_UsingMachineArithmetic(Omega_i - Omega_i_plus_1); if(W_i <= Common_i) // not possible to drop { Mu_I = 0; return true; } else { W_i = W_i - Common_i; } }// if(Pi_i > 1) ends here }// if(Kappa_j < Omega_i) ends here }// for each j ends here assert(Pi_i >= 1); Mu_I = Mu_I * W_i; }// for each i ends here unsigned Kappa_r = SortedKappaVector[SortedKappaVector.size()-1]; // the last element assert(Kappa_r < p); Mu_I = Mu_I << Kappa_r; // Mu_I = Mu_I * 2^{Kappa_r} return true; }//function ends here // Using bv-library, // finds Mu_I i.e. under-approximation of the number of valuations to the // most significant Kappa_0 bits of variable satisfying the inequations in I_neg_core_x. // Returns false in the case of errors; true otherwise. bool t_Project::computeCombinationsPermittedByInequations_UsingBVLibrary(unsigned Kappa_0, const set &I_neg_core_x, const string &variable, unsigned p, bvatom &Mu_I) { unsigned WidthOfResult = p+1; string ZeroString = getZeroBinaryStringOfGivenLength(WidthOfResult); string OneString = getOneBinaryStringOfGivenLength(WidthOfResult); // Let us create the map (s_j --> (u_j, v_j)), where s_j denotes a term // containing variable, u_j is the maximum among the lower bounds of s_j, and // v_j is the minimum among the upper bounds of s_j. map > BoundMap; // take each Inequation in I_neg_core_x for(set::iterator it = I_neg_core_x.begin(); it != I_neg_core_x.end(); it++) { t_Expression* Inequation = *it; assert(Inequation != NULL); // get the kadd nodes t_Expression* LHSOfLeqNode = getIthChild(Inequation, 0, pvt_em);// get the LHS t_Expression* RHSOfLeqNode = getIthChild(Inequation, 1, pvt_em);// get the RHS assert(LHSOfLeqNode != NULL); assert(RHSOfLeqNode != NULL); t_Expression* MonomWithVariableOnLHS; bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, pvt_em, pvt_VariableList); t_Expression* MonomWithVariableOnRHS; bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, pvt_em, pvt_VariableList); if(!LHSMonomFound || !RHSMonomFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::computeCombinationsPermittedByInequations_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariableOnLHS == NULL && MonomWithVariableOnRHS == NULL) //ERROR!!lhs is free of variable and rhs is free of variable { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! inequation free of variable to be eliminated in function t_Project::computeCombinationsPermittedByInequations_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariableOnLHS != NULL && MonomWithVariableOnRHS != NULL) //lhs contains variable and rhs contains variable: Dropping not possible { Mu_I = pvt_bvm->getBVatom(WidthOfResult, ZeroString); //Mu_I = 0 return true; } else if(MonomWithVariableOnLHS == NULL && MonomWithVariableOnRHS != NULL) //lhs is free of variable and rhs contains variable { // lhs is a lower bound for rhs // Let us find the maximum possible value of lhs bvatom MaxPossibleValueOfLHS; bool MaxPossibleValueComputed = computeMaximumPossibleValueOfKadd_UsingBVLibrary(LHSOfLeqNode, p, MaxPossibleValueOfLHS); if(!MaxPossibleValueComputed) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! in finding maximum possible value of a term in function t_Project::computeCombinationsPermittedByInequations_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } // update the BoundMap using rhs and maximum possible value of lhs // check if entry already exists for rhs map >::iterator bmap_it = BoundMap.find(RHSOfLeqNode); if(bmap_it != BoundMap.end()) //entry exists for rhs { bvatom ExistingMaximumLowerBound = (bmap_it->second).first; // new u_j = max(maximum possible value of lhs, existing u_j) if(pvt_bvm->checkBVGreaterThan(MaxPossibleValueOfLHS, ExistingMaximumLowerBound)) { // new u_j = maximum possible value of lhs (bmap_it->second).first = MaxPossibleValueOfLHS; } }//entry exists for rhs ends here else //entry does not exist for rhs; insert a new entry { bvatom MaximumPossibleValue = pvt_bvm->bvsub(findTwosPower_UsingBVLibrary(WidthOfResult, p), pvt_bvm->getBVatom(WidthOfResult, OneString)); //2^{p}-1 // insert (rhs --> (maximum possible value of lhs, 2^{p}-1)) in BoundMap BoundMap.insert(make_pair(RHSOfLeqNode, make_pair(MaxPossibleValueOfLHS, MaximumPossibleValue))); }//entry does not exist for rhs ends here }//lhs is free of variable and rhs contains variable ends here else if(MonomWithVariableOnLHS != NULL && MonomWithVariableOnRHS == NULL) //lhs contains variable and rhs is free of variable { // rhs is an upper bound for lhs // Let us find the minimum possible value of rhs bvatom MinPossibleValueOfRHS; bool MinPossibleValueComputed = computeMinimumPossibleValueOfKadd_UsingBVLibrary(RHSOfLeqNode, p, MinPossibleValueOfRHS); if(!MinPossibleValueComputed) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! in finding minimum possible value of a term in function t_Project::computeCombinationsPermittedByInequations_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } // update the BoundMap using lhs and minimum possible value of rhs // check if entry already exists for lhs map >::iterator bmap_it = BoundMap.find(LHSOfLeqNode); if(bmap_it != BoundMap.end()) //entry exists for lhs { bvatom ExistingMinimumUpperBound = (bmap_it->second).second; // new v_j = min(minimum possible value of rhs, existing v_j) if(pvt_bvm->checkBVGreaterThan(ExistingMinimumUpperBound, MinPossibleValueOfRHS)) { // new v_j = minimum possible value of rhs (bmap_it->second).second = MinPossibleValueOfRHS; } }//entry exists for lhs ends here else //entry does not exist for lhs; insert a new entry { bvatom MinimumPossibleValue = pvt_bvm->getBVatom(WidthOfResult, ZeroString); // insert (lhs --> (0, minimum possible value of rhs)) in BoundMap BoundMap.insert(make_pair(LHSOfLeqNode, make_pair(MinimumPossibleValue, MinPossibleValueOfRHS))); }//entry does not exist for lhs ends here }//lhs contains variable and rhs is free of variable else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! suspicious locatin reached in function t_Project::computeCombinationsPermittedByInequations_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; }// else ends here }// for each Inequation ends here // BoundMap i.e. the map (s_j --> (u_j, v_j)) is computed // Let's now create the vector of Kappa values, sorted vector of Kappa values, and vector of delta values vector KappaVector; vector DeltaVector; vector SortedKappaVector; // take each entry in BoundMap for(map >::iterator bmap_it = BoundMap.begin(); bmap_it != BoundMap.end(); bmap_it++) { // each entry is (s_j --> (u_j, v_j)) t_Expression* s_j = bmap_it->first; bvatom u_j = (bmap_it->second).first; bvatom v_j = (bmap_it->second).second; // compute Kappa_j unsigned int Kappa_j; bool KappaFound = findKappaValueOfKadd(s_j, variable, Kappa_j); if(!KappaFound) // Error!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kappa finding error in function t_Project::computeCombinationsPermittedByInequations_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa_j == UINT_MAX) //Error!! term free of variable; should not occure as we are working on bound constraints!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! constraint free of variable to be eliminated encountered in function t_Project::computeCombinationsPermittedByInequations_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else if(Kappa_j >= Kappa_0) //kappa of inequation >= kappa of equation; not possible to drop { Mu_I = pvt_bvm->getBVatom(WidthOfResult, ZeroString); //Mu_I = 0 return true; } // insert Kappa_j into KappaVector and SortedKappaVector KappaVector.push_back(Kappa_j); SortedKappaVector.push_back(Kappa_j); // compute Delta_j bvatom Delta_j; if(pvt_bvm->checkBVGreaterThan(u_j, v_j)) // this means that Delta_j is zero, not possible to drop { Mu_I = pvt_bvm->getBVatom(WidthOfResult, ZeroString); // Mu_I = 0 return true; } else { Delta_j = pvt_bvm->bvadd(pvt_bvm->bvsub(v_j, u_j), pvt_bvm->getBVatom(WidthOfResult, OneString)); } if(!(pvt_bvm->checkBVGreaterThan(findTwosPower_UsingBVLibrary(WidthOfResult, p), Delta_j))) // ~(2^{p} > Delta_j) i.e. (2^{p} <= Delta_j) Trivial inequation!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Delta_j >= 2^{p} in Project::computeCombinationsPermittedByInequations_UsingBVLibrary. Occuring due to trivial inequations which should be avoided a-priori", pvt_logFile, c_RunLevelVerbosity); return false; } // insert Delta_j into DeltaVector DeltaVector.push_back(Delta_j); }// for each entry in BoundMap ends here SortedKappaVector.push_back(Kappa_0); // sort SortedKappaVector in the descending order sort(SortedKappaVector.rbegin(), SortedKappaVector.rend()); // remove duplicates from SortedKappaVector SortedKappaVector.erase(unique(SortedKappaVector.begin(), SortedKappaVector.end()), SortedKappaVector.end()); // Let's compute Mu_I from KappaVector, SortedKappaVector, and DeltaVector assert(SortedKappaVector.size() >= 2); Mu_I = pvt_bvm->getBVatom(WidthOfResult, OneString); //Mu_I = 1 for(int i = 0; i < SortedKappaVector.size()-1; i++) { unsigned Omega_i = SortedKappaVector[i]; unsigned Omega_i_plus_1 = SortedKappaVector[i+1]; assert(Omega_i_plus_1 < Omega_i); bvatom W_i = pvt_bvm->getBVatom(WidthOfResult, ZeroString); //W_i = 0 t_compute Pi_i = 0; for(int j = 0; j < KappaVector.size(); j++) { unsigned Kappa_j = KappaVector[j]; bvatom Delta_j = DeltaVector[j]; if(Kappa_j < Omega_i) { Pi_i++; assert(p+Kappa_j >= Omega_i); bvatom Y_ji = pvt_bvm->bvrshift(Delta_j, p-Omega_i+Kappa_j); // Y_ij = \lfloor(Delta_j / 2^(p-Omega_i+Kappa_j))\rfloor bvatom Alpha_ji; if(i == 0) { // Alpha_ji = min(2^{Omega_i - Omega_i_plus_1}, Y_ji); Alpha_ji = minimum(findTwosPower_UsingBVLibrary(WidthOfResult, Omega_i - Omega_i_plus_1), Y_ji); } else { // Alpha_ji = min(2^{Omega_i - Omega_i_plus_1}, max(Y_ji, 1)); Alpha_ji = minimum(findTwosPower_UsingBVLibrary(WidthOfResult, Omega_i - Omega_i_plus_1), maximum(Y_ji, pvt_bvm->getBVatom(WidthOfResult, OneString))); } W_i = pvt_bvm->bvadd(W_i, Alpha_ji); if(Pi_i > 1) { // Common ways = 2^{Omega_i - Omega_i_plus_1}; bvatom Common_i = findTwosPower_UsingBVLibrary(WidthOfResult, Omega_i - Omega_i_plus_1); if(!(pvt_bvm->checkBVGreaterThan(W_i, Common_i))) // W_i <= Common_i; no: of ways <= 0; not possible to extend { Mu_I = pvt_bvm->getBVatom(WidthOfResult, ZeroString); //Mu_I = 0 return true; } else // W_i > Common_i { W_i = pvt_bvm->bvsub(W_i, Common_i); } }// if(Pi_i > 1) ends here }// if(Kappa_j < Omega_i) ends here }// for each j ends here assert(Pi_i >= 1); Mu_I = pvt_bvm->bvmul(Mu_I, W_i); }// for each i ends here unsigned Kappa_r = SortedKappaVector[SortedKappaVector.size()-1]; // the last element assert(Kappa_r < p); Mu_I = pvt_bvm->bvlshift(Mu_I, Kappa_r); // Mu_I = Mu_I * 2^{Kappa_r} return true; }//function ends here // Using machine arithmetic, // finds the maximum possible value a term (kaddNode) can take. // If the term is a constant, then the maximum possible value is the constant. // Otherwise, if the term can be expressed as 2^{Tau}.t, where Tau \in \{0,...,p-1}, // then the maximum possible value is 2^{p} - 2^{Tau}. // Returns false in case of errors; true otherwise. bool t_Project::computeMaximumPossibleValueOfKadd_UsingMachineArithmetic(t_Expression* kaddNode, unsigned int p, t_compute &MaxPossibleValue) { if(kaddNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode is NULL in function t_Project::computeMaximumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::computeMaximumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(kaddNode); if(Children.size() == 0) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode with no children in function t_Project::computeMaximumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else { assert(Children[0] != NULL); int index = 0; unsigned Tau = UINT_MAX; if(isBVConstant(Children[0], pvt_em)) //first child is constant { if(Children.size() == 1) //we have only one child which is a constant; max. value = constant { string Constant_str = pvt_em->getLabelOfExpression(Children[0]); // Constant_str is a (zero-padded) binary string starting with "0b"; // we need characters from position 2 to end Constant_str = Constant_str.substr(2); t_compute Constant = binaryStringToULLInteger(Constant_str); // set MaxPossibleValue to the constant MaxPossibleValue = Constant; return true; } else // we have other children also { // we need to compute Tau string Constant_str = pvt_em->getLabelOfExpression(Children[0]); // Constant_str is a (zero-padded) binary string starting with "0b"; // we need characters from position 2 to end Constant_str = Constant_str.substr(2); bvatom Constant = pvt_bvm->getBVatom(Constant_str.size(), Constant_str); // find Kappa of constant part unsigned Kappa; bool KappaFound = pvt_bvm->findKappa(Constant, Kappa); if(!KappaFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while computing kappa in function t_Project::computeMaximumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } Tau = (Kappa < Tau) ? Kappa : Tau; index++; }// we have other children also ends here }//first child is constant ends here for(; index < Children.size(); index++) { t_Expression* Child = Children[index]; assert(Child != NULL); // find the variable of monom string VariableOfMonom; bool VariableFound = findVariableOfMonom(Child, VariableOfMonom, pvt_em); if(!VariableFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while finding variable in function t_Project::computeMaximumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } // find kappa of monom unsigned Kappa; bool KappaFound = findKappaValueOfMonom(Child, VariableOfMonom, Kappa); if(!KappaFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while computing kappa in function t_Project::computeMaximumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } Tau = (Kappa < Tau) ? Kappa : Tau; }// for each child loop ends here assert(Tau < p); // MaxPossibleValue = 2^{p} - 2^{Tau} MaxPossibleValue = findTwosPower_UsingMachineArithmetic(p) - findTwosPower_UsingMachineArithmetic(Tau); return true; }// else of if(Children.size() == 0) ends here }// else of else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) ends here }// function ends here // Using bv-library, // finds the maximum possible value a term (kaddNode) can take. // If the term is a constant, then the maximum possible value is the constant. // Otherwise, if the term can be expressed as 2^{Tau}.t, where Tau \in \{0,...,p-1}, // then the maximum possible value is 2^{p} - 2^{Tau}. // Returns false in case of errors; true otherwise. bool t_Project::computeMaximumPossibleValueOfKadd_UsingBVLibrary(t_Expression* kaddNode, unsigned int p, bvatom &MaxPossibleValue) { if(kaddNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode is NULL in function t_Project::computeMaximumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::computeMaximumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(kaddNode); if(Children.size() == 0) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode with no children in function t_Project::computeMaximumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else { assert(Children[0] != NULL); int index = 0; unsigned Tau = UINT_MAX; unsigned WidthOfResult = p+1; if(isBVConstant(Children[0], pvt_em)) //first child is constant { if(Children.size() == 1) //we have only one child which is a constant; max. value = constant { string Constant_str = pvt_em->getLabelOfExpression(Children[0]); // Constant_str is a (zero-padded) binary string starting with "0b"; // we need characters from position 2 to end Constant_str = Constant_str.substr(2); // Constant_str has width = p string Constant_str_Proper_width = "0"; Constant_str_Proper_width += Constant_str; // Constant_str_Proper_width has width = p+1 bvatom Constant = pvt_bvm->getBVatom(WidthOfResult, Constant_str_Proper_width); // set MaxPossibleValue to the constant MaxPossibleValue = Constant; return true; } else // we have other children also { // we need to compute Tau string Constant_str = pvt_em->getLabelOfExpression(Children[0]); // Constant_str is a (zero-padded) binary string starting with "0b"; // we need characters from position 2 to end Constant_str = Constant_str.substr(2); // Constant_str has width = p string Constant_str_Proper_width = "0"; Constant_str_Proper_width += Constant_str; // Constant_str_Proper_width has width = p+1 bvatom Constant = pvt_bvm->getBVatom(WidthOfResult, Constant_str_Proper_width); // find Kappa of constant part unsigned Kappa; bool KappaFound = pvt_bvm->findKappa(Constant, Kappa); if(!KappaFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while computing kappa in function t_Project::computeMaximumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } Tau = (Kappa < Tau) ? Kappa : Tau; index++; }// we have other children also ends here }//first child is constant ends here for(; index < Children.size(); index++) { t_Expression* Child = Children[index]; assert(Child != NULL); // find the variable of monom string VariableOfMonom; bool VariableFound = findVariableOfMonom(Child, VariableOfMonom, pvt_em); if(!VariableFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while finding variable in function t_Project::computeMaximumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } // find kappa of monom unsigned Kappa; bool KappaFound = findKappaValueOfMonom(Child, VariableOfMonom, Kappa); if(!KappaFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while computing kappa in function t_Project::computeMaximumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } Tau = (Kappa < Tau) ? Kappa : Tau; }// for each child loop ends here assert(Tau < p); // MaxPossibleValue = 2^{p} - 2^{Tau} MaxPossibleValue = pvt_bvm->bvsub(findTwosPower_UsingBVLibrary(WidthOfResult, p), findTwosPower_UsingBVLibrary(WidthOfResult, Tau)); return true; }// else of if(Children.size() == 0) ends here }// else of else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) ends here }// function ends here // Using machine arithmetic, // finds the minimum possible value a term (kaddNode) can take. // If the term is a constant, then the minimum possible value is the constant. // Otherwise, if the term can be expressed as 2^{Tau}.t + Constant, // where Tau \in \{0,...,p-1}, then the minimum possible value is Constant mod 2^{Tau}. // Returns false in case of errors; true otherwise. bool t_Project::computeMinimumPossibleValueOfKadd_UsingMachineArithmetic(t_Expression* kaddNode, unsigned int p, t_compute &MinPossibleValue) { if(kaddNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode is NULL in function t_Project::computeMinimumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::computeMinimumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(kaddNode); if(Children.size() == 0) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode with no children in function t_Project::computeMinimumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } else { assert(Children[0] != NULL); int index = 0; unsigned Tau = UINT_MAX; t_compute Constant = 0; if(isBVConstant(Children[0], pvt_em)) //first child is constant { string Constant_str = pvt_em->getLabelOfExpression(Children[0]); // Constant_str is a (zero-padded) binary string starting with "0b"; // we need characters from position 2 to end Constant_str = Constant_str.substr(2); Constant = binaryStringToULLInteger(Constant_str); if(Children.size() == 1) //we have only one child - the constant; min. value = constant { // set MinPossibleValue to the constant MinPossibleValue = Constant; return true; } else // we have other children also { index++; }// we have other children also ends here }//first child is constant ends here if(Constant == 0) //Constant = 0. Hence Constant mod 2^{Tau} = 0; no need to compute Tau. { MinPossibleValue = 0; return true; } for(; index < Children.size(); index++) { t_Expression* Child = Children[index]; assert(Child != NULL); // find the variable of monom string VariableOfMonom; bool VariableFound = findVariableOfMonom(Child, VariableOfMonom, pvt_em); if(!VariableFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while finding variable in function t_Project::computeMinimumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } // find kappa of monom unsigned Kappa; bool KappaFound = findKappaValueOfMonom(Child, VariableOfMonom, Kappa); if(!KappaFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while computing kappa in function t_Project::computeMinimumPossibleValueOfKadd_UsingMachineArithmetic", pvt_logFile, c_RunLevelVerbosity); return false; } Tau = (Kappa < Tau) ? Kappa : Tau; }// for each child loop ends here assert(Tau < p); // MinPossibleValue = Constant % 2^{Tau} MinPossibleValue = Constant % findTwosPower_UsingMachineArithmetic(Tau); return true; }// else of if(Children.size() == 0) ends here }// else of else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) ends here }// function ends here // Using bv-library, // finds the minimum possible value a term (kaddNode) can take. // If the term is a constant, then the minimum possible value is the constant. // Otherwise, if the term can be expressed as 2^{Tau}.t + Constant, // where Tau \in \{0,...,p-1}, then the minimum possible value is Constant mod 2^{Tau}. // Returns false in case of errors; true otherwise. bool t_Project::computeMinimumPossibleValueOfKadd_UsingBVLibrary(t_Expression* kaddNode, unsigned int p, bvatom &MinPossibleValue) { if(kaddNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode is NULL in function t_Project::computeMinimumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::computeMinimumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else { vector Children = pvt_em->getVectorOfOperands(kaddNode); if(Children.size() == 0) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kaddNode with no children in function t_Project::computeMinimumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } else { assert(Children[0] != NULL); int index = 0; unsigned Tau = UINT_MAX; unsigned WidthOfResult = p+1; string ZeroString = getZeroBinaryStringOfGivenLength(WidthOfResult); bvatom Constant = pvt_bvm->getBVatom(WidthOfResult, ZeroString); // Constant = 0 if(isBVConstant(Children[0], pvt_em)) //first child is constant { string Constant_str = pvt_em->getLabelOfExpression(Children[0]); // Constant_str is a (zero-padded) binary string starting with "0b"; // we need characters from position 2 to end Constant_str = Constant_str.substr(2); // Constant_str has width = p string Constant_str_Proper_width = "0"; Constant_str_Proper_width += Constant_str; // Constant_str_Proper_width has width = p+1 Constant = pvt_bvm->getBVatom(WidthOfResult, Constant_str_Proper_width); if(Children.size() == 1) //we have only one child - the constant; min. value = constant { // set MinPossibleValue to the constant MinPossibleValue = Constant; return true; } else // we have other children also { index++; }// we have other children also ends here }//first child is constant ends here if(pvt_bvm->checkBVForZero(Constant)) //Constant = 0. Hence Constant mod 2^{Tau} = 0; no need to compute Tau. { MinPossibleValue = Constant; return true; } for(; index < Children.size(); index++) { t_Expression* Child = Children[index]; assert(Child != NULL); // find the variable of monom string VariableOfMonom; bool VariableFound = findVariableOfMonom(Child, VariableOfMonom, pvt_em); if(!VariableFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while finding variable in function t_Project::computeMinimumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } // find kappa of monom unsigned Kappa; bool KappaFound = findKappaValueOfMonom(Child, VariableOfMonom, Kappa); if(!KappaFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error while computing kappa in function t_Project::computeMinimumPossibleValueOfKadd_UsingBVLibrary", pvt_logFile, c_RunLevelVerbosity); return false; } Tau = (Kappa < Tau) ? Kappa : Tau; }// for each child loop ends here assert(Tau < p); // MinPossibleValue = Constant % 2^{Tau} MinPossibleValue = pvt_bvm->bvmod(Constant, findTwosPower_UsingBVLibrary(WidthOfResult, Tau)); return true; }// else of if(Children.size() == 0) ends here }// else of else if("kadd" != pvt_em->getLabelOfExpression(kaddNode)) ends here }// function ends here // Find min among two t_compute values t_compute t_Project::minimum(t_compute a, t_compute b) { return (a > b) ? b : a; } // Find min among two bvatoms bvatom t_Project::minimum(bvatom a, bvatom b) { return (pvt_bvm->checkBVGreaterThan(a, b)) ? b : a; } // Find max among two t_compute values t_compute t_Project::maximum(t_compute a, t_compute b) { return (a > b) ? a : b; } // Find max among two bvatoms bvatom t_Project::maximum(bvatom a, bvatom b) { return (pvt_bvm->checkBVGreaterThan(a, b)) ? a : b; } // displays bound map on screen bool t_Project::displayBoundMapOnScreen(map > &BoundMap) { for(map >::iterator it = BoundMap.begin(); it != BoundMap.end(); it++) { cout<printExpressionToFileAsDAG("s_j ", it->first, cout); cout<<"\nu_j = "<<(it->second).first<<"\nv_j = "<<(it->second).second< > &BoundMap) { for(map >::iterator it = BoundMap.begin(); it != BoundMap.end(); it++) { cout<printExpressionToFileAsDAG("s_j ", it->first, cout); cout<<"\nu_j = "<printBVasBinString((it->second).first)<<"\nv_j = "<printBVasBinString((it->second).second)<getLabelOfExpression(Inequation)); // get the kadd nodes t_Expression* LHSOfLeqNode = getIthChild(Inequation, 0, pvt_em);// get the first child t_Expression* RHSOfLeqNode = getIthChild(Inequation, 1, pvt_em);// get the second child assert(LHSOfLeqNode != NULL); assert(RHSOfLeqNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHSOfLeqNode)); assert("kadd" == pvt_em->getLabelOfExpression(RHSOfLeqNode)); t_side_of_variable_in_unification side_of_variable; t_Expression* MonomWithVariableOnLHS; bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, pvt_em, pvt_VariableList); assert(LHSMonomFound); if(MonomWithVariableOnLHS != NULL) //lhs contains variable { t_Expression* MonomWithVariableOnRHS; bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, pvt_em, pvt_VariableList); assert(RHSMonomFound); if(MonomWithVariableOnRHS != NULL) //rhs also contains variable { side_of_variable = BOTH; } else // rhs free of variable { side_of_variable = LEFT; } } else //lhs is free of variable { t_Expression* MonomWithVariableOnRHS; bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, pvt_em, pvt_VariableList); assert(RHSMonomFound); if(MonomWithVariableOnRHS != NULL) //rhs contains variable { side_of_variable = RIGHT; } else // rhs free of variable { side_of_variable = NONE; } }//lhs is free of variable ends here return side_of_variable; } // Checks if (InputKandNode, variables) is existing in pvt_Layer3_HashTable. // Returns the result if existing; NULL otherwise. t_Expression* t_Project::checkIn_Layer3_HashTable(t_Expression* InputKandNode, const vector &variables) { assert(InputKandNode != NULL); // key = address of input kand node + variables to be eliminated string key = toString(InputKandNode); int var_size = variables.size(); for(int i = 0; i < var_size; i++) { key += variables[i]; } t_HTStatusValue result_search = pvt_Layer3_HashTable.hashtable_search(key); if(result_search.success()) { return result_search.getValue(); } else { return NULL; } }//function ends here // Updates pvt_Layer3_HashTable with (InputKandNode, variables) ---> OutputKandNode. // Returns false in case of errors; true otherwise. bool t_Project::update_Layer3_HashTable(t_Expression* InputKandNode, const vector &variables, t_Expression* OutputKandNode) { assert(InputKandNode != NULL); assert(OutputKandNode != NULL); // key = address of input kand node + variables to be eliminated string key = toString(InputKandNode); int var_size = variables.size(); for(int i = 0; i < var_size; i++) { key += variables[i]; } t_HTStatusValue insert_result = pvt_Layer3_HashTable.hashtable_insert(key, OutputKandNode); if (insert_result.success()) { return true; } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in hash table insertion in function t_Project::update_Layer3_HashTable", pvt_logFile, c_RunLevelVerbosity); return false; } }//function ends here // Given a "kand" node, this function applies layer3 for eliminating multiple // variables. Returns NULL in case of errors, true node if the result is true, // and an equivalent Boolean combination otherwise. // IMPORTANT: The core algorithms in layer3 works on LMIs. Hence the LMEs and LMDs // present in the kandNode are converted to LMIs before the core algorithms are applied. t_Expression* t_Project::Layer3(t_Expression* kandNode, const vector &variables) { if(kandNode == NULL) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! kandNode is NULL in function t_Project::Layer3", pvt_logFile, c_RunLevelVerbosity); return NULL; } else if("kand" != pvt_em->getLabelOfExpression(kandNode)) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected node encountered in function t_Project::Layer3", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { // check in hash table first t_Expression* ResultFromHashTable = checkIn_Layer3_HashTable(kandNode, variables); if(ResultFromHashTable != NULL) //hash table hit { // for debugging cout<<"\nHash hit in layer3\n"; // for debugging ends here return ResultFromHashTable; } else //hash table miss { // for debugging cout<<"\nHash miss in layer3\n"; // for debugging ends here t_Expression* ResultOfLayer3; set E, D, I; // Recall that kandNode is a conjunction of equations, disequations, and inequations. // Obtain the equations in E, disequations in D, and inequations in I. bool ConstraintsFound = findConstraintsFromKandNode(kandNode, E, D, I, pvt_em); assert(ConstraintsFound); assert(!(E.empty() && D.empty() && I.empty())); // We need to compute exists X.(E \wedge D \wedge I) // The core algorithms in layer3 works on inequations. // Hence, let us convert the equations and disequations to inequations. // Let us convert the equations in E to inequations, and put them in I for(set::iterator E_it = E.begin(); E_it != E.end(); E_it++) { t_Expression* equation = *E_it; assert(equation != NULL); t_Expression* inequation_from_equation = obtainEquivalentLeqNodeFromEqzNode(equation, pvt_em, pvt_bvm, pvt_VariableList); assert(inequation_from_equation != NULL); I.insert(inequation_from_equation); } // Let us convert the disequations in D to inequations, and put them in I for(set::iterator D_it = D.begin(); D_it != D.end(); D_it++) { t_Expression* disequation = *D_it; assert(disequation != NULL); t_Expression* inequation_from_disequation = obtainEquivalentLeqNodeFromDiseqzNode(disequation, pvt_em, pvt_bvm, pvt_VariableList); assert(inequation_from_disequation != NULL); I.insert(inequation_from_disequation); } // We need to compute exists X.(I) set VariablesToElimWhichNeedUnification; set VariablesEliminated; t_Expression* ResultOfLoop; bool ResultOfLoopConjunctive = true; int var_size = variables.size(); for(int i = 0; i < var_size; i++) // take each variable to eliminate { string variable = variables[i]; // for debugging cout<<"\nvariable = "< E_x, E_neg_x; // temporary variables for the function call set D_x, D_neg_x; // temporary variables for the function call set I_x, I_neg_x; // Obtain the inequations with variable in I_x, inequations without variable in I_neg_x bool FreeAndBoundConstraintsFound = findFreeAndBoundConstraintsFromSet(I, variable, E_x, D_x, I_x, E_neg_x, D_neg_x, I_neg_x, pvt_em, pvt_VariableList); assert(FreeAndBoundConstraintsFound); assert(E_x.empty() && D_x.empty() && E_neg_x.empty() && D_neg_x.empty()); // I \equiv (I_x \wedge I_neg_x) // Recall that we need to find exists X.I // Now, exists X.I \equiv ((exists x.I_x) \wedge (exists X\{x}.I_neg_x)) // for debugging displaySetOfExpressionsOnScreen("I_x", I_x, pvt_em); displaySetOfExpressionsOnScreen("I_neg_x", I_neg_x, pvt_em); // for debugging ends here // computing exists x.(I_x) if(I_x.empty()) // We have I = I_neg_x // exists x.(I_x) \equiv true // exists X.(I) \equiv exists X\{x}.(I_neg_x) { // for debugging cout<<"\nI_x is empty, i.e. "< Inequations_From_FM; bool FourierMotzkinDone = standardFourierMotzkin(I_x, variable, Inequations_From_FM); assert(FourierMotzkinDone); // for debugging displaySetOfExpressionsOnScreen("Inequations_From_FM", Inequations_From_FM, pvt_em); // for debugging ends here // exists x.(I_x) is the conjunction of LMCs in Inequations_From_FM // exists X.(I) \equiv exists X\{x}.(Inequations_From_FM \union I_neg_x) // Hence we need I = Inequations_From_FM \union I_neg_x I.clear(); set_union(Inequations_From_FM.begin(), Inequations_From_FM.end(), I_neg_x.begin(), I_neg_x.end(), inserter(I, I.begin())); VariablesEliminated.insert(variable); } else // exists x.(I_x) can be found using modified Fourier-Motzkin // result of modified Fourier-Motzkin is NOT NECCESSARILY a conjunction of LMCs { // for debugging cout<<"\nKappa_Of_I_x == " << Kappa_Of_I_x << "; calling modifiedFourierMotzkin to compute exists x. I_x\n"; // for debugging ends here set Constraints_From_FM; bool FourierMotzkinDone = modifiedFourierMotzkin(I_x, variable, Kappa_Of_I_x, Constraints_From_FM, ResultOfLoopConjunctive); assert(FourierMotzkinDone); // for debugging displaySetOfExpressionsOnScreen("Constraints_From_FM", Constraints_From_FM, pvt_em); // for debugging ends here // let's see if the result of modified Fourier-Motzkin is conjunction of LMCs if(ResultOfLoopConjunctive) { // for debugging cout<<"\nResult of loop is conjunctive\n"; // for debugging ends here // exists x.(I_x) is the conjunction of LMCs in Constraints_From_FM // exists X.(I) \equiv exists X\{x}.(Constraints_From_FM \union I_neg_x) // Hence we need I = Constraints_From_FM \union I_neg_x I.clear(); set_union(Constraints_From_FM.begin(), Constraints_From_FM.end(), I_neg_x.begin(), I_neg_x.end(), inserter(I, I.begin())); VariablesEliminated.insert(variable); } else { // for debugging cout<<"\nResult of loop is not conjunctive\n"; // for debugging ends here // exists x.(I_x) is the conjunction of constraints in Constraints_From_FM; // Also each constraint in Constraints_From_FM is a disjunction of kand node. // Let us go out of this loop, as this loop assumes that // the result of exists x.(I_x) is a conjunction of LMCs. // exists X.(I) \equiv exists X\{x}.(LOGAND(LOGAND(Constraints_From_FM), KAND(I_neg_x))) // Hence we need ResultOfLoop = LOGAND(LOGAND(Constraints_From_FM), KAND(I_neg_x)) if(Constraints_From_FM.empty()) { if(I_neg_x.empty()) { ResultOfLoop = getTrue(pvt_em); assert(ResultOfLoop != NULL); } else { set TempEqzChildren;//temporary variable for the function set TempDiseqzChildren;//temporary variable for the function ResultOfLoop = CreateKandNode(TempEqzChildren, TempDiseqzChildren, I_neg_x, pvt_em); assert(ResultOfLoop != NULL); } } else { if(I_neg_x.empty()) { vector Constraints_From_FM_Vector(Constraints_From_FM.begin(), Constraints_From_FM.end()); if(Constraints_From_FM_Vector.size() == 1) { ResultOfLoop = Constraints_From_FM_Vector[0]; } else { string node_name = "logand"; ResultOfLoop = CreateNode(node_name, Constraints_From_FM_Vector, pvt_em); } assert(ResultOfLoop != NULL); } else { set TempEqzChildren;//temporary variable for the function set TempDiseqzChildren;//temporary variable for the function ResultOfLoop = CreateKandNode(TempEqzChildren, TempDiseqzChildren, I_neg_x, pvt_em); vector Constraints_From_FM_Vector(Constraints_From_FM.begin(), Constraints_From_FM.end()); if(Constraints_From_FM_Vector.size() == 1) { assert(ResultOfLoop != NULL); assert(Constraints_From_FM_Vector[0] != NULL); // conjoin ResultOfLoop with Constraints_From_FM_Vector[0] if(isTrue(ResultOfLoop, pvt_em)) { ResultOfLoop = Constraints_From_FM_Vector[0]; } else { if(!isTrue(Constraints_From_FM_Vector[0], pvt_em)) { string node_name = "logand"; ResultOfLoop = CreateNode(node_name, ResultOfLoop, Constraints_From_FM_Vector[0], pvt_em); } } }// if(Constraints_From_FM_Vector.size() == 1) ends here else { string node_name = "logand"; t_Expression* FMPartOfResult = CreateNode(node_name, Constraints_From_FM_Vector, pvt_em); assert(ResultOfLoop != NULL); assert(FMPartOfResult != NULL); // conjoin ResultOfLoop with FMPartOfResult if(isTrue(ResultOfLoop, pvt_em)) { ResultOfLoop = FMPartOfResult; } else { if(!isTrue(FMPartOfResult, pvt_em)) { string node_name = "logand"; ResultOfLoop = CreateNode(node_name, ResultOfLoop, FMPartOfResult, pvt_em); } } }// else of if(Constraints_From_FM_Vector.size() == 1) ends here assert(ResultOfLoop != NULL); } } // ResultOfLoop found // for debugging pvt_em->printExpressionToFileAsDAG("ResultOfLoop ", ResultOfLoop, cout); // for debugging ends here VariablesEliminated.insert(variable); break; }// result of modified Fourier-Motzkin is NOT a conjunction of LMCs ends here }// exists x.(I_x) can be found using modified Fourier-Motzkin ends here }//constraints involving the variable are already in unified form ends here else //constraints involving the variable are not in unified form // we need to convert them to unified form { // for debugging cout<<"\nconstraints in I_x are not in unified form; " << variable << "inserted into set VariablesToElimWhichNeedUnification\n"; // for debugging ends here VariablesToElimWhichNeedUnification.insert(variable); } }//I_x is non-empty ends here }//for ends here set VariablesStillToEliminate; set_difference(variables.begin(), variables.end(), VariablesEliminated.begin(), VariablesEliminated.end(),inserter(VariablesStillToEliminate, VariablesStillToEliminate.begin())); // for debugging displaySetOfStringsOnScreen("VariablesStillToEliminate", VariablesStillToEliminate); // for debugging ends here if(!ResultOfLoopConjunctive)// We have jumped out from the loop, as the result is no more a conjunction of LMCs. { // for debugging cout<<"\nResult of loop is not conjunctive\n"; // for debugging ends here //We need to compute ResultOfLayer3 = \exists VariablesStillToEliminate.(ResultOfLoop) if(VariablesStillToEliminate.empty() || isTrue(ResultOfLoop, pvt_em)) { // for debugging cout<<"\nNo more variables to eliminate\n"; // for debugging ends here ResultOfLayer3 = ResultOfLoop; assert(ResultOfLayer3 != NULL); } else { string ResultOfLoopLabel = pvt_em->getLabelOfExpression(ResultOfLoop); assert("kand" == ResultOfLoopLabel || "eqz" == ResultOfLoopLabel || "diseqz" == ResultOfLoopLabel || "leq" == ResultOfLoopLabel || "logand" == ResultOfLoopLabel || "logor" == ResultOfLoopLabel || "lognot" == ResultOfLoopLabel); if("kand" == ResultOfLoopLabel) { // for debugging cout<<"\nCalling Project to eliminate the remaining variables\n"; // for debugging ends here vector VariablesStillToEliminate_Vector(VariablesStillToEliminate.begin(), VariablesStillToEliminate.end()); ResultOfLayer3 = Project(ResultOfLoop, VariablesStillToEliminate_Vector); assert(ResultOfLayer3 != NULL); } else if("eqz" == ResultOfLoopLabel || "diseqz" == ResultOfLoopLabel || "leq" == ResultOfLoopLabel) { // for debugging cout<<"\nCalling Project to eliminate the remaining variables\n"; // for debugging ends here vector VariablesStillToEliminate_Vector(VariablesStillToEliminate.begin(), VariablesStillToEliminate.end()); set LoopConstraints; LoopConstraints.insert(ResultOfLoop); t_Expression* ConjunctionOfLoopConstraints = obtainKandNodeFromASetOfConstraints(LoopConstraints, pvt_em, pvt_bvm, pvt_VariableList, pvt_WidthTable); assert(ConjunctionOfLoopConstraints != NULL); ResultOfLayer3 = Project(ConjunctionOfLoopConstraints, VariablesStillToEliminate_Vector); assert(ResultOfLayer3 != NULL); } else if("logand" == ResultOfLoopLabel || "logor" == ResultOfLoopLabel || "lognot" == ResultOfLoopLabel) { // for debugging cout<<"\nCalling Monniaux to eliminate the remaining variables\n"; // for debugging ends here vector VariablesStillToEliminate_Vector(VariablesStillToEliminate.begin(), VariablesStillToEliminate.end()); t_Monniaux* Monniaux_Instance = t_Monniaux::getInstance(pvt_VariableList, pvt_WidthTable, pvt_use_bvlibrary_for_layer2_computations, pvt_em, pvt_bvm); assert(Monniaux_Instance != NULL); t_solver solver = stp; ResultOfLayer3 = Monniaux_Instance->Monniaux(ResultOfLoop, VariablesStillToEliminate_Vector, solver); assert(ResultOfLayer3 != NULL); } } // for debugging pvt_em->printExpressionToFileAsDAG("ResultOfLayer3 ", ResultOfLayer3, cout); // for debugging ends here } else { // for debugging cout<<"\nResult of loop is conjunctive\n"; // for debugging ends here //We need to compute ResultOfLayer3 = \exists VariablesStillToEliminate.(I) // Obtain the inequations with any variable in VariablesStillToEliminate in I_X, // inequations without variable in VariablesStillToEliminate in I_neg_X set E_X, E_neg_X; // temporary variables for the function call set D_X, D_neg_X; // temporary variables for the function call set I_X, I_neg_X; bool FreeAndBoundConstraintsFound = findFreeAndBoundConstraintsFromSetForMultipleVariables(I, VariablesStillToEliminate, E_X, D_X, I_X, E_neg_X, D_neg_X, I_neg_X, pvt_em); // I \equiv (I_X \wedge I_neg_X) // \exists X.I \equiv ((\exists X.(I_X) \wedge I_neg_X) assert(FreeAndBoundConstraintsFound); assert(E_X.empty() && D_X.empty() && E_neg_X.empty() && D_neg_X.empty()); if(VariablesStillToEliminate.empty() || I_X.empty()) { // for debugging cout<<"\nNo more variables to eliminate\n"; // for debugging ends here // exists X.I \equiv I_neg_X if(I_neg_X.empty()) { ResultOfLayer3 = getTrue(pvt_em); assert(ResultOfLayer3 != NULL); } else { set TempEqzChildren;//temporary variable for the function set TempDiseqzChildren;//temporary variable for the function ResultOfLayer3 = CreateKandNode(TempEqzChildren, TempDiseqzChildren, I_neg_X, pvt_em); assert(ResultOfLayer3 != NULL); } // for debugging pvt_em->printExpressionToFileAsDAG("ResultOfLayer3 ", ResultOfLayer3, cout); // for debugging ends here } else { // for debugging cout<<"\nThere are variables to eliminate\n"; // for debugging ends here // We need to compute \exists X.(I_X) and then conjunct it with I_neg_X // Let's compute FreePart = conjunction of LMCs in I_neg_X t_Expression* FreePart; if(I_neg_X.empty()) { FreePart = getTrue(pvt_em); } else { set TempEqzChildren;//temporary variable for the function set TempDiseqzChildren;//temporary variable for the function FreePart = CreateKandNode(TempEqzChildren, TempDiseqzChildren, I_neg_X, pvt_em); } assert(FreePart != NULL); // for debugging pvt_em->printExpressionToFileAsDAG("FreePart ", FreePart, cout); // for debugging ends here // Let's compute \exists X.(I_X) i.e. \exists VariablesStillToEliminate.(I_X) // We need to unify w.r.t. the variables in VariablesStillToEliminate // Let us find the variables which can be unified together // for debugging cout<<"\nFinding the variables which can be unified together\n"; // for debugging ends here set NonUnifiableVariables; bool unification_successful = false; t_Expression* UnifiedForm; do { // unification_successful == false and // there are variables which can be possibly unified set VariablesToUnifyTogether; bool UnifiableVariablesFound = findVariablesWhichCanBeUnifiedTogether(I_X, VariablesStillToEliminate, NonUnifiableVariables, VariablesToUnifyTogether); assert(UnifiableVariablesFound); // for debugging displaySetOfStringsOnScreen("VariablesToUnifyTogether", VariablesToUnifyTogether); // for debugging ends here // Recall that we need to compute \exists VariablesStillToEliminate.(I_X) // VariablesToUnifyTogether is a subset of VariablesStillToEliminate // Let us normalize I_X w.r.t. variables in VariablesToUnifyTogether UnifiedForm = convertToUnifiedForm(I_X, VariablesToUnifyTogether, unification_successful); assert(UnifiedForm != NULL); // for debugging cout<<"\nPerforming unification w.r.t. these variables\n"; pvt_em->printExpressionToFileAsDAG("UnifiedForm ", UnifiedForm, cout); // for debugging ends here if(!unification_successful) // none of the variables in VariablesToUnifyTogether could be unified { // for debugging cout<<"\nNone of the variables in VariablesToUnifyTogether could be unified\n"; // for debugging ends here // NonUnifiableVariables = NonUnifiableVariables \union VariablesToUnifyTogether set_union(NonUnifiableVariables.begin(), NonUnifiableVariables.end(), VariablesToUnifyTogether.begin(), VariablesToUnifyTogether.end(),inserter(NonUnifiableVariables, NonUnifiableVariables.begin())); } }while(!unification_successful && NonUnifiableVariables != VariablesStillToEliminate); if(unification_successful) { // for debugging cout<<"\nUnification successful\n"; // for debugging ends here t_Expression* QFreePart; string UnifiedFormLabel = pvt_em->getLabelOfExpression(UnifiedForm); assert("kand" == UnifiedFormLabel || "eqz" == UnifiedFormLabel || "diseqz" == UnifiedFormLabel || "leq" == UnifiedFormLabel || "logand" == UnifiedFormLabel || "logor" == UnifiedFormLabel || "lognot" == UnifiedFormLabel); if("kand" == UnifiedFormLabel) { // for debugging cout<<"\nCalling Project to eliminate the remaining variables\n"; // for debugging ends here vector VariablesStillToEliminate_Vector(VariablesStillToEliminate.begin(), VariablesStillToEliminate.end()); QFreePart = Project(UnifiedForm, VariablesStillToEliminate_Vector); assert(QFreePart != NULL); } else if("eqz" == UnifiedFormLabel || "diseqz" == UnifiedFormLabel || "leq" == UnifiedFormLabel) { // for debugging cout<<"\nCalling Project to eliminate the remaining variables\n"; // for debugging ends here vector VariablesStillToEliminate_Vector(VariablesStillToEliminate.begin(), VariablesStillToEliminate.end()); set UnifiedFormConstraints; UnifiedFormConstraints.insert(UnifiedForm); t_Expression* ConjunctionOfUnifiedFormConstraints = obtainKandNodeFromASetOfConstraints(UnifiedFormConstraints, pvt_em, pvt_bvm, pvt_VariableList, pvt_WidthTable); assert(ConjunctionOfUnifiedFormConstraints != NULL); QFreePart = Project(ConjunctionOfUnifiedFormConstraints, VariablesStillToEliminate_Vector); assert(QFreePart != NULL); } else if("logand" == UnifiedFormLabel || "logor" == UnifiedFormLabel || "lognot" == UnifiedFormLabel) { // for debugging cout<<"\nCalling Monniaux to eliminate the remaining variables\n"; // for debugging ends here vector VariablesStillToEliminate_Vector(VariablesStillToEliminate.begin(), VariablesStillToEliminate.end()); t_Monniaux* Monniaux_Instance = t_Monniaux::getInstance(pvt_VariableList, pvt_WidthTable, pvt_use_bvlibrary_for_layer2_computations, pvt_em, pvt_bvm); assert(Monniaux_Instance != NULL); t_solver solver = stp; QFreePart = Monniaux_Instance->Monniaux(UnifiedForm, VariablesStillToEliminate_Vector, solver); assert(QFreePart != NULL); } string node_name = "logand"; // ResultOfLayer3 = FreePart\wedge QFreePart if(isTrue(FreePart, pvt_em)) // FreePart == true { ResultOfLayer3 = QFreePart; } else if(isTrue(QFreePart, pvt_em)) // QFreePart == true { ResultOfLayer3 = FreePart; } else { ResultOfLayer3 = CreateNode(node_name, FreePart, QFreePart, pvt_em); } assert(ResultOfLayer3 != NULL); } else if(NonUnifiableVariables == VariablesStillToEliminate) // none of the variables in VariablesStillToEliminate could be unified // Layer3 cannot be used to eliminate the variables in VariablesStillToEliminate { // for debugging cout<<"\nNonUnifiableVariables == VariablesStillToEliminate\n"; // for debugging ends here // What we want to compute is, // FreePart \wedge \exists VariablesStillToEliminate. UnifiedForm // Problem is that Layer3 cannot compute \exists VariablesStillToEliminate. UnifiedForm cerr<<"\nWe wanted to compute FreePart and exists VariablesStillToEliminate. UnifiedForm."; cerr<<"\nHowever Layer3 cannot compute exists VariablesStillToEliminate. UnifiedForm."; cerr<<"\nWe need Layer4 for this. Exiting...\n"; // for debugging pvt_em->printExpressionToFileAsDAG("FreePart ", FreePart, cout); displaySetOfStringsOnScreen("VariablesStillToEliminate", VariablesStillToEliminate); pvt_em->printExpressionToFileAsDAG("UnifiedForm ", UnifiedForm, cout); // for debugging ends here assert(0); } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected location in function t_Project::Layer3", pvt_logFile, c_RunLevelVerbosity); return NULL; } // for debugging pvt_em->printExpressionToFileAsDAG("ResultOfLayer3 ", ResultOfLayer3, cout); // for debugging ends here }// !VariablesStillToEliminate.empty() && !I_X.empty() }// computing ResultOfLayer3 = \exists VariablesStillToEliminate.(I) ends here // update the hash table bool HashTable_Updated = update_Layer3_HashTable(kandNode, variables, ResultOfLayer3); if(!HashTable_Updated) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in hash table insertion in function t_Project::Layer3", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { return ResultOfLayer3; }// else of if(!HashTable_Updated) ends here }//hash table miss ends here }//else ends here }// function ends here // Given a set of inequations I_variable involving variable, this function checks if // all the inequations in I_variable are unified w.r.t. variable. // In other words, this function checks if each inequation is of the form // a.variable \bowtie t, where a is a constant, \bowtie \in {<=, >=}, and t is a term free of variable. // Note that a must be the same for all the inequations. // Sets constraints_with_variable_are_in_unified_form to // true if all the inequations in I_variable are unified w.r.t. variable, // false otherwise. // Returns false in case of errors, true otherwise. bool t_Project::constraintsInUnifiedForm(const set &I_variable, const string &variable, bool &constraints_with_variable_are_in_unified_form) { bvatom CommonCoefficient; // the common coefficient 'a' in a.variable \bowtie t bool CommonCoefficientFound = false; // take each inequation in I_variable for(set::iterator it = I_variable.begin(); it != I_variable.end(); it++) { t_Expression* LeqNode = *it; assert(LeqNode != NULL); assert("leq" == pvt_em->getLabelOfExpression(LeqNode)); // get the kadd nodes t_Expression* LHSOfLeqNode = getIthChild(LeqNode, 0, pvt_em);// get the LHS t_Expression* RHSOfLeqNode = getIthChild(LeqNode, 1, pvt_em);// get the RHS assert(LHSOfLeqNode != NULL); assert(RHSOfLeqNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHSOfLeqNode)); assert("kadd" == pvt_em->getLabelOfExpression(RHSOfLeqNode)); t_Expression* MonomWithVariableOnLHS; bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, pvt_em, pvt_VariableList); t_Expression* MonomWithVariableOnRHS; bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, pvt_em, pvt_VariableList); if(!LHSMonomFound || !RHSMonomFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::constraintsInUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariableOnLHS == NULL && MonomWithVariableOnRHS == NULL) //ERROR!!lhs is free of variable and rhs is free of variable: recall that we are working on inequations with variable { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! inequation free of variable to be eliminated in function t_Project::constraintsInUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariableOnLHS != NULL && MonomWithVariableOnRHS != NULL) //lhs contains variable and rhs contains variable: NOT IN UNIFIED FORM { constraints_with_variable_are_in_unified_form = false; return true; } else if(MonomWithVariableOnLHS == NULL && MonomWithVariableOnRHS != NULL) //lhs is free of variable and rhs is a term containing variable { // check if // rhs is of the form a.variable vector ChildrenOfRHSOfLeqNode = pvt_em->getVectorOfOperands(RHSOfLeqNode); if(ChildrenOfRHSOfLeqNode.size() != 1) //MonomWithVariableOnRHS is not the only child of RHSOfLeqNode // i.e. rhs is of the form constant.variable + s { constraints_with_variable_are_in_unified_form = false; return true; } else // rhs is of the form constant.variable { assert(MonomWithVariableOnRHS == ChildrenOfRHSOfLeqNode[0]); // find the variable and the coefficient of the monom MonomWithVariableOnRHS string VariableOfMonom; bvatom CoefficientOfMonom; bool VariableAndCoefficientFound = findVariableAndCoefficientOfMonom(MonomWithVariableOnRHS, VariableOfMonom, CoefficientOfMonom, pvt_em, pvt_bvm); assert(VariableAndCoefficientFound); assert(variable == VariableOfMonom); if(!CommonCoefficientFound)// a is not found; let's assign constant to a { CommonCoefficient = CoefficientOfMonom; CommonCoefficientFound = true; } else if(!pvt_bvm->checkBVEquality(CommonCoefficient, CoefficientOfMonom)) // CommonCoefficient != CoefficientOfMonom i.e. constant != a { constraints_with_variable_are_in_unified_form = false; return true; } } // rhs is of the form constant.variable ends here } else if(MonomWithVariableOnLHS != NULL && MonomWithVariableOnRHS == NULL) //rhs is free of variable and lhs is a term containing variable { // check if // lhs is of the form a.variable vector ChildrenOfLHSOfLeqNode = pvt_em->getVectorOfOperands(LHSOfLeqNode); if(ChildrenOfLHSOfLeqNode.size() != 1) //MonomWithVariableOnLHS is not the only child of LHSOfLeqNode // i.e. lhs is of the form constant.variable + s { constraints_with_variable_are_in_unified_form = false; return true; } else // lhs is of the form constant.variable { assert(MonomWithVariableOnLHS == ChildrenOfLHSOfLeqNode[0]); // find the variable and the coefficient of the monom MonomWithVariableOnLHS string VariableOfMonom; bvatom CoefficientOfMonom; bool VariableAndCoefficientFound = findVariableAndCoefficientOfMonom(MonomWithVariableOnLHS, VariableOfMonom, CoefficientOfMonom, pvt_em, pvt_bvm); assert(VariableAndCoefficientFound); assert(variable == VariableOfMonom); if(!CommonCoefficientFound)// a is not found; let's assign constant to a { CommonCoefficient = CoefficientOfMonom; CommonCoefficientFound = true; } else if(!pvt_bvm->checkBVEquality(CommonCoefficient, CoefficientOfMonom)) // CommonCoefficient != CoefficientOfMonom i.e. constant != a { constraints_with_variable_are_in_unified_form = false; return true; } } // lhs is of the form constant.variable ends here } else //ERROR!!unexpected location { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected location in function t_Project::constraintsInUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return false; } }//for ends here constraints_with_variable_are_in_unified_form = true; return true; }//function ends here // Here I_variable is a set of inequations involving variable, // where each inequation is of the form a.variable \bowtie t, // such that a is a constant, \bowtie \in {<=, >=}, and t is a term free of variable, // and Kappa(a.variable, variable) = 0. Also a is the same for all the inequations. // This function performs the standard Fourier-Motzkin algorithm // for QE from reals to compute \exists variable.(I_variable). // Note that since Kappa(a.variable, variable) = 0, standard // Fourier-Motzkin algorithm on reals works on bit-vectors also. // Result of \exists variable.(I_variable) is the conjunction of LMIs in Inequations_From_FM // Returns false in case of errors, true otherwise. bool t_Project::standardFourierMotzkin(const set &I_variable, const string &variable, set &Inequations_From_FM) { Inequations_From_FM.clear(); vector LowerBounds, UpperBounds; // lower bounds and upper bounds on a.variable // take each inequation in I_variable for(set::iterator it = I_variable.begin(); it != I_variable.end(); it++) { t_Expression* LeqNode = *it; assert(LeqNode != NULL); assert("leq" == pvt_em->getLabelOfExpression(LeqNode)); // get the kadd nodes t_Expression* LHSOfLeqNode = getIthChild(LeqNode, 0, pvt_em);// get the LHS t_Expression* RHSOfLeqNode = getIthChild(LeqNode, 1, pvt_em);// get the RHS assert(LHSOfLeqNode != NULL); assert(RHSOfLeqNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHSOfLeqNode)); assert("kadd" == pvt_em->getLabelOfExpression(RHSOfLeqNode)); t_Expression* MonomWithVariableOnLHS; bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, pvt_em, pvt_VariableList); t_Expression* MonomWithVariableOnRHS; bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, pvt_em, pvt_VariableList); if(!LHSMonomFound || !RHSMonomFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::standardFourierMotzkin", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariableOnLHS != NULL && MonomWithVariableOnRHS == NULL) //lhs is a.variable and rhs is t { UpperBounds.push_back(RHSOfLeqNode); } else if(MonomWithVariableOnLHS == NULL && MonomWithVariableOnRHS != NULL) //lhs is t and rhs is a.variable { LowerBounds.push_back(LHSOfLeqNode); } else //ERROR!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! non-unified inequation encountered in function t_Project::standardFourierMotzkin", pvt_logFile, c_RunLevelVerbosity); return false; } }// for ends here for(int i = 0; i < LowerBounds.size(); i++) for(int j = 0; j < UpperBounds.size(); j++) // take each lowerbound, upperbound { t_Expression* LB = LowerBounds[i]; t_Expression* UB = UpperBounds[j]; // create the LB <= UB string inequation_label = "leq"; t_Expression* QFreeInequation = CreateNode(inequation_label, LB, UB, pvt_em); assert(QFreeInequation != NULL); // insert QFreeInequation into Inequations_From_FM unless it is trivial if(!inequationIsTrivial(QFreeInequation, pvt_em, pvt_bvm)) //eg: 2 <= 3, t <= 2^{p}-1 etc. { Inequations_From_FM.insert(QFreeInequation); } }// for each lowerbound, upperbound ends here return true; } // Here I_variable is a set of inequations involving variable, // where each inequation is of the form a.variable \bowtie t, // such that a is a constant, \bowtie \in {<=, >=}, t is a term free of variable, // and Kappa = Kappa(a.variable, variable) != 0. // Also a is the same for all the inequations. // This function performs modified Fourier-Motzkin algorithm for LMIs // in the TACAS'13 paper to compute \exists variable.(I_variable). // Result of \exists variable.(I_variable) is the conjunction of constraints in Constraints_From_FM // If result_is_conjunctive then, // each constraint in Constraints_From_FM is an LMI // otherwise, // each constraint in Constraints_From_FM is a disjunction of kand nodes // Returns false in case of errors, true otherwise. bool t_Project::modifiedFourierMotzkin(const set &I_variable, const string &variable, unsigned Kappa, set &Constraints_From_FM, bool &result_is_conjunctive) { Constraints_From_FM.clear(); vector LowerBounds, UpperBounds; // lower bounds and upper bounds on a.variable // take each inequation in I_variable for(set::iterator it = I_variable.begin(); it != I_variable.end(); it++) { t_Expression* LeqNode = *it; assert(LeqNode != NULL); assert("leq" == pvt_em->getLabelOfExpression(LeqNode)); // get the kadd nodes t_Expression* LHSOfLeqNode = getIthChild(LeqNode, 0, pvt_em);// get the LHS t_Expression* RHSOfLeqNode = getIthChild(LeqNode, 1, pvt_em);// get the RHS assert(LHSOfLeqNode != NULL); assert(RHSOfLeqNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHSOfLeqNode)); assert("kadd" == pvt_em->getLabelOfExpression(RHSOfLeqNode)); t_Expression* MonomWithVariableOnLHS; bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, pvt_em, pvt_VariableList); t_Expression* MonomWithVariableOnRHS; bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, pvt_em, pvt_VariableList); if(!LHSMonomFound || !RHSMonomFound) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! monom finding error in function t_Project::modifiedFourierMotzkin", pvt_logFile, c_RunLevelVerbosity); return false; } else if(MonomWithVariableOnLHS != NULL && MonomWithVariableOnRHS == NULL) //lhs is a.variable and rhs is t { UpperBounds.push_back(RHSOfLeqNode); } else if(MonomWithVariableOnLHS == NULL && MonomWithVariableOnRHS != NULL) //lhs is t and rhs is a.variable { LowerBounds.push_back(LHSOfLeqNode); } else //ERROR!! { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! non-unified inequation encountered in function t_Project::modifiedFourierMotzkin", pvt_logFile, c_RunLevelVerbosity); return false; } }// for ends here // Find p, i.e. width of variable int p = getWidthOfVariable(variable, pvt_WidthTable); assert(p > 0); assert(Kappa < p); if(LowerBounds.size() == 0) // there are no lower bounds i.e. lower bound is zero { // \exists variable.(I_variable) is true // i.e. Constraints_From_FM is empty. But it is already empty result_is_conjunctive = true; return true; } else if(UpperBounds.size() == 0) // there are no upper bounds i.e. upper bound is 2^{p}-1 { // \exists variable.(I_variable) is // the conjunction of LB <= 2^p-2^Kappa for every lower bound LB. for(int i = 0; i < LowerBounds.size(); i++)// take each lower bound LB { t_Expression* LB = LowerBounds[i]; // We need to create the constraint LB <= 2^p-2^Kappa // Since 2^Kappa >=1 and Kappa < p, 2^p-2^Kappa = addInverse(2^Kappa) bvatom TwosPowerOfKappa = findTwosPower_UsingBVLibrary(p, Kappa); //2^Kappa: Note that TwosPowerOfKappa has p bits bvatom FinalConstant = pvt_bvm->addInverse(TwosPowerOfKappa); //2^p-2^Kappa vector< pair< string, bvatom > > FinalCoefficientMap; // create kadd node with constant 2^p-2^Kappa from final constant and final coefficient map t_Expression *RHSOfQFreeInequation = CreateKaddNodeFromConstantAndCoefficientMap(p, FinalConstant, FinalCoefficientMap, pvt_em, pvt_VariableList, pvt_bvm); assert(RHSOfQFreeInequation != NULL); // create LB <= 2^p-2^Kappa string inequation_label = "leq"; t_Expression* QFreeInequation = CreateNode(inequation_label, LB, RHSOfQFreeInequation, pvt_em); assert(QFreeInequation != NULL); // insert QFreeInequation into Constraints_From_FM unless it is trivial if(!inequationIsTrivial(QFreeInequation, pvt_em, pvt_bvm)) //eg: 2 <= 3, t <= 2^{p}-1 etc. { Constraints_From_FM.insert(QFreeInequation); } }// for each lowerbound ends here result_is_conjunctive = true; return true; } else // there are lower bounds as well as upper bounds { string inequation_label = "leq"; string equation_label = "eqz"; for(int i = 0; i < LowerBounds.size(); i++) for(int j = 0; j < UpperBounds.size(); j++) // take each lowerbound, upperbound { t_Expression* LB = LowerBounds[i]; t_Expression* UB = UpperBounds[j]; // We need to create the disjunction of // 1) kand of (LB <= UB) and (2^{p-Kappa}.LB = 0) // 2) kand of (LB <= UB), (LB+2^{Kappa}-1 <= UB), and (LB <= 2^p-2^Kappa) // 3) kand of (LB <= UB), (1 <= LB+2^{Kappa}-1), (UB <= LB+2^{Kappa}-2), (1 <= 2^{p-Kappa}.LB) ,and (2^{p-Kappa}.UB <= 2^{p-Kappa}.LB-1) // Let's create (LB <= UB) first: Let's call this Inequation_1 t_Expression* Inequation_1 = CreateNode(inequation_label, LB, UB, pvt_em); assert(Inequation_1 != NULL); // Let's create coefficient maps and constants for // LB, UB, 2^{p-Kappa}.LB, 2^{p-Kappa}.UB, 2^{p}-2^{Kappa}, and 1 set variables_to_exclude;// no variables to exclude bool CoefficientMapFound; // first, let's obtain coefficient maps and constants of LB and UB bvatom ConstantOfLB, ConstantOfUB; vector< pair< string, bvatom > > CoefficientMapOfLB, CoefficientMapOfUB; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(LB, variables_to_exclude, ConstantOfLB, CoefficientMapOfLB, pvt_em, pvt_bvm); assert(CoefficientMapFound); CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(UB, variables_to_exclude, ConstantOfUB, CoefficientMapOfUB, pvt_em, pvt_bvm); assert(CoefficientMapFound); // now, let's create coefficient maps and constants of 2^{p-Kappa}.LB and 2^{p-Kappa}.UB bvatom ShiftedConstantOfLB, ShiftedConstantOfUB; vector< pair< string, bvatom > > ShiftedCoefficientMapOfLB, ShiftedCoefficientMapOfUB; ShiftedConstantOfLB = pvt_bvm->bvlshift(ConstantOfLB, p-Kappa); leftShift(CoefficientMapOfLB, p-Kappa, ShiftedCoefficientMapOfLB, pvt_bvm); ShiftedConstantOfUB = pvt_bvm->bvlshift(ConstantOfUB, p-Kappa); leftShift(CoefficientMapOfUB, p-Kappa, ShiftedCoefficientMapOfUB, pvt_bvm); // now, let's create coefficient maps and constants of 2^{p}-2^{Kappa} and 1 bvatom ConstantOfAInverseOfTwosPowerOfKappa, ConstantOfOne; vector< pair< string, bvatom > > CoefficientMapOfAInverseOfTwosPowerOfKappa, CoefficientMapOfOne; bvatom TwosPowerOfKappa = findTwosPower_UsingBVLibrary(p, Kappa); //2^{Kappa} ConstantOfAInverseOfTwosPowerOfKappa = pvt_bvm->addInverse(TwosPowerOfKappa); //2^{p}-2^{Kappa} string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfOne = pvt_bvm->getBVatom(p, OneString); //1 bvatom ConstantOfTwo = pvt_bvm->bvadd(ConstantOfOne, ConstantOfOne); //2 // Let's create kadd node for 1 t_Expression *KaddNodeForOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfOne, CoefficientMapOfOne, pvt_em, pvt_VariableList, pvt_bvm); // kadd node for 1 assert(KaddNodeForOne != NULL); // Let's create (2^{p-Kappa}.LB = 0): Let's call this Equation_1 // Let's also create (1 <= 2^{p-Kappa}.LB): Let's call this Inequation_6 t_Expression *TemporaryKaddNode = CreateKaddNodeFromConstantAndCoefficientMap(p, ShiftedConstantOfLB, ShiftedCoefficientMapOfLB, pvt_em, pvt_VariableList, pvt_bvm); // 2^{p-Kappa}.LB assert(TemporaryKaddNode != NULL); t_Expression* Equation_1 = CreateNode(equation_label, TemporaryKaddNode, pvt_em); assert(Equation_1 != NULL); t_Expression* Inequation_6 = CreateNode(inequation_label, KaddNodeForOne, TemporaryKaddNode, pvt_em); assert(Inequation_6 != NULL); // Let's create (LB+2^{Kappa}-1 <= UB): Let's call this Inequation_2 // Let's also create (1 <= LB+2^{Kappa}-1): Let's call this Inequation_4 TemporaryKaddNode = CreateKaddNodeFromConstantAndCoefficientMap(p, pvt_bvm->bvadd(pvt_bvm->bvadd(ConstantOfLB, TwosPowerOfKappa), pvt_bvm->addInverse(ConstantOfOne)), CoefficientMapOfLB, pvt_em, pvt_VariableList, pvt_bvm); // LB+2^{Kappa}-1 assert(TemporaryKaddNode != NULL); t_Expression* Inequation_2 = CreateNode(inequation_label, TemporaryKaddNode, UB, pvt_em); assert(Inequation_2 != NULL); t_Expression* Inequation_4 = CreateNode(inequation_label, KaddNodeForOne, TemporaryKaddNode, pvt_em); assert(Inequation_4 != NULL); // Let's create (LB <= 2^p-2^Kappa): Let's call this Inequation_3 TemporaryKaddNode = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfAInverseOfTwosPowerOfKappa, CoefficientMapOfAInverseOfTwosPowerOfKappa, pvt_em, pvt_VariableList, pvt_bvm); // 2^p-2^Kappa assert(TemporaryKaddNode != NULL); t_Expression* Inequation_3 = CreateNode(inequation_label, LB, TemporaryKaddNode, pvt_em); assert(Inequation_3 != NULL); // Let's create (UB <= LB+2^{Kappa}-2): Let's call this Inequation_5 TemporaryKaddNode = CreateKaddNodeFromConstantAndCoefficientMap(p, pvt_bvm->bvadd(pvt_bvm->bvadd(ConstantOfLB, TwosPowerOfKappa), pvt_bvm->addInverse(ConstantOfTwo)), CoefficientMapOfLB, pvt_em, pvt_VariableList, pvt_bvm); // LB+2^{Kappa}-2 assert(TemporaryKaddNode != NULL); t_Expression* Inequation_5 = CreateNode(inequation_label, UB, TemporaryKaddNode, pvt_em); assert(Inequation_5 != NULL); // Let's create (2^{p-Kappa}.UB <= 2^{p-Kappa}.LB-1): Let's call this Inequation_7 TemporaryKaddNode = CreateKaddNodeFromConstantAndCoefficientMap(p, ShiftedConstantOfUB, ShiftedCoefficientMapOfUB, pvt_em, pvt_VariableList, pvt_bvm); // 2^{p-Kappa}.UB assert(TemporaryKaddNode != NULL); t_Expression* TemporaryKaddNode_2 = CreateKaddNodeFromConstantAndCoefficientMap(p, pvt_bvm->bvadd(ShiftedConstantOfLB, pvt_bvm->addInverse(ConstantOfOne)), ShiftedCoefficientMapOfLB, pvt_em, pvt_VariableList, pvt_bvm); // 2^{p-Kappa}.LB-1 assert(TemporaryKaddNode_2 != NULL); t_Expression* Inequation_7 = CreateNode(inequation_label, TemporaryKaddNode, TemporaryKaddNode_2, pvt_em); assert(Inequation_7 != NULL); // let's create the kand nodes now // let's first form their children set EqzChildren_1; // should contain Equation_1 set LeqChildren_1; // should contain Inequation_1 set LeqChildren_2; // should contain Inequation_1, Inequation_2, Inequation_3 set LeqChildren_3; // should contain Inequation_1, Inequation_4, Inequation_5, Inequation_6, Inequation_7 if(!equationIsTrivial(Equation_1, pvt_em)) //trivial equation such as 0=0 { EqzChildren_1.insert(Equation_1); } if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)) //eg: 2 <= 3, t <= 2^{p}-1 etc. { LeqChildren_1.insert(Inequation_1); LeqChildren_2.insert(Inequation_1); LeqChildren_3.insert(Inequation_1); } if(!inequationIsTrivial(Inequation_2, pvt_em, pvt_bvm)) { LeqChildren_2.insert(Inequation_2); } if(!inequationIsTrivial(Inequation_3, pvt_em, pvt_bvm)) { LeqChildren_2.insert(Inequation_3); } if(!inequationIsTrivial(Inequation_4, pvt_em, pvt_bvm)) { LeqChildren_3.insert(Inequation_4); } if(!inequationIsTrivial(Inequation_5, pvt_em, pvt_bvm)) { LeqChildren_3.insert(Inequation_5); } if(!inequationIsTrivial(Inequation_6, pvt_em, pvt_bvm)) { LeqChildren_3.insert(Inequation_6); } if(!inequationIsTrivial(Inequation_7, pvt_em, pvt_bvm)) { LeqChildren_3.insert(Inequation_7); } // now we can create the kand nodes t_Expression* kand_1; t_Expression* kand_2; t_Expression* kand_3; if(EqzChildren_1.empty() && LeqChildren_1.empty()) { // all children are trivial; hence result is true kand_1 = getTrue(pvt_em); assert(kand_1 != NULL); } else { set DiseqzChildren_1; kand_1 = CreateKandNode(EqzChildren_1, DiseqzChildren_1, LeqChildren_1, pvt_em); assert(kand_1 != NULL); } if(LeqChildren_2.empty()) { // all children are trivial; hence result is true kand_2 = getTrue(pvt_em); assert(kand_2 != NULL); } else { set EqzChildren_2; set DiseqzChildren_2; kand_2 = CreateKandNode(EqzChildren_2, DiseqzChildren_2, LeqChildren_2, pvt_em); assert(kand_2 != NULL); } if(LeqChildren_3.empty()) { // all children are trivial; hence result is true kand_3 = getTrue(pvt_em); assert(kand_3 != NULL); } else { set EqzChildren_3; set DiseqzChildren_3; kand_3 = CreateKandNode(EqzChildren_3, DiseqzChildren_3, LeqChildren_3, pvt_em); assert(kand_3 != NULL); } // let's create the disjunction of kand_1, kand_2, and kand_3, and // insert into Constraints_From_FM if(!isTrue(kand_1, pvt_em) && !isTrue(kand_2, pvt_em) && !isTrue(kand_3, pvt_em)) { // none of kand_1, kand_2, or kand_3 is true; hence result is not true string node_name = "logor"; vector ChildrenOfLogOr; ChildrenOfLogOr.push_back(kand_1); ChildrenOfLogOr.push_back(kand_2); ChildrenOfLogOr.push_back(kand_3); t_Expression* disjunction = CreateNode(node_name, ChildrenOfLogOr, pvt_em); assert(disjunction != NULL); Constraints_From_FM.insert(disjunction); } }// for each lowerbound, upperbound ends here result_is_conjunctive = false; return true; }// there are lower bounds as well as upper bounds ends here }// function ends here // Here I_variables is a set of inequations involving variables. // This function finds a subset of variables which can be unified together. // NonUnifiableVariables is a set of variables which cannot be unified. // The idea here is to select a subset of variables excluding those in NonUnifiableVariables, // such that no two variables in the subset appear in the same constraint. // Returns false in case of errors, true otherwise. bool t_Project::findVariablesWhichCanBeUnifiedTogether(const set &I_variables, const set &variables, const set &NonUnifiableVariables, set &VariablesToUnifyTogether) { VariablesToUnifyTogether.clear(); map > Neighbours;// let's find the set of neighbours of each variable // a variable t is neighbour of variable s if s and t appear in the same constraint for(set::iterator it = variables.begin(); it != variables.end(); it++) // take each variable { string variable = *it; // let us find the constraints in I_variables, which are free of and bound by variable set E_x, E_neg_x, D_x, D_neg_x, I_x, I_neg_x; bool FreeAndBoundConstraintsFound = findFreeAndBoundConstraintsFromSet(I_variables, variable, E_x, D_x, I_x, E_neg_x, D_neg_x, I_neg_x, pvt_em, pvt_VariableList); assert(FreeAndBoundConstraintsFound); assert(E_x.empty() && E_neg_x.empty() && D_x.empty() && D_neg_x.empty()); // Now I_variables = I_x \union I_neg_x // Let us find neighbours of variable; i.e. those variables which appear // with the variable in any constraint in I_x. set NeighboursOfVariable; for(set::iterator lit = I_x.begin(); lit != I_x.end(); lit++) // take each constraint in I_x { t_Expression* Inequation = *lit; assert(Inequation != NULL); set SupportOfInequation; bool SupportFound = findSupportOfConstraint(Inequation, SupportOfInequation, pvt_em); assert(SupportFound); // neighbours of variable = neighbours of variable \union support of constraint set_union(NeighboursOfVariable.begin(), NeighboursOfVariable.end(), SupportOfInequation.begin(), SupportOfInequation.end(),inserter(NeighboursOfVariable, NeighboursOfVariable.begin())); } // remove variable from NeighboursOfVariable assert(NeighboursOfVariable.size() >= 1); if(NeighboursOfVariable.size() == 1) // no neighbour for the variable { NeighboursOfVariable.clear(); } else { NeighboursOfVariable.erase(variable); } Neighbours.insert(make_pair(variable, NeighboursOfVariable)); }//for ends here set VariablesWhichCannotBeUnifiedTogether = NonUnifiableVariables; for(set::iterator it = variables.begin(); it != variables.end(); it++) // take each variable { string variable = *it; if(VariablesWhichCannotBeUnifiedTogether.find(variable) == VariablesWhichCannotBeUnifiedTogether.end()) { // select this variable for unification since it is not in VariablesWhichCannotBeUnifiedTogether VariablesToUnifyTogether.insert(variable); // insert the neighbours of variable in VariablesWhichCannotBeUnifiedTogether map >::iterator nit = Neighbours.find(variable); assert(nit != Neighbours.end()); set NeighboursOfVariable = nit->second; set_union(VariablesWhichCannotBeUnifiedTogether.begin(), VariablesWhichCannotBeUnifiedTogether.end(), NeighboursOfVariable.begin(), NeighboursOfVariable.end(), inserter(VariablesWhichCannotBeUnifiedTogether, VariablesWhichCannotBeUnifiedTogether.begin())); } }//for ends here return true; }//function // Suppose we need to compute \exists X.(I_X). // Let variables be a subset of X. This function unifies I_X w.r.t. variables. // Although the TACAS paper presents converting to unified form for a // number of cases, // this function performs unification of only constraints // of the form \exists x. A, // where x is a variable to be unified and A is a conjunction of LMIs, // such that, each LMI in A is of the form, // // ax+t_1 <= t_2, -ax+t_1 <= t_2, t_1 <= ax+t_2, t_1 <= -ax+t_2, // ax+b_1 <= ax+b_2, or -ax+b_1 <= -ax+b_2, // where a, b_1, b_2 are constants, and t_1, t_2 are terms free of x. // // The function converts each LMI in such a conjunction to a Boolean // combination of LMCs. // // In order to perform unification of I_X w.r.t. a set of variables, the function // takes each constraint and variable contained in it to be unified, checks if // the constraint can be unified w.r.t. the variable, and performs unification if possible. // // unification_successful is set to true if unification w.r.t. at least one variable could be // done; to false otherwise. // Returns NULL in case of errors; the unified expression otherwise. t_Expression* t_Project::convertToUnifiedForm(const set &I_X, const set &variables, bool &unification_successful) { vector< vector > UnifiedConstraints; // Each entry in UnifiedConstraints is a vector of constraints. // The final unified constraint is the conjunction of the disjunction // of constraints in each vector. map ConstraintVarToUnifyMap; // This is a map between inequation in I_X and the variable in it // to be unified. An inequation can have at-most one variable to // be unified. // let's create the ConstraintVarToUnifyMap first for(set::iterator it = I_X.begin(); it != I_X.end(); it++)// take each inequation { // Ensure that Constraint is inequation t_Expression* Constraint = *it; assert(Constraint != NULL); assert("leq" == pvt_em->getLabelOfExpression(Constraint)); // find support of the inequation set Support; bool SupportFound = findSupportOfConstraint(Constraint, Support, pvt_em); assert(SupportFound); // find variables in support to be unified set VariablesInSupportToUnify; set_intersection(Support.begin(), Support.end(), variables.begin(), variables.end(), inserter(VariablesInSupportToUnify, VariablesInSupportToUnify.begin())); if(VariablesInSupportToUnify.size() == 0) { // no variable in the support of the inequation to be unified // no entry for the inequation in ConstraintVarToUnifyMap continue; } else if(VariablesInSupportToUnify.size() > 1) { // more than one variable in the support of the inequation to be unified // ERROR!! something went wrong while computing variables to unify t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! more than one variable to normalize in the same constraint in function t_Project::convertToUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { // only one variable in the support of the inequation to be unified // enter (inequation, variable to unify) into ConstraintVarToUnifyMap ConstraintVarToUnifyMap.insert(make_pair(Constraint, *(VariablesInSupportToUnify.begin()))); } }// for loop to create the ConstraintVarToUnifyMap ends here map ConstraintWithVariableEncountered; // This map indicates if a constraint with the given variable // is already encountered or not for(set::iterator it = variables.begin(); it != variables.end(); it++) // take each variable to unify { ConstraintWithVariableEncountered.insert(make_pair(*it, false)); // initalizing to false } map CoefsOfVariable; // coefficient 'a' of each variable to be unified map AICoefsOfVariable; // additive inverse of coefficient, i.e. '-a' of each variable to be unified // now let's unify each inequation for(set::iterator it = I_X.begin(); it != I_X.end(); it++)// take each inequation { t_Expression* Constraint = *it; assert(Constraint != NULL); assert("leq" == pvt_em->getLabelOfExpression(Constraint)); // let's find the variable in the inequation to be unified map::iterator it = ConstraintVarToUnifyMap.find(Constraint); if(it == ConstraintVarToUnifyMap.end()) // no variable to unify // hence the constraint need not be unified { vector UnifiedVector; UnifiedVector.push_back(Constraint); UnifiedConstraints.push_back(UnifiedVector); continue; } else // there's variable to unify { string VarToUnify = it->second; // VarToUnify is the variable in the inequation to be unified t_side_of_variable_in_unification side_of_variable = findSideOfVariableInInequation(Constraint, VarToUnify); // let's find the side of the inequation where the variable appears - NONE, BOTH, LEFT, or RIGHT if(side_of_variable == NONE) { // ERROR!! inequation free of VarToUnify, but has entry (inequation, VarToUnify) in ConstraintVarToUnifyMap t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! constraint free of variable encountered in function t_Project::convertToUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return NULL; }//if(side_of_variable == NONE) else // side_of_variable can be BOTH, LEFT, or RIGHT { t_type_of_coefficient_in_unification type_of_coefficient = ORIGINAL;// default value map::iterator cit = ConstraintWithVariableEncountered.find(VarToUnify); if(cit == ConstraintWithVariableEncountered.end()) // no entry for VarToUnify in ConstraintWithVariableEncountered // ERROR!! each variable should have entry in ConstraintWithVariableEncountered { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! error in creation of map ConstraintWithVariableEncountered in function t_Project::convertToUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return NULL; }//if no entry for variable in ConstraintWithVariableEncountered else // there's entry for variable in ConstraintWithVariableEncountered { bool constraint_with_variable_encountered_before = cit->second; if(!constraint_with_variable_encountered_before)// Constraint is the first constraint with VarToUnify { // constraint with VarToUnify encountered for the first time bvatom CoefOfVarToUnify; bvatom AIOfCoefOfVarToUnify; bool constraint_non_unifiable; bool CoefficientFound = getCoefOfVarToUnifyAndAIOfCoefOfVarToUnify(Constraint, VarToUnify, side_of_variable, CoefOfVarToUnify, AIOfCoefOfVarToUnify, constraint_non_unifiable); assert(CoefficientFound); if(constraint_non_unifiable) // constraint is non unifiable // let's take the next constraint { vector UnifiedVector; UnifiedVector.push_back(Constraint); UnifiedConstraints.push_back(UnifiedVector); continue; } else // constraint is unifiable { CoefsOfVariable.insert(make_pair(VarToUnify, CoefOfVarToUnify)); AICoefsOfVariable.insert(make_pair(VarToUnify, AIOfCoefOfVarToUnify)); ConstraintWithVariableEncountered[VarToUnify] = true; }// constraint is unifiable ends here }//Constraint is the first constraint with VarToUnify ends here else { // constraint with VarToUnify is encountered before // Let's obtain the existing coefficient and additive inverse of coefficient for VarToUnify bvatom CoefOfVarToUnify; bvatom AIOfCoefOfVarToUnify; map::iterator coef_it = CoefsOfVariable.find(VarToUnify); if(coef_it == CoefsOfVariable.end()) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! no entry for variable to be unified in CoefsOfVariable in function t_Project::convertToUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return NULL; } CoefOfVarToUnify = coef_it->second; map::iterator aicoef_it = AICoefsOfVariable.find(VarToUnify); if(aicoef_it == AICoefsOfVariable.end()) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! no entry for variable to be unified in AICoefsOfVariable in function t_Project::convertToUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return NULL; } AIOfCoefOfVarToUnify = aicoef_it->second; bool constraint_non_unifiable; bool TypeOfCoefficientFound = findTypeOfCoefficient(Constraint, VarToUnify, side_of_variable, CoefOfVarToUnify, AIOfCoefOfVarToUnify, type_of_coefficient, constraint_non_unifiable); assert(TypeOfCoefficientFound); if(constraint_non_unifiable) // constraint is non unifiable // let's take the next constraint { vector UnifiedVector; UnifiedVector.push_back(Constraint); UnifiedConstraints.push_back(UnifiedVector); continue; } }// constraint with VarToUnify is encountered before ends here vector UnifiedVector; bool constraint_already_unified; bool UnificationDone; if(side_of_variable == LEFT || side_of_variable == RIGHT) { UnificationDone = unifyInequationWithVariableOnOneSide(Constraint, VarToUnify, side_of_variable, type_of_coefficient, UnifiedVector, constraint_already_unified); } else { UnificationDone = unifyInequationWithVariableOnBothSides(Constraint, VarToUnify, side_of_variable, type_of_coefficient, UnifiedVector, constraint_already_unified); } assert(UnificationDone); if(constraint_already_unified) // constraint was already unified { UnifiedVector.push_back(Constraint); UnifiedConstraints.push_back(UnifiedVector); continue; } else // constraint was not unified { UnifiedConstraints.push_back(UnifiedVector); unification_successful = true; // at least one variable unified } } // there's entry for variable in ConstraintWithVariableEncountered ends here }// side_of_variable can be BOTH, LEFT, or RIGHT ends here } // there's variable to unify ends here } //for loop which takes each inequation for unification ends here // Let's create the final answer vector Final_Result_Vector; for(int i = 0; i < UnifiedConstraints.size(); i++) { string operator_name = "logor"; vector ChildrenOfLogOr = UnifiedConstraints[i]; assert(ChildrenOfLogOr.size() > 0); t_Expression* disjunction; if(ChildrenOfLogOr.size() == 1) { disjunction = ChildrenOfLogOr[0]; } else { disjunction = CreateNode(operator_name, ChildrenOfLogOr, pvt_em); } assert(disjunction != NULL); Final_Result_Vector.push_back(disjunction); } string operator_name = "logand"; assert(Final_Result_Vector.size() > 0); t_Expression* Final_Result; if(Final_Result_Vector.size() == 1) { Final_Result = Final_Result_Vector[0]; } else { Final_Result = CreateNode(operator_name, Final_Result_Vector, pvt_em); } assert(Final_Result != NULL); return Final_Result; }// function ends here // Given an inequation t_1 <= t_2, a variable x in the support of t_1 <= t_2, // and side_of_variable indicating the side of t_1 <= t_2 where x occurs, // this function performs the following: // // (1) If side_of_variable is LEFT, i.e. t_1 <= t_2 is like ax+t_3 <= t_2, then // it finds a and -a in CoefOfVarToUnify and AIOfCoefOfVarToUnify respectively. // Also it sets constraint_non_unifiable to false. // (2) If side_of_variable is RIGHT, i.e. t_1 <= t_2 is like t_1 <= ax+t_3, then // it finds a and -a in CoefOfVarToUnify and AIOfCoefOfVarToUnify respectively. // Also it sets constraint_non_unifiable to false. // (3) If side_of_variable is BOTH, i.e. t_1 <= t_2 is like a_1x+t_3 <= a_2x+t_4, then // it checks if a_1 == a_2 and t_3 and t_4 are constants. If yes, then, // it finds a and -a in CoefOfVarToUnify and AIOfCoefOfVarToUnify respectively. // Also it sets constraint_non_unifiable to false. // Otherwise, it sets constraint_non_unifiable to true. // Returns false in case of errors; true otherwise. bool t_Project::getCoefOfVarToUnifyAndAIOfCoefOfVarToUnify(t_Expression* Inequation, const string &VarToUnify, t_side_of_variable_in_unification side_of_variable, bvatom &CoefOfVarToUnify, bvatom &AIOfCoefOfVarToUnify, bool &constraint_non_unifiable) { assert(Inequation != NULL); assert("leq" == pvt_em->getLabelOfExpression(Inequation)); // Let t_1 <= t_2 be the Inequation if(side_of_variable == LEFT) // Inequation is like ax+t_3 <= t_2 { t_Expression* LHSNode = getIthChild(Inequation, 0, pvt_em); // get the LHS node ax+t_3 assert(LHSNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHSNode)); // find the monom in the "kadd" node with VarToUnify t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(LHSNode, VarToUnify, MonomWithVariable, pvt_em, pvt_VariableList); // get the monom ax assert(MonomFound); assert(MonomWithVariable != NULL); // find the coefficient of variable in the monom bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefOfVarToUnify, pvt_em, pvt_bvm); // a obtained assert(CoefficientFound); // find the additive inverse AIOfCoefOfVarToUnify = pvt_bvm->addInverse(CoefOfVarToUnify); // -a obtained constraint_non_unifiable = false; return true; } else if(side_of_variable == RIGHT) // Inequation is like t_1 <= ax+t_3 { t_Expression* RHSNode = getIthChild(Inequation, 1, pvt_em); // get the RHS node ax+t_3 assert(RHSNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHSNode)); // find the monom in the "kadd" node with VarToUnify t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(RHSNode, VarToUnify, MonomWithVariable, pvt_em, pvt_VariableList); // get the monom ax assert(MonomFound); assert(MonomWithVariable != NULL); // find the coefficient of variable in the monom bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefOfVarToUnify, pvt_em, pvt_bvm); // a obtained assert(CoefficientFound); // find the additive inverse AIOfCoefOfVarToUnify = pvt_bvm->addInverse(CoefOfVarToUnify); // -a obtained constraint_non_unifiable = false; return true; } else if(side_of_variable == BOTH) // Inequation is like a_1x+t_3 <= a_2x+t_4 { t_Expression* LHSNode = getIthChild(Inequation, 0, pvt_em); // get the LHS node a_1x+t_3 assert(LHSNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHSNode)); t_Expression* RHSNode = getIthChild(Inequation, 1, pvt_em); // get the RHS node a_2x+t_4 assert(RHSNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHSNode)); set variables_to_exclude;// no variables to exclude bool CoefficientMapFound; // Let's obtain coefficient map and constant of LHSNode and RHSNode bvatom ConstantOfLHSNode, ConstantOfRHSNode; vector< pair< string, bvatom > > CoefficientMapOfLHSNode, CoefficientMapOfRHSNode; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(LHSNode, variables_to_exclude, ConstantOfLHSNode, CoefficientMapOfLHSNode, pvt_em, pvt_bvm); assert(CoefficientMapFound); CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(RHSNode, variables_to_exclude, ConstantOfRHSNode, CoefficientMapOfRHSNode, pvt_em, pvt_bvm); assert(CoefficientMapFound); if(CoefficientMapOfLHSNode.size() == 1 && CoefficientMapOfRHSNode.size() == 1) // x is the only variable // on both LHS and RHS, i.e., t_3 and t_4 are constants { bvatom CoefficientOnLHS, CoefficientOnRHS; string VariableOnLHS, VariableOnRHS; VariableOnLHS = CoefficientMapOfLHSNode[0].first; // get x CoefficientOnLHS = CoefficientMapOfLHSNode[0].second; // get a_1 VariableOnRHS = CoefficientMapOfRHSNode[0].first; // get x CoefficientOnRHS = CoefficientMapOfRHSNode[0].second; // get a_2 assert(VariableOnLHS == VarToUnify); assert(VariableOnRHS == VarToUnify); if(pvt_bvm->checkBVEquality(CoefficientOnLHS, CoefficientOnRHS)) // a_1 == a_2 { CoefOfVarToUnify = CoefficientOnLHS; // a = a_1 // find the additive inverse AIOfCoefOfVarToUnify = pvt_bvm->addInverse(CoefOfVarToUnify); // -a obtained constraint_non_unifiable = false; return true; } else // a_1 != a_2; non unifiable!! { constraint_non_unifiable = true; return true; } } else // t_3 and t_4 are not constants; non unifiable!! { constraint_non_unifiable = true; return true; } } else // ERROR!! unexpected value for side_of_variable { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected value for side_of_variable in function t_Project::convertToUnifiedForm", pvt_logFile, c_RunLevelVerbosity); return false; } }// function ends here // Checks if the coefficient of the variable to be eliminated is the same/additive inverse // of the coefficients which previously appeared. Sets type_of_coefficient to ORIGINAL/NEGATED according to it. // // Given an inequation t_1 <= t_2, a variable x in the support of t_1 <= t_2, // side_of_variable indicating the side of t_1 <= t_2 where x occurs, // CoefOfVarToUnify as the previously appeared coefficient, and AIOfCoefOfVarToUnify // as the additive inverse of the previously appeared coefficient, // this function performs the following: // // (1) If side_of_variable is LEFT, i.e. t_1 <= t_2 is like ax+t_3 <= t_2, then // it finds a and checks if a == CoefOfVarToUnify or a == AIOfCoefOfVarToUnify. // If a == CoefOfVarToUnify then, type_of_coefficient is set to ORIGINAL; // if a == AIOfCoefOfVarToUnify then, type_of_coefficient is set to NEGATED. // Also it sets constraint_non_unifiable to false. // If a != CoefOfVarToUnify and a != AIOfCoefOfVarToUnify then sets constraint_non_unifiable to true. // // (2) If side_of_variable is RIGHT, i.e. t_1 <= t_2 is like t_1 <= ax+t_3, then // it finds a and checks if a == CoefOfVarToUnify or a == AIOfCoefOfVarToUnify. // If a == CoefOfVarToUnify then, type_of_coefficient is set to ORIGINAL; // if a == AIOfCoefOfVarToUnify then, type_of_coefficient is set to NEGATED. // Also it sets constraint_non_unifiable to false. // If a != CoefOfVarToUnify and a != AIOfCoefOfVarToUnify then sets constraint_non_unifiable to true. // // (3) If side_of_variable is BOTH, i.e. t_1 <= t_2 is like a_1x+t_3 <= a_2x+t_4, then // it checks if a_1 == a_2 and t_3 and t_4 are constants. If yes, then, // it finds a = a_1 and checks if a == CoefOfVarToUnify or a == AIOfCoefOfVarToUnify. // If a == CoefOfVarToUnify then, type_of_coefficient is set to ORIGINAL; // if a == AIOfCoefOfVarToUnify then, type_of_coefficient is set to NEGATED. // Also it sets constraint_non_unifiable to false. // Otherwise, it sets constraint_non_unifiable to true. // // Returns false in case of errors; true otherwise. bool t_Project::findTypeOfCoefficient(t_Expression* Inequation, const string &VarToUnify, t_side_of_variable_in_unification side_of_variable, bvatom CoefOfVarToUnify, bvatom AIOfCoefOfVarToUnify, t_type_of_coefficient_in_unification &type_of_coefficient, bool &constraint_non_unifiable) { assert(Inequation != NULL); assert("leq" == pvt_em->getLabelOfExpression(Inequation)); // Let t_1 <= t_2 be the Inequation if(side_of_variable == LEFT) // Inequation is like ax+t_3 <= t_2 { t_Expression* LHSNode = getIthChild(Inequation, 0, pvt_em); // get the LHS node ax+t_3 assert(LHSNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHSNode)); // find the monom in the "kadd" node with VarToUnify t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(LHSNode, VarToUnify, MonomWithVariable, pvt_em, pvt_VariableList); // get the monom ax assert(MonomFound); assert(MonomWithVariable != NULL); // find the coefficient of variable in the monom bvatom CoefficientOfMonom; bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefficientOfMonom, pvt_em, pvt_bvm); // a obtained assert(CoefficientFound); if(pvt_bvm->checkBVEquality(CoefficientOfMonom, CoefOfVarToUnify)) // a == CoefOfVarToUnify { type_of_coefficient = ORIGINAL; constraint_non_unifiable = false; return true; } else if(pvt_bvm->checkBVEquality(CoefficientOfMonom, AIOfCoefOfVarToUnify)) // a == AIOfCoefOfVarToUnify { type_of_coefficient = NEGATED; constraint_non_unifiable = false; return true; } else { constraint_non_unifiable = true; return true; } } else if(side_of_variable == RIGHT) // Inequation is like t_1 <= ax+t_3 { t_Expression* RHSNode = getIthChild(Inequation, 1, pvt_em); // get the RHS node ax+t_3 assert(RHSNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHSNode)); // find the monom in the "kadd" node with VarToUnify t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(RHSNode, VarToUnify, MonomWithVariable, pvt_em, pvt_VariableList); // get the monom ax assert(MonomFound); assert(MonomWithVariable != NULL); // find the coefficient of variable in the monom bvatom CoefficientOfMonom; bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefficientOfMonom, pvt_em, pvt_bvm); // a obtained assert(CoefficientFound); if(pvt_bvm->checkBVEquality(CoefficientOfMonom, CoefOfVarToUnify)) // a == CoefOfVarToUnify { type_of_coefficient = ORIGINAL; constraint_non_unifiable = false; return true; } else if(pvt_bvm->checkBVEquality(CoefficientOfMonom, AIOfCoefOfVarToUnify)) // a == AIOfCoefOfVarToUnify { type_of_coefficient = NEGATED; constraint_non_unifiable = false; return true; } else { constraint_non_unifiable = true; return true; } } else if(side_of_variable == BOTH) // Inequation is like a_1x+t_3 <= a_2x+t_4 { t_Expression* LHSNode = getIthChild(Inequation, 0, pvt_em); // get the LHS node a_1x+t_3 assert(LHSNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHSNode)); t_Expression* RHSNode = getIthChild(Inequation, 1, pvt_em); // get the RHS node a_2x+t_4 assert(RHSNode != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHSNode)); set variables_to_exclude;// no variables to exclude bool CoefficientMapFound; // Let's obtain coefficient map and constant of LHSNode and RHSNode bvatom ConstantOfLHSNode, ConstantOfRHSNode; vector< pair< string, bvatom > > CoefficientMapOfLHSNode, CoefficientMapOfRHSNode; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(LHSNode, variables_to_exclude, ConstantOfLHSNode, CoefficientMapOfLHSNode, pvt_em, pvt_bvm); assert(CoefficientMapFound); CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(RHSNode, variables_to_exclude, ConstantOfRHSNode, CoefficientMapOfRHSNode, pvt_em, pvt_bvm); assert(CoefficientMapFound); if(CoefficientMapOfLHSNode.size() == 1 && CoefficientMapOfRHSNode.size() == 1) // x is the only variable // on both LHS and RHS, i.e., t_3 and t_4 are constants { bvatom CoefficientOnLHS, CoefficientOnRHS; string VariableOnLHS, VariableOnRHS; VariableOnLHS = CoefficientMapOfLHSNode[0].first; // get x CoefficientOnLHS = CoefficientMapOfLHSNode[0].second; // get a_1 VariableOnRHS = CoefficientMapOfRHSNode[0].first; // get x CoefficientOnRHS = CoefficientMapOfRHSNode[0].second; // get a_2 assert(VariableOnLHS == VarToUnify); assert(VariableOnRHS == VarToUnify); if(pvt_bvm->checkBVEquality(CoefficientOnLHS, CoefficientOnRHS)) // a_1 == a_2 { if(pvt_bvm->checkBVEquality(CoefficientOnLHS, CoefOfVarToUnify)) // a_1 == CoefOfVarToUnify { type_of_coefficient = ORIGINAL; constraint_non_unifiable = false; return true; } else if(pvt_bvm->checkBVEquality(CoefficientOnLHS, AIOfCoefOfVarToUnify)) // a_1 == AIOfCoefOfVarToUnify { type_of_coefficient = NEGATED; constraint_non_unifiable = false; return true; } else { constraint_non_unifiable = true; return true; } } else // a_1 != a_2; non unifiable!! { constraint_non_unifiable = true; return true; } } else // t_3 and t_4 are not constants; non unifiable!! { constraint_non_unifiable = true; return true; } } else // ERROR!! unexpected value for side_of_variable { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected value for side_of_variable in function t_Project::findTypeOfCoefficient", pvt_logFile, c_RunLevelVerbosity); return false; } }// function ends here // Given an inequation \alpha <= \beta, a variable x in the support of \alpha <= \beta, // side_of_variable indicating the side of \alpha <= \beta where x occurs, // this function performs the following: // // (1) If side_of_variable is LEFT and type_of_coefficient is ORIGINAL, // i.e. \alpha <= \beta is like ax+t_1 <= t_2, then // // If t_1 is zero, then we have ax <= t2; // in this case constraint_already_unified is set to true // // otherwise, it generates the following Boolean combination unified w.r.t. x: // // ((t_1 \neq 0)\wedge (-t_1 \le ax)\wedge (t_1 \le t_2)) \vee // ((t_1 = 0)\wedge (ax <= t_2 - t_1)) \vee // ((-t_1 \le ax)\wedge (ax <= t_2 - t_1)) \vee // ((t_1 \neq 0)\wedge (t_1 \le t_2)\wedge (ax <= t_2 - t_1)) // // also constraint_already_unified is set to false. // // (2) If side_of_variable is LEFT and type_of_coefficient is NEGATED, // i.e. \alpha <= \beta is like -ax+t_1 <= t_2, then it generates the following // Boolean combination unified w.r.t. x: // // ((t_1 \neq 0)\wedge (ax \neq 0)\wedge (ax \le t_1)\wedge (t_1 \le t_2)) \vee // ((t_2 = 0)\wedge (ax = 0)) \vee // ((t_1 = 0)\wedge (t_2 - t_1 \neq 0)\wedge (t_1 - t_2 <= ax)) \vee // ((ax \neq 0)\wedge (ax <= t_1)\wedge (t_2 - t_1 \neq 0)\wedge (t_1 - t_2 <= ax)) \vee // ((t_1 \neq 0)\wedge (t_1 \le t_2)\wedge (ax = 0)) \vee // ((t_1 \neq 0)\wedge (t_1 \le t_2)\wedge (t_2 - t_1 \neq 0)\wedge (t_1 - t_2 <= ax)) // // also constraint_already_unified is set to false. // // (3) If side_of_variable is RIGHT and type_of_coefficient is ORIGINAL, // i.e. \alpha <= \beta is like t_1 <= ax+t_2, then // // If t_2 is zero, then we have t_1 <= ax; // in this case constraint_already_unified is set to true // // otherwise, it generates the following Boolean combination unified w.r.t. x: // // ((t_2 \neq 0)\wedge (ax \le -t_2-1)\wedge (t_1 \le t_2-1))\vee // ((t_2 = 0)\wedge (t_1-t_2 <= ax))\vee // ((t_2 \neq 0)\wedge (t_1 \le t_2-1)\wedge (t_1-t_2 <= ax))\vee // ((t_2 \neq 0)\wedge (ax <= -t_2-1)\wedge (t_1-t_2 <= ax)) // // also constraint_already_unified is set to false. // // (4) If side_of_variable is RIGHT and type_of_coefficient is NEGATED, // i.e. \alpha <= \beta is like t_1 <= -ax+t_2, then it generates the following // Boolean combination unified w.r.t. x: // // ((t_2 \neq 0)\wedge (ax = 0)\wedge (t_1 \le t_2-1)) \vee // ((t_2 \neq 0)\wedge (t_2 + 1 \le ax)\wedge (-t_2 - 1 \neq 0)\wedge (t_1 \le t_2-1)) \vee // ((t_2 = 0)\wedge (t_1 - t_2 = 0)) \vee // ((t_2 = 0)\wedge (ax \neq 0)\wedge (ax \le t_2 - t_1)) \vee // ((t_1 \le t_2 - 1)\wedge (t_1 - t_2 = 0)\wedge (t_2 \neq 0)) \vee // ((t_1 \le t_2 - 1)\wedge (ax \neq 0)\wedge (ax \le t_2 - t_1)\wedge (t_2 \neq 0)) \vee // ((t_2 \neq 0)\wedge (ax = 0)\wedge (t_1 - t_2 = 0)) \vee // ((t_2 \neq 0)\wedge (-t_2 - 1 \neq 0)\wedge (t_2 + 1 \le ax)\wedge (t_1 - t_2 = 0)) \vee // ((t_2 \neq 0)\wedge (-t_2 - 1 \neq 0)\wedge (t_2 + 1 \le ax)\wedge (ax \neq 0)\wedge (ax \le t_2 - t_1)) // // also constraint_already_unified is set to false. // bool t_Project::unifyInequationWithVariableOnOneSide(t_Expression* Inequation, const string &VarToUnify, t_side_of_variable_in_unification side_of_variable, t_type_of_coefficient_in_unification type_of_coefficient, vector &UnifiedVector, bool &constraint_already_unified) { assert(Inequation != NULL); assert("leq" == pvt_em->getLabelOfExpression(Inequation)); // Find p, i.e. width of VarToUnify int p = getWidthOfVariable(VarToUnify, pvt_WidthTable); assert(p > 0); string inequation_label = "leq"; string equation_label = "eqz"; string disequation_label = "diseqz"; // Let \alpha <= \beta be the Inequation if(side_of_variable == LEFT && type_of_coefficient == ORIGINAL) // Inequation is like ax+t_1 <= t_2 { t_Expression* LHS = getIthChild(Inequation, 0, pvt_em); // get the LHS node ax+t_1 assert(LHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHS)); t_Expression* RHS = getIthChild(Inequation, 1, pvt_em); // get the RHS node t_2 assert(RHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHS)); // get the monom ax in LHS t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(LHS, VarToUnify, MonomWithVariable, pvt_em, pvt_VariableList); // get the monom ax assert(MonomFound); assert(MonomWithVariable != NULL); // find the coefficient of x in the monom bvatom CoefficientOfMonom; bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefficientOfMonom, pvt_em, pvt_bvm); // a obtained assert(CoefficientFound); // We need to push back the following into UnifiedVector: // 1) kand of (t_1 \neq 0), (-t_1 \le ax), and (t_1 \le t_2) // 2) kand of (t_1 = 0) and (ax <= t_2 - t_1) // 3) kand of (-t_1 \le ax) and (ax <= t_2 - t_1) // 4) kand of (t_1 \neq 0), (t_1 \le t_2), and (ax <= t_2 - t_1) // Let's create coefficient maps and constants for // t_1, -t_1, t_2-t_1, and ax set variables_to_exclude; bool CoefficientMapFound; // first, let's obtain coefficient map and constant of t_1 // t_1's coefficient map = LHS's coefficient map \ entry for VarToUnify variables_to_exclude.insert(VarToUnify); bvatom ConstantOft1; vector< pair< string, bvatom > > CoefficientMapOft1; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(LHS, variables_to_exclude, ConstantOft1, CoefficientMapOft1, pvt_em, pvt_bvm); assert(CoefficientMapFound); // Let's check if the Inequation is of the form ax <= t_2; i.e. already unified if(CoefficientMapOft1.size() == 0 && pvt_bvm->checkBVForZero(ConstantOft1)) // t_1 is zero; already unified { constraint_already_unified = true; return true; } else { constraint_already_unified = false; // now, let's obtain coefficient map and constant of t_2 // t_2's coefficient map = RHS's coefficient map variables_to_exclude.clear(); bvatom ConstantOft2; vector< pair< string, bvatom > > CoefficientMapOft2; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(RHS, variables_to_exclude, ConstantOft2, CoefficientMapOft2, pvt_em, pvt_bvm); assert(CoefficientMapFound); // now, let's obtain coefficient map and constant of -t_1 from those of t_1 bvatom ConstantOfMinust1; vector< pair< string, bvatom > > CoefficientMapOfMinust1; ConstantOfMinust1 = pvt_bvm->addInverse(ConstantOft1); additiveInverse(CoefficientMapOft1, CoefficientMapOfMinust1, pvt_bvm); // now, let's obtain coefficient map and constant of t_2-t_1 from those of t_2 and -t_1 bvatom ConstantOft2Minust1; vector< pair< string, bvatom > > CoefficientMapOft2Minust1; ConstantOft2Minust1 = pvt_bvm->bvadd(ConstantOft2, ConstantOfMinust1); addition(CoefficientMapOft2, CoefficientMapOfMinust1, CoefficientMapOft2Minust1, pvt_bvm, pvt_VariableList); // now, let's obtain coefficient map and constant of ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CoefficientOfMonom)); // push back (x, a) into CoefficientMapOfax // Let's create kadd nodes for // t_1, -t_1, t_2-t_1, and ax t_Expression *KaddNodeFort1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft1, CoefficientMapOft1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort1 != NULL); t_Expression *KaddNodeForMinust1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinust1, CoefficientMapOfMinust1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinust1 != NULL); t_Expression *KaddNodeFort2Minust1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2Minust1, CoefficientMapOft2Minust1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort2Minust1 != NULL); t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create (t_1 = 0): Let's call this Equation_1 // Let's also create (t_1 \neq 0): Let's call this Disequation_1 t_Expression* Equation_1 = CreateNode(equation_label, KaddNodeFort1, pvt_em); assert(Equation_1 != NULL); t_Expression* Disequation_1 = CreateNode(disequation_label, KaddNodeFort1, pvt_em); assert(Disequation_1 != NULL); // Let's create (-t_1 <= ax), (t_1 <= t_2), and (ax <= t_2-t_1) // Let's call them Inequation_1, Inequation_2, and Inequation_3 t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForMinust1, KaddNodeForax, pvt_em); assert(Inequation_1 != NULL); t_Expression* Inequation_2 = CreateNode(inequation_label, KaddNodeFort1, RHS, pvt_em); assert(Inequation_2 != NULL); t_Expression* Inequation_3 = CreateNode(inequation_label, KaddNodeForax, KaddNodeFort2Minust1, pvt_em); assert(Inequation_3 != NULL); // let's create the kand nodes now // let's first form their children set DiseqzChildren_1; // should contain Disequation_1 set LeqChildren_1; // should contain Inequation_1 and Inequation_2 set EqzChildren_2; // should contain Equation_1 set LeqChildren_2; // should contain Inequation_3 set LeqChildren_3; // should contain Inequation_1 and Inequation_3 set DiseqzChildren_4; // should contain Disequation_1 set LeqChildren_4; // should contain Inequation_2 and Inequation_3 if(!disequationIsTrivial(Disequation_1, pvt_em)) //not trivial disequation { DiseqzChildren_1.insert(Disequation_1); DiseqzChildren_4.insert(Disequation_1); } if(!equationIsTrivial(Equation_1, pvt_em)) //not trivial equation { EqzChildren_2.insert(Equation_1); } if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_1.insert(Inequation_1); LeqChildren_3.insert(Inequation_1); } if(!inequationIsTrivial(Inequation_2, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_1.insert(Inequation_2); LeqChildren_4.insert(Inequation_2); } if(!inequationIsTrivial(Inequation_3, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_2.insert(Inequation_3); LeqChildren_3.insert(Inequation_3); LeqChildren_4.insert(Inequation_3); } // now we can create the kand nodes set EmptyChildren; // place holder for the following function calls t_Expression* kand_1; t_Expression* kand_2; t_Expression* kand_3; t_Expression* kand_4; assert(!(DiseqzChildren_1.empty() && LeqChildren_1.empty())); // original Inequation is trivial: should have been detected earlier if(!disequationIsFalse(Disequation_1, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm)) { kand_1 = CreateKandNode(EmptyChildren, DiseqzChildren_1, LeqChildren_1, pvt_em); assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); } assert(!(EqzChildren_2.empty() && LeqChildren_2.empty())); // original Inequation is trivial: should have been detected earlier if(!equationIsFalse(Equation_1, pvt_em) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_2 = CreateKandNode(EqzChildren_2, EmptyChildren, LeqChildren_2, pvt_em); assert(kand_2 != NULL); UnifiedVector.push_back(kand_2); } assert(!LeqChildren_3.empty()); // original Inequation is trivial: should have been detected earlier if(!inequationIsFalse(Inequation_1, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_3 = CreateKandNode(EmptyChildren, EmptyChildren, LeqChildren_3, pvt_em); assert(kand_3 != NULL); UnifiedVector.push_back(kand_3); } assert(!(DiseqzChildren_4.empty() && LeqChildren_4.empty())); // original Inequation is trivial: should have been detected earlier if(!disequationIsFalse(Disequation_1, pvt_em) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_4 = CreateKandNode(EmptyChildren, DiseqzChildren_4, LeqChildren_4, pvt_em); assert(kand_4 != NULL); UnifiedVector.push_back(kand_4); } assert(UnifiedVector.size() > 0); return true; } } else if(side_of_variable == RIGHT && type_of_coefficient == ORIGINAL) // Inequation is like t_1 <= ax+t_2 { t_Expression* LHS = getIthChild(Inequation, 0, pvt_em); // get the LHS node t_1 assert(LHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHS)); t_Expression* RHS = getIthChild(Inequation, 1, pvt_em); // get the RHS node ax+t_2 assert(RHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHS)); // get the monom ax in RHS t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(RHS, VarToUnify, MonomWithVariable, pvt_em, pvt_VariableList); // get the monom ax assert(MonomFound); assert(MonomWithVariable != NULL); // find the coefficient of x in the monom bvatom CoefficientOfMonom; bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefficientOfMonom, pvt_em, pvt_bvm); // a obtained assert(CoefficientFound); // We need to push back the following into UnifiedVector: // 1) kand of (t_2 \neq 0), (ax \le -t_2-1), and (t_1 \le t_2-1) // 2) kand of (t_2 = 0) and (t_1-t_2 <= ax) // 3) kand of (t_2 \neq 0), (t_1 \le t_2-1), and (t_1-t_2 <= ax) // 4) kand of (t_2 \neq 0), (ax <= -t_2-1) and (t_1-t_2 <= ax) // Let's create coefficient maps and constants for // t_2, t_2-1, -t_2-1, t_1-t_2, and ax set variables_to_exclude; bool CoefficientMapFound; // first, let's obtain coefficient map and constant of t_2 // t_2's coefficient map = RHS's coefficient map \ entry for VarToUnify variables_to_exclude.insert(VarToUnify); bvatom ConstantOft2; vector< pair< string, bvatom > > CoefficientMapOft2; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(RHS, variables_to_exclude, ConstantOft2, CoefficientMapOft2, pvt_em, pvt_bvm); assert(CoefficientMapFound); // Let's check if the Inequation is of the form t_1 <= ax; i.e. already unified if(CoefficientMapOft2.size() == 0 && pvt_bvm->checkBVForZero(ConstantOft2)) // t_2 is zero; already unified { constraint_already_unified = true; return true; } else { constraint_already_unified = false; // now, let's obtain coefficient map and constant of t_1 // t_1's coefficient map = LHS's coefficient map variables_to_exclude.clear(); bvatom ConstantOft1; vector< pair< string, bvatom > > CoefficientMapOft1; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(LHS, variables_to_exclude, ConstantOft1, CoefficientMapOft1, pvt_em, pvt_bvm); assert(CoefficientMapFound); // now, let's obtain coefficient map and constant of -t_2 from those of t_2 bvatom ConstantOfMinust2; vector< pair< string, bvatom > > CoefficientMapOfMinust2; ConstantOfMinust2 = pvt_bvm->addInverse(ConstantOft2); additiveInverse(CoefficientMapOft2, CoefficientMapOfMinust2, pvt_bvm); // now, let's obtain coefficient map and constant of t_2-1 from those of t_2 bvatom ConstantOft2MinusOne; vector< pair< string, bvatom > > CoefficientMapOft2MinusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOft2MinusOne = pvt_bvm->bvsub(ConstantOft2, pvt_bvm->getBVatom(p, OneString)); CoefficientMapOft2MinusOne = CoefficientMapOft2; // now, let's obtain coefficient map and constant of -t_2-1 from those of -t_2 bvatom ConstantOfMinust2MinusOne; vector< pair< string, bvatom > > CoefficientMapOfMinust2MinusOne; ConstantOfMinust2MinusOne = pvt_bvm->bvsub(ConstantOfMinust2, pvt_bvm->getBVatom(p, OneString)); CoefficientMapOfMinust2MinusOne = CoefficientMapOfMinust2; // now, let's obtain coefficient map and constant of t_1-t_2 from those of t_1 and -t_2 bvatom ConstantOft1Minust2; vector< pair< string, bvatom > > CoefficientMapOft1Minust2; ConstantOft1Minust2 = pvt_bvm->bvadd(ConstantOft1, ConstantOfMinust2); addition(CoefficientMapOft1, CoefficientMapOfMinust2, CoefficientMapOft1Minust2, pvt_bvm, pvt_VariableList); // now, let's obtain coefficient map and constant of ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CoefficientOfMonom)); // push back (x, a) into CoefficientMapOfax // Let's create kadd nodes for // t_2, t_2-1, -t_2-1, t_1-t_2, and ax t_Expression *KaddNodeFort2 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2, CoefficientMapOft2, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort2 != NULL); t_Expression *KaddNodeFort2MinusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2MinusOne, CoefficientMapOft2MinusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort2MinusOne != NULL); t_Expression *KaddNodeForMinust2MinusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinust2MinusOne, CoefficientMapOfMinust2MinusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinust2MinusOne != NULL); t_Expression *KaddNodeFort1Minust2 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft1Minust2, CoefficientMapOft1Minust2, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort1Minust2 != NULL); t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create (t_2 = 0): Let's call this Equation_1 // Let's also create (t_2 \neq 0): Let's call this Disequation_1 t_Expression* Equation_1 = CreateNode(equation_label, KaddNodeFort2, pvt_em); assert(Equation_1 != NULL); t_Expression* Disequation_1 = CreateNode(disequation_label, KaddNodeFort2, pvt_em); assert(Disequation_1 != NULL); // Let's create (ax <= -t_2-1), (t_1 <= t_2-1), and (t_1-t_2 <= ax) // Let's call them Inequation_1, Inequation_2, and Inequation_3 t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeForMinust2MinusOne, pvt_em); assert(Inequation_1 != NULL); t_Expression* Inequation_2 = CreateNode(inequation_label, LHS, KaddNodeFort2MinusOne, pvt_em); assert(Inequation_2 != NULL); t_Expression* Inequation_3 = CreateNode(inequation_label, KaddNodeFort1Minust2, KaddNodeForax, pvt_em); assert(Inequation_3 != NULL); // let's create the kand nodes now // let's first form their children set DiseqzChildren_1; // should contain Disequation_1 set LeqChildren_1; // should contain Inequation_1 and Inequation_2 set EqzChildren_2; // should contain Equation_1 set LeqChildren_2; // should contain Inequation_3 set DiseqzChildren_3; // should contain Disequation_1 set LeqChildren_3; // should contain Inequation_2 and Inequation_3 set DiseqzChildren_4; // should contain Disequation_1 set LeqChildren_4; // should contain Inequation_1 and Inequation_3 if(!disequationIsTrivial(Disequation_1, pvt_em)) //not trivial disequation { DiseqzChildren_1.insert(Disequation_1); DiseqzChildren_3.insert(Disequation_1); DiseqzChildren_4.insert(Disequation_1); } if(!equationIsTrivial(Equation_1, pvt_em)) //not trivial equation { EqzChildren_2.insert(Equation_1); } if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_1.insert(Inequation_1); LeqChildren_4.insert(Inequation_1); } if(!inequationIsTrivial(Inequation_2, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_1.insert(Inequation_2); LeqChildren_3.insert(Inequation_2); } if(!inequationIsTrivial(Inequation_3, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_2.insert(Inequation_3); LeqChildren_3.insert(Inequation_3); LeqChildren_4.insert(Inequation_3); } // now we can create the kand nodes set EmptyChildren; // place holder for the following function calls t_Expression* kand_1; t_Expression* kand_2; t_Expression* kand_3; t_Expression* kand_4; assert(!(DiseqzChildren_1.empty() && LeqChildren_1.empty())); // original Inequation is trivial: should have been detected earlier if(!disequationIsFalse(Disequation_1, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm)) { kand_1 = CreateKandNode(EmptyChildren, DiseqzChildren_1, LeqChildren_1, pvt_em); assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); } assert(!(EqzChildren_2.empty() && LeqChildren_2.empty())); // original Inequation is trivial: should have been detected earlier if(!equationIsFalse(Equation_1, pvt_em) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_2 = CreateKandNode(EqzChildren_2, EmptyChildren, LeqChildren_2, pvt_em); assert(kand_2 != NULL); UnifiedVector.push_back(kand_2); } assert(!(DiseqzChildren_3.empty() && LeqChildren_3.empty())); // original Inequation is trivial: should have been detected earlier if(!disequationIsFalse(Disequation_1, pvt_em) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_3 = CreateKandNode(EmptyChildren, DiseqzChildren_3, LeqChildren_3, pvt_em); assert(kand_3 != NULL); UnifiedVector.push_back(kand_3); } assert(!(DiseqzChildren_4.empty() && LeqChildren_4.empty())); // original Inequation is trivial: should have been detected earlier if(!disequationIsFalse(Disequation_1, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_4 = CreateKandNode(EmptyChildren, DiseqzChildren_4, LeqChildren_4, pvt_em); assert(kand_4 != NULL); UnifiedVector.push_back(kand_4); } assert(UnifiedVector.size() > 0); return true; } } else if(side_of_variable == LEFT && type_of_coefficient == NEGATED) // Inequation is like -ax+t_1 <= t_2 { constraint_already_unified = false; t_Expression* LHS = getIthChild(Inequation, 0, pvt_em); // get the LHS node -ax+t_1 assert(LHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHS)); t_Expression* RHS = getIthChild(Inequation, 1, pvt_em); // get the RHS node t_2 assert(RHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHS)); // get the monom -ax in LHS t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(LHS, VarToUnify, MonomWithVariable, pvt_em, pvt_VariableList); // get the monom -ax assert(MonomFound); assert(MonomWithVariable != NULL); // find the coefficient of x in the monom bvatom CoefficientOfMonom; bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefficientOfMonom, pvt_em, pvt_bvm); // -a obtained assert(CoefficientFound); bvatom CommonCoefficient = pvt_bvm->addInverse(CoefficientOfMonom); // a obtained // We need to push back the following into UnifiedVector: // 1) kand of (t_1 \neq 0), (ax \neq 0), (ax \le t_1), and (t_1 \le t_2) // 2) kand of (t_2 = 0) and (ax = 0) // 3) kand of (t_1 = 0), (t_2 - t_1 \neq 0), and (t_1 - t_2 <= ax) // 4) kand of (ax \neq 0), (ax <= t_1), (t_2 - t_1 \neq 0), and (t_1 - t_2 <= ax) // 5) kand of (t_1 \neq 0), (t_1 \le t_2), and (ax = 0) // 6) kand of (t_1 \neq 0), (t_1 \le t_2), (t_2 - t_1 \neq 0), and (t_1 - t_2 <= ax) // Let's create coefficient maps and constants for // t_1, t_1-t_2, t_2-t_1, and ax set variables_to_exclude; bool CoefficientMapFound; // first, let's obtain coefficient map and constant of t_1 // t_1's coefficient map = LHS's coefficient map \ entry for VarToUnify variables_to_exclude.insert(VarToUnify); bvatom ConstantOft1; vector< pair< string, bvatom > > CoefficientMapOft1; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(LHS, variables_to_exclude, ConstantOft1, CoefficientMapOft1, pvt_em, pvt_bvm); assert(CoefficientMapFound); // now, let's obtain coefficient map and constant of t_2 // t_2's coefficient map = RHS's coefficient map variables_to_exclude.clear(); bvatom ConstantOft2; vector< pair< string, bvatom > > CoefficientMapOft2; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(RHS, variables_to_exclude, ConstantOft2, CoefficientMapOft2, pvt_em, pvt_bvm); assert(CoefficientMapFound); // now, let's obtain coefficient map and constant of -t_1 from those of t_1 bvatom ConstantOfMinust1; vector< pair< string, bvatom > > CoefficientMapOfMinust1; ConstantOfMinust1 = pvt_bvm->addInverse(ConstantOft1); additiveInverse(CoefficientMapOft1, CoefficientMapOfMinust1, pvt_bvm); // now, let's obtain coefficient map and constant of t_2-t_1 from those of t_2 and -t_1 bvatom ConstantOft2Minust1; vector< pair< string, bvatom > > CoefficientMapOft2Minust1; ConstantOft2Minust1 = pvt_bvm->bvadd(ConstantOft2, ConstantOfMinust1); addition(CoefficientMapOft2, CoefficientMapOfMinust1, CoefficientMapOft2Minust1, pvt_bvm, pvt_VariableList); // now, let's obtain coefficient map and constant of -t_2 from those of t_2 bvatom ConstantOfMinust2; vector< pair< string, bvatom > > CoefficientMapOfMinust2; ConstantOfMinust2 = pvt_bvm->addInverse(ConstantOft2); additiveInverse(CoefficientMapOft2, CoefficientMapOfMinust2, pvt_bvm); // now, let's obtain coefficient map and constant of t_1-t_2 from those of t_1 and -t_2 bvatom ConstantOft1Minust2; vector< pair< string, bvatom > > CoefficientMapOft1Minust2; ConstantOft1Minust2 = pvt_bvm->bvadd(ConstantOft1, ConstantOfMinust2); addition(CoefficientMapOft1, CoefficientMapOfMinust2, CoefficientMapOft1Minust2, pvt_bvm, pvt_VariableList); // now, let's obtain coefficient map and constant of ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create kadd nodes for // t_1, t_1-t_2, t_2-t_1, and ax t_Expression *KaddNodeFort1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft1, CoefficientMapOft1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort1 != NULL); t_Expression *KaddNodeFort1Minust2 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft1Minust2, CoefficientMapOft1Minust2, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort1Minust2 != NULL); t_Expression *KaddNodeFort2Minust1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2Minust1, CoefficientMapOft2Minust1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort2Minust1 != NULL); t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create (t_1 = 0), (t_2 = 0), and (ax = 0): Let's call them Equation_1, Equation_2, and Equation_3 t_Expression* Equation_1 = CreateNode(equation_label, KaddNodeFort1, pvt_em); assert(Equation_1 != NULL); t_Expression* Equation_2 = CreateNode(equation_label, RHS, pvt_em); assert(Equation_2 != NULL); t_Expression* Equation_3 = CreateNode(equation_label, KaddNodeForax, pvt_em); assert(Equation_3 != NULL); // Let's create (t_1 \neq 0), (ax \neq 0), and (t_2-t_1 \neq 0): Let's call them Disequation_1, Disequation_2, and Disequation_3 t_Expression* Disequation_1 = CreateNode(disequation_label, KaddNodeFort1, pvt_em); assert(Disequation_1 != NULL); t_Expression* Disequation_2 = CreateNode(disequation_label, KaddNodeForax, pvt_em); assert(Disequation_2 != NULL); t_Expression* Disequation_3 = CreateNode(disequation_label, KaddNodeFort2Minust1, pvt_em); assert(Disequation_3 != NULL); // Let's create (ax <= t_1), (t_1 <= t_2), and (t_1-t_2 <= ax): Let's call them Inequation_1, Inequation_2, and Inequation_3 t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeFort1, pvt_em); assert(Inequation_1 != NULL); t_Expression* Inequation_2 = CreateNode(inequation_label, KaddNodeFort1, RHS, pvt_em); assert(Inequation_2 != NULL); t_Expression* Inequation_3 = CreateNode(inequation_label, KaddNodeFort1Minust2, KaddNodeForax, pvt_em); assert(Inequation_3 != NULL); // let's create the kand nodes now // let's first form their children set DiseqzChildren_1; // should contain Disequation_1 and Disequation_2 set LeqChildren_1; // should contain Inequation_1 and Inequation_2 set EqzChildren_2; // should contain Equation_2 and Equation_3 set EqzChildren_3; // should contain Equation_1 set DiseqzChildren_3; // should contain Disequation_3 set LeqChildren_3; // should contain Inequation_3 set DiseqzChildren_4; // should contain Disequation_2 and Disequation_3 set LeqChildren_4; // should contain Inequation_1 and Inequation_3 set EqzChildren_5; // should contain Equation_3 set DiseqzChildren_5; // should contain Disequation_1 set LeqChildren_5; // should contain Inequation_2 set DiseqzChildren_6; // should contain Disequation_1 and Disequation_3 set LeqChildren_6; // should contain Inequation_2 and Inequation_3 if(!equationIsTrivial(Equation_1, pvt_em)) //not trivial equation { EqzChildren_3.insert(Equation_1); } if(!equationIsTrivial(Equation_2, pvt_em)) //not trivial equation { EqzChildren_2.insert(Equation_2); } if(!equationIsTrivial(Equation_3, pvt_em)) //not trivial equation { EqzChildren_2.insert(Equation_3); EqzChildren_5.insert(Equation_3); } if(!disequationIsTrivial(Disequation_1, pvt_em)) //not trivial disequation { DiseqzChildren_1.insert(Disequation_1); DiseqzChildren_5.insert(Disequation_1); DiseqzChildren_6.insert(Disequation_1); } if(!disequationIsTrivial(Disequation_2, pvt_em)) //not trivial disequation { DiseqzChildren_1.insert(Disequation_2); DiseqzChildren_4.insert(Disequation_2); } if(!disequationIsTrivial(Disequation_3, pvt_em)) //not trivial disequation { DiseqzChildren_3.insert(Disequation_3); DiseqzChildren_4.insert(Disequation_3); DiseqzChildren_6.insert(Disequation_3); } if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_1.insert(Inequation_1); LeqChildren_4.insert(Inequation_1); } if(!inequationIsTrivial(Inequation_2, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_1.insert(Inequation_2); LeqChildren_5.insert(Inequation_2); LeqChildren_6.insert(Inequation_2); } if(!inequationIsTrivial(Inequation_3, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_3.insert(Inequation_3); LeqChildren_4.insert(Inequation_3); LeqChildren_6.insert(Inequation_3); } // now we can create the kand nodes set EmptyChildren; // place holder for the following function calls t_Expression* kand_1; t_Expression* kand_2; t_Expression* kand_3; t_Expression* kand_4; t_Expression* kand_5; t_Expression* kand_6; assert(!(DiseqzChildren_1.empty() && LeqChildren_1.empty())); // original Inequation is trivial: should have been detected earlier if(!disequationIsFalse(Disequation_1, pvt_em) && !disequationIsFalse(Disequation_2, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm)) { kand_1 = CreateKandNode(EmptyChildren, DiseqzChildren_1, LeqChildren_1, pvt_em); assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); } assert(!EqzChildren_2.empty()); // original Inequation is trivial: should have been detected earlier if(!equationIsFalse(Equation_2, pvt_em) && !equationIsFalse(Equation_3, pvt_em)) { kand_2 = CreateKandNode(EqzChildren_2, EmptyChildren, EmptyChildren, pvt_em); assert(kand_2 != NULL); UnifiedVector.push_back(kand_2); } assert(!(EqzChildren_3.empty() && DiseqzChildren_3.empty() && LeqChildren_3.empty())); // original Inequation is trivial: should have been detected earlier if(!equationIsFalse(Equation_1, pvt_em) && !disequationIsFalse(Disequation_3, pvt_em) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_3 = CreateKandNode(EqzChildren_3, DiseqzChildren_3, LeqChildren_3, pvt_em); assert(kand_3 != NULL); UnifiedVector.push_back(kand_3); } assert(!(DiseqzChildren_4.empty() && LeqChildren_4.empty())); // original Inequation is trivial: should have been detected earlier if(!disequationIsFalse(Disequation_2, pvt_em) && !disequationIsFalse(Disequation_3, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_4 = CreateKandNode(EmptyChildren, DiseqzChildren_4, LeqChildren_4, pvt_em); assert(kand_4 != NULL); UnifiedVector.push_back(kand_4); } assert(!(EqzChildren_5.empty() && DiseqzChildren_5.empty() && LeqChildren_5.empty())); // original Inequation is trivial: should have been detected earlier if(!equationIsFalse(Equation_3, pvt_em) && !disequationIsFalse(Disequation_1, pvt_em) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm)) { kand_5 = CreateKandNode(EqzChildren_5, DiseqzChildren_5, LeqChildren_5, pvt_em); assert(kand_5 != NULL); UnifiedVector.push_back(kand_5); } assert(!(DiseqzChildren_6.empty() && LeqChildren_6.empty())); // original Inequation is trivial: should have been detected earlier if(!disequationIsFalse(Disequation_1, pvt_em) && !disequationIsFalse(Disequation_3, pvt_em) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_6 = CreateKandNode(EmptyChildren, DiseqzChildren_6, LeqChildren_6, pvt_em); assert(kand_6 != NULL); UnifiedVector.push_back(kand_6); } assert(UnifiedVector.size() > 0); return true; } else if(side_of_variable == RIGHT && type_of_coefficient == NEGATED) // Inequation is like t_1 <= -ax+t_2 { constraint_already_unified = false; t_Expression* LHS = getIthChild(Inequation, 0, pvt_em); // get the LHS node t_1 assert(LHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHS)); t_Expression* RHS = getIthChild(Inequation, 1, pvt_em); // get the RHS node -ax+t_2 assert(RHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHS)); // get the monom -ax in RHS t_Expression* MonomWithVariable; bool MonomFound = findMonomOfKaddNodeWithGivenVariable(RHS, VarToUnify, MonomWithVariable, pvt_em, pvt_VariableList); // get the monom -ax assert(MonomFound); assert(MonomWithVariable != NULL); // find the coefficient of x in the monom bvatom CoefficientOfMonom; bool CoefficientFound = findCoefficientOfMonom(MonomWithVariable, CoefficientOfMonom, pvt_em, pvt_bvm); // -a obtained assert(CoefficientFound); bvatom CommonCoefficient = pvt_bvm->addInverse(CoefficientOfMonom); // a obtained // We need to push back the following into UnifiedVector: // 1) kand of (t_2 \neq 0), (ax = 0), and (t_1 \le t_2-1) // 2) kand of (t_2 \neq 0), (t_2 + 1 \le ax), (-t_2 - 1 \neq 0), and (t_1 \le t_2-1) // 3) kand of (t_2 = 0) and (t_1 - t_2 = 0) // 4) kand of (t_2 = 0), (ax \neq 0), and (ax \le t_2 - t_1) // 5) kand of (t_1 \le t_2 - 1), (t_1 - t_2 = 0), and (t_2 \neq 0) // 6) kand of (t_1 \le t_2 - 1), (ax \neq 0), (ax \le t_2 - t_1), and (t_2 \neq 0) // 7) kand of (t_2 \neq 0), (ax = 0), and (t_1 - t_2 = 0) // 8) kand of (t_2 \neq 0), (-t_2 - 1 \neq 0), (t_2 + 1 \le ax), and (t_1 - t_2 = 0) // 9) kand of (t_2 \neq 0), (-t_2 - 1 \neq 0), (t_2 + 1 \le ax), (ax \neq 0), and (ax \le t_2 - t_1) // Let's create coefficient maps and constants for // t_2, t_1-t_2, t_2-t_1, t_2+1, t_2-1, -t_2-1 and ax set variables_to_exclude; bool CoefficientMapFound; // first, let's obtain coefficient map and constant of t_2 // t_2's coefficient map = RHS's coefficient map \ entry for VarToUnify variables_to_exclude.insert(VarToUnify); bvatom ConstantOft2; vector< pair< string, bvatom > > CoefficientMapOft2; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(RHS, variables_to_exclude, ConstantOft2, CoefficientMapOft2, pvt_em, pvt_bvm); assert(CoefficientMapFound); // now, let's obtain coefficient map and constant of t_1 // t_1's coefficient map = LHS's coefficient map variables_to_exclude.clear(); bvatom ConstantOft1; vector< pair< string, bvatom > > CoefficientMapOft1; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(LHS, variables_to_exclude, ConstantOft1, CoefficientMapOft1, pvt_em, pvt_bvm); assert(CoefficientMapFound); // now, let's obtain coefficient map and constant of -t_1 from those of t_1 bvatom ConstantOfMinust1; vector< pair< string, bvatom > > CoefficientMapOfMinust1; ConstantOfMinust1 = pvt_bvm->addInverse(ConstantOft1); additiveInverse(CoefficientMapOft1, CoefficientMapOfMinust1, pvt_bvm); // now, let's obtain coefficient map and constant of t_2-t_1 from those of t_2 and -t_1 bvatom ConstantOft2Minust1; vector< pair< string, bvatom > > CoefficientMapOft2Minust1; ConstantOft2Minust1 = pvt_bvm->bvadd(ConstantOft2, ConstantOfMinust1); addition(CoefficientMapOft2, CoefficientMapOfMinust1, CoefficientMapOft2Minust1, pvt_bvm, pvt_VariableList); // now, let's obtain coefficient map and constant of -t_2 from those of t_2 bvatom ConstantOfMinust2; vector< pair< string, bvatom > > CoefficientMapOfMinust2; ConstantOfMinust2 = pvt_bvm->addInverse(ConstantOft2); additiveInverse(CoefficientMapOft2, CoefficientMapOfMinust2, pvt_bvm); // now, let's obtain coefficient map and constant of t_1-t_2 from those of t_1 and -t_2 bvatom ConstantOft1Minust2; vector< pair< string, bvatom > > CoefficientMapOft1Minust2; ConstantOft1Minust2 = pvt_bvm->bvadd(ConstantOft1, ConstantOfMinust2); addition(CoefficientMapOft1, CoefficientMapOfMinust2, CoefficientMapOft1Minust2, pvt_bvm, pvt_VariableList); // now, let's obtain coefficient map and constant of t_2-1 from those of t_2 bvatom ConstantOft2MinusOne; vector< pair< string, bvatom > > CoefficientMapOft2MinusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOft2MinusOne = pvt_bvm->bvsub(ConstantOft2, pvt_bvm->getBVatom(p, OneString)); CoefficientMapOft2MinusOne = CoefficientMapOft2; // now, let's obtain coefficient map and constant of t_2+1 from those of t_2 bvatom ConstantOft2PlusOne; vector< pair< string, bvatom > > CoefficientMapOft2PlusOne; ConstantOft2PlusOne = pvt_bvm->bvadd(ConstantOft2, pvt_bvm->getBVatom(p, OneString)); CoefficientMapOft2PlusOne = CoefficientMapOft2; // now, let's obtain coefficient map and constant of -t_2-1 from those of -t_2 bvatom ConstantOfMinust2MinusOne; vector< pair< string, bvatom > > CoefficientMapOfMinust2MinusOne; ConstantOfMinust2MinusOne = pvt_bvm->bvsub(ConstantOfMinust2, pvt_bvm->getBVatom(p, OneString)); CoefficientMapOfMinust2MinusOne = CoefficientMapOfMinust2; // now, let's obtain coefficient map and constant of ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create kadd nodes for // t_2, t_1-t_2, t_2-t_1, t_2+1, t_2-1, -t_2-1 and ax t_Expression *KaddNodeFort2 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2, CoefficientMapOft2, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort2 != NULL); t_Expression *KaddNodeFort1Minust2 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft1Minust2, CoefficientMapOft1Minust2, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort1Minust2 != NULL); t_Expression *KaddNodeFort2Minust1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2Minust1, CoefficientMapOft2Minust1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort2Minust1 != NULL); t_Expression *KaddNodeFort2PlusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2PlusOne, CoefficientMapOft2PlusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort2PlusOne != NULL); t_Expression *KaddNodeFort2MinusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2MinusOne, CoefficientMapOft2MinusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeFort2MinusOne != NULL); t_Expression *KaddNodeForMinust2MinusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinust2MinusOne, CoefficientMapOfMinust2MinusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinust2MinusOne != NULL); t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create (ax = 0), (t_2 = 0), and (t_1 - t_2 = 0) : Let's call them Equation_1, Equation_2, and Equation_3 t_Expression* Equation_1 = CreateNode(equation_label, KaddNodeForax, pvt_em); assert(Equation_1 != NULL); t_Expression* Equation_2 = CreateNode(equation_label, KaddNodeFort2, pvt_em); assert(Equation_2 != NULL); t_Expression* Equation_3 = CreateNode(equation_label, KaddNodeFort1Minust2, pvt_em); assert(Equation_3 != NULL); // Let's create (t_2 \neq 0), (-t_2-1 \neq 0), and (ax \neq 0): Let's call them Disequation_1, Disequation_2, and Disequation_3 t_Expression* Disequation_1 = CreateNode(disequation_label, KaddNodeFort2, pvt_em); assert(Disequation_1 != NULL); t_Expression* Disequation_2 = CreateNode(disequation_label, KaddNodeForMinust2MinusOne, pvt_em); assert(Disequation_2 != NULL); t_Expression* Disequation_3 = CreateNode(disequation_label, KaddNodeForax, pvt_em); assert(Disequation_3 != NULL); // Let's create (t_1 <= t_2-1), (t_2+1 <= ax), and (ax <= t_2-t_1): Let's call them Inequation_1, Inequation_2, and Inequation_3 t_Expression* Inequation_1 = CreateNode(inequation_label, LHS, KaddNodeFort2MinusOne, pvt_em); assert(Inequation_1 != NULL); t_Expression* Inequation_2 = CreateNode(inequation_label, KaddNodeFort2PlusOne, KaddNodeForax, pvt_em); assert(Inequation_2 != NULL); t_Expression* Inequation_3 = CreateNode(inequation_label, KaddNodeForax, KaddNodeFort2Minust1, pvt_em); assert(Inequation_3 != NULL); // let's create the kand nodes now // let's first form their children set EqzChildren_1; // should contain Equation_1 set DiseqzChildren_1; // should contain Disequation_1 set LeqChildren_1; // should contain Inequation_1 set DiseqzChildren_2; // should contain Disequation_1 and Disequation_2 set LeqChildren_2; // should contain Inequation_1 and Inequation_2 set EqzChildren_3; // should contain Equation_2 and Equation_3 set EqzChildren_4; // should contain Equation_2 set DiseqzChildren_4; // should contain Disequation_3 set LeqChildren_4; // should contain Inequation_3 set EqzChildren_5; // should contain Equation_3 set DiseqzChildren_5; // should contain Disequation_1 set LeqChildren_5; // should contain Inequation_1 set DiseqzChildren_6; // should contain Disequation_1 and Disequation_3 set LeqChildren_6; // should contain Inequation_1 and Inequation_3 set EqzChildren_7; // should contain Equation_1 and Equation_3 set DiseqzChildren_7; // should contain Disequation_1 set EqzChildren_8; // should contain Equation_3 set DiseqzChildren_8; // should contain Disequation_1 and Disequation_2 set LeqChildren_8; // should contain Inequation_2 set DiseqzChildren_9; // should contain Disequation_1, Disequation_2 and Disequation_3 set LeqChildren_9; // should contain Inequation_2 and Inequation_3 if(!equationIsTrivial(Equation_1, pvt_em)) //not trivial equation { EqzChildren_1.insert(Equation_1); EqzChildren_7.insert(Equation_1); } if(!equationIsTrivial(Equation_2, pvt_em)) //not trivial equation { EqzChildren_3.insert(Equation_2); EqzChildren_4.insert(Equation_2); } if(!equationIsTrivial(Equation_3, pvt_em)) //not trivial equation { EqzChildren_3.insert(Equation_3); EqzChildren_5.insert(Equation_3); EqzChildren_7.insert(Equation_3); EqzChildren_8.insert(Equation_3); } if(!disequationIsTrivial(Disequation_1, pvt_em)) //not trivial disequation { DiseqzChildren_1.insert(Disequation_1); DiseqzChildren_2.insert(Disequation_1); DiseqzChildren_5.insert(Disequation_1); DiseqzChildren_6.insert(Disequation_1); DiseqzChildren_7.insert(Disequation_1); DiseqzChildren_8.insert(Disequation_1); DiseqzChildren_9.insert(Disequation_1); } if(!disequationIsTrivial(Disequation_2, pvt_em)) //not trivial disequation { DiseqzChildren_2.insert(Disequation_2); DiseqzChildren_8.insert(Disequation_2); DiseqzChildren_9.insert(Disequation_2); } if(!disequationIsTrivial(Disequation_3, pvt_em)) //not trivial disequation { DiseqzChildren_4.insert(Disequation_3); DiseqzChildren_6.insert(Disequation_3); DiseqzChildren_9.insert(Disequation_3); } if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_1.insert(Inequation_1); LeqChildren_2.insert(Inequation_1); LeqChildren_5.insert(Inequation_1); LeqChildren_6.insert(Inequation_1); } if(!inequationIsTrivial(Inequation_2, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_2.insert(Inequation_2); LeqChildren_8.insert(Inequation_2); LeqChildren_9.insert(Inequation_2); } if(!inequationIsTrivial(Inequation_3, pvt_em, pvt_bvm)) //not trivial inequation { LeqChildren_4.insert(Inequation_3); LeqChildren_6.insert(Inequation_3); LeqChildren_9.insert(Inequation_3); } // now we can create the kand nodes set EmptyChildren; // place holder for the following function calls t_Expression* kand_1; t_Expression* kand_2; t_Expression* kand_3; t_Expression* kand_4; t_Expression* kand_5; t_Expression* kand_6; t_Expression* kand_7; t_Expression* kand_8; t_Expression* kand_9; assert(!(EqzChildren_1.empty() && DiseqzChildren_1.empty() && LeqChildren_1.empty())); if(!equationIsFalse(Equation_1, pvt_em) && !disequationIsFalse(Disequation_1, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm)) { kand_1 = CreateKandNode(EqzChildren_1, DiseqzChildren_1, LeqChildren_1, pvt_em); assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); } assert(!(DiseqzChildren_2.empty() && LeqChildren_2.empty())); if(!disequationIsFalse(Disequation_1, pvt_em) && !disequationIsFalse(Disequation_2, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm)) { kand_2 = CreateKandNode(EmptyChildren, DiseqzChildren_2, LeqChildren_2, pvt_em); assert(kand_2 != NULL); UnifiedVector.push_back(kand_2); } assert(!EqzChildren_3.empty()); if(!equationIsFalse(Equation_2, pvt_em) && !equationIsFalse(Equation_3, pvt_em)) { kand_3 = CreateKandNode(EqzChildren_3, EmptyChildren, EmptyChildren, pvt_em); assert(kand_3 != NULL); UnifiedVector.push_back(kand_3); } assert(!(EqzChildren_4.empty() && DiseqzChildren_4.empty() && LeqChildren_4.empty())); if(!equationIsFalse(Equation_2, pvt_em) && !disequationIsFalse(Disequation_3, pvt_em) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_4 = CreateKandNode(EqzChildren_4, DiseqzChildren_4, LeqChildren_4, pvt_em); assert(kand_4 != NULL); UnifiedVector.push_back(kand_4); } assert(!(EqzChildren_5.empty() && DiseqzChildren_5.empty() && LeqChildren_5.empty())); if(!equationIsFalse(Equation_3, pvt_em) && !disequationIsFalse(Disequation_1, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm)) { kand_5 = CreateKandNode(EqzChildren_5, DiseqzChildren_5, LeqChildren_5, pvt_em); assert(kand_5 != NULL); UnifiedVector.push_back(kand_5); } assert(!(DiseqzChildren_6.empty() && LeqChildren_6.empty())); if(!disequationIsFalse(Disequation_1, pvt_em) && !disequationIsFalse(Disequation_3, pvt_em) && !inequationIsFalse(Inequation_1, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_6 = CreateKandNode(EmptyChildren, DiseqzChildren_6, LeqChildren_6, pvt_em); assert(kand_6 != NULL); UnifiedVector.push_back(kand_6); } assert(!(EqzChildren_7.empty() && DiseqzChildren_7.empty())); if(!equationIsFalse(Equation_1, pvt_em) && !equationIsFalse(Equation_3, pvt_em) && !disequationIsFalse(Disequation_1, pvt_em)) { kand_7 = CreateKandNode(EqzChildren_7, DiseqzChildren_7, EmptyChildren, pvt_em); assert(kand_7 != NULL); UnifiedVector.push_back(kand_7); } assert(!(EqzChildren_8.empty() && DiseqzChildren_8.empty() && LeqChildren_8.empty())); if(!equationIsFalse(Equation_3, pvt_em) && !disequationIsFalse(Disequation_1, pvt_em) && !disequationIsFalse(Disequation_2, pvt_em) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm)) { kand_8 = CreateKandNode(EqzChildren_8, DiseqzChildren_8, LeqChildren_8, pvt_em); assert(kand_8 != NULL); UnifiedVector.push_back(kand_8); } assert(!(DiseqzChildren_9.empty() && LeqChildren_9.empty())); if(!disequationIsFalse(Disequation_1, pvt_em) && !disequationIsFalse(Disequation_2, pvt_em) && !disequationIsFalse(Disequation_3, pvt_em) && !inequationIsFalse(Inequation_2, pvt_em, pvt_bvm) && !inequationIsFalse(Inequation_3, pvt_em, pvt_bvm)) { kand_9 = CreateKandNode(EmptyChildren, DiseqzChildren_9, LeqChildren_9, pvt_em); assert(kand_9 != NULL); UnifiedVector.push_back(kand_9); } assert(UnifiedVector.size() > 0); return true; } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected value for side_of_variable and type_of_coefficient in function t_Project::unifyInequationWithVariableOnOneSide", pvt_logFile, c_RunLevelVerbosity); return false; } }// end of function // Given an inequation of the form a.x+b_1 \le a.x+b_2, where b_1 and b_2 are constants, // this function performs the following: // // (1) If type_of_coefficient is ORIGINAL, then // // it generates the following Boolean combinations unified w.r.t. x: // // (ax \le -b_2-1) if b_1 = 0 and b_2\neq 0 // (ax \ge -b_1) if b_2 = 0 and b_1\neq 0 // (ax \le -b_2-1)\vee (ax \ge -b_1) if b_1 < b_2 and b_1\neq 0 // (ax \le -b_2-1)\wedge (ax \ge -b_1) if b_1 > b_2 and b_2\neq 0 // // (2) If type_of_coefficient is NEGATED, then // it generates the following Boolean combination unified w.r.t. x: // // (ax=0)\vee ((b_2+1 \neq 0)\wedge (ax \ge b_1+1)) if b_1=0 and b_2\neq 0 // ((ax \neq 0)\wedge (ax \le b_1)) if b_2=0 and b_1\neq 0 // (ax=0)\vee ((b_2+1 \neq 0)\wedge (ax \ge b_2+1))\vee ((ax \neq 0)\wedge (ax \le b_1)) if b_1 < b_2 and b_1\neq 0 // ((ax \ge b_2+1)\wedge (ax \le b_1)) if b_1 > b_2 and b_2\neq 0 // // constraint_already_unified is always set to false. // // bool t_Project::unifyInequationWithVariableOnBothSides(t_Expression* Inequation, const string &VarToUnify, t_side_of_variable_in_unification side_of_variable, t_type_of_coefficient_in_unification type_of_coefficient, vector &UnifiedVector, bool &constraint_already_unified) { constraint_already_unified = false; assert(Inequation != NULL); assert("leq" == pvt_em->getLabelOfExpression(Inequation)); // Find p, i.e. width of VarToUnify int p = getWidthOfVariable(VarToUnify, pvt_WidthTable); assert(p > 0); string inequation_label = "leq"; string equation_label = "eqz"; string disequation_label = "diseqz"; // In general, Inequation is a_1.x+b_1 \le a_2.x+b_2 // However, this function accepts cases only with a_1 = a_2 = a and b_1 and b_2 are constants // Let's 1) ensure that a_1 = a_2 = a and b_1 and b_2 are constants // 2) obtain a, b_1, and b_2 t_Expression* LHS = getIthChild(Inequation, 0, pvt_em); // get the LHS node a_1.x+b_1 assert(LHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(LHS)); t_Expression* RHS = getIthChild(Inequation, 1, pvt_em); // get the RHS node a_2.x+b_2 assert(RHS != NULL); assert("kadd" == pvt_em->getLabelOfExpression(RHS)); set variables_to_exclude;// no variables to exclude bool CoefficientMapFound; // Let's obtain coefficient maps and constants of LHS node a_1.x+b_1 and RHS node a_2.x+b_2 bvatom ConstantOfLHS, ConstantOfRHS; vector< pair< string, bvatom > > CoefficientMapOfLHS, CoefficientMapOfRHS; CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(LHS, variables_to_exclude, ConstantOfLHS, CoefficientMapOfLHS, pvt_em, pvt_bvm); assert(CoefficientMapFound); CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(RHS, variables_to_exclude, ConstantOfRHS, CoefficientMapOfRHS, pvt_em, pvt_bvm); assert(CoefficientMapFound); assert(CoefficientMapOfLHS.size() == 1 && CoefficientMapOfRHS.size() == 1); assert(CoefficientMapOfLHS[0].first == VarToUnify); assert(CoefficientMapOfRHS[0].first == VarToUnify); // x is the only variable on both the sides assert(pvt_bvm->checkBVEquality(CoefficientMapOfLHS[0].second , CoefficientMapOfRHS[0].second)); // a_1 == a_2 assert(!(pvt_bvm->checkBVEquality(ConstantOfLHS, ConstantOfRHS))); // b_1 != b_2; otherwise Inequation is like ax + b <= ax + b; i.e. true; why unify? if(type_of_coefficient == ORIGINAL) { bvatom CommonCoefficient = CoefficientMapOfLHS[0].second; // a = a_1 if(pvt_bvm->checkBVForZero(ConstantOfLHS)) // b_1 = 0; since b_1 != b_2, b_2 != 0 { // we have (ax+b_1 \le ax+b_2) \equiv (ax \le -b_2-1) when b_1 = 0 and b_2\neq 0 // Let's create constant and coefficient map for ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create constant and coefficient map for -b_2-1 bvatom ConstantOfMinusb2MinusOne; vector< pair< string, bvatom > > CoefficientMapOfMinusb2MinusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfMinusb2MinusOne = pvt_bvm->bvsub(pvt_bvm->addInverse(ConstantOfRHS), pvt_bvm->getBVatom(p, OneString)); // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create kadd node for -b_2-1 t_Expression *KaddNodeForMinusb2MinusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinusb2MinusOne, CoefficientMapOfMinusb2MinusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinusb2MinusOne != NULL); // Let's create (ax \le -b_2-1) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeForMinusb2MinusOne, pvt_em); assert(Inequation_1 != NULL); assert(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)); //I don't think it can be a trivial inequation UnifiedVector.push_back(Inequation_1); return true; } else if(pvt_bvm->checkBVForZero(ConstantOfRHS)) // b_2 = 0; since b_1 != b_2, b_1 != 0 { // we have (ax+b_1 \le ax+b_2) \equiv (ax \ge -b_1) when b_2 = 0 and b_1\neq 0 // Let's create constant and coefficient map for ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create constant and coefficient map for -b_1 bvatom ConstantOfMinusb1; vector< pair< string, bvatom > > CoefficientMapOfMinusb1; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfMinusb1 = pvt_bvm->addInverse(ConstantOfLHS); // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create kadd node for -b_1 t_Expression *KaddNodeForMinusb1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinusb1, CoefficientMapOfMinusb1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinusb1 != NULL); // Let's create (ax \ge -b_1) , i.e. (-b_1 \le ax) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForMinusb1, KaddNodeForax, pvt_em); assert(Inequation_1 != NULL); assert(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)); //I don't think it can be a trivial inequation UnifiedVector.push_back(Inequation_1); return true; } else if(pvt_bvm->checkBVGreaterThan(ConstantOfRHS, ConstantOfLHS)) { // we have (ax+b_1 \le ax+b_2) \equiv ((ax \le -b_2-1)\vee (ax \ge -b_1)) when b_2 > b_1 and b_1 != 0 // Let's create constant and coefficient map for ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create constant and coefficient map for -b_2-1 bvatom ConstantOfMinusb2MinusOne; vector< pair< string, bvatom > > CoefficientMapOfMinusb2MinusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfMinusb2MinusOne = pvt_bvm->bvsub(pvt_bvm->addInverse(ConstantOfRHS), pvt_bvm->getBVatom(p, OneString)); // Let's create constant and coefficient map for -b_1 bvatom ConstantOfMinusb1; vector< pair< string, bvatom > > CoefficientMapOfMinusb1; ConstantOfMinusb1 = pvt_bvm->addInverse(ConstantOfLHS); // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create kadd node for -b_2-1 t_Expression *KaddNodeForMinusb2MinusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinusb2MinusOne, CoefficientMapOfMinusb2MinusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinusb2MinusOne != NULL); // Let's create kadd node for -b_1 t_Expression *KaddNodeForMinusb1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinusb1, CoefficientMapOfMinusb1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinusb1 != NULL); // Let's create (ax \le -b_2-1) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeForMinusb2MinusOne, pvt_em); assert(Inequation_1 != NULL); // Let's create (ax \ge -b_1) , i.e. (-b_1 \le ax) t_Expression* Inequation_2 = CreateNode(inequation_label, KaddNodeForMinusb1, KaddNodeForax, pvt_em); assert(Inequation_2 != NULL); assert(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)); assert(!inequationIsTrivial(Inequation_2, pvt_em, pvt_bvm)); //I don't think any of these can be a trivial inequation UnifiedVector.push_back(Inequation_1); UnifiedVector.push_back(Inequation_2); return true; } else if(pvt_bvm->checkBVGreaterThan(ConstantOfLHS, ConstantOfRHS)) { // we have (ax+b_1 \le ax+b_2) \equiv ((ax \le -b_2-1)\wedge (ax \ge -b_1)) when b_1 > b_2 and b_2 != 0 // Let's create constant and coefficient map for ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create constant and coefficient map for -b_2-1 bvatom ConstantOfMinusb2MinusOne; vector< pair< string, bvatom > > CoefficientMapOfMinusb2MinusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfMinusb2MinusOne = pvt_bvm->bvsub(pvt_bvm->addInverse(ConstantOfRHS), pvt_bvm->getBVatom(p, OneString)); // Let's create constant and coefficient map for -b_1 bvatom ConstantOfMinusb1; vector< pair< string, bvatom > > CoefficientMapOfMinusb1; ConstantOfMinusb1 = pvt_bvm->addInverse(ConstantOfLHS); // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create kadd node for -b_2-1 t_Expression *KaddNodeForMinusb2MinusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinusb2MinusOne, CoefficientMapOfMinusb2MinusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinusb2MinusOne != NULL); // Let's create kadd node for -b_1 t_Expression *KaddNodeForMinusb1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfMinusb1, CoefficientMapOfMinusb1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForMinusb1 != NULL); // Let's create (ax \le -b_2-1) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeForMinusb2MinusOne, pvt_em); assert(Inequation_1 != NULL); // Let's create (ax \ge -b_1) , i.e. (-b_1 \le ax) t_Expression* Inequation_2 = CreateNode(inequation_label, KaddNodeForMinusb1, KaddNodeForax, pvt_em); assert(Inequation_2 != NULL); assert(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)); assert(!inequationIsTrivial(Inequation_2, pvt_em, pvt_bvm)); //I don't think any of these can be a trivial inequation set EmptyChildren; set LeqChildren; LeqChildren.insert(Inequation_1); LeqChildren.insert(Inequation_2); t_Expression* kand_1 = CreateKandNode(EmptyChildren, EmptyChildren, LeqChildren, pvt_em); assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); return true; } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! invalid location reached in function t_Project::unifyInequationWithVariableOnBothSides", pvt_logFile, c_RunLevelVerbosity); return false; } } else if(type_of_coefficient == NEGATED) { bvatom CommonCoefficient = pvt_bvm->addInverse(CoefficientMapOfLHS[0].second); // -a obtained, where a = a_1 if(pvt_bvm->checkBVForZero(ConstantOfLHS)) // b_1 = 0; since b_1 != b_2, b_2 != 0 { // we have (-ax+b_1 \le -ax+b_2) \equiv ((ax=0)\vee ((b_2+1 \neq 0)\wedge (ax \ge b_2+1))) when b_1=0 and b_2\neq 0 // Let's create constant and coefficient map for ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create constant and coefficient map for b_2+1 bvatom ConstantOfb2PlusOne; vector< pair< string, bvatom > > CoefficientMapOfb2PlusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfb2PlusOne = pvt_bvm->bvadd(ConstantOfRHS, pvt_bvm->getBVatom(p, OneString)); if(pvt_bvm->checkBVForZero(ConstantOfb2PlusOne)) // b_2+1 = 0; hence (-ax+b_1 \le -ax+b_2) \equiv (ax=0) { // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create ax = 0 t_Expression* Equation_1 = CreateNode(equation_label, KaddNodeForax, pvt_em); assert(Equation_1 != NULL); UnifiedVector.push_back(Equation_1); // Equation_1 is obviously non-trivial return true; } else // b_2+1 \neq 0; hence (-ax+b_1 \le -ax+b_2) \equiv ((ax=0)\vee (ax \ge b_2+1)) { // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create kadd node for b_2+1 t_Expression *KaddNodeForb2PlusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfb2PlusOne, CoefficientMapOfb2PlusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForb2PlusOne != NULL); // Let's create ax = 0 t_Expression* Equation_1 = CreateNode(equation_label, KaddNodeForax, pvt_em); assert(Equation_1 != NULL); // Let's create (b_2+1 \le ax) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForb2PlusOne, KaddNodeForax, pvt_em); assert(Inequation_1 != NULL); // Equation_1 is obviously non-trivial assert(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm)); //I don't think it can be a trivial inequation UnifiedVector.push_back(Equation_1); UnifiedVector.push_back(Inequation_1); return true; } } else if(pvt_bvm->checkBVForZero(ConstantOfRHS)) // b_2 = 0; since b_1 != b_2, b_1 != 0 { // we have (-ax+b_1 \le -ax+b_2) \equiv ((ax \neq 0)\wedge (ax \le b_1)) when b_2=0 and b_1\neq 0 // Let's create constant and coefficient map for ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create constant and coefficient map for b_1 bvatom ConstantOfb1; vector< pair< string, bvatom > > CoefficientMapOfb1; ConstantOfb1 = ConstantOfLHS; // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create kadd node for b_1 t_Expression *KaddNodeForb1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfb1, CoefficientMapOfb1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForb1 != NULL); // Let's create ax \neq 0 t_Expression* Disequation_1 = CreateNode(disequation_label, KaddNodeForax, pvt_em); assert(Disequation_1 != NULL); // Let's create (ax \le b_1) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeForb1, pvt_em); assert(Inequation_1 != NULL); // Disequation_1 is obviously non-trivial set EmptyChildren; set DiseqzChildren; set LeqChildren; DiseqzChildren.insert(Disequation_1); if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm))//Inequation_1 can be a trivial inequation { LeqChildren.insert(Inequation_1); } t_Expression* kand_1 = CreateKandNode(EmptyChildren, DiseqzChildren, LeqChildren, pvt_em); assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); return true; } else if(pvt_bvm->checkBVGreaterThan(ConstantOfRHS, ConstantOfLHS)) { // we have (-ax+b_1 \le -ax+b_2) \equiv (ax=0)\vee ((b_2+1 \neq 0)\wedge (ax \ge b_2+1))\vee ((ax \neq 0)\wedge (ax \le b_1)) // when b_2 > b_1 and b_1 != 0 // Let's create constant and coefficient map for ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create constant and coefficient map for b_1 bvatom ConstantOfb1; vector< pair< string, bvatom > > CoefficientMapOfb1; ConstantOfb1 = ConstantOfLHS; // Let's create constant and coefficient map for b_2+1 bvatom ConstantOfb2PlusOne; vector< pair< string, bvatom > > CoefficientMapOfb2PlusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfb2PlusOne = pvt_bvm->bvadd(ConstantOfRHS, pvt_bvm->getBVatom(p, OneString)); if(pvt_bvm->checkBVForZero(ConstantOfb2PlusOne)) // b_2+1 = 0; // (-ax+b_1 \le -ax+b_2) \equiv (ax=0)\vee ((ax \neq 0)\wedge (ax \le b_1)) { // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create ax = 0 t_Expression* Equation_1 = CreateNode(equation_label, KaddNodeForax, pvt_em); assert(Equation_1 != NULL); UnifiedVector.push_back(Equation_1); // Equation_1 is obviously non-trivial // Let's create kadd node for b_1 t_Expression *KaddNodeForb1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfb1, CoefficientMapOfb1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForb1 != NULL); // Let's create ax \neq 0 t_Expression* Disequation_1 = CreateNode(disequation_label, KaddNodeForax, pvt_em); assert(Disequation_1 != NULL); // Let's create (ax \le b_1) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeForb1, pvt_em); assert(Inequation_1 != NULL); // Disequation_1 is obviously non-trivial set EmptyChildren; set DiseqzChildren; set LeqChildren; DiseqzChildren.insert(Disequation_1); if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm))//Inequation_1 can be a trivial inequation { LeqChildren.insert(Inequation_1); } t_Expression* kand_1 = CreateKandNode(EmptyChildren, DiseqzChildren, LeqChildren, pvt_em); // (ax \neq 0)\wedge (ax \le b_1) assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); return true; } else // b_2+1 \neq 0; hence (-ax+b_1 \le -ax+b_2) \equiv (ax=0)\vee (ax \ge b_2+1)\vee ((ax \neq 0)\wedge (ax \le b_1)) { // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create ax = 0 t_Expression* Equation_1 = CreateNode(equation_label, KaddNodeForax, pvt_em); assert(Equation_1 != NULL); UnifiedVector.push_back(Equation_1); // Equation_1 is obviously non-trivial // Let's create kadd node for b_1 t_Expression *KaddNodeForb1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfb1, CoefficientMapOfb1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForb1 != NULL); // Let's create ax \neq 0 t_Expression* Disequation_1 = CreateNode(disequation_label, KaddNodeForax, pvt_em); assert(Disequation_1 != NULL); // Let's create (ax \le b_1) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeForb1, pvt_em); assert(Inequation_1 != NULL); // Disequation_1 is obviously non-trivial set EmptyChildren; set DiseqzChildren; set LeqChildren; DiseqzChildren.insert(Disequation_1); if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm))//Inequation_1 can be a trivial inequation { LeqChildren.insert(Inequation_1); } t_Expression* kand_1 = CreateKandNode(EmptyChildren, DiseqzChildren, LeqChildren, pvt_em); // (ax \neq 0)\wedge (ax \le b_1) assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); // Let's create constant and coefficient map for b_2+1 bvatom ConstantOfb2PlusOne; vector< pair< string, bvatom > > CoefficientMapOfb2PlusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfb2PlusOne = pvt_bvm->bvadd(ConstantOfRHS, pvt_bvm->getBVatom(p, OneString)); // Let's create kadd node for b_2+1 t_Expression *KaddNodeForb2PlusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfb2PlusOne, CoefficientMapOfb2PlusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForb2PlusOne != NULL); // Let's create (b_2+1 \le ax) t_Expression* Inequation_2 = CreateNode(inequation_label, KaddNodeForb2PlusOne, KaddNodeForax, pvt_em); assert(Inequation_2 != NULL); UnifiedVector.push_back(Inequation_2); return true; } } else if(pvt_bvm->checkBVGreaterThan(ConstantOfLHS, ConstantOfRHS)) { // we have (-ax+b_1 \le -ax+b_2) \equiv ((ax \ge b_2+1)\wedge (ax \le b_1)) // when b_1 > b_2 and b_2\neq 0 // Let's create constant and coefficient map for ax bvatom ConstantOfax; vector< pair< string, bvatom > > CoefficientMapOfax; string ZeroString = getZeroBinaryStringOfGivenLength(p); ConstantOfax = pvt_bvm->getBVatom(p, ZeroString); //0 CoefficientMapOfax.push_back(make_pair(VarToUnify, CommonCoefficient)); // push back (x, a) into CoefficientMapOfax // Let's create constant and coefficient map for b_1 bvatom ConstantOfb1; vector< pair< string, bvatom > > CoefficientMapOfb1; ConstantOfb1 = ConstantOfLHS; // Let's create constant and coefficient map for b_2+1 bvatom ConstantOfb2PlusOne; vector< pair< string, bvatom > > CoefficientMapOfb2PlusOne; string OneString = getOneBinaryStringOfGivenLength(p); ConstantOfb2PlusOne = pvt_bvm->bvadd(ConstantOfRHS, pvt_bvm->getBVatom(p, OneString)); // Let's create kadd node for ax t_Expression *KaddNodeForax = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfax, CoefficientMapOfax, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForax != NULL); // Let's create kadd node for b_1 t_Expression *KaddNodeForb1 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfb1, CoefficientMapOfb1, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForb1 != NULL); // Let's create kadd node for b_2+1 t_Expression *KaddNodeForb2PlusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfb2PlusOne, CoefficientMapOfb2PlusOne, pvt_em, pvt_VariableList, pvt_bvm); assert(KaddNodeForb2PlusOne != NULL); // Let's create (ax \le b_1) t_Expression* Inequation_1 = CreateNode(inequation_label, KaddNodeForax, KaddNodeForb1, pvt_em); assert(Inequation_1 != NULL); // Let's create (b_2+1 \le ax) t_Expression* Inequation_2 = CreateNode(inequation_label, KaddNodeForb2PlusOne, KaddNodeForax, pvt_em); assert(Inequation_2 != NULL); assert(!inequationIsTrivial(Inequation_2, pvt_em, pvt_bvm)); //I don't think any of these can be a trivial inequation set EmptyChildren; set LeqChildren; if(!inequationIsTrivial(Inequation_1, pvt_em, pvt_bvm))//Inequation_1 can be a trivial inequation { LeqChildren.insert(Inequation_1); } LeqChildren.insert(Inequation_2); t_Expression* kand_1 = CreateKandNode(EmptyChildren, EmptyChildren, LeqChildren, pvt_em); assert(kand_1 != NULL); UnifiedVector.push_back(kand_1); return true; } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! invalid location reached in function t_Project::unifyInequationWithVariableOnBothSides", pvt_logFile, c_RunLevelVerbosity); return false; } } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! unexpected value for type_of_coefficient in function t_Project::unifyInequationWithVariableOnBothSides", pvt_logFile, c_RunLevelVerbosity); return false; } }// function ends here /**********************************************************************/ /* Part 5: Functions for Project */ /**********************************************************************/ // Checks if (InputKandNode, variables) is existing in pvt_Project_HashTable. // Returns the result if existing; NULL otherwise. t_Expression* t_Project::checkIn_Project_HashTable(t_Expression* InputKandNode, const vector &variables) { assert(InputKandNode != NULL); // key = address of input kand node + variables to be eliminated string key = toString(InputKandNode); int var_size = variables.size(); for(int i = 0; i < var_size; i++) { key += variables[i]; } t_HTStatusValue result_search = pvt_Project_HashTable.hashtable_search(key); if(result_search.success()) { return result_search.getValue(); } else { return NULL; } }//function ends here // Updates pvt_Project_HashTable with (InputKandNode, variables) ---> OutputNode. bool t_Project::update_Project_HashTable(t_Expression* InputKandNode, const vector &variables, t_Expression* OutputNode) { assert(InputKandNode != NULL); assert(OutputNode != NULL); // key = address of input kand node + variables to be eliminated string key = toString(InputKandNode); int var_size = variables.size(); for(int i = 0; i < var_size; i++) { key += variables[i]; } t_HTStatusValue insert_result = pvt_Project_HashTable.hashtable_insert(key, OutputNode); if (insert_result.success()) { return true; } else { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in hash table insertion in function t_Project::update_Project_HashTable", pvt_logFile, c_RunLevelVerbosity); return false; } }//function ends here // Given a kandNode and vector of variables X, this function // applies the algorithm Project in TACAS'13 paper, in order to compute \exists X. kandNode. t_Expression* t_Project::Project(t_Expression* kandNode, const vector &X) { assert(kandNode != NULL); if(isTrue(kandNode, pvt_em) || X.size() == 0) // kandNode == true or X is empty { // result is kandNode itself return kandNode; } else { assert("kand" == pvt_em->getLabelOfExpression(kandNode)); // check in hash table first t_Expression* ResultFromHashTable = checkIn_Project_HashTable(kandNode, X); if(ResultFromHashTable != NULL) //hash table hit { return ResultFromHashTable; } else //hash table miss { t_Expression* result; // original problem here is \exists X. kandNode // Let's do scope reduction to express it as alpha_1 \wedge \exists Y. alpha_2 t_Expression* alpha_1; t_Expression* alpha_2; vector Y; bool sc_done = scopeReduction(kandNode, X, alpha_1, Y, alpha_2, pvt_em); assert(sc_done); assert(alpha_1 != NULL); assert(alpha_2 != NULL); assert(isTrue(alpha_1, pvt_em) || "kand" == pvt_em->getLabelOfExpression(alpha_1)); // (\exists X. kandNode) \equiv (alpha_1 \wedge \exists Y. alpha_2) // for debugging pvt_em->printExpressionToFileAsDAG("alpha_1 ", alpha_1, cout); pvt_em->printExpressionToFileAsDAG("alpha_2 ", alpha_2, cout); displayVectorOfStringsOnScreen("Y", Y); // for debugging ends here if(isTrue(alpha_2, pvt_em)) // alpha_2 == true { // this means that (\exists X. kandNode) \equiv (alpha_1) assert(Y.size() == 0); result = alpha_1; } else // alpha_2 != true { // Let's compute \exists Y. alpha_2 using Layer1 assert("kand" == pvt_em->getLabelOfExpression(alpha_2)); // Before calling Layer1, let's try synthesizing LMEs from LMIs alpha_2 = simplifyKandBySynthesisOfLMEsFromLMIs(alpha_2, pvt_em, pvt_bvm, pvt_VariableList); assert(alpha_2 != NULL); assert("kand" == pvt_em->getLabelOfExpression(alpha_2)); // for debugging pvt_em->printExpressionToFileAsDAG("alpha_2 after simplifyKandBySynthesisOfLMEsFromLMIs ", alpha_2, cout); // for debugging ends here t_Expression* ResultOfLayer1 = Layer1(alpha_2, Y); assert(ResultOfLayer1 != NULL); if(isTrue(ResultOfLayer1, pvt_em)) // ResultOfLayer1 == true, i.e. \exists Y. alpha_2 == true { // this means that (\exists X. kandNode) \equiv (alpha_1 \wedge \exists Y. alpha_2) \equiv (alpha_1) result = alpha_1; } else // ResultOfLayer1 != true { assert("kand" == pvt_em->getLabelOfExpression(ResultOfLayer1)); // We have \exists Y. alpha_2 \equiv \exists Y. ResultOfLayer1 here // Let us convert \exists Y. ResultOfLayer1 into (beta_1 \wedge \exists Z. beta_2) t_Expression* beta_1; t_Expression* beta_2; vector Z; sc_done = scopeReduction(ResultOfLayer1, Y, beta_1, Z, beta_2, pvt_em); assert(sc_done); assert(beta_1 != NULL); assert(beta_2 != NULL); assert(isTrue(beta_1, pvt_em) || "kand" == pvt_em->getLabelOfExpression(beta_1)); // (\exists Y. ResultOfLayer1) \equiv (beta_1 \wedge \exists Z. beta_2) // for debugging pvt_em->printExpressionToFileAsDAG("beta_1 ", beta_1, cout); pvt_em->printExpressionToFileAsDAG("beta_2 ", beta_2, cout); displayVectorOfStringsOnScreen("Z", Z); // for debugging ends here if(isTrue(beta_2, pvt_em)) // beta_2 == true { // this means that (\exists Y. ResultOfLayer1) \equiv (beta_1) // i.e. result = alpha_1 \wedge beta_1 assert(Z.size() == 0); result = CreateKandNode(alpha_1, beta_1, pvt_em); assert(result != NULL); } else // beta_2 != true { // Let's compute \exists Z. beta_2 using Layer2 assert("kand" == pvt_em->getLabelOfExpression(beta_2)); t_Expression* ResultOfLayer2 = Layer2(beta_2, Z); assert(ResultOfLayer2 != NULL); if(isTrue(ResultOfLayer2, pvt_em)) // ResultOfLayer2 == true, i.e. \exists Z. beta_2 == true { // this means that (\exists X. kandNode) \equiv (alpha_1 \wedge \exists Y. alpha_2) // \equiv (alpha_1 \wedge beta_1 \exists Z. beta_2) // \equiv (alpha_1 \wedge beta_1) result = CreateKandNode(alpha_1, beta_1, pvt_em); assert(result != NULL); } else // ResultOfLayer2 != true { assert("kand" == pvt_em->getLabelOfExpression(ResultOfLayer2)); // We have \exists Z. beta_2 \equiv \exists Z. ResultOfLayer2 here // Let us convert \exists Z. ResultOfLayer2 into (gamma_1 \wedge \exists W. gamma_2) t_Expression* gamma_1; t_Expression* gamma_2; vector W; sc_done = scopeReduction(ResultOfLayer2, Z, gamma_1, W, gamma_2, pvt_em); assert(sc_done); assert(gamma_1 != NULL); assert(gamma_2 != NULL); assert(isTrue(gamma_1, pvt_em) || "kand" == pvt_em->getLabelOfExpression(gamma_1)); // for debugging pvt_em->printExpressionToFileAsDAG("gamma_1 ", gamma_1, cout); pvt_em->printExpressionToFileAsDAG("gamma_2 ", gamma_2, cout); displayVectorOfStringsOnScreen("W", W); // for debugging ends here if(isTrue(gamma_2, pvt_em)) // gamma_2 == true { // this means that (\exists Z. ResultOfLayer2) \equiv (gamma_1) // i.e. result = alpha_1 \wedge beta_1 \wedge gamma_1 assert(W.size() == 0); result = CreateKandNode(alpha_1, beta_1, pvt_em); assert(result != NULL); result = CreateKandNode(result, gamma_1, pvt_em); assert(result != NULL); } else // gamma_2 != true { // Let's compute \exists W. gamma_2 using Layer3 assert("kand" == pvt_em->getLabelOfExpression(gamma_2)); t_Expression* ResultOfLayer3 = Layer3(gamma_2, W); assert(ResultOfLayer3 != NULL); // for debugging pvt_em->printExpressionToFileAsDAG("ResultOfLayer3 ",ResultOfLayer3, cout); // for debugging ends here // find alpha_1 \wedge beta_1 \wedge gamma_1 result = CreateKandNode(alpha_1, beta_1, pvt_em); assert(result != NULL); result = CreateKandNode(result, gamma_1, pvt_em); assert(result != NULL); if(isTrue(ResultOfLayer3, pvt_em)) // ResultOfLayer3 == true { // this means that \exists X. kandNode \equiv alpha_1 \wedge beta_1 \wedge gamma_1 // hence do nothing } else // ResultOfLayer3 != true { // result should be result \wedge ResultOfLayer3 if(isTrue(result, pvt_em)) // result == true; hence result = ResultOfLayer3 { result = ResultOfLayer3; } else // result = result \wedge ResultOfLayer3 { string node_name = "logand"; result = CreateNode(node_name, result, ResultOfLayer3, pvt_em); assert(result != NULL); }// result != true ends here } // ResultOfLayer3 != true ends here } // gamma_2 != true ends here } // ResultOfLayer2 != true ends here } // beta_2 != true ends here } // ResultOfLayer1 != true ends here }// alpha_2 != true ends here pvt_em->printExpressionToFileAsDAG("result ", result, cout); // update the hash table bool HashTable_Updated = update_Project_HashTable(kandNode, X, result); if(!HashTable_Updated) { t_Logger* logManager = t_Logger::getInstance(); logManager->LOG("ERROR!! Failure in hash table insertion in function t_Project::Project", pvt_logFile, c_RunLevelVerbosity); return NULL; } else { return result; }// else of if(!HashTable_Updated) ends here }// hash table miss ends here }// else of else if("kand" != pvt_em->getLabelOfExpression(kandNode)) ends here }//function ends here