diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-23 16:45:47 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-23 16:45:47 -0500 |
commit | fbc81b67ac1cfeb3afe37f3299180177faaa1ca6 (patch) | |
tree | 69b3028b333262b414ed188d1f575012793e0e2b /src/theory/arrays | |
parent | fee510eacd6ea9d35906218ce3d4b88f7d86f8b1 (diff) |
Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 9 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_model.cpp | 65 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_model.h | 58 |
4 files changed, 5 insertions, 131 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index ec834522f..77f102cf8 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -16,9 +16,7 @@ libarrays_la_SOURCES = \ array_info.h \ array_info.cpp \ static_fact_manager.h \ - static_fact_manager.cpp \ - theory_arrays_model.h \ - theory_arrays_model.cpp + static_fact_manager.cpp EXTRA_DIST = \ kinds diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 89f1dbf2c..98346d0e3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -21,7 +21,6 @@ #include <map> #include "theory/rewriter.h" #include "expr/command.h" -#include "theory/arrays/theory_arrays_model.h" #include "theory/model.h" #include "theory/arrays/options.h" #include "smt/logic_exception.h" @@ -495,7 +494,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node) } case kind::STORE_ALL: { throw LogicException("Array theory solver does not yet support assertions using constant array value"); - } + } default: // Variables etc if (node.getType().isArray()) { @@ -1082,7 +1081,7 @@ void TheoryArrays::checkModel(Effort e) if (constraintIdx == d_modelConstraints.size()) { break; } - + if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) { assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false); if (assertionToCheck.getKind() == kind::AND && @@ -1429,7 +1428,7 @@ Node TheoryArrays::getModelValRec(TNode node) } ++d_numGetModelValConflicts; getSatContext()->pop(); - } + } ++te; if (te.isFinished()) { Assert(false); @@ -1466,7 +1465,7 @@ bool TheoryArrays::hasLoop(TNode node, TNode target) return true; } } - + return false; } diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp deleted file mode 100644 index b5c81ef69..000000000 --- a/src/theory/arrays/theory_arrays_model.cpp +++ /dev/null @@ -1,65 +0,0 @@ -/********************* */ -/*! \file theory_arrays_model.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** 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 Implementation of theory_arrays_model class - **/ - -#include "theory/theory_engine.h" -#include "theory/arrays/theory_arrays_model.h" -#include "theory/model.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, TheoryModel* m ) : d_arr( arr ){ - d_base_arr = arr; - while( d_base_arr.getKind()==STORE ){ - Node ri = m->getRepresentative( d_base_arr[1] ); - if( d_values.find( ri )==d_values.end() ){ - d_values[ ri ] = m->getRepresentative( d_base_arr[2] ); - } - d_base_arr = d_base_arr[0]; - } -} - -Node ArrayModel::getValue( TheoryModel* m, Node i ){ - i = m->getRepresentative( i ); - std::map< Node, Node >::iterator it = d_values.find( i ); - if( it!=d_values.end() ){ - return it->second; - }else{ - return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i ); - //return d_default_value; //TODO: guarantee I can return this here - } -} - -void ArrayModel::setValue( TheoryModel* m, Node i, Node e ){ - Node ri = m->getRepresentative( i ); - if( d_values.find( ri )==d_values.end() ){ - d_values[ ri ] = m->getRepresentative( e ); - } -} - -void ArrayModel::setDefaultArray( Node arr ){ - d_base_arr = arr; -} - -Node ArrayModel::getArrayValue(){ - Node curr = d_base_arr; - 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 deleted file mode 100644 index 66dc80568..000000000 --- a/src/theory/arrays/theory_arrays_model.h +++ /dev/null @@ -1,58 +0,0 @@ -/********************* */ -/*! \file theory_arrays_model.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** 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 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 { - -class TheoryModel; - -namespace arrays { - -class ArrayModel{ -protected: - /** the array this model is for */ - Node d_arr; -public: - ArrayModel(){} - ArrayModel( Node arr, TheoryModel* m ); - ~ArrayModel() {} -public: - /** pre-defined values */ - std::map< Node, Node > d_values; - /** base array */ - Node d_base_arr; - /** get value, return arguments that the value depends on */ - Node getValue( TheoryModel* m, Node i ); - /** set value */ - void setValue( TheoryModel* m, Node i, Node e ); - /** set default */ - void setDefaultArray( Node arr ); -public: - /** get array value */ - Node getArrayValue(); -};/* class ArrayModel */ - -} -} -} - -#endif
\ No newline at end of file |