From 0c2eafec69b694a507ac914bf285fe0574be085f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Sep 2013 10:14:32 -0500 Subject: [PATCH] Bug fixes and improvements for symmetry breaking, it now supports multiple sorts. Working on monotonicity inference. --- src/theory/quantifiers/symmetry_breaking.cpp | 110 +++++++++------- src/theory/quantifiers/symmetry_breaking.h | 37 +++--- src/theory/uf/theory_uf_strong_solver.cpp | 12 +- src/util/sort_inference.cpp | 132 +++++++++++++++---- src/util/sort_inference.h | 13 +- 5 files changed, 204 insertions(+), 100 deletions(-) diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp index 6a7baebb1..507a50838 100755 --- a/src/theory/quantifiers/symmetry_breaking.cpp +++ b/src/theory/quantifiers/symmetry_breaking.cpp @@ -29,6 +29,12 @@ 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(); } @@ -50,18 +56,16 @@ 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( context::Context * c ) : +d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false) { } -SubsortSymmetryBreaker::TypeInfo::TypeInfo( SubsortSymmetryBreaker * ssb, context::Context * c ) : -d_ssb( ssb ), d_dom_constants( c ), d_first_active( c, 0 ){ +SubsortSymmetryBreaker::SubSortInfo::SubSortInfo( context::Context * c ) : +d_dom_constants( c ), d_first_active( c, 0 ){ d_dc_nodes = 0; } -unsigned SubsortSymmetryBreaker::TypeInfo::getNumDomainConstants() { +unsigned SubsortSymmetryBreaker::SubSortInfo::getNumDomainConstants() { if( d_nodes.empty() ){ return 0; }else{ @@ -69,7 +73,7 @@ unsigned SubsortSymmetryBreaker::TypeInfo::getNumDomainConstants() { } } -Node SubsortSymmetryBreaker::TypeInfo::getDomainConstant( int i ) { +Node SubsortSymmetryBreaker::SubSortInfo::getDomainConstant( int i ) { if( i==0 ){ return d_nodes[0]; }else{ @@ -78,18 +82,25 @@ Node SubsortSymmetryBreaker::TypeInfo::getDomainConstant( int i ) { } } -Node SubsortSymmetryBreaker::TypeInfo::getFirstActive() { +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 d_ssb->getEqualityEngine()->hasTerm( fa ) ? fa : Node::null(); + return ee->hasTerm( fa ) ? fa : Node::null(); }else{ return Node::null(); } } -SubsortSymmetryBreaker::TypeInfo * SubsortSymmetryBreaker::getTypeInfo( TypeNode tn, int sid ) { +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 TypeInfo( this, d_qe->getSatContext() ); + d_type_info[sid] = new SubSortInfo( d_qe->getSatContext() ); d_sub_sorts[tn].push_back( sid ); d_sid_to_type[sid] = tn; } @@ -104,7 +115,7 @@ void SubsortSymmetryBreaker::newEqClass( Node n ) { 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 ); + 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 @@ -123,9 +134,10 @@ void SubsortSymmetryBreaker::newEqClass( Node n ) { 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 ); + 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 ); } } } @@ -135,19 +147,37 @@ void SubsortSymmetryBreaker::newEqClass( Node n ) { 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 ){ - TypeInfo * ti = getTypeInfo( tn, sid ); + SubSortInfo * ti = getSubSortInfo( tn, sid ); if( (int)ti->getNumDomainConstants()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; - d_max_dom_const_sort.set( sid ); + 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 @@ -199,7 +230,7 @@ void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_ 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; + 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] ) ); } @@ -210,7 +241,7 @@ void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_ 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") << "*** 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 ); } @@ -219,42 +250,28 @@ void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_ } if( invalid ){ ti->d_first_active.set( ti->d_first_active + 1 ); - fa = ti->getFirstActive(); + fa = ti->getFirstActive(getEqualityEngine()); } } } } -void SubsortSymmetryBreaker::printDebugTypeInfo( const char * c, TypeNode tn, int sid ) { - Trace(c) << "TypeInfo( " << tn << ", " << sid << " ) = " << std::endl; +void SubsortSymmetryBreaker::printDebugSubSortInfo( const char * c, TypeNode tn, int sid ) { + Trace(c) << "SubSortInfo( " << tn << ", " << sid << " ) = " << std::endl; Trace(c) << " Domain constants : "; - TypeInfo * ti = getTypeInfo( tn, sid ); + 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() << 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 ); - } - */ + Trace(c) << " First active node : " << ti->getFirstActive(getEqualityEngine()) << std::endl; } bool SubsortSymmetryBreaker::check( Theory::Effort level ) { - d_pending_lemmas.clear(); 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 ); diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index 3db9097f5..05461d378 100755 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -62,11 +62,14 @@ public: private: class TypeInfo { - private: - SubsortSymmetryBreaker * d_ssb; - //bool isActive( Node n, unsigned & deq ); public: - TypeInfo( SubsortSymmetryBreaker * ssb, context::Context* c ); + 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 @@ -81,36 +84,30 @@ private: bool hasDomainConstant( Node n ); unsigned getNumDomainConstants(); Node getDomainConstant( int i ); - Node getFirstActive(); + Node getFirstActive(eq::EqualityEngine * ee); }; std::map< TypeNode, std::vector< int > > d_sub_sorts; std::map< int, TypeNode > d_sid_to_type; - std::map< int, TypeInfo * > d_type_info; - - //maximum domain constants sort - context::CDO< int > d_max_dom_const_sort; - context::CDO< bool > d_has_dom_const_sort; + std::map< TypeNode, TypeInfo * > d_t_info; + std::map< int, SubSortInfo * > d_type_info; - TypeInfo * getTypeInfo( TypeNode tn, int sid ); + 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 printDebugTypeInfo( const char * c, TypeNode tn, int sid ); + 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 ); - /** fact list */ - context::CDO< unsigned > d_fact_index; - NodeList d_fact_list; - std::vector< Node > d_pending_lemmas; - std::vector< Node > d_lemmas; -public: - /** queue fact */ - void queueFact( Node n ); /** check */ bool check( Theory::Effort level ); }; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 82cd1f809..163dd3c1f 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -120,8 +120,7 @@ void StrongSolverTheoryUF::SortModel::Region::setEqual( Node a, Node b ){ d_cf->d_thss->getDisequalityPropagator()->assertDisequal(a, n, Node::null()); } if( options::ufssSymBreak() ){ - //d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n ); - d_cf->d_thss->getSymmetryBreaker()->queueFact( a.eqNode( n ).negate() ); + d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n ); } } setDisequal( b, n, t, false ); @@ -527,8 +526,7 @@ void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){ d_thss->getDisequalityPropagator()->merge(a, b); } if( options::ufssSymBreak() ){ - //d_thss->getSymmetryBreaker()->merge(a, b); - d_thss->getSymmetryBreaker()->queueFact( a.eqNode( b ) ); + d_thss->getSymmetryBreaker()->merge(a, b); } } } @@ -583,8 +581,7 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null()); } if( options::ufssSymBreak() ){ - //d_thss->getSymmetryBreaker()->assertDisequal(a, b); - d_thss->getSymmetryBreaker()->queueFact( a.eqNode( b ).negate() ); + d_thss->getSymmetryBreaker()->assertDisequal(a, b); } } } @@ -1478,8 +1475,7 @@ void StrongSolverTheoryUF::newEqClass( Node n ){ Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << n << " : " << n.getType() << std::endl; c->newEqClass( n ); if( options::ufssSymBreak() ){ - //d_sym_break->newEqClass( n ); - d_sym_break->queueFact( n ); + d_sym_break->newEqClass( n ); } } } diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index a4c34faec..b66d1cbe4 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -20,13 +20,14 @@ #include #include "util/sort_inference.h" +#include "theory/uf/options.h" +//#include "theory/rewriter.h" using namespace CVC4; using namespace std; namespace CVC4 { - void SortInference::UnionFind::print(const char * c){ for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){ Trace(c) << "s_" << it->first << " = s_" << it->second << ", "; @@ -74,6 +75,13 @@ bool SortInference::UnionFind::isValid() { } +void SortInference::recordSubsort( int s ){ + s = d_type_union_find.getRepresentative( s ); + if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){ + d_sub_sorts.push_back( s ); + } +} + void SortInference::printSort( const char* c, int t ){ int rt = d_type_union_find.getRepresentative( t ); if( d_type_types.find( rt )!=d_type_types.end() ){ @@ -90,30 +98,49 @@ void SortInference::simplify( std::vector< Node >& assertions, bool doRewrite ){ std::map< Node, Node > var_bound; process( assertions[i], var_bound ); } - //print debug - if( Trace.isOn("sort-inference") ){ - for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ - Trace("sort-inference") << it->first << " : "; - if( !d_op_arg_types[ it->first ].empty() ){ - Trace("sort-inference") << "( "; - for( size_t i=0; ifirst ].size(); i++ ){ - printSort( "sort-inference", d_op_arg_types[ it->first ][i] ); - Trace("sort-inference") << " "; - } - Trace("sort-inference") << ") -> "; + for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ + Trace("sort-inference") << it->first << " : "; + if( !d_op_arg_types[ it->first ].empty() ){ + Trace("sort-inference") << "( "; + for( size_t i=0; ifirst ].size(); i++ ){ + recordSubsort( d_op_arg_types[ it->first ][i] ); + printSort( "sort-inference", d_op_arg_types[ it->first ][i] ); + Trace("sort-inference") << " "; } - printSort( "sort-inference", it->second ); - Trace("sort-inference") << std::endl; + Trace("sort-inference") << ") -> "; } - for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){ - Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl; - for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - printSort( "sort-inference", it2->second ); - Trace("sort-inference") << std::endl; - } + recordSubsort( it->second ); + printSort( "sort-inference", it->second ); + Trace("sort-inference") << std::endl; + } + for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){ + Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl; + for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + printSort( "sort-inference", it2->second ); Trace("sort-inference") << std::endl; } + Trace("sort-inference") << std::endl; + } + + //determine monotonicity of sorts + for( unsigned i=0; i var_bound; + processMonotonic( assertions[i], true, true, var_bound ); + } + + Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl; + for( unsigned i=0; i& assertions, bool doRewrite ){ } //add lemma enforcing introduced constants to be distinct? } + }else if( !options::ufssSymBreak() ){ + std::map< int, Node > constants; + //just add a bunch of unit lemmas + for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ + int rt = d_type_union_find.getRepresentative( it->second ); + if( d_op_arg_types[ it->first ].empty() && constants.find( rt )==constants.end() ){ + constants[ rt ] = it->first; + } + } + //add unit lemmas for each constant + Node first_const; + for( std::map< int, Node >::iterator it = constants.begin(); it != constants.end(); ++it ){ + if( first_const.isNull() ){ + first_const = it->second; + }else{ + Node eq = first_const.eqNode( it->second ); + //eq = Rewriter::rewrite( eq ); + Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl; + assertions.push_back( eq ); + } + } + + } initialSortCount = sortCount; } @@ -265,11 +315,11 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ //d_type_eq_class[sortCount].push_back( n ); } retType = d_op_return_types[n]; - }else if( n.isConst() ){ - Trace("sort-inference-debug") << n << " is a constant." << std::endl; + //}else if( n.isConst() ){ + // Trace("sort-inference-debug") << n << " is a constant." << std::endl; //can be any type we want - retType = sortCount; - sortCount++; + // retType = sortCount; + // sortCount++; }else{ Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl; //it is an interpretted term @@ -289,6 +339,40 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ return retType; } +void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) { + if( n.getKind()==kind::FORALL ){ + for( unsigned i=0; i > d_type_eq_class; + //all subsorts + std::vector< int > d_sub_sorts; + std::map< int, bool > d_non_monotonic_sorts; + void recordSubsort( int s ); public: class UnionFind { public: @@ -66,6 +68,12 @@ private: void printSort( const char* c, int t ); //process int process( Node n, std::map< Node, Node >& var_bound ); + +//for monotonicity inference +private: + void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ); + +//for rewriting private: //mapping from old symbols to new symbols std::map< Node, Node > d_symbol_map; @@ -79,6 +87,7 @@ private: Node getNewSymbol( Node old, TypeNode tn ); //simplify Node simplify( Node n, std::map< Node, Node >& var_bound ); + public: SortInference() : sortCount( 1 ){} ~SortInference(){} -- 2.30.2