Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quant_split.cpp	Lines:	100	102	98.0 %
Date:	2021-09-10	Branches:	201	392	51.3 %


/******************************************************************************
 * 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 dynamic quantifiers splitting.
 */

#include "theory/quantifiers/quant_split.h"

#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "options/quantifiers_options.h"
#include "theory/datatypes/theory_datatypes_utils.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

QuantDSplit::QuantDSplit(Env& env,
                         QuantifiersState& qs,
                         QuantifiersInferenceManager& qim,
                         QuantifiersRegistry& qr,
                         TermRegistry& tr)
    : QuantifiersModule(env, qs, qim, qr, tr),
      d_added_split(qs.getUserContext())
{
}

void QuantDSplit::checkOwnership(Node q)
{
  // If q is non-standard (marked as sygus, quantifier elimination, etc.), then
  // do no split it.
  QAttributes qa;
  QuantAttributes::computeQuantAttributes(q, qa);
  if (!qa.isStandard())
  {
    return;
  }
  bool takeOwnership = false;
  bool doSplit = false;
  QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
  Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
    TypeNode tn = q[0][i].getType();
    if( tn.isDatatype() ){
      bool isFinite = d_qstate.isFiniteType(tn);
      const DType& dt = tn.getDType();
      if (dt.isRecursiveSingleton(tn))
      {
        Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
      }
      else
      {
        if (options::quantDynamicSplit() == options::QuantDSplitMode::AGG)
        {
          // split if it is a finite datatype
          doSplit = isFinite;
        }
        else if (options::quantDynamicSplit()
                 == options::QuantDSplitMode::DEFAULT)
        {
          if (!qbi.isFiniteBound(q, q[0][i]))
          {
            if (isFinite)
            {
              // split if goes from being unhandled -> handled by finite
              // instantiation. An example is datatypes with uninterpreted sort
              // fields which are "interpreted finite" but not "finite".
              doSplit = true;
              // we additionally take ownership of this formula, in other words,
              // we mark it reduced.
              takeOwnership = true;
            }
            else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
            {
              // split if only one constructor
              doSplit = true;
            }
          }
        }
        if (doSplit)
        {
          // store the index to split
          d_quant_to_reduce[q] = i;
          Trace("quant-dsplit-debug")
              << "Split at index " << i << " based on datatype " << dt.getName()
              << std::endl;
          break;
        }
        Trace("quant-dsplit-debug")
            << "Do not split based on datatype " << dt.getName() << std::endl;
      }
    }
  }

  if (takeOwnership)
  {
    Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
    d_qreg.setOwner(q, this);
  }
  // Notice we may not take ownership in some cases, meaning that both the
  // original quantified formula and the split one are generated. This may
  // increase our ability to answer "unsat", since quantifier instantiation
  // heuristics may be more effective for one or the other (see issues #993
  // and 3481).
}

/* whether this module needs to check this round */
bool QuantDSplit::needsCheck( Theory::Effort e ) {
  return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
}

bool QuantDSplit::checkCompleteFor( Node q ) {
  // true if we split q
  return d_added_split.find( q )!=d_added_split.end();
}

