diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/theory/arrays | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_info.cpp | 4 | ||||
-rw-r--r-- | src/theory/arrays/array_info.h | 19 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 4 | ||||
-rw-r--r-- | src/theory/arrays/static_fact_manager.cpp | 4 | ||||
-rw-r--r-- | src/theory/arrays/static_fact_manager.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 31 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/union_find.cpp | 4 | ||||
-rw-r--r-- | src/theory/arrays/union_find.h | 4 |
10 files changed, 60 insertions, 26 deletions
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 5a836fdc2..1e06621b4 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: lianah ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index ce3f015b5..fcc45bbd5 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file array_info.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + /*! \file array_info.h ** \verbatim ** Original author: lianah diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 30242db30..2f4bc7313 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -5,6 +5,7 @@ # theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" +typechecker "theory/arrays/theory_arrays_type_rules.h" properties polite stable-infinite properties check propagate presolve @@ -23,4 +24,7 @@ operator SELECT 2 "array select" # store a i e is a[i] <= e operator STORE 3 "array store" +typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule +typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule + endtheory diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp index 1e135514a..dfa32418f 100644 --- a/src/theory/arrays/static_fact_manager.cpp +++ b/src/theory/arrays/static_fact_manager.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file static_fact_manager.cpp ** \verbatim - ** Original author: mdeters + ** Original author: barrett ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h index de487f97c..5e1ba27a3 100644 --- a/src/theory/arrays/static_fact_manager.h +++ b/src/theory/arrays/static_fact_manager.h @@ -1,11 +1,11 @@ /********************* */ /*! \file static_fact_manager.h ** \verbatim - ** Original author: mdeters + ** Original author: barrett ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 888a98a45..6985aaea8 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2,8 +2,8 @@ /*! \file theory_arrays.cpp ** \verbatim ** Original author: barrett - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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 @@ -22,6 +22,7 @@ #include "expr/kind.h" #include <map> #include "theory/rewriter.h" +#include "expr/command.h" using namespace std; using namespace CVC4; @@ -689,7 +690,7 @@ void TheoryArrays::appendToDiseqList(TNode of, TNode eq) { * Iterates through the indices of a and stores of b and checks if any new * Row lemmas need to be instantiated. */ -bool TheoryArrays::isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j) { +bool TheoryArrays::isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j) { Assert(a.getType().isArray()); Assert(b.getType().isArray()); @@ -984,7 +985,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) { TNode j = store[1]; TNode c = store[0]; - if( !isRedundandRowLemma(store, c, j, i)){ + if( !isRedundantRowLemma(store, c, j, i)){ //&&!propagateFromRow(store, c, j, i)) { queueRowLemma(store, c, j, i); } @@ -1004,7 +1005,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) { TNode c = store[0]; if ( isNonLinear(c) - &&!isRedundandRowLemma(store, c, j, i)){ + &&!isRedundantRowLemma(store, c, j, i)){ //&&!propagateFromRow(store, c, j, i)) { queueRowLemma(store, c, j, i); } @@ -1066,7 +1067,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { Assert(store.getKind()==kind::STORE); TNode j = store[1]; //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; - if(!isRedundandRowLemma(store, store[0], j, i)) { + if(!isRedundantRowLemma(store, store[0], j, i)) { //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; queueRowLemma(store, store[0], j, i); } @@ -1078,7 +1079,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { Assert(instore.getKind()==kind::STORE); TNode j = instore[1]; //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; - if(!isRedundandRowLemma(instore, instore[0], j, i)) { + if(!isRedundantRowLemma(instore, instore[0], j, i)) { //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; queueRowLemma(instore, instore[0], j, i); } @@ -1104,7 +1105,7 @@ void TheoryArrays::checkStore(TNode a) { for(; it!= js->end(); it++) { TNode j = *it; - if(!isRedundandRowLemma(a, b, i, j)) { + if(!isRedundantRowLemma(a, b, i, j)) { //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; queueRowLemma(a,b,i,j); } @@ -1141,7 +1142,17 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) { && d_extAlreadyAdded.count(make_pair(b, a)) == 0) { NodeManager* nm = NodeManager::currentNM(); - Node k = nm->mkVar(a.getType()[0]); + TypeNode ixType = a.getType()[0]; + Node k = nm->mkVar(ixType); + if(Dump.isOn("declarations")) { + stringstream kss; + kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << k; + string ks = kss.str(); + Dump("declarations") + << CommentCommand(ks + " is an extensional lemma index variable " + "from the theory of arrays") << endl + << DeclareFunctionCommand(ks, ixType.toType()) << endl; + } Node eq = nm->mkNode(kind::EQUAL, a, b); Node ak = nm->mkNode(kind::SELECT, a, k); Node bk = nm->mkNode(kind::SELECT, b, k); @@ -1154,7 +1165,7 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) { ++d_numExt; return; } - Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; + Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index cf822cb65..37fffd2ec 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -2,10 +2,10 @@ /*! \file theory_arrays.h ** \verbatim ** Original author: mdeters - ** Major contributors: barrett - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -254,7 +254,7 @@ private: bool isAxiom(TNode lhs, TNode rhs); - bool isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j); + bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j); bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j); diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index d7b37d8ba..8c1c16de2 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_arrays_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: barrett, mdeters ** 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) diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp index b0f06b78e..57fd412e4 100644 --- a/src/theory/arrays/union_find.cpp +++ b/src/theory/arrays/union_find.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file union_find.cpp ** \verbatim - ** Original author: mdeters + ** Original author: lianah ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index 4a882806c..7ae85424d 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -1,11 +1,11 @@ /********************* */ /*! \file union_find.h ** \verbatim - ** Original author: mdeters + ** Original author: lianah ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** 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 |