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

4 files changed, 16 insertions, 8 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 1c511be30..544ee6c85 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -19,6 +19,7 @@
 #include "smt/options.h"
 #include "smt/smt_engine.h"
 #include "theory/uf/theory_uf_model.h"
+#include "theory/uf/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -851,8 +852,10 @@ void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
           default_v = (*te);
         }
         ufmt.setDefaultValue( m, default_v );
-        ufmt.simplify();
-        Node val = ufmt.getFunctionValue( "_ufmt_" );
+        if(options::condenseFunctionValues()) {
+          ufmt.simplify();
+        }
+        Node val = ufmt.getFunctionValue( "_ufmt_", options::condenseFunctionValues() );
         Trace("model-builder") << "  Assigning (" << n << ") to (" << val << ")" << endl;
         m->d_uf_models[n] = val;
         //ufmt.debugPrint( std::cout, m );
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.
     */