Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/model_blocker.cpp	Lines:	123	145	84.8 %
Date:	2021-11-07	Branches:	279	764	36.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, 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 utility for blocking models.
 */

#include "smt/model_blocker.h"

#include "expr/node.h"
#include "expr/node_algorithm.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"

using namespace cvc5::kind;

namespace cvc5 {

ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {}

Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
                                   theory::TheoryModel* m,
                                   options::BlockModelsMode mode,
                                   const std::vector<Node>& exprToBlock)
{
  NodeManager* nm = NodeManager::currentNM();
  // convert to nodes
  std::vector<Node> tlAsserts = assertions;
  std::vector<Node> nodesToBlock = exprToBlock;
  Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
  Node blocker;
  if (mode == options::BlockModelsMode::LITERALS)
  {
    Assert(nodesToBlock.empty());
    // optimization: filter out top-level unit assertions, as they cannot
    // contribute to model blocking.
    unsigned counter = 0;
    std::vector<Node> asserts;
    while (counter < tlAsserts.size())
    {
      Node cur = tlAsserts[counter];
      counter++;
      Node catom = cur.getKind() == NOT ? cur[0] : cur;
      bool cpol = cur.getKind() != NOT;
      if (catom.getKind() == NOT)
      {
        tlAsserts.push_back(catom[0]);
      }
      else if (catom.getKind() == AND && cpol)
      {
        tlAsserts.insert(tlAsserts.end(), catom.begin(), catom.end());
      }
      else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
      {
        asserts.push_back(cur);
        Trace("model-blocker") << "  " << cur << std::endl;
      }
    }
    if (asserts.empty())
    {
      Node blockTriv = nm->mkConst(false);
      Trace("model-blocker")
          << "...model blocker is (trivially) " << blockTriv << std::endl;
      return blockTriv;
    }

    Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0];
    std::unordered_map<TNode, Node> visited;
    std::unordered_map<TNode, Node> implicant;
    std::unordered_map<TNode, Node>::iterator it;
    std::vector<TNode> visit;
    TNode cur;
    visit.push_back(formula);
    do
    {
      cur = visit.back();
      visit.pop_back();
      it = visited.find(cur);

      Trace("model-blocker-debug") << "Visit : " << cur << std::endl;

      if (it == visited.end())
      {
        visited[cur] = Node::null();
        Node catom = cur.getKind() == NOT ? cur[0] : cur;
        bool cpol = cur.getKind() != NOT;
        // compute the implicant
        // impl is a formula that implies cur that is also satisfied by m
        Node impl;
        if (catom.getKind() == NOT)
        {
          // double negation
          impl = catom[0];
        }
        else if (catom.getKind() == OR || catom.getKind() == AND)
        {
          // if disjunctive
          if ((catom.getKind() == OR) == cpol)
          {
            // take the first literal that is satisfied
            for (Node n : catom)
            {
              // rewrite, this ensures that e.g. the propositional value of
              // quantified formulas can be queried
              n = rewrite(n);
              Node vn = m->getValue(n);
              Assert(vn.isConst());
              if (vn.getConst<bool>() == cpol)
              {
                impl = cpol ? n : n.negate();
                break;
              }
            }
          }
          else if (catom.getKind() == OR)
          {
            // one step NNF
            std::vector<Node> children;
            for (const Node& cn : catom)
            {
              children.push_back(cn.negate());
            }
            impl = nm->mkNode(AND, children);
          }
        }
        else if (catom.getKind() == ITE)
        {
          Node vcond = m->getValue(cur[0]);
          Assert(vcond.isConst());
          Node cond = cur[0];
          Node branch;
          if (vcond.getConst<bool>())
          {
            branch = cur[1];
          }
          else
          {
            cond = cond.negate();
            branch = cur[2];
          }
          impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate());
        }
        else if ((catom.getKind() == EQUAL && catom[0].getType().isBoolean())
                 || catom.getKind() == XOR)
        {
          // based on how the children evaluate in the model
          std::vector<Node> children;
          for (const Node& cn : catom)
          {
            Node vn = m->getValue(cn);
            Assert(vn.isConst());
            children.push_back(vn.getConst<bool>() ? cn : cn.negate());
          }
          impl = nm->mkNode(AND, children);
        }
        else
        {
          // literals justified by themselves
          visited[cur] = cur;
          Trace("model-blocker-debug") << "...self justified" << std::endl;
        }
        if (visited[cur].isNull())
        {
          visit.push_back(cur);
          if (impl.isNull())
          {
            Assert(cur.getKind() == AND);
            Trace("model-blocker-debug") << "...recurse" << std::endl;
            visit.insert(visit.end(), cur.begin(), cur.end());
          }
          else
          {
            Trace("model-blocker-debug")
                << "...implicant : " << impl << std::endl;
            implicant[cur] = impl;
            visit.push_back(impl);
          }
        }
      }
      else if (it->second.isNull())
      {
        Node ret = cur;
        it = implicant.find(cur);
        if (it != implicant.end())
        {
          Node impl = it->second;
          it = visited.find(impl);
          Assert(it != visited.end());
          Assert(!it->second.isNull());
          ret = it->second;
          Trace("model-blocker-debug")
              << "...implicant res: " << ret << std::endl;
        }
        else
        {
          bool childChanged = false;
          std::vector<Node> children;
          // we never recurse to parameterized nodes
          Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
          for (const Node& cn : cur)
          {
            it = visited.find(cn);
            Assert(it != visited.end());
            Assert(!it->second.isNull());
            childChanged = childChanged || cn != it->second;
            children.push_back(it->second);
          }
          if (childChanged)
          {
            ret = nm->mkNode(cur.getKind(), children);
          }
          Trace("model-blocker-debug") << "...recons res: " << ret << std::endl;
        }
        visited[cur] = ret;
      }
    } while (!visit.empty());
    Assert(visited.find(formula) != visited.end());
    Assert(!visited.find(formula)->second.isNull());
    blocker = visited[formula].negate();
  }
  else
  {
    Assert(mode == options::BlockModelsMode::VALUES);
    std::vector<Node> blockers;
    // if specific terms were not specified, block all variables of
    // the model
    if (nodesToBlock.empty())
    {
      Trace("model-blocker")
          << "no specific terms to block recognized" << std::endl;
      std::unordered_set<Node> symbols;
      for (Node n : tlAsserts)
      {
        expr::getSymbols(n, symbols);
      }
      for (Node s : symbols)
      {
        if (s.getType().getKind() != kind::FUNCTION_TYPE)
        {
          Node v = m->getValue(s);
          Node a = nm->mkNode(DISTINCT, s, v);
          blockers.push_back(a);
        }
      }
    }
    // otherwise, block all terms that were specified in get-value
    else
    {
      std::unordered_set<Node> terms;
      for (Node n : nodesToBlock)
      {
        Node v = m->getValue(n);
        Node a = nm->mkNode(DISTINCT, n, v);
        blockers.push_back(a);
      }
    }
    if (blockers.size() == 0)
    {
      blocker = nm->mkConst<bool>(true);
    }
    else if (blockers.size() == 1)
    {
      blocker = blockers[0];
    }
    else
    {
      blocker = nm->mkNode(OR, blockers);
    }
  }
  Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
  return blocker;
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, 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 utility for blocking models.
14		*/
15
16		#include "smt/model_blocker.h"
17
18		#include "expr/node.h"
19		#include "expr/node_algorithm.h"
20		#include "theory/quantifiers/term_util.h"
21		#include "theory/rewriter.h"
22		#include "theory/theory_model.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27
28	26	ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {}
29
30	26	Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
31		theory::TheoryModel* m,
32		options::BlockModelsMode mode,
33		const std::vector<Node>& exprToBlock)
34		{
35	26	NodeManager* nm = NodeManager::currentNM();
36		// convert to nodes
37	52	std::vector<Node> tlAsserts = assertions;
38	52	std::vector<Node> nodesToBlock = exprToBlock;
39	26	Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl;
40	52	Node blocker;
41	26	if (mode == options::BlockModelsMode::LITERALS)
42		{
43	10	Assert(nodesToBlock.empty());
44		// optimization: filter out top-level unit assertions, as they cannot
45		// contribute to model blocking.
46	10	unsigned counter = 0;
47	20	std::vector<Node> asserts;
48	62	while (counter < tlAsserts.size())
49		{
50	52	Node cur = tlAsserts[counter];
51	26	counter++;
52	52	Node catom = cur.getKind() == NOT ? cur[0] : cur;
53	26	bool cpol = cur.getKind() != NOT;
54	26	if (catom.getKind() == NOT)
55		{
56		tlAsserts.push_back(catom[0]);
57		}
58	26	else if (catom.getKind() == AND && cpol)
59		{
60		tlAsserts.insert(tlAsserts.end(), catom.begin(), catom.end());
61		}
62	26	else if (theory::quantifiers::TermUtil::isBoolConnectiveTerm(catom))
63		{
64	10	asserts.push_back(cur);
65	10	Trace("model-blocker") << " " << cur << std::endl;
66		}
67		}
68	10	if (asserts.empty())
69		{
70		Node blockTriv = nm->mkConst(false);
71		Trace("model-blocker")
72		<< "...model blocker is (trivially) " << blockTriv << std::endl;
73		return blockTriv;
74		}
75
76	20	Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0];
77	20	std::unordered_map<TNode, Node> visited;
78	20	std::unordered_map<TNode, Node> implicant;
79	10	std::unordered_map<TNode, Node>::iterator it;
80	20	std::vector<TNode> visit;
81	20	TNode cur;
82	10	visit.push_back(formula);
83	26	do
84		{
85	36	cur = visit.back();
86	36	visit.pop_back();
87	36	it = visited.find(cur);
88
89	36	Trace("model-blocker-debug") << "Visit : " << cur << std::endl;
90
91	36	if (it == visited.end())
92		{
93	22	visited[cur] = Node::null();
94	44	Node catom = cur.getKind() == NOT ? cur[0] : cur;
95	22	bool cpol = cur.getKind() != NOT;
96		// compute the implicant
97		// impl is a formula that implies cur that is also satisfied by m
98	44	Node impl;
99	22	if (catom.getKind() == NOT)
100		{
101		// double negation
102		impl = catom[0];
103		}
104	22	else if (catom.getKind() == OR \|\| catom.getKind() == AND)
105		{
106		// if disjunctive
107	10	if ((catom.getKind() == OR) == cpol)
108		{
109		// take the first literal that is satisfied
110	24	for (Node n : catom)
111		{
112		// rewrite, this ensures that e.g. the propositional value of
113		// quantified formulas can be queried
114	24	n = rewrite(n);
115	40	Node vn = m->getValue(n);
116	24	Assert(vn.isConst());
117	24	if (vn.getConst<bool>() == cpol)
118		{
119	8	impl = cpol ? n : n.negate();
120	8	break;
121		}
122		}
123		}
124	2	else if (catom.getKind() == OR)
125		{
126		// one step NNF
127		std::vector<Node> children;
128		for (const Node& cn : catom)
129		{
130		children.push_back(cn.negate());
131		}
132		impl = nm->mkNode(AND, children);
133		}
134		}
135	12	else if (catom.getKind() == ITE)
136		{
137		Node vcond = m->getValue(cur[0]);
138		Assert(vcond.isConst());
139		Node cond = cur[0];
140		Node branch;
141		if (vcond.getConst<bool>())
142		{
143		branch = cur[1];
144		}
145		else
146		{
147		cond = cond.negate();
148		branch = cur[2];
149		}
150		impl = nm->mkNode(AND, cond, cpol ? branch : branch.negate());
151		}
152	34	else if ((catom.getKind() == EQUAL && catom[0].getType().isBoolean())
153	34	\|\| catom.getKind() == XOR)
154		{
155		// based on how the children evaluate in the model
156	4	std::vector<Node> children;
157	6	for (const Node& cn : catom)
158		{
159	8	Node vn = m->getValue(cn);
160	4	Assert(vn.isConst());
161	4	children.push_back(vn.getConst<bool>() ? cn : cn.negate());
162		}
163	2	impl = nm->mkNode(AND, children);
164		}
165		else
166		{
167		// literals justified by themselves
168	10	visited[cur] = cur;
169	10	Trace("model-blocker-debug") << "...self justified" << std::endl;
170		}
171	22	if (visited[cur].isNull())
172		{
173	12	visit.push_back(cur);
174	12	if (impl.isNull())
175		{
176	2	Assert(cur.getKind() == AND);
177	2	Trace("model-blocker-debug") << "...recurse" << std::endl;
178	2	visit.insert(visit.end(), cur.begin(), cur.end());
179		}
180		else
181		{
182	20	Trace("model-blocker-debug")
183	10	<< "...implicant : " << impl << std::endl;
184	10	implicant[cur] = impl;
185	10	visit.push_back(impl);
186		}
187		}
188		}
189	14	else if (it->second.isNull())
190		{
191	24	Node ret = cur;
192	12	it = implicant.find(cur);
193	12	if (it != implicant.end())
194		{
195	20	Node impl = it->second;
196	10	it = visited.find(impl);
197	10	Assert(it != visited.end());
198	10	Assert(!it->second.isNull());
199	10	ret = it->second;
200	20	Trace("model-blocker-debug")
201	10	<< "...implicant res: " << ret << std::endl;
202		}
203		else
204		{
205	2	bool childChanged = false;
206	4	std::vector<Node> children;
207		// we never recurse to parameterized nodes
208	2	Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
209	6	for (const Node& cn : cur)
210		{
211	4	it = visited.find(cn);
212	4	Assert(it != visited.end());
213	4	Assert(!it->second.isNull());
214	4	childChanged = childChanged \|\| cn != it->second;
215	4	children.push_back(it->second);
216		}
217	2	if (childChanged)
218		{
219		ret = nm->mkNode(cur.getKind(), children);
220		}
221	2	Trace("model-blocker-debug") << "...recons res: " << ret << std::endl;
222		}
223	12	visited[cur] = ret;
224		}
225	36	} while (!visit.empty());
226	10	Assert(visited.find(formula) != visited.end());
227	10	Assert(!visited.find(formula)->second.isNull());
228	10	blocker = visited[formula].negate();
229		}
230		else
231		{
232	16	Assert(mode == options::BlockModelsMode::VALUES);
233	32	std::vector<Node> blockers;
234		// if specific terms were not specified, block all variables of
235		// the model
236	16	if (nodesToBlock.empty())
237		{
238	12	Trace("model-blocker")
239	6	<< "no specific terms to block recognized" << std::endl;
240	12	std::unordered_set<Node> symbols;
241	33	for (Node n : tlAsserts)
242		{
243	27	expr::getSymbols(n, symbols);
244		}
245	24	for (Node s : symbols)
246		{
247	18	if (s.getType().getKind() != kind::FUNCTION_TYPE)
248		{
249	24	Node v = m->getValue(s);
250	24	Node a = nm->mkNode(DISTINCT, s, v);
251	12	blockers.push_back(a);
252		}
253		}
254		}
255		// otherwise, block all terms that were specified in get-value
256		else
257		{
258	20	std::unordered_set<Node> terms;
259	20	for (Node n : nodesToBlock)
260		{
261	20	Node v = m->getValue(n);
262	20	Node a = nm->mkNode(DISTINCT, n, v);
263	10	blockers.push_back(a);
264		}
265		}
266	16	if (blockers.size() == 0)
267		{
268		blocker = nm->mkConst<bool>(true);
269		}
270	16	else if (blockers.size() == 1)
271		{
272	10	blocker = blockers[0];
273		}
274		else
275		{
276	6	blocker = nm->mkNode(OR, blockers);
277		}
278		}
279	26	Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
280	26	return blocker;
281		}
282
283	31137	} // namespace cvc5