#include <array_proof_rules.h>
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.
Referenced by CVC3::TheoryArray::rewrite().
Referenced by CVC3::TheoryArray::rewrite().
Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
virtual Theorem CVC3::ArrayProofRules::rewriteRedundantWrite1 | ( | const Theorem & | v_eq_r, | |
const Expr & | write | |||
) | [pure virtual] |
Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Referenced by CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg).
Referenced by CVC3::TheoryArray::rewrite().
Lift ite over read.
Referenced by CVC3::TheoryArray::rewrite().
a /= b |- exists i. a[i] /= b[i]
Referenced by CVC3::TheoryArray::assertFact().