diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-27 22:01:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-27 22:01:03 +0000 |
commit | 485c03a323911142e460bd0a7c428759496dc631 (patch) | |
tree | 8c512712734dd2862c89acd8681357d0a2e0dabe /src/theory/arrays | |
parent | 33fd76601b42599d9883889a03d59d0d85729661 (diff) |
Minor cleanup after today's commits:
* change some uses of "std::cout" to "Message()"
* change some files to use Unix newlines instead of DOS newlines
* fix compiler warning
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays_model.cpp | 140 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_model.h | 122 |
2 files changed, 131 insertions, 131 deletions
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp index 49da2f851..7a574fac1 100644 --- a/src/theory/arrays/theory_arrays_model.cpp +++ b/src/theory/arrays/theory_arrays_model.cpp @@ -1,70 +1,70 @@ -/********************* */
-/*! \file theory_arrays_model.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_arrays_model class
- **/
-
-#include "theory/theory_engine.h"
-#include "theory/arrays/theory_arrays_model.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-
-ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){
- Assert( arr.getKind()!=STORE );
- //look at ground assertions
- Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) );
- Node sel_op = sel.getOperator(); //FIXME: easier way to do this?
- for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){
- Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];
- Assert( n.getKind()==SELECT );
- if( m->areEqual( n[0], arr ) ){
- //d_model->getTermDatabase()->computeModelBasisArgAttribute( n );
- //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
- Node r = d_model->getRepresentative( n );
- Node i = d_model->getRepresentative( n[1] );
- d_values[i] = r;
- //}
- }
- }
-}
-
-Node ArrayModel::getValue( Node n ){
- Assert( n.getKind()==SELECT );
- Assert( n[0]==d_arr );
- std::map< Node, Node >::iterator it = d_values.find( n[0] );
- if( it!=d_values.end() ){
- return it->second;
- }else{
- return n;
- //return d_default_value; TODO: guarentee I can return this here
- }
-}
-
-void ArrayModel::setDefaultValue( Node v ){
- d_default_value = v;
-}
-
-Node ArrayModel::getArrayValue(){
- Node curr = d_arr; //TODO: make constant default
- for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){
- curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );
- }
- return curr;
-}
+/********************* */ +/*! \file theory_arrays_model.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory_arrays_model class + **/ + +#include "theory/theory_engine.h" +#include "theory/arrays/theory_arrays_model.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::arrays; + +ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){ + Assert( arr.getKind()!=STORE ); + //look at ground assertions + Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) ); + Node sel_op = sel.getOperator(); //FIXME: easier way to do this? + for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){ + Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i]; + Assert( n.getKind()==SELECT ); + if( m->areEqual( n[0], arr ) ){ + //d_model->getTermDatabase()->computeModelBasisArgAttribute( n ); + //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ + Node r = d_model->getRepresentative( n ); + Node i = d_model->getRepresentative( n[1] ); + d_values[i] = r; + //} + } + } +} + +Node ArrayModel::getValue( Node n ){ + Assert( n.getKind()==SELECT ); + Assert( n[0]==d_arr ); + std::map< Node, Node >::iterator it = d_values.find( n[0] ); + if( it!=d_values.end() ){ + return it->second; + }else{ + return n; + //return d_default_value; TODO: guarentee I can return this here + } +} + +void ArrayModel::setDefaultValue( Node v ){ + d_default_value = v; +} + +Node ArrayModel::getArrayValue(){ + Node curr = d_arr; //TODO: make constant default + for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){ + curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second ); + } + return curr; +} diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h index 3895388e3..28852296d 100644 --- a/src/theory/arrays/theory_arrays_model.h +++ b/src/theory/arrays/theory_arrays_model.h @@ -1,62 +1,62 @@ -/********************* */
-/*! \file theory_arrays_model.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief MODEL for theory of arrays
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY_ARRAYS_MODEL_H
-#define __CVC4__THEORY_ARRAYS_MODEL_H
-
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-
-namespace quantifiers{
- class FirstOrderModel;
-}
-
-namespace arrays {
-
-class ArrayModel{
-protected:
- /** reference to model */
- quantifiers::FirstOrderModel* d_model;
- /** the array this model is for */
- Node d_arr;
-public:
- ArrayModel(){}
- ArrayModel( Node arr, quantifiers::FirstOrderModel* m );
- ~ArrayModel() {}
-public:
- /** pre-defined values */
- std::map< Node, Node > d_values;
- /** default value */
- Node d_default_value;
- /** get value, return arguments that the value depends on */
- Node getValue( Node n );
- /** set default */
- void setDefaultValue( Node v );
-public:
- /** get array value */
- Node getArrayValue();
-};/* class ArrayModel */
-
-}
-}
-}
-
+/********************* */ +/*! \file theory_arrays_model.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief MODEL for theory of arrays + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_ARRAYS_MODEL_H +#define __CVC4__THEORY_ARRAYS_MODEL_H + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { + +namespace quantifiers{ + class FirstOrderModel; +} + +namespace arrays { + +class ArrayModel{ +protected: + /** reference to model */ + quantifiers::FirstOrderModel* d_model; + /** the array this model is for */ + Node d_arr; +public: + ArrayModel(){} + ArrayModel( Node arr, quantifiers::FirstOrderModel* m ); + ~ArrayModel() {} +public: + /** pre-defined values */ + std::map< Node, Node > d_values; + /** default value */ + Node d_default_value; + /** get value, return arguments that the value depends on */ + Node getValue( Node n ); + /** set default */ + void setDefaultValue( Node v ); +public: + /** get array value */ + Node getArrayValue(); +};/* class ArrayModel */ + +} +} +} + #endif
\ No newline at end of file |