diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-28 14:49:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-28 14:49:26 -0500 |
commit | c137366e668aff70b1739a1f2c5cf8e6e2e28a72 (patch) | |
tree | b40055e588894833ac4d0e4f813994766a6744b6 /src/theory/quantifiers/theory_quantifiers.h | |
parent | d1bb100d75aca76fdeb7a18b6c044035029ffe17 (diff) |
(new theory) Update TheoryQuantifiers to the new interface (#4950)
TheoryQuantifiers is a theory that passes quantified formulas to QuantifiersEngine. This updates it to the new check template (see #4929).
Also does some minor cleanup in the cpp file.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.h')
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 6f8256c21..509b0e0ea 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -19,9 +19,7 @@ #ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#include "context/context.h" #include "expr/node.h" -#include "theory/output_channel.h" #include "theory/quantifiers/proof_checker.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/quantifiers_state.h" @@ -52,8 +50,19 @@ class TheoryQuantifiers : public Theory { void preRegisterTerm(TNode n) override; void presolve() override; void ppNotifyAssertions(const std::vector<Node>& assertions) override; - void check(Effort e) override; - bool collectModelInfo(TheoryModel* m) override; + //--------------------------------- standard check + /** Post-check, called after the fact queue of the theory is processed. */ + void postCheck(Effort level) override; + /** Pre-notify fact, return true if processed. */ + bool preNotifyFact(TNode atom, + bool pol, + TNode fact, + bool isPrereg, + bool isInternal) override; + //--------------------------------- end standard check + /** Collect model values in m based on the relevant terms given by termSet */ + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; void shutdown() override {} std::string identify() const override { |