Fix combinations of cegqi and non-standard triggers (#4271)

[cvc5.git] / src / theory / quantifiers / inst_match.h

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 86138feb3ed02a0de1d3c4e043461821e2d4a4bf..324b2c7368fb481525db64178aa2375775c1b2b7 100644 (file)
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
-#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
+#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
 
 #include <vector>
 
@@ -79,17 +79,15 @@ public:
     out << " )";
   }
   /** get the i^th term in the instantiation */
-  Node get(int i) const;
-  /** append the terms of this instantiation to inst */
-  void getInst(std::vector<Node>& inst) const;
+  Node get(size_t i) const;
   /** set/overwrites the i^th field in the instantiation with n */
-  void setValue( int i, TNode n );
+  void setValue(size_t i, TNode n);
   /** set the i^th term in the instantiation to n
    *
    * This method returns true if the i^th field was previously uninitialized,
    * or is equivalent to n modulo the equalities given by q.
    */
-  bool set(EqualityQuery* q, int i, TNode n);
+  bool set(EqualityQuery* q, size_t i, TNode n);
 };
 
 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
@@ -104,4 +102,4 @@ typedef CVC4::theory::inst::InstMatch InstMatch;
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */