Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/infer_bounds.cpp	Lines:	33	137	24.1 %
Date:	2021-05-22	Branches:	7	217	3.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "theory/arith/infer_bounds.h"
#include "theory/rewriter.h"

namespace cvc5 {
namespace theory {
namespace arith {

using namespace inferbounds;

InferBoundAlgorithm::InferBoundAlgorithm()
  : d_alg(None)
{}

InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
  : d_alg(a)
{
  Assert(a != Simplex);
}

InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds)
  : d_alg(Simplex)
{}

Algorithms InferBoundAlgorithm::getAlgorithm() const{
  return d_alg;
}

const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{
  Assert(getAlgorithm() == Simplex);
  return d_simplexRounds;
}


InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
  return InferBoundAlgorithm(Lookup);
}

InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
  return InferBoundAlgorithm(RowSum);
}

InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
  return InferBoundAlgorithm(rounds);
}

ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
    : d_algorithms()
{}

ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
{}


void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){
  addAlgorithm(InferBoundAlgorithm::mkLookup());
  addAlgorithm(InferBoundAlgorithm::mkRowSum());
}

void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){
  d_algorithms.push_back(alg);
}

ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{
  return d_algorithms.begin();
}

ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{
  return d_algorithms.end();
}

InferBoundsResult::InferBoundsResult()
  : d_foundBound(false)
  , d_budgetExhausted(false)
  , d_boundIsProvenOpt(false)
  , d_inconsistentState(false)
  , d_reachedThreshold(false)
  , d_value(false)
  , d_term(Node::null())
  , d_upperBound(true)
  , d_explanation(Node::null())
{}

InferBoundsResult::InferBoundsResult(Node term, bool ub)
  : d_foundBound(false)
  , d_budgetExhausted(false)
  , d_boundIsProvenOpt(false)
  , d_inconsistentState(false)
  , d_reachedThreshold(false)
  , d_value(false)
  , d_term(term)
  , d_upperBound(ub)
  , d_explanation(Node::null())
{}

bool InferBoundsResult::foundBound() const {
  return d_foundBound;
}
bool InferBoundsResult::boundIsOptimal() const {
  return d_boundIsProvenOpt;
}
bool InferBoundsResult::inconsistentState() const {
  return d_inconsistentState;
}

bool InferBoundsResult::boundIsInteger() const{
  return foundBound() && d_value.isIntegral();
}

bool InferBoundsResult::boundIsRational() const {
  return foundBound() && d_value.infinitesimalIsZero();
}

Integer InferBoundsResult::valueAsInteger() const{
  Assert(boundIsInteger());
  return getValue().floor();
}
const Rational& InferBoundsResult::valueAsRational() const{
  Assert(boundIsRational());
  return getValue().getNoninfinitesimalPart();
}

const DeltaRational& InferBoundsResult::getValue() const{
  return d_value;
}

Node InferBoundsResult::getTerm() const { return d_term; }

Node InferBoundsResult::getLiteral() const{
  const Rational& q = getValue().getNoninfinitesimalPart();
  NodeManager* nm = NodeManager::currentNM();
  Node qnode = nm->mkConst(q);

  Kind k;
  if(d_upperBound){
    // x <= q + c*delta
    Assert(getValue().infinitesimalSgn() <= 0);
    k = boundIsRational() ? kind::LEQ : kind::LT;
  }else{
    // x >= q + c*delta
    Assert(getValue().infinitesimalSgn() >= 0);
    k = boundIsRational() ? kind::GEQ : kind::GT;
  }
  Node atom = nm->mkNode(k, getTerm(), qnode);
  Node lit = Rewriter::rewrite(atom);
  return lit;
}

/* If there is a bound, this is a node that explains the bound. */
Node InferBoundsResult::getExplanation() const{
  return d_explanation;
}


void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){
  d_foundBound = true;
  d_value = dr;
  d_explanation = exp;
}

void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; }
void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; }
void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; }
void InferBoundsResult::setInconsistent() { d_inconsistentState = true; }

bool InferBoundsResult::thresholdWasReached() const{
  return d_reachedThreshold;
}
bool InferBoundsResult::budgetIsExhausted() const{
  return d_budgetExhausted;
}

