#include <array_proof_rules.h>
Inheritance diagram for CVC3::ArrayProofRules:
Definition at line 33 of file array_proof_rules.h.
virtual CVC3::ArrayProofRules::~ArrayProofRules | ( | ) | [inline, virtual] |
Definition at line 36 of file array_proof_rules.h.
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
virtual Theorem CVC3::ArrayProofRules::rewriteRedundantWrite1 | ( | const Theorem & | v_eq_r, | |
const Expr & | write | |||
) | [pure virtual] |
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg).
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite().
Lift ite over read.
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite().