diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-25 12:18:05 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-25 12:18:14 -0500 |
| commit | d8de492163b90974709a16918cb615515a536afc (patch) | |
| tree | 8241c94be9a610149b40af0fc0932ee05094b2aa /src/theory/uf | |
| parent | a9bf7fc500daba46ed86ca744c1346059880e6f4 (diff) | |
Refactoring of model engine to separate individual implementations of model builder. Begin work on interval models for integers. Other minor cleanup.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index baa40463f..71a342f76 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1001,14 +1001,14 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ if( applyTotality( d_aloc_cardinality ) ){ //must generate new cardinality lemma term Node var; - //if( d_aloc_cardinality==1 ){ + if( d_aloc_cardinality==1 && !options::ufssTotalitySymBreak() ){ //get arbitrary ground term - //var = d_cardinality_term; - //}else{ + var = d_cardinality_term; + }else{ std::stringstream ss; ss << "_c_" << d_aloc_cardinality; var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" ); - //} + } d_totality_terms[0].push_back( var ); Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl; //must be distinct from all other cardinality terms |