Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/assertions.cpp	Lines:	80	93	86.0 %
Date:	2021-09-18	Branches:	98	210	46.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
 *
 * 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.
 * ****************************************************************************
 *
 * The module for storing assertions for an SMT engine.
 */

#include "smt/assertions.h"

#include <sstream>

#include "base/modal_exception.h"
#include "expr/node_algorithm.h"
#include "options/base_options.h"
#include "options/expr_options.h"
#include "options/language.h"
#include "options/smt_options.h"
#include "smt/abstract_values.h"
#include "smt/env.h"
#include "smt/smt_engine.h"
#include "theory/trust_substitutions.h"

using namespace cvc5::theory;
using namespace cvc5::kind;

namespace cvc5 {
namespace smt {

Assertions::Assertions(Env& env, AbstractValues& absv)
    : d_env(env),
      d_absValues(absv),
      d_produceAssertions(false),
      d_assertionList(env.getUserContext()),
      d_globalNegation(false),
      d_assertions()
{
}

Assertions::~Assertions()
{
}

void Assertions::finishInit()
{
  // [MGD 10/20/2011] keep around in incremental mode, due to a
  // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
  // first, some user-context-dependent TNodes might still exist
  // with rc == 0.
  if (options::produceAssertions() || options::incrementalSolving())
  {
    // In the case of incremental solving, we appear to need these to
    // ensure the relevant Nodes remain live.
    d_produceAssertions = true;
    d_globalDefineFunLemmas.reset(new std::vector<Node>());
  }
}

void Assertions::clearCurrent()
{
  d_assertions.clear();
  d_assertions.getIteSkolemMap().clear();
}

void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
                                    bool isEntailmentCheck)
{
  NodeManager* nm = NodeManager::currentNM();
  // reset global negation
  d_globalNegation = false;
  // clear the assumptions
  d_assumptions.clear();
  if (isEntailmentCheck)
  {
    size_t size = assumptions.size();
    if (size > 1)
    {
      /* Assume: not (BIGAND assumptions)  */
      d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode());
    }
    else if (size == 1)
    {
      /* Assume: not expr  */
      d_assumptions.push_back(assumptions[0].notNode());
    }
  }
  else
  {
    /* Assume: BIGAND assumptions  */
    d_assumptions = assumptions;
  }

  Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
  for (const Node& e : d_assumptions)
  {
    // Substitute out any abstract values in ex.
    Node n = d_absValues.substituteAbstractValues(e);
    // Ensure expr is type-checked at this point.
    ensureBoolean(n);
    addFormula(n, true, true, false, false);
  }
  if (d_globalDefineFunLemmas != nullptr)
  {
    // Global definitions are asserted at check-sat-time because we have to
    // make sure that they are always present (they are essentially level
    // zero assertions)
    for (const Node& lemma : *d_globalDefineFunLemmas)
    {
      addFormula(lemma, true, false, true, false);
    }
  }
}

void Assertions::assertFormula(const Node& n)
{
  ensureBoolean(n);
  bool maybeHasFv = language::isLangSygus(options::inputLanguage());
  addFormula(n, true, false, false, maybeHasFv);
}

std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
bool Assertions::isGlobalNegated() const { return d_globalNegation; }
void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; }

preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
{
  return d_assertions;
}

context::CDList<Node>* Assertions::getAssertionList()
{
  return d_produceAssertions ? &d_assertionList : nullptr;
}

void Assertions::addFormula(TNode n,
                            bool inInput,
                            bool isAssumption,
                            bool isFunDef,
                            bool maybeHasFv)
{
  // add to assertion list if it exists
  if (d_produceAssertions)
  {
    d_assertionList.push_back(n);
  }
  if (n.isConst() && n.getConst<bool>())
  {
    // true, nothing to do
    return;
  }
  Trace("smt") << "SmtEnginePrivate::addFormula(" << n
               << ", inInput = " << inInput
               << ", isAssumption = " << isAssumption
               << ", isFunDef = " << isFunDef << std::endl;
  if (isFunDef)
  {
    // if a non-recursive define-fun, just add as a top-level substitution
    if (n.getKind() == EQUAL && n[0].isVar())
    {
      // A define-fun is an assumption in the overall proof, thus
      // we justify the substitution with ASSUME here.
      d_env.getTopLevelSubstitutions().addSubstitution(
          n[0], n[1], PfRule::ASSUME, {}, {n});
      return;
    }
  }

  // Ensure that it does not contain free variables
  if (maybeHasFv)
  {
    if (expr::hasFreeVar(n))
    {
      std::stringstream se;
      if (isFunDef)
      {
        se << "Cannot process function definition with free variable.";
      }
      else
      {
        se << "Cannot process assertion with free variable.";
        if (language::isLangSygus(options::inputLanguage()))
        {
          // Common misuse of SyGuS is to use top-level assert instead of
          // constraint when defining the synthesis conjecture.
          se << " Perhaps you meant `constraint` instead of `assert`?";
        }
      }
      throw ModalException(se.str().c_str());
    }
  }

  // Add the normalized formula to the queue
  d_assertions.push_back(n, isAssumption, true);
}

void Assertions::addDefineFunDefinition(Node n, bool global)
{
  n = d_absValues.substituteAbstractValues(n);
  if (global && d_globalDefineFunLemmas != nullptr)
  {
    // Global definitions are asserted at check-sat-time because we have to
    // make sure that they are always present
    Assert(!language::isLangSygus(options::inputLanguage()));
    d_globalDefineFunLemmas->emplace_back(n);
  }
  else
  {
    // We don't permit functions-to-synthesize within recursive function
    // definitions currently. Thus, we should check for free variables if the
    // input language is SyGuS.
    bool maybeHasFv = language::isLangSygus(options::inputLanguage());
    addFormula(n, true, false, true, maybeHasFv);
  }
}

void Assertions::ensureBoolean(const Node& n)
{
  TypeNode type = n.getType(options::typeChecking());
  if (!type.isBoolean())
  {
    std::stringstream ss;
    ss << "Expected Boolean type\n"
       << "The assertion : " << n << "\n"
       << "Its type      : " << type;
    throw TypeCheckingExceptionPrivate(n, ss.str());
  }
}

void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
{
  d_assertions.setProofGenerator(pppg);
}

bool Assertions::isProofEnabled() const
{
  return d_assertions.isProofEnabled();
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, Haniel Barbosa
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		* The module for storing assertions for an SMT engine.
14		*/
15
16		#include "smt/assertions.h"
17
18		#include <sstream>
19
20		#include "base/modal_exception.h"
21		#include "expr/node_algorithm.h"
22		#include "options/base_options.h"
23		#include "options/expr_options.h"
24		#include "options/language.h"
25		#include "options/smt_options.h"
26		#include "smt/abstract_values.h"
27		#include "smt/env.h"
28		#include "smt/smt_engine.h"
29		#include "theory/trust_substitutions.h"
30
31		using namespace cvc5::theory;
32		using namespace cvc5::kind;
33
34		namespace cvc5 {
35		namespace smt {
36
37	13207	Assertions::Assertions(Env& env, AbstractValues& absv)
38		: d_env(env),
39		d_absValues(absv),
40		d_produceAssertions(false),
41	13207	d_assertionList(env.getUserContext()),
42		d_globalNegation(false),
43	26414	d_assertions()
44		{
45	13207	}
46
47	10560	Assertions::~Assertions()
48		{
49	10560	}
50
51	9940	void Assertions::finishInit()
52		{
53		// [MGD 10/20/2011] keep around in incremental mode, due to a
54		// cleanup ordering issue and Nodes/TNodes. If SAT is popped
55		// first, some user-context-dependent TNodes might still exist
56		// with rc == 0.
57	9940	if (options::produceAssertions() \|\| options::incrementalSolving())
58		{
59		// In the case of incremental solving, we appear to need these to
60		// ensure the relevant Nodes remain live.
61	7610	d_produceAssertions = true;
62	7610	d_globalDefineFunLemmas.reset(new std::vector<Node>());
63		}
64	9940	}
65
66	17350	void Assertions::clearCurrent()
67		{
68	17350	d_assertions.clear();
69	17350	d_assertions.getIteSkolemMap().clear();
70	17350	}
71
72	15276	void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
73		bool isEntailmentCheck)
74		{
75	15276	NodeManager* nm = NodeManager::currentNM();
76		// reset global negation
77	15276	d_globalNegation = false;
78		// clear the assumptions
79	15276	d_assumptions.clear();
80	15276	if (isEntailmentCheck)
81		{
82	663	size_t size = assumptions.size();
83	663	if (size > 1)
84		{
85		/* Assume: not (BIGAND assumptions) */
86	2	d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode());
87		}
88	661	else if (size == 1)
89		{
90		/* Assume: not expr */
91	661	d_assumptions.push_back(assumptions[0].notNode());
92		}
93		}
94		else
95		{
96		/* Assume: BIGAND assumptions */
97	14613	d_assumptions = assumptions;
98		}
99
100	30552	Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
101	17767	for (const Node& e : d_assumptions)
102		{
103		// Substitute out any abstract values in ex.
104	4982	Node n = d_absValues.substituteAbstractValues(e);
105		// Ensure expr is type-checked at this point.
106	2491	ensureBoolean(n);
107	2491	addFormula(n, true, true, false, false);
108		}
109	15276	if (d_globalDefineFunLemmas != nullptr)
110		{
111		// Global definitions are asserted at check-sat-time because we have to
112		// make sure that they are always present (they are essentially level
113		// zero assertions)
114	13255	for (const Node& lemma : *d_globalDefineFunLemmas)
115		{
116	297	addFormula(lemma, true, false, true, false);
117		}
118		}
119	15276	}
120
121	89166	void Assertions::assertFormula(const Node& n)
122		{
123	89166	ensureBoolean(n);
124	89166	bool maybeHasFv = language::isLangSygus(options::inputLanguage());
125	89166	addFormula(n, true, false, false, maybeHasFv);
126	89166	}
127
128	13	std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
129	15246	bool Assertions::isGlobalNegated() const { return d_globalNegation; }
130	6	void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; }
131
132	51849	preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
133		{
134	51849	return d_assertions;
135		}
136
137	6666	context::CDList<Node>* Assertions::getAssertionList()
138		{
139	6666	return d_produceAssertions ? &d_assertionList : nullptr;
140		}
141
142	94204	void Assertions::addFormula(TNode n,
143		bool inInput,
144		bool isAssumption,
145		bool isFunDef,
146		bool maybeHasFv)
147		{
148		// add to assertion list if it exists
149	94204	if (d_produceAssertions)
150		{
151	63475	d_assertionList.push_back(n);
152		}
153	94204	if (n.isConst() && n.getConst<bool>())
154		{
155		// true, nothing to do
156	530	return;
157		}
158	187348	Trace("smt") << "SmtEnginePrivate::addFormula(" << n
159	93674	<< ", inInput = " << inInput
160	93674	<< ", isAssumption = " << isAssumption
161	93674	<< ", isFunDef = " << isFunDef << std::endl;
162	93674	if (isFunDef)
163		{
164		// if a non-recursive define-fun, just add as a top-level substitution
165	2547	if (n.getKind() == EQUAL && n[0].isVar())
166		{
167		// A define-fun is an assumption in the overall proof, thus
168		// we justify the substitution with ASSUME here.
169	4732	d_env.getTopLevelSubstitutions().addSubstitution(
170	2366	n[0], n[1], PfRule::ASSUME, {}, {n});
171	2366	return;
172		}
173		}
174
175		// Ensure that it does not contain free variables
176	91308	if (maybeHasFv)
177		{
178	558	if (expr::hasFreeVar(n))
179		{
180		std::stringstream se;
181		if (isFunDef)
182		{
183		se << "Cannot process function definition with free variable.";
184		}
185		else
186		{
187		se << "Cannot process assertion with free variable.";
188		if (language::isLangSygus(options::inputLanguage()))
189		{
190		// Common misuse of SyGuS is to use top-level assert instead of
191		// constraint when defining the synthesis conjecture.
192		se << " Perhaps you meant `constraint` instead of `assert`?";
193		}
194		}
195		throw ModalException(se.str().c_str());
196		}
197		}
198
199		// Add the normalized formula to the queue
200	91308	d_assertions.push_back(n, isAssumption, true);
201		}
202
203	2467	void Assertions::addDefineFunDefinition(Node n, bool global)
204		{
205	2467	n = d_absValues.substituteAbstractValues(n);
206	2467	if (global && d_globalDefineFunLemmas != nullptr)
207		{
208		// Global definitions are asserted at check-sat-time because we have to
209		// make sure that they are always present
210	217	Assert(!language::isLangSygus(options::inputLanguage()));
211	217	d_globalDefineFunLemmas->emplace_back(n);
212		}
213		else
214		{
215		// We don't permit functions-to-synthesize within recursive function
216		// definitions currently. Thus, we should check for free variables if the
217		// input language is SyGuS.
218	2250	bool maybeHasFv = language::isLangSygus(options::inputLanguage());
219	2250	addFormula(n, true, false, true, maybeHasFv);
220		}
221	2467	}
222
223	91657	void Assertions::ensureBoolean(const Node& n)
224		{
225	183314	TypeNode type = n.getType(options::typeChecking());
226	91657	if (!type.isBoolean())
227		{
228		std::stringstream ss;
229		ss << "Expected Boolean type\n"
230		<< "The assertion : " << n << "\n"
231		<< "Its type : " << type;
232		throw TypeCheckingExceptionPrivate(n, ss.str());
233		}
234	91657	}
235
236	3794	void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
237		{
238	3794	d_assertions.setProofGenerator(pppg);
239	3794	}
240
241		bool Assertions::isProofEnabled() const
242		{
243		return d_assertions.isProofEnabled();
244		}
245
246		} // namespace smt
247	29574	} // namespace cvc5