diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-24 13:16:04 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-24 13:16:04 -0500 |
commit | 6d53928cd9f16385d81124916311c372ec20b5ed (patch) | |
tree | 613e51c10005b401fd8b181bb94426c7d3834ab9 /src/theory/model_manager_distributed.h | |
parent | 983f41ea94f68e90d24e353ae3fd1aca04ac56ff (diff) |
Add the distributed model manager (#4934)
This class is responsible for model building when using a distributed approach for equality engines.
This PR defines the class but does not yet activate it in TheoryEngine.
This includes some model-specific things from TheoryEngine which will be migrated to this class on the next PR.
Diffstat (limited to 'src/theory/model_manager_distributed.h')
-rw-r--r-- | src/theory/model_manager_distributed.h | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h new file mode 100644 index 000000000..2f86c0b00 --- /dev/null +++ b/src/theory/model_manager_distributed.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \file model_manager_distributed.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Management of a distributed approach for model generation. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H +#define CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H + +#include <memory> + +#include "theory/ee_manager_distributed.h" +#include "theory/model_manager.h" + +namespace CVC4 { + +class TheoryEngine; + +namespace theory { + +/** + * Manager for building models in a distributed architecture. Its prepare + * model method uses collectModelInfo to assert all equalities from the equality + * engine of each theory into the equality engine of the model. It additionally + * uses the model equality engine context to clear the information from + * the model's equality engine, as maintained by the distributed equality + * engine manager. + */ +class ModelManagerDistributed : public ModelManager +{ + public: + ModelManagerDistributed(TheoryEngine& te, EqEngineManagerDistributed& eem); + ~ModelManagerDistributed(); + + /** Prepare the model, as described above. */ + bool prepareModel() override; + /** + * Assign values to all equivalence classes in the equality engine of the + * model, return true if successful. + */ + bool finishBuildModel() const override; + + protected: + /** + * Distributed equality engine manager, which maintains the context of the + * model's equality engine. + */ + EqEngineManagerDistributed& d_eem; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H */ |