diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:07 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:21 -0500 |
commit | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (patch) | |
tree | 409009a6ab55986308cc73d030db53489beef26d /src/theory/uf | |
parent | 3eaf02c01e74a2a43b2eff7638d6c16171a11a13 (diff) |
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/options | 5 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 94 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 6 |
3 files changed, 81 insertions, 24 deletions
diff --git a/src/theory/uf/options b/src/theory/uf/options index bed535342..437e30e46 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -23,6 +23,8 @@ option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1 apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default) option ufssTotalityLazy --uf-ss-totality-lazy bool :default false apply totality axioms lazily +option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false + apply symmetry breaking for totality axioms option ufssAbortCardinality --uf-ss-abort-card=N int :default -1 tells the uf strong solver a cardinality to abort at (-1 == no limit, default) option ufssSmartSplits --uf-ss-smart-split bool :default false @@ -35,5 +37,8 @@ option ufssDiseqPropagation --uf-ss-deq-prop bool :default false eagerly propagate disequalities for uf strong solver option ufssMinimalModel /--disable-uf-ss-min-model bool :default true disable finding a minimal model in uf strong solver +option ufssCliqueSplits --uf-ss-clique-splits bool :default false + use cliques instead of splitting on demand to shrink model + endmodule diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index e868460f8..baa40463f 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -322,6 +322,20 @@ bool StrongSolverTheoryUF::SortModel::Region::check( Theory::Effort level, int c return false; } +bool StrongSolverTheoryUF::SortModel::Region::getCandidateClique( int cardinality, std::vector< Node >& clique ) { + if( d_testCliqueSize>=long(cardinality+1) ){ + //test clique is a clique + for( NodeBoolMap::iterator it = d_testClique.begin(); it != d_testClique.end(); ++it ){ + if( (*it).second ){ + clique.push_back( (*it).first ); + } + } + return true; + } + return false; +} + + void StrongSolverTheoryUF::SortModel::Region::getRepresentatives( std::vector< Node >& reps ){ for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){ RegionNodeInfo* rni = it->second; @@ -625,11 +639,21 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel //see if we have any recommended splits from large regions for( int i=0; i<(int)d_regions_index; i++ ){ if( d_regions[i]->d_valid && d_regions[i]->getNumReps()>d_cardinality ){ - if( addSplit( d_regions[i], out ) ){ - addedLemma = true; + //just add the clique lemma + if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){ + std::vector< Node > clique; + if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){ + //add clique lemma + addCliqueLemma( clique, out ); + return; + } + }else{ + if( addSplit( d_regions[i], out ) ){ + addedLemma = true; #ifdef ONE_SPLIT_REGION - break; + break; #endif + } } } } @@ -977,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 ){ //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 @@ -1097,6 +1121,12 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu while( clique.size()>size_t(d_cardinality+1) ){ clique.pop_back(); } + //debugging information + if( Trace.isOn("uf-ss-cliques") ){ + std::vector< Node > clique_vec; + clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); + d_cliques[ d_cardinality ].push_back( clique_vec ); + } if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){ //add as lemma std::vector< Node > eqs; @@ -1109,16 +1139,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu } eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() ); Node lem = NodeManager::currentNM()->mkNode( OR, eqs ); - Trace("uf-ss-lemma") << "*** Add clique conflict " << lem << std::endl; + Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl; ++( d_thss->d_statistics.d_clique_lemmas ); out->lemma( lem ); }else{ - //debugging information - if( Trace.isOn("uf-ss-cliques") ){ - std::vector< Node > clique_vec; - clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); - d_cliques[ d_cardinality ].push_back( clique_vec ); - } //found a clique Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl; Debug("uf-ss-cliques") << " "; @@ -1243,17 +1267,39 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu } void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){ - Node cardLit = d_cardinality_literal[ cardinality ]; - std::vector< Node > eqs; - for( int i=0; i<cardinality; i++ ){ - eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) ); + if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){ + if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){ + d_totality_lems[n].push_back( cardinality ); + Node cardLit = d_cardinality_literal[ cardinality ]; + int sort_id = 0; + if( options::sortInference() ){ + sort_id = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(n); + } + Trace("uf-ss-totality") << "Add totality lemma for " << n << " " << cardinality << ", sort id is " << sort_id << std::endl; + int use_cardinality = cardinality; + if( options::ufssTotalitySymBreak() ){ + if( d_sym_break_index.find(n)!=d_sym_break_index.end() ){ + use_cardinality = d_sym_break_index[n]; + }else if( (int)d_sym_break_terms[n.getType()][sort_id].size()<cardinality-1 ){ + use_cardinality = d_sym_break_terms[n.getType()][sort_id].size() + 1; + d_sym_break_terms[n.getType()][sort_id].push_back( n ); + d_sym_break_index[n] = use_cardinality; + Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n << ", index = " << use_cardinality << std::endl; + } + } + + std::vector< Node > eqs; + for( int i=0; i<use_cardinality; i++ ){ + eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) ); + } + Node ax = NodeManager::currentNM()->mkNode( OR, eqs ); + Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax ); + Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl; + //send as lemma to the output channel + d_thss->getOutputChannel().lemma( lem ); + ++( d_thss->d_statistics.d_totality_lemmas ); + } } - Node ax = NodeManager::currentNM()->mkNode( OR, eqs ); - Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax ); - Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl; - //send as lemma to the output channel - d_thss->getOutputChannel().lemma( lem ); - ++( d_thss->d_statistics.d_totality_lemmas ); } /** apply totality */ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 0cc995723..d263d8cc7 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -45,6 +45,10 @@ protected: public: /** information for incremental conflict/clique finding for a particular sort */ class SortModel { + private: + std::map< Node, std::vector< int > > d_totality_lems; + std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms; + std::map< Node, int > d_sym_break_index; public: /** a partition of the current equality graph for which cliques can occur internally */ class Region { @@ -146,6 +150,8 @@ public: public: /** check for cliques */ bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique ); + /** get candidate clique */ + bool getCandidateClique( int cardinality, std::vector< Node >& clique ); //print debug void debugPrint( const char* c, bool incClique = false ); }; |