summaryrefslogtreecommitdiff
path: root/src/theory/theory.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r--src/theory/theory.h19
1 files changed, 9 insertions, 10 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index a6751e1ec..c777f164f 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -424,22 +424,21 @@ public:
virtual void finishInit() { }
/**
- * Some theories have kinds that are effectively definitions and
- * should be expanded before they are handled. Definitions allow
- * a much wider range of actions than the normal forms given by the
- * rewriter; they can enable other theories and create new terms.
- * However no assumptions can be made about subterms having been
- * expanded or rewritten. Where possible rewrite rules should be
- * used, definitions should only be used when rewrites are not
- * possible, for example in handling under-specified operations
- * using partially defined functions.
+ * Some theories have kinds that are effectively definitions and should be
+ * expanded before they are handled. Definitions allow a much wider range of
+ * actions than the normal forms given by the rewriter. However no
+ * assumptions can be made about subterms having been expanded or rewritten.
+ * Where possible rewrite rules should be used, definitions should only be
+ * used when rewrites are not possible, for example in handling
+ * under-specified operations using partially defined functions.
*
* Some theories like sets use expandDefinition as a "context
* independent preRegisterTerm". This is required for cases where
* a theory wants to be notified about a term before preprocessing
* and simplification but doesn't necessarily want to rewrite it.
*/
- virtual Node expandDefinition(LogicRequest &logicRequest, Node node) {
+ virtual Node expandDefinition(Node node)
+ {
// by default, do nothing
return node;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback