diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-08-19 02:08:15 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-08-19 02:08:15 +0000 |
commit | e8e85053afba60bd6060cb07c52c88c316d73b30 (patch) | |
tree | 05b0d8c37ab667cb8f22d2159bf5079557405a9b /src/theory/quantifiers/inst_match.cpp | |
parent | 958b0b56aad79df431376344420106115ab23778 (diff) |
1. Fix for inst_match.cpp to allow compilation on fedora
2. Initial implementation of computeIsConst for arrays - still needs
additional checks based on cardinality
3. Finally fixed pre-competition bug in array rewriter
4. Still to come: array rewrites for constants and STORE_ALL
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 271e04968..14a84ea72 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -31,8 +31,10 @@ using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; -using namespace CVC4::theory::inst; +namespace CVC4 { +namespace theory { +namespace inst { InstMatch::InstMatch() { } @@ -878,3 +880,5 @@ int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ } return qe->addInstantiation( f, m ) ? 1 : 0; } + +}}} |