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 | |
parent | f522d1e63e581cadeb987987ba3e3b0bd88f2e08 (diff) |
Refactor ITE simplification preprocessing pass. (#2360)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 29 | ||||
-rw-r--r-- | src/theory/arith/arith_ite_utils.h | 36 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 4 |
3 files changed, 38 insertions, 31 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); } diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index 7950ef05f..2c6a30758 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -2,7 +2,7 @@ /*! \file arith_ite_utils.h ** \verbatim ** Top contributors (to current version): - ** Tim King + ** Tim King, Aina Niemetz ** 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. @@ -29,15 +29,21 @@ #include "context/cdinsert_hashmap.h" namespace CVC4 { -namespace theory { +namespace preprocessing { +namespace util { class ContainsTermITEVisitor; +} +} // namespace preprocessing + +namespace theory { + class SubstitutionMap; class TheoryModel; namespace arith { class ArithIteUtils { - ContainsTermITEVisitor& d_contains; + preprocessing::util::ContainsTermITEVisitor& d_contains; SubstitutionMap* d_subs; TheoryModel* d_model; @@ -68,24 +74,24 @@ class ArithIteUtils { std::vector<Node> d_orBinEqs; public: - ArithIteUtils(ContainsTermITEVisitor& contains, - context::Context* userContext, - TheoryModel* model); - ~ArithIteUtils(); + ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains, + context::Context* userContext, + TheoryModel* model); + ~ArithIteUtils(); - //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256))) + //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256))) - /** removes common sums variables sums from term ites. */ - Node reduceVariablesInItes(Node n); + /** removes common sums variables sums from term ites. */ + Node reduceVariablesInItes(Node n); - Node reduceConstantIteByGCD(Node n); + Node reduceConstantIteByGCD(Node n); - void clear(); + void clear(); - Node applySubstitutions(TNode f); - unsigned getSubCount() const; + Node applySubstitutions(TNode f); + unsigned getSubCount() const; - void learnSubstitutions(const std::vector<Node>& assertions); + void learnSubstitutions(const std::vector<Node>& assertions); private: /* applies this to all children of n and constructs the result */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 968970049..89550295a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -36,6 +36,7 @@ #include "expr/node_builder.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() +#include "preprocessing/util/ite_utilities.h" #include "smt/logic_exception.h" #include "smt/logic_request.h" #include "smt/smt_statistics_registry.h" @@ -59,7 +60,6 @@ #include "theory/arith/simplex.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" -#include "theory/ite_utilities.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -5374,7 +5374,7 @@ bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational } // TODO Speed up - ContainsTermITEVisitor ctv; + preprocessing::util::ContainsTermITEVisitor ctv; if(ctv.containsTermITE(t)){ return false; } |