24 #define _CVC3_TRUSTED_
42 TheoryDatatype::createProofRules() {
54 vector<Theorem> thmVec;
55 for (
unsigned i = 0; i < facts.
size(); ++i)
56 thmVec.push_back(facts[i]);
59 return newTheorem(e, a, pf);
67 CHECK_SOUND(d_theoryDatatype->canCollapse(e),
"Expected canCollapse");
72 pair<Expr, unsigned> selectorInfo =
73 d_theoryDatatype->getSelectorInfo(e.
getOpExpr());
76 t = e[0][selectorInfo.second];
81 t = d_theoryDatatype->getConstant(type);
84 if (withProof()) pf = newPf(
"rewriteSelCons", e, t);
87 vector<Theorem> thmVec;
88 for (
unsigned i = 0; i < facts.
size(); ++i)
89 thmVec.push_back(facts[i]);
91 return newRWTheorem(e, t, a, pf);
94 return newRWTheorem(e, t, Assumptions::emptyAssump(), pf);
99 Theorem DatatypeTheoremProducer::rewriteTestCons(
const Expr& e) {
106 Expr cons = d_theoryDatatype->getConsForTester(e.
getOpExpr());
108 t = d_theoryDatatype->trueExpr();
111 t = d_theoryDatatype->falseExpr();
113 if (withProof()) pf = newPf(
"rewriteTestCons", e, t);
114 return newRWTheorem(e, t, Assumptions::emptyAssump(), pf);
129 "decompose precondition violated");
134 if (lhs.
arity() > 1) {
137 for (
int i = 1; i < lhs.
arity(); ++i) {
138 args.push_back(lhs[i].eqExpr(rhs[i]));
142 if (withProof()) pf = newPf(
"decompose", e.
getProof());
143 return newTheorem(res, a, pf);
150 "noCycle: expected constructor with children");
156 const Op& reach = d_theoryDatatype->getReachablePredicate(t);
159 args.push_back(!
Expr(reach, e, e));
160 for (
int i = 0; i < e.
arity(); ++i) {
162 d_theoryDatatype->getReachablePredicate(e[i].getType()) == reach)
163 args.push_back(
Expr(reach, e, e[i]));
166 if (withProof()) pf = newPf(
"noCycle", e);
167 return newTheorem(
andExpr(args), Assumptions::emptyAssump(), pf);
bool isConstructor(const Expr &e)
bool isDatatype(const Type &t)
Data structure of expressions in CVC3.
Expr getConstructor(const Expr &e)
MS C++ specific settings.
Expr eqExpr(const Expr &right) const
bool isSelector(const Expr &e)
#define CHECK_SOUND(cond, msg)
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
const Expr & getExpr() const
const Expr & getRHS() const
TRUSTED implementation of recursive datatype proof rules.
bool isTester(const Expr &e)
const Expr & getLHS() const
Type getType() const
Get the type. Recursively compute if necessary.
Expr andExpr(const std::vector< Expr > &children)