/******************************************************************** Developers: Ajith John, Supratik Chakraborty Last updated: July 24, 2013 *********************************************************************/ /********************************************************************* ExpressionMisc.cpp and ExpressionMisc.h contains a set of useful functions for operating on expressions. *********************************************************************/ #ifndef ExpressionMisc_h #define ExpressionMisc_h #include "ExpressionManager.h" #include "LogManager.h" using namespace std; // The following definition identifies the solver to be used in the // satisfiability checks. Presently only stp is supported. enum t_solver {stp}; /*******************************************************************************/ /* Part 1: Functions for creation of expressions */ /*******************************************************************************/ // function to create unsigned bit-vector symbols t_Expression* CreateSymbol(string &symb_name, unsigned symb_width, t_ExpressionManager *em); // function to create unsigned bit-vector constants // const_value should be a binary string of width const_width t_Expression* CreateConstant(string &const_value, unsigned const_width, t_ExpressionManager *em); // functions to create unsigned bit-vector terms t_Expression* CreateTerm(string &term_name, unsigned term_width, t_Expression* child1, t_ExpressionManager *em); t_Expression* CreateTerm(string &term_name, unsigned term_width, t_Expression* child1, t_Expression* child2, t_ExpressionManager *em); t_Expression* CreateTerm(string &term_name, unsigned term_width, t_Expression* child1, t_Expression* child2, t_Expression* child3, t_ExpressionManager *em); t_Expression* CreateTerm(string &term_name, unsigned term_width, vector &children, t_ExpressionManager *em); // functions to create boolean nodes t_Expression* CreateNode(string &node_name, t_Expression* child1, t_ExpressionManager *em); t_Expression* CreateNode(string &node_name, t_Expression* child1, t_Expression* child2, t_ExpressionManager *em); t_Expression* CreateNode(string &node_name, t_Expression* child1, t_Expression* child2, t_Expression* child3, t_ExpressionManager *em); t_Expression* CreateNode(string &node_name, vector &children, t_ExpressionManager *em); // function to create "kand" node from "eqz", "diseqz" and "leq" nodes // note that keeping "eqz", "diseqz" and "leq" children as sets avoids duplication // Precondition: None of the children should be NULL. This condition is not checked inside the function. // Ensure this before calling the function. t_Expression* CreateKandNode(set &EqzChildren, set &DiseqzChildren, set &LeqChildren, t_ExpressionManager *em); // function to create "kand" node from two existing "kand" nodes. // Collects the children of the existing "kand" nodes, and creates // a new "kand" node. t_Expression* CreateKandNode(t_Expression* kand_1, t_Expression* kand_2, t_ExpressionManager *em); // Given a set of constraints, where each constraint is // eqz, diseqz, leq, not (eqz), not(diseqz), or not(leq), // pushes the negation inside in case of not(eqz), not(diseqz), and not(leq), // and returns kand which is a conjunction of these constraints. // Returns true if the conjunction is true; returns NULL in case of errors. t_Expression* obtainKandNodeFromASetOfConstraints(set &Constraints, t_ExpressionManager *em, BVManager* bvm, t_HashTable &VariableList, t_HashTable &WidthTable); // functions to operate on VariableList // get index of variable from VariableList // returns -1 if the variable has no entry in VariableList int getVariableIndex(const string &variable, t_HashTable &VariableList); // adds entry (variable, index) into VariableList // index should be >= 0 bool addEntryToVariableList(const string &variable, int index, t_HashTable &VariableList); // check if // (1) children are sorted based on the indices of variables in the monoms // (2) all coefficients are non-zero // return true if (1) and (2) are satisfied, false otherwise bool checkIfChildrenOfKaddNodeAreSortedAndAllCoefficientsAreNonZero(const vector &children, t_ExpressionManager *em, t_HashTable &VariableList); // function to create "kadd" node from the constant child and sorted children (monoms). // note that the constant child is NULL by default. // preconditions: 1) monom children should be sorted (for correctness) // 2) no coefficient or constant should be zero (for efficiency) // both conditions are checked inside the function. NULL is returned if either is is false. // 3) None of the children should be NULL. This condition is not checked inside the function. // Ensure this before calling the function. t_Expression* CreateKaddNode(unsigned term_width, vector &SortedChildren, t_ExpressionManager *em, t_HashTable &VariableList, t_Expression* ConstantChild=NULL); // function to create "kadd" node from the constant and coefficient map. // precondition: monom children should be sorted (for correctness) // this condition is checked inside the function. NULL is returned if it is false. // note that if (1) the constant is zero and (2) the coefficient_map is empty or has only zero coefficients, // then "kadd" node with a single zero child is returned. t_Expression* CreateKaddNodeFromConstantAndCoefficientMap(unsigned term_width, bvatom constant, const vector< pair< string, bvatom > > &coefficient_map, t_ExpressionManager *em, t_HashTable &VariableList, BVManager* bvm); // functions to create boolean constants t_Expression* getTrue(t_ExpressionManager *em); t_Expression* getFalse(t_ExpressionManager *em); // adds entry (variable, width) into WidthTable // width should be >= 1 bool addEntryToWidthTable(const string &variable, int width, t_HashTable &WidthTable); // Given an eqz node, this function returns the negation of this node (a diseqz node) t_Expression* negateLME(t_Expression *eqzNode, t_ExpressionManager *em); // Given a diseqz node, this function returns the negation of this node (an eqz node) t_Expression* negateLMD(t_Expression *diseqzNode, t_ExpressionManager *em); // Given an leq node t1 <= t2, this function returns the negation of this node. // Note that negation of t1 \leq t2 \equiv t1 > t2 // t1 > t2 \equiv (t1-1 >= t2) \wedge (t1 \neq 0) // t1 > t2 \equiv (t1 >= t2+1) \wedge (t2 \neq 2^p-1) // If t1 is a constant and t1 \neq 0, then, (t1-1 >= t2) is returned and NegatedLMI_LMDPart is set to NULL // O/w, if t2 is a constant and t2 \neq 2^p-1, then, (t1 >= t2+1) is returned and NegatedLMI_LMDPart is set to NULL // O/w, (t1 >= t2+1) is returned and NegatedLMI_LMDPart is set to (t2 \neq 2^p-1) t_Expression* negateLMI(t_Expression *leqNode, t_Expression* &NegatedLMI_LMDPart, t_ExpressionManager *em, BVManager* bvm, t_HashTable &VariableList, t_HashTable &WidthTable); // Given an eqz node t = 0, this function returns the equivalent LeqNode t <= 0 t_Expression* obtainEquivalentLeqNodeFromEqzNode(t_Expression *eqzNode, t_ExpressionManager *em, BVManager* bvm, t_HashTable &VariableList); // Given a diseqz node t \neq 0, this function returns the equivalent LeqNode 1 <= t t_Expression* obtainEquivalentLeqNodeFromDiseqzNode(t_Expression *diseqzNode, t_ExpressionManager *em, BVManager* bvm, t_HashTable &VariableList); // Given a kand node, this function returns an equivalent simplified kand node. // The simplifications applied are: // (a) t <= 0 ---> t = 0 // (b) 2^{p}-1 <= t ---> t = 2^{p}-1 // (c) t_1 <= t_2 \wedge t_2 <= t_1 ---> t_1 = t_2 t_Expression* simplifyKandBySynthesisOfLMEsFromLMIs(t_Expression *kandNode, t_ExpressionManager *em, BVManager *bvm, t_HashTable &VariableList); // This function generates E_from_I and Remaining_I from I // s.t. I = E_from_I \union Remaining_I using the rules // (a) t <= 0 ---> t = 0 // (b) 2^{p}-1 <= t ---> t = 2^{p}-1 // (c) t_1 <= t_2 \wedge t_2 <= t_1 ---> t_1 = t_2 // returns true always bool SynthesizeLMEsFromLMIs(const set &I, set &E_from_I, set &Remaining_I, t_ExpressionManager *em, BVManager *bvm, t_HashTable &VariableList); // Given an leq node t_1 <= t_2, this function // (a) Checks if t_2 is 0. If yes, returns t_1 = 0 // (b) Checks if t_1 is 2^{p}-1. If yes, returns t_2 = 2^{p}-1 i.e. t_2 + 1 = 0 // (c) Otherwise returns NULL t_Expression* obtainEquivalentEqzNodeFromLeqNode(t_Expression *LeqNode, t_ExpressionManager *em, BVManager* bvm, t_HashTable &VariableList); // Given leq nodes t_1 <= t_2 and t_3 <= t_4, this function // (a) Checks if t_3 is the same as t2 and t_4 is the same as t1. If yes, returns t_1 = t_2 i.e., t_1 - t_2 = 0 // (b) Otherwise returns NULL t_Expression* obtainEquivalentEqzNodeFromPairOfLeqNodes(t_Expression *LeqNode_1, t_Expression *LeqNode_2, t_ExpressionManager *em, BVManager* bvm, t_HashTable &VariableList); /*******************************************************************************/ /* Part 2: Checking functions */ /*******************************************************************************/ // functions to check if expression is a constant bool isTrue(t_Expression* exp, t_ExpressionManager *em); bool isFalse(t_Expression* exp, t_ExpressionManager *em); bool isBVConstant(t_Expression* exp, t_ExpressionManager *em); bool isBooleanConstant(t_Expression* exp, t_ExpressionManager *em); bool isBVVariable(t_Expression* exp, t_ExpressionManager *em); // returns true if the eqzNode is trivial i.e. true, false otherwise bool equationIsTrivial(t_Expression *eqzNode, t_ExpressionManager *em); // returns true if the eqzNode is false, true otherwise bool equationIsFalse(t_Expression *eqzNode, t_ExpressionManager *em); // returns true if the diseqzNode is trivial i.e. true, false otherwise bool disequationIsTrivial(t_Expression *diseqzNode, t_ExpressionManager *em); // returns true if the diseqzNode is false, false otherwise bool disequationIsFalse(t_Expression *diseqzNode, t_ExpressionManager *em); // returns true if the leqNode is trivial i.e. true, false otherwise bool inequationIsTrivial(t_Expression *leqNode, t_ExpressionManager *em, BVManager* bvm); // returns true if the leqNode is false, false otherwise bool inequationIsFalse(t_Expression *leqNode, t_ExpressionManager *em, BVManager* bvm); // returns true if the kaddNode is zero constant, false otherwise bool kaddIsZeroConstant(t_Expression *kaddNode, t_ExpressionManager *em); // returns true if the kaddNode is a non-zero constant, false otherwise bool kaddIsNonZeroConstant(t_Expression *kaddNode, t_ExpressionManager *em); // returns true if the kaddNode is the maximum constant 2^{p}-1, false otherwise bool kaddIsMaximumConstant(t_Expression *kaddNode, t_ExpressionManager *em); // returns true if // (1) both the firstKaddNode and the secondKaddNode are constants and // (2) the firstKaddNode is less than or equal to the secondKaddNode // returns false otherwise bool firstKaddIsLteSecondKadd(t_Expression *firstKaddNode, t_Expression *secondKaddNode, t_ExpressionManager *em, BVManager* bvm); // returns true if // (1) both the firstKaddNode and the secondKaddNode are constants and // (2) the firstKaddNode is greater than the secondKaddNode // returns false otherwise bool firstKaddIsGtSecondKadd(t_Expression *firstKaddNode, t_Expression *secondKaddNode, t_ExpressionManager *em, BVManager* bvm); // Given a constraint (equation/disequation/inequation) and a variable, // Returns true if the constraint is free of variable; false otherwise. bool constraintFreeOfVariable(t_Expression* Constraint, const string &variable, t_ExpressionManager *em, t_HashTable &VariableList); /*******************************************************************************/ /* Part 3: Get functions */ /*******************************************************************************/ // finds the number of child nodes in the parameter degree // returns false in case of errors; false otherwise bool Degree(t_Expression* exp, t_ExpressionManager *em, unsigned int °ree); // returns i^{th} child node of exp // returns NULL in case of errors t_Expression* getIthChild(t_Expression* exp, unsigned int i, t_ExpressionManager *em); // get width of variable from WidthTable // returns -1 if the variable has no entry in WidthTable int getWidthOfVariable(const string &variable, t_HashTable &WidthTable); // Given a "kand" node, obtain the equations in E, disequations in D, and inequations in I bool findConstraintsFromKandNode(t_Expression* kandNode, set &E, set &D, set &I, t_ExpressionManager *em); // Given a "kadd" node, this function finds the monom i.e. bvmul node with the variable. // Sets "MonomWithVariable" to NULL if the "kadd" node is free of the variable. // Returns false in case of errors; true otherwise. bool findMonomOfKaddNodeWithGivenVariable(t_Expression* kaddNode, const string &variable, t_Expression* &MonomWithVariable, t_ExpressionManager *em, t_HashTable &VariableList); // Given a vector of monoms in "Children", find the location of the monom containing // the variable with index "key" in "MonomLocation". If there's no child with the variable, then set // "MonomLocation" to -1. Returns false in case of errors; true otherwise. bool binarySearch(const vector &Children, int first, int last, int key, int &MonomLocation, t_ExpressionManager *em, t_HashTable &VariableList); // Given a monom, i.e. "bvmul" node, this function finds the variable of the monom. // Returns false in case of errors; true otherwise. bool findVariableOfMonom(t_Expression* monom, string &VariableOfMonom, t_ExpressionManager *em); // Given a monom, i.e. "bvmul" node, this function finds the coefficient of the monom as a bvatom. // Returns false in case of errors; true otherwise. bool findCoefficientOfMonom(t_Expression* monom, bvatom &CoefficientOfMonom, t_ExpressionManager *em, BVManager* bvm); // Given a monom, i.e. "bvmul" node, this function finds the variable and the // coefficient of the variable in the monom. Returns false in case of errors; true otherwise. bool findVariableAndCoefficientOfMonom(t_Expression* monom, string &VariableOfMonom, bvatom &CoefficientOfMonom, t_ExpressionManager *em, BVManager* bvm); // Given a constraint (equation/disequation/inequation), this function finds the support of the constraint. // Returns false in case of errors; true otherwise. bool findSupportOfConstraint(t_Expression* Constraint, set &SupportOfConstraint, t_ExpressionManager *em); // Given a kadd node, this function finds the support of the kadd node. // Returns false in case of errors; true otherwise. bool findSupportOfKaddNode(t_Expression* kaddNode, set &SupportOfKaddNode, t_ExpressionManager *em); // Given a "kand" node and a variable, // obtain the equations with the variable in E_x, equations without the variable in E_neg_x, // disequations with the variable in D_x, disequations without the variable in D_neg_x, // inequations with the variable in I_x, inequations without the variable in I_neg_x bool findFreeAndBoundConstraintsFromKandNode(t_Expression* kandNode, const string &variable, set &E_x, set &D_x, set &I_x, set &E_neg_x, set &D_neg_x, set &I_neg_x, t_ExpressionManager *em, t_HashTable &VariableList); // Given a set of constraints and variable, // 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 findFreeAndBoundConstraintsFromSet(const set &Constraints, const string &variable, set &E_x, set &D_x, set &I_x, set &E_neg_x, set &D_neg_x, set &I_neg_x, t_ExpressionManager *em, t_HashTable &VariableList); // Version of findFreeAndBoundConstraintsFromKandNode which works for multiple variables. // i.e. Given a "kand" node and a set of variables X, // obtain the equations with variables in X in E_X, equations without variables in X in E_neg_X, // disequations with variables in X in D_X, disequations without variables in X in D_neg_X, // inequations with variables in X in I_X, inequations without variables in X in I_neg_X. // Also, common_variables_in_kandNode = X \intersection support of kand node. bool findFreeAndBoundConstraintsFromKandNodeForMultipleVariables(t_Expression* kandNode, const set &variables, set &E_X, set &D_X, set &I_X, set &E_neg_X, set &D_neg_X, set &I_neg_X, set &common_variables_in_kandNode, t_ExpressionManager *em); // Version of findFreeAndBoundConstraintsFromSet which works for multiple variables. // i.e. Given a set of constraints and a set of variables X, // obtain the equations with variables in X in E_X, equations without variables in X in E_neg_X, // disequations with variables in X in D_X, disequations without variables in X in D_neg_X, // inequations with variables in X in I_X, inequations without variables in X in I_neg_X bool findFreeAndBoundConstraintsFromSetForMultipleVariables(const set &Constraints, const set &variables, set &E_X, set &D_X, set &I_X, set &E_neg_X, set &D_neg_X, set &I_neg_X, t_ExpressionManager *em); // Given \exists X. alpha_kand where alpha_kand is a kand node and X is a vector of variables, // this function expresses it as beta_1_kand \wedge \exists Y. beta_2_kand, where // beta_1_kand, beta_2_kand are either true or kand nodes and Y is a vector of variables s.t. Y \subseteq X. bool scopeReduction(t_Expression* alpha_kand, const vector &X, t_Expression* &free_kand, vector &Y, t_Expression* &bound_kand, t_ExpressionManager *em); /*******************************************************************************/ /* Part 4: Functions on coefficient maps */ /*******************************************************************************/ // Given a "kadd" node c_0 + c_1.x_1 + ... +c_n.x_n and variables_to_exclude as say {x_i, x_{i+1}}, this // function returns Constant = c_0 and CoefficientMap = vector < (x_1, c_1), ... ,(x_{i-1}, c_{i-1}), (x_{i+2}, c_{i+2}), ..., (x_n, c_n) > // i.e. CoefficientMap has all coefficients and variables except those in variables_to_exclude. // Returns false in case of errors; true otherwise. bool getKaddNodeAsCoefficientMapExcludingGivenVariables(t_Expression* kaddNode, const set &variables_to_exclude, bvatom &Constant, vector< pair< string, bvatom > > &CoefficientMap, t_ExpressionManager *em, BVManager* bvm); // function to bvmul each coefficient in coefficient map source_map by multiplier, // and return the new coefficient map in destination_map bool scalarMultiplication(const vector< pair< string, bvatom > > &source_map, bvatom multiplier, vector< pair< string, bvatom > > &destination_map, BVManager* bvm); // function to find the additive inverse of each coefficient in coefficient map source_map, // and return the new coefficient map involving the additive inverses in destination_map bool additiveInverse(const vector< pair< string, bvatom > > &source_map, vector< pair< string, bvatom > > &destination_map, BVManager* bvm); // function to left shift each coefficient in coefficient map source_map by shift, // and return the new coefficient map in destination_map bool leftShift(const vector< pair< string, bvatom > > &source_map, int shift, vector< pair< string, bvatom > > &destination_map, BVManager* bvm); // function to add two coefficient maps, and return the result in destination_map bool addition(const vector< pair< string, bvatom > > &first_source_map, const vector< pair< string, bvatom > > &second_source_map, vector< pair< string, bvatom > > &destination_map, BVManager* bvm, t_HashTable &VariableList); /*******************************************************************************/ /* Part 5: Functions for evaluation and solving */ /*******************************************************************************/ // Function to evaluate a kadd node using the map "Model" between variables and values. // Note that each value is a binary string of size same as the width of corresponding variable. // Sets result to the evaluated value. // Returns false in case of errors; true otherwise. bool evaluateKaddNode(t_Expression* kaddNode, map &Model, bvatom &result, t_ExpressionManager *em, BVManager* bvm, t_HashTable &WidthTable); // Function to evaluate an "eqz", "diseqz", or "leq" node using the map "Model" between variables and values. // Note that each value is a binary string of size same as the width of corresponding variable. // Sets result to true if the node evaluates to true; to false if the node evaluates to false. // Returns false in case of errors; true otherwise. bool evaluateLMC(t_Expression* constraintNode, map &Model, bool &result, t_ExpressionManager *em, BVManager* bvm, t_HashTable &WidthTable); // This function checks if F is satisfiable. // If F is satisfiable, then, sat is set to true and model of F is obtained. // Otherwise, if F is unsatisfiable, then, sat is set to false. // Returns false in case of errors; true otherwise bool obtainModelOfFormula(t_Expression* F, bool &sat, t_solver solver, map &model, t_ExpressionManager *em, const string &smt_file_name = "formula.smt"); // This function reads the stp model in the file model_file_name // If the file contains "sat" then, result_of_check is set to "sat" and model is read. // o/w if the file contains "unsat" then, result_of_check is set to "unsat". // o/w if the file contains "unknown" then, result_of_check is set to "unknown". // Returns false in case of errors; true otherwise bool readSTPModelFile(const string &model_file_name, string &result_of_check, map &model); /*******************************************************************************/ /* Part 6: Functions for display */ /*******************************************************************************/ // displays the coefficient map on screen bool displayCoefficientMapOnScreen(const bvatom &Constant, const vector< pair< string, bvatom > > &CoefficientMap, BVManager* bvm); // displays a set of expressions on screen bool displaySetOfExpressionsOnScreen(const string &WhoAmI, const set &ExpressionSet, t_ExpressionManager *em); // displays a set of strings on screen bool displaySetOfStringsOnScreen(const string &WhoAmI, const set &StringSet); // displays a vector of strings on screen bool displayVectorOfStringsOnScreen(const string &WhoAmI, const vector &StringVector); #endif