diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/cardinality_extension.cpp (renamed from src/theory/uf/theory_uf_strong_solver.cpp) | 267 | ||||
-rw-r--r-- | src/theory/uf/cardinality_extension.h (renamed from src/theory/uf/theory_uf_strong_solver.h) | 86 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 173 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 32 | ||||
-rw-r--r-- | src/theory/uf/equality_engine_types.h | 6 | ||||
-rw-r--r-- | src/theory/uf/ho_extension.cpp | 434 | ||||
-rw-r--r-- | src/theory/uf/ho_extension.h | 195 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 366 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 116 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.h | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_rewriter.h | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 6 |
13 files changed, 1028 insertions, 669 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/cardinality_extension.cpp index a21edd8eb..87696ef5f 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_uf_strong_solver.cpp +/*! \file cardinality_extension.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King @@ -9,10 +9,10 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Implementation of theory uf strong solver class + ** \brief Implementation of theory of UF with cardinality. **/ -#include "theory/uf/theory_uf_strong_solver.h" +#include "theory/uf/cardinality_extension.h" #include "options/uf_options.h" #include "theory/uf/theory_uf.h" @@ -36,7 +36,7 @@ namespace theory { namespace uf { /* These are names are unambigious are we use abbreviations. */ -typedef StrongSolverTheoryUF::SortModel SortModel; +typedef CardinalityExtension::SortModel SortModel; typedef SortModel::Region Region; typedef Region::RegionNodeInfo RegionNodeInfo; typedef RegionNodeInfo::DiseqList DiseqList; @@ -228,7 +228,8 @@ struct sortExternalDegree { int gmcCount = 0; bool Region::getMustCombine( int cardinality ){ - if( options::ufssRegions() && d_total_diseq_external>=unsigned(cardinality) ){ + if (d_total_diseq_external >= static_cast<unsigned>(cardinality)) + { //The number of external disequalities is greater than or equal to //cardinality. Thus, a clique of size cardinality+1 may exist //between nodes in d_regions[i] and other regions Check if this is @@ -285,8 +286,9 @@ bool Region::check( Theory::Effort level, int cardinality, }else{ return false; } - }else if( options::ufssRegions() || options::ufssEagerSplits() || - level==Theory::EFFORT_FULL ) { + } + else if (level==Theory::EFFORT_FULL) + { //build test clique, up to size cardinality+1 if( d_testCliqueSize<=unsigned(cardinality) ){ std::vector< Node > newClique; @@ -460,7 +462,7 @@ std::string SortModel::CardinalityDecisionStrategy::identify() const SortModel::SortModel(Node n, context::Context* c, context::UserContext* u, - StrongSolverTheoryUF* thss) + CardinalityExtension* thss) : d_type(n.getType()), d_thss(thss), d_regions_index(c, 0), @@ -502,6 +504,8 @@ void SortModel::initialize( OutputChannel* out ){ if (d_c_dec_strat.get() != nullptr && !d_initialized) { d_initialized = true; + // Strategy is user-context-dependent, since it is in sync with + // user-context-dependent flag d_initialized. d_thss->getTheory()->getDecisionManager()->registerStrategy( DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get()); } @@ -528,21 +532,15 @@ void SortModel::newEqClass( Node n ){ d_regions_map[n] = -1; } }else{ - if( !options::ufssRegions() ){ - // If not using regions, always add new equivalence classes - // to region index = 0. - d_regions_index = 0; - } d_regions_map[n] = d_regions_index; - Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n + Debug("uf-ss") << "CardinalityExtension: New Eq Class " << n << std::endl; Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl; if( d_regions_index<d_regions.size() ){ d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true); d_regions[ d_regions_index ]->setValid(true); - Assert( !options::ufssRegions() || - d_regions[ d_regions_index ]->getNumReps()==0 ); + Assert(d_regions[d_regions_index]->getNumReps()==0); }else{ d_regions.push_back( new Region( this, d_thss->getSatContext() ) ); } @@ -563,10 +561,8 @@ void SortModel::merge( Node a, Node b ){ } d_regions_map[b] = -1; }else{ - //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) ); - //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) ); - Debug("uf-ss") << "StrongSolverTheoryUF: Merging " - << a << " = " << b << "..." << std::endl; + Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b + << "..." << std::endl; if( a!=b ){ Assert( d_regions_map.find( a )!=d_regions_map.end() ); Assert( d_regions_map.find( b )!=d_regions_map.end() ); @@ -620,8 +616,9 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ //do nothing }else{ //if they are not already disequal - a = d_thss->getTheory()->d_equalityEngine.getRepresentative( a ); - b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b ); + eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine(); + a = ee->getRepresentative(a); + b = ee->getRepresentative(b); int ai = d_regions_map[a]; int bi = d_regions_map[b]; if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){ @@ -660,8 +657,8 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ } bool SortModel::areDisequal( Node a, Node b ) { - Assert( a == d_thss->getTheory()->d_equalityEngine.getRepresentative( a ) ); - Assert( b == d_thss->getTheory()->d_equalityEngine.getRepresentative( b ) ); + Assert(a == d_thss->getTheory()->getEqualityEngine()->getRepresentative(a)); + Assert(b == d_thss->getTheory()->getEqualityEngine()->getRepresentative(b)); if( d_regions_map.find( a )!=d_regions_map.end() && d_regions_map.find( b )!=d_regions_map.end() ){ int ai = d_regions_map[a]; @@ -676,14 +673,14 @@ bool SortModel::areDisequal( Node a, Node b ) { void SortModel::check( Theory::Effort level, OutputChannel* out ){ Assert( options::ufssMode()==UF_SS_FULL ); if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){ - Debug("uf-ss") << "StrongSolverTheoryUF: Check " << level << " " << d_type << std::endl; + Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type + << std::endl; if( level==Theory::EFFORT_FULL ){ Debug("fmf-full-check") << std::endl; Debug("fmf-full-check") << "Full check for SortModel " << d_type << ", status : " << std::endl; debugPrint("fmf-full-check"); Debug("fmf-full-check") << std::endl; } - //Notice() << "StrongSolverTheoryUF: Check " << level << std::endl; if( d_reps<=(unsigned)d_cardinality ){ Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl; if( level==Theory::EFFORT_FULL ){ @@ -713,7 +710,8 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ if( !applyTotality( d_cardinality ) ){ //do splitting on demand bool addedLemma = false; - if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){ + if (level==Theory::EFFORT_FULL) + { Trace("uf-ss-debug") << "Add splits?" << std::endl; //see if we have any recommended splits from large regions for( int i=0; i<(int)d_regions_index; i++ ){ @@ -835,8 +833,9 @@ void SortModel::setSplitScore( Node n, int s ){ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ if( !d_conflict ){ Trace("uf-ss-assert") - << "Assert cardinality "<< d_type << " " << c << " " << val << " level = " - << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl; + << "Assert cardinality " << d_type << " " << c << " " << val + << " level = " + << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl; Assert( c>0 ); Node cl = getCardinalityLiteral( c ); if( val ){ @@ -1205,22 +1204,6 @@ bool SortModel::debugModel( TheoryModel* m ){ Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard << std::endl; Trace("uf-ss-warn") << " # Reps : " << nReps << std::endl; if( d_maxNegCard>=nReps ){ - /* - for( unsigned i=0; i<d_fresh_aloc_reps.size(); i++ ){ - if( add>0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){ - rs->d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] ); - add--; - } - } - for( int i=0; i<add; i++ ){ - std::stringstream ss; - ss << "r_" << d_type << "_"; - Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, - "enumeration to meet negative card constraint" ); - d_fresh_aloc_reps.push_back( nn ); - rs->d_type_reps[d_type].push_back( nn ); - } - */ while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){ std::stringstream ss; ss << "r_" << d_type << "_"; @@ -1316,7 +1299,7 @@ Node SortModel::getCardinalityLiteral(unsigned c) return lit; } -StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, +CardinalityExtension::CardinalityExtension(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) @@ -1341,38 +1324,46 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, } } -StrongSolverTheoryUF::~StrongSolverTheoryUF() { +CardinalityExtension::~CardinalityExtension() +{ for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it) { delete it->second; } } -SortInference* StrongSolverTheoryUF::getSortInference() { +SortInference* CardinalityExtension::getSortInference() +{ return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference(); } /** get default sat context */ -context::Context* StrongSolverTheoryUF::getSatContext() { +context::Context* CardinalityExtension::getSatContext() +{ return d_th->getSatContext(); } /** get default output channel */ -OutputChannel& StrongSolverTheoryUF::getOutputChannel() { +OutputChannel& CardinalityExtension::getOutputChannel() +{ return d_th->getOutputChannel(); } /** ensure eqc */ -void StrongSolverTheoryUF::ensureEqc( SortModel* c, Node a ) { +void CardinalityExtension::ensureEqc(SortModel* c, Node a) +{ if( !hasEqc( a ) ){ d_rel_eqc[a] = true; - Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : " + << a.getType() << std::endl; c->newEqClass( a ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class." + << std::endl; } } -void StrongSolverTheoryUF::ensureEqcRec( Node n ) { +void CardinalityExtension::ensureEqcRec(Node n) +{ if( !hasEqc( n ) ){ SortModel* c = getSortModel( n ); if( c ){ @@ -1385,66 +1376,75 @@ void StrongSolverTheoryUF::ensureEqcRec( Node n ) { } /** has eqc */ -bool StrongSolverTheoryUF::hasEqc( Node a ) { +bool CardinalityExtension::hasEqc(Node a) +{ NodeBoolMap::iterator it = d_rel_eqc.find( a ); return it!=d_rel_eqc.end() && (*it).second; } /** new node */ -void StrongSolverTheoryUF::newEqClass( Node a ){ +void CardinalityExtension::newEqClass(Node a) +{ SortModel* c = getSortModel( a ); if( c ){ #ifdef LAZY_REL_EQC //do nothing #else - Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : " + << a.getType() << std::endl; c->newEqClass( a ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class." + << std::endl; #endif } } /** merge */ -void StrongSolverTheoryUF::merge( Node a, Node b ){ +void CardinalityExtension::merge(Node a, Node b) +{ //TODO: ensure they are relevant SortModel* c = getSortModel( a ); if( c ){ #ifdef LAZY_REL_EQC ensureEqc( c, a ); if( hasEqc( b ) ){ - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b + << " : " << a.getType() << std::endl; c->merge( a, b ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl; }else{ //c->assignEqClass( b, a ); d_rel_eqc[b] = true; } #else - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b + << " : " << a.getType() << std::endl; c->merge( a, b ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl; #endif } } /** assert terms are disequal */ -void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){ +void CardinalityExtension::assertDisequal(Node a, Node b, Node reason) +{ SortModel* c = getSortModel( a ); if( c ){ #ifdef LAZY_REL_EQC ensureEqc( c, a ); ensureEqc( c, b ); #endif - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl; - //Assert( d_th->d_equalityEngine.getRepresentative( a )==a ); - //Assert( d_th->d_equalityEngine.getRepresentative( b )==b ); + Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a + << " " << b << " : " << a.getType() << std::endl; c->assertDisequal( a, b, reason ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Assert disequal." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal." + << std::endl; } } /** assert a node */ -void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ +void CardinalityExtension::assertNode(Node n, bool isDecision) +{ Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl; #ifdef LAZY_REL_EQC ensureEqcRec( n ); @@ -1542,32 +1542,49 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl; } -bool StrongSolverTheoryUF::areDisequal( Node a, Node b ) { +bool CardinalityExtension::areDisequal(Node a, Node b) +{ if( a==b ){ return false; - }else{ - a = d_th->d_equalityEngine.getRepresentative( a ); - b = d_th->d_equalityEngine.getRepresentative( b ); - if( d_th->d_equalityEngine.areDisequal( a, b, false ) ){ - return true; - }else{ - SortModel* c = getSortModel( a ); - if( c ){ - return c->areDisequal( a, b ); - }else{ - return false; - } - } } + eq::EqualityEngine* ee = d_th->getEqualityEngine(); + a = ee->getRepresentative(a); + b = ee->getRepresentative(b); + if (ee->areDisequal(a, b, false)) + { + return true; + } + SortModel* c = getSortModel(a); + if (c) + { + return c->areDisequal(a, b); + } + return false; } /** check */ -void StrongSolverTheoryUF::check( Theory::Effort level ){ +void CardinalityExtension::check(Theory::Effort level) +{ if( !d_conflict ){ if( options::ufssMode()==UF_SS_FULL ){ - Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl; - if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){ - debugPrint( "uf-ss-debug" ); + Trace("uf-ss-solver") + << "CardinalityExtension: check " << level << std::endl; + if (level == Theory::EFFORT_FULL) + { + if (Debug.isOn("uf-ss-debug")) + { + debugPrint("uf-ss-debug"); + } + if (Trace.isOn("uf-ss-state")) + { + Trace("uf-ss-state") + << "CardinalityExtension::check " << level << std::endl; + for (std::pair<const TypeNode, SortModel*>& rm : d_rep_model) + { + Trace("uf-ss-state") << " " << rm.first << " has cardinality " + << rm.second->getCardinality() << std::endl; + } + } } for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ it->second->check( level, d_out ); @@ -1612,11 +1629,13 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ // unhandled uf ss mode Assert( false ); } - Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl; + Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level + << std::endl; } } -void StrongSolverTheoryUF::presolve() { +void CardinalityExtension::presolve() +{ d_initializedCombinedCardinality = false; for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ it->second->presolve(); @@ -1624,13 +1643,13 @@ void StrongSolverTheoryUF::presolve() { } } -StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy:: +CardinalityExtension::CombinedCardinalityDecisionStrategy:: CombinedCardinalityDecisionStrategy(context::Context* satContext, Valuation valuation) : DecisionStrategyFmf(satContext, valuation) { } -Node StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::mkLiteral( +Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral( unsigned i) { NodeManager* nm = NodeManager::currentNM(); @@ -1638,12 +1657,13 @@ Node StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::mkLiteral( } std::string -StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::identify() const +CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const { return std::string("uf_combined_card"); } -void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ +void CardinalityExtension::preRegisterTerm(TNode n) +{ if( options::ufssMode()==UF_SS_FULL ){ //initialize combined cardinality initializeCombinedCardinality(); @@ -1685,17 +1705,8 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ } } -//void StrongSolverTheoryUF::registerQuantifier( Node f ){ -// Debug("uf-ss-register") << "Register quantifier " << f << std::endl; - //must ensure the quantifier does not quantify over arithmetic - //for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - // TypeNode tn = f[0][i].getType(); - // preRegisterType( tn, true ); - //} -//} - - -SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ +SortModel* CardinalityExtension::getSortModel(Node n) +{ TypeNode tn = n.getType(); std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn ); //pre-register the type if not done already @@ -1711,7 +1722,8 @@ SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ } /** get cardinality for sort */ -int StrongSolverTheoryUF::getCardinality( Node n ) { +int CardinalityExtension::getCardinality(Node n) +{ SortModel* c = getSortModel( n ); if( c ){ return c->getCardinality(); @@ -1720,7 +1732,8 @@ int StrongSolverTheoryUF::getCardinality( Node n ) { } } -int StrongSolverTheoryUF::getCardinality( TypeNode tn ) { +int CardinalityExtension::getCardinality(TypeNode tn) +{ std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn ); if( it!=d_rep_model.end() && it->second ){ return it->second->getCardinality(); @@ -1729,20 +1742,8 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) { } //print debug -void StrongSolverTheoryUF::debugPrint( const char* c ){ - //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine ); - //while( !eqc_iter.isFinished() ){ - // Debug( c ) << "Eq class [[" << (*eqc_iter) << "]]" << std::endl; - // EqClassIterator< TheoryUF::NotifyClass > eqc_iter2( *eqc_iter, &((TheoryUF*)d_th)->d_equalityEngine ); - // Debug( c ) << " "; - // while( !eqc_iter2.isFinished() ){ - // Debug( c ) << "[" << (*eqc_iter2) << "] "; - // eqc_iter2++; - // } - // Debug( c ) << std::endl; - // eqc_iter++; - //} - +void CardinalityExtension::debugPrint(const char* c) +{ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl; it->second->debugPrint( c ); @@ -1750,7 +1751,8 @@ void StrongSolverTheoryUF::debugPrint( const char* c ){ } } -bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){ +bool CardinalityExtension::debugModel(TheoryModel* m) +{ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ if( !it->second->debugModel( m ) ){ return false; @@ -1760,7 +1762,8 @@ bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){ } /** initialize */ -void StrongSolverTheoryUF::initializeCombinedCardinality() { +void CardinalityExtension::initializeCombinedCardinality() +{ if (d_cc_dec_strat.get() != nullptr && !d_initializedCombinedCardinality.get()) { @@ -1771,7 +1774,8 @@ void StrongSolverTheoryUF::initializeCombinedCardinality() { } /** check */ -void StrongSolverTheoryUF::checkCombinedCardinality() { +void CardinalityExtension::checkCombinedCardinality() +{ Assert( options::ufssMode()==UF_SS_FULL ); if( options::ufssFairness() ){ Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl; @@ -1851,13 +1855,13 @@ void StrongSolverTheoryUF::checkCombinedCardinality() { } } -StrongSolverTheoryUF::Statistics::Statistics(): - d_clique_conflicts("StrongSolverTheoryUF::Clique_Conflicts", 0), - d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0), - d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0), - d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0), - d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0), - d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1) +CardinalityExtension::Statistics::Statistics() + : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0), + d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0), + d_split_lemmas("CardinalityExtension::Split_Lemmas", 0), + d_disamb_term_lemmas("CardinalityExtension::Disambiguate_Term_Lemmas", 0), + d_totality_lemmas("CardinalityExtension::Totality_Lemmas", 0), + d_max_model_size("CardinalityExtension::Max_Model_Size", 1) { smtStatisticsRegistry()->registerStat(&d_clique_conflicts); smtStatisticsRegistry()->registerStat(&d_clique_lemmas); @@ -1867,7 +1871,8 @@ StrongSolverTheoryUF::Statistics::Statistics(): smtStatisticsRegistry()->registerStat(&d_max_model_size); } -StrongSolverTheoryUF::Statistics::~Statistics(){ +CardinalityExtension::Statistics::~Statistics() +{ smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts); smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/cardinality_extension.h index 41577f217..3e3d90be5 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/cardinality_extension.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_uf_strong_solver.h +/*! \file cardinality_extension.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King @@ -9,59 +9,62 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Theory uf strong solver + ** \brief Theory of UF with cardinality. **/ #include "cvc4_private.h" -#ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H -#define __CVC4__THEORY_UF_STRONG_SOLVER_H +#ifndef CVC4__THEORY_UF_STRONG_SOLVER_H +#define CVC4__THEORY_UF_STRONG_SOLVER_H #include "context/cdhashmap.h" #include "context/context.h" -#include "context/context_mm.h" #include "theory/theory.h" #include "util/statistics_registry.h" #include "theory/decision_manager.h" namespace CVC4 { + class SortInference; -namespace theory { -namespace uf { -class TheoryUF; -} /* namespace CVC4::theory::uf */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ -namespace CVC4 { namespace theory { namespace uf { -class StrongSolverTheoryUF{ -protected: +class TheoryUF; + +/** + * This module implements a theory solver for UF with cardinality constraints. + * For high level details, see Reynolds et al "Finite Model Finding in SMT", + * CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability + * Modulo Theories". + */ +class CardinalityExtension +{ + protected: typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; - typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; - typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap; -public: + + public: /** * Information for incremental conflict/clique finding for a * particular sort. */ - class SortModel { - private: + class SortModel + { + private: std::map< Node, std::vector< int > > d_totality_lems; std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms; std::map< Node, int > d_sym_break_index; - public: + public: /** * A partition of the current equality graph for which cliques * can occur internally. */ - class Region { - public: + class Region + { + public: /** information stored about each node in region */ class RegionNodeInfo { public: @@ -95,7 +98,7 @@ public: context::CDO< int > d_size; NodeBoolMap d_disequalities; }; /* class DiseqList */ - public: + public: /** constructor */ RegionNodeInfo( context::Context* c ) : d_internal(c), d_external(c), d_valid(c, true) { @@ -119,7 +122,7 @@ public: DiseqList* get(unsigned i) { return d_disequalities[i]; } - private: + private: DiseqList d_internal; DiseqList d_external; context::CDO< bool > d_valid; @@ -149,7 +152,7 @@ public: //whether region is valid context::CDO< bool > d_valid; - public: + public: //constructor Region( SortModel* cf, context::Context* c ); virtual ~Region(); @@ -209,11 +212,11 @@ public: Node frontKey() const { return d_nodes.begin()->first; } }; /* class Region */ - private: + private: /** the type this model is for */ TypeNode d_type; - /** strong solver pointer */ - StrongSolverTheoryUF* d_thss; + /** Pointer to the cardinality extension that owns this. */ + CardinalityExtension* d_thss; /** regions used to d_region_index */ context::CDO< unsigned > d_regions_index; /** vector of regions */ @@ -292,9 +295,11 @@ public: bool doSendLemma( Node lem ); - public: - SortModel( Node n, context::Context* c, context::UserContext* u, - StrongSolverTheoryUF* thss ); + public: + SortModel(Node n, + context::Context* c, + context::UserContext* u, + CardinalityExtension* thss); virtual ~SortModel(); /** initialize */ void initialize( OutputChannel* out ); @@ -359,10 +364,12 @@ public: std::unique_ptr<CardinalityDecisionStrategy> d_c_dec_strat; }; /** class SortModel */ -public: - StrongSolverTheoryUF(context::Context* c, context::UserContext* u, - OutputChannel& out, TheoryUF* th); - ~StrongSolverTheoryUF(); + public: + CardinalityExtension(context::Context* c, + context::UserContext* u, + OutputChannel& out, + TheoryUF* th); + ~CardinalityExtension(); /** get theory */ TheoryUF* getTheory() { return d_th; } /** get sort inference module */ @@ -388,7 +395,7 @@ public: /** preregister a term */ void preRegisterTerm( TNode n ); /** identify */ - std::string identify() const { return std::string("StrongSolverTheoryUF"); } + std::string identify() const { return std::string("CardinalityExtension"); } //print debug void debugPrint( const char* c ); /** debug a model */ @@ -428,7 +435,7 @@ public: /** ensure eqc for all subterms of n */ void ensureEqcRec(Node n); - /** The output channel for the strong solver. */ + /** The output channel used by this class. */ OutputChannel* d_out; /** theory uf pointer */ TheoryUF* d_th; @@ -469,11 +476,10 @@ public: context::CDO<int> d_min_pos_tn_master_card; /** relevant eqc */ NodeBoolMap d_rel_eqc; -}; /* class StrongSolverTheoryUF */ - +}; /* class CardinalityExtension */ }/* CVC4::theory namespace::uf */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY_UF_STRONG_SOLVER_H */ +#endif /* CVC4__THEORY_UF_STRONG_SOLVER_H */ diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index d1fc8341c..32d32b479 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -242,7 +242,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { Debug("equality") << d_name << "::eq::newNode(" << node << ") => " << newId << std::endl; - // notify e.g. the UF theory strong solver + // notify e.g. the theory that owns this equality engine. if (d_performNotify) { d_notify.eqNotifyNewClass(node); } @@ -929,9 +929,9 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const { void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof* eqp) const { - Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 - << ", " << (polarity ? "true" : "false") << ")" - << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; + Debug("pf::ee") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 + << ", " << (polarity ? "true" : "false") << ")" + << ", proof = " << (eqp ? "ON" : "OFF") << std::endl; // The terms must be there already Assert(hasTerm(t1) && hasTerm(t2));; @@ -940,9 +940,10 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, EqualityNodeId t1Id = getNodeId(t1); EqualityNodeId t2Id = getNodeId(t2); + std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*> cache; if (polarity) { // Get the explanation - getExplanation(t1Id, t2Id, equalities, eqp); + getExplanation(t1Id, t2Id, equalities, cache, eqp); } else { if (eqp) { eqp->d_id = eq::MERGED_THROUGH_TRANS; @@ -964,12 +965,15 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, eqpc = std::make_shared<EqProof>(); } - getExplanation(toExplain.first, toExplain.second, equalities, eqpc.get()); + getExplanation( + toExplain.first, toExplain.second, equalities, cache, eqpc.get()); if (eqpc) { - Debug("pf::ee") << "Child proof is:" << std::endl; - eqpc->debug_print("pf::ee", 1); - + if (Debug.isOn("pf::ee")) + { + Debug("pf::ee") << "Child proof is:" << std::endl; + eqpc->debug_print("pf::ee", 1); + } if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { std::vector<std::shared_ptr<EqProof>> orderedChildren; bool nullCongruenceFound = false; @@ -987,8 +991,13 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, if (nullCongruenceFound) { eqpc->d_children = orderedChildren; - Debug("pf::ee") << "Child proof's children have been reordered. It is now:" << std::endl; - eqpc->debug_print("pf::ee", 1); + if (Debug.isOn("pf::ee")) + { + Debug("pf::ee") + << "Child proof's children have been reordered. It is now:" + << std::endl; + eqpc->debug_print("pf::ee", 1); + } } } @@ -1011,8 +1020,11 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, *eqp = *temp; } - Debug("pf::ee") << "Disequality explanation final proof: " << std::endl; - eqp->debug_print("pf::ee", 1); + if (Debug.isOn("pf::ee")) + { + Debug("pf::ee") << "Disequality explanation final proof: " << std::endl; + eqp->debug_print("pf::ee", 1); + } } } } @@ -1024,15 +1036,65 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity, << std::endl; // Must have the term Assert(hasTerm(p)); + std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*> cache; // Get the explanation - getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, - eqp); + getExplanation( + getNodeId(p), polarity ? d_trueId : d_falseId, assertions, cache, eqp); } -void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, - std::vector<TNode>& equalities, - EqProof* eqp) const { - Debug("equality") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl; +void EqualityEngine::getExplanation( + EqualityNodeId t1Id, + EqualityNodeId t2Id, + std::vector<TNode>& equalities, + std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>& cache, + EqProof* eqp) const +{ + Trace("eq-exp") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," + << d_nodes[t2Id] << ") size = " << cache.size() << std::endl; + + // determine if we have already computed the explanation. + std::pair<EqualityNodeId, EqualityNodeId> cacheKey; + std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>::iterator it; + if (!eqp) + { + // If proofs are disabled, we order the ids, since explaining t1 = t2 is the + // same as explaining t2 = t1. + cacheKey = std::minmax(t1Id, t2Id); + it = cache.find(cacheKey); + if (it != cache.end()) + { + return; + } + } + else + { + // If proofs are enabled, note that proofs are sensitive to the order of t1 + // and t2, so we don't sort the ids in this case. TODO: Depending on how + // issue #2965 is resolved, we may be able to revisit this, if it is the + // case that proof/uf_proof.h,cpp is robust to equality ordering. + cacheKey = std::pair<EqualityNodeId, EqualityNodeId>(t1Id, t2Id); + it = cache.find(cacheKey); + if (it != cache.end()) + { + if (it->second) + { + eqp->d_id = it->second->d_id; + eqp->d_children.insert(eqp->d_children.end(), + it->second->d_children.begin(), + it->second->d_children.end()); + eqp->d_node = it->second->d_node; + } + else + { + // We may have cached null in its place, create the trivial proof now. + Assert(d_nodes[t1Id] == d_nodes[t2Id]); + Assert(eqp->d_id == MERGED_THROUGH_REFLEXIVITY); + eqp->d_node = d_nodes[t1Id]; + } + return; + } + } + cache[cacheKey] = eqp; // We can only explain the nodes that got merged #ifdef CVC4_ASSERTIONS @@ -1136,11 +1198,11 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, Debug("equality") << "Explaining left hand side equalities" << std::endl; std::shared_ptr<EqProof> eqpc1 = eqpc ? std::make_shared<EqProof>() : nullptr; - getExplanation(f1.a, f2.a, equalities, eqpc1.get()); + getExplanation(f1.a, f2.a, equalities, cache, eqpc1.get()); Debug("equality") << "Explaining right hand side equalities" << std::endl; std::shared_ptr<EqProof> eqpc2 = eqpc ? std::make_shared<EqProof>() : nullptr; - getExplanation(f1.b, f2.b, equalities, eqpc2.get()); + getExplanation(f1.b, f2.b, equalities, cache, eqpc2.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); eqpc->d_children.push_back( eqpc2 ); @@ -1185,7 +1247,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, Debug("equality") << push; std::shared_ptr<EqProof> eqpc1 = eqpc ? std::make_shared<EqProof>() : nullptr; - getExplanation(eq.a, eq.b, equalities, eqpc1.get()); + getExplanation(eq.a, eq.b, equalities, cache, eqpc1.get()); if( eqpc ){ eqpc->d_children.push_back( eqpc1 ); } @@ -1211,13 +1273,20 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, Assert(isConstant(childId)); std::shared_ptr<EqProof> eqpcc = eqpc ? std::make_shared<EqProof>() : nullptr; - getExplanation(childId, getEqualityNode(childId).getFind(), - equalities, eqpcc.get()); + getExplanation(childId, + getEqualityNode(childId).getFind(), + equalities, + cache, + eqpcc.get()); if( eqpc ) { eqpc->d_children.push_back( eqpcc ); - - Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl; - eqpc->debug_print("pf::ee", 1); + if (Debug.isOn("pf::ee")) + { + Debug("pf::ee") + << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" + << std::endl; + eqpc->debug_print("pf::ee", 1); + } } } @@ -1255,7 +1324,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, } eqpc->d_id = reasonType; } - equalities.push_back(reason); break; } @@ -1288,8 +1356,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); eqp->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); } - - eqp->debug_print("pf::ee", 1); + if (Debug.isOn("pf::ee")) + { + eqp->debug_print("pf::ee", 1); + } } // Done @@ -2236,27 +2306,48 @@ bool EqClassIterator::isFinished() const { } void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const { - for(unsigned i=0; i<tb; i++) { Debug( c ) << " "; } + std::stringstream ss; + debug_print(ss, tb, prettyPrinter); + Debug(c) << ss.str(); +} +void EqProof::debug_print(std::ostream& os, + unsigned tb, + PrettyPrinter* prettyPrinter) const +{ + for (unsigned i = 0; i < tb; i++) + { + os << " "; + } if (prettyPrinter) - Debug( c ) << prettyPrinter->printTag(d_id); + { + os << prettyPrinter->printTag(d_id); + } else - Debug( c ) << d_id; + { + os << d_id; + } - Debug( c ) << "("; + os << "("; if( !d_children.empty() || !d_node.isNull() ){ if( !d_node.isNull() ){ - Debug( c ) << std::endl; - for( unsigned i=0; i<tb+1; i++ ) { Debug( c ) << " "; } - Debug( c ) << d_node; + os << std::endl; + for (unsigned i = 0; i < tb + 1; i++) + { + os << " "; + } + os << d_node; } for( unsigned i=0; i<d_children.size(); i++ ){ - if( i>0 || !d_node.isNull() ) Debug( c ) << ","; - Debug( c ) << std::endl; - d_children[i]->debug_print( c, tb+1, prettyPrinter ); + if (i > 0 || !d_node.isNull()) + { + os << ","; + } + os << std::endl; + d_children[i]->debug_print(os, tb + 1, prettyPrinter); } } - Debug( c ) << ")" << std::endl; + os << ")" << std::endl; } } // Namespace uf diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index b93ff6d6d..73d8bd4e9 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -516,11 +516,24 @@ private: bool d_inPropagate; /** - * Get an explanation of the equality t1 = t2. Returns the asserted equalities that - * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere - * else. + * Get an explanation of the equality t1 = t2. Returns the asserted equalities + * that imply t1 = t2. Returns TNodes as the assertion equalities should be + * hashed somewhere else. + * + * This call refers to terms t1 and t2 by their ids t1Id and t2Id. + * + * If eqp is non-null, then this method populates eqp's information and + * children such that it is a proof of t1 = t2. + * + * We cache results of this call in cache, where cache[t1Id][t2Id] stores + * a proof of t1 = t2. */ - void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof* eqp) const; + void getExplanation( + EqualityEdgeId t1Id, + EqualityNodeId t2Id, + std::vector<TNode>& equalities, + std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>& cache, + EqProof* eqp) const; /** * Print the equality graph. @@ -941,8 +954,19 @@ public: unsigned d_id; Node d_node; std::vector<std::shared_ptr<EqProof>> d_children; + /** + * Debug print this proof on debug trace c with tabulation tb and pretty + * printer prettyPrinter. + */ void debug_print(const char* c, unsigned tb = 0, PrettyPrinter* prettyPrinter = nullptr) const; + /** + * Debug print this proof on output stream os with tabulation tb and pretty + * printer prettyPrinter. + */ + void debug_print(std::ostream& os, + unsigned tb = 0, + PrettyPrinter* prettyPrinter = nullptr) const; };/* class EqProof */ } // Namespace eq diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index 75216d10e..3813bb697 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H -#define __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H +#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H +#define CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H #include <string> #include <iostream> @@ -360,4 +360,4 @@ struct TriggerInfo { } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */ +#endif /* CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */ diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp new file mode 100644 index 000000000..88b2ba8d2 --- /dev/null +++ b/src/theory/uf/ho_extension.cpp @@ -0,0 +1,434 @@ +/********************* */ +/*! \file ho_extension.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Implementation of the higher-order extension of TheoryUF. + ** + **/ + +#include "theory/uf/ho_extension.h" + +#include "expr/node_algorithm.h" +#include "options/uf_options.h" +#include "theory/theory_model.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_rewriter.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace uf { + +HoExtension::HoExtension(TheoryUF& p, + context::Context* c, + context::UserContext* u) + : d_parent(p), d_extensionality(u), d_uf_std_skolem(u) +{ + d_true = NodeManager::currentNM()->mkConst(true); +} + +Node HoExtension::expandDefinition(Node node) +{ + // convert HO_APPLY to APPLY_UF if fully applied + if (node[0].getType().getNumChildren() == 2) + { + Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; + Node ret = getApplyUfForHoApply(node); + Trace("uf-ho") << "uf-ho : expandDefinition : " << node << " to " << ret + << std::endl; + return ret; + } + return node; +} + +Node HoExtension::getExtensionalityDeq(TNode deq) +{ + Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL); + Assert(deq[0][0].getType().isFunction()); + std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq); + if (it == d_extensionality_deq.end()) + { + TypeNode tn = deq[0][0].getType(); + std::vector<TypeNode> argTypes = tn.getArgTypes(); + std::vector<Node> skolems; + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) + { + Node k = + nm->mkSkolem("k", argTypes[i], "skolem created for extensionality."); + skolems.push_back(k); + } + Node t[2]; + for (unsigned i = 0; i < 2; i++) + { + std::vector<Node> children; + Node curr = deq[0][i]; + while (curr.getKind() == HO_APPLY) + { + children.push_back(curr[1]); + curr = curr[0]; + } + children.push_back(curr); + std::reverse(children.begin(), children.end()); + children.insert(children.end(), skolems.begin(), skolems.end()); + t[i] = nm->mkNode(APPLY_UF, children); + } + Node conc = t[0].eqNode(t[1]).negate(); + d_extensionality_deq[deq] = conc; + return conc; + } + return it->second; +} + +unsigned HoExtension::applyExtensionality(TNode deq) +{ + Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL); + Assert(deq[0][0].getType().isFunction()); + // apply extensionality + if (d_extensionality.find(deq) == d_extensionality.end()) + { + d_extensionality.insert(deq); + Node conc = getExtensionalityDeq(deq); + Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc); + Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem + << std::endl; + d_parent.getOutputChannel().lemma(lem); + return 1; + } + return 0; +} + +Node HoExtension::getApplyUfForHoApply(Node node) +{ + Assert(node[0].getType().getNumChildren() == 2); + std::vector<TNode> args; + Node f = TheoryUfRewriter::decomposeHoApply(node, args, true); + Node new_f = f; + NodeManager* nm = NodeManager::currentNM(); + if (!TheoryUfRewriter::canUseAsApplyUfOperator(f)) + { + NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f); + if (itus == d_uf_std_skolem.end()) + { + std::unordered_set<Node, NodeHashFunction> fvs; + expr::getFreeVariables(f, fvs); + Node lem; + if (!fvs.empty()) + { + std::vector<TypeNode> newTypes; + std::vector<Node> vs; + std::vector<Node> nvs; + for (const Node& v : fvs) + { + TypeNode vt = v.getType(); + newTypes.push_back(vt); + Node nv = nm->mkBoundVar(vt); + vs.push_back(v); + nvs.push_back(nv); + } + TypeNode ft = f.getType(); + std::vector<TypeNode> argTypes = ft.getArgTypes(); + TypeNode rangeType = ft.getRangeType(); + + newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end()); + TypeNode nft = nm->mkFunctionType(newTypes, rangeType); + new_f = nm->mkSkolem("app_uf", nft); + for (const Node& v : vs) + { + new_f = nm->mkNode(HO_APPLY, new_f, v); + } + Assert(new_f.getType() == f.getType()); + Node eq = new_f.eqNode(f); + Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end()); + lem = nm->mkNode( + FORALL, nm->mkNode(BOUND_VAR_LIST, nvs), seq); + } + else + { + // introduce skolem to make a standard APPLY_UF + new_f = nm->mkSkolem("app_uf", f.getType()); + lem = new_f.eqNode(f); + } + Trace("uf-ho-lemma") + << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem + << std::endl; + d_parent.getOutputChannel().lemma(lem); + d_uf_std_skolem[f] = new_f; + } + else + { + new_f = (*itus).second; + } + // unroll the HO_APPLY, adding to the first argument position + // Note arguments in the vector args begin at position 1. + while (new_f.getKind() == HO_APPLY) + { + args.insert(args.begin() + 1, new_f[1]); + new_f = new_f[0]; + } + } + Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f)); + args[0] = new_f; + Node ret = nm->mkNode(APPLY_UF, args); + Assert(ret.getType() == node.getType()); + return ret; +} + +unsigned HoExtension::checkExtensionality(TheoryModel* m) +{ + eq::EqualityEngine* ee = d_parent.getEqualityEngine(); + unsigned num_lemmas = 0; + bool isCollectModel = (m != nullptr); + Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel=" + << isCollectModel << "..." << std::endl; + std::map<TypeNode, std::vector<Node> > func_eqcs; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); + while (!eqcs_i.isFinished()) + { + Node eqc = (*eqcs_i); + TypeNode tn = eqc.getType(); + if (tn.isFunction()) + { + // if during collect model, must have an infinite type + // if not during collect model, must have a finite type + if (tn.isInterpretedFinite() != isCollectModel) + { + func_eqcs[tn].push_back(eqc); + Trace("uf-ho-debug") + << " func eqc : " << tn << " : " << eqc << std::endl; + } + } + ++eqcs_i; + } + + for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin(); + itf != func_eqcs.end(); + ++itf) + { + for (unsigned j = 0, sizej = itf->second.size(); j < sizej; j++) + { + for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++) + { + // if these equivalence classes are not explicitly disequal, do + // extensionality to ensure distinctness + if (!ee->areDisequal(itf->second[j], itf->second[k], false)) + { + Node deq = + Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate()); + // either add to model, or add lemma + if (isCollectModel) + { + // add extentionality disequality to the model + Node edeq = getExtensionalityDeq(deq); + Assert(edeq.getKind() == NOT && edeq[0].getKind() == EQUAL); + // introducing terms, must add required constraints, e.g. to + // force equalities between APPLY_UF and HO_APPLY terms + for (unsigned r = 0; r < 2; r++) + { + if (!collectModelInfoHoTerm(edeq[0][r], m)) + { + return 1; + } + } + Trace("uf-ho-debug") + << "Add extensionality deq to model : " << edeq << std::endl; + if (!m->assertEquality(edeq[0][0], edeq[0][1], false)) + { + return 1; + } + } + else + { + // apply extensionality lemma + num_lemmas += applyExtensionality(deq); + } + } + } + } + } + return num_lemmas; +} + +unsigned HoExtension::applyAppCompletion(TNode n) +{ + Assert(n.getKind() == APPLY_UF); + + eq::EqualityEngine* ee = d_parent.getEqualityEngine(); + // must expand into APPLY_HO version if not there already + Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n); + if (!ee->hasTerm(ret) || !ee->areEqual(ret, n)) + { + Node eq = ret.eqNode(n); + Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq + << std::endl; + ee->assertEquality(eq, true, d_true); + return 1; + } + Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "." + << std::endl; + return 0; +} + +unsigned HoExtension::checkAppCompletion() +{ + Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl; + // compute the operators that are relevant (those for which an HO_APPLY exist) + std::set<TNode> rlvOp; + eq::EqualityEngine* ee = d_parent.getEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); + std::map<TNode, std::vector<Node> > apply_uf; + while (!eqcs_i.isFinished()) + { + Node eqc = (*eqcs_i); + Trace("uf-ho-debug") << " apply completion : visit eqc " << eqc + << std::endl; + eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); + while (!eqc_i.isFinished()) + { + Node n = *eqc_i; + if (n.getKind() == APPLY_UF || n.getKind() == HO_APPLY) + { + int curr_sum = 0; + std::map<TNode, bool> curr_rops; + if (n.getKind() == APPLY_UF) + { + TNode rop = ee->getRepresentative(n.getOperator()); + if (rlvOp.find(rop) != rlvOp.end()) + { + // try if its operator is relevant + curr_sum = applyAppCompletion(n); + if (curr_sum > 0) + { + return curr_sum; + } + } + else + { + // add to pending list + apply_uf[rop].push_back(n); + } + // Arguments are also relevant operators. + // It might be possible include fewer terms here, see #1115. + for (unsigned k = 0; k < n.getNumChildren(); k++) + { + if (n[k].getType().isFunction()) + { + TNode rop = ee->getRepresentative(n[k]); + curr_rops[rop] = true; + } + } + } + else + { + Assert(n.getKind() == HO_APPLY); + TNode rop = ee->getRepresentative(n[0]); + curr_rops[rop] = true; + } + for (std::map<TNode, bool>::iterator itc = curr_rops.begin(); + itc != curr_rops.end(); + ++itc) + { + TNode rop = itc->first; + if (rlvOp.find(rop) == rlvOp.end()) + { + rlvOp.insert(rop); + // now, try each pending APPLY_UF for this operator + std::map<TNode, std::vector<Node> >::iterator itu = + apply_uf.find(rop); + if (itu != apply_uf.end()) + { + for (unsigned j = 0, size = itu->second.size(); j < size; j++) + { + curr_sum = applyAppCompletion(itu->second[j]); + if (curr_sum > 0) + { + return curr_sum; + } + } + } + } + } + } + ++eqc_i; + } + ++eqcs_i; + } + return 0; +} + +unsigned HoExtension::check() +{ + Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl; + + // infer new facts based on apply completion until fixed point + unsigned num_facts; + do + { + num_facts = checkAppCompletion(); + if (d_parent.inConflict()) + { + Trace("uf-ho") << "...conflict during app-completion." << std::endl; + return 1; + } + } while (num_facts > 0); + + if (options::ufHoExt()) + { + unsigned num_lemmas = 0; + + num_lemmas = checkExtensionality(); + if (num_lemmas > 0) + { + Trace("uf-ho") << "...extensionality returned " << num_lemmas + << " lemmas." << std::endl; + return num_lemmas; + } + } + + Trace("uf-ho") << "...finished check higher order." << std::endl; + + return 0; +} + +bool HoExtension::collectModelInfoHo(std::set<Node>& termSet, TheoryModel* m) +{ + for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it) + { + Node n = *it; + // For model-building with ufHo, we require that APPLY_UF is always + // expanded to HO_APPLY. That is, we always expand to a fully applicative + // encoding during model construction. + if (!collectModelInfoHoTerm(n, m)) + { + return false; + } + } + int addedLemmas = checkExtensionality(m); + return addedLemmas == 0; +} + +bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m) +{ + if (n.getKind() == APPLY_UF) + { + Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n); + if (!m->assertEquality(n, hn, true)) + { + return false; + } + } + return true; +} + +} // namespace uf +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h new file mode 100644 index 000000000..a38d1803a --- /dev/null +++ b/src/theory/uf/ho_extension.h @@ -0,0 +1,195 @@ +/********************* */ +/*! \file ho_extension.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 The higher-order extension of TheoryUF. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__HO_EXTENSION_H +#define __CVC4__THEORY__UF__HO_EXTENSION_H + +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdo.h" +#include "expr/node.h" +#include "theory/theory_model.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +class TheoryUF; + +/** The higher-order extension of the theory of uninterpreted functions + * + * This extension is capable of handling UF constraints involving partial + * applications via the applicative encoding (kind HO_APPLY), and + * (dis)equalities involving function sorts. It uses a lazy applicative + * encoding and implements two axiom schemes, at a high level: + * + * (1) Extensionality, where disequalities between functions witnessed by + * arguments where the two functions differ, + * + * (2) App-Encode, where full applications of UF (kind APPLY_UF) are equated + * with curried applications (kind HO_APPLY). + * + * For more details, see "Extending SMT Solvers to Higher-Order", Barbosa et al. + */ +class HoExtension +{ + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + + public: + HoExtension(TheoryUF& p, context::Context* c, context::UserContext* u); + + /** expand definition + * + * This returns the expanded form of node. + * + * In particular, this function will convert applications of HO_APPLY + * to applications of APPLY_UF if they are fully applied, and introduce + * function variables for function heads that are not variables via the + * getApplyUfForHoApply method below. + */ + Node expandDefinition(Node node); + + /** check higher order + * + * This is called at full effort and infers facts and sends lemmas + * based on higher-order reasoning (specifically, extentionality and + * app completion). It returns the number of lemmas plus facts + * added to the equality engine. + */ + unsigned check(); + + /** applyExtensionality + * + * Given disequality deq f != g, if not already cached, this sends a lemma of + * the form: + * f = g V (f k) != (g k) for fresh constant k on the output channel of the + * parent TheoryUF object. This is an "extensionality lemma". + * Return value is the number of lemmas of this form sent on the output + * channel. + */ + unsigned applyExtensionality(TNode deq); + + /** collect model info + * + * This method adds the necessary equalities to the model m such that + * model construction is possible if this method returns true. These + * equalities may include HO_APPLY versions of all APPLY_UF terms. + * + * The argument termSet is the set of relevant terms that the parent TheoryUF + * object has added to m that belong to TheoryUF. + * + * This method ensures that the function variables in termSet + * respect extensionality. If some pair does not, then this method adds an + * extensionality equality directly to the equality engine of m. + * + * In more detail, functions f and g do not respect extensionality if f and g + * are not equal in the model, and there is not a pair of unequal witness + * terms f(k), g(k). In this case, we add the disequality + * f(k') != g(k') + * for fresh (tuple) of variables k' to the equality engine of m. Notice + * this is done only for functions whose type has infinite cardinality, + * since all functions with finite cardinality are ensured to respect + * extensionality by this point due to our extentionality inference schema. + * + * If this method returns true, then all pairs of functions that are in + * distinct equivalence classes will be guaranteed to be assigned different + * values in m. It returns false if any (dis)equality added to m led to + * an inconsistency in m. + */ + bool collectModelInfoHo(std::set<Node>& termSet, TheoryModel* m); + + protected: + /** get apply uf for ho apply + * + * This returns the APPLY_UF equivalent for the HO_APPLY term node, where + * node has non-functional return type (that is, it corresponds to a fully + * applied function term). + * This call may introduce a skolem for the head operator and send out a lemma + * specifying the definition. + */ + Node getApplyUfForHoApply(Node node); + + /** get extensionality disequality + * + * Given disequality deq f != g, this returns the disequality: + * (f k) != (g k) for fresh constant(s) k. + */ + Node getExtensionalityDeq(TNode deq); + + /** + * Check whether extensionality should be applied for any pair of terms in the + * equality engine. + * + * If we pass a null model m to this function, then we add extensionality + * lemmas to the output channel and return the total number of lemmas added. + * We only add lemmas for functions whose type is finite, since pairs of + * functions whose types are infinite can be made disequal in a model by + * witnessing a point they are disequal. + * + * If we pass a non-null model m to this function, then we add disequalities + * that correspond to the conclusion of extensionality lemmas to the model's + * equality engine. We return 0 if the equality engine of m is consistent + * after this call, and 1 otherwise. We only add disequalities for functions + * whose type is infinite, since our decision procedure guarantees that + * extensionality lemmas are added for all pairs of functions whose types are + * finite. + */ + unsigned checkExtensionality(TheoryModel* m = nullptr); + + /** applyAppCompletion + * This infers a correspondence between APPLY_UF and HO_APPLY + * versions of terms for higher-order. + * Given APPLY_UF node e.g. (f a b c), this adds the equality to its + * HO_APPLY equivalent: + * (f a b c) == (@ (@ (@ f a) b) c) + * to equality engine, if not already equal. + * Return value is the number of equalities added. + */ + unsigned applyAppCompletion(TNode n); + + /** check whether app-completion should be applied for any + * pair of terms in the equality engine. + */ + unsigned checkAppCompletion(); + /** collect model info for higher-order term + * + * This adds required constraints to m for term n. In particular, if n is + * an APPLY_UF term, we add its HO_APPLY equivalent in this call. We return + * true if the model m is consistent after this call. + */ + bool collectModelInfoHoTerm(Node n, TheoryModel* m); + + private: + /** common constants */ + Node d_true; + /** the parent of this extension */ + TheoryUF& d_parent; + /** extensionality has been applied to these disequalities */ + NodeSet d_extensionality; + + /** cache of getExtensionalityDeq below */ + std::map<Node, Node> d_extensionality_deq; + + /** map from non-standard operators to their skolems */ + NodeNodeMap d_uf_std_skolem; +}; /* class TheoryUF */ + +} // namespace uf +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__UF__HO_EXTENSION_H */ diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index dd79b571a..d528e948f 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -41,8 +41,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__UF__SYMMETRY_BREAKER_H -#define __CVC4__THEORY__UF__SYMMETRY_BREAKER_H +#ifndef CVC4__THEORY__UF__SYMMETRY_BREAKER_H +#define CVC4__THEORY__UF__SYMMETRY_BREAKER_H #include <iostream> #include <list> @@ -176,4 +176,4 @@ std::ostream& operator<<(std::ostream& out, const ::CVC4::theory::uf::SymmetryBr }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__SYMMETRY_BREAKER_H */ +#endif /* CVC4__THEORY__UF__SYMMETRY_BREAKER_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ddc0e1b90..6284ae31e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -29,8 +29,9 @@ #include "proof/uf_proof.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" +#include "theory/uf/cardinality_extension.h" +#include "theory/uf/ho_extension.h" #include "theory/uf/theory_uf_rewriter.h" -#include "theory/uf/theory_uf_strong_solver.h" using namespace std; @@ -49,11 +50,10 @@ TheoryUF::TheoryUF(context::Context* c, d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ - d_thss(NULL), + d_thss(nullptr), + d_ho(nullptr), d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true), d_conflict(c, false), - d_extensionality(u), - d_uf_std_skolem(u), d_functionsTerms(c), d_symb(u, instanceName) { @@ -61,13 +61,9 @@ TheoryUF::TheoryUF(context::Context* c, // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo()); - if( options::ufHo() ){ - d_equalityEngine.addFunctionKind(kind::HO_APPLY); - } } TheoryUF::~TheoryUF() { - delete d_thss; } void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -85,7 +81,13 @@ void TheoryUF::finishInit() { if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind() && options::ufssMode() != UF_SS_NONE) { - d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this); + d_thss.reset(new CardinalityExtension( + getSatContext(), getUserContext(), *d_out, this)); + } + if (options::ufHo()) + { + d_equalityEngine.addFunctionKind(kind::HO_APPLY); + d_ho.reset(new HoExtension(*this, getSatContext(), getUserContext())); } } @@ -143,7 +145,8 @@ void TheoryUF::check(Effort level) { d_equalityEngine.assertEquality(atom, polarity, fact); if( options::ufHo() && options::ufHoExt() ){ if( !polarity && !d_conflict && atom[0].getType().isFunction() ){ - applyExtensionality( fact ); + // apply extensionality eagerly using the ho extension + d_ho->applyExtensionality(fact); } } } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { @@ -168,89 +171,22 @@ void TheoryUF::check(Effort level) { } if(! d_conflict ){ + // check with the cardinality constraints extension if (d_thss != NULL) { d_thss->check(level); if( d_thss->isConflict() ){ d_conflict = true; } } + // check with the higher-order extension if(! d_conflict && fullEffort(level) ){ if( options::ufHo() ){ - checkHigherOrder(); + d_ho->check(); } } } }/* TheoryUF::check() */ -Node TheoryUF::getApplyUfForHoApply( Node node ) { - Assert( node[0].getType().getNumChildren()==2 ); - std::vector< TNode > args; - Node f = TheoryUfRewriter::decomposeHoApply( node, args, true ); - Node new_f = f; - NodeManager* nm = NodeManager::currentNM(); - if( !TheoryUfRewriter::canUseAsApplyUfOperator( f ) ){ - NodeNodeMap::const_iterator itus = d_uf_std_skolem.find( f ); - if( itus==d_uf_std_skolem.end() ){ - std::unordered_set<Node, NodeHashFunction> fvs; - expr::getFreeVariables(f, fvs); - Node lem; - if (!fvs.empty()) - { - std::vector<TypeNode> newTypes; - std::vector<Node> vs; - std::vector<Node> nvs; - for (const Node& v : fvs) - { - TypeNode vt = v.getType(); - newTypes.push_back(vt); - Node nv = nm->mkBoundVar(vt); - vs.push_back(v); - nvs.push_back(nv); - } - TypeNode ft = f.getType(); - std::vector<TypeNode> argTypes = ft.getArgTypes(); - TypeNode rangeType = ft.getRangeType(); - - newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end()); - TypeNode nft = nm->mkFunctionType(newTypes, rangeType); - new_f = nm->mkSkolem("app_uf", nft); - for (const Node& v : vs) - { - new_f = nm->mkNode(kind::HO_APPLY, new_f, v); - } - Assert(new_f.getType() == f.getType()); - Node eq = new_f.eqNode(f); - Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end()); - lem = nm->mkNode( - kind::FORALL, nm->mkNode(kind::BOUND_VAR_LIST, nvs), seq); - } - else - { - // introduce skolem to make a standard APPLY_UF - new_f = nm->mkSkolem("app_uf", f.getType()); - lem = new_f.eqNode(f); - } - Trace("uf-ho-lemma") << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem << std::endl; - d_out->lemma( lem ); - d_uf_std_skolem[f] = new_f; - }else{ - new_f = (*itus).second; - } - // unroll the HO_APPLY, adding to the first argument position - // Note arguments in the vector args begin at position 1. - while (new_f.getKind() == kind::HO_APPLY) - { - args.insert(args.begin() + 1, new_f[1]); - new_f = new_f[0]; - } - } - Assert( TheoryUfRewriter::canUseAsApplyUfOperator( new_f ) ); - args[0] = new_f; - Node ret = nm->mkNode(kind::APPLY_UF, args); - Assert(ret.getType() == node.getType()); - return ret; -} - Node TheoryUF::getOperatorForApplyTerm( TNode node ) { Assert( node.getKind()==kind::APPLY_UF || node.getKind()==kind::HO_APPLY ); if( node.getKind()==kind::APPLY_UF ){ @@ -266,18 +202,19 @@ unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) { } Node TheoryUF::expandDefinition(LogicRequest &logicRequest, Node node) { - Trace("uf-ho-debug") << "uf-ho-debug : expanding definition : " << node << std::endl; + Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : " + << node << std::endl; if( node.getKind()==kind::HO_APPLY ){ if( !options::ufHo() ){ std::stringstream ss; ss << "Partial function applications are not supported in default mode, try --uf-ho."; throw LogicException(ss.str()); } - // convert HO_APPLY to APPLY_UF if fully applied - if( node[0].getType().getNumChildren()==2 ){ - Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; - Node ret = getApplyUfForHoApply( node ); - Trace("uf-ho") << "uf-ho : expandDefinition : " << node << " to " << ret << std::endl; + Node ret = d_ho->expandDefinition(node); + if (ret != node) + { + Trace("uf-exp-def") << "TheoryUF::expandDefinition: higher-order: " + << node << " to " << ret << std::endl; return ret; } } @@ -391,18 +328,9 @@ bool TheoryUF::collectModelInfo(TheoryModel* m) } if( options::ufHo() ){ - for( std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it ){ - Node n = *it; - // for model-building with ufHo, we require that APPLY_UF is always - // expanded to HO_APPLY - if (!collectModelInfoHoTerm(n, m)) - { - return false; - } - } // must add extensionality disequalities for all pairs of (non-disequal) // function equivalence classes. - if (checkExtensionality(m) != 0) + if (!d_ho->collectModelInfoHo(termSet, m)) { return false; } @@ -412,19 +340,6 @@ bool TheoryUF::collectModelInfo(TheoryModel* m) return true; } -bool TheoryUF::collectModelInfoHoTerm(Node n, TheoryModel* m) -{ - if (n.getKind() == kind::APPLY_UF) - { - Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n); - if (!m->assertEquality(n, hn, true)) - { - return false; - } - } - return true; -} - void TheoryUF::presolve() { // TimerStat::CodeTimer codeTimer(d_presolveTimer); @@ -455,7 +370,8 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { while(!workList.empty()) { n = workList.back(); - if(n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS) { + if (n.isClosure()) + { // unsafe to go under quantifiers; we might pull bound vars out of scope! processed.insert(n); workList.pop_back(); @@ -748,236 +664,6 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } } -Node TheoryUF::getExtensionalityDeq(TNode deq) -{ - Assert( deq.getKind()==kind::NOT && deq[0].getKind()==kind::EQUAL ); - Assert( deq[0][0].getType().isFunction() ); - std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq); - if (it == d_extensionality_deq.end()) - { - TypeNode tn = deq[0][0].getType(); - std::vector<TypeNode> argTypes = tn.getArgTypes(); - std::vector< Node > skolems; - NodeManager* nm = NodeManager::currentNM(); - for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) - { - Node k = - nm->mkSkolem("k", argTypes[i], "skolem created for extensionality."); - skolems.push_back( k ); - } - Node t[2]; - for (unsigned i = 0; i < 2; i++) - { - std::vector< Node > children; - Node curr = deq[0][i]; - while( curr.getKind()==kind::HO_APPLY ){ - children.push_back( curr[1] ); - curr = curr[0]; - } - children.push_back( curr ); - std::reverse( children.begin(), children.end() ); - children.insert( children.end(), skolems.begin(), skolems.end() ); - t[i] = nm->mkNode(kind::APPLY_UF, children); - } - Node conc = t[0].eqNode( t[1] ).negate(); - d_extensionality_deq[deq] = conc; - return conc; - } - return it->second; -} - -unsigned TheoryUF::applyExtensionality(TNode deq) -{ - Assert(deq.getKind() == kind::NOT && deq[0].getKind() == kind::EQUAL); - Assert(deq[0][0].getType().isFunction()); - // apply extensionality - if (d_extensionality.find(deq) == d_extensionality.end()) - { - d_extensionality.insert(deq); - Node conc = getExtensionalityDeq(deq); - Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq[0], conc ); - Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem << std::endl; - d_out->lemma( lem ); - return 1; - } - return 0; -} - -unsigned TheoryUF::checkExtensionality(TheoryModel* m) -{ - unsigned num_lemmas = 0; - bool isCollectModel = (m != nullptr); - Trace("uf-ho") << "TheoryUF::checkExtensionality, collectModel=" - << isCollectModel << "..." << std::endl; - std::map< TypeNode, std::vector< Node > > func_eqcs; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - TypeNode tn = eqc.getType(); - if( tn.isFunction() ){ - // if during collect model, must have an infinite type - // if not during collect model, must have a finite type - if (tn.isInterpretedFinite() != isCollectModel) - { - func_eqcs[tn].push_back(eqc); - Trace("uf-ho-debug") - << " func eqc : " << tn << " : " << eqc << std::endl; - } - } - ++eqcs_i; - } - - for( std::map< TypeNode, std::vector< Node > >::iterator itf = func_eqcs.begin(); - itf != func_eqcs.end(); ++itf ){ - for( unsigned j=0; j<itf->second.size(); j++ ){ - for( unsigned k=(j+1); k<itf->second.size(); k++ ){ - // if these equivalence classes are not explicitly disequal, do extensionality to ensure distinctness - if (!d_equalityEngine.areDisequal( - itf->second[j], itf->second[k], false)) - { - Node deq = Rewriter::rewrite( itf->second[j].eqNode( itf->second[k] ).negate() ); - // either add to model, or add lemma - if (isCollectModel) - { - // add extentionality disequality to the model - Node edeq = getExtensionalityDeq(deq); - Assert(edeq.getKind() == kind::NOT - && edeq[0].getKind() == kind::EQUAL); - // introducing terms, must add required constraints, e.g. to - // force equalities between APPLY_UF and HO_APPLY terms - for (unsigned r = 0; r < 2; r++) - { - if (!collectModelInfoHoTerm(edeq[0][r], m)) - { - return 1; - } - } - Trace("uf-ho-debug") - << "Add extensionality deq to model : " << edeq << std::endl; - if (!m->assertEquality(edeq[0][0], edeq[0][1], false)) - { - return 1; - } - } - else - { - // apply extensionality lemma - num_lemmas += applyExtensionality(deq); - } - } - } - } - } - return num_lemmas; -} - -unsigned TheoryUF::applyAppCompletion( TNode n ) { - Assert( n.getKind()==kind::APPLY_UF ); - - //must expand into APPLY_HO version if not there already - Node ret = TheoryUfRewriter::getHoApplyForApplyUf( n ); - if( !d_equalityEngine.hasTerm( ret ) || !d_equalityEngine.areEqual( ret, n ) ){ - Node eq = ret.eqNode( n ); - Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq << std::endl; - d_equalityEngine.assertEquality(eq, true, d_true); - return 1; - }else{ - Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "." << std::endl; - return 0; - } -} - -unsigned TheoryUF::checkAppCompletion() { - Trace("uf-ho") << "TheoryUF::checkApplyCompletion..." << std::endl; - // compute the operators that are relevant (those for which an HO_APPLY exist) - std::set< TNode > rlvOp; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - std::map< TNode, std::vector< Node > > apply_uf; - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - Trace("uf-ho-debug") << " apply completion : visit eqc " << eqc << std::endl; - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - if( n.getKind()==kind::APPLY_UF || n.getKind()==kind::HO_APPLY ){ - int curr_sum = 0; - std::map< TNode, bool > curr_rops; - if( n.getKind()==kind::APPLY_UF ){ - TNode rop = d_equalityEngine.getRepresentative( n.getOperator() ); - if( rlvOp.find( rop )!=rlvOp.end() ){ - // try if its operator is relevant - curr_sum = applyAppCompletion( n ); - if( curr_sum>0 ){ - return curr_sum; - } - }else{ - // add to pending list - apply_uf[rop].push_back( n ); - } - //arguments are also relevant operators FIXME (github issue #1115) - for( unsigned k=0; k<n.getNumChildren(); k++ ){ - if( n[k].getType().isFunction() ){ - TNode rop = d_equalityEngine.getRepresentative( n[k] ); - curr_rops[rop] = true; - } - } - }else{ - Assert( n.getKind()==kind::HO_APPLY ); - TNode rop = d_equalityEngine.getRepresentative( n[0] ); - curr_rops[rop] = true; - } - for( std::map< TNode, bool >::iterator itc = curr_rops.begin(); itc != curr_rops.end(); ++itc ){ - TNode rop = itc->first; - if( rlvOp.find( rop )==rlvOp.end() ){ - rlvOp.insert( rop ); - // now, try each pending APPLY_UF for this operator - std::map< TNode, std::vector< Node > >::iterator itu = apply_uf.find( rop ); - if( itu!=apply_uf.end() ){ - for( unsigned j=0; j<itu->second.size(); j++ ){ - curr_sum = applyAppCompletion( itu->second[j] ); - if( curr_sum>0 ){ - return curr_sum; - } - } - } - } - } - } - ++eqc_i; - } - ++eqcs_i; - } - return 0; -} - -unsigned TheoryUF::checkHigherOrder() { - Trace("uf-ho") << "TheoryUF::checkHigherOrder..." << std::endl; - - // infer new facts based on apply completion until fixed point - unsigned num_facts; - do{ - num_facts = checkAppCompletion(); - if( d_conflict ){ - Trace("uf-ho") << "...conflict during app-completion." << std::endl; - return 1; - } - }while( num_facts>0 ); - - if( options::ufHoExt() ){ - unsigned num_lemmas = 0; - - num_lemmas = checkExtensionality(); - if( num_lemmas>0 ){ - Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas." << std::endl; - return num_lemmas; - } - } - - Trace("uf-ho") << "...finished check higher order." << std::endl; - - return 0; -} - } /* namespace CVC4::theory::uf */ } /* namespace CVC4::theory */ } /* namespace CVC4 */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index fb873e7dc..dd69b2ee2 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -17,9 +17,10 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__UF__THEORY_UF_H -#define __CVC4__THEORY__UF__THEORY_UF_H +#ifndef CVC4__THEORY__UF__THEORY_UF_H +#define CVC4__THEORY__UF__THEORY_UF_H +#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdo.h" #include "expr/node.h" @@ -32,12 +33,11 @@ namespace CVC4 { namespace theory { namespace uf { -class UfTermDb; -class StrongSolverTheoryUF; +class CardinalityExtension; +class HoExtension; class TheoryUF : public Theory { - friend class StrongSolverTheoryUF; typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; public: @@ -118,8 +118,10 @@ private: /** The notify class */ NotifyClass d_notify; - /** The associated theory strong solver (or NULL if none) */ - StrongSolverTheoryUF* d_thss; + /** The associated cardinality extension (or nullptr if it does not exist) */ + std::unique_ptr<CardinalityExtension> d_thss; + /** the higher-order solver extension (or nullptr if it does not exist) */ + std::unique_ptr<HoExtension> d_ho; /** Equaltity engine */ eq::EqualityEngine d_equalityEngine; @@ -130,14 +132,6 @@ private: /** The conflict node */ Node d_conflictNode; - /** extensionality has been applied to these disequalities */ - NodeSet d_extensionality; - - /** cache of getExtensionalityDeq below */ - std::map<Node, Node> d_extensionality_deq; - - /** map from non-standard operators to their skolems */ - NodeNodeMap d_uf_std_skolem; /** node for true */ Node d_true; @@ -180,85 +174,7 @@ private: /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - private: // for higher-order - /** get extensionality disequality - * - * Given disequality deq f != g, this returns the disequality: - * (f k) != (g k) for fresh constant(s) k. - */ - Node getExtensionalityDeq(TNode deq); - - /** applyExtensionality - * - * Given disequality deq f != g, if not already cached, this sends a lemma of - * the form: - * f = g V (f k) != (g k) for fresh constant k. - * on the output channel. This is an "extensionality lemma". - * Return value is the number of lemmas of this form sent on the output - * channel. - */ - unsigned applyExtensionality(TNode deq); - - /** - * Check whether extensionality should be applied for any pair of terms in the - * equality engine. - * - * If we pass a null model m to this function, then we add extensionality - * lemmas to the output channel and return the total number of lemmas added. - * We only add lemmas for functions whose type is finite, since pairs of - * functions whose types are infinite can be made disequal in a model by - * witnessing a point they are disequal. - * - * If we pass a non-null model m to this function, then we add disequalities - * that correspond to the conclusion of extensionality lemmas to the model's - * equality engine. We return 0 if the equality engine of m is consistent - * after this call, and 1 otherwise. We only add disequalities for functions - * whose type is infinite, since our decision procedure guarantees that - * extensionality lemmas are added for all pairs of functions whose types are - * finite. - */ - unsigned checkExtensionality(TheoryModel* m = nullptr); - - /** applyAppCompletion - * This infers a correspondence between APPLY_UF and HO_APPLY - * versions of terms for higher-order. - * Given APPLY_UF node e.g. (f a b c), this adds the equality to its - * HO_APPLY equivalent: - * (f a b c) == (@ (@ (@ f a) b) c) - * to equality engine, if not already equal. - * Return value is the number of equalities added. - */ - unsigned applyAppCompletion(TNode n); - - /** check whether app-completion should be applied for any - * pair of terms in the equality engine. - */ - unsigned checkAppCompletion(); - - /** check higher order - * This is called at full effort and infers facts and sends lemmas - * based on higher-order reasoning (specifically, extentionality and - * app completion above). It returns the number of lemmas plus facts - * added to the equality engine. - */ - unsigned checkHigherOrder(); - - /** collect model info for higher-order term - * - * This adds required constraints to m for term n. In particular, if n is - * an APPLY_UF term, we add its HO_APPLY equivalent in this call. We return - * true if the model m is consistent after this call. - */ - bool collectModelInfoHoTerm(Node n, TheoryModel* m); - - /** get apply uf for ho apply - * This returns the APPLY_UF equivalent for the HO_APPLY term node, where - * node has non-functional return type (that is, it corresponds to a fully - * applied function term). - * This call may introduce a skolem for the head operator and send out a lemma - * specifying the definition. - */ - Node getApplyUfForHoApply(Node node); + private: /** get the operator for this node (node should be either APPLY_UF or * HO_APPLY) */ @@ -300,10 +216,12 @@ private: eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } - StrongSolverTheoryUF* getStrongSolver() { - return d_thss; - } -private: + /** get a pointer to the uf with cardinality */ + CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); } + /** are we in conflict? */ + bool inConflict() const { return d_conflict; } + + private: bool areCareDisequal(TNode x, TNode y); void addCarePairs(TNodeTrie* t1, TNodeTrie* t2, @@ -315,4 +233,4 @@ private: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__THEORY_UF_H */ +#endif /* CVC4__THEORY__UF__THEORY_UF_H */ diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index f8c947d7a..4454b7e8c 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY_UF_MODEL_H -#define __CVC4__THEORY_UF_MODEL_H +#ifndef CVC4__THEORY_UF_MODEL_H +#define CVC4__THEORY_UF_MODEL_H #include "theory/theory_model.h" diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index d9b2cccaa..bad4189d6 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__UF__THEORY_UF_REWRITER_H -#define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H +#ifndef CVC4__THEORY__UF__THEORY_UF_REWRITER_H +#define CVC4__THEORY__UF__THEORY_UF_REWRITER_H #include "expr/node_algorithm.h" #include "theory/rewriter.h" @@ -213,4 +213,4 @@ public: //conversion between HO_APPLY AND APPLY_UF }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__THEORY_UF_REWRITER_H */ +#endif /* CVC4__THEORY__UF__THEORY_UF_REWRITER_H */ diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 013eb89a0..cb373b535 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H -#define __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H +#ifndef CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H +#define CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H namespace CVC4 { namespace theory { @@ -178,4 +178,4 @@ class HoApplyTypeRule { } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */ +#endif /* CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */ |