fixed files with DOS newlines; fixed contrib/ scripts to use git

1 files changed, 109 insertions, 109 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 3ee423fe7..de548ab14 100755..100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -1,110 +1,110 @@
-/*********************                                                        */

-/*! \file inst_strategy_cbqi.h

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: none

- ** Minor contributors (to current version): mdeters

- ** This file is part of the CVC4 prototype.

- ** Copyright (c) 2009-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief instantiator_arith_instantiator

- **/

-

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__INST_STRATEGT_CBQI_H

-#define __CVC4__INST_STRATEGT_CBQI_H

-

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

-#include "theory/arith/arithvar_node_map.h"

-

-#include "util/statistics_registry.h"

-

-namespace CVC4 {

-namespace theory {

-

-namespace arith {

-  class TheoryArith;

-}

-

-namespace datatypes {

-  class TheoryDatatypes;

-}

-

-namespace quantifiers {

-

-

-class InstStrategySimplex : public InstStrategy{

-protected:

-  /** calculate if we should process this quantifier */

-  bool calculateShouldProcess( Node f );

-private:

-  /** reference to theory arithmetic */

-  arith::TheoryArith* d_th;

-  /** delta */

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

-  /** for each quantifier, simplex rows */

-  std::map< Node, std::vector< arith::ArithVar > > d_instRows;

-  /** tableaux */

-  std::map< arith::ArithVar, Node > d_tableaux_term;

-  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;

-  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;

-  /** ce tableaux */

-  std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;

-  /** get value */

-  Node getTableauxValue( Node n, bool minus_delta = false );

-  Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );

-  /** do instantiation */

-  bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );

-  bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );

-  /** add term to row */

-  void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );

-  /** print debug */

-  void debugPrint( const char* c );

-private:

-  /** */

-  int d_counter;

-  /** negative one */

-  Node d_negOne;

-  /** process functions */

-  void processResetInstantiationRound( Theory::Effort effort );

-  int process( Node f, Theory::Effort effort, int e );

-public:

-  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );

-  ~InstStrategySimplex(){}

-  /** identify */

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

-};

-

-

-class InstStrategyDatatypesValue : public InstStrategy

-{

-protected:

-  /** calculate if we should process this quantifier */

-  bool calculateShouldProcess( Node f );

-private:

-  /** reference to theory datatypes */

-  datatypes::TheoryDatatypes* d_th;

-  /** get value function */

-  Node getValueFor( Node n );

-public:

-  //constructor

-  InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );

-  ~InstStrategyDatatypesValue(){}

-  /** reset instantiation */

-  void processResetInstantiationRound( Theory::Effort effort );

-  /** process method, returns a status */

-  int process( Node f, Theory::Effort effort, int e );

-  /** identify */

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

-

-};/* class InstStrategy */

-

-}

-}

-}

-

+/*********************                                                        */
+/*! \file inst_strategy_cbqi.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds <andrew.j.reynolds@gmail.com>
+ ** Major contributors: Morgan Deters <mdeters@cs.nyu.edu>
+ ** 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 instantiator_arith_instantiator
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INST_STRATEGT_CBQI_H
+#define __CVC4__INST_STRATEGT_CBQI_H
+
+#include "theory/quantifiers/instantiation_engine.h"
+#include "theory/arith/arithvar_node_map.h"
+
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace arith {
+  class TheoryArith;
+}
+
+namespace datatypes {
+  class TheoryDatatypes;
+}
+
+namespace quantifiers {
+
+
+class InstStrategySimplex : public InstStrategy{
+protected:
+  /** calculate if we should process this quantifier */
+  bool calculateShouldProcess( Node f );
+private:
+  /** reference to theory arithmetic */
+  arith::TheoryArith* d_th;
+  /** delta */
+  std::map< TypeNode, Node > d_deltas;
+  /** for each quantifier, simplex rows */
+  std::map< Node, std::vector< arith::ArithVar > > d_instRows;
+  /** tableaux */
+  std::map< arith::ArithVar, Node > d_tableaux_term;
+  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
+  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;
+  /** ce tableaux */
+  std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;
+  /** get value */
+  Node getTableauxValue( Node n, bool minus_delta = false );
+  Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );
+  /** do instantiation */
+  bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );
+  bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
+  /** add term to row */
+  void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );
+  /** print debug */
+  void debugPrint( const char* c );
+private:
+  /** */
+  int d_counter;
+  /** negative one */
+  Node d_negOne;
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e );
+public:
+  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
+  ~InstStrategySimplex(){}
+  /** identify */
+  std::string identify() const { return std::string("Simplex"); }
+};
+
+
+class InstStrategyDatatypesValue : public InstStrategy
+{
+protected:
+  /** calculate if we should process this quantifier */
+  bool calculateShouldProcess( Node f );
+private:
+  /** reference to theory datatypes */
+  datatypes::TheoryDatatypes* d_th;
+  /** get value function */
+  Node getValueFor( Node n );
+public:
+  //constructor
+  InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );
+  ~InstStrategyDatatypesValue(){}
+  /** reset instantiation */
+  void processResetInstantiationRound( Theory::Effort effort );
+  /** process method, returns a status */
+  int process( Node f, Theory::Effort effort, int e );
+  /** identify */
+  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
+
+};/* class InstStrategy */
+
+}
+}
+}
+
 #endif
\ No newline at end of file