diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/proof_checker.cpp | 20 |
2 files changed, 10 insertions, 18 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 75f93af47..5d05e5383 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -350,10 +350,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } Trace("builtin-pfcheck") << "Result is " << res << std::endl; Trace("builtin-pfcheck") << "Witness form is " - << SkolemManager::getWitnessForm(res) << std::endl; + << SkolemManager::getOriginalForm(res) << std::endl; // **** NOTE: can rewrite the witness form here. This enables certain lemmas // to be provable, e.g. (= k t) where k is a purification Skolem for t. - res = Rewriter::rewrite(SkolemManager::getWitnessForm(res)); + res = Rewriter::rewrite(SkolemManager::getOriginalForm(res)); if (!res.isConst() || !res.getConst<bool>()) { Trace("builtin-pfcheck") @@ -400,8 +400,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, if (res1 != res2) { // can rewrite the witness forms - res1 = Rewriter::rewrite(SkolemManager::getWitnessForm(res1)); - res2 = Rewriter::rewrite(SkolemManager::getWitnessForm(res2)); + res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1)); + res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2)); if (res1.isNull() || res1 != res2) { Trace("builtin-pfcheck") << "Failed to match results" << std::endl; diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 81273fdf9..afbc9efca 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -27,7 +27,7 @@ namespace quantifiers { void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc) { // add checkers - pc->registerChecker(PfRule::WITNESS_INTRO, this); + pc->registerChecker(PfRule::SKOLEM_INTRO, this); pc->registerChecker(PfRule::EXISTS_INTRO, this); pc->registerChecker(PfRule::SKOLEMIZE, this); pc->registerChecker(PfRule::INSTANTIATE, this); @@ -64,20 +64,12 @@ Node QuantifiersProofRuleChecker::checkInternal( } return exists; } - else if (id == PfRule::WITNESS_INTRO) + else if (id == PfRule::SKOLEM_INTRO) { - Assert(children.size() == 1); - Assert(args.empty()); - if (children[0].getKind() != EXISTS || children[0][0].getNumChildren() != 1) - { - return Node::null(); - } - std::vector<Node> skolems; - sm->mkSkolemize(children[0], skolems, "k"); - Assert(skolems.size() == 1); - Node witness = SkolemManager::getWitnessForm(skolems[0]); - Assert(witness.getKind() == WITNESS && witness[0] == children[0][0]); - return skolems[0].eqNode(witness); + Assert(children.empty()); + Assert(args.size() == 1); + Node t = SkolemManager::getOriginalForm(args[0]); + return args[0].eqNode(t); } else if (id == PfRule::SKOLEMIZE) { |