A few more minor updates to match google repository with CVC4 repository

(mostly whitespace differences).

1 files changed, 255 insertions, 255 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 829b67777..d2a982781 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -1,255 +1,255 @@
-/*********************                                                        */

-/*! \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-2014  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"

-#include "theory/quantifiers/term_database.h"

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-class QuantConflictFind;

-class QuantInfo;

-

-//match generator

-class MatchGen {

-  friend class QuantInfo;

-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]]; }

-  //MatchGen * getChild( int i ) { return &d_children[i]; }

-  //current matching information

-  std::vector< TermArgTrie * > d_qn;

-  std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni;

-  bool doMatching( QuantConflictFind * p, QuantInfo * qi );

-  //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, TNode > d_qni_gterm;

-  std::map< int, TNode > d_qni_gterm_rep;

-  std::map< int, int > d_qni_bound;

-  std::vector< int > d_qni_bound_except;

-  std::map< int, TNode > d_qni_bound_cons;

-  std::map< int, int > d_qni_bound_cons_var;

-  std::map< int, int >::iterator d_binding_it;

-  //std::vector< int > d_independent;

-  bool d_matched_basis;

-  bool d_binding;

-  //int getVarBindingVar();

-  std::map< int, Node > d_ground_eval;

-  //determine variable order

-  void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars );

-  void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars );

-public:

-  //type of the match generator

-  enum {

-    typ_invalid,

-    typ_ground,

-    typ_pred,

-    typ_eq,

-    typ_formula,

-    typ_var,

-    typ_ite_var,

-    typ_bool_var,

-    typ_tconstraint,

-    typ_tsym,

-  };

-  void debugPrintType( const char * c, short typ, bool isTrace = false );

-public:

-  MatchGen() : d_type( typ_invalid ){}

-  MatchGen( QuantInfo * qi, Node n, bool isVar = false );

-  bool d_tgt;

-  bool d_tgt_orig;

-  bool d_wasSet;

-  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, QuantInfo * qi );

-  bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );

-  bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp );

-  Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp );

-  bool isValid() { return d_type!=typ_invalid; }

-  void setInvalid();

-

-  // is this term treated as UF application?

-  static bool isHandledBoolConnective( TNode n );

-  static bool isHandledUfTerm( TNode n );

-  static Node getOperator( QuantConflictFind * p, Node n );

-  //can this node be handled by the algorithm

-  static bool isHandled( TNode n );

-};

-

-//info for quantifiers

-class QuantInfo {

-private:

-  void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );

-  void flatten( Node n, bool beneathQuant );

-private: //for completing match

-  std::vector< int > d_unassigned;

-  std::vector< TypeNode > d_unassigned_tn;

-  int d_unassigned_nvar;

-  int d_una_index;

-  std::vector< int > d_una_eqc_count;

-public:

-  QuantInfo() : d_mg( NULL ) {}

-  ~QuantInfo() { delete d_mg; }

-  std::vector< TNode > d_vars;

-  std::vector< TypeNode > d_var_types;

-  std::map< TNode, int > d_var_num;

-  std::vector< int > d_tsym_vars;

-  std::map< TNode, bool > d_inMatchConstraint;

-  std::map< int, std::vector< Node > > d_var_constraint[2];

-  int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }

-  bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }

-  int getNumVars() { return (int)d_vars.size(); }

-  TNode getVar( int i ) { return d_vars[i]; }

-

-  MatchGen * d_mg;

-  Node d_q;

-  std::map< int, MatchGen * > d_var_mg;

-  void reset_round( QuantConflictFind * p );

-public:

-  //initialize

-  void initialize( Node q, Node qn );

-  //current constraints

-  std::vector< TNode > d_match;

-  std::vector< TNode > d_match_term;

-  std::map< int, std::map< TNode, int > > d_curr_var_deq;

-  std::map< Node, bool > d_tconstraints;

-  int getCurrentRepVar( int v );

-  TNode getCurrentValue( TNode n );

-  TNode getCurrentExpValue( TNode n );

-  bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );

-  int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );

-  int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );

-  bool setMatch( QuantConflictFind * p, int v, TNode n );

-  bool isMatchSpurious( QuantConflictFind * p );

-  bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );

-  bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );

-  bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );

-  void revertMatch( std::vector< int >& assigned );

-  void debugPrintMatch( const char * c );

-  bool isConstrainedVar( int v );

-public:

-  void getMatch( std::vector< Node >& terms );

-};

-

-class QuantConflictFind : public QuantifiersModule

-{

-  friend class MatchGen;

-  friend class QuantInfo;

-  typedef context::CDChunkList<Node> NodeList;

-  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;

-private:

-  context::CDO< bool > d_conflict;

-  std::vector< Node > d_quant_order;

-  std::map< Kind, Node > d_zero;

-  //for storing nodes created during t-constraint solving (prevents memory leaks)

-  std::vector< Node > d_tempCache;

-private:

-  std::map< Node, Node > d_op_node;

-  int d_fid_count;

-  std::map< Node, int > d_fid;

-  Node mkEqNode( Node a, Node b );

-public:  //for ground terms

-  Node d_true;

-  Node d_false;

-  TNode getZero( Kind k );

-private:

-  Node evaluateTerm( Node n );

-  int evaluate( Node n, bool pref = false, bool hasPref = false );

-private:

-  //currently asserted quantifiers

-  NodeList d_qassert;

-  std::map< Node, QuantInfo > d_qinfo;

-private:  //for equivalence classes

-  // type -> list(eqc)

-  std::map< TypeNode, std::vector< TNode > > d_eqcs;

-  std::map< TypeNode, Node > d_model_basis;

-public:

-  enum {

-    effort_conflict,

-    effort_prop_eq,

-    effort_mc,

-  };

-  short d_effort;

-  void setEffort( int e ) { d_effort = e; }

-  static short getMaxQcfEffort();

-  bool areMatchEqual( TNode n1, TNode n2 );

-  bool areMatchDisequal( TNode n1, TNode n2 );

-public:

-  QuantConflictFind( QuantifiersEngine * qe, context::Context* c );

-  ~QuantConflictFind() throw() {}

-  /** 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 );

-  /** needs check */

-  bool needsCheck( Theory::Effort level );

-  /** reset round */

-  void reset_round( Theory::Effort level );

-  /** check */

-  void check( Theory::Effort level, unsigned quant_e );

-private:

-  bool d_needs_computeRelEqr;

-public:

-  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 );

-public:

-  /** statistics class */

-  class Statistics {

-  public:

-    IntStat d_inst_rounds;

-    IntStat d_conflict_inst;

-    IntStat d_prop_inst;

-    IntStat d_entailment_checks;

-    Statistics();

-    ~Statistics();

-  };

-  Statistics d_statistics;

-  /** Identify this module */

-  std::string identify() const { return "QcfEngine"; }

-};

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \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-2014  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"
+#include "theory/quantifiers/term_database.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantConflictFind;
+class QuantInfo;
+
+//match generator
+class MatchGen {
+  friend class QuantInfo;
+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]]; }
+  //MatchGen * getChild( int i ) { return &d_children[i]; }
+  //current matching information
+  std::vector< TermArgTrie * > d_qn;
+  std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni;
+  bool doMatching( QuantConflictFind * p, QuantInfo * qi );
+  //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, TNode > d_qni_gterm;
+  std::map< int, TNode > d_qni_gterm_rep;
+  std::map< int, int > d_qni_bound;
+  std::vector< int > d_qni_bound_except;
+  std::map< int, TNode > d_qni_bound_cons;
+  std::map< int, int > d_qni_bound_cons_var;
+  std::map< int, int >::iterator d_binding_it;
+  //std::vector< int > d_independent;
+  bool d_matched_basis;
+  bool d_binding;
+  //int getVarBindingVar();
+  std::map< int, Node > d_ground_eval;
+  //determine variable order
+  void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars );
+  void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars );
+public:
+  //type of the match generator
+  enum {
+    typ_invalid,
+    typ_ground,
+    typ_pred,
+    typ_eq,
+    typ_formula,
+    typ_var,
+    typ_ite_var,
+    typ_bool_var,
+    typ_tconstraint,
+    typ_tsym,
+  };
+  void debugPrintType( const char * c, short typ, bool isTrace = false );
+public:
+  MatchGen() : d_type( typ_invalid ){}
+  MatchGen( QuantInfo * qi, Node n, bool isVar = false );
+  bool d_tgt;
+  bool d_tgt_orig;
+  bool d_wasSet;
+  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, QuantInfo * qi );
+  bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
+  bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp );
+  Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp );
+  bool isValid() { return d_type!=typ_invalid; }
+  void setInvalid();
+
+  // is this term treated as UF application?
+  static bool isHandledBoolConnective( TNode n );
+  static bool isHandledUfTerm( TNode n );
+  static Node getOperator( QuantConflictFind * p, Node n );
+  //can this node be handled by the algorithm
+  static bool isHandled( TNode n );
+};
+
+//info for quantifiers
+class QuantInfo {
+private:
+  void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );
+  void flatten( Node n, bool beneathQuant );
+private: //for completing match
+  std::vector< int > d_unassigned;
+  std::vector< TypeNode > d_unassigned_tn;
+  int d_unassigned_nvar;
+  int d_una_index;
+  std::vector< int > d_una_eqc_count;
+public:
+  QuantInfo() : d_mg( NULL ) {}
+  ~QuantInfo() { delete d_mg; }
+  std::vector< TNode > d_vars;
+  std::vector< TypeNode > d_var_types;
+  std::map< TNode, int > d_var_num;
+  std::vector< int > d_tsym_vars;
+  std::map< TNode, bool > d_inMatchConstraint;
+  std::map< int, std::vector< Node > > d_var_constraint[2];
+  int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
+  bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }
+  int getNumVars() { return (int)d_vars.size(); }
+  TNode getVar( int i ) { return d_vars[i]; }
+
+  MatchGen * d_mg;
+  Node d_q;
+  std::map< int, MatchGen * > d_var_mg;
+  void reset_round( QuantConflictFind * p );
+public:
+  //initialize
+  void initialize( Node q, Node qn );
+  //current constraints
+  std::vector< TNode > d_match;
+  std::vector< TNode > d_match_term;
+  std::map< int, std::map< TNode, int > > d_curr_var_deq;
+  std::map< Node, bool > d_tconstraints;
+  int getCurrentRepVar( int v );
+  TNode getCurrentValue( TNode n );
+  TNode getCurrentExpValue( TNode n );
+  bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );
+  int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );
+  int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );
+  bool setMatch( QuantConflictFind * p, int v, TNode n );
+  bool isMatchSpurious( QuantConflictFind * p );
+  bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
+  bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
+  bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
+  void revertMatch( std::vector< int >& assigned );
+  void debugPrintMatch( const char * c );
+  bool isConstrainedVar( int v );
+public:
+  void getMatch( std::vector< Node >& terms );
+};
+
+class QuantConflictFind : public QuantifiersModule
+{
+  friend class MatchGen;
+  friend class QuantInfo;
+  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+private:
+  context::CDO< bool > d_conflict;
+  std::vector< Node > d_quant_order;
+  std::map< Kind, Node > d_zero;
+  //for storing nodes created during t-constraint solving (prevents memory leaks)
+  std::vector< Node > d_tempCache;
+private:
+  std::map< Node, Node > d_op_node;
+  int d_fid_count;
+  std::map< Node, int > d_fid;
+  Node mkEqNode( Node a, Node b );
+public:  //for ground terms
+  Node d_true;
+  Node d_false;
+  TNode getZero( Kind k );
+private:
+  Node evaluateTerm( Node n );
+  int evaluate( Node n, bool pref = false, bool hasPref = false );
+private:
+  //currently asserted quantifiers
+  NodeList d_qassert;
+  std::map< Node, QuantInfo > d_qinfo;
+private:  //for equivalence classes
+  // type -> list(eqc)
+  std::map< TypeNode, std::vector< TNode > > d_eqcs;
+  std::map< TypeNode, Node > d_model_basis;
+public:
+  enum {
+    effort_conflict,
+    effort_prop_eq,
+    effort_mc,
+  };
+  short d_effort;
+  void setEffort( int e ) { d_effort = e; }
+  static short getMaxQcfEffort();
+  bool areMatchEqual( TNode n1, TNode n2 );
+  bool areMatchDisequal( TNode n1, TNode n2 );
+public:
+  QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
+  ~QuantConflictFind() throw() {}
+  /** 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 );
+  /** needs check */
+  bool needsCheck( Theory::Effort level );
+  /** reset round */
+  void reset_round( Theory::Effort level );
+  /** check */
+  void check( Theory::Effort level, unsigned quant_e );
+private:
+  bool d_needs_computeRelEqr;
+public:
+  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 );
+public:
+  /** statistics class */
+  class Statistics {
+  public:
+    IntStat d_inst_rounds;
+    IntStat d_conflict_inst;
+    IntStat d_prop_inst;
+    IntStat d_entailment_checks;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
+  /** Identify this module */
+  std::string identify() const { return "QcfEngine"; }
+};
+
+}
+}
+}
+
+#endif