From 09a2f1a01f5cf807112bc31d5f79f5f73e026b03 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Nov 2013 16:40:23 -0600 Subject: [PATCH] Add fair strategy for finite model finding multiple sorts --uf-ss-fair. --- src/printer/cvc/cvc_printer.cpp | 1 + src/theory/model.cpp | 4 + src/theory/uf/kinds | 3 + src/theory/uf/options | 2 + src/theory/uf/theory_uf.cpp | 4 +- src/theory/uf/theory_uf_strong_solver.cpp | 117 ++++++++++++++++++++-- src/theory/uf/theory_uf_strong_solver.h | 29 ++++-- src/theory/uf/theory_uf_type_rules.h | 14 +++ 8 files changed, 155 insertions(+), 19 deletions(-) diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e0375e6e1..7667acdd0 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -270,6 +270,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo toStream(op, n.getOperator(), depth, types, false); break; case kind::CARDINALITY_CONSTRAINT: + case kind::COMBINED_CARDINALITY_CONSTRAINT: out << "CARDINALITY_CONSTRAINT"; break; diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 393f3883c..b6ef924d7 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -162,6 +162,10 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const if(val.getKind() == kind::CARDINALITY_CONSTRAINT) { val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst().getNumerator()); } + if(val.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){ + //FIXME + val = NodeManager::currentNM()->mkConst(false); + } return val; } diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index fa24df717..e99c3366c 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -18,4 +18,7 @@ typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule operator CARDINALITY_CONSTRAINT 2 "cardinality constraint" typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule +operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint" +typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule + endtheory diff --git a/src/theory/uf/options b/src/theory/uf/options index b9f60b83d..cfa6e6c04 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -42,5 +42,7 @@ option ufssCliqueSplits --uf-ss-clique-splits bool :default false option ufssSymBreak --uf-ss-sym-break bool :default false finite model finding symmetry breaking techniques +option ufssFairness --uf-ss-fair bool :default false + use fair strategy for finite model finding multiple sorts endmodule diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 41935984f..0ee7a2bdd 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -72,7 +72,6 @@ static Node mkAnd(const std::vector& conjunctions) { }/* mkAnd() */ void TheoryUF::check(Effort level) { - while (!done() && !d_conflict) { // Get all the assertions @@ -94,7 +93,7 @@ void TheoryUF::check(Effort level) { TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); - } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT) { + } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { // do nothing } else { d_equalityEngine.assertPredicate(atom, polarity, fact); @@ -136,6 +135,7 @@ void TheoryUF::preRegisterTerm(TNode node) { d_functionsTerms.push_back(node); break; case kind::CARDINALITY_CONSTRAINT: + case kind::COMBINED_CARDINALITY_CONSTRAINT: //do nothing break; default: diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 4ef11c042..5f63fa8df 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -416,7 +416,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ), d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ), d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ), - d_cardinality_assertions( c ), d_hasCard( c, false ){ + d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ){ d_cardinality_term = n; } @@ -894,6 +894,10 @@ void StrongSolverTheoryUF::SortModel::assertCardinality( OutputChannel* out, int allocateCardinality( out ); } } + if( c>d_maxNegCard.get() ){ + Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for " << d_type << " is now " << c << std::endl; + d_maxNegCard.set( c ); + } } } } @@ -1449,13 +1453,12 @@ void StrongSolverTheoryUF::SortModel::getRepresentatives( std::vector< Node >& r } } +Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) { + return d_cardinality_literal.find( c )!=d_cardinality_literal.end() ? d_cardinality_literal[c] : Node::null(); +} + StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : -d_out( &out ), -d_th( th ), -d_conflict( c, false ), -d_rep_model(), -d_conf_types(), -d_rep_model_init( c ) +d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ) { if( options::ufssColoringSat() ){ d_term_amb = new TermDisambiguator( th->getQuantifiersEngine(), c ); @@ -1539,6 +1542,25 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ Assert( d_rep_model[tn] ); long nCard = lit[1].getConst().getNumerator().getLong(); d_rep_model[tn]->assertCardinality( d_out, nCard, polarity ); + + //check if combined cardinality is violated + checkCombinedCardinality(); + }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ + d_com_card_assertions[lit] = polarity; + if( polarity ){ + checkCombinedCardinality(); + }else{ + bool needsCard = true; + for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){ + if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() || d_com_card_assertions[it->second] ){ + needsCard = false; + break; + } + } + if( needsCard ){ + allocateCombinedCardinality(); + } + } }else{ if( Trace.isOn("uf-ss-warn") ){ ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but @@ -1625,6 +1647,18 @@ void StrongSolverTheoryUF::propagate( Theory::Effort level ){ /** get next decision request */ Node StrongSolverTheoryUF::getNextDecisionRequest(){ + //request the combined cardinality as a decision literal, if not already asserted + int comCard = 0; + Node com_lit; + do { + com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null(); + if( d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){ + Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl; + return com_lit; + } + comCard++; + }while( !com_lit.isNull() ); + //otherwise, check each individual sort for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ Node n = it->second->getNextDecisionRequest(); if( !n.isNull() ){ @@ -1635,6 +1669,9 @@ Node StrongSolverTheoryUF::getNextDecisionRequest(){ } void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ + //initialize combined cardinality + initializeCombinedCardinality(); + Trace("uf-ss-register") << "Preregister " << n << "." << std::endl; //shouldn't have to preregister this type (it may be that there are no quantifiers over tn) TypeNode tn = n.getType(); @@ -1661,7 +1698,7 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ if( rm ){ rm->initialize( d_out ); d_rep_model[tn] = rm; - d_rep_model_init[tn] = true; + //d_rep_model_init[tn] = true; } }else{ Trace("uf-ss-register") << "Already preregistered sort " << tn << "." << std::endl; @@ -1769,6 +1806,70 @@ void StrongSolverTheoryUF::debugModel( TheoryModel* m ){ } } +/** initialize */ +void StrongSolverTheoryUF::initializeCombinedCardinality() { + if( options::ufssFairness() ){ + Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl; + if( d_aloc_com_card.get()==0 ){ + allocateCombinedCardinality(); + } + } +} + +/** check */ +void StrongSolverTheoryUF::checkCombinedCardinality() { + if( options::ufssFairness() ){ + int totalCombinedCard = 0; + for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + totalCombinedCard += it->second->getMaximumNegativeCardinality(); + } + Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl; + for( int i=0; i conf; + conf.push_back( com_lit ); + int totalAdded = 0; + for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + int c = it->second->getMaximumNegativeCardinality(); + if( c>0 ){ + conf.push_back( it->second->getCardinalityLiteral( c ).negate() ); + totalAdded += c; + } + if( totalAdded>i ){ + break; + } + } + Node cc = NodeManager::currentNM()->mkNode( AND, conf ); + Trace("uf-ss-lemma") << "Combined cardinality conflict : " << cc << std::endl; + Trace("uf-ss-com-card") << "Combined cardinality conflict : " << cc << std::endl; + getOutputChannel().conflict( cc ); + d_conflict.set( true ); + } + } + } + } +} + +void StrongSolverTheoryUF::allocateCombinedCardinality() { + Trace("uf-ss-com-card") << "Allocate combined cardinality (" << d_aloc_com_card.get() << ")" << std::endl; + //make node + Node lem = NodeManager::currentNM()->mkNode( COMBINED_CARDINALITY_CONSTRAINT, + NodeManager::currentNM()->mkConst( Rational( d_aloc_com_card.get() ) ) ); + Trace("uf-ss-com-card") << "Split on " << lem << std::endl; + lem = Rewriter::rewrite(lem); + d_com_card_literal[ d_aloc_com_card.get() ] = lem; + lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); + //add as lemma to output channel + getOutputChannel().lemma( lem ); + //require phase + getOutputChannel().requirePhase( d_com_card_literal[ d_aloc_com_card.get() ], true ); + //increment cardinality + d_aloc_com_card.set( d_aloc_com_card.get() + 1 ); +} + StrongSolverTheoryUF::Statistics::Statistics(): d_clique_conflicts("StrongSolverTheoryUF::Clique_Conflicts", 0), d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0), diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 079a03c36..4f41ebf2e 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -245,6 +245,8 @@ public: context::CDO< bool > d_hasCard; /** clique lemmas that have been asserted */ std::map< int, std::vector< std::vector< Node > > > d_cliques; + /** maximum negatively asserted cardinality */ + context::CDO< int > d_maxNegCard; private: /** apply totality */ bool applyTotality( int cardinality ); @@ -281,6 +283,10 @@ public: void getRepresentatives( std::vector< Node >& reps ); /** has cardinality */ bool hasCardinalityAsserted() { return d_hasCard; } + /** get cardinality literal */ + Node getCardinalityLiteral( int c ); + /** get maximum negative cardinality */ + int getMaximumNegativeCardinality() { return d_maxNegCard.get(); } //print debug void debugPrint( const char* c ); /** debug a model */ @@ -298,12 +304,21 @@ private: context::CDO d_conflict; /** rep model structure, one for each type */ std::map< TypeNode, SortModel* > d_rep_model; - /** all types */ - std::vector< TypeNode > d_conf_types; - /** whether conflict find data structures have been initialized */ - TypeNodeBoolMap d_rep_model_init; - /** get conflict find */ + /** get sort model */ SortModel* getSortModel( Node n ); +private: + /** allocated combined cardinality */ + context::CDO< int > d_aloc_com_card; + /** combined cardinality constraints */ + std::map< int, Node > d_com_card_literal; + /** combined cardinality assertions (indexed by cardinality literals ) */ + NodeBoolMap d_com_card_assertions; + /** initialize */ + void initializeCombinedCardinality(); + /** allocateCombinedCardinality */ + void allocateCombinedCardinality(); + /** check */ + void checkCombinedCardinality(); private: /** term disambiguator */ TermDisambiguator* d_term_amb; @@ -359,10 +374,6 @@ public: /** debug a model */ void debugModel( TheoryModel* m ); public: - /** get number of types */ - int getNumCardinalityTypes() { return (int)d_conf_types.size(); } - /** get type */ - TypeNode getCardinalityType( int i ) { return d_conf_types[i]; } /** get is in conflict */ bool isConflict() { return d_conflict; } /** get cardinality for node */ diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index b9a8ed12e..50a746205 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -70,6 +70,20 @@ public: } };/* class CardinalityConstraintTypeRule */ +class CombinedCardinalityConstraintTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + if( check ) { + TypeNode valType = n[0].getType(check); + if( valType != nodeManager->integerType() ) { + throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be integer"); + } + } + return nodeManager->booleanType(); + } +};/* class CardinalityConstraintTypeRule */ + }/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ -- 2.30.2