std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){
  os << "{InferBoundsResult " << std::endl;
  os << "on " << ibr.getTerm() << ", ";
  if(ibr.findUpperBound()){
    os << "find upper bound, ";
  }else{
    os << "find lower bound, ";
  }
  if(ibr.foundBound()){
    os << "found a bound: ";
    if(ibr.boundIsInteger()){
      os << ibr.valueAsInteger() << "(int), ";
    }else if(ibr.boundIsRational()){
      os << ibr.valueAsRational() << "(rat), ";
    }else{
      os << ibr.getValue() << "(extended), ";
    }

    os << "as term " << ibr.getLiteral() << ", ";
    os << "explanation " << ibr.getExplanation() << ", ";
  }else {
    os << "did not find a bound, ";
  }

  if(ibr.boundIsOptimal()){
    os << "(opt), ";
  }

  if(ibr.inconsistentState()){
    os << "(inconsistent), ";
  }
  if(ibr.budgetIsExhausted()){
    os << "(budget exhausted), ";
  }
  if(ibr.thresholdWasReached()){
    os << "(reached threshold), ";
  }
  os << "}";
  return os;
}

ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
    : d_simplexSideEffects(NULL)
{}

ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
  if(d_simplexSideEffects != NULL){
    delete d_simplexSideEffects;
    d_simplexSideEffects = NULL;
  }
}

InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){
  if(d_simplexSideEffects == NULL){
    d_simplexSideEffects = new InferBoundsResult;
  }
  return *d_simplexSideEffects;
}

