Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/ackermann.cpp	Lines:	110	113	97.3 %
Date:	2021-09-30	Branches:	216	518	41.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Ying Sheng, Yoni Zohar, 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.
 * ****************************************************************************
 *
 * Ackermannization preprocessing pass.
 *
 * This implements the Ackermannization preprocessing pass, which enables
 * very limited theory combination support for eager bit-blasting via
 * Ackermannization. It reduces constraints over the combination of the
 * theories of fixed-size bit-vectors and uninterpreted functions as
 * described in
 *   Liana Hadarean, An Efficient and Trustworthy Theory Solver for
 *   Bit-vectors in Satisfiability Modulo Theories.
 *   https://cs.nyu.edu/media/publications/hadarean_liana.pdf
 */

#include "preprocessing/passes/ackermann.h"

#include <cmath>

#include "base/check.h"
#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"

using namespace cvc5;
using namespace cvc5::theory;

namespace cvc5 {
namespace preprocessing {
namespace passes {

/* -------------------------------------------------------------------------- */

namespace {

void addLemmaForPair(TNode args1,
                     TNode args2,
                     const TNode func,
                     AssertionPipeline* assertionsToPreprocess,
                     NodeManager* nm)
{
  Node args_eq;

  if (args1.getKind() == kind::APPLY_UF)
  {
    Assert(args1.getOperator() == func);
    Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func);
    Assert(args1.getNumChildren() == args2.getNumChildren());
    Assert(args1.getNumChildren() >= 1);

    std::vector<Node> eqs(args1.getNumChildren());

    for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
    {
      eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
    }
    if (eqs.size() >= 2)
    {
      args_eq = nm->mkNode(kind::AND, eqs);
    }
    else
    {
      args_eq = eqs[0];
    }
  }
  else
  {
    Assert(args1.getKind() == kind::SELECT && args1.getOperator() == func);
    Assert(args2.getKind() == kind::SELECT && args2.getOperator() == func);
    Assert(args1.getNumChildren() == 2);
    Assert(args2.getNumChildren() == 2);
    args_eq = nm->mkNode(Kind::AND,
      nm->mkNode(kind::EQUAL, args1[0], args2[0]),
      nm->mkNode(kind::EQUAL, args1[1], args2[1])
    );
  }
  Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
  Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
  assertionsToPreprocess->push_back(lemma);
}

void storeFunctionAndAddLemmas(TNode func,
                               TNode term,
                               FunctionToArgsMap& fun_to_args,
                               SubstitutionMap& fun_to_skolem,
                               AssertionPipeline* assertions,
                               NodeManager* nm,
                               std::vector<TNode>* vec)
{
  if (fun_to_args.find(func) == fun_to_args.end())
  {
    fun_to_args.insert(make_pair(func, TNodeSet()));
  }
  TNodeSet& set = fun_to_args[func];
  if (set.find(term) == set.end())
  {
    TypeNode tn = term.getType();
    SkolemManager* sm = nm->getSkolemManager();
    Node skolem =
        sm->mkDummySkolem("SKOLEM$$",
                          tn,
                          "is a variable created by the ackermannization "
                          "preprocessing pass");
    for (const auto& t : set)
    {
      addLemmaForPair(t, term, func, assertions, nm);
    }
    fun_to_skolem.addSubstitution(term, skolem);
    set.insert(term);
    /* Add the arguments of term (newest element in set) to the vector, so that
     * collectFunctionsAndLemmas will process them as well.
     * This is only needed if the set has at least two elements
     * (otherwise, no lemma is generated).
     * Therefore, we defer this for term in case it is the first element in the
     * set*/
    if (set.size() == 2)
    {
      for (TNode elem : set)
      {
        vec->insert(vec->end(), elem.begin(), elem.end());
      }
    }
    else if (set.size() > 2)
    {
      vec->insert(vec->end(), term.begin(), term.end());
    }
  }
}

/* We only add top-level applications of functions.
 * For example: when we see "f(g(x))", we do not add g as a function and x as a
 * parameter.
 * Instead, we only include f as a function and g(x) as a parameter.
 * However, if we see g(x) later on as a top-level application, we will add it
 * as well.
 * Another example: for the formula f(g(x))=f(g(y)),
 * we first only add f as a function and g(x),g(y) as arguments.
 * storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) ->
 * f(g(x))=f(g(y)).
 * Now that we see g(x) and g(y), we explicitly add them as well. */
void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
                               SubstitutionMap& fun_to_skolem,
                               std::vector<TNode>* vec,
                               AssertionPipeline* assertions)
{
  TNodeSet seen;
  NodeManager* nm = NodeManager::currentNM();
  TNode term;
  while (!vec->empty())
  {
    term = vec->back();
    vec->pop_back();
    if (seen.find(term) == seen.end())
    {
      TNode func;
      if (term.getKind() == kind::APPLY_UF || term.getKind() == kind::SELECT)
      {
        storeFunctionAndAddLemmas(term.getOperator(),
                                  term,
                                  fun_to_args,
                                  fun_to_skolem,
                                  assertions,
                                  nm,
                                  vec);
      }
      else
      {
        AlwaysAssert(term.getKind() != kind::STORE)
            << "Cannot use Ackermannization on formula with stores to arrays";
        /* add children to the vector, so that they are processed later */
        for (TNode n : term)
        {
          vec->push_back(n);
        }
      }
      seen.insert(term);
    }
  }
}

}  // namespace

/* -------------------------------------------------------------------------- */

/* Given a minimum capacity for an uninterpreted sort, return the size of the
 * new BV type */
size_t getBVSkolemSize(size_t capacity)
{
  return static_cast<size_t>(log2(capacity)) + 1;
}

/* Given the lowest capacity requirements for each uninterpreted sort, assign
 * a sufficient bit-vector size.
 * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
 * the fresh skolem BV variables. variables */
void collectUSortsToBV(const std::unordered_set<TNode>& vars,
                       const USortToBVSizeMap& usortCardinality,
                       SubstitutionMap& usVarsToBVVars)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();

  for (TNode var : vars)
  {
    TypeNode type = var.getType();
    size_t size = getBVSkolemSize(usortCardinality.at(type));
    Node skolem = sm->mkDummySkolem(
        "BVSKOLEM$$",
        nm->mkBitVectorType(size),
        "a variable created by the ackermannization "
        "preprocessing pass, representing a variable with uninterpreted sort "
            + type.toString() + ".");
    usVarsToBVVars.addSubstitution(var, skolem);
  }
}

/* This function returns the list of terms with uninterpreted sort in the
 * formula represented by assertions. */
std::unordered_set<TNode> getVarsWithUSorts(AssertionPipeline* assertions)
{
  std::unordered_set<TNode> res;

  for (const Node& assertion : assertions->ref())
  {
    std::unordered_set<TNode> vars;
    expr::getVariables(assertion, vars);

    for (const TNode& var : vars)
    {
      if (var.getType().isSort())
      {
        res.insert(var);
      }
    }
  }

  return res;
}

/* This is the top level of converting uninterpreted sorts to bit-vectors.
 * We count the number of different variables for each uninterpreted sort.
 * Then for each sort, we will assign a new bit-vector type with a sufficient
 * size. The size is calculated to have enough capacity, that can accommodate
 * the variables occured in the original formula. At the end, all variables of
 * uninterpreted sorts will be converted into Skolem variables of BV */
void usortsToBitVectors(const LogicInfo& d_logic,
                        AssertionPipeline* assertions,
                        USortToBVSizeMap& usortCardinality,
                        SubstitutionMap& usVarsToBVVars)
{
  std::unordered_set<TNode> toProcess = getVarsWithUSorts(assertions);

  if (toProcess.size() > 0)
  {
    /* the current version only supports BV for removing uninterpreted sorts */
    if (not d_logic.isTheoryEnabled(theory::THEORY_BV))
    {
      return;
    }

    for (TNode term : toProcess)
    {
      TypeNode type = term.getType();
      /* Update the counts for each uninterpreted sort.
       * For non-existing keys, C++ will create a new element for it, which has
       * a default 0 value, before incrementing by 1. */
      usortCardinality[type] = usortCardinality[type] + 1;
    }

    collectUSortsToBV(toProcess, usortCardinality, usVarsToBVVars);

    for (size_t i = 0, size = assertions->size(); i < size; ++i)
    {
      Node old = (*assertions)[i];
      Node newA = usVarsToBVVars.apply((*assertions)[i]);
      if (newA != old)
      {
        assertions->replace(i, newA);
        Trace("uninterpretedSorts-to-bv")
            << "  " << old << " => " << (*assertions)[i] << "\n";
      }
    }
  }
}

