summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
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.cpp173
-rw-r--r--src/theory/uf/equality_engine.h32
-rw-r--r--src/theory/uf/equality_engine_types.h6
-rw-r--r--src/theory/uf/ho_extension.cpp434
-rw-r--r--src/theory/uf/ho_extension.h195
-rw-r--r--src/theory/uf/symmetry_breaker.h6
-rw-r--r--src/theory/uf/theory_uf.cpp366
-rw-r--r--src/theory/uf/theory_uf.h116
-rw-r--r--src/theory/uf/theory_uf_model.h4
-rw-r--r--src/theory/uf/theory_uf_rewriter.h6
-rw-r--r--src/theory/uf/theory_uf_type_rules.h6
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback