diff options
Diffstat (limited to 'src/theory/sep/theory_sep.h')
| -rw-r--r-- | src/theory/sep/theory_sep.h | 294 |
1 files changed, 294 insertions, 0 deletions
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h new file mode 100644 index 000000000..852a36721 --- /dev/null +++ b/src/theory/sep/theory_sep.h @@ -0,0 +1,294 @@ +/********************* */ +/*! \file theory_sep.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Dejan Jovanovic, Clark Barrett + ** Minor contributors (to current version): Tim King, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory of sep + ** + ** Theory of sep. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__SEP__THEORY_SEP_H +#define __CVC4__THEORY__SEP__THEORY_SEP_H + +#include "theory/theory.h" +#include "util/statistics_registry.h" +#include "theory/uf/equality_engine.h" +#include "context/cdchunk_list.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdqueue.h" + +namespace CVC4 { +namespace theory { + +class TheoryModel; + +namespace sep { + +class TheorySep : public Theory { + typedef context::CDChunkList<Node> NodeList; + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + + ///////////////////////////////////////////////////////////////////////////// + // MISC + ///////////////////////////////////////////////////////////////////////////// + + private: + + /** True node for predicates = true */ + Node d_true; + + /** True node for predicates = false */ + Node d_false; + + Node mkAnd( std::vector< TNode >& assumptions ); + + void processAssertion( Node n, std::map< Node, bool >& visited ); + + public: + + TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + ~TheorySep(); + + void setMasterEqualityEngine(eq::EqualityEngine* eq); + + std::string identify() const { return std::string("TheorySep"); } + + ///////////////////////////////////////////////////////////////////////////// + // PREPROCESSING + ///////////////////////////////////////////////////////////////////////////// + + public: + + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + Node ppRewrite(TNode atom); + + void processAssertions( std::vector< Node >& assertions ); + ///////////////////////////////////////////////////////////////////////////// + // T-PROPAGATION / REGISTRATION + ///////////////////////////////////////////////////////////////////////////// + + private: + + /** Should be called to propagate the literal. */ + bool propagate(TNode literal); + + /** Explain why this literal is true by adding assumptions */ + void explain(TNode literal, std::vector<TNode>& assumptions); + + void preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ); + public: + + void preRegisterTerm(TNode t); + void propagate(Effort e); + Node explain(TNode n); + + public: + + void addSharedTerm(TNode t); + EqualityStatus getEqualityStatus(TNode a, TNode b); + void computeCareGraph(); + + ///////////////////////////////////////////////////////////////////////////// + // MODEL GENERATION + ///////////////////////////////////////////////////////////////////////////// + + public: + + void collectModelInfo(TheoryModel* m, bool fullModel); + + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// + + private: + public: + + Node getNextDecisionRequest(); + + void presolve(); + void shutdown() { } + + ///////////////////////////////////////////////////////////////////////////// + // MAIN SOLVER + ///////////////////////////////////////////////////////////////////////////// + public: + + void check(Effort e); + + private: + + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module + class NotifyClass : public eq::EqualityEngineNotify { + TheorySep& d_sep; + public: + NotifyClass(TheorySep& sep): d_sep(sep) {} + + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl; + // Just forward to sep + if (value) { + return d_sep.propagate(equality); + } else { + return d_sep.propagate(equality.notNode()); + } + } + + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Unreachable(); + } + + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + Debug("sep::propagate") << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) { + // Propagate equality between shared terms + return d_sep.propagate(t1.eqNode(t2)); + } else { + return d_sep.propagate(t1.eqNode(t2).notNode()); + } + return true; + } + + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + d_sep.conflict(t1, t2); + } + + void eqNotifyNewClass(TNode t) { } + void eqNotifyPreMerge(TNode t1, TNode t2) { d_sep.eqNotifyPreMerge( t1, t2 ); } + void eqNotifyPostMerge(TNode t1, TNode t2) { d_sep.eqNotifyPostMerge( t1, t2 ); } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + }; + + /** The notify class for d_equalityEngine */ + NotifyClass d_notify; + + /** Equaltity engine */ + eq::EqualityEngine d_equalityEngine; + + /** Are we in conflict? */ + context::CDO<bool> d_conflict; + std::vector< Node > d_pending_exp; + std::vector< Node > d_pending; + std::vector< int > d_pending_lem; + + /** list of all refinement lemms */ + std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem; + + /** Conflict when merging constants */ + void conflict(TNode a, TNode b); + + //cache for positive polarity start reduction + NodeSet d_reduce; + std::map< Node, std::map< Node, Node > > d_red_conc; + std::map< Node, std::map< Node, Node > > d_neg_guard; + std::vector< Node > d_neg_guards; + std::map< Node, Node > d_guard_to_assertion; + //cache for references + std::map< Node, std::map< int, TypeNode > > d_reference_type; + std::map< Node, std::map< int, int > > d_reference_type_card; + std::map< Node, std::map< int, std::vector< Node > > > d_references; + /** inferences: maintained to ensure ref count for internally introduced nodes */ + NodeList d_infer; + NodeList d_infer_exp; + NodeList d_spatial_assertions; + + //currently fix one data type for each location type, throw error if using more than one + std::map< TypeNode, TypeNode > d_loc_to_data_type; + //information about types + std::map< TypeNode, Node > d_base_label; + std::map< TypeNode, Node > d_nil_ref; + //reference bound + std::map< TypeNode, Node > d_reference_bound; + std::map< TypeNode, Node > d_reference_bound_max; + std::map< TypeNode, bool > d_reference_bound_invalid; + std::map< TypeNode, std::vector< Node > > d_type_references; + std::map< TypeNode, std::vector< Node > > d_type_references_all; + std::map< TypeNode, unsigned > d_card_max; + //bounds for labels + std::map< Node, std::vector< Node > > d_lbl_reference_bound; + //for empty argument + std::map< TypeNode, Node > d_emp_arg; + //map from ( atom, label, child index ) -> label + std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map; + std::map< Node, Node > d_label_map_parent; + + //term model + std::map< Node, Node > d_tmodel; + std::map< Node, Node > d_pto_model; + + class HeapAssertInfo { + public: + HeapAssertInfo( context::Context* c ); + ~HeapAssertInfo(){} + context::CDO< Node > d_pto; + context::CDO< bool > d_has_neg_pto; + }; + std::map< Node, HeapAssertInfo * > d_eqc_info; + HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false ); + + //calculate the element type of the heap for spatial assertions + TypeNode getReferenceType( Node atom, int& card, int index = -1 ); + TypeNode getReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited); + //get the base label for the spatial assertion + Node getBaseLabel( TypeNode tn ); + Node getNilRef( TypeNode tn ); + Node getLabel( Node atom, int child, Node lbl ); + Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ); + void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels ); + + class HeapInfo { + public: + HeapInfo() : d_computed(false) {} + //information about the model + bool d_computed; + std::vector< Node > d_heap_locs; + std::vector< Node > d_heap_locs_model; + //get value + Node getValue( TypeNode tn ); + }; + //heap info ( label -> HeapInfo ) + std::map< Node, HeapInfo > d_label_model; + + void debugPrintHeap( HeapInfo& heap, const char * c ); + void validatePto( HeapAssertInfo * ei, Node ei_n ); + void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ); + void mergePto( Node p1, Node p2 ); + void computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ); + Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model, std::map< Node, Node >& tmodel, + TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 ); + void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ); + + Node mkUnion( TypeNode tn, std::vector< Node >& locs ); +private: + Node getRepresentative( Node t ); + bool hasTerm( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); + void eqNotifyPreMerge(TNode t1, TNode t2); + void eqNotifyPostMerge(TNode t1, TNode t2); + + void sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer = false ); + void doPendingFacts(); +public: + eq::EqualityEngine* getEqualityEngine() { + return &d_equalityEngine; + } + +};/* class TheorySep */ + +}/* CVC4::theory::sep namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__SEP__THEORY_SEP_H */ |