The Constraint Contextual Rewriting Project

Software: RDL

• RDL Version 1.1
  • README
  • Highlights
  • Tutorial
  • Problems
  • Experiments
  • Dowloading
• 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 Version 1.1: Highlights

• RDL simplifies clauses in a quantifier-free first-order 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 `plug-and-play' 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 [edp-jucs2001]. 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 quantifier-free first-order 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 state-based, 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, cs-unsat 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, cs-simp 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, cs-norm 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 cs-unsat 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 cs-unsat 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 cs-norm.
  • Lemma speculation. Three instances of the lemma speculation mechanism described in [edp-jucs2001] 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 [edp-jucs2001] for details).
    The simplest form of lemma speculation is augment [edp-jucs2001], 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 `on-the-fly' generation of lemmas about multiplication over integers. To understand how affinize works, consider the non-linear 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 semi-planes represented by X >= 1 and X =< -1 as those represented by Y =< -1 and Y >= 1 are non-intersecting. 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 non-linear 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 top-most function symbol of the largest (according to <) literal in C triggers the invocation of either affinization or augmentation.

RDL Version 1.1: Tutorial

RDL Version 1.1: Problems

RDL Version 1.1: Experiments

RDL Version 1.1: Downloading

News

• June 15, 2001: RDL distribution updated!
  • RDL can now be invoked via command line
  • The RDL command-line 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 AI-Lab webmaster.
Last updated: 14-Dec-2006