diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-09-22 15:40:48 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 17:40:48 -0500 |
| commit | 30e6dc83aed15ef002087e55cf228f0735c63f40 (patch) | |
| tree | 76547d252a34cc2b56015957e2d5f9740b1002b2 /src/theory/theory_state.h | |
| parent | e4a29a6033ecc7ba5ec266f37e8f151f09ead020 (diff) | |
Add simple BV solver (#5065)
This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.
Diffstat (limited to 'src/theory/theory_state.h')
| -rw-r--r-- | src/theory/theory_state.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 1c73912d7..187d586a1 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -80,6 +80,9 @@ class TheoryState */ TheoryModel* getModel(); + /** Returns true if n has a current SAT assignment and stores it in value. */ + virtual bool hasSatValue(TNode n, bool& value) const; + protected: /** Pointer to the SAT context object used by the theory. */ context::Context* d_context; |