diff options
author | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
commit | aa9aa46b77f048f2865c29e40ed946371fd115ef (patch) | |
tree | 254f392449a03901f7acb7a65e9499193d07ac9a /src/proof/skolemization_manager.h | |
parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) |
squash-merge from proof branch
Diffstat (limited to 'src/proof/skolemization_manager.h')
-rw-r--r-- | src/proof/skolemization_manager.h | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h new file mode 100644 index 000000000..649f0bf40 --- /dev/null +++ b/src/proof/skolemization_manager.h @@ -0,0 +1,42 @@ +/********************* */ +/*! \file skolemization_manager.h + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SKOLEMIZATION_MANAGER_H +#define __CVC4__SKOLEMIZATION_MANAGER_H + +#include <iostream> +#include <map> +#include "proof/proof.h" +#include "util/proof.h" +#include "expr/node.h" +#include "theory/logic_info.h" +#include "theory/substitutions.h" + +namespace CVC4 { + +class SkolemizationManager { +public: + void registerSkolem(Node disequality, Node skolem); + bool hasSkolem(Node disequality); + Node getSkolem(Node disequality); + Node getDisequality(Node skolem); + bool isSkolem(Node skolem); + + void clear(); + + std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin(); + std::hash_map<Node, Node, NodeHashFunction>::const_iterator end(); + +private: + std::hash_map<Node, Node, NodeHashFunction> d_disequalityToSkolem; + std::hash_map<Node, Node, NodeHashFunction> d_skolemToDisequality; +}; + +}/* CVC4 namespace */ + + + +#endif /* __CVC4__SKOLEMIZATION_MANAGER_H */ |