namespace inferbounds { /* namespace arith */

std::ostream& operator<<(std::ostream& os,  const Algorithms a){
  switch(a){
  case None:    os << "AlgNone"; break;
  case Lookup:  os << "AlgLookup"; break;
  case RowSum:  os << "AlgRowSum"; break;
  case Simplex: os << "AlgSimplex"; break;
  default:
    Unhandled();
  }

  return os;
}

} /* namespace inferbounds */

} /* namespace arith */
} /* namespace theory */
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, 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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "theory/arith/infer_bounds.h"
20		#include "theory/rewriter.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace arith {
25
26		using namespace inferbounds;
27
28		InferBoundAlgorithm::InferBoundAlgorithm()
29		: d_alg(None)
30		{}
31
32	9660	InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
33	9660	: d_alg(a)
34		{
35	9660	Assert(a != Simplex);
36	9660	}
37
38		InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds)
39		: d_alg(Simplex)
40		{}
41
42	28734	Algorithms InferBoundAlgorithm::getAlgorithm() const{
43	28734	return d_alg;
44		}
45
46		const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{
47		Assert(getAlgorithm() == Simplex);
48		return d_simplexRounds;
49		}
50
51
52	4830	InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
53	4830	return InferBoundAlgorithm(Lookup);
54		}
55
56	4830	InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
57	4830	return InferBoundAlgorithm(RowSum);
58		}
59
60		InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
61		return InferBoundAlgorithm(rounds);
62		}
63
64	4830	ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
65	4830	: d_algorithms()
66	4830	{}
67
68	4830	ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
69	4830	{}
70
71
72	4830	void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){
73	4830	addAlgorithm(InferBoundAlgorithm::mkLookup());
74	4830	addAlgorithm(InferBoundAlgorithm::mkRowSum());
75	4830	}
76
77	9660	void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){
78	9660	d_algorithms.push_back(alg);
79	9660	}
80
81	4830	ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{
82	4830	return d_algorithms.begin();
83		}
84
85	4830	ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{
86	4830	return d_algorithms.end();
87		}
88
89		InferBoundsResult::InferBoundsResult()
90		: d_foundBound(false)
91		, d_budgetExhausted(false)
92		, d_boundIsProvenOpt(false)
93		, d_inconsistentState(false)
94		, d_reachedThreshold(false)
95		, d_value(false)
96		, d_term(Node::null())
97		, d_upperBound(true)
98		, d_explanation(Node::null())
99		{}
100
101		InferBoundsResult::InferBoundsResult(Node term, bool ub)
102		: d_foundBound(false)
103		, d_budgetExhausted(false)
104		, d_boundIsProvenOpt(false)
105		, d_inconsistentState(false)
106		, d_reachedThreshold(false)
107		, d_value(false)
108		, d_term(term)
109		, d_upperBound(ub)
110		, d_explanation(Node::null())
111		{}
112
113		bool InferBoundsResult::foundBound() const {
114		return d_foundBound;
115		}
116		bool InferBoundsResult::boundIsOptimal() const {
117		return d_boundIsProvenOpt;
118		}
119		bool InferBoundsResult::inconsistentState() const {
120		return d_inconsistentState;
121		}
122
123		bool InferBoundsResult::boundIsInteger() const{
124		return foundBound() && d_value.isIntegral();
125		}
126
127		bool InferBoundsResult::boundIsRational() const {
128		return foundBound() && d_value.infinitesimalIsZero();
129		}
130
131		Integer InferBoundsResult::valueAsInteger() const{
132		Assert(boundIsInteger());
133		return getValue().floor();
134		}
135		const Rational& InferBoundsResult::valueAsRational() const{
136		Assert(boundIsRational());
137		return getValue().getNoninfinitesimalPart();
138		}
139
140		const DeltaRational& InferBoundsResult::getValue() const{
141		return d_value;
142		}
143
144		Node InferBoundsResult::getTerm() const { return d_term; }
145
146		Node InferBoundsResult::getLiteral() const{
147		const Rational& q = getValue().getNoninfinitesimalPart();
148		NodeManager* nm = NodeManager::currentNM();
149		Node qnode = nm->mkConst(q);
150
151		Kind k;
152		if(d_upperBound){
153		// x <= q + c*delta
154		Assert(getValue().infinitesimalSgn() <= 0);
155		k = boundIsRational() ? kind::LEQ : kind::LT;
156		}else{
157		// x >= q + c*delta
158		Assert(getValue().infinitesimalSgn() >= 0);
159		k = boundIsRational() ? kind::GEQ : kind::GT;
160		}
161		Node atom = nm->mkNode(k, getTerm(), qnode);
162		Node lit = Rewriter::rewrite(atom);
163		return lit;
164		}
165
166		/* If there is a bound, this is a node that explains the bound. */
167		Node InferBoundsResult::getExplanation() const{
168		return d_explanation;
169		}
170
171
172		void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){
173		d_foundBound = true;
174		d_value = dr;
175		d_explanation = exp;
176		}
177
178		void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; }
179		void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; }
180		void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; }
181		void InferBoundsResult::setInconsistent() { d_inconsistentState = true; }
182
183		bool InferBoundsResult::thresholdWasReached() const{
184		return d_reachedThreshold;
185		}
186		bool InferBoundsResult::budgetIsExhausted() const{
187		return d_budgetExhausted;
188		}
189
190		std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){
191		os << "{InferBoundsResult " << std::endl;
192		os << "on " << ibr.getTerm() << ", ";
193		if(ibr.findUpperBound()){
194		os << "find upper bound, ";
195		}else{
196		os << "find lower bound, ";
197		}
198		if(ibr.foundBound()){
199		os << "found a bound: ";
200		if(ibr.boundIsInteger()){
201		os << ibr.valueAsInteger() << "(int), ";
202		}else if(ibr.boundIsRational()){
203		os << ibr.valueAsRational() << "(rat), ";
204		}else{
205		os << ibr.getValue() << "(extended), ";
206		}
207
208		os << "as term " << ibr.getLiteral() << ", ";
209		os << "explanation " << ibr.getExplanation() << ", ";
210		}else {
211		os << "did not find a bound, ";
212		}
213
214		if(ibr.boundIsOptimal()){
215		os << "(opt), ";
216		}
217
218		if(ibr.inconsistentState()){
219		os << "(inconsistent), ";
220		}
221		if(ibr.budgetIsExhausted()){
222		os << "(budget exhausted), ";
223		}
224		if(ibr.thresholdWasReached()){
225		os << "(reached threshold), ";
226		}
227		os << "}";
228		return os;
229		}
230
231	4830	ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
232	4830	: d_simplexSideEffects(NULL)
233	4830	{}
234
235	9660	ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
236	4830	if(d_simplexSideEffects != NULL){
237		delete d_simplexSideEffects;
238		d_simplexSideEffects = NULL;
239		}
240	4830	}
241
242		InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){
243		if(d_simplexSideEffects == NULL){
244		d_simplexSideEffects = new InferBoundsResult;
245		}
246		return *d_simplexSideEffects;
247		}
248
249		namespace inferbounds { /* namespace arith */
250
251		std::ostream& operator<<(std::ostream& os, const Algorithms a){
252		switch(a){
253		case None: os << "AlgNone"; break;
254		case Lookup: os << "AlgLookup"; break;
255		case RowSum: os << "AlgRowSum"; break;
256		case Simplex: os << "AlgSimplex"; break;
257		default:
258		Unhandled();
259		}
260
261		return os;
262		}
263
264		} /* namespace inferbounds */
265
266		} /* namespace arith */
267		} /* namespace theory */
268	28191	} // namespace cvc5