diff options
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
| -rw-r--r-- | src/theory/quantifiers/instantiate.h | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 753213f35..b4972a7b6 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -65,7 +65,7 @@ class InstantiationRewriter * and its proof generator. */ virtual TrustNode rewriteInstantiation(Node q, - std::vector<Node>& terms, + const std::vector<Node>& terms, Node inst, bool doVts) = 0; }; @@ -203,7 +203,7 @@ class Instantiate : public QuantifiersUtil * but does not enqueue an instantiation lemma. */ void recordInstantiation(Node q, - std::vector<Node>& terms, + const std::vector<Node>& terms, bool doVts = false); /** exists instantiation * @@ -212,7 +212,7 @@ class Instantiate : public QuantifiersUtil * modEq : whether to check for duplication modulo equality */ bool existsInstantiation(Node q, - std::vector<Node>& terms, + const std::vector<Node>& terms, bool modEq = false); //--------------------------------------general utilities /** get instantiation @@ -225,8 +225,8 @@ class Instantiate : public QuantifiersUtil * single INSTANTIATE step concluding the instantiated body of q from q. */ Node getInstantiation(Node q, - std::vector<Node>& vars, - std::vector<Node>& terms, + const std::vector<Node>& vars, + const std::vector<Node>& terms, InferenceId id = InferenceId::UNKNOWN, Node pfArg = Node::null(), bool doVts = false, @@ -235,7 +235,9 @@ class Instantiate : public QuantifiersUtil * * Same as above but with vars equal to the bound variables of q. */ - Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false); + Node getInstantiation(Node q, + const std::vector<Node>& terms, + bool doVts = false); //--------------------------------------end general utilities /** @@ -297,9 +299,9 @@ class Instantiate : public QuantifiersUtil private: /** record instantiation, return true if it was not a duplicate */ - bool recordInstantiationInternal(Node q, std::vector<Node>& terms); + bool recordInstantiationInternal(Node q, const std::vector<Node>& terms); /** remove instantiation from the cache */ - bool removeInstantiationInternal(Node q, std::vector<Node>& terms); + bool removeInstantiationInternal(Node q, const std::vector<Node>& terms); /** * Ensure that n has type tn, return a term equivalent to it for that type * if possible. |