Complement of a logical Equation
Hi I am using Parma Polyhedra library in a Formal Verification project. I was unable to find a function that computes the complement of a logical equation. For example, complement of a=5 will be a!=5. Could you tell me how I could do this. Thanks and Regards Nakul
Hello. The PPL encodes some forms of logical statements as constraints. "a = 5" can be encoded as a Constraint object as follows (in the appropriate context, assuming you are using the C++ interface): Variable a(0); Constraint c(a == 5); There is no way to compute the complement of an equality constraint, because it is not a hyper/half space (it is the union of two open half-spaces). You can compute the two half-spaces separately: the constraint above is encoded as "a - 5 == 0". You can tale the underlying linear expression (a - 5) and use it to construct the two open half-spaces (a - 5 < 0 and a - 5 > 0). Hope my answer is clear enough. Enea. On 02/25/2016 07:17 PM, Rao,Nakul I wrote:
Hi I am using Parma Polyhedra library in a Formal Verification project. I was unable to find a function that computes the complement of a logical equation. For example, complement of a=5 will be a!=5. Could you tell me how I could do this. Thanks and Regards Nakul
_______________________________________________ PPL-devel mailing list PPL-devel@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel
On 02/25/2016 07:17 PM, Rao,Nakul I wrote:
I am using Parma Polyhedra library in a Formal Verification project. I was unable to find a function that computes the complement of a logical equation. For example, complement of a=5 will be a!=5. Could you tell me how I could do this.
Dear Nakul, I am not sure what you are trying to achieve, but perhaps the linear_partition() function might be of interest. Here is an example for you (see the manual for details): $ cat t.cc #include <ppl.hh> #include <iostream> int main() { using namespace Parma_Polyhedra_Library; Variable a(0); Variable b(1); // Build a universe polyhedron of dimension 2. C_Polyhedron p(2); C_Polyhedron q(2); q.add_constraint(a == 5); using namespace std; using namespace IO_Operators; cout << "p = " << p << endl; cout << "q = " << q << endl; std::pair<C_Polyhedron, Pointset_Powerset<NNC_Polyhedron> > result = linear_partition(q, p); cout << "*** p partition ***" << endl; cout << " +++ q inters p +++" << endl << " " << result.first << endl; cout << " +++ rest +++" << endl << " " << result.second << endl; return 0; } $ g++ -W -Wall t.cc -lppl -lgmpxx -lgmp $ a.out p = true q = A = 5 *** p partition *** +++ q inters p +++ A = 5 +++ rest +++ { A > 5 }, { -A > -5 } $ Kind regards, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
participants (3)
-
Enea Zaffanella -
Rao,Nakul I -
Roberto Bagnara