diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-02 14:09:17 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-02 14:09:17 -0500 |
| commit | 20e1247461c3b6be51c08d2d6104bd1aea9bc8c3 (patch) | |
| tree | 3d5ce9847d0cd85bca2cb18a6c53296724149bcb /src/theory | |
| parent | f4d9d607c3a63a1b3842e291f06a621f71b0e966 (diff) | |
Make uf strong solver user-context dependent, fixes bug 522.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 8 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 4 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 71a342f76..c8b7d76eb 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -408,9 +408,9 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in -StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, StrongSolverTheoryUF* thss ) : d_type( n.getType() ), +StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ), d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ), - d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( 0 ), + d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ), d_cardinality_assertions( c ), d_hasCard( c, false ){ d_cardinality_term = n; } @@ -990,7 +990,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ } } } - d_aloc_cardinality++; + d_aloc_cardinality = d_aloc_cardinality + 1; //check for abort case if( options::ufssAbortCardinality()==d_aloc_cardinality ){ @@ -1574,7 +1574,7 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ SortModel* rm = NULL; if( tn.isSort() ){ Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl; - rm = new SortModel( n, d_th->getSatContext(), this ); + rm = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this ); }else{ /* if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index d263d8cc7..fa8d60b49 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -207,7 +207,7 @@ public: /** cardinality */ context::CDO< int > d_cardinality; /** maximum allocated cardinality */ - int d_aloc_cardinality; + context::CDO< int > d_aloc_cardinality; /** cardinality lemma term */ Node d_cardinality_term; /** cardinality totality terms */ @@ -228,7 +228,7 @@ public: /** get totality lemma terms */ Node getTotalityLemmaTerm( int cardinality, int i ); public: - SortModel( Node n, context::Context* c, StrongSolverTheoryUF* thss ); + SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ); virtual ~SortModel(){} /** initialize */ void initialize( OutputChannel* out ); |