diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-31 06:46:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-31 06:46:42 -0500 |
| commit | fc784f0273099b84581862b8587940c6db3459ed (patch) | |
| tree | f8eb682b426b14f01d349983d0e40f2bcbfcb8b1 /src/expr | |
| parent | 0675545dde7ed679b7045a37470148c7e1bdfd25 (diff) | |
Basic proof support in inference manager (#4975)
This adds basic support for asserting internal facts with proofs in the inference manager class.
The purpose of this PR is twofold:
(1) From the point of view of proofs, this PR standardizes the management of proof equality engine within inference manager. Theories no longer have to manually construct proof equality engines, and instead are recommended to create inference managers.
(2) From the point of view of the new approach to theory combination, this PR ensures standard theory callbacks (preNotifyFact / notifyFact) are used for internal facts, regardless of whether proofs are enabled.
This will simplify several of the current (unmerged) changes for proof production in theory solvers on proof-new.
Notice this PR adds the utility method NodeManager::mkAnd, which is arguably long overdue.
Also notice this code is not yet active, but will be used on proof-new after this PR is merged.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/node_manager.h | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 592b5e7e9..abbe998b5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -473,6 +473,17 @@ class NodeManager { template <bool ref_count> Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children); + /** + * Create an AND node with arbitrary number of children. This returns the + * true node if children is empty, or the single node in children if + * it contains only one node. + * + * We define construction of AND as a special case here since it is widely + * used for e.g. constructing explanations. + */ + template <bool ref_count> + Node mkAnd(const std::vector<NodeTemplate<ref_count> >& children); + /** Create a node (with no children) by operator. */ Node mkNode(TNode opNode); Node* mkNodePtr(TNode opNode); @@ -1360,6 +1371,20 @@ inline Node NodeManager::mkNode(Kind kind, } template <bool ref_count> +Node NodeManager::mkAnd(const std::vector<NodeTemplate<ref_count> >& children) +{ + if (children.empty()) + { + return mkConst(true); + } + else if (children.size() == 1) + { + return children[0]; + } + return mkNode(kind::AND, children); +} + +template <bool ref_count> inline Node* NodeManager::mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children) { |