diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-23 11:05:38 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-23 11:05:38 -0700 |
commit | f66f40912490226291d5af6c1f8b66e9ba6d7633 (patch) | |
tree | 5dc889390b7107cab051472e3bedd8ac151ab8f7 /src/theory/arith/arith_ite_utils.cpp | |
parent | f522d1e63e581cadeb987987ba3e3b0bd88f2e08 (diff) |
Refactor ITE simplification preprocessing pass. (#2360)
Diffstat (limited to 'src/theory/arith/arith_ite_utils.cpp')
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index a683d2bbb..5b51e162d 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -2,7 +2,7 @@ /*! \file arith_ite_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Kshitij Bansal + ** Tim King, Aina Niemetz, Kshitij Bansal ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -21,9 +21,9 @@ #include "base/output.h" #include "options/smt_options.h" +#include "preprocessing/util/ite_utilities.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" -#include "theory/ite_utilities.h" #include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/theory_model.h" @@ -140,18 +140,19 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ Unreachable(); } -ArithIteUtils::ArithIteUtils(ContainsTermITEVisitor& contains, - context::Context* uc, - TheoryModel* model) - : d_contains(contains) - , d_subs(NULL) - , d_model(model) - , d_one(1) - , d_subcount(uc, 0) - , d_skolems(uc) - , d_implies() - , d_skolemsAdded() - , d_orBinEqs() +ArithIteUtils::ArithIteUtils( + preprocessing::util::ContainsTermITEVisitor& contains, + context::Context* uc, + TheoryModel* model) + : d_contains(contains), + d_subs(NULL), + d_model(model), + d_one(1), + d_subcount(uc, 0), + d_skolems(uc), + d_implies(), + d_skolemsAdded(), + d_orBinEqs() { d_subs = new SubstitutionMap(uc); } |