From 33fd76601b42599d9883889a03d59d0d85729661 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 27 Jul 2012 21:07:42 +0000 Subject: [PATCH] removing unecessary files --- src/theory/datatypes/Makefile.am | 4 - src/theory/datatypes/explanation_manager.cpp | 104 -- src/theory/datatypes/explanation_manager.h | 222 ---- src/theory/datatypes/theory_datatypes.h | 4 +- .../theory_datatypes_candidate_generator.h | 67 - src/theory/datatypes/union_find.cpp | 59 - src/theory/datatypes/union_find.h | 148 --- src/util/Makefile.am | 1 - src/util/congruence_closure.cpp | 25 - src/util/congruence_closure.h | 1094 ----------------- test/unit/Makefile.am | 2 - test/unit/theory/union_find_black.h | 189 --- test/unit/util/congruence_closure_white.h | 529 -------- 13 files changed, 1 insertion(+), 2447 deletions(-) delete mode 100644 src/theory/datatypes/explanation_manager.cpp delete mode 100644 src/theory/datatypes/explanation_manager.h delete mode 100644 src/theory/datatypes/theory_datatypes_candidate_generator.h delete mode 100644 src/theory/datatypes/union_find.cpp delete mode 100644 src/theory/datatypes/union_find.h delete mode 100644 src/util/congruence_closure.cpp delete mode 100644 src/util/congruence_closure.h delete mode 100644 test/unit/theory/union_find_black.h delete mode 100644 test/unit/util/congruence_closure_white.h diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am index 0e6197ac1..8b5fbe979 100644 --- a/src/theory/datatypes/Makefile.am +++ b/src/theory/datatypes/Makefile.am @@ -11,10 +11,6 @@ libdatatypes_la_SOURCES = \ theory_datatypes.h \ datatypes_rewriter.h \ theory_datatypes.cpp \ - union_find.h \ - union_find.cpp \ - explanation_manager.h \ - explanation_manager.cpp \ theory_datatypes_instantiator.h \ theory_datatypes_instantiator.cpp diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp deleted file mode 100644 index be0bf6805..000000000 --- a/src/theory/datatypes/explanation_manager.cpp +++ /dev/null @@ -1,104 +0,0 @@ -/********************* */ -/*! \file explanation_manager.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/datatypes/explanation_manager.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::datatypes; - -void ProofManager::setExplanation( Node n, Node jn, unsigned r ) -{ - Assert( n!=jn ); - d_exp[n] = std::pair< Node, unsigned >( jn, r ); -} - -//std::ostream& operator<<(std::ostream& os, Reason::Rule r) -//{ -// switch( r ){ -// -// } -//} - -void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm ) -{ - if( n.getKind()==kind::AND ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ) { - process( n[i], nb, pm ); - } - }else{ - if( !pm->hasExplained( n ) ){ - context::CDHashMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n ); - Reason r; - Node exp; - if( it!=d_drv_map.end() ){ - r = (*it).second; - if( !r.d_isInput ){ - if( r.d_e ){ - - Debug("emanager") << "Em::process: Consult externally for " << n << std::endl; - exp = r.d_e->explain( n, pm ); - //trivial case, explainer says that n is an input - if( exp==n ){ - r.d_isInput = true; - } - }else{ - exp = r.d_node; - pm->setExplanation( n, exp, r.d_reason ); - if( exp.isNull() ) Debug("emanager") << "Em::process: " << n << " is an axiom, reason = " << r.d_reason << endl; - } - } - } - - if( r.d_isInput ){ - Debug("emanager") << "Em::process: " << n << " is an input " << endl; - nb << n; - pm->setExplanation( n, Node::null(), Reason::input ); - }else if( !exp.isNull() ){ - Debug("emanager") << "Em::process: " << exp << " is the explanation for " << n << " " - << ", reason = " << pm->getReason( n ) << endl; - if( exp.getKind()==kind::AND ){ - for( int i=0; i<(int)exp.getNumChildren(); i++ ) { - process( exp[i], nb, pm ); - } - }else{ - process( exp, nb, pm ); - } - } - }else{ - Debug("emanager") << "Em::process: proof manager has already explained " << n << endl; - } - } -} - -Node ExplanationManager::explain( Node n, ProofManager* pm ) -{ - NodeBuilder<> nb(kind::AND); - if( pm ){ - pm->clear(); - process( n, nb, pm ); - }else{ - ProofManager pm; - process( n, nb, &pm ); - } - return ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; -} diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h deleted file mode 100644 index 174b90ff5..000000000 --- a/src/theory/datatypes/explanation_manager.h +++ /dev/null @@ -1,222 +0,0 @@ -/********************* */ -/*! \file explanation_manager.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Theory of datatypes. - ** - ** Theory of datatypes. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__DATATYPES__EXPLANATION_MANAGER_H -#define __CVC4__THEORY__DATATYPES__EXPLANATION_MANAGER_H - -#include "theory/theory.h" -#include "util/congruence_closure.h" -#include "util/datatype.h" -#include "util/hash.h" -#include "util/trans_closure.h" - -#include -#include -#include - -namespace CVC4 { -namespace theory { -namespace datatypes { - - -class Explainer; - -/** reason class */ -class Reason { -public: - enum Rule { - unspecified = 0, - contradiction = 1, - - cc_coarse, - - //coarse rules for idt - idt_cycle_coarse, - idt_inst_coarse, - //unification rules - idt_unify, - idt_clash, - //tester rules - idt_taxiom, - idt_tcong, - idt_tclash, - idt_texhaust, - //other rules - idt_inst, - idt_collapse, - idt_collapse2, - - input, - }; -public: - Reason() : d_e( NULL ), d_isInput( true ){} - Reason( Node n, unsigned r ) : d_node( n ), d_reason( r ), d_e( NULL ), d_isInput( false ) {} - Reason( Explainer* e ) : d_reason( 0 ), d_e( e ), d_isInput( false ){} - virtual ~Reason(){} - Node d_node; - unsigned d_reason; - Explainer* d_e; - bool d_isInput; -}; - -/** proof manager for theory lemmas */ -class ProofManager { -protected: - enum Effort { - MIN_EFFORT = 0, - STANDARD = 50, - FULL_EFFORT = 100 - };/* enum Effort */ - /** map from nodes to a description of how they are explained */ - std::map< Node, std::pair< Node, unsigned > > d_exp; - /** whether to produce proofs */ - Effort d_effort; -public: - ProofManager( Effort effort = STANDARD ) : d_effort( effort ){} - ~ProofManager(){} - void setExplanation( Node n, Node jn, unsigned r = 0 ); - bool hasExplained( Node n ) { return d_exp.find( n )!=d_exp.end(); } - Effort getEffort() { return d_effort; } - void clear() { d_exp.clear(); } - /** for debugging */ - Node getJustification( Node n ) { return d_exp[n].first; } - unsigned getReason( Node n ) { return d_exp[n].second; } -}; - -class Explainer -{ -public: - /** assert that n is true */ - virtual void assertTrue( Node n ) = 0; - /** get the explanation for n. - This should call pm->setExplanation( n1, jn1, r1 ) ... pm->setExplanation( nk, jnk, rk ) - for some set of Nodes n1...nk. - Satisfies post conditions: - - If pm->getEffort() = MAX_EFFORT, then each ( ni, jni, ri ) should be a precise - application or rule ri, i.e. applying proof rule ri to jni derives ni. - - If pm->getEffort() = STANDARD, then for each ( ni, jni, ri ), - jni is the (at least informal) justification for ni. - - Return value should be a (possibly empty) conjunction of nodes n'1...n'k, where each n'i occurs - (as a conjunct) in jn1...jnk, but not in n1...nk. - For each of these literals n'i, assertTrue( n'i ) was called. - - either pm->setExplanation( n, ... ) is called, or n is the return value. - */ - virtual Node explain( Node n, ProofManager* pm ) = 0; -}; - -template -class CongruenceClosureExplainer : public Explainer -{ -protected: - //pointer to the congruence closure module - CongruenceClosure* d_cc; -public: - CongruenceClosureExplainer(CongruenceClosure* cc) : - Explainer(), - d_cc( cc ){ - } - ~CongruenceClosureExplainer(){} - /** assert that n is true */ - void assertTrue( Node n ){ - Assert( n.getKind() == kind::EQUAL || n.getKind() == kind::IFF ); - d_cc->addEquality( n ); - } - /** get the explanation for n */ - Node explain( Node n, ProofManager* pm ){ - Assert( n.getKind() == kind::EQUAL || n.getKind() == kind::IFF ); - if( pm->getEffort()==ProofManager::FULL_EFFORT ){ - //unsupported - Assert( false ); - return Node::null(); - }else{ - Node exp = d_cc->explain( n[0], n[1] ); - if( exp!=n ){ - pm->setExplanation( n, exp, Reason::cc_coarse ); - } - return exp; - } - } -}; - - -class ExplanationManager : public Explainer -{ -private: - /** map from nodes and the reason for them */ - context::CDHashMap< Node, Reason, NodeHashFunction > d_drv_map; - /** has conflict */ - context::CDO< bool > d_hasConflict; - /** process the reason for node n */ - void process( Node n, NodeBuilder<>& nb, ProofManager* pm ); -public: - ExplanationManager(context::Context* c) : Explainer(), d_drv_map(c), d_hasConflict( c, false ){} - ~ExplanationManager(){} - - /** assert that n is true (n is an input) */ - void assertTrue( Node n ) { - //TODO: this can be optimized: - // if the previous explanation for n was empty (n is a tautology), - // then we should not claim it to be an input. - Reason r = d_drv_map[n]; - r.d_isInput = true; - } - /** n is explained */ - bool hasNode( Node n ) { return d_drv_map.find( n )!=d_drv_map.end(); } - /** n is explained */ - bool hasConflict() { return d_hasConflict.get() || hasNode( NodeManager::currentNM()->mkConst(false) ); } - /** jn is why n is true, by rule r */ - void addNode( Node n, Node jn, unsigned r = 0 ) { - if( !hasNode( n ) ){ - Assert( n!=jn ); - Debug("emanager") << "em::addNode: (" << jn << ", " << r << ") -> " << n << std::endl; - d_drv_map[n] = Reason( jn, r ); - } - } - /** Explainer e can tell you why n is true in the current state. */ - void addNode( Node n, Explainer* e ) { - if( !hasNode( n ) ){ - Debug("emanager") << "em::addNodeEx: (" << e << ") -> " << n << std::endl; - d_drv_map[n] = Reason( e ); - } - } - /** n is true by reason (axiom) r */ - void addNodeAxiom( Node n, unsigned r = 0 ) { addNode( n, Node::null(), r ); } - /** conclude a contradiction by jn and reason r */ - void addNodeConflict( Node jn, unsigned r = 0 ){ - addNode( NodeManager::currentNM()->mkConst(false), jn, r ); - d_hasConflict.set( true ); - } - /** get explanation for n - Requires pre conditions: TBD - Satisfies post conditions: TBD - */ - Node explain( Node n, ProofManager* pm = NULL ); - /** get conflict */ - Node getConflict( ProofManager* pm = NULL ){ - return explain( NodeManager::currentNM()->mkConst(false), pm ); - } -}; - - -} -} -} - -#endif diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 6d9672f95..725f9a5e6 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -22,17 +22,15 @@ #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H #include "theory/theory.h" -#include "util/congruence_closure.h" #include "util/datatype.h" -#include "theory/datatypes/union_find.h" #include "util/hash.h" #include "util/trans_closure.h" -#include "theory/datatypes/explanation_manager.h" #include "theory/uf/equality_engine.h" #include #include #include +#include "context/cdchunk_list.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/theory_datatypes_candidate_generator.h b/src/theory/datatypes/theory_datatypes_candidate_generator.h deleted file mode 100644 index 46c7ce7fb..000000000 --- a/src/theory/datatypes/theory_datatypes_candidate_generator.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file theory_uf_candidate generator.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Theory datatypes candidate generator - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H -#define __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H - -#include "theory/quantifiers_engine.h" -#include "theory/datatypes/theory_datatypes.h" -#include "theory/rr_inst_match.h" - -namespace CVC4 { -namespace theory { -namespace datatypes { - -namespace rrinst { -typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; - -// Just iterate amoung the equivalence class of the given node -// node::Null() *can't* be given to reset -class CandidateGeneratorTheoryClass : public CandidateGenerator{ -private: - //instantiator pointer - TheoryDatatypes* d_th; - //the equality class iterator - TheoryDatatypes::EqListN::const_iterator d_eqc_i; - TheoryDatatypes::EqListN* d_eqc; -public: - CandidateGeneratorTheoryClass( TheoryDatatypes* th): d_th( th ), d_eqc(NULL){} - ~CandidateGeneratorTheoryClass(){} - void resetInstantiationRound(){}; - void reset( TNode n ){ - TheoryDatatypes::EqListsN::const_iterator i = d_th->d_equivalence_class.find(n); - if(i == d_th->d_equivalence_class.end()){ - d_eqc = NULL; - } else { - d_eqc = (*i).second; - d_eqc_i = d_eqc->begin(); - } - }; //* the argument is not used - TNode getNextCandidate(){ - if( d_eqc == NULL || d_eqc_i == d_eqc->end() ) return Node::null(); - return *(d_eqc_i++); - }; -}; - - -} -} -} -} - -#endif /* __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H */ diff --git a/src/theory/datatypes/union_find.cpp b/src/theory/datatypes/union_find.cpp deleted file mode 100644 index 34706719e..000000000 --- a/src/theory/datatypes/union_find.cpp +++ /dev/null @@ -1,59 +0,0 @@ -/********************* */ -/*! \file union_find.cpp - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Path-compressing, backtrackable union-find using an undo - ** stack. Refactored from the UF union-find. - ** - ** Path-compressing, backtrackable union-find using an undo stack - ** rather than storing items in a CDMap<>. - **/ - -#include - -#include "theory/datatypes/union_find.h" -#include "util/Assert.h" -#include "expr/node.h" - -using namespace std; - -namespace CVC4 { -namespace theory { -namespace datatypes { - -template -void UnionFind::contextNotifyPop() { - Trace("datatypesuf") << "datatypesUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; - while(d_offset < d_trace.size()) { - pair p = d_trace.back(); - if(p.second.isNull()) { - d_map.erase(p.first); - Trace("datatypesuf") << "datatypesUF " << d_trace.size() << " erasing " << p.first << endl; - } else { - d_map[p.first] = p.second; - Trace("datatypesuf") << "datatypesUF " << d_trace.size() << " replacing " << p << endl; - } - d_trace.pop_back(); - } - Trace("datatypesuf") << "datatypesUF cancelling finished." << endl; -} - -// The following declarations allow us to put functions in the .cpp file -// instead of the header, since we know which instantiations are needed. - -template void UnionFind::contextNotifyPop(); - -template void UnionFind::contextNotifyPop(); - -}/* CVC4::theory::datatypes namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/datatypes/union_find.h b/src/theory/datatypes/union_find.h deleted file mode 100644 index 4893c3502..000000000 --- a/src/theory/datatypes/union_find.h +++ /dev/null @@ -1,148 +0,0 @@ -/********************* */ -/*! \file union_find.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Path-compressing, backtrackable union-find using an undo - ** stack. Refactored from the UF union-find. - ** - ** Path-compressing, backtrackable union-find using an undo stack - ** rather than storing items in a CDMap<>. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__DATATYPES__UNION_FIND_H -#define __CVC4__THEORY__DATATYPES__UNION_FIND_H - -#include -#include -#include - -#include "expr/node.h" -#include "context/cdo.h" - -namespace CVC4 { - -namespace context { - class Context; -}/* CVC4::context namespace */ - -namespace theory { -namespace datatypes { - -// NodeType \in { Node, TNode } -template -class UnionFind : context::ContextNotifyObj { - /** Our underlying map type. */ - typedef __gnu_cxx::hash_map MapType; - - /** - * Our map of Nodes to their canonical representatives. - * If a Node is not present in the map, it is its own - * representative. - */ - MapType d_map; - - /** Our undo stack for changes made to d_map. */ - std::vector > d_trace; - - /** Our current offset in the d_trace stack (context-dependent). */ - context::CDO d_offset; - -public: - UnionFind(context::Context* ctxt) : - context::ContextNotifyObj(ctxt), - d_offset(ctxt, 0) { - } - - ~UnionFind() throw() { } - - /** - * Return a Node's union-find representative, doing path compression. - */ - inline TNode find(TNode n); - - /** - * Return a Node's union-find representative, NOT doing path compression. - * This is useful for Assert() statements, debug checking, and similar - * things that you do NOT want to mutate the structure. - */ - inline TNode debugFind(TNode n) const; - - /** - * Set the canonical representative of n to newParent. They should BOTH - * be their own canonical representatives on entry to this funciton. - */ - inline void setCanon(TNode n, TNode newParent); - -protected: - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::contextNotifyPop(). - */ - void contextNotifyPop(); - -};/* class UnionFind<> */ - -template -inline TNode UnionFind::debugFind(TNode n) const { - typename MapType::const_iterator i = d_map.find(n); - if(i == d_map.end()) { - return n; - } else { - return debugFind((*i).second); - } -} - -template -inline TNode UnionFind::find(TNode n) { - Trace("datatypesuf") << "datatypesUF find of " << n << std::endl; - typename MapType::iterator i = d_map.find(n); - if(i == d_map.end()) { - Trace("datatypesuf") << "datatypesUF it is rep" << std::endl; - return n; - } else { - Trace("datatypesuf") << "datatypesUF not rep: par is " << (*i).second << std::endl; - std::pair pr = *i; - // our iterator is invalidated by the recursive call to find(), - // since it mutates the map - TNode p = find(pr.second); - if(p == pr.second) { - return p; - } - d_trace.push_back(std::make_pair(n, pr.second)); - d_offset = d_trace.size(); - Trace("datatypesuf") << "datatypesUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl; - pr.second = p; - d_map.insert(pr); - return p; - } -} - -template -inline void UnionFind::setCanon(TNode n, TNode newParent) { - Assert(d_map.find(n) == d_map.end()); - Assert(d_map.find(newParent) == d_map.end()); - if(n != newParent) { - Trace("datatypesuf") << "datatypesUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl; - d_map[n] = newParent; - d_trace.push_back(std::make_pair(n, TNode::null())); - d_offset = d_trace.size(); - } -} - -}/* CVC4::theory::datatypes namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /*__CVC4__THEORY__DATATYPES__UNION_FIND_H */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index a3c6a00e9..85c5f9657 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -23,7 +23,6 @@ libutil_la_SOURCES = \ backtrackable.h \ Makefile.am \ Makefile.in \ - congruence_closure.h \ debug.h \ exception.h \ hash.h \ diff --git a/src/util/congruence_closure.cpp b/src/util/congruence_closure.cpp deleted file mode 100644 index 14315ac5a..000000000 --- a/src/util/congruence_closure.cpp +++ /dev/null @@ -1,25 +0,0 @@ -/********************* */ -/*! \file congruence_closure.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief The congruence closure module implementation - ** - ** The congruence closure module implementation. - **/ - -#include "util/congruence_closure.h" - -using namespace std; - -namespace CVC4 { - -}/* CVC4 namespace */ diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h deleted file mode 100644 index d7b8b0a22..000000000 --- a/src/util/congruence_closure.h +++ /dev/null @@ -1,1094 +0,0 @@ -/********************* */ -/*! \file congruence_closure.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief The congruence closure module - ** - ** The congruence closure module. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__UTIL__CONGRUENCE_CLOSURE_H -#define __CVC4__UTIL__CONGRUENCE_CLOSURE_H - -#include -#include - -#include - -#include "expr/node_manager.h" -#include "expr/node.h" -#include "context/context_mm.h" -#include "context/cdo.h" -#include "context/cdhashmap.h" -#include "context/cdhashset.h" -#include "context/cdchunk_list.h" -#include "util/exception.h" -#include "context/stacking_map.h" -#include "util/stats.h" - -namespace CVC4 { - -template -class CongruenceClosure; - -template -std::ostream& operator<<(std::ostream& out, - const CongruenceClosure& cc); - -/** - * A CongruenceClosureException is thrown by - * CongruenceClosure::explain() when that method is asked to explain a - * congruence that doesn't exist. - */ -class CVC4_PUBLIC CongruenceClosureException : public Exception { -public: - inline CongruenceClosureException(std::string msg) : - Exception(std::string("Congruence closure exception: ") + msg) {} - inline CongruenceClosureException(const char* msg) : - Exception(std::string("Congruence closure exception: ") + msg) {} -};/* class CongruenceClosureException */ - -struct EndOfCongruenceOpList; -template -struct CongruenceOperator { - enum { kind = kind_ }; - typedef Tail_ Tail; -};/* class CongruenceOperator<> */ - -#define CONGRUENCE_OPERATORS_1(kind1) ::CVC4::CongruenceOperator -#define CONGRUENCE_OPERATORS_2(kind1, kind2) ::CVC4::CongruenceOperator -#define CONGRUENCE_OPERATORS_3(kind1, kind2, kind3) ::CVC4::CongruenceOperator -#define CONGRUENCE_OPERATORS_4(kind1, kind2, kind3, kind4) ::CVC4::CongruenceOperator -#define CONGRUENCE_OPERATORS_5(kind1, kind2, kind3, kind4, kind5) ::CVC4::CongruenceOperator - -/** - * Returns true if the kind k is registered as a congruence operator - * for this CongruenceClosure. (That is, if it's in the - * CongruenceOperatorList template parameter.) False otherwise. - */ -template -inline bool isInCongruenceOperatorList(Kind k) { - typedef typename CongruenceOperatorList::Tail Tail; - return k == Kind(CongruenceOperatorList::kind) || - isInCongruenceOperatorList(k); -} - -// specialization for empty list -template <> -inline bool isInCongruenceOperatorList(Kind k) { - return false; -} - -/** - * Congruence closure module for CVC4. - * - * This is a service class for theories. One uses a CongruenceClosure - * by adding a number of relevant terms with addTerm() and equalities - * with addEquality(). It then gets notified (through OutputChannel, - * below), of new equalities. - * - * OutputChannel is a template argument (it's probably a thin layer, - * and we want to avoid a virtual call hierarchy in this case, and - * enable aggressive inlining). It need only implement one method, - * notifyCongruent(): - * - * class MyOutputChannel { - * public: - * void notifyCongruent(TNode a, TNode b) { - * // CongruenceClosure is notifying us that "a" is now the EC - * // representative for "b" in this context. After a pop, "a" - * // will be its own representative again. Note that "a" and - * // "b" might never have been added with addTerm(). However, - * // something in their equivalence class was (for which a - * // previous notifyCongruent() would have notified you of - * // their EC representative, which is now "a" or "b"). - * // - * // This call is made while the merge is being done. If you - * // throw any exception here, you'll immediately exit the - * // CongruenceClosure call and will miss whatever pending - * // merges were being performed, leaving the CongruenceClosure - * // module in a bad state. Therefore if you throw, you should - * // only do so if you are going to backjump, re-establishing a - * // good (former) state. Keep this in mind if a - * // CVC4::Interrupted that *doesn't* lead to a backjump can - * // interrupt you. - * } - * }; - * - * CongruenceOperatorList is a typelist of congruence Kinds, - * e.g., CONGRUENCE_OPERATORS_1(kind::APPLY_UF) - * or CONGRUENCE_OPERATORS_2(kind::SELECT, kind::STORE) - */ -template -class CongruenceClosure { - /** The context */ - context::Context* d_context; - - /** The output channel */ - OutputChannel* d_out; - - // typedef all of these so that iterators are easy to define - typedef context::StackingMap RepresentativeMap; - typedef context::CDChunkList ClassList; - typedef context::CDHashMap ClassLists; - typedef context::CDChunkList UseList; - typedef context::CDHashMap UseLists; - typedef context::CDHashMap LookupMap; - - typedef __gnu_cxx::hash_map EqMap; - - typedef context::CDHashMap ProofMap; - typedef context::CDHashMap ProofLabel; - - // Simple, NON-context-dependent pending list, union find and "seen - // set" types for constructing explanations and - // nearestCommonAncestor(); see explain(). - typedef std::list > PendingProofList_t; - typedef __gnu_cxx::hash_map UnionFind_t; - typedef __gnu_cxx::hash_set SeenSet_t; - - RepresentativeMap d_representative; - ClassLists d_classList; - UseLists d_useList; - LookupMap d_lookup; - - EqMap d_eqMap; - context::CDHashSet d_added; - - ProofMap d_proof; - ProofLabel d_proofLabel; - - ProofMap d_proofRewrite; - - /** - * The set of terms we care about (i.e. those that have been given - * us with addTerm() and their representatives). - */ - typedef context::CDHashSet CareSet; - CareSet d_careSet; - - // === STATISTICS === - AverageStat d_explanationLength;/**< average explanation length */ - IntStat d_newSkolemVars;/**< new vars created */ - - static inline bool isCongruenceOperator(TNode n) { - // For the datatypes theory, we've removed the invariant that - // parameterized kinds must have at least one argument. Consider - // (CONSTRUCTOR nil) for instance. So, n here can be an operator - // that's normally checked for congruence (like CONSTRUCTOR) but - // shouldn't be treated as a congruence operator if it only has an - // operator and no children (like CONSTRUCTOR nil), since we can - // treat that as a simple variable. - return n.getNumChildren() > 0 && - isInCongruenceOperatorList(n.getKind()); - } - -public: - /** Construct a congruence closure module instance */ - CongruenceClosure(context::Context* ctxt, OutputChannel* out) - throw(AssertionException) : - d_context(ctxt), - d_out(out), - d_representative(ctxt), - d_classList(ctxt), - d_useList(ctxt), - d_lookup(ctxt), - d_added(ctxt), - d_proof(ctxt), - d_proofLabel(ctxt), - d_proofRewrite(ctxt), - d_careSet(ctxt), - d_explanationLength("congruence_closure::AverageExplanationLength"), - d_newSkolemVars("congruence_closure::NewSkolemVariables", 0) { - } - - ~CongruenceClosure() {} - - /** - * Add a term into CC consideration. This is context-dependent. - * Calls OutputChannel::notifyCongruent(), so it can throw anything - * that that function can. - */ - void addTerm(TNode trm); - - /** - * Add an equality literal eq into CC consideration. This is - * context-dependent. Calls OutputChannel::notifyCongruent() - * indirectly, so it can throw anything that that function can. - */ - void addEquality(TNode inputEq) { - if(Debug.isOn("cc")) { - Debug("cc") << "CC addEquality[" << d_context->getLevel() << "]: " << inputEq << std::endl; - } - Assert(inputEq.getKind() == kind::EQUAL || - inputEq.getKind() == kind::IFF); - NodeBuilder<> eqb(inputEq.getKind()); - if(isCongruenceOperator(inputEq[1]) && - !isCongruenceOperator(inputEq[0])) { - eqb << flatten(inputEq[1]) << inputEq[0]; - } else { - eqb << flatten(inputEq[0]) << replace(flatten(inputEq[1])); - } - Node eq = eqb; - addEq(eq, inputEq); - } - -private: - void addEq(TNode eq, TNode inputEq); - - Node flatten(TNode t) { - if(isCongruenceOperator(t)) { - NodeBuilder<> appb(t.getKind()); - Assert(replace(flatten(t.getOperator())) == t.getOperator(), - "CongruenceClosure:: bad state: higher-order term ??"); - if(t.getMetaKind() == kind::metakind::PARAMETERIZED) { - appb << t.getOperator(); - } - for(TNode::iterator i = t.begin(); i != t.end(); ++i) { - appb << replace(flatten(*i)); - } - return Node(appb); - } else { - return t; - } - } - - Node replace(TNode t) { - if(isCongruenceOperator(t)) { - EqMap::iterator i = d_eqMap.find(t); - if(i == d_eqMap.end()) { - ++d_newSkolemVars; - Node v = NodeManager::currentNM()->mkSkolem(t.getType()); - Debug("cc") << "CC made skolem " << v << std::endl; - addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null()); - d_added.insert(v); - d_eqMap[t] = v; - return v; - } else { - TNode v = (*i).second; - if(!d_added.contains(v)) { - addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null()); - d_added.insert(v); - } - return v; - } - } else { - return t; - } - } - - TNode proofRewrite(TNode pfStep) const { - ProofMap::const_iterator i = d_proofRewrite.find(pfStep); - if(i == d_proofRewrite.end()) { - return pfStep; - } else { - return (*i).second; - } - } - -public: - /** - * Inquire whether two expressions are congruent in the current - * context. - */ - inline bool areCongruent(TNode a, TNode b) const throw(AssertionException) { - if(Debug.isOn("cc")) { - Debug("cc") << "CC areCongruent? " << a << " == " << b << std::endl; - Debug("cc") << " a " << a << std::endl; - Debug("cc") << " a' " << normalize(a) << std::endl; - Debug("cc") << " b " << b << std::endl; - Debug("cc") << " b' " << normalize(b) << std::endl; - } - - Node ap = find(a), bp = find(b); - - // areCongruent() works fine as just find(a) == find(b) _except_ - // for terms not appearing in equalities. For example, let's say - // you have unary f and binary g, h, and - // - // a == f(b) ; f(a) == b ; g == h - // - // it's clear that h(f(a),a) == g(b,a), but it's not in the - // union-find even if you addTerm() on those two. - // - // we implement areCongruent() to handle more general - // queries---i.e., to check for new congruences---but shortcut a - // cheap & common case - // - return ap == bp || normalize(ap) == normalize(bp); - } - -private: - /** - * Find the EC representative for a term t in the current context. - */ - inline TNode find(TNode t) const throw(AssertionException) { - TNode rep1 = d_representative[t]; - return rep1.isNull() ? t : rep1; - } - - void explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list& pf) - throw(AssertionException); - - Node highestNode(TNode a, UnionFind_t& unionFind) const - throw(AssertionException); - - Node nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind) - throw(AssertionException); - -public: - /** - * Request an explanation for why a and b are in the same EC in the - * current context. Throws a CongruenceClosureException if they - * aren't in the same EC. - */ - Node explain(Node a, Node b) - throw(CongruenceClosureException, AssertionException); - - /** - * Request an explanation for why the lhs and rhs of this equality - * are in the same EC. Throws a CongruenceClosureException if they - * aren't in the same EC. - */ - inline Node explain(TNode eq) - throw(CongruenceClosureException, AssertionException) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - return explain(eq[0], eq[1]); - } - - /** - * Normalization. - */ - Node normalize(TNode t) const throw(AssertionException); - -private: - - friend std::ostream& operator<< <>(std::ostream& out, - const CongruenceClosure& cc); - - /** - * Internal propagation of information. Propagation tends to - * cascade (this implementation uses an iterative "pending" - * worklist), and "seed" is the "seeding" propagation to do (the - * first one). Calls OutputChannel::notifyCongruent() indirectly, - * so it can throw anything that that function can. - */ - void propagate(TNode seed); - - /** - * Internal lookup mapping from tuples to equalities. - */ - inline TNode lookup(TNode a) const { - LookupMap::iterator i = d_lookup.find(a); - if(i == d_lookup.end()) { - return TNode::null(); - } else { - TNode l = (*i).second; - Assert(l.getKind() == kind::EQUAL || - l.getKind() == kind::IFF); - return l; - } - } - - /** - * Internal lookup mapping. - */ - inline void setLookup(TNode a, TNode b) { - Assert(a.getKind() == kind::TUPLE); - Assert(b.getKind() == kind::EQUAL || - b.getKind() == kind::IFF); - d_lookup[a] = b; - } - - /** - * Given an apply (f a1 a2...), build a TUPLE expression - * (f', a1', a2', ...) suitable for a lookup() key. - */ - Node buildRepresentativesOfApply(TNode apply, Kind kindToBuild = kind::TUPLE) - throw(AssertionException); - - /** - * Append equality "eq" to uselist of "of". - */ - inline void appendToUseList(TNode of, TNode eq) { - Trace("cc") << "adding " << eq << " to use list of " << of << std::endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - Assert(of == find(of)); - UseLists::iterator usei = d_useList.find(of); - UseList* ul; - if(usei == d_useList.end()) { - ul = new(d_context->getCMM()) UseList(true, d_context, false, - context::ContextMemoryAllocator(d_context->getCMM())); - d_useList.insertDataFromContextMemory(of, ul); - } else { - ul = (*usei).second; - } - ul->push_back(eq); - } - - /** - * Merge equivalence class ec1 under ec2. ec1's new union-find - * representative becomes ec2. Calls - * OutputChannel::notifyCongruent(), so it can throw anything that - * that function can. - */ - void merge(TNode ec1, TNode ec2); - void mergeProof(TNode a, TNode b, TNode e); - -public: - - // === STATISTICS ACCESSORS === - - /** - * Get access to the explanation-length statistic. Returns the - * statistic itself so that reference-statistics can be wrapped - * around it, useful since CongruenceClosure is a client class and - * shouldn't be directly registered with the StatisticsRegistry. - */ - const AverageStat& getExplanationLength() const throw() { - return d_explanationLength; - } - - /** - * Get access to the new-skolem-vars statistic. Returns the - * statistic itself so that reference-statistics can be wrapped - * around it, useful since CongruenceClosure is a client class and - * shouldn't be directly registered with the StatisticsRegistry. - */ - const IntStat& getNewSkolemVars() const throw() { - return d_newSkolemVars; - } - -};/* class CongruenceClosure */ - - -template -void CongruenceClosure::addTerm(TNode t) { - Node trm = replace(flatten(t)); - Node trmp = find(trm); - - if(Debug.isOn("cc")) { - Debug("cc") << "CC addTerm [" << d_careSet.size() << "] " << d_careSet.contains(t) << ": " << t << std::endl - << " [" << d_careSet.size() << "] " << d_careSet.contains(trm) << ": " << trm << std::endl - << " [" << d_careSet.size() << "] " << d_careSet.contains(trmp) << ": " << trmp << std::endl; - } - - if(t != trm && !d_careSet.contains(t)) { - // we take care to only notify our client once of congruences - d_out->notifyCongruent(t, trm); - d_careSet.insert(t); - } - - if(!d_careSet.contains(trm)) { - if(trm != trmp) { - // if part of an equivalence class headed by another node, - // notify the client of this merge that's already been - // performed.. - d_out->notifyCongruent(trm, trmp); - } - - // add its representative to the care set - d_careSet.insert(trmp); - } -} - - -template -void CongruenceClosure::addEq(TNode eq, TNode inputEq) { - Assert(!eq[0].getType().isFunction() && !eq[1].getType().isFunction(), - "CongruenceClosure:: equality between function symbols not allowed"); - - d_proofRewrite[eq] = inputEq; - - if(Trace.isOn("cc")) { - Trace("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl; - } - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - Assert(!isCongruenceOperator(eq[1])); - if(areCongruent(eq[0], eq[1])) { - Trace("cc") << "CC -- redundant, ignoring...\n"; - return; - } - - TNode s = eq[0], t = eq[1]; - - Assert(s != t); - - Trace("cc:detail") << "CC " << s << " == " << t << std::endl; - - // change from paper: do this whether or not s, t are applications - Trace("cc:detail") << "CC propagating the eq" << std::endl; - - if(!isCongruenceOperator(s)) { - // s, t are constants - propagate(eq); - } else { - // s is an apply, t is a constant - Node ap = buildRepresentativesOfApply(s); - - Trace("cc:detail") << "CC rewrLHS " << "op_and_args_a == " << t << std::endl; - Trace("cc") << "CC ap is " << ap << std::endl; - - TNode l = lookup(ap); - Trace("cc:detail") << "CC lookup(ap): " << l << std::endl; - if(!l.isNull()) { - // ensure a hard Node link exists to this during the call - Node pending = NodeManager::currentNM()->mkNode(kind::TUPLE, eq, l); - Trace("cc:detail") << "pending1 " << pending << std::endl; - propagate(pending); - } else { - Trace("cc") << "CC lookup(ap) setting to " << eq << std::endl; - setLookup(ap, eq); - for(Node::iterator i = ap.begin(); i != ap.end(); ++i) { - appendToUseList(*i, eq); - } - } - } -}/* addEq() */ - - -template -Node CongruenceClosure::buildRepresentativesOfApply(TNode apply, - Kind kindToBuild) - throw(AssertionException) { - Assert(isCongruenceOperator(apply)); - NodeBuilder<> argspb(kindToBuild); - Assert(find(apply.getOperator()) == apply.getOperator(), - "CongruenceClosure:: bad state: " - "function symbol (or other congruence operator) merged with another"); - if(apply.getMetaKind() == kind::metakind::PARAMETERIZED) { - argspb << apply.getOperator(); - } - for(TNode::iterator i = apply.begin(); i != apply.end(); ++i) { - argspb << find(*i); - } - return argspb; -}/* buildRepresentativesOfApply() */ - - -template -void CongruenceClosure::propagate(TNode seed) { - Trace("cc:detail") << "=== doing a round of propagation ===" << std::endl - << "the \"seed\" propagation is: " << seed << std::endl; - - std::list pending; - - Trace("cc") << "seed propagation with: " << seed << std::endl; - pending.push_back(seed); - do { // while(!pending.empty()) - Node e = pending.front(); - pending.pop_front(); - - Trace("cc") << "=== top of propagate loop ===" << std::endl - << "=== e is " << e << " ===" << std::endl; - - TNode a, b; - if(e.getKind() == kind::EQUAL || - e.getKind() == kind::IFF) { - // e is an equality a = b (a, b are constants) - - a = e[0]; - b = e[1]; - - Trace("cc:detail") << "propagate equality: " << a << " == " << b << std::endl; - } else { - // e is a tuple ( apply f A... = a , apply f B... = b ) - - Trace("cc") << "propagate tuple: " << e << "\n"; - - Assert(e.getKind() == kind::TUPLE); - - Assert(e.getNumChildren() == 2); - Assert(e[0].getKind() == kind::EQUAL || - e[0].getKind() == kind::IFF); - Assert(e[1].getKind() == kind::EQUAL || - e[1].getKind() == kind::IFF); - - // tuple is (eq, lookup) - a = e[0][1]; - b = e[1][1]; - - Assert(!isCongruenceOperator(a)); - Assert(!isCongruenceOperator(b)); - - Trace("cc") << " ( " << a << " , " << b << " )" << std::endl; - } - - if(Debug.isOn("cc")) { - Trace("cc:detail") << "=====at start=====" << std::endl - << "a :" << a << std::endl - << "NORMALIZE a:" << normalize(a) << std::endl - << "b :" << b << std::endl - << "NORMALIZE b:" << normalize(b) << std::endl - << "alreadyCongruent?:" << areCongruent(a,b) << std::endl; - } - - // change from paper: need to normalize() here since in our - // implementation, a and b can be applications - Node ap = find(a), bp = find(b); - if(ap != bp) { - - Trace("cc:detail") << "EC[a] == " << ap << std::endl - << "EC[b] == " << bp << std::endl; - - { // w.l.o.g., |classList ap| <= |classList bp| - ClassLists::iterator cl_api = d_classList.find(ap); - ClassLists::iterator cl_bpi = d_classList.find(bp); - unsigned sizeA = (cl_api == d_classList.end() ? 0 : (*cl_api).second->size()); - unsigned sizeB = (cl_bpi == d_classList.end() ? 0 : (*cl_bpi).second->size()); - Trace("cc") << "sizeA == " << sizeA << " sizeB == " << sizeB << std::endl; - if(sizeA > sizeB) { - Trace("cc") << "swapping..\n"; - TNode tmp = ap; ap = bp; bp = tmp; - tmp = a; a = b; b = tmp; - } - } - - { // class list handling - ClassLists::iterator cl_bpi = d_classList.find(bp); - ClassList* cl_bp; - if(cl_bpi == d_classList.end()) { - cl_bp = new(d_context->getCMM()) ClassList(true, d_context, false, - context::ContextMemoryAllocator(d_context->getCMM())); - d_classList.insertDataFromContextMemory(bp, cl_bp); - Trace("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl; - } else { - cl_bp = (*cl_bpi).second; - } - // we don't store 'ap' in its own class list; so process it here - Trace("cc:detail") << "calling mergeproof/merge1 " << ap - << " AND " << bp << std::endl; - mergeProof(a, b, e); - merge(ap, bp); - - Trace("cc") << " adding ap == " << ap << std::endl - << " to class list of " << bp << std::endl; - cl_bp->push_back(ap); - ClassLists::const_iterator cli = d_classList.find(ap); - if(cli != d_classList.end()) { - const ClassList* cl = (*cli).second; - for(ClassList::const_iterator i = cl->begin(); - i != cl->end(); - ++i) { - TNode c = *i; - if(Debug.isOn("cc")) { - Debug("cc") << "c is " << c << "\n" - << " from cl of " << ap << std::endl; - Debug("cc") << " it's find ptr is: " << find(c) << std::endl; - } - Assert(find(c) == ap); - Trace("cc:detail") << "calling merge2 " << c << bp << std::endl; - merge(c, bp); - // move c from classList(ap) to classlist(bp); - //i = cl.erase(i);// difference from paper: don't need to erase - Trace("cc") << " adding c to class list of " << bp << std::endl; - cl_bp->push_back(c); - } - } - Trace("cc:detail") << "bottom\n"; - } - - { // use list handling - if(Debug.isOn("cc:detail")) { - Debug("cc:detail") << "ap is " << ap << std::endl; - Debug("cc:detail") << "find(ap) is " << find(ap) << std::endl; - Debug("cc:detail") << "CC in prop go through useList of " << ap << std::endl; - } - UseLists::iterator usei = d_useList.find(ap); - if(usei != d_useList.end()) { - UseList* ul = (*usei).second; - //for( f(c1,c2)=c in UseList(ap) ) - for(UseList::const_iterator i = ul->begin(); - i != ul->end(); - ++i) { - TNode eq = *i; - Trace("cc") << "CC -- useList: " << eq << std::endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - // change from paper - // use list elts can have form (apply c..) = x OR x = (apply c..) - Assert(isCongruenceOperator(eq[0]) || - isCongruenceOperator(eq[1])); - // do for each side that is an application - for(int side = 0; side <= 1; ++side) { - if(!isCongruenceOperator(eq[side])) { - continue; - } - - Node cp = buildRepresentativesOfApply(eq[side]); - - // if lookup(c1',c2') is some f(d1,d2)=d then - TNode n = lookup(cp); - - Trace("cc:detail") << "CC -- c' is " << cp << std::endl; - - if(!n.isNull()) { - Trace("cc:detail") << "CC -- lookup(c') is " << n << std::endl; - // add (f(c1,c2)=c,f(d1,d2)=d) to pending - Node tuple = NodeManager::currentNM()->mkNode(kind::TUPLE, eq, n); - Trace("cc") << "CC add tuple to pending: " << tuple << std::endl; - pending.push_back(tuple); - // remove f(c1,c2)=c from UseList(ap) - Trace("cc:detail") << "supposed to remove " << eq << std::endl - << " from UseList of " << ap << std::endl; - //i = ul.erase(i);// difference from paper: don't need to erase - } else { - Trace("cc") << "CC -- lookup(c') is null" << std::endl; - Trace("cc") << "CC -- setlookup(c') to " << eq << std::endl; - // set lookup(c1',c2') to f(c1,c2)=c - setLookup(cp, eq); - // move f(c1,c2)=c from UseList(ap) to UseList(b') - //i = ul.erase(i);// difference from paper: don't need to erase - appendToUseList(bp, eq); - } - } - } - } - }/* use lists */ - Trace("cc:detail") << "CC in prop done with useList of " << ap << std::endl; - } else { - Trace("cc:detail") << "CCs the same ( == " << ap << "), do nothing." << std::endl; - } - - if(Debug.isOn("cc")) { - Debug("cc") << "=====at end=====" << std::endl - << "a :" << a << std::endl - << "NORMALIZE a:" << normalize(a) << std::endl - << "b :" << b << std::endl - << "NORMALIZE b:" << normalize(b) << std::endl - << "alreadyCongruent?:" << areCongruent(a,b) << std::endl; - } - Assert(areCongruent(a, b)); - } while(!pending.empty()); -}/* propagate() */ - - -template -void CongruenceClosure::merge(TNode ec1, TNode ec2) { - /* - if(Debug.isOn("cc:detail")) { - Debug("cc:detail") << " -- merging " << ec1 - << (d_careSet.find(ec1) == d_careSet.end() ? - " -- NOT in care set" : " -- IN CARE SET") << std::endl - << " and " << ec2 - << (d_careSet.find(ec2) == d_careSet.end() ? - " -- NOT in care set" : " -- IN CARE SET") << std::endl; - } - */ - - Trace("cc") << "CC setting rep of " << ec1 << std::endl; - Trace("cc") << "CC to " << ec2 << std::endl; - - /* can now be applications - Assert(!isCongruenceOperator(ec1)); - Assert(!isCongruenceOperator(ec2)); - */ - - Assert(find(ec1) != ec2); - //Assert(find(ec1) == ec1); - Assert(find(ec2) == ec2); - - d_representative.set(ec1, ec2); - - if(d_careSet.find(ec1) != d_careSet.end()) { - d_careSet.insert(ec2); - d_out->notifyCongruent(ec1, ec2); - } -}/* merge() */ - - -template -void CongruenceClosure::mergeProof(TNode a, TNode b, TNode e) { - Trace("cc") << " -- merge-proofing " << a << "\n" - << " and " << b << "\n" - << " with " << e << "\n"; - - // proof forest gets a -> b labeled with e - - // first reverse all the edges in proof forest to root of this proof tree - Trace("cc") << "CC PROOF reversing proof tree\n"; - // c and p are child and parent in (old) proof tree - Node c = a, p = d_proof[a], edgePf = d_proofLabel[a]; - // when we hit null p, we're at the (former) root - Trace("cc") << "CC PROOF start at c == " << c << std::endl - << " p == " << p << std::endl - << " edgePf == " << edgePf << std::endl; - while(!p.isNull()) { - // in proof forest, - // we have edge c --edgePf-> p - // turn it into c <-edgePf-- p - - Node pParSave = d_proof[p]; - Node pLabelSave = d_proofLabel[p]; - d_proof[p] = c; - d_proofLabel[p] = edgePf; - c = p; - p = pParSave; - edgePf = pLabelSave; - Trace("cc") << "CC PROOF now at c == " << c << std::endl - << " p == " << p << std::endl - << " edgePf == " << edgePf << std::endl; - } - - // add an edge from a to b - d_proof[a] = b; - d_proofLabel[a] = e; -}/* mergeProof() */ - - -template -Node CongruenceClosure::normalize(TNode t) const - throw(AssertionException) { - Trace("cc:detail") << "normalize " << t << std::endl; - if(!isCongruenceOperator(t)) {// t is a constant - t = find(t); - Trace("cc:detail") << " find " << t << std::endl; - return t; - } else {// t is an apply - NodeBuilder<> apb(kind::TUPLE); - Assert(normalize(t.getOperator()) == t.getOperator(), - "CongruenceClosure:: bad state: " - "function symbol merged with another"); - if(t.getMetaKind() == kind::metakind::PARAMETERIZED) { - apb << t.getOperator(); - } - Node n; - bool allConstants = (!isCongruenceOperator(n)); - for(TNode::iterator i = t.begin(); i != t.end(); ++i) { - TNode c = *i; - n = normalize(c); - apb << n; - allConstants = (allConstants && !isCongruenceOperator(n)); - } - - Node ap = apb; - Trace("cc:detail") << " got ap " << ap << std::endl; - - Node theLookup = lookup(ap); - if(allConstants && !theLookup.isNull()) { - Assert(theLookup.getKind() == kind::EQUAL || - theLookup.getKind() == kind::IFF); - Assert(isCongruenceOperator(theLookup[0])); - Assert(!isCongruenceOperator(theLookup[1])); - return find(theLookup[1]); - } else { - NodeBuilder<> fa(t.getKind()); - for(Node::iterator i = ap.begin(); i != ap.end(); ++i) { - fa << *i; - } - // ensure a hard Node link exists for the return - Node n = fa; - return n; - } - } -}/* normalize() */ - - -// This is the find() operation for the auxiliary union-find. This -// union-find is not context-dependent, as it's used only during -// explain(). It does path compression. -template -Node CongruenceClosure::highestNode(TNode a, UnionFind_t& unionFind) const - throw(AssertionException) { - UnionFind_t::iterator i = unionFind.find(a); - if(i == unionFind.end()) { - return a; - } else { - return unionFind[a] = highestNode((*i).second, unionFind); - } -}/* highestNode() */ - - -template -void CongruenceClosure::explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list& pf) - throw(AssertionException) { - - a = highestNode(a, unionFind); - Assert(c == highestNode(c, unionFind)); - - while(a != c) { - Node b = d_proof[a]; - Node e = d_proofLabel[a]; - if(e.getKind() == kind::EQUAL || - e.getKind() == kind::IFF) { - pf.push_back(e); - } else { - Assert(e.getKind() == kind::TUPLE); - pf.push_back(e[0]); - pf.push_back(e[1]); - Assert(isCongruenceOperator(e[0][0])); - Assert(!isCongruenceOperator(e[0][1])); - Assert(isCongruenceOperator(e[1][0])); - Assert(!isCongruenceOperator(e[1][1])); - Assert(e[0][0].getNumChildren() == e[1][0].getNumChildren()); - Assert(e[0][0].getOperator() == e[1][0].getOperator(), - "CongruenceClosure:: bad state: function symbols should be equal"); - // shouldn't have to prove this for operators - //pending.push_back(std::make_pair(e[0][0].getOperator(), e[1][0].getOperator())); - for(int i = 0, nc = e[0][0].getNumChildren(); i < nc; ++i) { - pending.push_back(std::make_pair(e[0][0][i], e[1][0][i])); - } - } - unionFind[a] = b; - a = highestNode(b, unionFind); - } -}/* explainAlongPath() */ - - -template -Node CongruenceClosure::nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind) - throw(AssertionException) { - SeenSet_t seen; - - Assert(find(a) == find(b)); - - do { - a = highestNode(a, unionFind); - seen.insert(a); - a = d_proof[a]; - } while(!a.isNull()); - - for(;;) { - b = highestNode(b, unionFind); - if(seen.find(b) != seen.end()) { - return b; - } - b = d_proof[b]; - - Assert(!b.isNull()); - } -}/* nearestCommonAncestor() */ - - -template -Node CongruenceClosure::explain(Node a, Node b) - throw(CongruenceClosureException, AssertionException) { - - Assert(a != b); - - if(!areCongruent(a, b)) { - throw CongruenceClosureException("asked to explain() congruence of nodes " - "that aren't congruent"); - } - - if(isCongruenceOperator(a)) { - a = replace(flatten(a)); - } - if(isCongruenceOperator(b)) { - b = replace(flatten(b)); - } - - PendingProofList_t pending; - UnionFind_t unionFind; - std::list terms; - - pending.push_back(std::make_pair(a, b)); - - Trace("cc") << "CC EXPLAINING " << a << " == " << b << std::endl; - - do {// while(!pending.empty()) - std::pair eq = pending.front(); - pending.pop_front(); - - a = eq.first; - b = eq.second; - - Node c = nearestCommonAncestor(a, b, unionFind); - - explainAlongPath(a, c, pending, unionFind, terms); - explainAlongPath(b, c, pending, unionFind, terms); - } while(!pending.empty()); - - if(Trace.isOn("cc")) { - Trace("cc") << "CC EXPLAIN final proof has size " << terms.size() << std::endl; - } - - NodeBuilder<> pf(kind::AND); - while(!terms.empty()) { - Node p = terms.front(); - terms.pop_front(); - Trace("cc") << "CC EXPLAIN " << p << std::endl; - p = proofRewrite(p); - Trace("cc") << " rewrite " << p << std::endl; - if(!p.isNull()) { - pf << p; - } - } - - Trace("cc") << "CC EXPLAIN done" << std::endl; - - Assert(pf.getNumChildren() > 0); - - if(pf.getNumChildren() == 1) { - d_explanationLength.addEntry(1.0); - return pf[0]; - } else { - d_explanationLength.addEntry(double(pf.getNumChildren())); - return pf; - } -}/* explain() */ - - -template -std::ostream& operator<<(std::ostream& out, - const CongruenceClosure& cc) { - out << "==============================================" << std::endl; - - /*out << "Representatives:" << std::endl; - for(typename CongruenceClosure::RepresentativeMap::const_iterator i = cc.d_representative.begin(); i != cc.d_representative.end(); ++i) { - out << " " << (*i).first << " => " << (*i).second << std::endl; - }*/ - - out << "ClassLists:" << std::endl; - for(typename CongruenceClosure::ClassLists::const_iterator i = cc.d_classList.begin(); i != cc.d_classList.end(); ++i) { - if(cc.find((*i).first) == (*i).first) { - out << " " << (*i).first << " =>" << std::endl; - for(typename CongruenceClosure::ClassList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) { - out << " " << *j << std::endl; - } - } - } - - out << "UseLists:" << std::endl; - for(typename CongruenceClosure::UseLists::const_iterator i = cc.d_useList.begin(); i != cc.d_useList.end(); ++i) { - if(cc.find((*i).first) == (*i).first) { - out << " " << (*i).first << " =>" << std::endl; - for(typename CongruenceClosure::UseList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) { - out << " " << *j << std::endl; - } - } - } - - out << "Lookup:" << std::endl; - for(typename CongruenceClosure::LookupMap::const_iterator i = cc.d_lookup.begin(); i != cc.d_lookup.end(); ++i) { - TNode n = (*i).second; - out << " " << (*i).first << " => " << n << std::endl; - } - - out << "Care set:" << std::endl; - for(typename CongruenceClosure::CareSet::const_iterator i = cc.d_careSet.begin(); i != cc.d_careSet.end(); ++i) { - out << " " << *i << std::endl; - } - - out << "==============================================" << std::endl; - - return out; -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__UTIL__CONGRUENCE_CLOSURE_H */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index d5b6ce5bf..1ab00bf8d 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,7 +4,6 @@ UNIT_TESTS = \ theory/theory_engine_white \ theory/theory_white \ theory/theory_arith_white \ - theory/union_find_black \ theory/theory_bv_white \ theory/type_enumerator_white \ expr/expr_public \ @@ -41,7 +40,6 @@ UNIT_TESTS = \ util/bitvector_black \ util/datatype_black \ util/configuration_black \ - util/congruence_closure_white \ util/output_black \ util/exception_black \ util/integer_black \ diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h deleted file mode 100644 index fead619d2..000000000 --- a/test/unit/theory/union_find_black.h +++ /dev/null @@ -1,189 +0,0 @@ -/********************* */ -/*! \file union_find_black.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Black box testing of CVC4::datatypes::UnionFind - ** - ** Black box testing of CVC4::theory::datatypes::UnionFind. - **/ - -#include - -#include "context/context.h" -#include "expr/node.h" -#include "theory/datatypes/union_find.h" - -using namespace CVC4; -using namespace CVC4::theory::datatypes; -using namespace CVC4::context; - -using namespace std; - -/** - * Test the UnionFind. - */ -class UnionFindBlack : public CxxTest::TestSuite { - Context* d_ctxt; - UnionFind* d_uf; - NodeManager* d_nm; - NodeManagerScope* d_scope; - - Node a, b, c, d, e, f, g; - -public: - - void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); - d_uf = new UnionFind(d_ctxt); - - a = d_nm->mkVar("a", d_nm->realType()); - b = d_nm->mkVar("b", d_nm->realType()); - c = d_nm->mkVar("c", d_nm->realType()); - d = d_nm->mkVar("d", d_nm->realType()); - e = d_nm->mkVar("e", d_nm->realType()); - f = d_nm->mkVar("f", d_nm->realType()); - g = d_nm->mkVar("g", d_nm->realType()); - } - - void tearDown() { - g = Node::null(); - f = Node::null(); - e = Node::null(); - d = Node::null(); - c = Node::null(); - b = Node::null(); - a = Node::null(); - - delete d_uf; - delete d_scope; - delete d_nm; - delete d_ctxt; - } - - void testSimpleContextual() { - TS_ASSERT(d_uf->find(a) == a); - TS_ASSERT(d_uf->find(b) == b); - TS_ASSERT(d_uf->find(c) == c); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == e); - TS_ASSERT(d_uf->find(f) == f); - TS_ASSERT(d_uf->find(g) == g); - - d_ctxt->push(); - - d_uf->setCanon(a, b); - - TS_ASSERT(d_uf->find(a) == b); - TS_ASSERT(d_uf->find(b) == b); - TS_ASSERT(d_uf->find(c) == c); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == e); - TS_ASSERT(d_uf->find(f) == f); - TS_ASSERT(d_uf->find(g) == g); - - d_ctxt->push(); - { - TS_ASSERT(d_uf->find(a) == b); - TS_ASSERT(d_uf->find(b) == b); - TS_ASSERT(d_uf->find(c) == c); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == e); - TS_ASSERT(d_uf->find(f) == f); - TS_ASSERT(d_uf->find(g) == g); - - d_uf->setCanon(c, d); - d_uf->setCanon(f, e); - - TS_ASSERT(d_uf->find(a) == b); - TS_ASSERT(d_uf->find(b) == b); - TS_ASSERT(d_uf->find(c) == d); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == e); - TS_ASSERT(d_uf->find(f) == e); - TS_ASSERT(d_uf->find(g) == g); - - d_ctxt->push(); - { - - TS_ASSERT(d_uf->find(a) == b); - TS_ASSERT(d_uf->find(b) == b); - TS_ASSERT(d_uf->find(c) == d); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == e); - TS_ASSERT(d_uf->find(f) == e); - TS_ASSERT(d_uf->find(g) == g); - -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(d_uf->setCanon(a, c), AssertionException); - TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(a), c), AssertionException); - TS_ASSERT_THROWS(d_uf->setCanon(a, d_uf->find(c)), AssertionException); -#endif /* CVC4_ASSERTIONS */ - d_uf->setCanon(d_uf->find(a), d_uf->find(c)); - d_uf->setCanon(d_uf->find(f), g); - d_uf->setCanon(d_uf->find(e), d); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(c), f), AssertionException); -#endif /* CVC4_ASSERTIONS */ - d_uf->setCanon(d_uf->find(c), d_uf->find(f)); - - TS_ASSERT(d_uf->find(a) == d); - TS_ASSERT(d_uf->find(b) == d); - TS_ASSERT(d_uf->find(c) == d); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == d); - TS_ASSERT(d_uf->find(f) == d); - TS_ASSERT(d_uf->find(g) == d); - - d_uf->setCanon(d_uf->find(g), d_uf->find(a)); - - TS_ASSERT(d_uf->find(a) == d); - TS_ASSERT(d_uf->find(b) == d); - TS_ASSERT(d_uf->find(c) == d); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == d); - TS_ASSERT(d_uf->find(f) == d); - TS_ASSERT(d_uf->find(g) == d); - - } - d_ctxt->pop(); - - TS_ASSERT(d_uf->find(a) == b); - TS_ASSERT(d_uf->find(b) == b); - TS_ASSERT(d_uf->find(c) == d); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == e); - TS_ASSERT(d_uf->find(f) == e); - TS_ASSERT(d_uf->find(g) == g); - } - d_ctxt->pop(); - - TS_ASSERT(d_uf->find(a) == b); - TS_ASSERT(d_uf->find(b) == b); - TS_ASSERT(d_uf->find(c) == c); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == e); - TS_ASSERT(d_uf->find(f) == f); - TS_ASSERT(d_uf->find(g) == g); - - d_ctxt->pop(); - - TS_ASSERT(d_uf->find(a) == a); - TS_ASSERT(d_uf->find(b) == b); - TS_ASSERT(d_uf->find(c) == c); - TS_ASSERT(d_uf->find(d) == d); - TS_ASSERT(d_uf->find(e) == e); - TS_ASSERT(d_uf->find(f) == f); - TS_ASSERT(d_uf->find(g) == g); - } -}; diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h deleted file mode 100644 index 0c14160f7..000000000 --- a/test/unit/util/congruence_closure_white.h +++ /dev/null @@ -1,529 +0,0 @@ -/********************* */ -/*! \file congruence_closure_white.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief White box testing of CVC4::CongruenceClosure. - ** - ** White box testing of CVC4::CongruenceClosure. - **/ - -#include -#include - -#include "context/context.h" -#include "context/cdhashset.h" -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "expr/kind.h" -#include "expr/node_manager.h" -#include "util/congruence_closure.h" - - -using namespace CVC4; -using namespace CVC4::context; -using namespace std; - - -struct MyOutputChannel { - CDHashSet d_notifications; - CDHashMap d_equivalences; - NodeManager* d_nm; - - MyOutputChannel(Context* ctxt, NodeManager* nm) : - d_notifications(ctxt), - d_equivalences(ctxt), - d_nm(nm) { - } - - bool saw(TNode a, TNode b) { - return d_notifications.contains(d_nm->mkNode(kind::EQUAL, a, b)) || - d_notifications.contains(d_nm->mkNode(kind::EQUAL, b, a)); - } - - TNode find(TNode n) { - CDHashMap::iterator i = d_equivalences.find(n); - if(i == d_equivalences.end()) { - return n; - } else { - // lazy path compression - TNode p = (*i).second; // parent - TNode f = d_equivalences[n] = find(p); // compress - return f; - } - } - - bool areCongruent(TNode a, TNode b) { - Debug("cc") << "=== a is " << a << std::endl - << "=== a' is " << find(a) << std::endl - << "=== b is " << b << std::endl - << "=== b' is " << find(b) << std::endl; - - return find(a) == find(b); - } - - void notifyCongruent(TNode a, TNode b) { - Debug("cc") << "======OI! I've been notified of: " - << a << " == " << b << std::endl; - - Node eq = d_nm->mkNode(kind::EQUAL, a, b); - Node eqRev = d_nm->mkNode(kind::EQUAL, b, a); - - TS_ASSERT(!d_notifications.contains(eq)); - TS_ASSERT(!d_notifications.contains(eqRev)); - - d_notifications.insert(eq); - - d_equivalences.insert(a, b); - } -};/* class MyOutputChannel */ - - -class CongruenceClosureWhite : public CxxTest::TestSuite { - Context* d_context; - NodeManager* d_nm; - NodeManagerScope* d_scope; - MyOutputChannel* d_out; - CongruenceClosure >* d_cc; - CongruenceClosure* d_ccArray; - - TypeNode U; - Node a, f, fa, ffa, fffa, ffffa, b, fb, ffb, fffb, ffffb; - Node g, gab, gba, gfafb, gfbfa, gfaa, gbfb; - Node h, hab, hba, hfaa; - Node a_eq_b, fa_eq_b, a_eq_fb, fa_eq_fb, h_eq_g; - - Node ar, ar_a, ar_b; - Node arar, arar_a, arar_b; - -public: - - void setUp() { - d_context = new Context; - d_nm = new NodeManager(d_context, NULL); - d_scope = new NodeManagerScope(d_nm); - d_out = new MyOutputChannel(d_context, d_nm); - d_cc = new CongruenceClosure >(d_context, d_out); - d_ccArray = new CongruenceClosure(d_context, d_out); - - U = d_nm->mkSort("U"); - - f = d_nm->mkVar("f", d_nm->mkFunctionType(U, U)); - a = d_nm->mkVar("a", U); - fa = d_nm->mkNode(kind::APPLY_UF, f, a); - ffa = d_nm->mkNode(kind::APPLY_UF, f, fa); - fffa = d_nm->mkNode(kind::APPLY_UF, f, ffa); - ffffa = d_nm->mkNode(kind::APPLY_UF, f, fffa); - b = d_nm->mkVar("b", U); - fb = d_nm->mkNode(kind::APPLY_UF, f, b); - ffb = d_nm->mkNode(kind::APPLY_UF, f, fb); - fffb = d_nm->mkNode(kind::APPLY_UF, f, ffb); - ffffb = d_nm->mkNode(kind::APPLY_UF, f, fffb); - vector args(2, U); - g = d_nm->mkVar("g", d_nm->mkFunctionType(args, U)); - gab = d_nm->mkNode(kind::APPLY_UF, g, a, b); - gfafb = d_nm->mkNode(kind::APPLY_UF, g, fa, fb); - gba = d_nm->mkNode(kind::APPLY_UF, g, b, a); - gfbfa = d_nm->mkNode(kind::APPLY_UF, g, fb, fa); - gfaa = d_nm->mkNode(kind::APPLY_UF, g, fa, a); - gbfb = d_nm->mkNode(kind::APPLY_UF, g, b, fb); - h = d_nm->mkVar("h", d_nm->mkFunctionType(args, U)); - hab = d_nm->mkNode(kind::APPLY_UF, h, a, b); - hba = d_nm->mkNode(kind::APPLY_UF, h, b, a); - hfaa = d_nm->mkNode(kind::APPLY_UF, h, fa, a); - - a_eq_b = d_nm->mkNode(kind::EQUAL, a, b); - fa_eq_b = d_nm->mkNode(kind::EQUAL, fa, b); - a_eq_fb = d_nm->mkNode(kind::EQUAL, a, fb); - fa_eq_fb = d_nm->mkNode(kind::EQUAL, fa, fb); - - h_eq_g = d_nm->mkNode(kind::EQUAL, h, g); - - // arrays - ar = d_nm->mkVar("ar", d_nm->mkArrayType(U, U)); - ar_a = d_nm->mkNode(kind::SELECT, ar, a); - ar_b = d_nm->mkNode(kind::SELECT, ar, b); - - arar = d_nm->mkVar("arar", d_nm->mkArrayType(U, d_nm->mkArrayType(U, U))); - arar_a = d_nm->mkNode(kind::SELECT, arar, a); - arar_b = d_nm->mkNode(kind::SELECT, arar, b); - } - - void tearDown() { - try { - arar = arar_a = arar_b = Node::null(); - ar = ar_a = ar_b = Node::null(); - - f = a = fa = ffa = fffa = ffffa = Node::null(); - b = fb = ffb = fffb = ffffb = Node::null(); - g = gab = gba = gfafb = gfbfa = gfaa = gbfb = Node::null(); - h = hab = hba = hfaa = Node::null(); - a_eq_b = fa_eq_b = a_eq_fb = fa_eq_fb = h_eq_g = Node::null(); - U = TypeNode::null(); - - delete d_ccArray; - delete d_cc; - delete d_out; - delete d_scope; - delete d_nm; - delete d_context; - } catch(Exception& e) { - cout << "\n\n" << e << "\n\n"; - throw; - } - } - - void testSimple() { - //Debug.on("cc"); - // add terms, then add equalities - - d_cc->addTerm(fa); - d_cc->addTerm(fb); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - } - - void testSimpleReverse() { - // add equalities, then add terms; should get the same as - // testSimple() - - d_cc->addEquality(a_eq_b); - - d_cc->addTerm(fa); - d_cc->addTerm(fb); - - TS_ASSERT(d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - } - - void testSimpleContextual() { - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - - { - d_context->push(); - - d_cc->addTerm(fa); - d_cc->addTerm(fb); - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - - { - d_context->push(); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - - d_context->pop(); - } - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - - d_context->pop(); - } - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - } - - void testSimpleContextualReverse() { - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - - { - d_context->push(); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - - { - d_context->push(); - - d_cc->addTerm(fa); - d_cc->addTerm(fb); - - TS_ASSERT(d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - - d_context->pop(); - } - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - - d_context->pop(); - } - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - } - - void test_f_of_f_of_something() { - d_cc->addTerm(ffa); - d_cc->addTerm(ffb); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(ffa, ffb)); - TS_ASSERT(d_cc->areCongruent(ffa, ffb)); - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - } - - void test_f4_of_something() { - d_cc->addTerm(ffffa); - d_cc->addTerm(ffffb); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(ffffa, ffffb)); - TS_ASSERT(d_cc->areCongruent(ffffa, ffffb)); - - TS_ASSERT(!d_out->areCongruent(fffa, fffb)); - TS_ASSERT(d_cc->areCongruent(fffa, fffb)); - - TS_ASSERT(!d_out->areCongruent(ffa, ffb)); - TS_ASSERT(d_cc->areCongruent(ffa, ffb)); - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - } - - void testSimpleBinaryFunction() { - d_cc->addTerm(gab); - d_cc->addTerm(gba); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(gab, gba)); - TS_ASSERT(d_cc->areCongruent(gab, gba)); - } - - void testSimpleBinaryFunction2() { - - //Debug.on("cc"); - try { - - d_cc->addTerm(gfafb); - d_cc->addTerm(gba); - d_cc->addTerm(gfaa); - d_cc->addTerm(hfaa); - - d_cc->addEquality(a_eq_fb); - d_cc->addEquality(fa_eq_b); - - TS_ASSERT(d_cc->areCongruent(a, fb)); - TS_ASSERT(d_cc->areCongruent(b, fa)); - TS_ASSERT(d_cc->areCongruent(fb, ffa)); - - Debug("cc") << "\n\n\n" - << "a norm: " << d_cc->normalize(a) << std::endl - << "fb norm: " << d_cc->normalize(fb) << std::endl - << "b norm: " << d_cc->normalize(b) << std::endl - << "fa norm: " << d_cc->normalize(fa) << std::endl - << "ffa norm: " << d_cc->normalize(ffa) << std::endl - << "ffffa norm " << d_cc->normalize(ffffa) << std::endl - << "ffffb norm " << d_cc->normalize(ffffb) << std::endl - << "gba norm: " << d_cc->normalize(gba) << std::endl - << "gfaa norm: " << d_cc->normalize(gfaa) << std::endl - << "gbfb norm: " << d_cc->normalize(gbfb) << std::endl - << "gfafb norm: " << d_cc->normalize(gfafb) << std::endl - << "hab norm: " << d_cc->normalize(hab) << std::endl - << "hba norm: " << d_cc->normalize(hba) << std::endl - << "hfaa norm: " << d_cc->normalize(hfaa) << std::endl; - - TS_ASSERT(d_out->areCongruent(gfafb, gba)); - TS_ASSERT(d_cc->areCongruent(b, fa)); - TS_ASSERT(d_cc->areCongruent(gfafb, gba)); - TS_ASSERT(d_cc->areCongruent(hba, hba)); - TS_ASSERT(d_cc->areCongruent(hfaa, hba)); - TS_ASSERT(d_out->areCongruent(gfaa, gba)); - TS_ASSERT(d_cc->areCongruent(gfaa, gba)); - - } catch(Exception& e) { - cout << "\n\n" << e << "\n\n"; - throw; - } - } - - void testUF() { - //Debug.on("cc"); - try{ - Node c_0 = d_nm->mkVar("c_0", U); - Node c_1 = d_nm->mkVar("c_1", U); - Node c_2 = d_nm->mkVar("c_2", U); - Node c2 = d_nm->mkVar("c2", U); - Node c3 = d_nm->mkVar("c3", U); - Node c4 = d_nm->mkVar("c4", U); - Node c5 = d_nm->mkVar("c5", U); - Node c6 = d_nm->mkVar("c6", U); - Node c7 = d_nm->mkVar("c7", U); - Node c8 = d_nm->mkVar("c8", U); - Node c9 = d_nm->mkVar("c9", U); - vector args2U(2, U); - Node f1 = d_nm->mkVar("f1", d_nm->mkFunctionType(args2U, U)); - - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_2)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_1),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_1)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_0),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_1),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0)))),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_2)))))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c2,c8),d_nm->mkNode(kind::APPLY_UF, f1,c4,c9))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c9,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c8,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c4,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c2,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c5,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c7,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c3,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c6,c_1)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_1),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_0),c_1)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0)); - } catch(Exception& e) { - cout << "\n\n" << e << "\n\n"; - throw e; - } - } - - void testUF2() { - Node f = d_nm->mkVar("f", d_nm->mkFunctionType(U, U)); - Node x = d_nm->mkVar("x", U); - Node y = d_nm->mkVar("y", U); - Node z = d_nm->mkVar("z", U); - Node ffx = d_nm->mkNode(kind::APPLY_UF, f, d_nm->mkNode(kind::APPLY_UF, f, x)); - Node fffx = d_nm->mkNode(kind::APPLY_UF, f, ffx); - Node ffffx = d_nm->mkNode(kind::APPLY_UF, f, fffx); - Node ffx_eq_fffx = ffx.eqNode(fffx); - Node ffx_eq_y = ffx.eqNode(y); - Node ffffx_eq_z = ffffx.eqNode(z); - - d_cc->addEquality(ffx_eq_fffx); - d_cc->addEquality(ffx_eq_y); - d_cc->addEquality(ffffx_eq_z); - } - - void testSimpleArray() { - //Debug.on("cc"); - // add terms, then add equalities - try { - d_ccArray->addTerm(ar_a); - d_ccArray->addTerm(ar_b); - - d_ccArray->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(ar_a, ar_b)); - TS_ASSERT(d_ccArray->areCongruent(ar_a, ar_b)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_ccArray->areCongruent(a, b)); - } catch(Exception& e) { - cout << "\n\n" << e << "\n\n"; - throw; - } - } - - void testSimpleReverseArray() { - // add equalities, then add terms; should get the same as - // testSimple() - - d_ccArray->addEquality(a_eq_b); - - d_ccArray->addTerm(ar_a); - d_ccArray->addTerm(ar_b); - - TS_ASSERT(d_out->areCongruent(ar_a, ar_b)); - TS_ASSERT(d_ccArray->areCongruent(ar_a, ar_b)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_ccArray->areCongruent(a, b)); - } - - void testArray() { - Node ar_eq_arar_a = d_nm->mkNode(kind::EQUAL, ar, arar_a); - Node ar2 = d_nm->mkVar("ar2", d_nm->mkArrayType(U, U)); - Node store_arar_b_ar2 = d_nm->mkNode(kind::STORE, arar, b, ar2); - Node select__store_arar_b_ar2__a = - d_nm->mkNode(kind::SELECT, store_arar_b_ar2, a); - Node select__store_arar_b_ar2__a__eq__arar_a = - d_nm->mkNode(kind::EQUAL, select__store_arar_b_ar2__a, arar_a); - - d_ccArray->addTerm(ar); - d_ccArray->addTerm(select__store_arar_b_ar2__a); - - d_ccArray->addEquality(ar_eq_arar_a); - d_ccArray->addEquality(select__store_arar_b_ar2__a__eq__arar_a); - - TS_ASSERT(d_ccArray->areCongruent(ar, select__store_arar_b_ar2__a)); - TS_ASSERT(d_out->areCongruent(ar, select__store_arar_b_ar2__a)); - } - -};/* class CongruenceClosureWhite */ -- 2.30.2