[PPL-devel] Complement of a logical Equation

[Roberto Bagnara]

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 at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com