/*! \file proof_checker.cpp
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa
+ ** Haniel Barbosa, 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.
+ ** 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
**
**/
#include "theory/booleans/proof_checker.h"
+#include "expr/skolem_manager.h"
+#include "theory/rewriter.h"
namespace CVC4 {
namespace theory {
void BoolProofRuleChecker::registerTo(ProofChecker* pc)
{
pc->registerChecker(PfRule::SPLIT, this);
+ pc->registerChecker(PfRule::RESOLUTION, this);
+ pc->registerChecker(PfRule::CHAIN_RESOLUTION, this);
+ pc->registerChecker(PfRule::FACTORING, this);
+ pc->registerChecker(PfRule::REORDERING, this);
pc->registerChecker(PfRule::EQ_RESOLVE, this);
+ pc->registerChecker(PfRule::MODUS_PONENS, this);
+ pc->registerChecker(PfRule::NOT_NOT_ELIM, this);
+ pc->registerChecker(PfRule::CONTRA, this);
pc->registerChecker(PfRule::AND_ELIM, this);
pc->registerChecker(PfRule::AND_INTRO, this);
pc->registerChecker(PfRule::NOT_OR_ELIM, this);
const std::vector<Node>& children,
const std::vector<Node>& args)
{
+ if (id == PfRule::RESOLUTION)
+ {
+ Assert(children.size() == 2);
+ Assert(args.size() == 2);
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> disjuncts;
+ Node pivots[2];
+ if (args[0] == nm->mkConst(true))
+ {
+ pivots[0] = args[1];
+ pivots[1] = args[1].notNode();
+ }
+ else
+ {
+ Assert(args[0] == nm->mkConst(false));
+ pivots[0] = args[1].notNode();
+ pivots[1] = args[1];
+ }
+ for (unsigned i = 0; i < 2; ++i)
+ {
+ // determine whether the clause is unit for effects of resolution, which
+ // is the case if it's not an OR node or it is an OR node but it is equal
+ // to the pivot
+ std::vector<Node> lits;
+ if (children[i].getKind() == kind::OR && pivots[i] != children[i])
+ {
+ lits.insert(lits.end(), children[i].begin(), children[i].end());
+ }
+ else
+ {
+ lits.push_back(children[i]);
+ }
+ for (unsigned j = 0, size = lits.size(); j < size; ++j)
+ {
+ if (pivots[i] != lits[j])
+ {
+ disjuncts.push_back(lits[j]);
+ }
+ else
+ {
+ // just eliminate first occurrence
+ pivots[i] = Node::null();
+ }
+ }
+ }
+ return disjuncts.empty()
+ ? nm->mkConst(false)
+ : disjuncts.size() == 1 ? disjuncts[0]
+ : nm->mkNode(kind::OR, disjuncts);
+ }
+ if (id == PfRule::FACTORING)
+ {
+ Assert(children.size() == 1);
+ Assert(args.empty());
+ if (children[0].getKind() != kind::OR)
+ {
+ return Node::null();
+ }
+ // remove duplicates while keeping the order of children
+ std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+ std::vector<Node> disjuncts;
+ unsigned size = children[0].getNumChildren();
+ for (unsigned i = 0; i < size; ++i)
+ {
+ if (clauseSet.count(children[0][i]))
+ {
+ continue;
+ }
+ disjuncts.push_back(children[0][i]);
+ clauseSet.insert(children[0][i]);
+ }
+ if (disjuncts.size() == size)
+ {
+ return Node::null();
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ return disjuncts.empty()
+ ? nm->mkConst<bool>(false)
+ : disjuncts.size() == 1 ? disjuncts[0]
+ : nm->mkNode(kind::OR, disjuncts);
+ }
+ if (id == PfRule::REORDERING)
+ {
+ Assert(children.size() == 1);
+ Assert(args.size() == 1);
+ std::unordered_set<Node, NodeHashFunction> clauseSet1, clauseSet2;
+ if (children[0].getKind() == kind::OR)
+ {
+ clauseSet1.insert(children[0].begin(), children[0].end());
+ }
+ else
+ {
+ clauseSet1.insert(children[0]);
+ }
+ if (args[0].getKind() == kind::OR)
+ {
+ clauseSet2.insert(args[0].begin(), args[0].end());
+ }
+ else
+ {
+ clauseSet2.insert(args[0]);
+ }
+ if (clauseSet1 != clauseSet2)
+ {
+ Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n"
+ << id << ": clause set2: " << clauseSet2 << "\n";
+ return Node::null();
+ }
+ return args[0];
+ }
+ if (id == PfRule::CHAIN_RESOLUTION)
+ {
+ Assert(children.size() > 1);
+ Assert(args.size() == children.size() - 1);
+ Trace("bool-pfcheck") << "chain_res:\n" << push;
+ std::vector<Node> clauseNodes;
+ for (unsigned i = 0, childrenSize = children.size(); i < childrenSize; ++i)
+ {
+ std::unordered_set<Node, NodeHashFunction> elim;
+ // literals to be removed from "first" clause
+ if (i < childrenSize - 1)
+ {
+ elim.insert(args.begin() + i, args.end());
+ }
+ // literal to be removed from "second" clause. They will be negated
+ if (i > 0)
+ {
+ elim.insert(args[i - 1].negate());
+ }
+ Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n";
+ // only add to conclusion nodes that are not in elimination set. First get
+ // the nodes.
+ //
+ // Since unit clauses can also be OR nodes, we rely on the invariant that
+ // non-unit clauses will not occur themselves in their elimination sets.
+ // If they do then they must be unit.
+ std::vector<Node> lits;
+ if (children[i].getKind() == kind::OR && elim.count(children[i]) == 0)
+ {
+ lits.insert(lits.end(), children[i].begin(), children[i].end());
+ }
+ else
+ {
+ lits.push_back(children[i]);
+ }
+ Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n";
+ std::vector<Node> added;
+ for (unsigned j = 0, size = lits.size(); j < size; ++j)
+ {
+ if (elim.count(lits[j]) == 0)
+ {
+ clauseNodes.push_back(lits[j]);
+ added.push_back(lits[j]);
+ }
+ }
+ Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n";
+ }
+ Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop;
+ NodeManager* nm = NodeManager::currentNM();
+ return clauseNodes.empty()
+ ? nm->mkConst<bool>(false)
+ : clauseNodes.size() == 1 ? clauseNodes[0]
+ : nm->mkNode(kind::OR, clauseNodes);
+ }
if (id == PfRule::SPLIT)
{
Assert(children.empty());
return NodeManager::currentNM()->mkNode(
kind::OR, args[0], args[0].notNode());
}
+ if (id == PfRule::CONTRA)
+ {
+ Assert(children.size() == 2);
+ if (children[1].getKind() == Kind::NOT && children[0] == children[1][0])
+ {
+ return NodeManager::currentNM()->mkConst(false);
+ }
+ return Node::null();
+ }
if (id == PfRule::EQ_RESOLVE)
{
Assert(children.size() == 2);
}
return children[1][1];
}
+ if (id == PfRule::MODUS_PONENS)
+ {
+ Assert(children.size() == 2);
+ Assert(args.empty());
+ if (children[1].getKind() != kind::IMPLIES || children[0] != children[1][0])
+ {
+ return Node::null();
+ }
+ return children[1][1];
+ }
+ if (id == PfRule::NOT_NOT_ELIM)
+ {
+ Assert(children.size() == 1);
+ Assert(args.empty());
+ if (children[0].getKind() != kind::NOT || children[0][0].getKind() != kind::NOT)
+ {
+ return Node::null();
+ }
+ return children[0][0][0];
+ }
// natural deduction rules
if (id == PfRule::AND_ELIM)
{
projects / cvc5.git / blobdiff