diff options
Diffstat (limited to 'src/theory/arith/arith_ite_utils.h')
-rw-r--r-- | src/theory/arith/arith_ite_utils.h | 100 |
1 files changed, 100 insertions, 0 deletions
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h new file mode 100644 index 000000000..fab0f32cb --- /dev/null +++ b/src/theory/arith/arith_ite_utils.h @@ -0,0 +1,100 @@ + + + + + +// Pass 1: label the ite as (constant) or (+ constant variable) + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H +#define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H + +#include "expr/node.h" +#include <ext/hash_map> +#include <ext/hash_set> +#include "context/cdo.h" +#include "context/cdtrail_hashmap.h" + +namespace CVC4 { +namespace theory { +class ContainsTermITEVistor; +class SubstitutionMap; +class TheoryModel; + +namespace arith { + +class ArithIteUtils { + ContainsTermITEVistor& d_contains; + SubstitutionMap* d_subs; + TheoryModel* d_model; + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + // cache for reduce vars + NodeMap d_reduceVar; // if reduceVars[n].isNull(), treat reduceVars[n] == n + + // reduceVars[n] = d_constants[n] + d_varParts[n] + NodeMap d_constants; // d_constants[n] is a constant ite tree + NodeMap d_varParts; // d_varParts[n] is a polynomial + + + NodeMap d_reduceGcd; + typedef std::hash_map<Node, Integer, NodeHashFunction> NodeIntegerMap; + NodeIntegerMap d_gcds; + + Integer d_one; + + context::CDO<unsigned> d_subcount; + typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeMap; + CDNodeMap d_skolems; + + typedef std::map<Node, std::set<Node> > ImpMap; + ImpMap d_implies; + + std::vector<Node> d_skolemsAdded; + + std::vector<Node> d_orBinEqs; + +public: + ArithIteUtils(ContainsTermITEVistor& contains, + context::Context* userContext, + TheoryModel* model); + ~ArithIteUtils(); + + //(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); + + Node reduceConstantIteByGCD(Node n); + + void clear(); + + Node applySubstitutions(TNode f); + unsigned getSubCount() const; + + void learnSubstitutions(const std::vector<Node>& assertions); + +private: + /* applies this to all children of n and constructs the result */ + Node applyReduceVariablesInItes(Node n); + + const Integer& gcdIte(Node n); + Node reduceIteConstantIteByGCD_rec(Node n, const Rational& q); + Node reduceIteConstantIteByGCD(Node n); + + void addSubstitution(TNode f, TNode t); + Node selectForCmp(Node n) const; + + void collectAssertions(TNode assertion); + void addImplications(Node x, Node y); + Node findIteCnd(TNode tb, TNode fb) const; + bool solveBinOr(TNode binor); + +}; /* class ArithIteUtils */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */ |