Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/callbacks.cpp	Lines:	100	114	87.7 %
Date:	2021-08-01	Branches:	112	466	24.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Haniel Barbosa, Mathias Preiner
 *
 * 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/callbacks.h"

#include "expr/skolem_manager.h"
#include "proof/proof_node.h"
#include "theory/arith/proof_macros.h"
#include "theory/arith/theory_arith_private.h"

namespace cvc5 {
namespace theory {
namespace arith {

SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta)
  : d_arith(ta)
{}
void SetupLiteralCallBack::operator()(TNode lit){
  TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
  if(!d_arith.isSetup(atom)){
    d_arith.setupAtom(atom);
  }
}

DeltaComputeCallback::DeltaComputeCallback(const TheoryArithPrivate& ta)
  : d_ta(ta)
{}
Rational DeltaComputeCallback::operator()() const{
  return d_ta.deltaValueForTotalOrder();
}

TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
: d_ta(ta)
{}
ArithVar TempVarMalloc::request(){
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Node skolem = sm->mkDummySkolem("tmpVar", nm->realType());
  return d_ta.requestArithVar(skolem, false, true);
}
void TempVarMalloc::release(ArithVar v){
  d_ta.releaseArithVar(v);
}

BasicVarModelUpdateCallBack::BasicVarModelUpdateCallBack(TheoryArithPrivate& ta)
  : d_ta(ta)
{}
void BasicVarModelUpdateCallBack::operator()(ArithVar x){
  d_ta.signal(x);
}

RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
  : d_ta(ta)
{}

void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
  Assert(c->inConflict());
  d_ta.raiseConflict(c, id);
}

FarkasConflictBuilder::FarkasConflictBuilder()
  : d_farkas()
  , d_constraints()
  , d_consequent(NullConstraint)
  , d_consequentSet(false)
{
  reset();
}

bool FarkasConflictBuilder::underConstruction() const{
  return d_consequent != NullConstraint;
}

bool FarkasConflictBuilder::consequentIsSet() const{
  return d_consequentSet;
}

void FarkasConflictBuilder::reset(){
  d_consequent = NullConstraint;
  d_constraints.clear();
  d_consequentSet = false;
  ARITH_PROOF(d_farkas.clear());
  Assert(!underConstruction());
}

/* Adds a constraint to the constraint under construction. */
void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
  Assert(
      !ARITH_PROOF_ON()
      || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
      || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
  Assert(ARITH_PROOF_ON() || d_farkas.empty());
  Assert(c->isTrue());

  if(d_consequent == NullConstraint){
    d_consequent = c;
  } else {
    d_constraints.push_back(c);
  }
  ARITH_PROOF(d_farkas.push_back(fc));
  Assert(!ARITH_PROOF_ON() || d_constraints.size() + 1 == d_farkas.size());
  Assert(ARITH_PROOF_ON() || d_farkas.empty());
}

void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
  Assert(!mult.isZero());
  if (ARITH_PROOF_ON() && !mult.isOne())
  {
    Rational prod = fc * mult;
    addConstraint(c, prod);
  }
  else
  {
    addConstraint(c, fc);
  }
}

void FarkasConflictBuilder::makeLastConsequent(){
  Assert(!d_consequentSet);
  Assert(underConstruction());

  if(d_constraints.empty()){
    // no-op
    d_consequentSet = true;
  } else {
    Assert(d_consequent != NullConstraint);
    ConstraintCP last = d_constraints.back();
    d_constraints.back() = d_consequent;
    d_consequent = last;
    ARITH_PROOF(std::swap(d_farkas.front(), d_farkas.back()));
    d_consequentSet = true;
  }

  Assert(!d_consequent->negationHasProof());
  Assert(d_consequentSet);
}

/* Turns the vector under construction into a conflict */
ConstraintCP FarkasConflictBuilder::commitConflict(){
  Assert(underConstruction());
  Assert(!d_constraints.empty());
  Assert(
      !ARITH_PROOF_ON()
      || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
      || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
  Assert(ARITH_PROOF_ON() || d_farkas.empty());
  Assert(d_consequentSet);

  ConstraintP not_c = d_consequent->getNegation();
  RationalVectorCP coeffs = ARITH_NULLPROOF(&d_farkas);
  not_c->impliedByFarkas(d_constraints, coeffs, true );

  reset();
  Assert(!underConstruction());
  Assert(not_c->inConflict());
  Assert(!d_consequentSet);
  return not_c;
}

RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
  : d_ta(ta)
{}

/* If you are not an equality engine, don't use this! */
void RaiseEqualityEngineConflict::raiseEEConflict(
    Node n, std::shared_ptr<ProofNode> pf) const
{
  d_ta.raiseBlackBoxConflict(n, pf);
}

BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
: d_ta(ta)
{}

const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{
  return d_ta.boundsInfo(basic);
}

BoundCounts BoundCountingLookup::atBounds(ArithVar basic) const{
  return boundsInfo(basic).atBounds();
}
BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const {
  return boundsInfo(basic).hasBounds();
}

}  // 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, Haniel Barbosa, Mathias Preiner
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/callbacks.h"
20
21		#include "expr/skolem_manager.h"
22		#include "proof/proof_node.h"
23		#include "theory/arith/proof_macros.h"
24		#include "theory/arith/theory_arith_private.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace arith {
29
30	9838	SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta)
31	9838	: d_arith(ta)
32	9838	{}
33	18905	void SetupLiteralCallBack::operator()(TNode lit){
34	37810	TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
35	18905	if(!d_arith.isSetup(atom)){
36	18905	d_arith.setupAtom(atom);
37		}
38	18905	}
39
40	9838	DeltaComputeCallback::DeltaComputeCallback(const TheoryArithPrivate& ta)
41	9838	: d_ta(ta)
42	9838	{}
43	12708	Rational DeltaComputeCallback::operator()() const{
44	12708	return d_ta.deltaValueForTotalOrder();
45		}
46
47	39352	TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
48	39352	: d_ta(ta)
49	39352	{}
50		ArithVar TempVarMalloc::request(){
51		NodeManager* nm = NodeManager::currentNM();
52		SkolemManager* sm = nm->getSkolemManager();
53		Node skolem = sm->mkDummySkolem("tmpVar", nm->realType());
54		return d_ta.requestArithVar(skolem, false, true);
55		}
56		void TempVarMalloc::release(ArithVar v){
57		d_ta.releaseArithVar(v);
58		}
59
60	9838	BasicVarModelUpdateCallBack::BasicVarModelUpdateCallBack(TheoryArithPrivate& ta)
61	9838	: d_ta(ta)
62	9838	{}
63	5535966	void BasicVarModelUpdateCallBack::operator()(ArithVar x){
64	5535966	d_ta.signal(x);
65	5535966	}
66
67	49190	RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
68	49190	: d_ta(ta)
69	49190	{}
70
71	58041	void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
72	58041	Assert(c->inConflict());
73	58041	d_ta.raiseConflict(c, id);
74	58041	}
75
76	39352	FarkasConflictBuilder::FarkasConflictBuilder()
77		: d_farkas()
78		, d_constraints()
79		, d_consequent(NullConstraint)
80	39352	, d_consequentSet(false)
81		{
82	39352	reset();
83	39352	}
84
85	725741	bool FarkasConflictBuilder::underConstruction() const{
86	725741	return d_consequent != NullConstraint;
87		}
88
89	58041	bool FarkasConflictBuilder::consequentIsSet() const{
90	58041	return d_consequentSet;
91		}
92
93	97393	void FarkasConflictBuilder::reset(){
94	97393	d_consequent = NullConstraint;
95	97393	d_constraints.clear();
96	97393	d_consequentSet = false;
97	97393	ARITH_PROOF(d_farkas.clear());
98	97393	Assert(!underConstruction());
99	97393	}
100
101		/* Adds a constraint to the constraint under construction. */
102	860137	void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
103	860137	Assert(
104		!ARITH_PROOF_ON()
105		\|\| (!underConstruction() && d_constraints.empty() && d_farkas.empty())
106		\|\| (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
107	860137	Assert(ARITH_PROOF_ON() \|\| d_farkas.empty());
108	860137	Assert(c->isTrue());
109
110	860137	if(d_consequent == NullConstraint){
111	58041	d_consequent = c;
112		} else {
113	802096	d_constraints.push_back(c);
114		}
115	860137	ARITH_PROOF(d_farkas.push_back(fc));
116	860137	Assert(!ARITH_PROOF_ON() \|\| d_constraints.size() + 1 == d_farkas.size());
117	860137	Assert(ARITH_PROOF_ON() \|\| d_farkas.empty());
118	860137	}
119
120	860137	void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
121	860137	Assert(!mult.isZero());
122	860137	if (ARITH_PROOF_ON() && !mult.isOne())
123		{
124	175136	Rational prod = fc * mult;
125	87568	addConstraint(c, prod);
126		}
127		else
128		{
129	772569	addConstraint(c, fc);
130		}
131	860137	}
132
133	58041	void FarkasConflictBuilder::makeLastConsequent(){
134	58041	Assert(!d_consequentSet);
135	58041	Assert(underConstruction());
136
137	58041	if(d_constraints.empty()){
138		// no-op
139	2383	d_consequentSet = true;
140		} else {
141	55658	Assert(d_consequent != NullConstraint);
142	55658	ConstraintCP last = d_constraints.back();
143	55658	d_constraints.back() = d_consequent;
144	55658	d_consequent = last;
145	55658	ARITH_PROOF(std::swap(d_farkas.front(), d_farkas.back()));
146	55658	d_consequentSet = true;
147		}
148
149	58041	Assert(!d_consequent->negationHasProof());
150	58041	Assert(d_consequentSet);
151	58041	}
152
153		/* Turns the vector under construction into a conflict */
154	58041	ConstraintCP FarkasConflictBuilder::commitConflict(){
155	58041	Assert(underConstruction());
156	58041	Assert(!d_constraints.empty());
157	58041	Assert(
158		!ARITH_PROOF_ON()
159		\|\| (!underConstruction() && d_constraints.empty() && d_farkas.empty())
160		\|\| (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
161	58041	Assert(ARITH_PROOF_ON() \|\| d_farkas.empty());
162	58041	Assert(d_consequentSet);
163
164	58041	ConstraintP not_c = d_consequent->getNegation();
165	58041	RationalVectorCP coeffs = ARITH_NULLPROOF(&d_farkas);
166	58041	not_c->impliedByFarkas(d_constraints, coeffs, true );
167
168	58041	reset();
169	58041	Assert(!underConstruction());
170	58041	Assert(not_c->inConflict());
171	58041	Assert(!d_consequentSet);
172	58041	return not_c;
173		}
174
175	9838	RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
176	9838	: d_ta(ta)
177	9838	{}
178
179		/* If you are not an equality engine, don't use this! */
180	1990	void RaiseEqualityEngineConflict::raiseEEConflict(
181		Node n, std::shared_ptr<ProofNode> pf) const
182		{
183	1990	d_ta.raiseBlackBoxConflict(n, pf);
184	1990	}
185
186	9838	BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
187	9838	: d_ta(ta)
188	9838	{}
189
190		const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{
191		return d_ta.boundsInfo(basic);
192		}
193
194		BoundCounts BoundCountingLookup::atBounds(ArithVar basic) const{
195		return boundsInfo(basic).atBounds();
196		}
197		BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const {
198		return boundsInfo(basic).hasBounds();
199		}
200
201		} // namespace arith
202		} // namespace theory
203	29280	} // namespace cvc5