/* -------------------------------------------------------------------------- */

Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
    : PreprocessingPass(preprocContext, "ackermann"),
      d_funcToSkolem(userContext()),
      d_usVarsToBVVars(userContext()),
      d_logic(logicInfo())
{
}

PreprocessingPassResult Ackermann::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  AlwaysAssert(!options().base.incrementalSolving);

  /* collect all function applications and generate consistency lemmas
   * accordingly */
  std::vector<TNode> to_process;
  for (const Node& a : assertionsToPreprocess->ref())
  {
    to_process.push_back(a);
  }
  collectFunctionsAndLemmas(
      d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess);

  /* replace applications of UF by skolems */
  // FIXME for model building, github issue #1901
  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  {
    assertionsToPreprocess->replace(
        i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
  }

  /* replace uninterpreted sorts with bit-vectors */
  usortsToBitVectors(
      d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars);

  return PreprocessingPassResult::NO_CONFLICT;
}

/* -------------------------------------------------------------------------- */

}  // namespace passes
}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Ying Sheng, Yoni Zohar, 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		* Ackermannization preprocessing pass.
14		*
15		* This implements the Ackermannization preprocessing pass, which enables
16		* very limited theory combination support for eager bit-blasting via
17		* Ackermannization. It reduces constraints over the combination of the
18		* theories of fixed-size bit-vectors and uninterpreted functions as
19		* described in
20		* Liana Hadarean, An Efficient and Trustworthy Theory Solver for
21		* Bit-vectors in Satisfiability Modulo Theories.
22		* https://cs.nyu.edu/media/publications/hadarean_liana.pdf
23		*/
24
25		#include "preprocessing/passes/ackermann.h"
26
27		#include <cmath>
28
29		#include "base/check.h"
30		#include "expr/node_algorithm.h"
31		#include "expr/skolem_manager.h"
32		#include "options/base_options.h"
33		#include "options/options.h"
34		#include "preprocessing/assertion_pipeline.h"
35		#include "preprocessing/preprocessing_pass_context.h"
36
37		using namespace cvc5;
38		using namespace cvc5::theory;
39
40		namespace cvc5 {
41		namespace preprocessing {
42		namespace passes {
43
44		/* -------------------------------------------------------------------------- */
45
46		namespace {
47
48	185	void addLemmaForPair(TNode args1,
49		TNode args2,
50		const TNode func,
51		AssertionPipeline* assertionsToPreprocess,
52		NodeManager* nm)
53		{
54	370	Node args_eq;
55
56	185	if (args1.getKind() == kind::APPLY_UF)
57		{
58	155	Assert(args1.getOperator() == func);
59	155	Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func);
60	155	Assert(args1.getNumChildren() == args2.getNumChildren());
61	155	Assert(args1.getNumChildren() >= 1);
62
63	310	std::vector<Node> eqs(args1.getNumChildren());
64
65	310	for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
66		{
67	155	eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
68		}
69	155	if (eqs.size() >= 2)
70		{
71		args_eq = nm->mkNode(kind::AND, eqs);
72		}
73		else
74		{
75	155	args_eq = eqs[0];
76		}
77		}
78		else
79		{
80	30	Assert(args1.getKind() == kind::SELECT && args1.getOperator() == func);
81	30	Assert(args2.getKind() == kind::SELECT && args2.getOperator() == func);
82	30	Assert(args1.getNumChildren() == 2);
83	30	Assert(args2.getNumChildren() == 2);
84	90	args_eq = nm->mkNode(Kind::AND,
85	60	nm->mkNode(kind::EQUAL, args1[0], args2[0]),
86	60	nm->mkNode(kind::EQUAL, args1[1], args2[1])
87		);
88		}
89	370	Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
90	370	Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
91	185	assertionsToPreprocess->push_back(lemma);
92	185	}
93
94	118	void storeFunctionAndAddLemmas(TNode func,
95		TNode term,
96		FunctionToArgsMap& fun_to_args,
97		SubstitutionMap& fun_to_skolem,
98		AssertionPipeline* assertions,
99		NodeManager* nm,
100		std::vector<TNode>* vec)
101		{
102	118	if (fun_to_args.find(func) == fun_to_args.end())
103		{
104	38	fun_to_args.insert(make_pair(func, TNodeSet()));
105		}
106	118	TNodeSet& set = fun_to_args[func];
107	118	if (set.find(term) == set.end())
108		{
109	236	TypeNode tn = term.getType();
110	118	SkolemManager* sm = nm->getSkolemManager();
111		Node skolem =
112		sm->mkDummySkolem("SKOLEM$$",
113		tn,
114		"is a variable created by the ackermannization "
115	236	"preprocessing pass");
116	303	for (const auto& t : set)
117		{
118	185	addLemmaForPair(t, term, func, assertions, nm);
119		}
120	118	fun_to_skolem.addSubstitution(term, skolem);
121	118	set.insert(term);
122		/* Add the arguments of term (newest element in set) to the vector, so that
123		* collectFunctionsAndLemmas will process them as well.
124		* This is only needed if the set has at least two elements
125		* (otherwise, no lemma is generated).
126		* Therefore, we defer this for term in case it is the first element in the
127		* set*/
128	118	if (set.size() == 2)
129		{
130	93	for (TNode elem : set)
131		{
132	62	vec->insert(vec->end(), elem.begin(), elem.end());
133		}
134		}
135	87	else if (set.size() > 2)
136		{
137	49	vec->insert(vec->end(), term.begin(), term.end());
138		}
139		}
140	118	}
141
142		/* We only add top-level applications of functions.
143		* For example: when we see "f(g(x))", we do not add g as a function and x as a
144		* parameter.
145		* Instead, we only include f as a function and g(x) as a parameter.
146		* However, if we see g(x) later on as a top-level application, we will add it
147		* as well.
148		* Another example: for the formula f(g(x))=f(g(y)),
149		* we first only add f as a function and g(x),g(y) as arguments.
150		* storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) ->
151		* f(g(x))=f(g(y)).
152		* Now that we see g(x) and g(y), we explicitly add them as well. */
153	32	void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
154		SubstitutionMap& fun_to_skolem,
155		std::vector<TNode>* vec,
156		AssertionPipeline* assertions)
157		{
158	64	TNodeSet seen;
159	32	NodeManager* nm = NodeManager::currentNM();
160	64	TNode term;
161	2312	while (!vec->empty())
162		{
163	1140	term = vec->back();
164	1140	vec->pop_back();
165	1140	if (seen.find(term) == seen.end())
166		{
167	1462	TNode func;
168	731	if (term.getKind() == kind::APPLY_UF \|\| term.getKind() == kind::SELECT)
169		{
170	118	storeFunctionAndAddLemmas(term.getOperator(),
171		term,
172		fun_to_args,
173		fun_to_skolem,
174		assertions,
175		nm,
176		vec);
177		}
178		else
179		{
180	613	AlwaysAssert(term.getKind() != kind::STORE)
181		<< "Cannot use Ackermannization on formula with stores to arrays";
182		/* add children to the vector, so that they are processed later */
183	1511	for (TNode n : term)
184		{
185	898	vec->push_back(n);
186		}
187		}
188	731	seen.insert(term);
189		}
190		}
191	32	}
192
193		} // namespace
194
195		/* -------------------------------------------------------------------------- */
196
197		/* Given a minimum capacity for an uninterpreted sort, return the size of the
198		* new BV type */
199	29	size_t getBVSkolemSize(size_t capacity)
200		{
201	29	return static_cast<size_t>(log2(capacity)) + 1;
202		}
203
204		/* Given the lowest capacity requirements for each uninterpreted sort, assign
205		* a sufficient bit-vector size.
206		* Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
207		* the fresh skolem BV variables. variables */
208	4	void collectUSortsToBV(const std::unordered_set<TNode>& vars,
209		const USortToBVSizeMap& usortCardinality,
210		SubstitutionMap& usVarsToBVVars)
211		{
212	4	NodeManager* nm = NodeManager::currentNM();
213	4	SkolemManager* sm = nm->getSkolemManager();
214
215	33	for (TNode var : vars)
216		{
217	58	TypeNode type = var.getType();
218	29	size_t size = getBVSkolemSize(usortCardinality.at(type));
219		Node skolem = sm->mkDummySkolem(
220		"BVSKOLEM$$",
221	58	nm->mkBitVectorType(size),
222		"a variable created by the ackermannization "
223		"preprocessing pass, representing a variable with uninterpreted sort "
224	116	+ type.toString() + ".");
225	29	usVarsToBVVars.addSubstitution(var, skolem);
226		}
227	4	}
228
229		/* This function returns the list of terms with uninterpreted sort in the
230		* formula represented by assertions. */
231	32	std::unordered_set<TNode> getVarsWithUSorts(AssertionPipeline* assertions)
232		{
233	32	std::unordered_set<TNode> res;
234
235	336	for (const Node& assertion : assertions->ref())
236		{
237	608	std::unordered_set<TNode> vars;
238	304	expr::getVariables(assertion, vars);
239
240	1249	for (const TNode& var : vars)
241		{
242	945	if (var.getType().isSort())
243		{
244	110	res.insert(var);
245		}
246		}
247		}
248
249	32	return res;
250		}
251
252		/* This is the top level of converting uninterpreted sorts to bit-vectors.
253		* We count the number of different variables for each uninterpreted sort.
254		* Then for each sort, we will assign a new bit-vector type with a sufficient
255		* size. The size is calculated to have enough capacity, that can accommodate
256		* the variables occured in the original formula. At the end, all variables of
257		* uninterpreted sorts will be converted into Skolem variables of BV */
258	32	void usortsToBitVectors(const LogicInfo& d_logic,
259		AssertionPipeline* assertions,
260		USortToBVSizeMap& usortCardinality,
261		SubstitutionMap& usVarsToBVVars)
262		{
263	64	std::unordered_set<TNode> toProcess = getVarsWithUSorts(assertions);
264
265	32	if (toProcess.size() > 0)
266		{
267		/* the current version only supports BV for removing uninterpreted sorts */
268	4	if (not d_logic.isTheoryEnabled(theory::THEORY_BV))
269		{
270		return;
271		}
272
273	33	for (TNode term : toProcess)
274		{
275	58	TypeNode type = term.getType();
276		/* Update the counts for each uninterpreted sort.
277		* For non-existing keys, C++ will create a new element for it, which has
278		* a default 0 value, before incrementing by 1. */
279	29	usortCardinality[type] = usortCardinality[type] + 1;
280		}
281
282	4	collectUSortsToBV(toProcess, usortCardinality, usVarsToBVVars);
283
284	68	for (size_t i = 0, size = assertions->size(); i < size; ++i)
285		{
286	128	Node old = (*assertions)[i];
287	128	Node newA = usVarsToBVVars.apply((*assertions)[i]);
288	64	if (newA != old)
289		{
290	49	assertions->replace(i, newA);
291	98	Trace("uninterpretedSorts-to-bv")
292	49	<< " " << old << " => " << (*assertions)[i] << "\n";
293		}
294		}
295		}
296		}
297
298		/* -------------------------------------------------------------------------- */
299
300	6278	Ackermann::Ackermann(PreprocessingPassContext* preprocContext)
301		: PreprocessingPass(preprocContext, "ackermann"),
302	6278	d_funcToSkolem(userContext()),
303	6278	d_usVarsToBVVars(userContext()),
304	18834	d_logic(logicInfo())
305		{
306	6278	}
307
308	32	PreprocessingPassResult Ackermann::applyInternal(
309		AssertionPipeline* assertionsToPreprocess)
310		{
311	32	AlwaysAssert(!options().base.incrementalSolving);
312
313		/* collect all function applications and generate consistency lemmas
314		* accordingly */
315	64	std::vector<TNode> to_process;
316	151	for (const Node& a : assertionsToPreprocess->ref())
317		{
318	119	to_process.push_back(a);
319		}
320	32	collectFunctionsAndLemmas(
321		d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess);
322
323		/* replace applications of UF by skolems */
324		// FIXME for model building, github issue #1901
325	336	for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
326		{
327	304	assertionsToPreprocess->replace(
328	608	i, d_funcToSkolem.apply((*assertionsToPreprocess)[i]));
329		}
330
331		/* replace uninterpreted sorts with bit-vectors */
332	32	usortsToBitVectors(
333		d_logic, assertionsToPreprocess, d_usortCardinality, d_usVarsToBVVars);
334
335	64	return PreprocessingPassResult::NO_CONFLICT;
336		}
337
338		/* -------------------------------------------------------------------------- */
339
340		} // namespace passes
341		} // namespace preprocessing
342	22755	} // namespace cvc5