Add --no-condense-function-values option for explicit function models (useful in some applications)

3 files changed, 11 insertions, 6 deletions

diff --git a/src/theory/uf/options b/src/theory/uf/options
index bea11621a..bed535342 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -8,6 +8,9 @@ module UF "theory/uf/options.h" Uninterpreted functions theory
 option ufSymmetryBreaker uf-symmetry-breaker --symmetry-breaker bool :read-write :default true
  use UF symmetry breaker (Deharbe et al., CADE 2011)
 
+option condenseFunctionValues condense-function-values --condense-function-values bool :default true
+ condense models for functions rather than explicitly representing them
+
 option ufssRegions /--disable-uf-ss-regions bool :default true
  disable region-based method for discovering cliques and splits in uf strong solver
 option ufssEagerSplits --uf-ss-eager-split bool :default false
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 2c853a4fa..f30106174 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -260,14 +260,16 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector
   }
 }
 
-Node UfModelTree::getFunctionValue( std::vector< Node >& args ){
+Node UfModelTree::getFunctionValue( std::vector< Node >& args, bool simplify ){
   Node body = d_tree.getFunctionValue( args, 0, Node::null() );
-  body = Rewriter::rewrite( body );
+  if(simplify) {
+    body = Rewriter::rewrite( body );
+  }
   Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
 }
 
-Node UfModelTree::getFunctionValue( const char* argPrefix ){
+Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
   TypeNode type = d_op.getType();
   std::vector< Node > vars;
   for( size_t i=0; i<type.getNumChildren()-1; i++ ){
@@ -275,7 +277,7 @@ Node UfModelTree::getFunctionValue( const char* argPrefix ){
     ss << argPrefix << (i+1);
     vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
   }
-  return getFunctionValue( vars );
+  return getFunctionValue( vars, simplify );
 }
 
 Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 2149a6583..fbfcc4b7d 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -125,9 +125,9 @@ public:
   /** getFunctionValue
     *   Returns a representation of this function.
     */
-  Node getFunctionValue( std::vector< Node >& args );
+  Node getFunctionValue( std::vector< Node >& args, bool simplify = true );
   /** getFunctionValue for args with set prefix */
-  Node getFunctionValue( const char* argPrefix );
+  Node getFunctionValue( const char* argPrefix, bool simplify = true );
   /** update
     *   This will update all values in the tree to be representatives in m.
     */