/* Call during quantifier engine's check */
void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
{
  //add lemmas ASAP (they are a reduction)
  if (quant_e != QEFFORT_CONFLICT)
  {
    return;
  }
  Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
  NodeManager* nm = NodeManager::currentNM();
  FirstOrderModel* m = d_treg.getModel();
  std::vector<Node> lemmas;
  for (std::map<Node, int>::iterator it = d_quant_to_reduce.begin();
       it != d_quant_to_reduce.end();
       ++it)
  {
    Node q = it->first;
    Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
    if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q)
        && d_added_split.find(q) == d_added_split.end())
    {
      d_added_split.insert(q);
      std::vector<Node> bvs;
      for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
      {
        if (static_cast<int>(i) != it->second)
        {
          bvs.push_back(q[0][i]);
        }
      }
      std::vector<Node> disj;
      disj.push_back(q.negate());
      TNode svar = q[0][it->second];
      TypeNode tn = svar.getType();
      Assert(tn.isDatatype());
      std::vector<Node> cons;
      const DType& dt = tn.getDType();
      for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
      {
        std::vector<Node> vars;
        TypeNode dtjtn = dt[j].getSpecializedConstructorType(tn);
        Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1);
        for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
        {
          TypeNode tns = dtjtn[k];
          Node v = nm->mkBoundVar(tns);
          vars.push_back(v);
        }
        std::vector<Node> bvs_cmb;
        bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
        bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
        Node c = datatypes::utils::mkApplyCons(tn, dt, j, vars);
        TNode ct = c;
        Node body = q[1].substitute(svar, ct);
        if (!bvs_cmb.empty())
        {
          Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, bvs_cmb);
          std::vector<Node> children;
          children.push_back(bvl);
          children.push_back(body);
          if (q.getNumChildren() == 3)
          {
            Node ipls = q[2].substitute(svar, ct);
            children.push_back(ipls);
          }
          body = nm->mkNode(kind::FORALL, children);
        }
        cons.push_back(body);
      }
      Node conc = cons.size() == 1 ? cons[0] : nm->mkNode(kind::AND, cons);
      disj.push_back(conc);
      lemmas.push_back(disj.size() == 1 ? disj[0] : nm->mkNode(kind::OR, disj));
    }
  }

  // add lemmas to quantifiers engine
  for (const Node& lem : lemmas)
  {
    Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
    d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_DSPLIT);
  }
  Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
}

}  // namespace quantifiers
}  // namespace theory
}  // 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 dynamic quantifiers splitting.
14		*/
15
16		#include "theory/quantifiers/quant_split.h"
17
18		#include "expr/dtype.h"
19		#include "expr/dtype_cons.h"
20		#include "options/quantifiers_options.h"
21		#include "theory/datatypes/theory_datatypes_utils.h"
22		#include "theory/quantifiers/first_order_model.h"
23		#include "theory/quantifiers/term_database.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace quantifiers {
30
31	5505	QuantDSplit::QuantDSplit(Env& env,
32		QuantifiersState& qs,
33		QuantifiersInferenceManager& qim,
34		QuantifiersRegistry& qr,
35	5505	TermRegistry& tr)
36		: QuantifiersModule(env, qs, qim, qr, tr),
37	5505	d_added_split(qs.getUserContext())
38		{
39	5505	}
40
41	11387	void QuantDSplit::checkOwnership(Node q)
42		{
43		// If q is non-standard (marked as sygus, quantifier elimination, etc.), then
44		// do no split it.
45	22053	QAttributes qa;
46	11387	QuantAttributes::computeQuantAttributes(q, qa);
47	11387	if (!qa.isStandard())
48		{
49	721	return;
50		}
51	10666	bool takeOwnership = false;
52	10666	bool doSplit = false;
53	10666	QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
54	10666	Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
55	34296	for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
56	49072	TypeNode tn = q[0][i].getType();
57	25442	if( tn.isDatatype() ){
58	4627	bool isFinite = d_qstate.isFiniteType(tn);
59	4627	const DType& dt = tn.getDType();
60	4627	if (dt.isRecursiveSingleton(tn))
61		{
62		Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
63		}
64		else
65		{
66	4627	if (options::quantDynamicSplit() == options::QuantDSplitMode::AGG)
67		{
68		// split if it is a finite datatype
69		doSplit = isFinite;
70		}
71	9254	else if (options::quantDynamicSplit()
72	4627	== options::QuantDSplitMode::DEFAULT)
73		{
74	4627	if (!qbi.isFiniteBound(q, q[0][i]))
75		{
76	4492	if (isFinite)
77		{
78		// split if goes from being unhandled -> handled by finite
79		// instantiation. An example is datatypes with uninterpreted sort
80		// fields which are "interpreted finite" but not "finite".
81	902	doSplit = true;
82		// we additionally take ownership of this formula, in other words,
83		// we mark it reduced.
84	902	takeOwnership = true;
85		}
86	3590	else if (dt.getNumConstructors() == 1 && !dt.isCodatatype())
87		{
88		// split if only one constructor
89	910	doSplit = true;
90		}
91		}
92		}
93	4627	if (doSplit)
94		{
95		// store the index to split
96	1812	d_quant_to_reduce[q] = i;
97	3624	Trace("quant-dsplit-debug")
98	3624	<< "Split at index " << i << " based on datatype " << dt.getName()
99	1812	<< std::endl;
100	1812	break;
101		}
102	5630	Trace("quant-dsplit-debug")
103	2815	<< "Do not split based on datatype " << dt.getName() << std::endl;
104		}
105		}
106		}
107
108	10666	if (takeOwnership)
109		{
110	902	Trace("quant-dsplit-debug") << "Will take ownership." << std::endl;
111	902	d_qreg.setOwner(q, this);
112		}
113		// Notice we may not take ownership in some cases, meaning that both the
114		// original quantified formula and the split one are generated. This may
115		// increase our ability to answer "unsat", since quantifier instantiation
116		// heuristics may be more effective for one or the other (see issues #993
117		// and 3481).
118		}
119
120		/* whether this module needs to check this round */
121	47272	bool QuantDSplit::needsCheck( Theory::Effort e ) {
122	47272	return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
123		}
124
125	201	bool QuantDSplit::checkCompleteFor( Node q ) {
126		// true if we split q
127	201	return d_added_split.find( q )!=d_added_split.end();
128		}
129
130		/* Call during quantifier engine's check */
131	1602	void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
132		{
133		//add lemmas ASAP (they are a reduction)
134	1602	if (quant_e != QEFFORT_CONFLICT)
135		{
136	941	return;
137		}
138	661	Trace("quant-dsplit") << "QuantDSplit::check" << std::endl;
139	661	NodeManager* nm = NodeManager::currentNM();
140	661	FirstOrderModel* m = d_treg.getModel();
141	1322	std::vector<Node> lemmas;
142	28046	for (std::map<Node, int>::iterator it = d_quant_to_reduce.begin();
143	28046	it != d_quant_to_reduce.end();
144		++it)
145		{
146	54770	Node q = it->first;
147	27385	Trace("quant-dsplit") << "- Split quantifier " << q << std::endl;
148	109515	if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q)
149	109515	&& d_added_split.find(q) == d_added_split.end())
150		{
151	1804	d_added_split.insert(q);
152	3608	std::vector<Node> bvs;
153	7535	for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
154		{
155	5731	if (static_cast<int>(i) != it->second)
156		{
157	3927	bvs.push_back(q[0][i]);
158		}
159		}
160	3608	std::vector<Node> disj;
161	1804	disj.push_back(q.negate());
162	3608	TNode svar = q[0][it->second];
163	3608	TypeNode tn = svar.getType();
164	1804	Assert(tn.isDatatype());
165	3608	std::vector<Node> cons;
166	1804	const DType& dt = tn.getDType();
167	4273	for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
168		{
169	4938	std::vector<Node> vars;
170	4938	TypeNode dtjtn = dt[j].getSpecializedConstructorType(tn);
171	2469	Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1);
172	6063	for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
173		{
174	7188	TypeNode tns = dtjtn[k];
175	7188	Node v = nm->mkBoundVar(tns);
176	3594	vars.push_back(v);
177		}
178	4938	std::vector<Node> bvs_cmb;
179	2469	bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end());
180	2469	bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end());
181	4938	Node c = datatypes::utils::mkApplyCons(tn, dt, j, vars);
182	4938	TNode ct = c;
183	4938	Node body = q[1].substitute(svar, ct);
184	2469	if (!bvs_cmb.empty())
185		{
186	4930	Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, bvs_cmb);
187	4930	std::vector<Node> children;
188	2465	children.push_back(bvl);
189	2465	children.push_back(body);
190	2465	if (q.getNumChildren() == 3)
191		{
192	1764	Node ipls = q[2].substitute(svar, ct);
193	882	children.push_back(ipls);
194		}
195	2465	body = nm->mkNode(kind::FORALL, children);
196		}
197	2469	cons.push_back(body);
198		}
199	3608	Node conc = cons.size() == 1 ? cons[0] : nm->mkNode(kind::AND, cons);
200	1804	disj.push_back(conc);
201	1804	lemmas.push_back(disj.size() == 1 ? disj[0] : nm->mkNode(kind::OR, disj));
202		}
203		}
204
205		// add lemmas to quantifiers engine
206	2465	for (const Node& lem : lemmas)
207		{
208	1804	Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl;
209	1804	d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_DSPLIT);
210		}
211	661	Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
212		}
213
214		} // namespace quantifiers
215		} // namespace theory
216	29502	} // namespace cvc5