dos2unix-convert some sources.

1 files changed, 102 insertions, 102 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 349073cb4..d586d9c8f 100755
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -1,102 +1,102 @@
-/*********************                                                        */

-/*! \file ambqi_builder.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 Abstract MBQI model builder class

- **/

-

-#include "cvc4_private.h"

-

-#ifndef ABSTRACT_MBQI_BUILDER

-#define ABSTRACT_MBQI_BUILDER

-

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

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

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-class FirstOrderModelAbs;

-

-//representiation of function and term interpretations

-class AbsDef

-{

-private:

-  bool addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth );

-  void construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,

-                          std::map< unsigned, AbsDef * >& children,

-                          std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,

-                          std::vector< unsigned >& entry, std::vector< bool >& entry_def );

-  void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );

-  void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );

-  void apply_ucompose( FirstOrderModelAbs * m, TNode q,

-                       std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,

-                       std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );

-  void construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 );

-  void construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth = 0 );

-  void get_defs( unsigned u, std::vector< AbsDef * >& defs );

-  void construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth = 0 );

-public:

-  enum {

-    val_none = -1,

-    val_unk = -2,

-  };

-  AbsDef() : d_default( 0 ), d_value( -1 ){}

-  std::map< unsigned, AbsDef > d_def;

-  unsigned d_default;

-  int d_value;

-

-  void clear() { d_def.clear(); d_default = 0; d_value = -1; }

-  AbsDef * getDefault() { return &d_def[d_default]; }

-  void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );

-  void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;

-  void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;

-  void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );

-  int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){

-    std::vector< Node > terms;

-    terms.resize( q[0].getNumChildren() );

-    return addInstantiations( m, qe, q, terms, inst, 0 );

-  }

-  bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,

-                  std::map< unsigned, AbsDef * >& children,

-                  std::map< unsigned, int >& bchildren,

-                  std::map< unsigned, int >& vchildren,

-                  int varChCount );

-  void negate();

-  Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );

-  static bool isSimple( unsigned n );

-  static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );

-  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );

-  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );

-  //for debugging

-  bool is_normalized();

-};

-

-class AbsMbqiBuilder : public QModelBuilder

-{

-  friend class AbsDef;

-private:

-  Node d_true;

-  Node d_false;

-  bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );

-public:

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

-  //process build model

-  void processBuildModel(TheoryModel* m, bool fullModel);

-  //do exhaustive instantiation

-  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );

-};

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file ambqi_builder.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 Abstract MBQI model builder class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef ABSTRACT_MBQI_BUILDER
+#define ABSTRACT_MBQI_BUILDER
+
+#include "theory/quantifiers/model_builder.h"
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class FirstOrderModelAbs;
+
+//representiation of function and term interpretations
+class AbsDef
+{
+private:
+  bool addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth );
+  void construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
+                          std::map< unsigned, AbsDef * >& children,
+                          std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
+                          std::vector< unsigned >& entry, std::vector< bool >& entry_def );
+  void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );
+  void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );
+  void apply_ucompose( FirstOrderModelAbs * m, TNode q,
+                       std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,
+                       std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );
+  void construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 );
+  void construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth = 0 );
+  void get_defs( unsigned u, std::vector< AbsDef * >& defs );
+  void construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth = 0 );
+public:
+  enum {
+    val_none = -1,
+    val_unk = -2,
+  };
+  AbsDef() : d_default( 0 ), d_value( -1 ){}
+  std::map< unsigned, AbsDef > d_def;
+  unsigned d_default;
+  int d_value;
+
+  void clear() { d_def.clear(); d_default = 0; d_value = -1; }
+  AbsDef * getDefault() { return &d_def[d_default]; }
+  void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );
+  void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;
+  void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;
+  void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );
+  int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
+    std::vector< Node > terms;
+    terms.resize( q[0].getNumChildren() );
+    return addInstantiations( m, qe, q, terms, inst, 0 );
+  }
+  bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
+                  std::map< unsigned, AbsDef * >& children,
+                  std::map< unsigned, int >& bchildren,
+                  std::map< unsigned, int >& vchildren,
+                  int varChCount );
+  void negate();
+  Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
+  static bool isSimple( unsigned n );
+  static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );
+  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
+  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
+  //for debugging
+  bool is_normalized();
+};
+
+class AbsMbqiBuilder : public QModelBuilder
+{
+  friend class AbsDef;
+private:
+  Node d_true;
+  Node d_false;
+  bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
+public:
+  AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
+  //process build model
+  void processBuildModel(TheoryModel* m, bool fullModel);
+  //do exhaustive instantiation
+  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+};
+
+}
+}
+}
+
+#endif