Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/proof_checker.cpp	Lines:	45	65	69.2 %
Date:	2021-08-14	Branches:	108	460	23.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * 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.
 * ****************************************************************************
 *
 * Implementation of arrays proof checker.
 */

#include "theory/arrays/proof_checker.h"

#include "expr/skolem_manager.h"
#include "theory/arrays/skolem_cache.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace theory {
namespace arrays {

void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
{
  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE, this);
  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this);
  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this);
  pc->registerChecker(PfRule::ARRAYS_EXT, this);
  pc->registerChecker(PfRule::ARRAYS_EQ_RANGE_EXPAND, this);
  // trusted rules
  pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2);
}

Node ArraysProofRuleChecker::checkInternal(PfRule id,
                                           const std::vector<Node>& children,
                                           const std::vector<Node>& args)
{
  NodeManager* nm = NodeManager::currentNM();
  if (id == PfRule::ARRAYS_READ_OVER_WRITE)
  {
    Assert(children.size() == 1);
    Assert(args.size() == 1);
    Node ideq = children[0];
    if (ideq.getKind() != kind::NOT || ideq[0].getKind() != kind::EQUAL)
    {
      return Node::null();
    }
    Node lhs = args[0];
    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
        || lhs[0][1] != ideq[0][0])
    {
      return Node::null();
    }
    Node rhs = nm->mkNode(kind::SELECT, lhs[0][0], ideq[0][1]);
    return lhs.eqNode(rhs);
  }
  else if (id == PfRule::ARRAYS_READ_OVER_WRITE_CONTRA)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    Node adeq = children[0];
    if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL)
    {
      return Node::null();
    }
    Node lhs = adeq[0][0];
    Node rhs = adeq[0][1];
    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
        || rhs.getKind() != kind::SELECT || lhs[1] != rhs[1])
    {
      return Node::null();
    }
    return lhs[1].eqNode(lhs[0][1]);
  }
  if (id == PfRule::ARRAYS_READ_OVER_WRITE_1)
  {
    Assert(children.empty());
    Assert(args.size() == 1);
    Node lhs = args[0];
    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
        || lhs[0][1] != lhs[1])
    {
      return Node::null();
    }
    Node rhs = lhs[0][2];
    return lhs.eqNode(rhs);
  }
  if (id == PfRule::ARRAYS_EXT)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    Node adeq = children[0];
    if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL
        || !adeq[0][0].getType().isArray())
    {
      return Node::null();
    }
    Node k = SkolemCache::getExtIndexSkolem(adeq);
    Node a = adeq[0][0];
    Node b = adeq[0][1];
    Node as = nm->mkNode(kind::SELECT, a, k);
    Node bs = nm->mkNode(kind::SELECT, b, k);
    return as.eqNode(bs).notNode();
  }
  if (id == PfRule::ARRAYS_EQ_RANGE_EXPAND)
  {
    Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]);
    return args[0].eqNode(expandedEqRange);
  }
  if (id == PfRule::ARRAYS_TRUST)
  {
    // "trusted" rules
    Assert(!args.empty());
    Assert(args[0].getType().isBoolean());
    return args[0];
  }
  // no rule
  return Node::null();
}

}  // namespace arrays
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of arrays proof checker.
14		*/
15
16		#include "theory/arrays/proof_checker.h"
17
18		#include "expr/skolem_manager.h"
19		#include "theory/arrays/skolem_cache.h"
20		#include "theory/arrays/theory_arrays_rewriter.h"
21		#include "theory/rewriter.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace arrays {
26
27	3768	void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
28		{
29	3768	pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE, this);
30	3768	pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this);
31	3768	pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this);
32	3768	pc->registerChecker(PfRule::ARRAYS_EXT, this);
33	3768	pc->registerChecker(PfRule::ARRAYS_EQ_RANGE_EXPAND, this);
34		// trusted rules
35	3768	pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2);
36	3768	}
37
38	1975	Node ArraysProofRuleChecker::checkInternal(PfRule id,
39		const std::vector<Node>& children,
40		const std::vector<Node>& args)
41		{
42	1975	NodeManager* nm = NodeManager::currentNM();
43	1975	if (id == PfRule::ARRAYS_READ_OVER_WRITE)
44		{
45	443	Assert(children.size() == 1);
46	443	Assert(args.size() == 1);
47	886	Node ideq = children[0];
48	443	if (ideq.getKind() != kind::NOT \|\| ideq[0].getKind() != kind::EQUAL)
49		{
50		return Node::null();
51		}
52	886	Node lhs = args[0];
53	1329	if (lhs.getKind() != kind::SELECT \|\| lhs[0].getKind() != kind::STORE
54	1329	\|\| lhs[0][1] != ideq[0][0])
55		{
56		return Node::null();
57		}
58	886	Node rhs = nm->mkNode(kind::SELECT, lhs[0][0], ideq[0][1]);
59	443	return lhs.eqNode(rhs);
60		}
61	1532	else if (id == PfRule::ARRAYS_READ_OVER_WRITE_CONTRA)
62		{
63		Assert(children.size() == 1);
64		Assert(args.empty());
65		Node adeq = children[0];
66		if (adeq.getKind() != kind::NOT \|\| adeq[0].getKind() != kind::EQUAL)
67		{
68		return Node::null();
69		}
70		Node lhs = adeq[0][0];
71		Node rhs = adeq[0][1];
72		if (lhs.getKind() != kind::SELECT \|\| lhs[0].getKind() != kind::STORE
73		\|\| rhs.getKind() != kind::SELECT \|\| lhs[1] != rhs[1])
74		{
75		return Node::null();
76		}
77		return lhs[1].eqNode(lhs[0][1]);
78		}
79	1532	if (id == PfRule::ARRAYS_READ_OVER_WRITE_1)
80		{
81	1400	Assert(children.empty());
82	1400	Assert(args.size() == 1);
83	2800	Node lhs = args[0];
84	4200	if (lhs.getKind() != kind::SELECT \|\| lhs[0].getKind() != kind::STORE
85	4200	\|\| lhs[0][1] != lhs[1])
86		{
87		return Node::null();
88		}
89	2800	Node rhs = lhs[0][2];
90	1400	return lhs.eqNode(rhs);
91		}
92	132	if (id == PfRule::ARRAYS_EXT)
93		{
94	129	Assert(children.size() == 1);
95	129	Assert(args.empty());
96	258	Node adeq = children[0];
97	387	if (adeq.getKind() != kind::NOT \|\| adeq[0].getKind() != kind::EQUAL
98	387	\|\| !adeq[0][0].getType().isArray())
99		{
100		return Node::null();
101		}
102	258	Node k = SkolemCache::getExtIndexSkolem(adeq);
103	258	Node a = adeq[0][0];
104	258	Node b = adeq[0][1];
105	258	Node as = nm->mkNode(kind::SELECT, a, k);
106	258	Node bs = nm->mkNode(kind::SELECT, b, k);
107	129	return as.eqNode(bs).notNode();
108		}
109	3	if (id == PfRule::ARRAYS_EQ_RANGE_EXPAND)
110		{
111	6	Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]);
112	3	return args[0].eqNode(expandedEqRange);
113		}
114		if (id == PfRule::ARRAYS_TRUST)
115		{
116		// "trusted" rules
117		Assert(!args.empty());
118		Assert(args[0].getType().isBoolean());
119		return args[0];
120		}
121		// no rule
122		return Node::null();
123		}
124
125		} // namespace arrays
126		} // namespace theory
127	29340	} // namespace cvc5