diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-11 12:59:13 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-11 13:07:55 -0600 |
| commit | e2f28f39b3a3749a5eeed5294f25bec1e210b129 (patch) | |
| tree | 6bd5fc8c198139bdf518ad3ae443d87eac13816f /src/theory/bv/theory_bv.h | |
| parent | 4ee85fbbe8f1bbc6261b804916f897b26d500fbf (diff) | |
Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions.
Diffstat (limited to 'src/theory/bv/theory_bv.h')
| -rw-r--r-- | src/theory/bv/theory_bv.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 3cf471356..9973b0736 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -70,6 +70,8 @@ public: void preRegisterTerm(TNode n); void check(Effort e); + + bool needsCheckLastEffort(); void propagate(Effort e); @@ -175,7 +177,14 @@ private: AbstractionModule* d_abstractionModule; bool d_isCoreTheory; bool d_calledPreregister; - + + //for extended functions + bool d_needsLastCallCheck; + context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer; + context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer; + bool doExtfInferences( std::vector< Node >& terms ); + bool doExtfReductions( std::vector< Node >& terms ); + bool wasPropagatedBySubtheory(TNode literal) const { return d_propagatedBy.find(literal) != d_propagatedBy.end(); } |