array_theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file array_theorem_producer.h
00004  * 
00005  * Author: Clark Barrett, 5/29/2003
00006  * 
00007  * Created: May 29 19:16:33 GMT 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  * CLASS: ArrayProofRules
00019  * 
00020  * 
00021  * Description: TRUSTED implementation of array proof rules.  DO
00022  * NOT use this file in any DP code, use the exported API in
00023  * array_proof_rules.h instead.
00024  * 
00025  */
00026 /*****************************************************************************/
00027 #ifndef _cvc3__theory_array__array_theorem_producer_h_
00028 #define _cvc3__theory_array__array_theorem_producer_h_
00029 
00030 #include "array_proof_rules.h"
00031 #include "theorem_producer.h"
00032 
00033 namespace CVC3 {
00034   
00035 
00036   class ArrayTheoremProducer: public ArrayProofRules, public TheoremProducer {
00037   private:
00038     // Inserting flea proof arguments for a canonical sum
00039   public:
00040     // Constructor
00041     ArrayTheoremProducer(TheoremManager* tm) : TheoremProducer(tm) { }
00042 
00043     ////////////////////////////////////////////////////////////////////
00044     // Proof rules
00045     ////////////////////////////////////////////////////////////////////
00046 
00047     // ==>
00048     // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
00049     //
00050     // read(store, index_n) = v_n &
00051     // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
00052     // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
00053     // ...
00054     // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
00055     // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
00056     Theorem rewriteSameStore(const Expr& e, int n);
00057 
00058     // ==> write(store, index, value) = write(...) IFF
00059     //       store = write(write(...), index, read(store, index)) &
00060     //       value = read(write(...), index)
00061     Theorem rewriteWriteWrite(const Expr& e);
00062 
00063     // ==> read(write(store, index1, value), index2) =
00064     //   ite(index1 = index2, value, read(store, index2))
00065     Theorem rewriteReadWrite(const Expr& e);
00066 
00067     // value = read(store, index) ==>
00068     //   write(store, index, value) = store
00069     Theorem rewriteRedundantWrite1(const Theorem& v_eq_r,
00070            const Expr& write);
00071 
00072     // ==>
00073     //   write(write(store, index, v1), index, v2) = write(store, index, v2)
00074     Theorem rewriteRedundantWrite2(const Expr& e);
00075 
00076     // ==>
00077     //   write(write(store, index1, v1), index2, v2) =
00078     //   write(write(store, index2, v2), index1, ite(index1 = index2, v2, v1))
00079     Theorem interchangeIndices(const Expr& e);
00080     // Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
00081     Theorem readArrayLiteral(const Expr& e);
00082 
00083     Theorem liftReadIte(const Expr& e);
00084 
00085   }; // end of class ArrayTheoremProducer
00086 
00087 } // end of namespace CVC3
00088 
00089 #endif

Generated on Tue Jul 3 14:33:34 2007 for CVC3 by  doxygen 1.5.1