Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/process_assertions.cpp	Lines:	173	186	93.0 %
Date:	2021-08-14	Branches:	355	694	51.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Morgan Deters, Aina Niemetz
 *
 * 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 module for processing assertions for an SMT engine.
 */

#include "smt/process_assertions.h"

#include <utility>

#include "expr/node_manager_attributes.h"
#include "options/arith_options.h"
#include "options/base_options.h"
#include "options/bv_options.h"
#include "options/quantifiers_options.h"
#include "options/sep_options.h"
#include "options/smt_options.h"
#include "options/strings_options.h"
#include "options/uf_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/preprocessing_pass_registry.h"
#include "printer/printer.h"
#include "smt/assertions.h"
#include "smt/dump.h"
#include "smt/expand_definitions.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_stats.h"
#include "theory/logic_info.h"
#include "theory/theory_engine.h"

using namespace std;
using namespace cvc5::preprocessing;
using namespace cvc5::theory;
using namespace cvc5::kind;

namespace cvc5 {
namespace smt {

/** Useful for counting the number of recursive calls. */
class ScopeCounter
{
 public:
  ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
  ~ScopeCounter() { --d_depth; }

 private:
  unsigned& d_depth;
};

ProcessAssertions::ProcessAssertions(SmtEngine& smt,
                                     ResourceManager& rm,
                                     SmtEngineStatistics& stats)
    : d_smt(smt),
      d_resourceManager(rm),
      d_smtStats(stats),
      d_preprocessingPassContext(nullptr)
{
  d_true = NodeManager::currentNM()->mkConst(true);
}

ProcessAssertions::~ProcessAssertions()
{
}

void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
{
  Assert(d_preprocessingPassContext == nullptr);
  d_preprocessingPassContext = pc;

  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
  // TODO: this will likely change when we add support for actually assembling
  // preprocessing pipelines. For now, we just create an instance of each
  // available preprocessing pass.
  std::vector<std::string> passNames = ppReg.getAvailablePasses();
  for (const std::string& passName : passNames)
  {
    d_passes[passName].reset(
        ppReg.createPass(d_preprocessingPassContext, passName));
  }
}

void ProcessAssertions::cleanup() { d_passes.clear(); }

void ProcessAssertions::spendResource(Resource r)
{
  d_resourceManager.spendResource(r);
}

bool ProcessAssertions::apply(Assertions& as)
{
  AssertionPipeline& assertions = as.getAssertionPipeline();
  Assert(d_preprocessingPassContext != nullptr);
  // Dump the assertions
  dumpAssertions("pre-everything", assertions);

  Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
  Trace("smt") << "ProcessAssertions::processAssertions()" << endl;

  Debug("smt") << "#Assertions : " << assertions.size() << endl;
  Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;

  if (assertions.size() == 0)
  {
    // nothing to do
    return true;
  }

  if (options::bvGaussElim())
  {
    d_passes["bv-gauss"]->apply(&assertions);
  }

  // Add dummy assertion in last position - to be used as a
  // placeholder for any new assertions to get added
  assertions.push_back(d_true);
  // any assertions added beyond realAssertionsEnd must NOT affect the
  // equisatisfiability
  assertions.updateRealAssertionsEnd();

  // Assertions are NOT guaranteed to be rewritten by this point

  Trace("smt-proc")
      << "ProcessAssertions::processAssertions() : pre-definition-expansion"
      << endl;
  dumpAssertions("pre-definition-expansion", assertions);
  // Apply substitutions first. If we are non-incremental, this has only the
  // effect of replacing defined functions with their definitions.
  // We do not call theory-specific expand definitions here, since we want
  // to give the opportunity to rewrite/preprocess terms before expansion.
  d_passes["apply-substs"]->apply(&assertions);
  Trace("smt-proc")
      << "ProcessAssertions::processAssertions() : post-definition-expansion"
      << endl;
  dumpAssertions("post-definition-expansion", assertions);

  Debug("smt") << " assertions     : " << assertions.size() << endl;

  if (options::globalNegate())
  {
    // global negation of the formula
    d_passes["global-negate"]->apply(&assertions);
    as.flipGlobalNegated();
  }

  if (options::nlExtPurify())
  {
    d_passes["nl-ext-purify"]->apply(&assertions);
  }

  if (options::solveRealAsInt())
  {
    d_passes["real-to-int"]->apply(&assertions);
  }

  if (options::solveIntAsBV() > 0)
  {
    d_passes["int-to-bv"]->apply(&assertions);
  }

  if (options::ackermann())
  {
    d_passes["ackermann"]->apply(&assertions);
  }

  if (options::bvAbstraction())
  {
    d_passes["bv-abstraction"]->apply(&assertions);
  }

  Debug("smt") << " assertions     : " << assertions.size() << endl;

  bool noConflict = true;

  if (options::extRewPrep())
  {
    d_passes["ext-rew-pre"]->apply(&assertions);
  }

  // Unconstrained simplification
  if (options::unconstrainedSimp())
  {
    d_passes["rewrite"]->apply(&assertions);
    d_passes["unconstrained-simplifier"]->apply(&assertions);
  }

  if (options::bvIntroducePow2())
  {
    d_passes["bv-intro-pow2"]->apply(&assertions);
  }

  // Lift bit-vectors of size 1 to bool
  if (options::bitvectorToBool())
  {
    d_passes["bv-to-bool"]->apply(&assertions);
  }
  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
  {
    d_passes["bv-to-int"]->apply(&assertions);
  }
  if (options::foreignTheoryRewrite())
  {
    d_passes["foreign-theory-rewrite"]->apply(&assertions);
  }

  // Since this pass is not robust for the information tracking necessary for
  // unsat cores, it's only applied if we are not doing unsat core computation
  d_passes["apply-substs"]->apply(&assertions);

  // Assertions MUST BE guaranteed to be rewritten by this point
  d_passes["rewrite"]->apply(&assertions);

  // Convert non-top-level Booleans to bit-vectors of size 1
  if (options::boolToBitvector() != options::BoolToBVMode::OFF)
  {
    d_passes["bool-to-bv"]->apply(&assertions);
  }
  if (options::sepPreSkolemEmp())
  {
    d_passes["sep-skolem-emp"]->apply(&assertions);
  }

  if (d_smt.getLogicInfo().isQuantified())
  {
    // remove rewrite rules, apply pre-skolemization to existential quantifiers
    d_passes["quantifiers-preprocess"]->apply(&assertions);

    // fmf-fun : assume admissible functions, applying preprocessing reduction
    // to FMF
    if (options::fmfFunWellDefined())
    {
      d_passes["fun-def-fmf"]->apply(&assertions);
    }
  }
  if (!options::stringLazyPreproc())
  {
    d_passes["strings-eager-pp"]->apply(&assertions);
  }
  if (options::sortInference() || options::ufssFairnessMonotone())
  {
    d_passes["sort-inference"]->apply(&assertions);
  }

  if (options::pbRewrites())
  {
    d_passes["pseudo-boolean-processor"]->apply(&assertions);
  }

  // rephrasing normal inputs as sygus problems
  if (!d_smt.isInternalSubsolver())
  {
    if (options::sygusInference())
    {
      d_passes["sygus-infer"]->apply(&assertions);
    }
    else if (options::sygusRewSynthInput())
    {
      // do candidate rewrite rule synthesis
      d_passes["synth-rr"]->apply(&assertions);
    }
  }

  Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
                    << endl;
  dumpAssertions("pre-simplify", assertions);
  Chat() << "simplifying assertions..." << endl;
  noConflict = simplifyAssertions(assertions);
  if (!noConflict)
  {
    ++(d_smtStats.d_simplifiedToFalse);
  }
  Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
                    << endl;
  dumpAssertions("post-simplify", assertions);

  if (options::doStaticLearning())
  {
    d_passes["static-learning"]->apply(&assertions);
  }
  Debug("smt") << " assertions     : " << assertions.size() << endl;

  if (options::learnedRewrite())
  {
    d_passes["learned-rewrite"]->apply(&assertions);
  }

  if (options::earlyIteRemoval())
  {
    d_smtStats.d_numAssertionsPre += assertions.size();
    d_passes["ite-removal"]->apply(&assertions);
    // This is needed because when solving incrementally, removeITEs may
    // introduce skolems that were solved for earlier and thus appear in the
    // substitution map.
    d_passes["apply-substs"]->apply(&assertions);
    d_smtStats.d_numAssertionsPost += assertions.size();
  }

  dumpAssertions("pre-repeat-simplify", assertions);
  if (options::repeatSimp())
  {
    Trace("smt-proc")
        << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
        << endl;
    Chat() << "re-simplifying assertions..." << endl;
    ScopeCounter depth(d_simplifyAssertionsDepth);
    noConflict &= simplifyAssertions(assertions);
    Trace("smt-proc")
        << "ProcessAssertions::processAssertions() : post-repeat-simplify"
        << endl;
  }
  dumpAssertions("post-repeat-simplify", assertions);

  if (options::ufHo())
  {
    d_passes["ho-elim"]->apply(&assertions);
  }

  // begin: INVARIANT to maintain: no reordering of assertions or
  // introducing new ones

  Debug("smt") << " assertions     : " << assertions.size() << endl;

  Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
               << endl;
  Debug("smt") << " assertions     : " << assertions.size() << endl;

  // ensure rewritten
  d_passes["rewrite"]->apply(&assertions);
  // rewrite equalities based on theory-specific rewriting
  d_passes["theory-rewrite-eq"]->apply(&assertions);
  // apply theory preprocess, which includes ITE removal
  d_passes["theory-preprocess"]->apply(&assertions);
  // notice that we do not apply substitutions as a last step here, since
  // the range of substitutions is not theory-preprocessed.

  if (options::bitblastMode() == options::BitblastMode::EAGER)
  {
    d_passes["bv-eager-atoms"]->apply(&assertions);
  }

  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
  dumpAssertions("post-everything", assertions);

  return noConflict;
}

// returns false if simplification led to "false"
bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
{
  spendResource(Resource::PreprocessStep);
  try
  {
    ScopeCounter depth(d_simplifyAssertionsDepth);

    Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;

    if (options::simplificationMode() != options::SimplificationMode::NONE)
    {
      // Perform non-clausal simplification
      PreprocessingPassResult res =
          d_passes["non-clausal-simp"]->apply(&assertions);
      if (res == PreprocessingPassResult::CONFLICT)
      {
        return false;
      }

      // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
      // do the miplib trick.
      if (  // check that option is on
          options::arithMLTrick() &&
          // only useful in arith
          d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
          // we add new assertions and need this (in practice, this
          // restriction only disables miplib processing during
          // re-simplification, which we don't expect to be useful anyway)
          assertions.getRealAssertionsEnd() == assertions.size())
      {
        d_passes["miplib-trick"]->apply(&assertions);
      }
      else
      {
        Trace("simplify") << "SmtEnginePrivate::simplify(): "
                          << "skipping miplib pseudobooleans pass..." << endl;
      }
    }

    Debug("smt") << " assertions     : " << assertions.size() << endl;

    // ITE simplification
    if (options::doITESimp()
        && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
    {
      PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
      if (res == PreprocessingPassResult::CONFLICT)
      {
        Chat() << "...ITE simplification found unsat..." << endl;
        return false;
      }
    }

    Debug("smt") << " assertions     : " << assertions.size() << endl;

    // Unconstrained simplification
    if (options::unconstrainedSimp())
    {
      d_passes["unconstrained-simplifier"]->apply(&assertions);
    }

    if (options::repeatSimp()
        && options::simplificationMode() != options::SimplificationMode::NONE)
    {
      PreprocessingPassResult res =
          d_passes["non-clausal-simp"]->apply(&assertions);
      if (res == PreprocessingPassResult::CONFLICT)
      {
        return false;
      }
    }

    dumpAssertions("post-repeatsimp", assertions);
    Trace("smt") << "POST repeatSimp" << endl;
    Debug("smt") << " assertions     : " << assertions.size() << endl;
  }
  catch (TypeCheckingExceptionPrivate& tcep)
  {
    // Calls to this function should have already weeded out any
    // typechecking exceptions via (e.g.) ensureBoolean().  But a
    // theory could still create a new expression that isn't
    // well-typed, and we don't want the C++ runtime to abort our
    // process without any error notice.
    InternalError()
        << "A bad expression was produced.  Original exception follows:\n"
        << tcep;
  }
  return true;
}

void ProcessAssertions::dumpAssertions(const char* key,
                                       const AssertionPipeline& assertionList)
{
  if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
  {
    // Push the simplified assertions to the dump output stream
    for (unsigned i = 0; i < assertionList.size(); ++i)
    {
      TNode n = assertionList[i];
      d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
          d_smt.getOutputManager().getDumpOut(), n);
    }
  }
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Morgan Deters, Aina Niemetz
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 module for processing assertions for an SMT engine.
14		*/
15
16		#include "smt/process_assertions.h"
17
18		#include <utility>
19
20		#include "expr/node_manager_attributes.h"
21		#include "options/arith_options.h"
22		#include "options/base_options.h"
23		#include "options/bv_options.h"
24		#include "options/quantifiers_options.h"
25		#include "options/sep_options.h"
26		#include "options/smt_options.h"
27		#include "options/strings_options.h"
28		#include "options/uf_options.h"
29		#include "preprocessing/assertion_pipeline.h"
30		#include "preprocessing/preprocessing_pass.h"
31		#include "preprocessing/preprocessing_pass_registry.h"
32		#include "printer/printer.h"
33		#include "smt/assertions.h"
34		#include "smt/dump.h"
35		#include "smt/expand_definitions.h"
36		#include "smt/smt_engine.h"
37		#include "smt/smt_engine_stats.h"
38		#include "theory/logic_info.h"
39		#include "theory/theory_engine.h"
40
41		using namespace std;
42		using namespace cvc5::preprocessing;
43		using namespace cvc5::theory;
44		using namespace cvc5::kind;
45
46		namespace cvc5 {
47		namespace smt {
48
49		/** Useful for counting the number of recursive calls. */
50		class ScopeCounter
51		{
52		public:
53	14241	ScopeCounter(unsigned& d) : d_depth(d) { ++d_depth; }
54	14241	~ScopeCounter() { --d_depth; }
55
56		private:
57		unsigned& d_depth;
58		};
59
60	10497	ProcessAssertions::ProcessAssertions(SmtEngine& smt,
61		ResourceManager& rm,
62	10497	SmtEngineStatistics& stats)
63		: d_smt(smt),
64		d_resourceManager(rm),
65		d_smtStats(stats),
66	10497	d_preprocessingPassContext(nullptr)
67		{
68	10497	d_true = NodeManager::currentNM()->mkConst(true);
69	10497	}
70
71	10497	ProcessAssertions::~ProcessAssertions()
72		{
73	10497	}
74
75	9853	void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
76		{
77	9853	Assert(d_preprocessingPassContext == nullptr);
78	9853	d_preprocessingPassContext = pc;
79
80	9853	PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
81		// TODO: this will likely change when we add support for actually assembling
82		// preprocessing pipelines. For now, we just create an instance of each
83		// available preprocessing pass.
84	19706	std::vector<std::string> passNames = ppReg.getAvailablePasses();
85	344855	for (const std::string& passName : passNames)
86		{
87	335002	d_passes[passName].reset(
88		ppReg.createPass(d_preprocessingPassContext, passName));
89		}
90	9853	}
91
92	10497	void ProcessAssertions::cleanup() { d_passes.clear(); }
93
94	13994	void ProcessAssertions::spendResource(Resource r)
95		{
96	13994	d_resourceManager.spendResource(r);
97	13994	}
98
99	13750	bool ProcessAssertions::apply(Assertions& as)
100		{
101	13750	AssertionPipeline& assertions = as.getAssertionPipeline();
102	13750	Assert(d_preprocessingPassContext != nullptr);
103		// Dump the assertions
104	13750	dumpAssertions("pre-everything", assertions);
105
106	13750	Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl;
107	13750	Trace("smt") << "ProcessAssertions::processAssertions()" << endl;
108
109	13750	Debug("smt") << "#Assertions : " << assertions.size() << endl;
110	13750	Debug("smt") << "#Assumptions: " << assertions.getNumAssumptions() << endl;
111
112	13750	if (assertions.size() == 0)
113		{
114		// nothing to do
115		return true;
116		}
117
118	13750	if (options::bvGaussElim())
119		{
120		d_passes["bv-gauss"]->apply(&assertions);
121		}
122
123		// Add dummy assertion in last position - to be used as a
124		// placeholder for any new assertions to get added
125	13750	assertions.push_back(d_true);
126		// any assertions added beyond realAssertionsEnd must NOT affect the
127		// equisatisfiability
128	13750	assertions.updateRealAssertionsEnd();
129
130		// Assertions are NOT guaranteed to be rewritten by this point
131
132	27500	Trace("smt-proc")
133	13750	<< "ProcessAssertions::processAssertions() : pre-definition-expansion"
134	13750	<< endl;
135	13750	dumpAssertions("pre-definition-expansion", assertions);
136		// Apply substitutions first. If we are non-incremental, this has only the
137		// effect of replacing defined functions with their definitions.
138		// We do not call theory-specific expand definitions here, since we want
139		// to give the opportunity to rewrite/preprocess terms before expansion.
140	13752	d_passes["apply-substs"]->apply(&assertions);
141	27496	Trace("smt-proc")
142	13748	<< "ProcessAssertions::processAssertions() : post-definition-expansion"
143	13748	<< endl;
144	13748	dumpAssertions("post-definition-expansion", assertions);
145
146	13748	Debug("smt") << " assertions : " << assertions.size() << endl;
147
148	13748	if (options::globalNegate())
149		{
150		// global negation of the formula
151	6	d_passes["global-negate"]->apply(&assertions);
152	6	as.flipGlobalNegated();
153		}
154
155	13748	if (options::nlExtPurify())
156		{
157	6	d_passes["nl-ext-purify"]->apply(&assertions);
158		}
159
160	13748	if (options::solveRealAsInt())
161		{
162	13	d_passes["real-to-int"]->apply(&assertions);
163		}
164
165	13748	if (options::solveIntAsBV() > 0)
166		{
167	16	d_passes["int-to-bv"]->apply(&assertions);
168		}
169
170	13747	if (options::ackermann())
171		{
172	66	d_passes["ackermann"]->apply(&assertions);
173		}
174
175	13747	if (options::bvAbstraction())
176		{
177	4	d_passes["bv-abstraction"]->apply(&assertions);
178		}
179
180	13747	Debug("smt") << " assertions : " << assertions.size() << endl;
181
182	13747	bool noConflict = true;
183
184	13747	if (options::extRewPrep())
185		{
186	24	d_passes["ext-rew-pre"]->apply(&assertions);
187		}
188
189		// Unconstrained simplification
190	13747	if (options::unconstrainedSimp())
191		{
192	180	d_passes["rewrite"]->apply(&assertions);
193	180	d_passes["unconstrained-simplifier"]->apply(&assertions);
194		}
195
196	13747	if (options::bvIntroducePow2())
197		{
198	2	d_passes["bv-intro-pow2"]->apply(&assertions);
199		}
200
201		// Lift bit-vectors of size 1 to bool
202	13747	if (options::bitvectorToBool())
203		{
204	147	d_passes["bv-to-bool"]->apply(&assertions);
205		}
206	13747	if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
207		{
208	205	d_passes["bv-to-int"]->apply(&assertions);
209		}
210	13747	if (options::foreignTheoryRewrite())
211		{
212	2	d_passes["foreign-theory-rewrite"]->apply(&assertions);
213		}
214
215		// Since this pass is not robust for the information tracking necessary for
216		// unsat cores, it's only applied if we are not doing unsat core computation
217	13747	d_passes["apply-substs"]->apply(&assertions);
218
219		// Assertions MUST BE guaranteed to be rewritten by this point
220	13747	d_passes["rewrite"]->apply(&assertions);
221
222		// Convert non-top-level Booleans to bit-vectors of size 1
223	13747	if (options::boolToBitvector() != options::BoolToBVMode::OFF)
224		{
225	12	d_passes["bool-to-bv"]->apply(&assertions);
226		}
227	13747	if (options::sepPreSkolemEmp())
228		{
229	1	d_passes["sep-skolem-emp"]->apply(&assertions);
230		}
231
232	13747	if (d_smt.getLogicInfo().isQuantified())
233		{
234		// remove rewrite rules, apply pre-skolemization to existential quantifiers
235	8130	d_passes["quantifiers-preprocess"]->apply(&assertions);
236
237		// fmf-fun : assume admissible functions, applying preprocessing reduction
238		// to FMF
239	8130	if (options::fmfFunWellDefined())
240		{
241	121	d_passes["fun-def-fmf"]->apply(&assertions);
242		}
243		}
244	13747	if (!options::stringLazyPreproc())
245		{
246	40	d_passes["strings-eager-pp"]->apply(&assertions);
247		}
248	13747	if (options::sortInference() \|\| options::ufssFairnessMonotone())
249		{
250	24	d_passes["sort-inference"]->apply(&assertions);
251		}
252
253	13747	if (options::pbRewrites())
254		{
255	2	d_passes["pseudo-boolean-processor"]->apply(&assertions);
256		}
257
258		// rephrasing normal inputs as sygus problems
259	13747	if (!d_smt.isInternalSubsolver())
260		{
261	10212	if (options::sygusInference())
262		{
263	58	d_passes["sygus-infer"]->apply(&assertions);
264		}
265	10154	else if (options::sygusRewSynthInput())
266		{
267		// do candidate rewrite rule synthesis
268		d_passes["synth-rr"]->apply(&assertions);
269		}
270		}
271
272	27494	Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify"
273	13747	<< endl;
274	13747	dumpAssertions("pre-simplify", assertions);
275	13747	Chat() << "simplifying assertions..." << endl;
276	13747	noConflict = simplifyAssertions(assertions);
277	13747	if (!noConflict)
278		{
279	1074	++(d_smtStats.d_simplifiedToFalse);
280		}
281	27494	Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
282	13747	<< endl;
283	13747	dumpAssertions("post-simplify", assertions);
284
285	13747	if (options::doStaticLearning())
286		{
287	13747	d_passes["static-learning"]->apply(&assertions);
288		}
289	13747	Debug("smt") << " assertions : " << assertions.size() << endl;
290
291	13747	if (options::learnedRewrite())
292		{
293	2	d_passes["learned-rewrite"]->apply(&assertions);
294		}
295
296	13747	if (options::earlyIteRemoval())
297		{
298	2	d_smtStats.d_numAssertionsPre += assertions.size();
299	2	d_passes["ite-removal"]->apply(&assertions);
300		// This is needed because when solving incrementally, removeITEs may
301		// introduce skolems that were solved for earlier and thus appear in the
302		// substitution map.
303	2	d_passes["apply-substs"]->apply(&assertions);
304	2	d_smtStats.d_numAssertionsPost += assertions.size();
305		}
306
307	13747	dumpAssertions("pre-repeat-simplify", assertions);
308	13747	if (options::repeatSimp())
309		{
310	494	Trace("smt-proc")
311	247	<< "ProcessAssertions::processAssertions() : pre-repeat-simplify"
312	247	<< endl;
313	247	Chat() << "re-simplifying assertions..." << endl;
314	494	ScopeCounter depth(d_simplifyAssertionsDepth);
315	247	noConflict &= simplifyAssertions(assertions);
316	494	Trace("smt-proc")
317	247	<< "ProcessAssertions::processAssertions() : post-repeat-simplify"
318	247	<< endl;
319		}
320	13747	dumpAssertions("post-repeat-simplify", assertions);
321
322	13747	if (options::ufHo())
323		{
324	183	d_passes["ho-elim"]->apply(&assertions);
325		}
326
327		// begin: INVARIANT to maintain: no reordering of assertions or
328		// introducing new ones
329
330	13747	Debug("smt") << " assertions : " << assertions.size() << endl;
331
332	27494	Debug("smt") << "ProcessAssertions::processAssertions() POST SIMPLIFICATION"
333	13747	<< endl;
334	13747	Debug("smt") << " assertions : " << assertions.size() << endl;
335
336		// ensure rewritten
337	13747	d_passes["rewrite"]->apply(&assertions);
338		// rewrite equalities based on theory-specific rewriting
339	13747	d_passes["theory-rewrite-eq"]->apply(&assertions);
340		// apply theory preprocess, which includes ITE removal
341	13754	d_passes["theory-preprocess"]->apply(&assertions);
342		// notice that we do not apply substitutions as a last step here, since
343		// the range of substitutions is not theory-preprocessed.
344
345	13740	if (options::bitblastMode() == options::BitblastMode::EAGER)
346		{
347	58	d_passes["bv-eager-atoms"]->apply(&assertions);
348		}
349
350	13740	Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
351	13740	dumpAssertions("post-everything", assertions);
352
353	13740	return noConflict;
354		}
355
356		// returns false if simplification led to "false"
357	13994	bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
358		{
359	13994	spendResource(Resource::PreprocessStep);
360		try
361		{
362	26905	ScopeCounter depth(d_simplifyAssertionsDepth);
363
364	13994	Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
365
366	13994	if (options::simplificationMode() != options::SimplificationMode::NONE)
367		{
368		// Perform non-clausal simplification
369		PreprocessingPassResult res =
370	10555	d_passes["non-clausal-simp"]->apply(&assertions);
371	10555	if (res == PreprocessingPassResult::CONFLICT)
372		{
373	1079	return false;
374		}
375
376		// We piggy-back off of the BackEdgesMap in the CircuitPropagator to
377		// do the miplib trick.
378	9476	if ( // check that option is on
379	9484	options::arithMLTrick() &&
380		// only useful in arith
381	9484	d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) &&
382		// we add new assertions and need this (in practice, this
383		// restriction only disables miplib processing during
384		// re-simplification, which we don't expect to be useful anyway)
385	8	assertions.getRealAssertionsEnd() == assertions.size())
386		{
387	8	d_passes["miplib-trick"]->apply(&assertions);
388		}
389		else
390		{
391	18936	Trace("simplify") << "SmtEnginePrivate::simplify(): "
392	9468	<< "skipping miplib pseudobooleans pass..." << endl;
393		}
394		}
395
396	12915	Debug("smt") << " assertions : " << assertions.size() << endl;
397
398		// ITE simplification
399	25830	if (options::doITESimp()
400	12915	&& (d_simplifyAssertionsDepth <= 1 \|\| options::doITESimpOnRepeat()))
401		{
402	2	PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
403	2	if (res == PreprocessingPassResult::CONFLICT)
404		{
405		Chat() << "...ITE simplification found unsat..." << endl;
406		return false;
407		}
408		}
409
410	12915	Debug("smt") << " assertions : " << assertions.size() << endl;
411
412		// Unconstrained simplification
413	12915	if (options::unconstrainedSimp())
414		{
415	329	d_passes["unconstrained-simplifier"]->apply(&assertions);
416		}
417
418	25830	if (options::repeatSimp()
419	12915	&& options::simplificationMode() != options::SimplificationMode::NONE)
420		{
421		PreprocessingPassResult res =
422	466	d_passes["non-clausal-simp"]->apply(&assertions);
423	466	if (res == PreprocessingPassResult::CONFLICT)
424		{
425	4	return false;
426		}
427		}
428
429	12911	dumpAssertions("post-repeatsimp", assertions);
430	12911	Trace("smt") << "POST repeatSimp" << endl;
431	12911	Debug("smt") << " assertions : " << assertions.size() << endl;
432		}
433		catch (TypeCheckingExceptionPrivate& tcep)
434		{
435		// Calls to this function should have already weeded out any
436		// typechecking exceptions via (e.g.) ensureBoolean(). But a
437		// theory could still create a new expression that isn't
438		// well-typed, and we don't want the C++ runtime to abort our
439		// process without any error notice.
440		InternalError()
441		<< "A bad expression was produced. Original exception follows:\n"
442		<< tcep;
443		}
444	12911	return true;
445		}
446
447	122887	void ProcessAssertions::dumpAssertions(const char* key,
448		const AssertionPipeline& assertionList)
449		{
450	122887	if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key))
451		{
452		// Push the simplified assertions to the dump output stream
453		for (unsigned i = 0; i < assertionList.size(); ++i)
454		{
455		TNode n = assertionList[i];
456		d_smt.getOutputManager().getPrinter().toStreamCmdAssert(
457		d_smt.getOutputManager().getDumpOut(), n);
458		}
459		}
460	122887	}
461
462		} // namespace smt
463	29340	} // namespace cvc5