From e9c29bb348bd8fab5cedc48ab96ce2a0e6f98078 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Jun 2020 10:19:10 -0500 Subject: (proof-new) Rename ProofSkolemCache to SkolemManager (#4556) This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing. This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form. Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler. Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal. --- src/expr/skolem_manager.h | 163 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 163 insertions(+) create mode 100644 src/expr/skolem_manager.h (limited to 'src/expr/skolem_manager.h') diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h new file mode 100644 index 000000000..eaf74bcce --- /dev/null +++ b/src/expr/skolem_manager.h @@ -0,0 +1,163 @@ +/********************* */ +/*! \file skolem_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** 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 + ** + ** \brief Skolem manager utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__SKOLEM_MANAGER_H +#define CVC4__EXPR__SKOLEM_MANAGER_H + +#include + +#include "expr/node.h" + +namespace CVC4 { + +class ProofGenerator; + +/** + * A manager for skolems that can be used in proofs. This is designed to be + * a trusted interface to NodeManager::mkSkolem, where one + * must provide a definition for the skolem they create in terms of a + * predicate that the introduced variable is intended to witness. + * + * It is implemented by mapping terms to an attribute corresponding to their + * "witness form" as described below. Hence, this class does not impact the + * reference counting of skolem variables which may be deleted if they are not + * used. + */ +class SkolemManager +{ + public: + SkolemManager() {} + ~SkolemManager() {} + /** + * This makes a skolem of same type as bound variable v, (say its type is T), + * whose definition is (witness ((v T)) pred). This definition is maintained + * by this class. + * + * Notice that (exists ((v T)) pred) should be a valid formula. This fact + * captures the reason for why the returned Skolem was introduced. + * + * Take as an example extensionality in arrays: + * + * (declare-fun a () (Array Int Int)) + * (declare-fun b () (Array Int Int)) + * (assert (not (= a b))) + * + * To witness the index where the arrays a and b are disequal, it is intended + * we call this method on: + * Node k = mkSkolem( x, F ) + * where F is: + * (=> (not (= a b)) (not (= (select a x) (select b x)))) + * and x is a fresh bound variable of integer type. Internally, this will map + * k to the term: + * (witness ((x Int)) (=> (not (= a b)) + * (not (= (select a x) (select b x))))) + * A lemma generated by the array solver for extensionality may safely use + * the skolem k in the standard way: + * (=> (not (= a b)) (not (= (select a k) (select b k)))) + * Furthermore, notice that the following lemma does not involve fresh + * skolem variables and is valid according to the theory of arrays extended + * with support for witness: + * (let ((w (witness ((x Int)) (=> (not (= a b)) + * (not (= (select a x) (select b x))))))) + * (=> (not (= a b)) (not (= (select a w) (select b w))))) + * This version of the lemma, which requires no explicit tracking of free + * Skolem variables, can be obtained by a call to getWitnessForm(...) + * below. We call this the "witness form" of the lemma above. + * + * @param v The bound variable of the same type of the Skolem to create. + * @param pred The desired property of the Skolem to create, in terms of bound + * variable v. + * @param prefix The prefix of the name of the Skolem + * @param comment Debug information about the Skolem + * @param flags The flags for the Skolem (see NodeManager::mkSkolem) + * @param pg The proof generator for this skolem. If non-null, this proof + * generator must respond to a call to getProofFor(exists x. pred) during + * the lifetime of the current node manager. + * @return The skolem whose witness form is registered by this class. + */ + Node mkSkolem(Node v, + Node pred, + const std::string& prefix, + const std::string& comment = "", + int flags = NodeManager::SKOLEM_DEFAULT, + ProofGenerator* pg = nullptr); + /** + * Same as above, but where pred is an existential quantified formula + * whose bound variable list contains v. For example, calling this method on: + * x, (exists ((x Int) (y Int)) (P x y)) + * will return: + * (witness ((x Int)) (exists ((y Int)) (P x y))) + * If the variable v is not in the bound variable list of q, then null is + * returned and an assertion failure is thrown. + */ + Node mkSkolemExists(Node v, + Node q, + const std::string& prefix, + const std::string& comment = "", + int flags = NodeManager::SKOLEM_DEFAULT, + ProofGenerator* pg = nullptr); + /** + * Same as above, but for special case of (witness ((x T)) (= x t)) + * where T is the type of t. This skolem is unique for each t, which we + * implement via an attribute on t. This attribute is used to ensure to + * associate a unique skolem for each t. + * + * Notice that a purification skolem is trivial to justify, and hence it + * does not require a proof generator. + */ + Node mkPurifySkolem(Node t, + const std::string& prefix, + const std::string& comment = "", + int flags = NodeManager::SKOLEM_DEFAULT); + /** + * Get proof generator for witness term t. This returns the proof generator + * that was provided in a call to mkSkolem above. + */ + ProofGenerator* getProofGenerator(Node t); + /** convert to witness form + * + * @param n The term or formula to convert to witness form described above + * @return n in witness form. + */ + static Node getWitnessForm(Node n); + /** convert to Skolem form + * + * @param n The term or formula to convert to Skolem form described above + * @return n in Skolem form. + */ + static Node getSkolemForm(Node n); + /** convert to witness form vector */ + static void convertToWitnessFormVec(std::vector& vec); + /** convert to Skolem form vector */ + static void convertToSkolemFormVec(std::vector& vec); + + private: + /** + * Mapping from witness terms to proof generators. + */ + std::map d_gens; + /** Convert to witness or skolem form */ + static Node convertInternal(Node n, bool toWitness); + /** Get or make skolem attribute for witness term w */ + static Node getOrMakeSkolem(Node w, + const std::string& prefix, + const std::string& comment, + int flags); +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */ -- cgit v1.2.3 From 2a518941922855626c015a73572a5a9a5a2d0ed7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Jun 2020 16:36:25 -0500 Subject: (proof-new) Refactor skolemization (#4586) This PR refactors skolemization in SkolemManager so that we use a "curried" form, where witnesses for a variable x is based on the existential where the prefix up to x has already been skolemized. This additionally adds more utility functions that will be used in the internal proof checker for quantifiers. --- src/expr/skolem_manager.cpp | 129 +++++++++++++++++++++++++++++++++++--------- src/expr/skolem_manager.h | 88 ++++++++++++++++++++++++------ 2 files changed, 176 insertions(+), 41 deletions(-) (limited to 'src/expr/skolem_manager.h') diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 0570af687..ced58eaf2 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -20,6 +20,8 @@ using namespace CVC4::kind; namespace CVC4 { +// Attributes are global maps from Nodes to data. Thus, note that these could +// be implemented as internal maps in SkolemManager. struct WitnessFormAttributeId { }; @@ -50,43 +52,97 @@ Node SkolemManager::mkSkolem(Node v, Node predw = getWitnessForm(pred); // make the witness term, which should not contain any skolem Node w = nm->mkNode(WITNESS, bvl, predw); - // store the mapping to proof generator - d_gens[w] = pg; + // store the mapping to proof generator if it exists + if (pg != nullptr) + { + Node q = nm->mkNode(EXISTS, w[0], w[1]); + // Notice this may overwrite an existing proof generator. This does not + // matter since either should be able to prove q. + d_gens[q] = pg; + } return getOrMakeSkolem(w, prefix, comment, flags); } -Node SkolemManager::mkSkolemExists(Node v, - Node q, - const std::string& prefix, - const std::string& comment, - int flags, - ProofGenerator* pg) +Node SkolemManager::mkSkolemize(Node q, + std::vector& skolems, + const std::string& prefix, + const std::string& comment, + int flags, + ProofGenerator* pg) +{ + Trace("sk-manager-debug") << "mkSkolemize..." << std::endl; + Assert(q.getKind() == EXISTS); + Node currQ = q; + for (const Node& av : q[0]) + { + Assert(currQ.getKind() == EXISTS && av == currQ[0][0]); + // currQ is updated to the result of skolemizing its first variable in + // the method below. + Node sk = skolemize(currQ, currQ, prefix, comment, flags); + Trace("sk-manager-debug") + << "made skolem " << sk << " for " << av << std::endl; + skolems.push_back(sk); + } + if (pg != nullptr) + { + // Same as above, this may overwrite an existing proof generator + d_gens[q] = pg; + } + return currQ; +} + +Node SkolemManager::skolemize(Node q, + Node& qskolem, + const std::string& prefix, + const std::string& comment, + int flags) { Assert(q.getKind() == EXISTS); - bool foundVar = false; + Node v; std::vector ovars; + std::vector ovarsW; + Trace("sk-manager-debug") << "mkSkolemize..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); for (const Node& av : q[0]) { - if (av == v) + if (v.isNull()) { - foundVar = true; + v = av; continue; } + // must make fresh variable to avoid shadowing, which is unique per + // variable av to ensure that this method is deterministic. Having this + // method deterministic ensures that the proof checker (e.g. for + // quantifiers) is capable of proving the expected value for conclusions + // of proof rules, instead of an alpha-equivalent variant of a conclusion. + Node avp = getOrMakeBoundVariable(av, av); + ovarsW.push_back(avp); ovars.push_back(av); } - if (!foundVar) - { - Assert(false); - return Node::null(); - } + Assert(!v.isNull()); Node pred = q[1]; + qskolem = q[1]; + Trace("sk-manager-debug") << "make exists predicate" << std::endl; if (!ovars.empty()) { - NodeManager* nm = NodeManager::currentNM(); - Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars); + Node bvl = nm->mkNode(BOUND_VAR_LIST, ovarsW); pred = nm->mkNode(EXISTS, bvl, pred); + // skolem form keeps the old variables + bvl = nm->mkNode(BOUND_VAR_LIST, ovars); + qskolem = nm->mkNode(EXISTS, bvl, pred); } - return mkSkolem(v, pred, prefix, comment, flags, pg); + Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl; + // don't use a proof generator, since this may be an intermediate, partially + // skolemized formula. + Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr); + Assert(k.getType() == v.getType()); + TNode tv = v; + TNode tk = k; + Trace("sk-manager-debug") + << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl; + qskolem = qskolem.substitute(tv, tk); + Trace("sk-manager-debug") << "qskolem done substitution" << std::endl; + return k; } Node SkolemManager::mkPurifySkolem(Node t, @@ -111,6 +167,16 @@ Node SkolemManager::mkPurifySkolem(Node t, return k; } +Node SkolemManager::mkExistential(Node t, Node p) +{ + Assert(p.getType().isBoolean()); + NodeManager* nm = NodeManager::currentNM(); + Node v = getOrMakeBoundVariable(t, p); + Node bvl = nm->mkNode(BOUND_VAR_LIST, v); + Node psubs = p.substitute(TNode(t), TNode(v)); + return nm->mkNode(EXISTS, bvl, psubs); +} + ProofGenerator* SkolemManager::getProofGenerator(Node t) { std::map::iterator it = d_gens.find(t); @@ -131,8 +197,8 @@ Node SkolemManager::convertInternal(Node n, bool toWitness) { return n; } - Trace("pf-skolem-debug") << "SkolemManager::convertInternal: " << toWitness - << " " << n << std::endl; + Trace("sk-manager-debug") << "SkolemManager::convertInternal: " << toWitness + << " " << n << std::endl; WitnessFormAttribute wfa; SkolemFormAttribute sfa; NodeManager* nm = NodeManager::currentNM(); @@ -217,7 +283,7 @@ Node SkolemManager::convertInternal(Node n, bool toWitness) } while (!visit.empty()); Assert(visited.find(n) != visited.end()); Assert(!visited.find(n)->second.isNull()); - Trace("pf-skolem-debug") << "..return " << visited[n] << std::endl; + Trace("sk-manager-debug") << "..return " << visited[n] << std::endl; return visited[n]; } @@ -256,9 +322,24 @@ Node SkolemManager::getOrMakeSkolem(Node w, k.setAttribute(wfa, w); // set skolem form attribute for w w.setAttribute(sfa, k); - Trace("pf-skolem") << "SkolemManager::mkSkolem: " << k << " : " << w - << std::endl; + Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w + << std::endl; return k; } +Node SkolemManager::getOrMakeBoundVariable(Node t, Node s) +{ + std::pair key(t, s); + std::map, Node>::iterator it = + d_witnessBoundVar.find(key); + if (it != d_witnessBoundVar.end()) + { + return it->second; + } + TypeNode tt = t.getType(); + Node v = NodeManager::currentNM()->mkBoundVar(tt); + d_witnessBoundVar[key] = v; + return v; +} + } // namespace CVC4 diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index eaf74bcce..557947214 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -84,7 +84,7 @@ class SkolemManager * @param comment Debug information about the Skolem * @param flags The flags for the Skolem (see NodeManager::mkSkolem) * @param pg The proof generator for this skolem. If non-null, this proof - * generator must respond to a call to getProofFor(exists x. pred) during + * generator must respond to a call to getProofFor(exists v. pred) during * the lifetime of the current node manager. * @return The skolem whose witness form is registered by this class. */ @@ -95,20 +95,40 @@ class SkolemManager int flags = NodeManager::SKOLEM_DEFAULT, ProofGenerator* pg = nullptr); /** - * Same as above, but where pred is an existential quantified formula - * whose bound variable list contains v. For example, calling this method on: - * x, (exists ((x Int) (y Int)) (P x y)) - * will return: - * (witness ((x Int)) (exists ((y Int)) (P x y))) - * If the variable v is not in the bound variable list of q, then null is - * returned and an assertion failure is thrown. + * Make skolemized form of existentially quantified formula q, and store its + * Skolems into the argument skolems. + * + * For example, calling this method on: + * (exists ((x Int) (y Int)) (P x y)) + * returns: + * (P w1 w2) + * where w1 and w2 are skolems with witness forms: + * (witness ((x Int)) (exists ((y' Int)) (P x y'))) + * (witness ((y Int)) (P w1 y)) + * respectively. Additionally, this method will add { w1, w2 } to skolems. + * Notice that y is renamed to y' in the witness form of w1 to avoid variable + * shadowing. + * + * In contrast to mkSkolem, the proof generator is for the *entire* + * existentially quantified formula q, which may have multiple variables in + * its prefix. + * + * @param q The existentially quantified formula to skolemize, + * @param skolems Vector to add Skolems of q to, + * @param prefix The prefix of the name of each of the Skolems + * @param comment Debug information about each of the Skolems + * @param flags The flags for the Skolem (see NodeManager::mkSkolem) + * @param pg The proof generator for this skolem. If non-null, this proof + * generator must respond to a call to getProofFor(q) during + * the lifetime of the current node manager. + * @return The skolemized form of q. */ - Node mkSkolemExists(Node v, - Node q, - const std::string& prefix, - const std::string& comment = "", - int flags = NodeManager::SKOLEM_DEFAULT, - ProofGenerator* pg = nullptr); + Node mkSkolemize(Node q, + std::vector& skolems, + const std::string& prefix, + const std::string& comment = "", + int flags = NodeManager::SKOLEM_DEFAULT, + ProofGenerator* pg = nullptr); /** * Same as above, but for special case of (witness ((x T)) (= x t)) * where T is the type of t. This skolem is unique for each t, which we @@ -123,10 +143,16 @@ class SkolemManager const std::string& comment = "", int flags = NodeManager::SKOLEM_DEFAULT); /** - * Get proof generator for witness term t. This returns the proof generator - * that was provided in a call to mkSkolem above. + * Get proof generator for existentially quantified formula q. This returns + * the proof generator that was provided in a call to mkSkolem above. */ - ProofGenerator* getProofGenerator(Node t); + ProofGenerator* getProofGenerator(Node q); + /** + * Make existential. Given t and p[t] where p is a formula, this returns + * (exists ((x T)) p[x]) + * where T is the type of t, and x is a variable unique to t,p. + */ + Node mkExistential(Node t, Node p); /** convert to witness form * * @param n The term or formula to convert to witness form described above @@ -149,6 +175,11 @@ class SkolemManager * Mapping from witness terms to proof generators. */ std::map d_gens; + /** + * Map to canonical bound variables. This is used for example by the method + * mkExistential. + */ + std::map, Node> d_witnessBoundVar; /** Convert to witness or skolem form */ static Node convertInternal(Node n, bool toWitness); /** Get or make skolem attribute for witness term w */ @@ -156,6 +187,29 @@ class SkolemManager const std::string& prefix, const std::string& comment, int flags); + /** + * Skolemize the first variable of existentially quantified formula q. + * For example, calling this method on: + * (exists ((x Int) (y Int)) (P x y)) + * will return: + * (witness ((x Int)) (exists ((y Int)) (P x y))) + * If q is not an existentially quantified formula, then null is + * returned and an assertion failure is thrown. + * + * This method additionally updates qskolem to be the skolemized form of q. + * In the above example, this is set to: + * (exists ((y Int)) (P (witness ((x Int)) (exists ((y' Int)) (P x y'))) y)) + */ + Node skolemize(Node q, + Node& qskolem, + const std::string& prefix, + const std::string& comment = "", + int flags = NodeManager::SKOLEM_DEFAULT); + /** + * Get or make bound variable unique to (s,t), for d_witnessBoundVar, where + * t and s are terms. + */ + Node getOrMakeBoundVariable(Node t, Node s); }; } // namespace CVC4 -- cgit v1.2.3 From e37d0c385d698d46f14fb30e5a44de63c686fadb Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 16 Jun 2020 13:48:05 -0700 Subject: Update copyright headers. --- contrib/get-authors | 4 +++- contrib/update-copyright.pl | 4 ++-- examples/SimpleVC.java | 4 ++-- examples/api/bitvectors-new.cpp | 2 +- examples/api/bitvectors.cpp | 2 +- examples/api/bitvectors_and_arrays-new.cpp | 4 ++-- examples/api/bitvectors_and_arrays.cpp | 2 +- examples/api/combination-new.cpp | 4 ++-- examples/api/combination.cpp | 4 ++-- examples/api/datatypes-new.cpp | 4 ++-- examples/api/datatypes.cpp | 4 ++-- examples/api/extract-new.cpp | 2 +- examples/api/extract.cpp | 4 ++-- examples/api/helloworld-new.cpp | 4 ++-- examples/api/helloworld.cpp | 2 +- examples/api/java/BitVectors.java | 4 ++-- examples/api/java/BitVectorsAndArrays.java | 4 ++-- examples/api/java/CVC4Streams.java | 4 ++-- examples/api/java/Combination.java | 4 ++-- examples/api/java/Datatypes.java | 4 ++-- examples/api/java/Exceptions.java | 2 +- examples/api/java/FloatingPointArith.java | 2 +- examples/api/java/HelloWorld.java | 4 ++-- examples/api/java/LinearArith.java | 4 ++-- examples/api/java/PipedInput.java | 4 ++-- examples/api/java/Relations.java | 2 +- examples/api/java/Statistics.java | 2 +- examples/api/java/Strings.java | 4 ++-- examples/api/java/UnsatCores.java | 4 ++-- examples/api/linear_arith-new.cpp | 4 ++-- examples/api/linear_arith.cpp | 4 ++-- examples/api/sets-new.cpp | 4 ++-- examples/api/sets.cpp | 4 ++-- examples/api/strings-new.cpp | 4 ++-- examples/api/strings.cpp | 2 +- examples/api/sygus-fun.cpp | 4 ++-- examples/api/sygus-grammar.cpp | 4 ++-- examples/api/sygus-inv.cpp | 4 ++-- examples/hashsmt/sha1.hpp | 2 +- examples/hashsmt/sha1_collision.cpp | 2 +- examples/hashsmt/sha1_inversion.cpp | 2 +- examples/hashsmt/word.cpp | 2 +- examples/hashsmt/word.h | 2 +- examples/nra-translate/normalize.cpp | 2 +- examples/nra-translate/smt2info.cpp | 2 +- examples/nra-translate/smt2todreal.cpp | 2 +- examples/nra-translate/smt2toisat.cpp | 2 +- examples/nra-translate/smt2tomathematica.cpp | 2 +- examples/nra-translate/smt2toqepcad.cpp | 2 +- examples/nra-translate/smt2toredlog.cpp | 2 +- examples/sets-translate/sets_translate.cpp | 2 +- examples/simple_vc_cxx.cpp | 4 ++-- examples/simple_vc_quant_cxx.cpp | 2 +- examples/translator.cpp | 4 ++-- src/api/cvc4cpp.cpp | 4 ++-- src/api/cvc4cpp.h | 4 ++-- src/api/cvc4cppkind.h | 4 ++-- src/base/check.cpp | 4 ++-- src/base/check.h | 4 ++-- src/base/configuration.cpp | 2 +- src/base/configuration.h | 2 +- src/base/configuration_private.h | 4 ++-- src/base/exception.cpp | 2 +- src/base/exception.h | 4 ++-- src/base/git_versioninfo.cpp.in | 2 +- src/base/listener.cpp | 2 +- src/base/listener.h | 4 ++-- src/base/map_util.h | 4 ++-- src/base/modal_exception.h | 4 ++-- src/base/output.cpp | 2 +- src/base/output.h | 2 +- src/bindings/java_iterator_adapter.h | 4 ++-- src/bindings/java_stream_adapters.h | 4 ++-- src/bindings/swig.h | 4 ++-- src/context/backtrackable.h | 4 ++-- src/context/cddense_set.h | 2 +- src/context/cdhashmap.h | 2 +- src/context/cdhashmap_forward.h | 4 ++-- src/context/cdhashset.h | 4 ++-- src/context/cdhashset_forward.h | 4 ++-- src/context/cdinsert_hashmap.h | 2 +- src/context/cdinsert_hashmap_forward.h | 4 ++-- src/context/cdlist.h | 2 +- src/context/cdlist_forward.h | 4 ++-- src/context/cdmaybe.h | 2 +- src/context/cdo.h | 4 ++-- src/context/cdqueue.h | 4 ++-- src/context/cdtrail_queue.h | 4 ++-- src/context/context.cpp | 2 +- src/context/context.h | 2 +- src/context/context_mm.cpp | 2 +- src/context/context_mm.h | 2 +- src/decision/decision_attributes.h | 4 ++-- src/decision/decision_engine.cpp | 4 ++-- src/decision/decision_engine.h | 4 ++-- src/decision/decision_strategy.h | 4 ++-- src/decision/justification_heuristic.cpp | 4 ++-- src/decision/justification_heuristic.h | 4 ++-- src/expr/array.h | 4 ++-- src/expr/array_store_all.cpp | 2 +- src/expr/array_store_all.h | 4 ++-- src/expr/ascription_type.h | 4 ++-- src/expr/attribute.cpp | 2 +- src/expr/attribute.h | 2 +- src/expr/attribute_internals.h | 4 ++-- src/expr/attribute_unique_id.h | 2 +- src/expr/datatype.cpp | 2 +- src/expr/datatype.h | 2 +- src/expr/dtype.cpp | 4 ++-- src/expr/dtype.h | 4 ++-- src/expr/dtype_cons.cpp | 4 ++-- src/expr/dtype_cons.h | 4 ++-- src/expr/dtype_selector.cpp | 2 +- src/expr/dtype_selector.h | 4 ++-- src/expr/emptyset.cpp | 2 +- src/expr/emptyset.h | 2 +- src/expr/expr_iomanip.cpp | 2 +- src/expr/expr_iomanip.h | 4 ++-- src/expr/expr_manager_scope.h | 4 ++-- src/expr/expr_manager_template.cpp | 2 +- src/expr/expr_manager_template.h | 4 ++-- src/expr/expr_sequence.cpp | 2 +- src/expr/expr_sequence.h | 2 +- src/expr/expr_template.cpp | 4 ++-- src/expr/expr_template.h | 2 +- src/expr/kind_map.h | 4 ++-- src/expr/kind_template.cpp | 4 ++-- src/expr/kind_template.h | 4 ++-- src/expr/lazy_proof.cpp | 2 +- src/expr/lazy_proof.h | 2 +- src/expr/match_trie.cpp | 2 +- src/expr/match_trie.h | 4 ++-- src/expr/metakind_template.cpp | 4 ++-- src/expr/metakind_template.h | 4 ++-- src/expr/node.cpp | 2 +- src/expr/node.h | 4 ++-- src/expr/node_algorithm.cpp | 4 ++-- src/expr/node_algorithm.h | 4 ++-- src/expr/node_builder.h | 4 ++-- src/expr/node_manager.cpp | 2 +- src/expr/node_manager.h | 2 +- src/expr/node_manager_attributes.h | 2 +- src/expr/node_manager_listeners.cpp | 2 +- src/expr/node_manager_listeners.h | 2 +- src/expr/node_self_iterator.h | 4 ++-- src/expr/node_traversal.cpp | 2 +- src/expr/node_traversal.h | 2 +- src/expr/node_trie.cpp | 2 +- src/expr/node_trie.h | 4 ++-- src/expr/node_value.cpp | 4 ++-- src/expr/node_value.h | 4 ++-- src/expr/node_visitor.h | 4 ++-- src/expr/proof.cpp | 2 +- src/expr/proof.h | 2 +- src/expr/proof_checker.cpp | 2 +- src/expr/proof_checker.h | 2 +- src/expr/proof_generator.cpp | 2 +- src/expr/proof_generator.h | 2 +- src/expr/proof_node.cpp | 2 +- src/expr/proof_node.h | 2 +- src/expr/proof_node_algorithm.cpp | 2 +- src/expr/proof_node_algorithm.h | 2 +- src/expr/proof_node_manager.cpp | 2 +- src/expr/proof_node_manager.h | 2 +- src/expr/proof_node_to_sexpr.cpp | 2 +- src/expr/proof_node_to_sexpr.h | 4 ++-- src/expr/proof_rule.cpp | 4 ++-- src/expr/proof_rule.h | 4 ++-- src/expr/proof_step_buffer.cpp | 2 +- src/expr/proof_step_buffer.h | 2 +- src/expr/record.cpp | 4 ++-- src/expr/record.h | 4 ++-- src/expr/sequence.cpp | 2 +- src/expr/sequence.h | 2 +- src/expr/skolem_manager.cpp | 2 +- src/expr/skolem_manager.h | 2 +- src/expr/sygus_datatype.cpp | 4 ++-- src/expr/sygus_datatype.h | 4 ++-- src/expr/symbol_table.cpp | 2 +- src/expr/symbol_table.h | 2 +- src/expr/term_canonize.cpp | 2 +- src/expr/term_canonize.h | 2 +- src/expr/term_conversion_proof_generator.cpp | 2 +- src/expr/term_conversion_proof_generator.h | 2 +- src/expr/type.cpp | 4 ++-- src/expr/type.h | 4 ++-- src/expr/type_checker.h | 4 ++-- src/expr/type_checker_template.cpp | 4 ++-- src/expr/type_checker_util.h | 2 +- src/expr/type_matcher.cpp | 4 ++-- src/expr/type_matcher.h | 4 ++-- src/expr/type_node.cpp | 2 +- src/expr/type_node.h | 2 +- src/expr/type_properties_template.h | 4 ++-- src/expr/uninterpreted_constant.cpp | 4 ++-- src/expr/uninterpreted_constant.h | 2 +- src/expr/variable_type_map.h | 4 ++-- src/include/cvc4.h | 4 ++-- src/include/cvc4_private.h | 4 ++-- src/include/cvc4_private_library.h | 4 ++-- src/include/cvc4_public.h | 4 ++-- src/include/cvc4parser_private.h | 2 +- src/include/cvc4parser_public.h | 2 +- src/lib/clock_gettime.c | 2 +- src/lib/clock_gettime.h | 4 ++-- src/lib/ffs.c | 2 +- src/lib/ffs.h | 4 ++-- src/lib/replacements.h | 4 ++-- src/lib/strtok_r.c | 2 +- src/lib/strtok_r.h | 4 ++-- src/main/command_executor.cpp | 4 ++-- src/main/command_executor.h | 4 ++-- src/main/driver_unified.cpp | 4 ++-- src/main/interactive_shell.cpp | 2 +- src/main/interactive_shell.h | 2 +- src/main/main.cpp | 2 +- src/main/main.h | 4 ++-- src/main/util.cpp | 2 +- src/options/base_handlers.h | 4 ++-- src/options/decision_weight.h | 4 ++-- src/options/didyoumean.cpp | 2 +- src/options/didyoumean.h | 2 +- src/options/didyoumean_test.cpp | 4 ++-- src/options/language.cpp | 4 ++-- src/options/language.h | 2 +- src/options/module_template.cpp | 2 +- src/options/module_template.h | 2 +- src/options/open_ostream.cpp | 2 +- src/options/open_ostream.h | 4 ++-- src/options/option_exception.cpp | 2 +- src/options/option_exception.h | 4 ++-- src/options/options.h | 2 +- src/options/options_handler.cpp | 4 ++-- src/options/options_handler.h | 4 ++-- src/options/options_holder_template.h | 4 ++-- src/options/options_public_functions.cpp | 4 ++-- src/options/options_template.cpp | 4 ++-- src/options/printer_modes.cpp | 4 ++-- src/options/printer_modes.h | 4 ++-- src/options/set_language.cpp | 2 +- src/options/set_language.h | 4 ++-- src/parser/antlr_input.cpp | 4 ++-- src/parser/antlr_input.h | 2 +- src/parser/antlr_input_imports.cpp | 2 +- src/parser/antlr_line_buffered_input.cpp | 2 +- src/parser/antlr_line_buffered_input.h | 4 ++-- src/parser/antlr_tracing.h | 4 ++-- src/parser/bounded_token_buffer.cpp | 2 +- src/parser/bounded_token_buffer.h | 4 ++-- src/parser/bounded_token_factory.cpp | 2 +- src/parser/bounded_token_factory.h | 4 ++-- src/parser/cvc/Cvc.g | 2 +- src/parser/cvc/cvc.cpp | 4 ++-- src/parser/cvc/cvc.h | 4 ++-- src/parser/cvc/cvc_input.cpp | 4 ++-- src/parser/cvc/cvc_input.h | 4 ++-- src/parser/input.cpp | 2 +- src/parser/input.h | 2 +- src/parser/line_buffer.cpp | 4 ++-- src/parser/line_buffer.h | 4 ++-- src/parser/memory_mapped_input_buffer.cpp | 2 +- src/parser/memory_mapped_input_buffer.h | 4 ++-- src/parser/parse_op.cpp | 2 +- src/parser/parse_op.h | 2 +- src/parser/parser.cpp | 4 ++-- src/parser/parser.h | 4 ++-- src/parser/parser_builder.cpp | 2 +- src/parser/parser_builder.h | 2 +- src/parser/parser_exception.h | 2 +- src/parser/smt2/Smt2.g | 4 ++-- src/parser/smt2/smt2.cpp | 4 ++-- src/parser/smt2/smt2.h | 4 ++-- src/parser/smt2/smt2_input.cpp | 4 ++-- src/parser/smt2/smt2_input.h | 4 ++-- src/parser/smt2/sygus_input.cpp | 4 ++-- src/parser/smt2/sygus_input.h | 4 ++-- src/parser/tptp/Tptp.g | 4 ++-- src/parser/tptp/tptp.cpp | 4 ++-- src/parser/tptp/tptp.h | 4 ++-- src/parser/tptp/tptp_input.cpp | 4 ++-- src/parser/tptp/tptp_input.h | 4 ++-- src/preprocessing/assertion_pipeline.cpp | 2 +- src/preprocessing/assertion_pipeline.h | 2 +- src/preprocessing/passes/ackermann.cpp | 4 ++-- src/preprocessing/passes/ackermann.h | 4 ++-- src/preprocessing/passes/apply_substs.cpp | 4 ++-- src/preprocessing/passes/apply_substs.h | 4 ++-- src/preprocessing/passes/bool_to_bv.cpp | 2 +- src/preprocessing/passes/bool_to_bv.h | 4 ++-- src/preprocessing/passes/bv_abstraction.cpp | 2 +- src/preprocessing/passes/bv_abstraction.h | 2 +- src/preprocessing/passes/bv_eager_atoms.cpp | 2 +- src/preprocessing/passes/bv_eager_atoms.h | 2 +- src/preprocessing/passes/bv_gauss.cpp | 4 ++-- src/preprocessing/passes/bv_gauss.h | 4 ++-- src/preprocessing/passes/bv_intro_pow2.cpp | 2 +- src/preprocessing/passes/bv_intro_pow2.h | 2 +- src/preprocessing/passes/bv_to_bool.cpp | 2 +- src/preprocessing/passes/bv_to_bool.h | 4 ++-- src/preprocessing/passes/bv_to_int.cpp | 4 ++-- src/preprocessing/passes/bv_to_int.h | 4 ++-- src/preprocessing/passes/extended_rewriter_pass.cpp | 2 +- src/preprocessing/passes/extended_rewriter_pass.h | 4 ++-- src/preprocessing/passes/global_negate.cpp | 2 +- src/preprocessing/passes/global_negate.h | 4 ++-- src/preprocessing/passes/ho_elim.cpp | 2 +- src/preprocessing/passes/ho_elim.h | 2 +- src/preprocessing/passes/int_to_bv.cpp | 4 ++-- src/preprocessing/passes/int_to_bv.h | 4 ++-- src/preprocessing/passes/ite_removal.cpp | 4 ++-- src/preprocessing/passes/ite_removal.h | 4 ++-- src/preprocessing/passes/ite_simp.cpp | 2 +- src/preprocessing/passes/ite_simp.h | 4 ++-- src/preprocessing/passes/miplib_trick.cpp | 4 ++-- src/preprocessing/passes/miplib_trick.h | 2 +- src/preprocessing/passes/nl_ext_purify.cpp | 4 ++-- src/preprocessing/passes/nl_ext_purify.h | 4 ++-- src/preprocessing/passes/non_clausal_simp.cpp | 4 ++-- src/preprocessing/passes/non_clausal_simp.h | 4 ++-- src/preprocessing/passes/pseudo_boolean_processor.cpp | 2 +- src/preprocessing/passes/pseudo_boolean_processor.h | 4 ++-- src/preprocessing/passes/quantifier_macros.cpp | 4 ++-- src/preprocessing/passes/quantifier_macros.h | 4 ++-- src/preprocessing/passes/quantifiers_preprocess.cpp | 2 +- src/preprocessing/passes/quantifiers_preprocess.h | 4 ++-- src/preprocessing/passes/real_to_int.cpp | 4 ++-- src/preprocessing/passes/real_to_int.h | 4 ++-- src/preprocessing/passes/rewrite.cpp | 2 +- src/preprocessing/passes/rewrite.h | 4 ++-- src/preprocessing/passes/sep_skolem_emp.cpp | 2 +- src/preprocessing/passes/sep_skolem_emp.h | 4 ++-- src/preprocessing/passes/sort_infer.cpp | 2 +- src/preprocessing/passes/sort_infer.h | 4 ++-- src/preprocessing/passes/static_learning.cpp | 4 ++-- src/preprocessing/passes/static_learning.h | 4 ++-- src/preprocessing/passes/sygus_inference.cpp | 4 ++-- src/preprocessing/passes/sygus_inference.h | 4 ++-- src/preprocessing/passes/synth_rew_rules.cpp | 4 ++-- src/preprocessing/passes/synth_rew_rules.h | 4 ++-- src/preprocessing/passes/theory_preprocess.cpp | 2 +- src/preprocessing/passes/theory_preprocess.h | 2 +- src/preprocessing/passes/unconstrained_simplifier.cpp | 4 ++-- src/preprocessing/passes/unconstrained_simplifier.h | 4 ++-- src/preprocessing/preprocessing_pass.cpp | 2 +- src/preprocessing/preprocessing_pass.h | 4 ++-- src/preprocessing/preprocessing_pass_context.cpp | 2 +- src/preprocessing/preprocessing_pass_context.h | 4 ++-- src/preprocessing/preprocessing_pass_registry.cpp | 4 ++-- src/preprocessing/preprocessing_pass_registry.h | 4 ++-- src/preprocessing/util/ite_utilities.cpp | 2 +- src/preprocessing/util/ite_utilities.h | 2 +- src/printer/ast/ast_printer.cpp | 4 ++-- src/printer/ast/ast_printer.h | 4 ++-- src/printer/cvc/cvc_printer.cpp | 2 +- src/printer/cvc/cvc_printer.h | 4 ++-- src/printer/dagification_visitor.cpp | 4 ++-- src/printer/dagification_visitor.h | 4 ++-- src/printer/printer.cpp | 2 +- src/printer/printer.h | 4 ++-- src/printer/smt2/smt2_printer.cpp | 2 +- src/printer/smt2/smt2_printer.h | 2 +- src/printer/sygus_print_callback.cpp | 2 +- src/printer/sygus_print_callback.h | 4 ++-- src/printer/tptp/tptp_printer.cpp | 4 ++-- src/printer/tptp/tptp_printer.h | 2 +- src/proof/arith_proof.cpp | 4 ++-- src/proof/arith_proof.h | 2 +- src/proof/arith_proof_recorder.cpp | 2 +- src/proof/arith_proof_recorder.h | 4 ++-- src/proof/array_proof.cpp | 2 +- src/proof/array_proof.h | 2 +- src/proof/bitvector_proof.cpp | 2 +- src/proof/bitvector_proof.h | 2 +- src/proof/clausal_bitvector_proof.cpp | 4 ++-- src/proof/clausal_bitvector_proof.h | 2 +- src/proof/clause_id.h | 4 ++-- src/proof/cnf_proof.cpp | 2 +- src/proof/cnf_proof.h | 2 +- src/proof/dimacs.cpp | 2 +- src/proof/dimacs.h | 2 +- src/proof/drat/drat_proof.cpp | 4 ++-- src/proof/drat/drat_proof.h | 4 ++-- src/proof/er/er_proof.cpp | 4 ++-- src/proof/er/er_proof.h | 4 ++-- src/proof/lemma_proof.cpp | 4 ++-- src/proof/lemma_proof.h | 4 ++-- src/proof/lfsc_proof_printer.cpp | 2 +- src/proof/lfsc_proof_printer.h | 4 ++-- src/proof/lrat/lrat_proof.cpp | 4 ++-- src/proof/lrat/lrat_proof.h | 4 ++-- src/proof/proof.h | 4 ++-- src/proof/proof_manager.cpp | 2 +- src/proof/proof_manager.h | 4 ++-- src/proof/proof_output_channel.cpp | 2 +- src/proof/proof_output_channel.h | 2 +- src/proof/proof_utils.cpp | 2 +- src/proof/proof_utils.h | 2 +- src/proof/resolution_bitvector_proof.cpp | 2 +- src/proof/resolution_bitvector_proof.h | 2 +- src/proof/sat_proof.h | 2 +- src/proof/sat_proof_implementation.h | 2 +- src/proof/simplify_boolean_node.cpp | 2 +- src/proof/simplify_boolean_node.h | 4 ++-- src/proof/skolemization_manager.cpp | 4 ++-- src/proof/skolemization_manager.h | 4 ++-- src/proof/theory_proof.cpp | 2 +- src/proof/theory_proof.h | 4 ++-- src/proof/uf_proof.cpp | 2 +- src/proof/uf_proof.h | 4 ++-- src/proof/unsat_core.cpp | 2 +- src/proof/unsat_core.h | 4 ++-- src/prop/bv_sat_solver_notify.h | 4 ++-- src/prop/bvminisat/bvminisat.cpp | 2 +- src/prop/bvminisat/bvminisat.h | 2 +- src/prop/cadical.cpp | 4 ++-- src/prop/cadical.h | 4 ++-- src/prop/cnf_stream.cpp | 2 +- src/prop/cnf_stream.h | 2 +- src/prop/cryptominisat.cpp | 2 +- src/prop/cryptominisat.h | 4 ++-- src/prop/minisat/minisat.cpp | 2 +- src/prop/minisat/minisat.h | 4 ++-- src/prop/prop_engine.cpp | 2 +- src/prop/prop_engine.h | 2 +- src/prop/registrar.h | 4 ++-- src/prop/sat_solver.h | 2 +- src/prop/sat_solver_factory.cpp | 4 ++-- src/prop/sat_solver_factory.h | 4 ++-- src/prop/sat_solver_types.cpp | 2 +- src/prop/sat_solver_types.h | 4 ++-- src/prop/theory_proxy.cpp | 4 ++-- src/prop/theory_proxy.h | 4 ++-- src/smt/command.cpp | 2 +- src/smt/command.h | 2 +- src/smt/command_list.cpp | 2 +- src/smt/command_list.h | 4 ++-- src/smt/defined_function.h | 2 +- src/smt/dump.cpp | 4 ++-- src/smt/dump.h | 2 +- src/smt/logic_exception.h | 4 ++-- src/smt/logic_request.cpp | 2 +- src/smt/logic_request.h | 4 ++-- src/smt/managed_ostreams.cpp | 2 +- src/smt/managed_ostreams.h | 2 +- src/smt/model.cpp | 4 ++-- src/smt/model.h | 4 ++-- src/smt/model_blocker.cpp | 4 ++-- src/smt/model_blocker.h | 4 ++-- src/smt/model_core_builder.cpp | 4 ++-- src/smt/model_core_builder.h | 4 ++-- src/smt/process_assertions.cpp | 4 ++-- src/smt/process_assertions.h | 4 ++-- src/smt/set_defaults.cpp | 4 ++-- src/smt/set_defaults.h | 2 +- src/smt/smt_engine.cpp | 4 ++-- src/smt/smt_engine.h | 4 ++-- src/smt/smt_engine_scope.cpp | 4 ++-- src/smt/smt_engine_scope.h | 2 +- src/smt/smt_engine_stats.cpp | 2 +- src/smt/smt_engine_stats.h | 2 +- src/smt/smt_statistics_registry.cpp | 2 +- src/smt/smt_statistics_registry.h | 4 ++-- src/smt/term_formula_removal.cpp | 4 ++-- src/smt/term_formula_removal.h | 2 +- src/smt/update_ostream.h | 2 +- src/smt_util/boolean_simplification.cpp | 2 +- src/smt_util/boolean_simplification.h | 4 ++-- src/smt_util/nary_builder.cpp | 4 ++-- src/smt_util/nary_builder.h | 2 +- src/theory/arith/approx_simplex.cpp | 4 ++-- src/theory/arith/approx_simplex.h | 2 +- src/theory/arith/arith_ite_utils.cpp | 4 ++-- src/theory/arith/arith_ite_utils.h | 4 ++-- src/theory/arith/arith_msum.cpp | 2 +- src/theory/arith/arith_msum.h | 4 ++-- src/theory/arith/arith_rewriter.cpp | 2 +- src/theory/arith/arith_rewriter.h | 4 ++-- src/theory/arith/arith_static_learner.cpp | 2 +- src/theory/arith/arith_static_learner.h | 4 ++-- src/theory/arith/arith_utilities.cpp | 4 ++-- src/theory/arith/arith_utilities.h | 4 ++-- src/theory/arith/arithvar.cpp | 2 +- src/theory/arith/arithvar.h | 2 +- src/theory/arith/arithvar_node_map.h | 4 ++-- src/theory/arith/attempt_solution_simplex.cpp | 4 ++-- src/theory/arith/attempt_solution_simplex.h | 2 +- src/theory/arith/bound_counts.h | 2 +- src/theory/arith/callbacks.cpp | 4 ++-- src/theory/arith/callbacks.h | 2 +- src/theory/arith/congruence_manager.cpp | 4 ++-- src/theory/arith/congruence_manager.h | 4 ++-- src/theory/arith/constraint.cpp | 4 ++-- src/theory/arith/constraint.h | 2 +- src/theory/arith/constraint_forward.h | 4 ++-- src/theory/arith/cut_log.cpp | 4 ++-- src/theory/arith/cut_log.h | 2 +- src/theory/arith/delta_rational.cpp | 2 +- src/theory/arith/delta_rational.h | 2 +- src/theory/arith/dio_solver.cpp | 4 ++-- src/theory/arith/dio_solver.h | 4 ++-- src/theory/arith/dual_simplex.cpp | 4 ++-- src/theory/arith/dual_simplex.h | 2 +- src/theory/arith/error_set.cpp | 4 ++-- src/theory/arith/error_set.h | 4 ++-- src/theory/arith/fc_simplex.cpp | 4 ++-- src/theory/arith/fc_simplex.h | 2 +- src/theory/arith/infer_bounds.cpp | 2 +- src/theory/arith/infer_bounds.h | 2 +- src/theory/arith/linear_equality.cpp | 4 ++-- src/theory/arith/linear_equality.h | 2 +- src/theory/arith/matrix.cpp | 2 +- src/theory/arith/matrix.h | 2 +- src/theory/arith/nl/nl_constraint.cpp | 4 ++-- src/theory/arith/nl/nl_constraint.h | 4 ++-- src/theory/arith/nl/nl_lemma_utils.cpp | 2 +- src/theory/arith/nl/nl_lemma_utils.h | 4 ++-- src/theory/arith/nl/nl_model.cpp | 4 ++-- src/theory/arith/nl/nl_model.h | 4 ++-- src/theory/arith/nl/nl_monomial.cpp | 4 ++-- src/theory/arith/nl/nl_monomial.h | 2 +- src/theory/arith/nl/nl_solver.cpp | 4 ++-- src/theory/arith/nl/nl_solver.h | 4 ++-- src/theory/arith/nl/nonlinear_extension.cpp | 2 +- src/theory/arith/nl/nonlinear_extension.h | 4 ++-- src/theory/arith/nl/transcendental_solver.cpp | 4 ++-- src/theory/arith/nl/transcendental_solver.h | 4 ++-- src/theory/arith/normal_form.cpp | 2 +- src/theory/arith/normal_form.h | 4 ++-- src/theory/arith/partial_model.cpp | 2 +- src/theory/arith/partial_model.h | 4 ++-- src/theory/arith/simplex.cpp | 2 +- src/theory/arith/simplex.h | 4 ++-- src/theory/arith/simplex_update.cpp | 2 +- src/theory/arith/simplex_update.h | 2 +- src/theory/arith/soi_simplex.cpp | 4 ++-- src/theory/arith/soi_simplex.h | 2 +- src/theory/arith/tableau.cpp | 2 +- src/theory/arith/tableau.h | 2 +- src/theory/arith/tableau_sizes.cpp | 2 +- src/theory/arith/tableau_sizes.h | 2 +- src/theory/arith/theory_arith.cpp | 4 ++-- src/theory/arith/theory_arith.h | 2 +- src/theory/arith/theory_arith_private.cpp | 4 ++-- src/theory/arith/theory_arith_private.h | 2 +- src/theory/arith/theory_arith_private_forward.h | 2 +- src/theory/arith/theory_arith_type_rules.h | 4 ++-- src/theory/arith/type_enumerator.h | 4 ++-- src/theory/arrays/array_info.cpp | 2 +- src/theory/arrays/array_info.h | 2 +- src/theory/arrays/array_proof_reconstruction.cpp | 2 +- src/theory/arrays/array_proof_reconstruction.h | 4 ++-- src/theory/arrays/static_fact_manager.cpp | 4 ++-- src/theory/arrays/static_fact_manager.h | 4 ++-- src/theory/arrays/theory_arrays.cpp | 2 +- src/theory/arrays/theory_arrays.h | 2 +- src/theory/arrays/theory_arrays_rewriter.cpp | 2 +- src/theory/arrays/theory_arrays_rewriter.h | 4 ++-- src/theory/arrays/theory_arrays_type_rules.h | 2 +- src/theory/arrays/type_enumerator.h | 2 +- src/theory/arrays/union_find.cpp | 2 +- src/theory/arrays/union_find.h | 4 ++-- src/theory/assertion.cpp | 4 ++-- src/theory/assertion.h | 4 ++-- src/theory/atom_requests.cpp | 4 ++-- src/theory/atom_requests.h | 4 ++-- src/theory/booleans/circuit_propagator.cpp | 2 +- src/theory/booleans/circuit_propagator.h | 2 +- src/theory/booleans/proof_checker.cpp | 4 ++-- src/theory/booleans/proof_checker.h | 4 ++-- src/theory/booleans/theory_bool.cpp | 2 +- src/theory/booleans/theory_bool.h | 4 ++-- src/theory/booleans/theory_bool_rewriter.cpp | 2 +- src/theory/booleans/theory_bool_rewriter.h | 4 ++-- src/theory/booleans/theory_bool_type_rules.h | 2 +- src/theory/booleans/type_enumerator.h | 4 ++-- src/theory/builtin/proof_checker.cpp | 2 +- src/theory/builtin/proof_checker.h | 2 +- src/theory/builtin/theory_builtin.cpp | 4 ++-- src/theory/builtin/theory_builtin.h | 4 ++-- src/theory/builtin/theory_builtin_rewriter.cpp | 4 ++-- src/theory/builtin/theory_builtin_rewriter.h | 4 ++-- src/theory/builtin/theory_builtin_type_rules.h | 2 +- src/theory/builtin/type_enumerator.cpp | 2 +- src/theory/builtin/type_enumerator.h | 2 +- src/theory/bv/abstraction.cpp | 2 +- src/theory/bv/abstraction.h | 4 ++-- src/theory/bv/bitblast/aig_bitblaster.cpp | 2 +- src/theory/bv/bitblast/aig_bitblaster.h | 2 +- src/theory/bv/bitblast/bitblast_strategies_template.h | 2 +- src/theory/bv/bitblast/bitblast_utils.h | 2 +- src/theory/bv/bitblast/bitblaster.h | 2 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 2 +- src/theory/bv/bitblast/eager_bitblaster.h | 2 +- src/theory/bv/bitblast/lazy_bitblaster.cpp | 2 +- src/theory/bv/bitblast/lazy_bitblaster.h | 4 ++-- src/theory/bv/bv_eager_solver.cpp | 2 +- src/theory/bv/bv_eager_solver.h | 2 +- src/theory/bv/bv_inequality_graph.cpp | 4 ++-- src/theory/bv/bv_inequality_graph.h | 4 ++-- src/theory/bv/bv_quick_check.cpp | 2 +- src/theory/bv/bv_quick_check.h | 4 ++-- src/theory/bv/bv_subtheory.h | 2 +- src/theory/bv/bv_subtheory_algebraic.cpp | 2 +- src/theory/bv/bv_subtheory_algebraic.h | 2 +- src/theory/bv/bv_subtheory_bitblast.cpp | 2 +- src/theory/bv/bv_subtheory_bitblast.h | 2 +- src/theory/bv/bv_subtheory_core.cpp | 2 +- src/theory/bv/bv_subtheory_core.h | 2 +- src/theory/bv/bv_subtheory_inequality.cpp | 2 +- src/theory/bv/bv_subtheory_inequality.h | 2 +- src/theory/bv/slicer.cpp | 4 ++-- src/theory/bv/slicer.h | 4 ++-- src/theory/bv/theory_bv.cpp | 2 +- src/theory/bv/theory_bv.h | 4 ++-- src/theory/bv/theory_bv_rewrite_rules.h | 2 +- .../bv/theory_bv_rewrite_rules_constant_evaluation.h | 2 +- src/theory/bv/theory_bv_rewrite_rules_core.h | 2 +- src/theory/bv/theory_bv_rewrite_rules_normalization.h | 2 +- .../bv/theory_bv_rewrite_rules_operator_elimination.h | 4 ++-- src/theory/bv/theory_bv_rewrite_rules_simplification.h | 2 +- src/theory/bv/theory_bv_rewriter.cpp | 2 +- src/theory/bv/theory_bv_rewriter.h | 4 ++-- src/theory/bv/theory_bv_type_rules.h | 4 ++-- src/theory/bv/theory_bv_utils.cpp | 4 ++-- src/theory/bv/theory_bv_utils.h | 4 ++-- src/theory/bv/type_enumerator.h | 2 +- src/theory/care_graph.h | 4 ++-- src/theory/datatypes/datatypes_rewriter.cpp | 4 ++-- src/theory/datatypes/datatypes_rewriter.h | 4 ++-- src/theory/datatypes/sygus_datatype_utils.cpp | 4 ++-- src/theory/datatypes/sygus_datatype_utils.h | 2 +- src/theory/datatypes/sygus_extension.cpp | 4 ++-- src/theory/datatypes/sygus_extension.h | 4 ++-- src/theory/datatypes/sygus_simple_sym.cpp | 4 ++-- src/theory/datatypes/sygus_simple_sym.h | 4 ++-- src/theory/datatypes/theory_datatypes.cpp | 4 ++-- src/theory/datatypes/theory_datatypes.h | 2 +- src/theory/datatypes/theory_datatypes_type_rules.h | 2 +- src/theory/datatypes/theory_datatypes_utils.cpp | 4 ++-- src/theory/datatypes/theory_datatypes_utils.h | 4 ++-- src/theory/datatypes/type_enumerator.cpp | 2 +- src/theory/datatypes/type_enumerator.h | 4 ++-- src/theory/decision_manager.cpp | 2 +- src/theory/decision_manager.h | 4 ++-- src/theory/decision_strategy.cpp | 2 +- src/theory/decision_strategy.h | 4 ++-- src/theory/eager_proof_generator.cpp | 2 +- src/theory/eager_proof_generator.h | 2 +- src/theory/engine_output_channel.cpp | 4 ++-- src/theory/engine_output_channel.h | 4 ++-- src/theory/evaluator.cpp | 2 +- src/theory/evaluator.h | 4 ++-- src/theory/example/ecdata.cpp | 2 +- src/theory/example/ecdata.h | 4 ++-- src/theory/example/theory_uf_tim.cpp | 4 ++-- src/theory/example/theory_uf_tim.h | 4 ++-- src/theory/ext_theory.cpp | 2 +- src/theory/ext_theory.h | 4 ++-- src/theory/fp/fp_converter.cpp | 4 ++-- src/theory/fp/fp_converter.h | 4 ++-- src/theory/fp/theory_fp.cpp | 4 ++-- src/theory/fp/theory_fp.h | 4 ++-- src/theory/fp/theory_fp_rewriter.cpp | 4 ++-- src/theory/fp/theory_fp_rewriter.h | 4 ++-- src/theory/fp/theory_fp_type_rules.h | 4 ++-- src/theory/fp/type_enumerator.h | 2 +- src/theory/interrupted.h | 4 ++-- src/theory/logic_info.cpp | 2 +- src/theory/logic_info.h | 2 +- src/theory/output_channel.h | 2 +- src/theory/quantifiers/alpha_equivalence.cpp | 4 ++-- src/theory/quantifiers/alpha_equivalence.h | 4 ++-- src/theory/quantifiers/anti_skolem.cpp | 4 ++-- src/theory/quantifiers/anti_skolem.h | 4 ++-- src/theory/quantifiers/bv_inverter.cpp | 2 +- src/theory/quantifiers/bv_inverter.h | 2 +- src/theory/quantifiers/bv_inverter_utils.cpp | 2 +- src/theory/quantifiers/bv_inverter_utils.h | 4 ++-- src/theory/quantifiers/candidate_rewrite_database.cpp | 2 +- src/theory/quantifiers/candidate_rewrite_database.h | 4 ++-- src/theory/quantifiers/candidate_rewrite_filter.cpp | 4 ++-- src/theory/quantifiers/candidate_rewrite_filter.h | 4 ++-- src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp | 2 +- src/theory/quantifiers/cegqi/ceg_arith_instantiator.h | 4 ++-- src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp | 4 ++-- src/theory/quantifiers/cegqi/ceg_bv_instantiator.h | 4 ++-- .../quantifiers/cegqi/ceg_bv_instantiator_utils.cpp | 4 ++-- .../quantifiers/cegqi/ceg_bv_instantiator_utils.h | 2 +- src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp | 4 ++-- src/theory/quantifiers/cegqi/ceg_dt_instantiator.h | 2 +- src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp | 2 +- src/theory/quantifiers/cegqi/ceg_epr_instantiator.h | 2 +- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 4 ++-- src/theory/quantifiers/cegqi/ceg_instantiator.h | 2 +- src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 4 ++-- src/theory/quantifiers/cegqi/inst_strategy_cegqi.h | 2 +- src/theory/quantifiers/cegqi/vts_term_cache.cpp | 4 ++-- src/theory/quantifiers/cegqi/vts_term_cache.h | 2 +- src/theory/quantifiers/conjecture_generator.cpp | 4 ++-- src/theory/quantifiers/conjecture_generator.h | 2 +- src/theory/quantifiers/dynamic_rewrite.cpp | 2 +- src/theory/quantifiers/dynamic_rewrite.h | 4 ++-- .../quantifiers/ematching/candidate_generator.cpp | 2 +- src/theory/quantifiers/ematching/candidate_generator.h | 2 +- src/theory/quantifiers/ematching/ho_trigger.cpp | 4 ++-- src/theory/quantifiers/ematching/ho_trigger.h | 4 ++-- .../quantifiers/ematching/inst_match_generator.cpp | 4 ++-- src/theory/quantifiers/ematching/inst_match_generator.h | 2 +- .../quantifiers/ematching/inst_strategy_e_matching.cpp | 4 ++-- .../quantifiers/ematching/inst_strategy_e_matching.h | 2 +- .../quantifiers/ematching/instantiation_engine.cpp | 2 +- src/theory/quantifiers/ematching/instantiation_engine.h | 2 +- src/theory/quantifiers/ematching/trigger.cpp | 4 ++-- src/theory/quantifiers/ematching/trigger.h | 4 ++-- src/theory/quantifiers/equality_infer.cpp | 2 +- src/theory/quantifiers/equality_infer.h | 4 ++-- src/theory/quantifiers/equality_query.cpp | 4 ++-- src/theory/quantifiers/equality_query.h | 2 +- src/theory/quantifiers/expr_miner.cpp | 2 +- src/theory/quantifiers/expr_miner.h | 4 ++-- src/theory/quantifiers/expr_miner_manager.cpp | 2 +- src/theory/quantifiers/expr_miner_manager.h | 4 ++-- src/theory/quantifiers/extended_rewrite.cpp | 4 ++-- src/theory/quantifiers/extended_rewrite.h | 4 ++-- src/theory/quantifiers/first_order_model.cpp | 2 +- src/theory/quantifiers/first_order_model.h | 2 +- src/theory/quantifiers/fmf/bounded_integers.cpp | 4 ++-- src/theory/quantifiers/fmf/bounded_integers.h | 4 ++-- src/theory/quantifiers/fmf/full_model_check.cpp | 4 ++-- src/theory/quantifiers/fmf/full_model_check.h | 4 ++-- src/theory/quantifiers/fmf/model_builder.cpp | 2 +- src/theory/quantifiers/fmf/model_builder.h | 4 ++-- src/theory/quantifiers/fmf/model_engine.cpp | 2 +- src/theory/quantifiers/fmf/model_engine.h | 4 ++-- src/theory/quantifiers/fun_def_evaluator.cpp | 4 ++-- src/theory/quantifiers/fun_def_evaluator.h | 2 +- src/theory/quantifiers/fun_def_process.cpp | 4 ++-- src/theory/quantifiers/fun_def_process.h | 4 ++-- src/theory/quantifiers/inst_match.cpp | 2 +- src/theory/quantifiers/inst_match.h | 4 ++-- src/theory/quantifiers/inst_match_trie.cpp | 2 +- src/theory/quantifiers/inst_match_trie.h | 4 ++-- src/theory/quantifiers/inst_strategy_enumerative.cpp | 2 +- src/theory/quantifiers/inst_strategy_enumerative.h | 4 ++-- src/theory/quantifiers/instantiate.cpp | 4 ++-- src/theory/quantifiers/instantiate.h | 2 +- src/theory/quantifiers/lazy_trie.cpp | 2 +- src/theory/quantifiers/lazy_trie.h | 4 ++-- src/theory/quantifiers/proof_checker.cpp | 2 +- src/theory/quantifiers/proof_checker.h | 2 +- src/theory/quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/quant_conflict_find.h | 2 +- src/theory/quantifiers/quant_epr.cpp | 2 +- src/theory/quantifiers/quant_epr.h | 4 ++-- src/theory/quantifiers/quant_relevance.cpp | 2 +- src/theory/quantifiers/quant_relevance.h | 2 +- src/theory/quantifiers/quant_rep_bound_ext.cpp | 4 ++-- src/theory/quantifiers/quant_rep_bound_ext.h | 4 ++-- src/theory/quantifiers/quant_split.cpp | 4 ++-- src/theory/quantifiers/quant_split.h | 2 +- src/theory/quantifiers/quant_util.cpp | 2 +- src/theory/quantifiers/quant_util.h | 4 ++-- src/theory/quantifiers/quantifiers_attributes.cpp | 2 +- src/theory/quantifiers/quantifiers_attributes.h | 4 ++-- src/theory/quantifiers/quantifiers_rewriter.cpp | 4 ++-- src/theory/quantifiers/quantifiers_rewriter.h | 4 ++-- src/theory/quantifiers/query_generator.cpp | 4 ++-- src/theory/quantifiers/query_generator.h | 4 ++-- src/theory/quantifiers/relevant_domain.cpp | 4 ++-- src/theory/quantifiers/relevant_domain.h | 2 +- src/theory/quantifiers/single_inv_partition.cpp | 4 ++-- src/theory/quantifiers/single_inv_partition.h | 4 ++-- src/theory/quantifiers/skolemize.cpp | 2 +- src/theory/quantifiers/skolemize.h | 4 ++-- src/theory/quantifiers/solution_filter.cpp | 4 ++-- src/theory/quantifiers/solution_filter.h | 4 ++-- src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 4 ++-- src/theory/quantifiers/sygus/ce_guided_single_inv.h | 2 +- .../quantifiers/sygus/ce_guided_single_inv_sol.cpp | 4 ++-- src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h | 4 ++-- src/theory/quantifiers/sygus/cegis.cpp | 4 ++-- src/theory/quantifiers/sygus/cegis.h | 4 ++-- src/theory/quantifiers/sygus/cegis_core_connective.cpp | 4 ++-- src/theory/quantifiers/sygus/cegis_core_connective.h | 2 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 4 ++-- src/theory/quantifiers/sygus/cegis_unif.h | 2 +- .../quantifiers/sygus/enum_stream_substitution.cpp | 2 +- src/theory/quantifiers/sygus/enum_stream_substitution.h | 4 ++-- src/theory/quantifiers/sygus/example_eval_cache.cpp | 2 +- src/theory/quantifiers/sygus/example_eval_cache.h | 2 +- src/theory/quantifiers/sygus/example_infer.cpp | 2 +- src/theory/quantifiers/sygus/example_infer.h | 4 ++-- src/theory/quantifiers/sygus/example_min_eval.cpp | 2 +- src/theory/quantifiers/sygus/example_min_eval.h | 2 +- src/theory/quantifiers/sygus/sygus_abduct.cpp | 2 +- src/theory/quantifiers/sygus/sygus_abduct.h | 2 +- src/theory/quantifiers/sygus/sygus_enumerator.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_enumerator.h | 4 ++-- src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_enumerator_basic.h | 2 +- src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_eval_unfold.h | 4 ++-- src/theory/quantifiers/sygus/sygus_explain.cpp | 2 +- src/theory/quantifiers/sygus/sygus_explain.h | 4 ++-- src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_grammar_cons.h | 4 ++-- src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 2 +- src/theory/quantifiers/sygus/sygus_grammar_norm.h | 2 +- src/theory/quantifiers/sygus/sygus_grammar_red.cpp | 2 +- src/theory/quantifiers/sygus/sygus_grammar_red.h | 4 ++-- src/theory/quantifiers/sygus/sygus_invariance.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_invariance.h | 2 +- src/theory/quantifiers/sygus/sygus_module.cpp | 2 +- src/theory/quantifiers/sygus/sygus_module.h | 4 ++-- src/theory/quantifiers/sygus/sygus_pbe.cpp | 2 +- src/theory/quantifiers/sygus/sygus_pbe.h | 4 ++-- src/theory/quantifiers/sygus/sygus_process_conj.cpp | 2 +- src/theory/quantifiers/sygus/sygus_process_conj.h | 4 ++-- src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 +- src/theory/quantifiers/sygus/sygus_repair_const.h | 4 ++-- src/theory/quantifiers/sygus/sygus_stats.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_stats.h | 2 +- src/theory/quantifiers/sygus/sygus_unif.cpp | 2 +- src/theory/quantifiers/sygus/sygus_unif.h | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_io.h | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_rl.h | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_strat.h | 4 ++-- src/theory/quantifiers/sygus/synth_conjecture.cpp | 4 ++-- src/theory/quantifiers/sygus/synth_conjecture.h | 4 ++-- src/theory/quantifiers/sygus/synth_engine.cpp | 4 ++-- src/theory/quantifiers/sygus/synth_engine.h | 2 +- src/theory/quantifiers/sygus/term_database_sygus.cpp | 4 ++-- src/theory/quantifiers/sygus/term_database_sygus.h | 2 +- src/theory/quantifiers/sygus/transition_inference.cpp | 4 ++-- src/theory/quantifiers/sygus/transition_inference.h | 2 +- src/theory/quantifiers/sygus/type_info.cpp | 4 ++-- src/theory/quantifiers/sygus/type_info.h | 2 +- src/theory/quantifiers/sygus/type_node_id_trie.cpp | 2 +- src/theory/quantifiers/sygus/type_node_id_trie.h | 2 +- src/theory/quantifiers/sygus_inst.cpp | 2 +- src/theory/quantifiers/sygus_sampler.cpp | 4 ++-- src/theory/quantifiers/sygus_sampler.h | 4 ++-- src/theory/quantifiers/term_database.cpp | 4 ++-- src/theory/quantifiers/term_database.h | 4 ++-- src/theory/quantifiers/term_enumeration.cpp | 2 +- src/theory/quantifiers/term_enumeration.h | 4 ++-- src/theory/quantifiers/term_util.cpp | 4 ++-- src/theory/quantifiers/term_util.h | 2 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- src/theory/quantifiers/theory_quantifiers.h | 4 ++-- src/theory/quantifiers/theory_quantifiers_type_rules.h | 2 +- src/theory/quantifiers_engine.cpp | 4 ++-- src/theory/quantifiers_engine.h | 2 +- src/theory/rep_set.cpp | 2 +- src/theory/rep_set.h | 4 ++-- src/theory/rewriter.cpp | 4 ++-- src/theory/rewriter.h | 4 ++-- src/theory/rewriter_attributes.h | 2 +- src/theory/rewriter_tables_template.h | 4 ++-- src/theory/sep/theory_sep.cpp | 2 +- src/theory/sep/theory_sep.h | 2 +- src/theory/sep/theory_sep_rewriter.cpp | 2 +- src/theory/sep/theory_sep_rewriter.h | 4 ++-- src/theory/sep/theory_sep_type_rules.h | 4 ++-- src/theory/sets/cardinality_extension.cpp | 4 ++-- src/theory/sets/cardinality_extension.h | 4 ++-- src/theory/sets/inference_manager.cpp | 4 ++-- src/theory/sets/inference_manager.h | 2 +- src/theory/sets/normal_form.h | 2 +- src/theory/sets/rels_utils.h | 2 +- src/theory/sets/skolem_cache.cpp | 2 +- src/theory/sets/skolem_cache.h | 2 +- src/theory/sets/solver_state.cpp | 4 ++-- src/theory/sets/solver_state.h | 4 ++-- src/theory/sets/theory_sets.cpp | 4 ++-- src/theory/sets/theory_sets.h | 2 +- src/theory/sets/theory_sets_private.cpp | 4 ++-- src/theory/sets/theory_sets_private.h | 4 ++-- src/theory/sets/theory_sets_rels.cpp | 4 ++-- src/theory/sets/theory_sets_rels.h | 2 +- src/theory/sets/theory_sets_rewriter.cpp | 2 +- src/theory/sets/theory_sets_rewriter.h | 4 ++-- src/theory/sets/theory_sets_type_enumerator.cpp | 2 +- src/theory/sets/theory_sets_type_enumerator.h | 2 +- src/theory/sets/theory_sets_type_rules.h | 2 +- src/theory/shared_terms_database.cpp | 2 +- src/theory/shared_terms_database.h | 2 +- src/theory/smt_engine_subsolver.cpp | 4 ++-- src/theory/smt_engine_subsolver.h | 4 ++-- src/theory/sort_inference.cpp | 4 ++-- src/theory/sort_inference.h | 4 ++-- src/theory/strings/arith_entail.cpp | 2 +- src/theory/strings/arith_entail.h | 2 +- src/theory/strings/base_solver.cpp | 4 ++-- src/theory/strings/base_solver.h | 4 ++-- src/theory/strings/core_solver.cpp | 6 +++--- src/theory/strings/core_solver.h | 6 +++--- src/theory/strings/eqc_info.cpp | 4 ++-- src/theory/strings/eqc_info.h | 2 +- src/theory/strings/extf_solver.cpp | 6 +++--- src/theory/strings/extf_solver.h | 6 +++--- src/theory/strings/infer_info.cpp | 4 ++-- src/theory/strings/infer_info.h | 4 ++-- src/theory/strings/inference_manager.cpp | 4 ++-- src/theory/strings/inference_manager.h | 4 ++-- src/theory/strings/normal_form.cpp | 4 ++-- src/theory/strings/normal_form.h | 4 ++-- src/theory/strings/regexp_elim.cpp | 4 ++-- src/theory/strings/regexp_elim.h | 4 ++-- src/theory/strings/regexp_entail.cpp | 4 ++-- src/theory/strings/regexp_entail.h | 4 ++-- src/theory/strings/regexp_operation.cpp | 4 ++-- src/theory/strings/regexp_operation.h | 4 ++-- src/theory/strings/regexp_solver.cpp | 4 ++-- src/theory/strings/regexp_solver.h | 2 +- src/theory/strings/rewrites.cpp | 4 ++-- src/theory/strings/rewrites.h | 4 ++-- src/theory/strings/sequences_rewriter.cpp | 2 +- src/theory/strings/sequences_rewriter.h | 4 ++-- src/theory/strings/sequences_stats.cpp | 2 +- src/theory/strings/sequences_stats.h | 2 +- src/theory/strings/skolem_cache.cpp | 2 +- src/theory/strings/skolem_cache.h | 4 ++-- src/theory/strings/solver_state.cpp | 4 ++-- src/theory/strings/solver_state.h | 4 ++-- src/theory/strings/strings_entail.cpp | 2 +- src/theory/strings/strings_entail.h | 2 +- src/theory/strings/strings_fmf.cpp | 4 ++-- src/theory/strings/strings_fmf.h | 4 ++-- src/theory/strings/strings_rewriter.cpp | 4 ++-- src/theory/strings/strings_rewriter.h | 4 ++-- src/theory/strings/term_registry.cpp | 4 ++-- src/theory/strings/term_registry.h | 6 +++--- src/theory/strings/theory_strings.cpp | 4 ++-- src/theory/strings/theory_strings.h | 2 +- src/theory/strings/theory_strings_preprocess.cpp | 4 ++-- src/theory/strings/theory_strings_preprocess.h | 4 ++-- src/theory/strings/theory_strings_type_rules.h | 4 ++-- src/theory/strings/theory_strings_utils.cpp | 4 ++-- src/theory/strings/theory_strings_utils.h | 4 ++-- src/theory/strings/type_enumerator.cpp | 4 ++-- src/theory/strings/type_enumerator.h | 4 ++-- src/theory/strings/word.cpp | 2 +- src/theory/strings/word.h | 4 ++-- src/theory/subs_minimize.cpp | 4 ++-- src/theory/subs_minimize.h | 4 ++-- src/theory/substitutions.cpp | 2 +- src/theory/substitutions.h | 2 +- src/theory/term_registration_visitor.cpp | 2 +- src/theory/term_registration_visitor.h | 2 +- src/theory/theory.cpp | 4 ++-- src/theory/theory.h | 4 ++-- src/theory/theory_engine.cpp | 4 ++-- src/theory/theory_engine.h | 4 ++-- src/theory/theory_id.cpp | 17 +++++++++++++++++ src/theory/theory_id.h | 17 +++++++++++++++++ src/theory/theory_model.cpp | 2 +- src/theory/theory_model.h | 2 +- src/theory/theory_model_builder.cpp | 2 +- src/theory/theory_model_builder.h | 4 ++-- src/theory/theory_preprocessor.cpp | 4 ++-- src/theory/theory_preprocessor.h | 4 ++-- src/theory/theory_proof_step_buffer.cpp | 2 +- src/theory/theory_proof_step_buffer.h | 2 +- src/theory/theory_registrar.h | 4 ++-- src/theory/theory_rewriter.h | 4 ++-- src/theory/theory_test_utils.h | 4 ++-- src/theory/theory_traits_template.h | 4 ++-- src/theory/trust_node.cpp | 2 +- src/theory/trust_node.h | 2 +- src/theory/type_enumerator.h | 2 +- src/theory/type_enumerator_template.cpp | 4 ++-- src/theory/type_set.cpp | 2 +- src/theory/type_set.h | 4 ++-- src/theory/uf/cardinality_extension.cpp | 2 +- src/theory/uf/cardinality_extension.h | 2 +- src/theory/uf/equality_engine.cpp | 4 ++-- src/theory/uf/equality_engine.h | 4 ++-- src/theory/uf/equality_engine_types.h | 4 ++-- src/theory/uf/ho_extension.cpp | 4 ++-- src/theory/uf/ho_extension.h | 2 +- src/theory/uf/proof_checker.cpp | 4 ++-- src/theory/uf/proof_checker.h | 4 ++-- src/theory/uf/symmetry_breaker.cpp | 4 ++-- src/theory/uf/symmetry_breaker.h | 2 +- src/theory/uf/theory_uf.cpp | 2 +- src/theory/uf/theory_uf.h | 4 ++-- src/theory/uf/theory_uf_model.cpp | 4 ++-- src/theory/uf/theory_uf_model.h | 4 ++-- src/theory/uf/theory_uf_rewriter.h | 2 +- src/theory/uf/theory_uf_type_rules.h | 2 +- src/theory/valuation.cpp | 2 +- src/theory/valuation.h | 2 +- src/util/abstract_value.cpp | 2 +- src/util/abstract_value.h | 2 +- src/util/bin_heap.h | 4 ++-- src/util/bitvector.cpp | 2 +- src/util/bitvector.h | 4 ++-- src/util/bool.h | 4 ++-- src/util/cardinality.cpp | 4 ++-- src/util/cardinality.h | 4 ++-- src/util/dense_map.h | 2 +- src/util/divisible.cpp | 2 +- src/util/divisible.h | 4 ++-- src/util/floatingpoint.cpp | 4 ++-- src/util/floatingpoint.h.in | 4 ++-- src/util/gmp_util.h | 4 ++-- src/util/hash.h | 4 ++-- src/util/index.cpp | 2 +- src/util/index.h | 4 ++-- src/util/integer.h.in | 2 +- src/util/integer_cln_imp.cpp | 2 +- src/util/integer_cln_imp.h | 2 +- src/util/integer_gmp_imp.cpp | 2 +- src/util/integer_gmp_imp.h | 2 +- src/util/maybe.h | 4 ++-- src/util/ostream_util.cpp | 2 +- src/util/ostream_util.h | 4 ++-- src/util/proof.h | 4 ++-- src/util/random.cpp | 2 +- src/util/random.h | 4 ++-- src/util/rational.h.in | 2 +- src/util/rational_cln_imp.cpp | 2 +- src/util/rational_cln_imp.h | 2 +- src/util/rational_gmp_imp.cpp | 2 +- src/util/rational_gmp_imp.h | 2 +- src/util/regexp.cpp | 2 +- src/util/regexp.h | 2 +- src/util/resource_manager.cpp | 4 ++-- src/util/resource_manager.h | 4 ++-- src/util/result.cpp | 4 ++-- src/util/result.h | 4 ++-- src/util/safe_print.cpp | 4 ++-- src/util/safe_print.h | 4 ++-- src/util/sampler.cpp | 2 +- src/util/sampler.h | 4 ++-- src/util/sexpr.cpp | 2 +- src/util/sexpr.h | 2 +- src/util/smt2_quote_string.cpp | 4 ++-- src/util/smt2_quote_string.h | 4 ++-- src/util/statistics.cpp | 2 +- src/util/statistics.h | 4 ++-- src/util/statistics_registry.cpp | 4 ++-- src/util/statistics_registry.h | 2 +- src/util/string.cpp | 4 ++-- src/util/string.h | 2 +- src/util/tuple.h | 4 ++-- src/util/unsafe_interrupt_exception.h | 4 ++-- src/util/utility.cpp | 2 +- src/util/utility.h | 2 +- test/java/BitVectors.java | 4 ++-- test/java/BitVectorsAndArrays.java | 4 ++-- test/java/Combination.java | 4 ++-- test/java/HelloWorld.java | 4 ++-- test/java/LinearArith.java | 4 ++-- test/system/CVC4JavaTest.java | 2 +- test/system/boilerplate.cpp | 4 ++-- test/system/ouroborous.cpp | 2 +- test/system/reset_assertions.cpp | 2 +- test/system/sep_log_api.cpp | 2 +- test/system/smt2_compliance.cpp | 2 +- test/system/statistics.cpp | 4 ++-- test/system/two_smt_engines.cpp | 4 ++-- test/unit/api/datatype_api_black.h | 4 ++-- test/unit/api/grammar_black.h | 4 ++-- test/unit/api/op_black.h | 4 ++-- test/unit/api/solver_black.h | 4 ++-- test/unit/api/sort_black.h | 4 ++-- test/unit/api/term_black.h | 4 ++-- test/unit/base/map_util_black.h | 2 +- test/unit/context/cdlist_black.h | 2 +- test/unit/context/cdmap_black.h | 4 ++-- test/unit/context/cdmap_white.h | 4 ++-- test/unit/context/cdo_black.h | 2 +- test/unit/context/context_black.h | 2 +- test/unit/context/context_mm_black.h | 4 ++-- test/unit/context/context_white.h | 2 +- test/unit/expr/attribute_black.h | 2 +- test/unit/expr/attribute_white.h | 2 +- test/unit/expr/expr_manager_public.h | 2 +- test/unit/expr/expr_public.h | 2 +- test/unit/expr/kind_black.h | 2 +- test/unit/expr/kind_map_black.h | 2 +- test/unit/expr/node_algorithm_black.h | 2 +- test/unit/expr/node_black.h | 2 +- test/unit/expr/node_builder_black.h | 4 ++-- test/unit/expr/node_manager_black.h | 2 +- test/unit/expr/node_manager_white.h | 2 +- test/unit/expr/node_self_iterator_black.h | 2 +- test/unit/expr/node_traversal_black.h | 2 +- test/unit/expr/node_white.h | 2 +- test/unit/expr/symbol_table_black.h | 2 +- test/unit/expr/type_cardinality_public.h | 2 +- test/unit/expr/type_node_white.h | 2 +- test/unit/main/interactive_shell_black.h | 4 ++-- test/unit/memory.h | 2 +- test/unit/parser/parser_black.h | 2 +- test/unit/parser/parser_builder_black.h | 2 +- test/unit/preprocessing/pass_bv_gauss_white.h | 4 ++-- test/unit/proof/drat_proof_black.h | 2 +- test/unit/proof/er_proof_black.h | 2 +- test/unit/proof/lfsc_proof_printer_black.h | 2 +- test/unit/proof/lrat_proof_black.h | 4 ++-- test/unit/proof/utils.h | 2 +- test/unit/prop/cnf_stream_white.h | 2 +- test/unit/test_utils.h | 2 +- test/unit/theory/evaluator_white.h | 2 +- test/unit/theory/logic_info_white.h | 2 +- test/unit/theory/regexp_operation_black.h | 4 ++-- test/unit/theory/sequences_rewriter_white.h | 4 ++-- test/unit/theory/theory_arith_white.h | 4 ++-- test/unit/theory/theory_black.h | 2 +- test/unit/theory/theory_bv_rewriter_white.h | 2 +- test/unit/theory/theory_bv_white.h | 2 +- test/unit/theory/theory_engine_white.h | 2 +- .../theory/theory_quantifiers_bv_instantiator_white.h | 2 +- test/unit/theory/theory_quantifiers_bv_inverter_white.h | 4 ++-- test/unit/theory/theory_sets_type_enumerator_white.h | 4 ++-- test/unit/theory/theory_strings_skolem_cache_black.h | 2 +- test/unit/theory/theory_strings_word_white.h | 2 +- test/unit/theory/theory_white.h | 2 +- test/unit/theory/type_enumerator_white.h | 4 ++-- test/unit/util/array_store_all_black.h | 4 ++-- test/unit/util/assert_white.h | 4 ++-- test/unit/util/binary_heap_black.h | 4 ++-- test/unit/util/bitvector_black.h | 2 +- test/unit/util/boolean_simplification_black.h | 2 +- test/unit/util/cardinality_public.h | 2 +- test/unit/util/check_white.h | 4 ++-- test/unit/util/configuration_black.h | 2 +- test/unit/util/datatype_black.h | 2 +- test/unit/util/exception_black.h | 2 +- test/unit/util/integer_black.h | 2 +- test/unit/util/integer_white.h | 2 +- test/unit/util/listener_black.h | 2 +- test/unit/util/output_black.h | 2 +- test/unit/util/rational_black.h | 2 +- test/unit/util/rational_white.h | 2 +- test/unit/util/stats_black.h | 2 +- 1142 files changed, 1790 insertions(+), 1754 deletions(-) (limited to 'src/expr/skolem_manager.h') diff --git a/contrib/get-authors b/contrib/get-authors index 0fb3f6ae1..80c4f57a5 100755 --- a/contrib/get-authors +++ b/contrib/get-authors @@ -1,7 +1,7 @@ #!/bin/sh # # get-authors -# Copyright (c) 2009-2019 The CVC4 Project +# Copyright (c) 2009-2020 The CVC4 Project # # usage: get-authors [ files... ] # @@ -65,6 +65,8 @@ while [ $# -gt 0 ]; do sed 's/justinxu421/Justin Xu/' | \ sed 's/yoni206/Yoni Zohar/' | \ sed 's/ayveejay/Andrew V. Jones/' | \ + sed 's/FabianWolff/Fabian Wolff/' | \ + sed 's/mudathirmahgoub/Mudathir Mohamed/' | \ # Determine top three contributors sort | uniq -c | sort -rn | head -n3 | \ diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 148392aab..bbe0ebb12 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -1,7 +1,7 @@ #!/usr/bin/perl -w # # update-copyright.pl -# Copyright (c) 2009-2019 The CVC4 Project +# Copyright (c) 2009-2020 The CVC4 Project # # usage: update-copyright [-m] [files/directories...] # update-copyright [-h | --help] @@ -47,7 +47,7 @@ $excluded_paths .= ')$'; # Years of copyright for the template. E.g., the string # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever. -my $years = '2009-2019'; +my $years = '2009-2020'; my $standard_template = <