diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-17 16:39:48 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-17 16:39:48 +0000 |
| commit | 1417d43cca9eae841cef84d7bc5d245d235daaa1 (patch) | |
| tree | 2cfc3e8220b9401ae40677bc9706617cacf1c97f | |
| parent | 249c19d48e6a69ca4b083cae701d51d4ff54cfc5 (diff) | |
minor fix for models, added simple cliques option for uf strong solver
| -rw-r--r-- | src/theory/model.cpp | 1 | ||||
| -rw-r--r-- | src/theory/uf/options | 3 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 13 | ||||
| -rw-r--r-- | test/regress/regress0/bug382.smt2 | 4 |
4 files changed, 18 insertions, 3 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() ); 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) |