diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-15 03:58:54 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-15 01:58:54 -0700 |
| commit | eb58f1ef8917c5d57d64c54f9188b0ed489b47c1 (patch) | |
| tree | c7d4fc304f72dc06b10f052ecf29d5f629fc0193 /src/theory/valuation.h | |
| parent | a932b4478e397d760d9457be7c6a80f9ba724391 (diff) | |
Simplify entailment check interface (#4744)
The generality of this interface is unnecessary.
Diffstat (limited to 'src/theory/valuation.h')
| -rw-r--r-- | src/theory/valuation.h | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 01ae61fcb..b1985971a 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -30,8 +30,6 @@ class TheoryEngine; namespace theory { -class EntailmentCheckParameters; -class EntailmentCheckSideEffects; class TheoryModel; /** @@ -141,11 +139,7 @@ public: * Request an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). */ - std::pair<bool, Node> entailmentCheck( - options::TheoryOfMode mode, - TNode lit, - const theory::EntailmentCheckParameters* params = NULL, - theory::EntailmentCheckSideEffects* out = NULL); + std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit); /** need check ? */ bool needCheck() const; |