diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 09:03:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-27 09:03:07 -0500 |
commit | 03cc40cc070df0bc11c1556cef3016f784a95d23 (patch) | |
tree | 6360b66292cfd6a1f46a4970c8f8e3cfc9e2e853 /src/smt/term_formula_removal.cpp | |
parent | 425bfb52e2a6aca7a968ccf3785356ac469ec046 (diff) |
Implement Hilbert choice operator (#1291)
* Initial support for Hilbert choice operator.
* Clang format.
* Fix
* Minor
Diffstat (limited to 'src/smt/term_formula_removal.cpp')
-rw-r--r-- | src/smt/term_formula_removal.cpp | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 0cd166c87..01cf59c15 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -116,7 +116,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, } //if a lambda, do lambda-lifting if( node.getKind() == kind::LAMBDA && !inQuant ){ - // Make the skolem to represent the ITE + // Make the skolem to represent the lambda skolem = nodeManager->mkSkolem("lambdaF", nodeType, "a function introduced due to term-level lambda removal"); // The new assertion @@ -134,6 +134,25 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, // axiom defining skolem newAssertion = nodeManager->mkNode( kind::FORALL, children ); } + + // If a Hilbert choice function, witness the choice. + // For details on this operator, see + // http://planetmath.org/hilbertsvarepsilonoperator. + if (node.getKind() == kind::CHOICE && !inQuant) + { + // Make the skolem to witness the choice + skolem = nodeManager->mkSkolem( + "choiceK", + nodeType, + "a skolem introduced due to term-level Hilbert choice removal"); + + Assert(node[0].getNumChildren() == 1); + + // The new assertion is the assumption that the body + // of the choice operator holds for the Skolem + newAssertion = node[1].substitute(node[0], skolem); + } + //if a non-variable Boolean term, replace it if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ |