diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/theory/quantifiers/equality_infer.h | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/theory/quantifiers/equality_infer.h')
-rw-r--r-- | src/theory/quantifiers/equality_infer.h | 103 |
1 files changed, 103 insertions, 0 deletions
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h new file mode 100644 index 000000000..93c7bd080 --- /dev/null +++ b/src/theory/quantifiers/equality_infer.h @@ -0,0 +1,103 @@ +/********************* */ +/*! \file equality_infer.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief additional inference for equalities + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H +#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H + +#include <ext/hash_set> +#include <iostream> +#include <map> +#include <vector> + +#include "context/context.h" +#include "context/context_mm.h" +#include "context/cdhashmap.h" +#include "context/cdchunk_list.h" +#include "context/cdhashset.h" +#include "theory/theory.h" + + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class EqualityInference +{ + typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; + typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; + typedef context::CDChunkList<Node> NodeList; + typedef context::CDHashMap< Node, NodeList *, NodeHashFunction > NodeListMap; +private: + context::Context * d_c; + Node d_one; + Node d_true; + class EqcInfo { + public: + EqcInfo(context::Context* c); + ~EqcInfo(){} + context::CDO< Node > d_rep; + //whether the eqc of this info is a representative and d_rep can been computed successfully + context::CDO< bool > d_valid; + //whether the eqc of this info is a solved variable + context::CDO< bool > d_solved; + //master equivalence class (a union find) + context::CDO< Node > d_master; + //a vector of equalities t1=t2 for which eqNotifyMerge(t1,t2) was called that explains d_rep + //NodeList d_rep_exp; + //the list of other eqc where this variable may be appear + //NodeList d_uselist; + }; + + /** track explanations */ + bool d_trackExplain; + /** information necessary for equivalence classes */ + BoolMap d_elim_vars; + std::map< Node, EqcInfo * > d_eqci; + NodeMap d_rep_to_eqc; + NodeListMap d_rep_exp; + /** set eqc rep */ + void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ); + /** use list */ + NodeListMap d_uselist; + void addToUseList( Node used, Node eqc ); + /** pending merges */ + NodeList d_pending_merges; + NodeList d_pending_merge_exp; + /** add to explanation */ + void addToExplanation( std::vector< Node >& exp, Node e ); + void addToExplanationEqc( std::vector< Node >& exp, Node eqc ); + void addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ); + /** for setting master/slave */ + Node getMaster( Node t, EqcInfo * eqc, bool& updated, Node new_m = Node::null() ); + bool updateMaster( Node t1, Node t2, EqcInfo * eqc1, EqcInfo * eqc2 ); +public: + //second argument is whether explanations should be tracked + EqualityInference(context::Context* c, bool trackExp = false); + virtual ~EqualityInference(); + /** input : notification when equality engine is updated */ + void eqNotifyNewClass(TNode t); + void eqNotifyMerge(TNode t1, TNode t2); + /** output : inferred equalities */ + unsigned getNumPendingMerges() { return d_pending_merges.size(); } + Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; } + Node getPendingMergeExplanation( unsigned i ); +}; + +} +} +} + +#endif |