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
+++ /dev/null
-/********************* */
-/*! \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;
-}
+++ /dev/null
-/********************* */
-/*! \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 <ext/hash_set>
-#include <iostream>
-#include <map>
-
-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 OutputChannel, class CongruenceOperatorList>
-class CongruenceClosureExplainer : public Explainer
-{
-protected:
- //pointer to the congruence closure module
- CongruenceClosure<OutputChannel, CongruenceOperatorList>* d_cc;
-public:
- CongruenceClosureExplainer(CongruenceClosure<OutputChannel, CongruenceOperatorList>* 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
#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 <ext/hash_set>
#include <iostream>
#include <map>
+#include "context/cdchunk_list.h"
namespace CVC4 {
namespace theory {
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 <iostream>
-
-#include "theory/datatypes/union_find.h"
-#include "util/Assert.h"
-#include "expr/node.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace datatypes {
-
-template <class NodeType, class NodeHash>
-void UnionFind<NodeType, NodeHash>::contextNotifyPop() {
- Trace("datatypesuf") << "datatypesUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl;
- while(d_offset < d_trace.size()) {
- pair<TNode, TNode> 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<Node, NodeHashFunction>::contextNotifyPop();
-
-template void UnionFind<TNode, TNodeHashFunction>::contextNotifyPop();
-
-}/* CVC4::theory::datatypes namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \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 <utility>
-#include <vector>
-#include <ext/hash_map>
-
-#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 NodeType, class NodeHash>
-class UnionFind : context::ContextNotifyObj {
- /** Our underlying map type. */
- typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> 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<std::pair<TNode, TNode> > d_trace;
-
- /** Our current offset in the d_trace stack (context-dependent). */
- context::CDO<size_t> 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 <class NodeType, class NodeHash>
-inline TNode UnionFind<NodeType, NodeHash>::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 <class NodeType, class NodeHash>
-inline TNode UnionFind<NodeType, NodeHash>::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<TNode, TNode> 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 <class NodeType, class NodeHash>
-inline void UnionFind<NodeType, NodeHash>::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 */
backtrackable.h \
Makefile.am \
Makefile.in \
- congruence_closure.h \
debug.h \
exception.h \
hash.h \
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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 <sstream>
-#include <list>
-
-#include <ext/hash_map>
-
-#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 OutputChannel, class CongruenceOperatorList>
-class CongruenceClosure;
-
-template <class OutputChannel, class CongruenceOperatorList>
-std::ostream& operator<<(std::ostream& out,
- const CongruenceClosure<OutputChannel, CongruenceOperatorList>& 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 <Kind kind_, class Tail_ = EndOfCongruenceOpList>
-struct CongruenceOperator {
- enum { kind = kind_ };
- typedef Tail_ Tail;
-};/* class CongruenceOperator<> */
-
-#define CONGRUENCE_OPERATORS_1(kind1) ::CVC4::CongruenceOperator<kind1, ::CVC4::EndOfCongruenceOpList>
-#define CONGRUENCE_OPERATORS_2(kind1, kind2) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_1(kind2)>
-#define CONGRUENCE_OPERATORS_3(kind1, kind2, kind3) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_2(kind2, kind3)>
-#define CONGRUENCE_OPERATORS_4(kind1, kind2, kind3, kind4) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_3(kind2, kind3, kind4)>
-#define CONGRUENCE_OPERATORS_5(kind1, kind2, kind3, kind4, kind5) ::CVC4::CongruenceOperator<kind1, CONGRUENCE_OPERATORS_4(kind2, kind3, kind4, kind5)>
-
-/**
- * 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 <class CongruenceOperatorList>
-inline bool isInCongruenceOperatorList(Kind k) {
- typedef typename CongruenceOperatorList::Tail Tail;
- return k == Kind(CongruenceOperatorList::kind) ||
- isInCongruenceOperatorList<Tail>(k);
-}
-
-// specialization for empty list
-template <>
-inline bool isInCongruenceOperatorList<EndOfCongruenceOpList>(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 OutputChannel, class CongruenceOperatorList>
-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<Node, Node, NodeHashFunction> RepresentativeMap;
- typedef context::CDChunkList<TNode> ClassList;
- typedef context::CDHashMap<Node, ClassList*, NodeHashFunction> ClassLists;
- typedef context::CDChunkList<TNode> UseList;
- typedef context::CDHashMap<TNode, UseList*, TNodeHashFunction> UseLists;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> LookupMap;
-
- typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> EqMap;
-
- typedef context::CDHashMap<Node, Node, NodeHashFunction> ProofMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> ProofLabel;
-
- // Simple, NON-context-dependent pending list, union find and "seen
- // set" types for constructing explanations and
- // nearestCommonAncestor(); see explain().
- typedef std::list<std::pair<Node, Node> > PendingProofList_t;
- typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> UnionFind_t;
- typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> SeenSet_t;
-
- RepresentativeMap d_representative;
- ClassLists d_classList;
- UseLists d_useList;
- LookupMap d_lookup;
-
- EqMap d_eqMap;
- context::CDHashSet<TNode, TNodeHashFunction> 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<TNode, TNodeHashFunction> 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<CongruenceOperatorList>(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<Node>& 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<OutputChannel, CongruenceOperatorList>& 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<TNode>(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 <class OutputChannel, class CongruenceOperatorList>
-void CongruenceClosure<OutputChannel, CongruenceOperatorList>::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 <class OutputChannel, class CongruenceOperatorList>
-void CongruenceClosure<OutputChannel, CongruenceOperatorList>::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 <class OutputChannel, class CongruenceOperatorList>
-Node CongruenceClosure<OutputChannel, CongruenceOperatorList>::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 <class OutputChannel, class CongruenceOperatorList>
-void CongruenceClosure<OutputChannel, CongruenceOperatorList>::propagate(TNode seed) {
- Trace("cc:detail") << "=== doing a round of propagation ===" << std::endl
- << "the \"seed\" propagation is: " << seed << std::endl;
-
- std::list<Node> 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<TNode>(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 <class OutputChannel, class CongruenceOperatorList>
-void CongruenceClosure<OutputChannel, CongruenceOperatorList>::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 <class OutputChannel, class CongruenceOperatorList>
-void CongruenceClosure<OutputChannel, CongruenceOperatorList>::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 <class OutputChannel, class CongruenceOperatorList>
-Node CongruenceClosure<OutputChannel, CongruenceOperatorList>::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 <class OutputChannel, class CongruenceOperatorList>
-Node CongruenceClosure<OutputChannel, CongruenceOperatorList>::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 <class OutputChannel, class CongruenceOperatorList>
-void CongruenceClosure<OutputChannel, CongruenceOperatorList>::explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list<Node>& 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 <class OutputChannel, class CongruenceOperatorList>
-Node CongruenceClosure<OutputChannel, CongruenceOperatorList>::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 <class OutputChannel, class CongruenceOperatorList>
-Node CongruenceClosure<OutputChannel, CongruenceOperatorList>::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<Node> terms;
-
- pending.push_back(std::make_pair(a, b));
-
- Trace("cc") << "CC EXPLAINING " << a << " == " << b << std::endl;
-
- do {// while(!pending.empty())
- std::pair<Node, Node> 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 <class OutputChannel, class CongruenceOperatorList>
-std::ostream& operator<<(std::ostream& out,
- const CongruenceClosure<OutputChannel, CongruenceOperatorList>& cc) {
- out << "==============================================" << std::endl;
-
- /*out << "Representatives:" << std::endl;
- for(typename CongruenceClosure<OutputChannel, CongruenceOperatorList>::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<OutputChannel, CongruenceOperatorList>::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<OutputChannel, CongruenceOperatorList>::ClassList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) {
- out << " " << *j << std::endl;
- }
- }
- }
-
- out << "UseLists:" << std::endl;
- for(typename CongruenceClosure<OutputChannel, CongruenceOperatorList>::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<OutputChannel, CongruenceOperatorList>::UseList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) {
- out << " " << *j << std::endl;
- }
- }
- }
-
- out << "Lookup:" << std::endl;
- for(typename CongruenceClosure<OutputChannel, CongruenceOperatorList>::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<OutputChannel, CongruenceOperatorList>::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 */
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 \
util/bitvector_black \
util/datatype_black \
util/configuration_black \
- util/congruence_closure_white \
util/output_black \
util/exception_black \
util/integer_black \
+++ /dev/null
-/********************* */
-/*! \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 <cxxtest/TestSuite.h>
-
-#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<TNode, TNodeHashFunction>* 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<TNode, TNodeHashFunction>(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);
- }
-};
+++ /dev/null
-/********************* */
-/*! \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 <cxxtest/TestSuite.h>
-#include <sstream>
-
-#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<Node, NodeHashFunction> d_notifications;
- CDHashMap<Node, Node, NodeHashFunction> 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<Node, Node, NodeHashFunction>::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<MyOutputChannel, CongruenceOperator<kind::APPLY_UF> >* d_cc;
- CongruenceClosure<MyOutputChannel, CONGRUENCE_OPERATORS_2(kind::SELECT, kind::STORE)>* 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<MyOutputChannel, CongruenceOperator<kind::APPLY_UF> >(d_context, d_out);
- d_ccArray = new CongruenceClosure<MyOutputChannel, CONGRUENCE_OPERATORS_2(kind::SELECT, kind::STORE)>(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<TypeNode> 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<TypeNode> 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 */
projects / cvc5.git / commitdiff