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