Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/cad/proof_generator.cpp	Lines:	78	85	91.8 %
Date:	2021-11-05	Branches:	124	276	44.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer
 *
 * 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 CAD proof generator.
 */

#include "theory/arith/nl/cad/proof_generator.h"

#ifdef CVC5_POLY_IMP

#include "proof/lazy_tree_proof_generator.h"
#include "theory/arith/nl/poly_conversion.h"
#include "util/indexed_root_predicate.h"

namespace cvc5 {
namespace theory {
namespace arith {
namespace nl {
namespace cad {

namespace {
/**
 * Retrieves the root indices of the sign-invariant region of v.
 *
 * We assume that roots holds a sorted list of roots from one polynomial.
 * If v is equal to one of these roots, we return (id,id) where id is the index
 * of this root within roots. Otherwise, we return the id of the largest root
 * below v and the id of the smallest root above v. To make sure a smaller root
 * and a larger root always exist, we implicitly extend the roots by -infty and
 * infty.
 *
 * ATTENTION: if we return id, the corresponding root is:
 *   - id = 0: -infty
 *   - 0 < id <= roots.size(): roots[id-1]
 *   - id = roots.size() + 1: infty
 */
std::pair<std::size_t, std::size_t> getRootIDs(
    const std::vector<poly::Value>& roots, const poly::Value& v)
{
  for (std::size_t i = 0; i < roots.size(); ++i)
  {
    if (roots[i] == v)
    {
      return {i + 1, i + 1};
    }
    if (roots[i] > v)
    {
      return {i, i + 1};
    }
  }
  return {roots.size(), roots.size() + 1};
}

/**
 * Constructs an IndexedRootExpression:
 *   var ~rel~ root_k(poly)
 * where root_k(poly) is "the k'th root of the polynomial".
 *
 * @param var The variable that is bounded
 * @param rel The relation for this constraint
 * @param zero A node representing Rational(0)
 * @param k The index of the root (starting with 1)
 * @param poly The polynomial whose root shall be considered
 * @param vm A variable mapper from cvc5 to libpoly variables
 */
Node mkIRP(const Node& var,
           Kind rel,
           const Node& zero,
           std::size_t k,
           const poly::Polynomial& poly,
           VariableMapper& vm)
{
  auto* nm = NodeManager::currentNM();
  auto op = nm->mkConst<IndexedRootPredicate>(IndexedRootPredicate(k));
  return nm->mkNode(Kind::INDEXED_ROOT_PREDICATE,
                    op,
                    nm->mkNode(rel, var, zero),
                    as_cvc_polynomial(poly, vm));
}

}  // namespace

CADProofGenerator::CADProofGenerator(context::Context* ctx,
                                     ProofNodeManager* pnm)
    : d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr)
{
  d_false = NodeManager::currentNM()->mkConst<bool>(false);
  d_zero = NodeManager::currentNM()->mkConst<Rational>(0);
}

void CADProofGenerator::startNewProof()
{
  d_current = d_proofs.allocateProof();
}
void CADProofGenerator::startRecursive() { d_current->openChild(); }
void CADProofGenerator::endRecursive(size_t intervalId)
{
  d_current->setCurrent(
      intervalId, PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false);
  d_current->closeChild();
}
void CADProofGenerator::startScope()
{
  d_current->openChild();
  d_current->getCurrent().d_rule = PfRule::SCOPE;
}
void CADProofGenerator::endScope(const std::vector<Node>& args)
{
  d_current->setCurrent(0, PfRule::SCOPE, {}, args, d_false);
  d_current->closeChild();
}

ProofGenerator* CADProofGenerator::getProofGenerator() const
{
  return d_current;
}

void CADProofGenerator::addDirect(Node var,
                                  VariableMapper& vm,
                                  const poly::Polynomial& poly,
                                  const poly::Assignment& a,
                                  poly::SignCondition& sc,
                                  const poly::Interval& interval,
                                  Node constraint,
                                  size_t intervalId)
{
  if (is_minus_infinity(get_lower(interval))
      && is_plus_infinity(get_upper(interval)))
  {
    // "Full conflict", constraint excludes (-inf,inf)
    d_current->openChild();
    d_current->setCurrent(intervalId,
                          PfRule::ARITH_NL_CAD_DIRECT,
                          {constraint},
                          {d_false},
                          d_false);
    d_current->closeChild();
    return;
  }
  std::vector<Node> res;
  auto roots = poly::isolate_real_roots(poly, a);
  if (get_lower(interval) == get_upper(interval))
  {
    // Excludes a single point only
    auto ids = getRootIDs(roots, get_lower(interval));
    Assert(ids.first == ids.second);
    res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
  }
  else
  {
    // Excludes an open interval
    if (!is_minus_infinity(get_lower(interval)))
    {
      // Interval has lower bound that is not -inf
      auto ids = getRootIDs(roots, get_lower(interval));
      Assert(ids.first == ids.second);
      Kind rel = poly::get_lower_open(interval) ? Kind::GT : Kind::GEQ;
      res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm));
    }
    if (!is_plus_infinity(get_upper(interval)))
    {
      // Interval has upper bound that is not inf
      auto ids = getRootIDs(roots, get_upper(interval));
      Assert(ids.first == ids.second);
      Kind rel = poly::get_upper_open(interval) ? Kind::LT : Kind::LEQ;
      res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm));
    }
  }
  // Add to proof manager
  startScope();
  d_current->openChild();
  d_current->setCurrent(intervalId,
                        PfRule::ARITH_NL_CAD_DIRECT,
                        {constraint},
                        {d_false},
                        d_false);
  d_current->closeChild();
  endScope(res);
}

std::vector<Node> CADProofGenerator::constructCell(Node var,
                                                   const CACInterval& i,
                                                   const poly::Assignment& a,
                                                   const poly::Value& s,
                                                   VariableMapper& vm)
{
  if (is_minus_infinity(get_lower(i.d_interval))
      && is_plus_infinity(get_upper(i.d_interval)))
  {
    // "Full conflict", constraint excludes (-inf,inf)
    return {};
  }

  std::vector<Node> res;

  // Just use bounds for all polynomials
  for (const auto& poly : i.d_mainPolys)
  {
    auto roots = poly::isolate_real_roots(poly, a);
    auto ids = getRootIDs(roots, s);
    if (ids.first == ids.second)
    {
      // Excludes a single point only
      res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
    }
    else
    {
      // Excludes an open interval
      if (ids.first > 0)
      {
        // Interval has lower bound that is not -inf
        res.emplace_back(mkIRP(var, Kind::GT, d_zero, ids.first, poly, vm));
      }
      if (ids.second <= roots.size())
      {
        // Interval has upper bound that is not inf
        res.emplace_back(mkIRP(var, Kind::LT, d_zero, ids.first, poly, vm));
      }
    }
  }

  return res;
}

std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof)
{
  return os << *proof.d_current;
}

}  // namespace cad
}  // namespace nl
}  // namespace arith
}  // namespace theory
}  // namespace cvc5

