From a6ef5fbd9ac3a6a247c6ecbcac2fc9e518be6f1c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Apr 2018 13:54:07 -0500 Subject: [PATCH] Remove subsort symmetry breaking (#1807) --- src/Makefile.am | 2 - src/options/uf_options.toml | 9 - src/smt/smt_engine.cpp | 3 - src/theory/quantifiers/symmetry_breaking.cpp | 316 ------------------- src/theory/quantifiers/symmetry_breaking.h | 115 ------- src/theory/sort_inference.cpp | 232 ++++++++------ src/theory/uf/theory_uf_strong_solver.cpp | 42 +-- src/theory/uf/theory_uf_strong_solver.h | 6 - 8 files changed, 142 insertions(+), 583 deletions(-) delete mode 100644 src/theory/quantifiers/symmetry_breaking.cpp delete mode 100644 src/theory/quantifiers/symmetry_breaking.h diff --git a/src/Makefile.am b/src/Makefile.am index 80bd082d6..886cd1af9 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -499,8 +499,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus_inference.h \ theory/quantifiers/sygus_sampler.cpp \ theory/quantifiers/sygus_sampler.h \ - theory/quantifiers/symmetry_breaking.cpp \ - theory/quantifiers/symmetry_breaking.h \ theory/quantifiers/term_database.cpp \ theory/quantifiers/term_database.h \ theory/quantifiers/term_enumeration.cpp \ diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index 06f58cca3..791b6e0bb 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -94,15 +94,6 @@ header = "options/uf_options.h" read_only = true help = "use cliques instead of splitting on demand to shrink model" -[[option]] - name = "ufssSymBreak" - category = "regular" - long = "uf-ss-sym-break" - type = "bool" - default = "false" - read_only = true - help = "finite model finding symmetry breaking techniques" - [[option]] name = "ufssFairness" category = "regular" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 97fbe82b8..55576870d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1846,9 +1846,6 @@ void SmtEngine::setDefaults() { options::mbqiMode.set( quantifiers::MBQI_FMC ); } } - if( options::ufssSymBreak() ){ - options::sortInference.set( true ); - } if( options::fmfFunWellDefinedRelevant() ){ if( !options::fmfFunWellDefined.wasSetByUser() ){ options::fmfFunWellDefined.set( true ); 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 - -#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()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; id_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() >::iterator it = d_sub_sorts.begin(); it != d_sub_sorts.end(); ++it ){ - int card = getStrongSolver()->getCardinality( it->first ); - for( unsigned i=0; isecond.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; igetOutputChannel().lemma( d_pending_lemmas[i], false, true ); - ++( getStrongSolver()->d_statistics.d_sym_break_lemmas ); - } - d_pending_lemmas.clear(); - return true; - }else{ - return false; - } -} - - - -} - diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h deleted file mode 100644 index 091490cec..000000000 --- a/src/theory/quantifiers/symmetry_breaking.h +++ /dev/null @@ -1,115 +0,0 @@ -/********************* */ -/*! \file symmetry_breaking.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, 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 Pre-process step for first-order reasoning - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__QUANT_SYMMETRY_BREAKING_H -#define __CVC4__QUANT_SYMMETRY_BREAKING_H - -#include -#include -#include -#include - -#include "context/cdhashmap.h" -#include "context/context.h" -#include "context/context_mm.h" -#include "expr/node.h" -#include "expr/type_node.h" -#include "theory/sort_inference.h" -#include "theory/theory.h" - -namespace CVC4 { -namespace theory { - -namespace uf { - class StrongSolverTheoryUF; -} - -class SubsortSymmetryBreaker { - typedef context::CDHashMap NodeBoolMap; - typedef context::CDHashMap NodeIntMap; - typedef context::CDHashMap NodeNodeMap; - typedef context::CDList NodeList; -private: - /** quantifiers engine */ - QuantifiersEngine* d_qe; - eq::EqualityEngine * getEqualityEngine(); - bool areDisequal( Node n1, Node n2 ); - bool areEqual( Node n1, Node n2 ); - Node getRepresentative( Node n ); - uf::StrongSolverTheoryUF * getStrongSolver(); - std::vector< Node > d_unit_lemmas; - Node d_true; - context::CDO< bool > d_conflict; -public: - SubsortSymmetryBreaker( QuantifiersEngine* qe, context::Context* c ); - ~SubsortSymmetryBreaker(){} - -private: - class TypeInfo { - public: - TypeInfo( context::Context* c ); - context::CDO< int > d_max_dom_const_sort; - context::CDO< bool > d_has_dom_const_sort; - }; - class SubSortInfo { - public: - SubSortInfo( context::Context* c ); - //list of all nodes from this (sub)type - std::vector< Node > d_nodes; - //the current domain constants for this (sub)type - NodeList d_dom_constants; - //# nodes in d_nodes that have been domain constants, size of this distinct # of domain constants seen - unsigned d_dc_nodes; - //the node we are currently watching to become a domain constant - context::CDO< int > d_first_active; - //node to id - std::map< Node, unsigned > d_node_to_id; - Node getBaseConstant() { return d_nodes.empty() ? Node::null() : d_nodes[0]; } - bool hasDomainConstant( Node n ); - unsigned getNumDomainConstants(); - Node getDomainConstant( int i ); - Node getFirstActive(eq::EqualityEngine * ee); - }; - std::map< TypeNode, std::vector< int > > d_sub_sorts; - std::map< int, TypeNode > d_sid_to_type; - std::map< TypeNode, TypeInfo * > d_t_info; - std::map< int, SubSortInfo * > d_type_info; - - TypeInfo * getTypeInfo( TypeNode tn ); - SubSortInfo * getSubSortInfo( TypeNode tn, int sid ); - - void processFirstActive( TypeNode tn, int sid, int curr_card ); -private: - //void printDebugNodeInfo( const char * c, Node n ); - void printDebugSubSortInfo( const char * c, TypeNode tn, int sid ); - /** fact list */ - std::vector< Node > d_pending_lemmas; - std::vector< Node > d_lemmas; -public: - /** new node */ - void newEqClass( Node n ); - /** merge */ - void merge( Node a, Node b ); - /** assert disequal */ - void assertDisequal( Node a, Node b ); - /** check */ - bool check( Theory::Effort level ); -}; - -} -} - -#endif diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index b469ac9d0..7a059771f 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -117,6 +117,7 @@ void SortInference::reset() { void SortInference::simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference ){ if( doSortInference ){ Trace("sort-inference-proc") << "Calculating sort inference..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); //process all assertions std::map< Node, int > visited; for( unsigned i=0; i& assertions, bool doSortInfere Trace("sort-inference") << std::endl; } - if( !options::ufssSymBreak() ){ - bool rewritten = false; - //determine monotonicity of sorts - Trace("sort-inference-proc") << "Calculating monotonicty for subsorts..." << std::endl; - std::map< Node, std::map< int, bool > > visited; - for( unsigned i=0; i var_bound; - processMonotonic( assertions[i], true, true, var_bound, visited ); - } - Trace("sort-inference-proc") << "...done" << std::endl; - - Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl; - for( unsigned i=0; i > visitedm; + for (const Node& a : assertions) + { + Trace("sort-inference-debug") << "Process monotonicity for " << a + << std::endl; + std::map var_bound; + processMonotonic(a, true, true, var_bound, visitedm); + } + Trace("sort-inference-proc") << "...done" << std::endl; + + Trace("sort-inference") << "We have " << d_sub_sorts.size() + << " sub-sorts : " << std::endl; + for (unsigned i = 0, size = d_sub_sorts.size(); i < size; i++) + { + printSort("sort-inference", d_sub_sorts[i]); + if (d_type_types.find(d_sub_sorts[i]) != d_type_types.end()) + { + Trace("sort-inference") << " is interpreted." << std::endl; + } + else if (d_non_monotonic_sorts.find(d_sub_sorts[i]) + == d_non_monotonic_sorts.end()) + { + Trace("sort-inference") << " is monotonic." << std::endl; + } + else + { + Trace("sort-inference") << " is not monotonic." << std::endl; } + } - //simplify all assertions by introducing new symbols wherever necessary - Trace("sort-inference-proc") << "Perform simplification..." << std::endl; - std::map< Node, std::map< TypeNode, Node > > visited2; - for( unsigned i=0; i var_bound; - Trace("sort-inference-debug") << "Simplify " << assertions[i] << std::endl; - TypeNode tnn; - Node curr = simplifyNode( assertions[i], var_bound, tnn, visited2 ); - Trace("sort-inference-debug") << "Done." << std::endl; - if( curr!=assertions[i] ){ - Trace("sort-inference-debug") << "Rewrite " << curr << std::endl; - curr = theory::Rewriter::rewrite( curr ); - rewritten = true; - Trace("sort-inference-rewrite") << assertions << std::endl; - Trace("sort-inference-rewrite") << " --> " << curr << std::endl; - PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); - assertions[i] = curr; - } + // simplify all assertions by introducing new symbols wherever necessary + Trace("sort-inference-proc") << "Perform simplification..." << std::endl; + std::map > visited2; + for (unsigned i = 0, size = assertions.size(); i < size; i++) + { + Node prev = assertions[i]; + std::map var_bound; + Trace("sort-inference-debug") << "Simplify " << prev << std::endl; + TypeNode tnn; + Node curr = simplifyNode(assertions[i], var_bound, tnn, visited2); + Trace("sort-inference-debug") << "Done." << std::endl; + if (curr != assertions[i]) + { + Trace("sort-inference-debug") << "Rewrite " << curr << std::endl; + curr = theory::Rewriter::rewrite(curr); + rewritten = true; + Trace("sort-inference-rewrite") << assertions << std::endl; + Trace("sort-inference-rewrite") << " --> " << curr << std::endl; + PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]);); + assertions[i] = curr; } - Trace("sort-inference-proc") << "...done" << std::endl; - //now, ensure constants are distinct - for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){ - std::vector< Node > consts; - for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - Assert( it2->first.isConst() ); - consts.push_back( it2->second ); - } - //add lemma enforcing introduced constants to be distinct - if( consts.size()>1 ){ - Node distinct_const = NodeManager::currentNM()->mkNode( kind::DISTINCT, consts ); - Trace("sort-inference-rewrite") << "Add the constant distinctness lemma: " << std::endl; - Trace("sort-inference-rewrite") << " " << distinct_const << std::endl; - assertions.push_back( distinct_const ); - rewritten = true; - } + } + Trace("sort-inference-proc") << "...done" << std::endl; + // now, ensure constants are distinct + for (std::map >::iterator it = + d_const_map.begin(); + it != d_const_map.end(); + ++it) + { + std::vector consts; + for (std::map::iterator it2 = it->second.begin(); + it2 != it->second.end(); + ++it2) + { + Assert(it2->first.isConst()); + consts.push_back(it2->second); + } + // add lemma enforcing introduced constants to be distinct + if (consts.size() > 1) + { + Node distinct_const = nm->mkNode(kind::DISTINCT, consts); + Trace("sort-inference-rewrite") + << "Add the constant distinctness lemma: " << std::endl; + Trace("sort-inference-rewrite") << " " << distinct_const << std::endl; + assertions.push_back(distinct_const); + rewritten = true; } + } - //enforce constraints based on monotonicity - Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl; - for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){ - int nmonSort = -1; - for( unsigned i=0; isecond.size(); i++ ){ - if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ - nmonSort = it->second[i]; - break; - } + // enforce constraints based on monotonicity + Trace("sort-inference-proc") << "Enforce monotonicity..." << std::endl; + for (std::map >::iterator it = + d_type_sub_sorts.begin(); + it != d_type_sub_sorts.end(); + ++it) + { + int nmonSort = -1; + unsigned nsorts = it->second.size(); + for (unsigned i = 0; i < nsorts; i++) + { + if (d_non_monotonic_sorts.find(it->second[i]) + != d_non_monotonic_sorts.end()) + { + nmonSort = it->second[i]; + break; } - if( nmonSort!=-1 ){ - std::vector< Node > injections; - TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first ); - for( unsigned i=0; isecond.size(); i++ ){ - if( it->second[i]!=nmonSort ){ - TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first ); - //make injection to nmonSort - Node a1 = mkInjection( new_tn, base_tn ); - injections.push_back( a1 ); - if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ - //also must make injection from nmonSort to this - Node a2 = mkInjection( base_tn, new_tn ); - injections.push_back( a2 ); - } + } + if (nmonSort != -1) + { + std::vector injections; + TypeNode base_tn = getOrCreateTypeForId(nmonSort, it->first); + for (unsigned i = 0; i < nsorts; i++) + { + if (it->second[i] != nmonSort) + { + TypeNode new_tn = getOrCreateTypeForId(it->second[i], it->first); + // make injection to nmonSort + Node a1 = mkInjection(new_tn, base_tn); + injections.push_back(a1); + if (d_non_monotonic_sorts.find(it->second[i]) + != d_non_monotonic_sorts.end()) + { + // also must make injection from nmonSort to this + Node a2 = mkInjection(base_tn, new_tn); + injections.push_back(a2); } } + } + if (Trace.isOn("sort-inference-rewrite")) + { Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl; - for( unsigned j=0; j var_bound; - processMonotonic( assertions[i], true, true, var_bound, visited, true ); + processMonotonic(a, true, true, var_bound, visitedmt, true); } Trace("sort-inference-proc") << "...done" << std::endl; } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 76cb95867..0e3f9c7a2 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" #include "theory/theory_model.h" -#include "theory/quantifiers/symmetry_breaking.h" //#define ONE_SPLIT_REGION //#define DISABLE_QUICK_CLIQUE_CHECKS @@ -144,9 +143,6 @@ void Region::setEqual( Node a, Node b ){ if( !isDisequal( a, n, t ) ){ setDisequal( a, n, t, true ); nr->setDisequal( n, a, t, true ); - if( options::ufssSymBreak() ){ - d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n ); - } } setDisequal( b, n, t, false ); nr->setDisequal( n, b, t, false ); @@ -608,12 +604,6 @@ void SortModel::merge( Node a, Node b ){ d_regions_map[b] = -1; } d_reps = d_reps - 1; - - if( !d_conflict ){ - if( options::ufssSymBreak() ){ - d_thss->getSymmetryBreaker()->merge(a, b); - } - } } } } @@ -659,12 +649,6 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ checkRegion( ai ); checkRegion( bi ); } - - if( !d_conflict ){ - if( options::ufssSymBreak() ){ - d_thss->getSymmetryBreaker()->assertDisequal(a, b); - } - } } } } @@ -1508,7 +1492,8 @@ Node SortModel::getCardinalityLiteral( int c ) { StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, - OutputChannel& out, TheoryUF* th) + OutputChannel& out, + TheoryUF* th) : d_out(&out), d_th(th), d_conflict(c, false), @@ -1518,11 +1503,8 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, d_min_pos_com_card(c, -1), d_card_assertions_eqv_lemma(u), d_min_pos_tn_master_card(c, -1), - d_rel_eqc(c), - d_sym_break(NULL) { - if (options::ufssSymBreak()) { - d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c); - } + d_rel_eqc(c) +{ } StrongSolverTheoryUF::~StrongSolverTheoryUF() { @@ -1530,9 +1512,6 @@ StrongSolverTheoryUF::~StrongSolverTheoryUF() { it != d_rep_model.end(); ++it) { delete it->second; } - if (d_sym_break) { - delete d_sym_break; - } } SortInference* StrongSolverTheoryUF::getSortInference() { @@ -1555,9 +1534,6 @@ void StrongSolverTheoryUF::ensureEqc( SortModel* c, Node a ) { d_rel_eqc[a] = true; Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; c->newEqClass( a ); - if( options::ufssSymBreak() ){ - d_sym_break->newEqClass( a ); - } Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; } } @@ -1589,9 +1565,6 @@ void StrongSolverTheoryUF::newEqClass( Node a ){ #else Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; c->newEqClass( a ); - if( options::ufssSymBreak() ){ - d_sym_break->newEqClass( a ); - } Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; #endif } @@ -1790,10 +1763,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ break; } } - //check symmetry breaker - if( !d_conflict && options::ufssSymBreak() ){ - d_sym_break->check( level ); - } }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){ if( level==Theory::EFFORT_FULL ){ // split on an equality between two equivalence classes (at most one per type) @@ -2125,7 +2094,6 @@ StrongSolverTheoryUF::Statistics::Statistics(): d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0), d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0), d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0), - d_sym_break_lemmas("StrongSolverTheoryUF::Symmetry_Breaking_Lemmas", 0), d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0), d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1) { @@ -2133,7 +2101,6 @@ StrongSolverTheoryUF::Statistics::Statistics(): smtStatisticsRegistry()->registerStat(&d_clique_lemmas); smtStatisticsRegistry()->registerStat(&d_split_lemmas); smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas); - smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas); smtStatisticsRegistry()->registerStat(&d_totality_lemmas); smtStatisticsRegistry()->registerStat(&d_max_model_size); } @@ -2143,7 +2110,6 @@ StrongSolverTheoryUF::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas); smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas); smtStatisticsRegistry()->unregisterStat(&d_max_model_size); } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index f634a493c..ecbfd9a87 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -26,7 +26,6 @@ namespace CVC4 { class SortInference; namespace theory { -class SubsortSymmetryBreaker; namespace uf { class TheoryUF; } /* namespace CVC4::theory::uf */ @@ -370,8 +369,6 @@ public: ~StrongSolverTheoryUF(); /** get theory */ TheoryUF* getTheory() { return d_th; } - /** symmetry breaker */ - SubsortSymmetryBreaker* getSymmetryBreaker() { return d_sym_break; } /** get sort inference module */ SortInference* getSortInference(); /** get default sat context */ @@ -421,7 +418,6 @@ public: IntStat d_clique_lemmas; IntStat d_split_lemmas; IntStat d_disamb_term_lemmas; - IntStat d_sym_break_lemmas; IntStat d_totality_lemmas; IntStat d_max_model_size; Statistics(); @@ -468,8 +464,6 @@ public: context::CDO d_min_pos_tn_master_card; /** relevant eqc */ NodeBoolMap d_rel_eqc; - /** symmetry breaking techniques */ - SubsortSymmetryBreaker* d_sym_break; }; /* class StrongSolverTheoryUF */ -- 2.30.2