diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-11-06 12:31:31 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-06 17:19:09 -0600 |
commit | 6d2def1c2e44974227fb06d3aa199722a4193a04 (patch) | |
tree | 1020f03dfbef0e9e5c8759b888dd75885aa2ac37 /src/theory/uf | |
parent | 4ab031f6173ca18aa21c938bc2672ef25c283428 (diff) |
Bug fixes for bounded integer quantification. Current best strategy is to turn off MBQI. Disable relevant triggers by default.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 16 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 46 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 4 |
3 files changed, 43 insertions, 23 deletions
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index c0d114052..284212ba9 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -345,14 +345,14 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v; if( optUsePartialDefaults() ){ if( !ground ){ - int defSize = (int)d_defaults.size(); - for( int i=0; i<defSize; i++ ){ - //for soundness, to allow variable order-independent function interpretations, - // we must ensure that the intersection of all default terms - // is also defined. - //for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., - // then we must define f( b, a ). - if (!options::fmfFullModelCheck()) { + if (!options::fmfFullModelCheck()) { + int defSize = (int)d_defaults.size(); + for( int i=0; i<defSize; i++ ){ + //for soundness, to allow variable order-independent function interpretations, + // we must ensure that the intersection of all default terms + // is also defined. + //for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., + // then we must define f( b, a ). bool isGround; Node ni = getIntersection( m, n, d_defaults[i], isGround ); if( !ni.isNull() ){ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 8aa7d625d..4ef11c042 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -542,7 +542,9 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso //if they are not already disequal a = d_thss->getTheory()->d_equalityEngine.getRepresentative( a ); b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b ); - if( !d_thss->getTheory()->d_equalityEngine.areDisequal( a, b, true ) ){ + int ai = d_regions_map[a]; + int bi = d_regions_map[b]; + if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){ Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl; //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) || // a!=reason[0][0] || b!=reason[0][1] ){ @@ -559,8 +561,6 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso //now, add disequalities to regions Assert( d_regions_map.find( a )!=d_regions_map.end() ); Assert( d_regions_map.find( b )!=d_regions_map.end() ); - int ai = d_regions_map[a]; - int bi = d_regions_map[b]; Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; if( ai==bi ){ //internal disequality @@ -663,11 +663,15 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel return; } }else{ - if( addSplit( d_regions[i], out ) ){ + int sp = addSplit( d_regions[i], out ); + if( sp==1 ){ addedLemma = true; #ifdef ONE_SPLIT_REGION break; #endif + }else if( sp==-1 ){ + check( level, out ); + return; } } } @@ -771,6 +775,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* } #endif }else{ + Trace("uf-ss-debug") << "Minimize the UF model..." << std::endl; //internal minimize, ensure that model forms a clique: // if two equivalence classes are neither equal nor disequal, add a split int validRegionIndex = -1; @@ -778,7 +783,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* if( d_regions[i]->d_valid ){ if( validRegionIndex!=-1 ){ combineRegions( validRegionIndex, i ); - if( addSplit( d_regions[validRegionIndex], out ) ){ + if( addSplit( d_regions[validRegionIndex], out )!=0 ){ return false; } }else{ @@ -786,7 +791,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* } } } - if( addSplit( d_regions[validRegionIndex], out ) ){ + if( addSplit( d_regions[validRegionIndex], out )!=0 ){ return false; } } @@ -1074,7 +1079,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ } } -bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ +int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ Node s; if( r->hasSplits() ){ if( !options::ufssSmartSplits() ){ @@ -1120,11 +1125,26 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ if (!s.isNull() ){ //add lemma to output channel Assert( s.getKind()==EQUAL ); - s = Rewriter::rewrite( s ); Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; + Node ss = Rewriter::rewrite( s ); + if( ss.getKind()!=EQUAL ){ + Node b_t = NodeManager::currentNM()->mkConst( true ); + Node b_f = NodeManager::currentNM()->mkConst( false ); + if( ss==b_f ){ + Trace("uf-ss-lemma") << "....Assert disequal directly : " << s[0] << " " << s[1] << std::endl; + assertDisequal( s[0], s[1], b_t ); + return -1; + }else{ + Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl; + } + if( ss==b_t ){ + Message() << "Bad split " << s << std::endl; + exit( 16 ); + } + } if( options::sortInference()) { for( int i=0; i<2; i++ ){ - int si = d_thss->getSortInference()->getSortId( s[i] ); + int si = d_thss->getSortInference()->getSortId( ss[i] ); Trace("uf-ss-split-si") << si << " "; } Trace("uf-ss-split-si") << std::endl; @@ -1134,13 +1154,13 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; //Notice() << "*** Split on " << s << std::endl; //split on the equality s - out->split( s ); + out->split( ss ); //tell the sat solver to explore the equals branch first - out->requirePhase( s, true ); + out->requirePhase( ss, true ); ++( d_thss->d_statistics.d_split_lemmas ); - return true; + return 1; }else{ - return false; + return 0; } } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 8e568444b..9111ec6a7 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -200,8 +200,8 @@ public: private: /** allocate cardinality */ void allocateCardinality( OutputChannel* out ); - /** add split */ - bool addSplit( Region* r, OutputChannel* out ); + /** add split 0 = no split, -1 = entailed disequality added, 1 = split added */ + int addSplit( Region* r, OutputChannel* out ); /** add clique lemma */ void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ); /** add totality axiom */ |