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/theory_arrays.cpp | |
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/theory_arrays.cpp')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 31 |
1 files changed, 21 insertions, 10 deletions
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"; } |