summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-11-16 21:11:11 +0000
committerTim King <taking@cs.nyu.edu>2010-11-16 21:11:11 +0000
commitbb2a0e0e12f39a1b4dea8fb0c990decba4708a1c (patch)
tree6e5824f8cf1b0f1cb32e6cae5cbd214b1b48d965 /src/theory/arrays
parente66924cb0f425ca70969058532340e68c9c17a54 (diff)
Added Theory::presolve().
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/theory_arrays.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 89631d59f..22a0148e1 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -48,6 +48,10 @@ public:
return RewriteComplete(in);
}
+ void presolve() {
+ Unimplemented();
+ }
+
void addSharedTerm(TNode t);
void notifyEq(TNode lhs, TNode rhs);
void check(Effort e);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback