diff options
Diffstat (limited to 'src/theory/quantifiers/symmetry_breaking.cpp')
| -rwxr-xr-x | src/theory/quantifiers/symmetry_breaking.cpp | 296 |
1 files changed, 296 insertions, 0 deletions
diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp new file mode 100755 index 000000000..6a7baebb1 --- /dev/null +++ b/src/theory/quantifiers/symmetry_breaking.cpp @@ -0,0 +1,296 @@ +/********************* */ +/*! \file symmetry_breaking.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief symmetry breaking module + ** + **/ + +#include <vector> + +#include "theory/quantifiers/symmetry_breaking.h" +#include "theory/rewriter.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" +#include "util/sort_inference.h" +#include "theory/uf/theory_uf_strong_solver.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace std; + +namespace CVC4 { + +eq::EqualityEngine * SubsortSymmetryBreaker::getEqualityEngine() { + return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine(); +} + +bool SubsortSymmetryBreaker::areEqual( Node n1, Node n2 ) { + return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 ); +} + +bool SubsortSymmetryBreaker::areDisequal( Node n1, Node n2 ) { + return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false ); +} + + +Node SubsortSymmetryBreaker::getRepresentative( Node n ) { + return getEqualityEngine()->getRepresentative( n ); +} + +uf::StrongSolverTheoryUF * SubsortSymmetryBreaker::getStrongSolver() { + return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getStrongSolver(); +} + +SubsortSymmetryBreaker::SubsortSymmetryBreaker(QuantifiersEngine* qe, context::Context* c) : +d_qe(qe), d_conflict(c,false), d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false), +d_fact_index(c,0), d_fact_list(c) { + d_true = NodeManager::currentNM()->mkConst( true ); +} + +SubsortSymmetryBreaker::TypeInfo::TypeInfo( SubsortSymmetryBreaker * ssb, context::Context * c ) : +d_ssb( ssb ), d_dom_constants( c ), d_first_active( c, 0 ){ + d_dc_nodes = 0; +} + +unsigned SubsortSymmetryBreaker::TypeInfo::getNumDomainConstants() { + if( d_nodes.empty() ){ + return 0; + }else{ + return 1 + d_dom_constants.size(); + } +} + +Node SubsortSymmetryBreaker::TypeInfo::getDomainConstant( int i ) { + if( i==0 ){ + return d_nodes[0]; + }else{ + Assert( i<=(int)d_dom_constants.size() ); + return d_dom_constants[i-1]; + } +} + +Node SubsortSymmetryBreaker::TypeInfo::getFirstActive() { + if( d_first_active.get()<(int)d_nodes.size() ){ + Node fa = d_nodes[d_first_active.get()]; + return d_ssb->getEqualityEngine()->hasTerm( fa ) ? fa : Node::null(); + }else{ + return Node::null(); + } +} + +SubsortSymmetryBreaker::TypeInfo * SubsortSymmetryBreaker::getTypeInfo( TypeNode tn, int sid ) { + if( d_type_info.find( sid )==d_type_info.end() ){ + d_type_info[sid] = new TypeInfo( this, d_qe->getSatContext() ); + d_sub_sorts[tn].push_back( sid ); + d_sid_to_type[sid] = tn; + } + return d_type_info[sid]; +} + +void SubsortSymmetryBreaker::newEqClass( Node n ) { + Trace("sym-break-temp") << "New eq class " << n << std::endl; + if( !d_conflict ){ + TypeNode tn = n.getType(); + SortInference * si = d_qe->getTheoryEngine()->getSortInference(); + if( si->isWellSorted( n ) ){ + int sid = si->getSortId( n ); + Trace("sym-break-debug") << "SSB: New eq class " << n << " : " << n.getType() << " : " << sid << std::endl; + TypeInfo * ti = getTypeInfo( tn, sid ); + if( std::find( ti->d_nodes.begin(), ti->d_nodes.end(), n )==ti->d_nodes.end() ){ + if( ti->d_nodes.empty() ){ + //for first subsort, we add unit equality + if( d_sub_sorts[tn][0]!=sid ){ + Trace("sym-break-temp") << "Do sym break unit with " << d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() << std::endl; + //add unit symmetry breaking lemma + Node eq = n.eqNode( d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() ); + eq = Rewriter::rewrite( eq ); + d_unit_lemmas.push_back( eq ); + Trace("sym-break-lemma") << "*** SymBreak : Unit lemma (" << sid << "==" << d_sub_sorts[tn][0] << ") : " << eq << std::endl; + d_pending_lemmas.push_back( eq ); + } + Trace("sym-break-dc") << "* Set first domain constant : " << n << " for " << tn << " : " << sid << std::endl; + ti->d_dc_nodes++; + } + ti->d_node_to_id[n] = ti->d_nodes.size(); + ti->d_nodes.push_back( n ); + } + if( !d_has_dom_const_sort.get() ){ + d_has_dom_const_sort.set( true ); + d_max_dom_const_sort.set( sid ); + } + } + } + Trace("sym-break-temp") << "Done new eq class" << std::endl; +} + + + +void SubsortSymmetryBreaker::merge( Node a, Node b ) { + +} + +void SubsortSymmetryBreaker::assertDisequal( Node a, Node b ) { + +} + +void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_card ){ + TypeInfo * ti = getTypeInfo( tn, sid ); + if( (int)ti->getNumDomainConstants()<curr_card ){ + Trace("sym-break-dc-debug") << "Check for domain constants " << tn << " : " << sid << ", curr_card = " << curr_card << ", "; + Trace("sym-break-dc-debug") << "#domain constants = " << ti->getNumDomainConstants() << std::endl; + Node fa = ti->getFirstActive(); + bool invalid = true; + while( invalid && !fa.isNull() && (int)ti->getNumDomainConstants()<curr_card ){ + invalid = false; + unsigned deq = 0; + for( unsigned i=0; i<ti->getNumDomainConstants(); i++ ){ + Node dc = ti->getDomainConstant( i ); + if( areEqual( fa, dc ) ){ + invalid = true; + break; + }else if( areDisequal( fa, dc ) ){ + deq++; + } + } + if( deq==ti->getNumDomainConstants() ){ + Trace("sym-break-dc") << "* Can infer domain constant #" << ti->getNumDomainConstants()+1; + Trace("sym-break-dc") << " : " << fa << " for " << tn << " : " << sid << std::endl; + //add to domain constants + ti->d_dom_constants.push_back( fa ); + if( ti->d_node_to_id[fa]>ti->d_dc_nodes ){ + Trace("sym-break-dc-debug") << "Swap nodes... " << ti->d_dc_nodes << " " << ti->d_node_to_id[fa] << " " << ti->d_nodes.size() << std::endl; + //swap + Node on = ti->d_nodes[ti->d_dc_nodes]; + int id = ti->d_node_to_id[fa]; + + ti->d_nodes[ti->d_dc_nodes] = fa; + ti->d_nodes[id] = on; + ti->d_node_to_id[fa] = ti->d_dc_nodes; + ti->d_node_to_id[on] = id; + } + ti->d_dc_nodes++; + Trace("sym-break-dc-debug") << "Get max type info..." << std::endl; + Assert( d_has_dom_const_sort.get() ); + int msid = d_max_dom_const_sort.get(); + TypeInfo * max_ti = getTypeInfo( d_sid_to_type[msid], msid ); + Trace("sym-break-dc-debug") << "Swap nodes..." << std::endl; + //now, check if we can apply symmetry breaking to another sort + if( ti->getNumDomainConstants()>max_ti->getNumDomainConstants() ){ + Trace("sym-break-dc") << "Max domain constant subsort for " << tn << " becomes " << sid << std::endl; + d_max_dom_const_sort.set( sid ); + }else if( ti!=max_ti ){ + //construct symmetry breaking lemma + //current domain constant must be disequal from all current ones + Trace("sym-break-dc") << "Get domain constant " << ti->getNumDomainConstants()-1; + Trace("sym-break-dc") << " from max_ti, " << max_ti->getNumDomainConstants() << std::endl; + //apply a symmetry breaking lemma + Node m = max_ti->getDomainConstant(ti->getNumDomainConstants()-1); + //if fa and m are disequal from all previous domain constants in the other sort + std::vector< Node > cc; + for( unsigned r=0; r<2; r++ ){ + Node n = ((r==0)==(msid>sid)) ? fa : m; + Node on = ((r==0)==(msid>sid)) ? m : fa; + TypeInfo * t = ((r==0)==(msid>sid)) ? max_ti : ti; + for( unsigned i=0; i<t->d_node_to_id[on]; i++ ){ + cc.push_back( n.eqNode( t->d_nodes[i] ) ); + } + } + //then, we can assume fa = m + cc.push_back( fa.eqNode( m ) ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, cc ); + lem = Rewriter::rewrite( lem ); + if( std::find( d_lemmas.begin(), d_lemmas.end(), lem )==d_lemmas.end() ){ + d_lemmas.push_back( lem ); + Trace("sym-break-lemma") << "*** Symmetry break lemma for " << tn << " (" << sid << "==" << d_max_dom_const_sort.get() << ") : "; + Trace("sym-break-lemma") << lem << std::endl; + d_pending_lemmas.push_back( lem ); + } + } + invalid = true; + } + if( invalid ){ + ti->d_first_active.set( ti->d_first_active + 1 ); + fa = ti->getFirstActive(); + } + } + } +} + +void SubsortSymmetryBreaker::printDebugTypeInfo( const char * c, TypeNode tn, int sid ) { + Trace(c) << "TypeInfo( " << tn << ", " << sid << " ) = " << std::endl; + Trace(c) << " Domain constants : "; + TypeInfo * ti = getTypeInfo( tn, sid ); + for( NodeList::const_iterator it = ti->d_dom_constants.begin(); it != ti->d_dom_constants.end(); ++it ){ + Node dc = *it; + Trace(c) << dc << " "; + } + Trace(c) << std::endl; + Trace(c) << " First active node : " << ti->getFirstActive() << std::endl; +} + + +void SubsortSymmetryBreaker::queueFact( Node n ) { + d_fact_list.push_back( n ); + /* + if( n.getKind()==EQUAL ){ + merge( n[0], n[1] ); + }else if( n.getKind()==NOT && n[0].getKind()==EQUAL ){ + assertDisequal( n[0][0], n[0][1] ); + }else{ + newEqClass( n ); + } + */ +} + +bool SubsortSymmetryBreaker::check( Theory::Effort level ) { + d_pending_lemmas.clear(); + + Trace("sym-break-debug") << "SymBreak : check " << level << std::endl; + while( d_fact_index.get()<d_fact_list.size() ){ + Node f = d_fact_list[d_fact_index.get()]; + d_fact_index.set( d_fact_index.get() + 1 ); + if( f.getKind()==EQUAL ){ + merge( f[0], f[1] ); + }else if( f.getKind()==NOT && f[0].getKind()==EQUAL ){ + assertDisequal( f[0][0], f[0][1] ); + }else{ + newEqClass( f ); + } + } + Trace("sym-break-debug") << "SymBreak : update first actives" << std::endl; + for( std::map< TypeNode, std::vector< int > >::iterator it = d_sub_sorts.begin(); it != d_sub_sorts.end(); ++it ){ + int card = getStrongSolver()->getCardinality( it->first ); + for( unsigned i=0; i<it->second.size(); i++ ){ + //check if the first active is disequal from all domain constants + processFirstActive( it->first, it->second[i], card ); + } + } + + + Trace("sym-break-debug") << "SymBreak : finished check, now flush lemmas... (#lemmas = " << d_pending_lemmas.size() << ")" << std::endl; + //flush pending lemmas + if( !d_pending_lemmas.empty() ){ + for( unsigned i=0; i<d_pending_lemmas.size(); i++ ){ + getStrongSolver()->getOutputChannel().lemma( d_pending_lemmas[i] ); + ++( getStrongSolver()->d_statistics.d_sym_break_lemmas ); + } + d_pending_lemmas.clear(); + return true; + }else{ + return false; + } +} + + + +} + |