#endif


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer
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 CAD proof generator.
14		*/
15
16		#include "theory/arith/nl/cad/proof_generator.h"
17
18		#ifdef CVC5_POLY_IMP
19
20		#include "proof/lazy_tree_proof_generator.h"
21		#include "theory/arith/nl/poly_conversion.h"
22		#include "util/indexed_root_predicate.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace arith {
27		namespace nl {
28		namespace cad {
29
30		namespace {
31		/**
32		* Retrieves the root indices of the sign-invariant region of v.
33		*
34		* We assume that roots holds a sorted list of roots from one polynomial.
35		* If v is equal to one of these roots, we return (id,id) where id is the index
36		* of this root within roots. Otherwise, we return the id of the largest root
37		* below v and the id of the smallest root above v. To make sure a smaller root
38		* and a larger root always exist, we implicitly extend the roots by -infty and
39		* infty.
40		*
41		* ATTENTION: if we return id, the corresponding root is:
42		* - id = 0: -infty
43		* - 0 < id <= roots.size(): roots[id-1]
44		* - id = roots.size() + 1: infty
45		*/
46	1255	std::pair<std::size_t, std::size_t> getRootIDs(
47		const std::vector<poly::Value>& roots, const poly::Value& v)
48		{
49	1517	for (std::size_t i = 0; i < roots.size(); ++i)
50		{
51	1499	if (roots[i] == v)
52		{
53	1223	return {i + 1, i + 1};
54		}
55	276	if (roots[i] > v)
56		{
57	14	return {i, i + 1};
58		}
59		}
60	18	return {roots.size(), roots.size() + 1};
61		}
62
63		/**
64		* Constructs an IndexedRootExpression:
65		* var ~rel~ root_k(poly)
66		* where root_k(poly) is "the k'th root of the polynomial".
67		*
68		* @param var The variable that is bounded
69		* @param rel The relation for this constraint
70		* @param zero A node representing Rational(0)
71		* @param k The index of the root (starting with 1)
72		* @param poly The polynomial whose root shall be considered
73		* @param vm A variable mapper from cvc5 to libpoly variables
74		*/
75	1257	Node mkIRP(const Node& var,
76		Kind rel,
77		const Node& zero,
78		std::size_t k,
79		const poly::Polynomial& poly,
80		VariableMapper& vm)
81		{
82	1257	auto* nm = NodeManager::currentNM();
83	2514	auto op = nm->mkConst<IndexedRootPredicate>(IndexedRootPredicate(k));
84		return nm->mkNode(Kind::INDEXED_ROOT_PREDICATE,
85		op,
86	2514	nm->mkNode(rel, var, zero),
87	5028	as_cvc_polynomial(poly, vm));
88		}
89
90		} // namespace
91
92	4682	CADProofGenerator::CADProofGenerator(context::Context* ctx,
93	4682	ProofNodeManager* pnm)
94	4682	: d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr)
95		{
96	4682	d_false = NodeManager::currentNM()->mkConst<bool>(false);
97	4682	d_zero = NodeManager::currentNM()->mkConst<Rational>(0);
98	4682	}
99
100	43	void CADProofGenerator::startNewProof()
101		{
102	43	d_current = d_proofs.allocateProof();
103	43	}
104	101	void CADProofGenerator::startRecursive() { d_current->openChild(); }
105	81	void CADProofGenerator::endRecursive(size_t intervalId)
106		{
107	162	d_current->setCurrent(
108	81	intervalId, PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false);
109	81	d_current->closeChild();
110	81	}
111	1244	void CADProofGenerator::startScope()
112		{
113	1244	d_current->openChild();
114	1244	d_current->getCurrent().d_rule = PfRule::SCOPE;
115	1244	}
116	1249	void CADProofGenerator::endScope(const std::vector<Node>& args)
117		{
118	1249	d_current->setCurrent(0, PfRule::SCOPE, {}, args, d_false);
119	1249	d_current->closeChild();
120	1249	}
121
122	25	ProofGenerator* CADProofGenerator::getProofGenerator() const
123		{
124	25	return d_current;
125		}
126
127	1186	void CADProofGenerator::addDirect(Node var,
128		VariableMapper& vm,
129		const poly::Polynomial& poly,
130		const poly::Assignment& a,
131		poly::SignCondition& sc,
132		const poly::Interval& interval,
133		Node constraint,
134		size_t intervalId)
135		{
136	2372	if (is_minus_infinity(get_lower(interval))
137	1186	&& is_plus_infinity(get_upper(interval)))
138		{
139		// "Full conflict", constraint excludes (-inf,inf)
140		d_current->openChild();
141		d_current->setCurrent(intervalId,
142		PfRule::ARITH_NL_CAD_DIRECT,
143		{constraint},
144		{d_false},
145		d_false);
146		d_current->closeChild();
147		return;
148		}
149	2372	std::vector<Node> res;
150	2372	auto roots = poly::isolate_real_roots(poly, a);
151	1186	if (get_lower(interval) == get_upper(interval))
152		{
153		// Excludes a single point only
154	749	auto ids = getRootIDs(roots, get_lower(interval));
155	749	Assert(ids.first == ids.second);
156	749	res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
157		}
158		else
159		{
160		// Excludes an open interval
161	437	if (!is_minus_infinity(get_lower(interval)))
162		{
163		// Interval has lower bound that is not -inf
164	190	auto ids = getRootIDs(roots, get_lower(interval));
165	190	Assert(ids.first == ids.second);
166	190	Kind rel = poly::get_lower_open(interval) ? Kind::GT : Kind::GEQ;
167	190	res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm));
168		}
169	437	if (!is_plus_infinity(get_upper(interval)))
170		{
171		// Interval has upper bound that is not inf
172	278	auto ids = getRootIDs(roots, get_upper(interval));
173	278	Assert(ids.first == ids.second);
174	278	Kind rel = poly::get_upper_open(interval) ? Kind::LT : Kind::LEQ;
175	278	res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm));
176		}
177		}
178		// Add to proof manager
179	1186	startScope();
180	1186	d_current->openChild();
181	3558	d_current->setCurrent(intervalId,
182		PfRule::ARITH_NL_CAD_DIRECT,
183		{constraint},
184		{d_false},
185	2372	d_false);
186	1186	d_current->closeChild();
187	1186	endScope(res);
188		}
189
190	38	std::vector<Node> CADProofGenerator::constructCell(Node var,
191		const CACInterval& i,
192		const poly::Assignment& a,
193		const poly::Value& s,
194		VariableMapper& vm)
195		{
196	76	if (is_minus_infinity(get_lower(i.d_interval))
197	38	&& is_plus_infinity(get_upper(i.d_interval)))
198		{
199		// "Full conflict", constraint excludes (-inf,inf)
200	8	return {};
201		}
202
203	60	std::vector<Node> res;
204
205		// Just use bounds for all polynomials
206	68	for (const auto& poly : i.d_mainPolys)
207		{
208	76	auto roots = poly::isolate_real_roots(poly, a);
209	38	auto ids = getRootIDs(roots, s);
210	38	if (ids.first == ids.second)
211		{
212		// Excludes a single point only
213	6	res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
214		}
215		else
216		{
217		// Excludes an open interval
218	32	if (ids.first > 0)
219		{
220		// Interval has lower bound that is not -inf
221	20	res.emplace_back(mkIRP(var, Kind::GT, d_zero, ids.first, poly, vm));
222		}
223	32	if (ids.second <= roots.size())
224		{
225		// Interval has upper bound that is not inf
226	14	res.emplace_back(mkIRP(var, Kind::LT, d_zero, ids.first, poly, vm));
227		}
228		}
229		}
230
231	30	return res;
232		}
233
234		std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof)
235		{
236		return os << *proof.d_current;
237		}
238
239		} // namespace cad
240		} // namespace nl
241		} // namespace arith
242		} // namespace theory
243	31125	} // namespace cvc5
244
245		#endif