mergecav2019strings_countRewRed

12 files changed, 38 insertions, 33 deletions

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 612a1938a..cb0fcaf50 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -2,9 +2,9 @@
 /*! \file candidate_generator.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Morgan Deters
+ **   Andrew Reynolds, Morgan Deters, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index da4ec2d83..8cff12477 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
 
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -212,4 +212,4 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 2fcfa19d9..7598e6fdc 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -270,6 +270,11 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
         // Assert( f==value );
         for (unsigned k = 0, size = args.size(); k < size; k++)
         {
+          // must now subsitute back, to handle cases like
+          // (@ x y) matching (@ t (@ t s))
+          // where the above substitution would produce (@ x (@ x s)),
+          // but the argument should be (@ t s).
+          args[k] = args[k].substitute(var, value);
           Node val = args[k];
           std::map<unsigned, Node>::iterator itf = fixed_vals.find(k);
           if (itf == fixed_vals.end())
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index 8840c949f..6f0ff0635 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
-#define __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#define CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
 
 #include <map>
 #include <unordered_set>
@@ -275,4 +275,4 @@ class HigherOrderTrigger : public Trigger
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index f26df5b79..0a4386db9 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -2,9 +2,9 @@
 /*! \file inst_match_generator.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 83d4ce82e..3995c67b4 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -2,9 +2,9 @@
 /*! \file inst_match_generator.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Clark Barrett
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
 
 #include <map>
 #include "expr/node_trie.h"
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 6784fb8e3..8f671fb55 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -2,9 +2,9 @@
 /*! \file inst_strategy_e_matching.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters
+ **   Andrew Reynolds, Morgan Deters, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index a8d53cf4b..5eb992368 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H
-#define __CVC4__INST_STRATEGY_E_MATCHING_H
+#ifndef CVC4__INST_STRATEGY_E_MATCHING_H
+#define CVC4__INST_STRATEGY_E_MATCHING_H
 
 #include "context/context.h"
 #include "context/context_mm.h"
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 2aa8af53d..d2650f01f 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index c94320b74..139adcb04 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -2,9 +2,9 @@
 /*! \file instantiation_engine.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Tim King
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
-#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
 
 #include <memory>
 
@@ -95,4 +95,4 @@ class InstantiationEngine : public QuantifiersModule {
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index b50deea11..31bd1aa96 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index bbd7c386b..f276585d6 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
-#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H
+#define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 
 #include <map>
 
@@ -464,4 +464,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */