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

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index c4fc0310c08bf88cdb239c14cc4275d9fa4f72f0..42654b74cd399a49cd75747e265036a107e11662 100644 (file)
--- 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 8185f0b3df47c8368ce8068ce63fdaa8df0e82a1..3b6a0818fe7360b87b74d71bcf3f60e4d3bc62ec 100644 (file)
--- 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 47c51d8b90e7bf5ef9c656f35c9dfeec37f76aa2..de7061022b6e5c28a4d1d591d10ca2eaa3520a57 100644 (file)
--- 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() );

diff --git a/test/regress/regress0/bug382.smt2 b/test/regress/regress0/bug382.smt2
index d92682d35b47f32edde182a0e77647b4cadfd15a..c44c0ceb821048669afc61e91a6da8f79b350315 100644 (file)
--- a/test/regress/regress0/bug382.smt2
+++ b/test/regress/regress0/bug382.smt2
@@ -1,8 +1,8 @@
 ; EXPECT: sat
 ; EXPECT: ((x 0))
 ; EXPECT: ((x 0))
-; EXPECT: (((f x) 1))
-; EXPECT: (((f x) 1))
+; EXPECT: (((f x) 0))
+; EXPECT: (((f x) 0))
 ; EXIT: 10
 (set-option :produce-models true)
 (set-logic QF_UFLIA)