

The Constraint Contextual Rewriting Project
Software: RDL
RDL is a system for formula simplification developed within the
Constraint Contextual Rewriting Project. RDL is an acronym for
Rewrite and Decision procedure Laboratory. The
system allows for experimenting with the integration of decision
procedures and conditional rewriting.
 RDL Version 1.1
 News
RDL Version 1.1
Excerpt from the README
This software is being developed as a research tool. We continue to
make significant changes to it. This is an alpha release which we are
doing primarily in order to get feedback. We want to know what you
think of RDL, so please send comments to us at Alessandro Armando or Silvio Ranise.
In order to execute RDL v. 1.1 you need SICStus 3.8 installed on your
machine. (If you don't have it, you can get a free 30 days evaluation
license at the URL http://www.sics.se/sicstus.)
 RDL simplifies clauses in a quantifierfree firstorder
logic with equality using CCR. As a consequence, RDL is sound,
terminating and fully automatic.
 RDL is an open system which can be modularly extended with
new decision procedures provided these offer certain interface
functionalities.
In its current version, RDL offers `plugandplay'
decision procedures for the theories of Universal Presburger
Arithmetic over Integers (UPAI), Universal Theory of Equality
(UTE), and UPAI extended with uninterpreted function symbols.
 RDL implements instances of a generic extension
schema for decision procedures [edpjucs2001]. The key
ingredient of such a schema is a lemma speculation
mechanism which `reduces' the validity problem of a given
theory to the validity problem of one of its subtheory for which a
decision procedure is available.
 RDL is an open reasoning module which can be integrated in
larger verification systems, since extensions of quantifierfree
firstorder logic with equality are useful in practically all
verification efforts.
 RDL features a tight integration of the following three
modules: a module for ordered conditional rewriting, a
satisfiability decision procedure, and a module for
lemma speculation.
In the following, let cl be the clause to be
simplified and p be a literal in cl which is
going to be rewritten. The context C
associated to p is the conjunction of the negation of
the literals occurring in cl except p. Let
T be the theory decided by the decision procedure.
 The decision procedure. For efficiency reasons,
this module is required to be statebased, incremental,
and resettable. The context C is stored by a
specialized data structure in the state of the decision
procedure. There are three functionalities. First,
csunsat characterizes
a set of inconsistent (in T) contexts whose
inconsistency can be checked by means of computationally
inexpensive checks. Second, given a literal l
and the current context C, cssimp
computes the new context C' resulting from the
addition of l to C in such a way that
C' is entailed by the conjunction
of l and C in T. Third,
csnorm computes a normal representation
p' of p w.r.t. T and the
information stored in C. This functionality
must be compatible with rewriting, i.e. it is required
that p'< p where < denotes a total term ordering
on ground literals. (The actual implementation provides
a fixed total ordering on ground RDL literals.)
 Constraint Contextual Rewriting. The rewriter
provides the functionality ccr. It handles
conditional rules of the form h1 /\ ... /\ hn ==>
(l=r), where l and r are RDL
terms, and h1, ..., hn are RDL literals.
Assume r sigma < l sigma for a ground
substitution sigma (otherwise, if l
sigma is different from r sigma, swap
l with r in the following). Given
p[l sigma], ccr returns
p[r sigma] if h1 sigma, ..., hn sigma,
and p[r sigma] are smaller (w.r.t. <) than
p[l sigma], and for i=1,...,n either
hi\sigma is (recursively) rewritten to
true by invoking ccr or by checking
whether hi sigma is entailed by C
(this is done by invoking csunsat so to check
that the negation of hi sigma is inconsistent
with C). There are two other means of
rewriting. Firstly, p is rewritten to
false (true) if csunsat
checks that p (the negation of p,
resp.) is inconsistent with C. Secondly,
p is rewritten to p' if p'
has been obtained by invoking csnorm.
 Lemma speculation. Three instances of the
lemma speculation mechanism described in [edpjucs2001]
are implemented in RDL. All the instances share the
goal of feeding the decision procedure with new facts
about function symbols which are otherwise uninterpreted
in T. More precisely, they inspect the context
C and return a set of ground facts entailed by
C using T as the background theory.
Furthermore, these facts must enjoy some properties to
ensure termination (see [edpjucs2001]
for details).
The simplest form of lemma speculation is
augment [edpjucs2001],
which consists of selecting and instantiating lemmas
from a set of available valid formulae in order to
obtain ground facts whose conclusions can be readily
used by the decision procedure. More precisely,
augment finds instances of the conclusions
among the conditional lemmas which can promote further
inference steps in the decision procedure. There are
two crucial problems. Firstly, we must relieve
hypotheses of lemmas in order to be able to send their
conclusions to the decision procedure. We solve this
problem by rewriting each hypothesis to true
(if possible). This is done by invoking ccr
and it implies that the rewriter and the decision
procedure are mutually recursive. The other problem is
the presence of extra variables in the hypotheses
(w.r.t. the conclusion) of lemmas. RDL avoids this
problem by requiring that the conclusion contains all
the variables occurring in the lemma and that all the
variables get instantiated by matching the conclusion of
the lemma against the largest (according to <) literal
in C.
If a suitable set of lemmas is defined,
augment increases dramatically the
effectiveness of the decision procedure. Unfortunately,
devising such a suitable set is a time consuming
activity. This problem can be solved for some important
special cases. In the actual version of RDL,
affinize
implements the `onthefly' generation of lemmas about
multiplication over integers. To understand how
affinize works, consider the nonlinear
inequality X Y =< 1 (where X and
Y range over integers). By resorting to its
geometrical interpretation, it is easy to verify that
X Y =< 1 is equivalent to (X >= 1 /\ Y =<
1) \/ (X =< 1 /\ Y >= 1). To avoid case
splitting, we observe that the semiplanes represented
by X >= 1 and X =< 1 as those
represented by Y =< 1 and Y >= 1 are
nonintersecting. This allows to derive the following
four lemmas: X >= 1 ==> Y =< 1, X =< 1
==> Y >= 1, Y >= 1 ==> X =< 1, and Y
=< 1 ==> X >= 1. This process can be generalized
to nonlinear inequalities which can be put in the form
X Y =< K (where K is an integer) by
factorization. The generated (conditional) lemmas are
used as for augment.
On the one hand affinize can be seen as a
significant improvement over augment since it
does not require any user intervention. On the other
hand it fails to apply when inequalities cannot be
transformed into a form suitable for affinization. RDL
combines augmentation and affinization by considering the function
symbols occurring in the context C, i.e. the
topmost function symbol of the largest (according to <)
literal in C triggers the invocation of either
affinization or augmentation.
RDL Version 1.1: Tutorial
An online tutorial to RDL.
RDL Version 1.1: Problems
There is a set of problems successfully
processed by RDL. Many problems show proof obligations about
nonlinear inequalities and show the power of the
affinization technique described in [edpjucs2001].
A set of experimental results on
RDL and a comparison with other systems.
A download area containing the RDL
distribution of Version 1.1 of the
system.
 June 15, 2001: RDL distribution updated!
 RDL can now be invoked via command line
 The RDL commandline executable does not require Sicstus
Prolog installed on your machine!
[ Home
 Overview
 Publications
 Lectures and Talks
 Software
 Related links
]
This web site is maintained by the AILab webmaster.
Last updated: 14Dec2006
