From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 17 Sep 2012 16:39:48 +0000 (+0000)
Subject: minor fix for models, added simple cliques option for uf strong solver
X-Git-Tag: cvc5-1.0.0~7805
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1417d43cca9eae841cef84d7bc5d245d235daaa1;p=cvc5.git

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 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() );
diff --git a/test/regress/regress0/bug382.smt2 b/test/regress/regress0/bug382.smt2
index d92682d35..c44c0ceb8 100644
--- 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)