diff options
Diffstat (limited to 'src/theory/quantifiers/quant_equality_engine.h')
-rw-r--r-- | src/theory/quantifiers/quant_equality_engine.h | 124 |
1 files changed, 0 insertions, 124 deletions
diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h deleted file mode 100644 index aa201bbc3..000000000 --- a/src/theory/quantifiers/quant_equality_engine.h +++ /dev/null @@ -1,124 +0,0 @@ -/********************* */ -/*! \file quant_equality_engine.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 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 Congruence closure with free variables - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H -#define __CVC4__QUANTIFIERS_EQUALITY_ENGINE_H - -#include <iostream> -#include <string> -#include <vector> -#include <map> -#include "expr/node.h" -#include "expr/type_node.h" -#include "theory/quantifiers_engine.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class QuantEqualityEngine : public QuantifiersModule { - typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; -private: - //notification class for equality engine - class NotifyClass : public eq::EqualityEngineNotify { - QuantEqualityEngine& d_qee; - public: - NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) override - { - return true; - } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) override - { - return true; - } - bool eqNotifyTriggerTermEquality(TheoryId tag, - TNode t1, - TNode t2, - bool value) override - { - return true; - } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) override - { - d_qee.conflict(t1, t2); - } - void eqNotifyNewClass(TNode t) override { d_qee.eqNotifyNewClass(t); } - void eqNotifyPreMerge(TNode t1, TNode t2) override - { - d_qee.eqNotifyPreMerge(t1, t2); - } - void eqNotifyPostMerge(TNode t1, TNode t2) override - { - d_qee.eqNotifyPostMerge(t1, t2); - } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override - { - d_qee.eqNotifyDisequal(t1, t2, reason); - } - };/* class ConjectureGenerator::NotifyClass */ - /** The notify class */ - NotifyClass d_notify; - /** (universal) equaltity engine */ - eq::EqualityEngine d_uequalityEngine; - /** Are we in conflict */ - context::CDO<bool> d_conflict; - /** list of redundant quantifiers in current context */ - context::CDList<Node> d_quant_red; - /** unprocessed quantifiers in current context */ - NodeBoolMap d_quant_unproc; - // map predicates to functions over int - TypeNode d_intType; - std::map< Node, Node > d_pred_to_func; - Node getFunctionForPredicate( Node f ); - Node getFunctionAppForPredicateApp( Node n ); -private: - void conflict(TNode t1, TNode t2); - void eqNotifyNewClass(TNode t); - void eqNotifyPreMerge(TNode t1, TNode t2); - void eqNotifyPostMerge(TNode t1, TNode t2); - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - //queries - bool areUnivDisequalInternal( TNode n1, TNode n2 ); - bool areUnivEqualInternal( TNode n1, TNode n2 ); - TNode getUnivRepresentativeInternal( TNode n ); -public: - QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c ); - - /* whether this module needs to check this round */ - bool needsCheck(Theory::Effort e) override; - /* reset at a round */ - void reset_round(Theory::Effort e) override; - /* Call during quantifier engine's check */ - void check(Theory::Effort e, QEffort quant_e) override; - /* Called for new quantifiers */ - void registerQuantifier(Node q) override; - /** called for everything that gets asserted */ - void assertNode(Node n) override; - /** Identify this module (for debugging, dynamic configuration, etc..) */ - std::string identify() const override { return "QuantEqualityEngine"; } - /** queries */ - bool areUnivDisequal( TNode n1, TNode n2 ); - bool areUnivEqual( TNode n1, TNode n2 ); - TNode getUnivRepresentative( TNode n ); -}; - - -} -} -} - -#endif |