diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-26 20:24:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-26 20:24:28 -0500 |
commit | 00c9ae6e2796c45d821ea9dd45ff7c33a5770922 (patch) | |
tree | 814c741134a68a23679adc23a9597bde5d12ec6f /src/theory/theory.h | |
parent | a407bd70c09724dc20af3241775abedd3a73ec67 (diff) |
(new theory) Update TheoryUF to new interface (#4944)
This updates TheoryUF to use the 4 check callbacks instead of implementing check, and uses the official TheoryState object instead of its context::CDO<bool> d_conflict field.
It also makes a minor change to collectModelValues for const and to preNotifyFact to include an isInternal flag.
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 8ea64e724..1fdf96331 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -644,18 +644,22 @@ class Theory { * @param polarity Its polarity * @param fact The original literal that was asserted * @param isPrereg Whether the assertion is preregistered + * @param isInternal Whether the origin of the fact was internal. If this + * is false, the fact was asserted via the fact queue of the theory. * @return true if the theory completely processed this fact, i.e. it does * not need to assert the fact to its equality engine. */ - virtual bool preNotifyFact(TNode atom, bool pol, TNode fact, bool isPrereg); + virtual bool preNotifyFact( + TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal); /** * Notify fact, called immediately after the fact was pushed into the * equality engine. * * @param atom The atom * @param polarity Its polarity - * @param fact The original literal that was asserted - * @param isInternal Whether the origin of the fact was internal + * @param fact The original literal that was asserted. + * @param isInternal Whether the origin of the fact was internal. If this + * is false, the fact was asserted via the fact queue of the theory. */ virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal); //--------------------------------- end check @@ -690,7 +694,8 @@ class Theory { * The argument termSet is the set of relevant terms returned by * computeRelevantTerms. */ - virtual bool collectModelValues(TheoryModel* m, std::set<Node>& termSet); + virtual bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet); /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } //--------------------------------- end collect model info |