20 #ifndef _cvc3__records_proof_rules_h_
21 #define _cvc3__records_proof_rules_h_
Data structure of expressions in CVC3.
virtual Theorem expandEq(const Theorem &eqThrm)=0
From T|- e = e' return T|- AND (e.i = e'.i) for all i.
virtual ~RecordsProofRules()
< Destructor
virtual Theorem rewriteLitSelect(const Expr &e)=0
==> (REC_LITERAL (f1 v1) ... (fi vi) ...).fi = vi
virtual Theorem expandRecord(const Expr &e)=0
Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #)
virtual Theorem expandNeq(const Theorem &neqThrm)=0
From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i.
virtual Theorem rewriteUpdateSelect(const Expr &e)=0
==> (REC_SELECT (REC_UPDATE e fi vi) fi) = vi
virtual Theorem expandTuple(const Expr &e)=0
Expand a tuple into a literal: |- e = (e.0, ..., e.n-1)
virtual Theorem rewriteLitUpdate(const Expr &e)=0
==> (REC_UPDATE (REC_LITERAL (f1 v1) ... (fi vi) ...) fi v') =(REC_LITERAL (f1 v1) ...