summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/morgan/theory_uf_morgan.h4
-rw-r--r--src/theory/uf/tim/theory_uf_tim.h4
2 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index 023e100a9..569f9bb49 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -130,6 +130,10 @@ public:
*/
void check(Effort level);
+ void presolve(){
+ Unimplemented();
+ }
+
/**
* Rewrites a node in the theory of uninterpreted functions.
* This is fairly basic and only ensures that atoms that are
diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
index 4c8a1a71a..44f061c12 100644
--- a/src/theory/uf/tim/theory_uf_tim.h
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -126,6 +126,10 @@ public:
void check(Effort level);
+ void presolve() {
+ Unimplemented();
+ }
+
/**
* Rewrites a node in the theory of uninterpreted functions.
* This is fairly basic and only ensures that atoms that are
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback