minor fix for models, added simple cliques option for uf strong solver

3 files changed, 16 insertions, 1 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index c4fc0310c..42654b74c 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -432,6 +432,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){
       n = d_equalityEngine.getRepresentative( n );
       if( d_reps.find( n )==d_reps.end() ){
         d_reps[n] = ret;
+        d_rep_set.add( ret );
       }
       //TODO: make sure that this doesn't affect the representatives in the equality engine
       //  in other words, we need to be sure that all representatives of the equality engine
diff --git a/src/theory/uf/options b/src/theory/uf/options
index 8185f0b3d..3b6a0818f 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -25,6 +25,7 @@ option ufssSmartSplits --uf-ss-smart-split bool :default false
  use smart splitting heuristic for uf strong solver
 option ufssModelInference --uf-ss-model-infer bool :default false
  use model inference method for uf strong solver
-
+option ufssSimpleCliques --uf-ss-simple-cliques bool :default false
+ add simple clique lemmas for uf strong solver
 
 endmodule
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 47c51d8b9..de7061022 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1009,6 +1009,19 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
   while( clique.size()>size_t(d_cardinality+1) ){
     clique.pop_back();
   }
+  if( options::ufssSimpleCliques() ){
+    //add as lemma
+    std::vector< Node > eqs;
+    for( int i=0; i<(int)clique.size(); i++ ){
+      for( int j=0; j<i; j++ ){
+        eqs.push_back( clique[i].eqNode( clique[j] ) );
+      }
+    }
+    eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
+    Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
+    out->lemma( lem );
+    return;
+  }
   if( options::ufssModelInference() || Trace.isOn("uf-ss-cliques") ){
     std::vector< Node > clique_vec;
     clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );