From e8b6775c1c43a704e4e6afdefad6378fdb200fd0 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 14 Jun 2010 16:06:51 +0000 Subject: [PATCH] Started work on array theory --- src/theory/arrays/Makefile.am | 3 +- src/theory/arrays/theory_arrays.cpp | 43 +++++++++++++++++++++++++++++ src/theory/arrays/theory_arrays.h | 21 +++++++------- test/regress/regress0/arr1.smt | 7 +++++ 4 files changed, 63 insertions(+), 11 deletions(-) create mode 100644 src/theory/arrays/theory_arrays.cpp create mode 100644 test/regress/regress0/arr1.smt diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 5d3514dda..813a91314 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarrays.la libarrays_la_SOURCES = \ - theory_arrays.h + theory_arrays.h \ + theory_arrays.cpp EXTRA_DIST = kinds diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp new file mode 100644 index 000000000..106d1a8da --- /dev/null +++ b/src/theory/arrays/theory_arrays.cpp @@ -0,0 +1,43 @@ +/********************* */ +/*! \file theory_arrays.cpp + ** \verbatim + ** Original author: barrett + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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 the theory of arrays. + ** + ** Implementation of the theory of arrays. + **/ + +#include "theory/arrays/theory_arrays.h" +#include "expr/kind.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::arrays; + +TheoryArrays::TheoryArrays(Context* c, OutputChannel& out) : + Theory(c, out) +{ +} + +TheoryArrays::~TheoryArrays() { +} + +void TheoryArrays::check(Effort e) { + while(!done()) { + Node assertion = get(); + Debug("arrays") << "TheoryArrays::check(): " << assertion << endl; + } + Debug("arrays") << "TheoryArrays::check(): done" << endl; +} diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 6ab0fac90..52e63831c 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -22,7 +22,10 @@ #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H #include "theory/theory.h" -#include "context/context.h" + +namespace context { +class Context; +} namespace CVC4 { namespace theory { @@ -30,15 +33,13 @@ namespace arrays { class TheoryArrays : public Theory { public: - TheoryArrays(context::Context* c, OutputChannel& out) : - Theory(c, out) { - } - - void preRegisterTerm(TNode n) { Unimplemented(); } - void registerTerm(TNode n) { Unimplemented(); } - void check(Effort e) { Unimplemented(); } - void propagate(Effort e) { Unimplemented(); } - void explain(TNode n, Effort e) { Unimplemented(); } + TheoryArrays(context::Context* c, OutputChannel& out); + ~TheoryArrays(); + void preRegisterTerm(TNode n) { } + void registerTerm(TNode n) { } + void check(Effort e); + void propagate(Effort e) { } + void explain(TNode n, Effort e) { } }; }/* CVC4::theory::arrays namespace */ diff --git a/test/regress/regress0/arr1.smt b/test/regress/regress0/arr1.smt new file mode 100644 index 000000000..55ca99601 --- /dev/null +++ b/test/regress/regress0/arr1.smt @@ -0,0 +1,7 @@ +(benchmark simple_arr + :logic QF_AX + :status unsat + :extrafuns ((a Array)) + :extrafuns ((i1 Index) (i2 Index)) + :formula (not (implies (= i1 i2) (= (select a i1) (select a i2)))) +) -- 2.30.2