diff options
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.h')
| -rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.h | 235 |
1 files changed, 235 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h new file mode 100755 index 000000000..a43e2f70d --- /dev/null +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -0,0 +1,235 @@ +/********************* */
+/*! \file quant_conflict_find.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief quantifiers conflict find class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef QUANT_CONFLICT_FIND
+#define QUANT_CONFLICT_FIND
+
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QcfNode;
+
+class QuantConflictFind;
+
+class QcfNodeIndex {
+public:
+ std::map< Node, QcfNodeIndex > d_children;
+ void clear() { d_children.clear(); }
+ Node addTerm( QuantConflictFind * qcf, Node n, bool doAdd = true, int index = 0 );
+ bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 );
+ void debugPrint( const char * c, int t );
+};
+
+class EqRegistry {
+ typedef context::CDChunkList<Node> NodeList;
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+public:
+ EqRegistry( context::Context* c );
+ //active
+ context::CDO< bool > d_active;
+ //NodeIndex describing pairs that meet the criteria of the EqRegistry
+ QcfNodeIndex d_qni;
+
+ //qcf nodes that this helps to 1:satisfy -1:falsify 0:both a quantifier conflict node
+ //std::map< QcfNode *, int > d_qcf;
+ //has eqc
+ //bool hasEqc( Node n ) { return d_t_eqc.find( n )!=d_t_eqc.end() && d_t_eqc[n]; }
+ //void setEqc( Node n, bool val = true ) { d_t_eqc[n] = val; }
+ void clear() { d_qni.clear(); }
+ void debugPrint( const char * c, int t );
+};
+
+/*
+class QcfNode {
+public:
+ QcfNode( context::Context* c );
+ QcfNode * d_parent;
+ std::map< int, QcfNode * > d_child;
+ Node d_node;
+ EqRegistry * d_reg[2];
+};
+*/
+
+class QuantConflictFind : public QuantifiersModule
+{
+ friend class QcfNodeIndex;
+ typedef context::CDChunkList<Node> NodeList;
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+private:
+ context::Context* d_c;
+ context::CDO< bool > d_conflict;
+ //void registerAssertion( Node n );
+ void registerQuant( Node q, Node n, bool hasPol, bool pol );
+ void flatten( Node q, Node n );
+private:
+ std::map< TypeNode, Node > d_fv;
+ Node getFv( TypeNode tn );
+ std::map< Node, Node > d_op_node;
+ int getFunctionId( Node f );
+ bool isLessThan( Node a, Node b );
+ Node getFunction( Node n, bool isQuant = false );
+ int d_fid_count;
+ std::map< Node, int > d_fid;
+ Node mkEqNode( Node a, Node b );
+private: //for ground terms
+ Node d_true;
+ Node d_false;
+ std::map< Node, std::map< Node, EqRegistry * > > d_eqr[2];
+ EqRegistry * getEqRegistry( bool polarity, Node lit, bool doCreate = true );
+ void getEqRegistryApps( Node lit, std::vector< Node >& terms );
+ int evaluate( Node n );
+public: //for quantifiers
+ //match generator
+ class MatchGen {
+ private:
+ //current children information
+ int d_child_counter;
+ //children of this object
+ std::vector< int > d_children_order;
+ unsigned getNumChildren() { return d_children.size(); }
+ MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
+ //current matching information
+ std::vector< QcfNodeIndex * > d_qn;
+ std::vector< std::map< Node, QcfNodeIndex >::iterator > d_qni;
+ bool doMatching( QuantConflictFind * p, Node q );
+ //for matching : each index is either a variable or a ground term
+ unsigned d_qni_size;
+ std::map< int, int > d_qni_var_num;
+ std::map< int, Node > d_qni_gterm;
+ std::map< int, Node > d_qni_gterm_rep;
+ std::map< int, int > d_qni_bound;
+ std::map< int, Node > d_qni_bound_cons;
+ public:
+ //type of the match generator
+ enum {
+ typ_invalid,
+ typ_ground,
+ typ_var_eq,
+ typ_valid_lit,
+ typ_valid,
+ typ_var,
+ typ_top,
+ };
+ void debugPrintType( const char * c, short typ, bool isTrace = false );
+ public:
+ MatchGen() : d_type( typ_invalid ){}
+ MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop = false, bool isVar = false );
+ bool d_tgt;
+ Node d_n;
+ std::vector< MatchGen > d_children;
+ short d_type;
+ bool d_type_not;
+ void reset_round( QuantConflictFind * p );
+ void reset( QuantConflictFind * p, bool tgt, Node q );
+ bool getNextMatch( QuantConflictFind * p, Node q );
+ bool isValid() { return d_type!=typ_invalid; }
+ };
+private:
+ //currently asserted quantifiers
+ NodeList d_qassert;
+ //info for quantifiers
+ class QuantInfo {
+ public:
+ QuantInfo() : d_mg( NULL ) {}
+ std::vector< Node > d_vars;
+ std::map< Node, int > d_var_num;
+ std::map< EqRegistry *, bool > d_rel_eqr;
+ std::map< int, std::vector< Node > > d_var_constraint[2];
+ int getVarNum( Node v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
+ bool isVar( Node v ) { return d_var_num.find( v )!=d_var_num.end(); }
+ int getNumVars() { return (int)d_vars.size(); }
+ Node getVar( int i ) { return d_vars[i]; }
+ MatchGen * d_mg;
+ void reset_round( QuantConflictFind * p );
+ public:
+ //current constraints
+ std::map< int, Node > d_match;
+ std::map< int, std::map< Node, int > > d_curr_var_deq;
+ int getCurrentRepVar( int v );
+ Node getCurrentValue( Node n );
+ bool getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n );
+ int addConstraint( QuantConflictFind * p, int v, Node n, bool polarity );
+ int addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove );
+ bool setMatch( QuantConflictFind * p, int v, Node n );
+ bool isMatchSpurious( QuantConflictFind * p );
+ void debugPrintMatch( const char * c );
+ };
+ std::map< Node, QuantInfo > d_qinfo;
+private: //for equivalence classes
+ eq::EqualityEngine * getEqualityEngine();
+ bool areDisequal( Node n1, Node n2 );
+ bool areEqual( Node n1, Node n2 );
+ Node getRepresentative( Node n );
+ Node getTerm( Node n );
+
+ class EqcInfo {
+ public:
+ EqcInfo( context::Context* c ) : d_diseq( c ) {}
+ NodeBoolMap d_diseq;
+ bool isDisequal( Node n ) { return d_diseq.find( n )!=d_diseq.end() && d_diseq[n]; }
+ void setDisequal( Node n, bool val = true ) { d_diseq[n] = val; }
+ //NodeBoolMap& getRelEqr( int index ) { return index==0 ? d_rel_eqr_e : d_rel_eqr_d; }
+ };
+ std::map< Node, EqcInfo * > d_eqc_info;
+ EqcInfo * getEqcInfo( Node n, bool doCreate = true );
+ // operator -> index(terms)
+ std::map< Node, QcfNodeIndex > d_uf_terms;
+ // eqc x operator -> index(terms)
+ std::map< Node, std::map< Node, QcfNodeIndex > > d_eqc_uf_terms;
+ // type -> list(eqc)
+ std::map< TypeNode, std::vector< Node > > d_eqcs;
+public:
+ QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
+
+ /** register assertions */
+ //void registerAssertions( std::vector< Node >& assertions );
+ /** register quantifier */
+ void registerQuantifier( Node q );
+
+public:
+ /** assert quantifier */
+ void assertNode( Node q );
+ /** new node */
+ void newEqClass( Node n );
+ /** merge */
+ void merge( Node a, Node b );
+ /** assert disequal */
+ void assertDisequal( Node a, Node b );
+ /** check */
+ void check( Theory::Effort level );
+ /** needs check */
+ bool needsCheck( Theory::Effort level );
+private:
+ void computeRelevantEqr();
+private:
+ void debugPrint( const char * c );
+ //for debugging
+ std::vector< Node > d_quants;
+ std::map< Node, int > d_quant_id;
+ void debugPrintQuant( const char * c, Node q );
+ void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true );
+};
+
+}
+}
+}
+
+#endif
|