LPEQ: Equivalence Testing of Logic Programs

Short Summary of the Programs

• lpeq: test the equivalence of the given two logic programs
• testsm: verifying if a program has a particular stable model
• rsat: generate a random 3-SAT instance as a logic program
• drop: drop random rules from a program
• planar: generate random planar graphs using the SGB library (version 20020130-1)

This software has been designed to be used with smodels (versions 2.*) and the front-end lparse which are are available here.

Related Publications

Using the Software

• lpeq is used as follows in order to check the equivalence of program1.lp and program2.lp:
  
  lparse program1.lp > program1.sm
lparse program2.lp > program2.sm
lpeq program1.sm program2.sm | smodels 1
lpeq program2.sm program1.sm | smodels 1

When given the option -c (resp. -s) lpeq produces a program for testing the classical (resp. strong) equivalence of the programs given as input. In this case, you have to invoke lparse (using only versions 1.0.11 and later) using the command line option -d all.

The other programs are more or less subsidiary (invoked by the scripts we have used in the experiments).

• testsm is used as follows:
  lparse program.lp > program.sm
testsm program.sm list_of_atoms | smodels 1
  

  The program adds a compute statement to the program which requires the given atoms to be true.

• rsat [-sseed] [-r] [-d] vars_per_clause vars clauses

  Generates an random 3-SAT instance encoded as a logic program. Option -r enables several occurrences of the same variable in a clause. Variables are distinct by default. Option -d produces a disjunctive logic program.

• drop [-v] [-sseed] [-nnumber of rules] program

  Drops randomly the given number of rules from the program. The internal format of smodels is used. Given the option -v, the program is printed in a textual format.

• planar number_of_nodes seed

  Produces a random planar graph containing the given number of nodes (consult Stanford GraphBase library for details).

Disclaimer

Copyright

Download

Separate programs: lpeq (version 1.13), testsm (version 1.5), rsat-1.7 (version 1.7), drop (version 1.4), planar-1.1 (version 1.1)

Shell scripts (some experiments): queens_test, queens_times.sh, general_test, running_times.sh, naive.sh, README

Logic programs (used in experiments); queens.lp, queens_choice.lp, color.lp, hc.lp

All in one: lpeq.tgz

DLPEQ: Equivalence Testing of Disjunctive Logic Programs

• dlpeq: test the equivalence of the given two disjunctive logic programs

This software has been designed to be used with GnT and the front-end lparse which are are available here.

Using the Software

Disclaimer

Copyright

Download