Remove subsort symmetry breaking (#1807)

1 files changed, 0 insertions, 316 deletions

diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
deleted file mode 100644
index a8218480b..000000000
--- a/src/theory/quantifiers/symmetry_breaking.cpp
+++ /dev/null
@@ -1,316 +0,0 @@
-/*********************                                                        */
-/*! \file symmetry_breaking.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Paul Meng, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief symmetry breaking module
- **
- **/
-
-#include "theory/quantifiers/symmetry_breaking.h"
-
-#include <vector>
-
-#include "theory/quantifiers_engine.h"
-#include "theory/rewriter.h"
-#include "theory/sort_inference.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.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 {
-
-
-SubsortSymmetryBreaker::SubsortSymmetryBreaker(QuantifiersEngine* qe, context::Context* c) :
-d_qe(qe), d_conflict(c,false) {
-  d_true =  NodeManager::currentNM()->mkConst( true );
-}
-
-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::TypeInfo::TypeInfo( context::Context * c ) :
-d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false) {
-}
-
-SubsortSymmetryBreaker::SubSortInfo::SubSortInfo( context::Context * c ) :
-d_dom_constants( c ), d_first_active( c, 0 ){
-  d_dc_nodes = 0;
-}
-
-unsigned SubsortSymmetryBreaker::SubSortInfo::getNumDomainConstants() {
-  if( d_nodes.empty() ){
-    return 0;
-  }else{
-    return 1 + d_dom_constants.size();
-  }
-}
-
-Node SubsortSymmetryBreaker::SubSortInfo::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::SubSortInfo::getFirstActive(eq::EqualityEngine * ee) {
-  if( d_first_active.get()<(int)d_nodes.size() ){
-    Node fa = d_nodes[d_first_active.get()];
-    return ee->hasTerm( fa ) ? fa : Node::null();
-  }else{
-    return Node::null();
-  }
-}
-
-SubsortSymmetryBreaker::TypeInfo * SubsortSymmetryBreaker::getTypeInfo( TypeNode tn ) {
-  if( d_t_info.find( tn )==d_t_info.end() ){
-    d_t_info[tn] = new TypeInfo( d_qe->getSatContext() );
-  }
-  return d_t_info[tn];
-}
-
-SubsortSymmetryBreaker::SubSortInfo * SubsortSymmetryBreaker::getSubSortInfo( TypeNode tn, int sid ) {
-  if( d_type_info.find( sid )==d_type_info.end() ){
-    d_type_info[sid] = new SubSortInfo( 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;
-      SubSortInfo * ti = getSubSortInfo( 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 );
-      }
-      TypeInfo * tti = getTypeInfo( tn );
-      if( !tti->d_has_dom_const_sort.get() ){
-        tti->d_has_dom_const_sort.set( true );
-        tti->d_max_dom_const_sort.set( sid );
-      }
-    }
-  }
-  Trace("sym-break-temp") << "Done new eq class" << std::endl;
-}
-
-
-
-void SubsortSymmetryBreaker::merge( Node a, Node b ) {
-  if( Trace.isOn("sym-break-debug") ){
-    SortInference * si = d_qe->getTheoryEngine()->getSortInference();
-    int as = si->getSortId( a );
-    int bs = si->getSortId( b );
-    Trace("sym-break-debug") << "SSB: New merge " << a.getType() << " :: " << a << " : " << as;
-    Trace("sym-break-debug") << " == " << b << " : " << bs << std::endl;
-  }
-}
-
-void SubsortSymmetryBreaker::assertDisequal( Node a, Node b ) {
-  if( Trace.isOn("sym-break-debug") ){
-    SortInference * si = d_qe->getTheoryEngine()->getSortInference();
-    int as = si->getSortId( a );
-    int bs = si->getSortId( b );
-    Trace("sym-break-debug") << "SSB: New assert disequal " << a.getType() << " :: " << a << " : " << as;
-    Trace("sym-break-debug") << " != " << b << " : " << bs << std::endl;
-  }
-}
-
-void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_card ){
-  SubSortInfo * ti = getSubSortInfo( tn, sid );
-  if( (int)ti->getNumDomainConstants()<curr_card ){
-      //static int checkCount = 0;
-      //checkCount++;
-      //if( checkCount%1000==0 ){
-      //  std::cout << "Check count = " << checkCount << std::endl;
-      //}
-
-    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(getEqualityEngine());
-    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;
-        TypeInfo * tti = getTypeInfo( tn );
-        Assert( tti->d_has_dom_const_sort.get() );
-        int msid = tti->d_max_dom_const_sort.get();
-        SubSortInfo * max_ti = getSubSortInfo( 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;
-          tti->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;
-            SubSortInfo * 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 << "==" << tti->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(getEqualityEngine());
-      }
-    }
-  }
-}
-
-void SubsortSymmetryBreaker::printDebugSubSortInfo( const char * c, TypeNode tn, int sid ) {
-  Trace(c) << "SubSortInfo( " << tn << ", " << sid << " ) = " << std::endl;
-  Trace(c) << "  Domain constants : ";
-  SubSortInfo * ti = getSubSortInfo( 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(getEqualityEngine()) << std::endl;
-}
-
-bool SubsortSymmetryBreaker::check( Theory::Effort level ) {
-
-  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], false, true );
-      ++( getStrongSolver()->d_statistics.d_sym_break_lemmas );
-    }
-    d_pending_lemmas.clear();
-    return true;
-  }else{
-    return false;
-  }
-}
-
-
-
-}
-