Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/synth_engine.cpp	Lines:	127	133	95.5 %
Date:	2021-05-24	Branches:	214	386	55.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, Gereon Kremer
 *
 * 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 the quantifiers module for managing all approaches
 * to synthesis, in particular, those described in Reynolds et al CAV 2015.
 */
#include "theory/quantifiers/sygus/synth_engine.h"

#include "options/quantifiers_options.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_registry.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

SynthEngine::SynthEngine(QuantifiersState& qs,
                         QuantifiersInferenceManager& qim,
                         QuantifiersRegistry& qr,
                         TermRegistry& tr)
    : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp()
{
  d_conjs.push_back(std::unique_ptr<SynthConjecture>(
      new SynthConjecture(qs, qim, qr, tr, d_statistics)));
  d_conj = d_conjs.back().get();
}

SynthEngine::~SynthEngine() {}

void SynthEngine::presolve()
{
  Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
  {
    d_conjs[i]->presolve();
  }
  Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
}

bool SynthEngine::needsCheck(Theory::Effort e)
{
  return e >= Theory::EFFORT_LAST_CALL;
}

QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
{
  return QEFFORT_MODEL;
}

void SynthEngine::check(Theory::Effort e, QEffort quant_e)
{
  // are we at the proper effort level?
  if (quant_e != QEFFORT_MODEL)
  {
    return;
  }

  // if we are waiting to assign the conjecture, do it now
  bool assigned = !d_waiting_conj.empty();
  while (!d_waiting_conj.empty())
  {
    Node q = d_waiting_conj.back();
    d_waiting_conj.pop_back();
    Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
                          << std::endl;
    assignConjecture(q);
  }
  if (assigned)
  {
    // assign conjecture always uses the output channel, either by reducing a
    // quantified formula to another, or adding initial lemmas during
    // SynthConjecture::assign. Thus, we return here and re-check.
    return;
  }

  Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
                        << std::endl;
  Trace("sygus-engine-debug") << std::endl;
  Valuation& valuation = d_qstate.getValuation();
  std::vector<SynthConjecture*> activeCheckConj;
  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
  {
    SynthConjecture* sc = d_conjs[i].get();
    bool active = false;
    bool value;
    if (valuation.hasSatValue(sc->getConjecture(), value))
    {
      active = value;
    }
    else
    {
      Trace("sygus-engine-debug") << "...no value for quantified formula."
                                  << std::endl;
    }
    Trace("sygus-engine-debug")
        << "Current conjecture status : active : " << active << std::endl;
    if (active && sc->needsCheck())
    {
      activeCheckConj.push_back(sc);
    }
  }
  std::vector<SynthConjecture*> acnext;
  do
  {
    Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
                                << " active conjectures..." << std::endl;
    for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
    {
      SynthConjecture* sc = activeCheckConj[i];
      if (!checkConjecture(sc))
      {
        if (!sc->needsRefinement())
        {
          acnext.push_back(sc);
        }
      }
    }
    activeCheckConj.clear();
    activeCheckConj = acnext;
    acnext.clear();
  } while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
  Trace("sygus-engine")
      << "Finished Counterexample Guided Instantiation engine." << std::endl;
}

void SynthEngine::assignConjecture(Node q)
{
  Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
  if (options::sygusQePreproc())
  {
    Node lem = d_sqp.preprocess(q);
    if (!lem.isNull())
    {
      Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
                           << std::endl;
      d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
      // we've reduced the original to a preprocessed version, return
      return;
    }
  }
  // allocate a new synthesis conjecture if not assigned
  if (d_conjs.back()->isAssigned())
  {
    d_conjs.push_back(std::unique_ptr<SynthConjecture>(
        new SynthConjecture(d_qstate, d_qim, d_qreg, d_treg, d_statistics)));
  }
  d_conjs.back()->assign(q);
}

void SynthEngine::checkOwnership(Node q)
{
  // take ownership of quantified formulas with sygus attribute, and function
  // definitions when options::sygusRecFun is true.
  QuantAttributes& qa = d_qreg.getQuantAttributes();
  if (qa.isSygus(q) || (options::sygusRecFun() && qa.isFunDef(q)))
  {
    d_qreg.setOwner(q, this, 2);
  }
}

void SynthEngine::registerQuantifier(Node q)
{
  Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
                       << std::endl;
  if (d_qreg.getOwner(q) != this)
  {
    return;
  }
  if (d_qreg.getQuantAttributes().isFunDef(q))
  {
    Assert(options::sygusRecFun());
    // If it is a recursive function definition, add it to the function
    // definition evaluator class.
    Trace("cegqi") << "Registering function definition : " << q << "\n";
    FunDefEvaluator* fde = d_treg.getTermDatabaseSygus()->getFunDefEvaluator();
    fde->assertDefinition(q);
    return;
  }
  Trace("cegqi") << "Register conjecture : " << q << std::endl;
  if (options::sygusQePreproc())
  {
    d_waiting_conj.push_back(q);
  }
  else
  {
    // assign it now
    assignConjecture(q);
  }
}

bool SynthEngine::checkConjecture(SynthConjecture* conj)
{
  if (Trace.isOn("sygus-engine-debug"))
  {
    conj->debugPrint("sygus-engine-debug");
    Trace("sygus-engine-debug") << std::endl;
  }

  if (!conj->needsRefinement())
  {
    Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
    Trace("sygus-engine-debug")
        << "  *** Check candidate phase..." << std::endl;
    std::vector<Node> cclems;
    bool ret = conj->doCheck(cclems);
    bool addedLemma = false;
    for (const Node& lem : cclems)
    {
      if (d_qim.addPendingLemma(lem, InferenceId::UNKNOWN))
      {
        ++(d_statistics.d_cegqi_lemmas_ce);
        addedLemma = true;
      }
      else
      {
        // this may happen if we eagerly unfold, simplify to true
        Trace("sygus-engine-debug")
            << "  ...FAILED to add candidate!" << std::endl;
      }
    }
    if (addedLemma)
    {
      Trace("sygus-engine-debug")
          << "  ...check for counterexample." << std::endl;
      return true;
    }
    if (!conj->needsRefinement())
    {
      return ret;
    }
    // otherwise, immediately go to refine candidate
  }
  Trace("sygus-engine-debug") << "  *** Refine candidate phase..." << std::endl;
  return conj->doRefine();
}

bool SynthEngine::getSynthSolutions(
    std::map<Node, std::map<Node, Node> >& sol_map)
{
  bool ret = true;
  for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
  {
    if (d_conjs[i]->isAssigned())
    {
      if (!d_conjs[i]->getSynthSolutions(sol_map))
      {
        // if one conjecture fails, we fail overall
        ret = false;
        break;
      }
    }
  }
  return ret;
}

void SynthEngine::preregisterAssertion(Node n)
{
  // check if it sygus conjecture
  if (QuantAttributes::checkSygusConjecture(n))
  {
    // this is a sygus conjecture
    Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
    d_conj->preregisterConjecture(n);
  }
}

}  // 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, Haniel Barbosa, Gereon Kremer
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 the quantifiers module for managing all approaches
14		* to synthesis, in particular, those described in Reynolds et al CAV 2015.
15		*/
16		#include "theory/quantifiers/sygus/synth_engine.h"
17
18		#include "options/quantifiers_options.h"
19		#include "theory/quantifiers/quantifiers_attributes.h"
20		#include "theory/quantifiers/sygus/term_database_sygus.h"
21		#include "theory/quantifiers/term_registry.h"
22
23		using namespace cvc5::kind;
24
25		namespace cvc5 {
26		namespace theory {
27		namespace quantifiers {
28
29	1529	SynthEngine::SynthEngine(QuantifiersState& qs,
30		QuantifiersInferenceManager& qim,
31		QuantifiersRegistry& qr,
32	1529	TermRegistry& tr)
33	1529	: QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp()
34		{
35	3058	d_conjs.push_back(std::unique_ptr<SynthConjecture>(
36	1529	new SynthConjecture(qs, qim, qr, tr, d_statistics)));
37	1529	d_conj = d_conjs.back().get();
38	1529	}
39
40	3058	SynthEngine::~SynthEngine() {}
41
42	1505	void SynthEngine::presolve()
43		{
44	1505	Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
45	3010	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
46		{
47	1505	d_conjs[i]->presolve();
48		}
49	1505	Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
50	1505	}
51
52	11440	bool SynthEngine::needsCheck(Theory::Effort e)
53		{
54	11440	return e >= Theory::EFFORT_LAST_CALL;
55		}
56
57	4922	QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
58		{
59	4922	return QEFFORT_MODEL;
60		}
61
62	16343	void SynthEngine::check(Theory::Effort e, QEffort quant_e)
63		{
64		// are we at the proper effort level?
65	16343	if (quant_e != QEFFORT_MODEL)
66		{
67	23424	return;
68		}
69
70		// if we are waiting to assign the conjecture, do it now
71	4633	bool assigned = !d_waiting_conj.empty();
72	4647	while (!d_waiting_conj.empty())
73		{
74	14	Node q = d_waiting_conj.back();
75	7	d_waiting_conj.pop_back();
76	14	Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
77	7	<< std::endl;
78	7	assignConjecture(q);
79		}
80	4633	if (assigned)
81		{
82		// assign conjecture always uses the output channel, either by reducing a
83		// quantified formula to another, or adding initial lemmas during
84		// SynthConjecture::assign. Thus, we return here and re-check.
85	4	return;
86		}
87
88	9258	Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
89	4629	<< std::endl;
90	4629	Trace("sygus-engine-debug") << std::endl;
91	4629	Valuation& valuation = d_qstate.getValuation();
92	9258	std::vector<SynthConjecture*> activeCheckConj;
93	9258	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
94		{
95	4629	SynthConjecture* sc = d_conjs[i].get();
96	4629	bool active = false;
97		bool value;
98	4629	if (valuation.hasSatValue(sc->getConjecture(), value))
99		{
100	4585	active = value;
101		}
102		else
103		{
104	88	Trace("sygus-engine-debug") << "...no value for quantified formula."
105	44	<< std::endl;
106		}
107	9258	Trace("sygus-engine-debug")
108	4629	<< "Current conjecture status : active : " << active << std::endl;
109	4629	if (active && sc->needsCheck())
110		{
111	4577	activeCheckConj.push_back(sc);
112		}
113		}
114	9258	std::vector<SynthConjecture*> acnext;
115	34285	do
116		{
117	77828	Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
118	38914	<< " active conjectures..." << std::endl;
119	77767	for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
120		{
121	38862	SynthConjecture* sc = activeCheckConj[i];
122	38862	if (!checkConjecture(sc))
123		{
124	34442	if (!sc->needsRefinement())
125		{
126	34442	acnext.push_back(sc);
127		}
128		}
129		}
130	38905	activeCheckConj.clear();
131	38905	activeCheckConj = acnext;
132	38905	acnext.clear();
133	38905	} while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
134	9240	Trace("sygus-engine")
135	4620	<< "Finished Counterexample Guided Instantiation engine." << std::endl;
136		}
137
138	328	void SynthEngine::assignConjecture(Node q)
139		{
140	328	Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
141	990	if (options::sygusQePreproc())
142		{
143	11	Node lem = d_sqp.preprocess(q);
144	7	if (!lem.isNull())
145		{
146	6	Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
147	3	<< std::endl;
148	3	d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
149		// we've reduced the original to a preprocessed version, return
150	3	return;
151		}
152		}
153		// allocate a new synthesis conjecture if not assigned
154	325	if (d_conjs.back()->isAssigned())
155		{
156		d_conjs.push_back(std::unique_ptr<SynthConjecture>(
157		new SynthConjecture(d_qstate, d_qim, d_qreg, d_treg, d_statistics)));
158		}
159	325	d_conjs.back()->assign(q);
160		}
161
162	760	void SynthEngine::checkOwnership(Node q)
163		{
164		// take ownership of quantified formulas with sygus attribute, and function
165		// definitions when options::sygusRecFun is true.
166	760	QuantAttributes& qa = d_qreg.getQuantAttributes();
167	760	if (qa.isSygus(q) \|\| (options::sygusRecFun() && qa.isFunDef(q)))
168		{
169	362	d_qreg.setOwner(q, this, 2);
170		}
171	760	}
172
173	760	void SynthEngine::registerQuantifier(Node q)
174		{
175	1520	Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
176	760	<< std::endl;
177	760	if (d_qreg.getOwner(q) != this)
178		{
179	398	return;
180		}
181	362	if (d_qreg.getQuantAttributes().isFunDef(q))
182		{
183	32	Assert(options::sygusRecFun());
184		// If it is a recursive function definition, add it to the function
185		// definition evaluator class.
186	32	Trace("cegqi") << "Registering function definition : " << q << "\n";
187	32	FunDefEvaluator* fde = d_treg.getTermDatabaseSygus()->getFunDefEvaluator();
188	32	fde->assertDefinition(q);
189	32	return;
190		}
191	330	Trace("cegqi") << "Register conjecture : " << q << std::endl;
192	330	if (options::sygusQePreproc())
193		{
194	9	d_waiting_conj.push_back(q);
195		}
196		else
197		{
198		// assign it now
199	321	assignConjecture(q);
200		}
201		}
202
203	38862	bool SynthEngine::checkConjecture(SynthConjecture* conj)
204		{
205	38862	if (Trace.isOn("sygus-engine-debug"))
206		{
207		conj->debugPrint("sygus-engine-debug");
208		Trace("sygus-engine-debug") << std::endl;
209		}
210
211	38862	if (!conj->needsRefinement())
212		{
213	38857	Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
214	77714	Trace("sygus-engine-debug")
215	38857	<< " *** Check candidate phase..." << std::endl;
216	39270	std::vector<Node> cclems;
217	38857	bool ret = conj->doCheck(cclems);
218	38848	bool addedLemma = false;
219	52343	for (const Node& lem : cclems)
220		{
221	13495	if (d_qim.addPendingLemma(lem, InferenceId::UNKNOWN))
222		{
223	11048	++(d_statistics.d_cegqi_lemmas_ce);
224	11048	addedLemma = true;
225		}
226		else
227		{
228		// this may happen if we eagerly unfold, simplify to true
229	4894	Trace("sygus-engine-debug")
230	2447	<< " ...FAILED to add candidate!" << std::endl;
231		}
232		}
233	38848	if (addedLemma)
234		{
235	4656	Trace("sygus-engine-debug")
236	2328	<< " ...check for counterexample." << std::endl;
237	2328	return true;
238		}
239	36520	if (!conj->needsRefinement())
240		{
241	36116	return ret;
242		}
243		// otherwise, immediately go to refine candidate
244		}
245	409	Trace("sygus-engine-debug") << " *** Refine candidate phase..." << std::endl;
246	409	return conj->doRefine();
247		}
248
249	253	bool SynthEngine::getSynthSolutions(
250		std::map<Node, std::map<Node, Node> >& sol_map)
251		{
252	253	bool ret = true;
253	506	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
254		{
255	253	if (d_conjs[i]->isAssigned())
256		{
257	249	if (!d_conjs[i]->getSynthSolutions(sol_map))
258		{
259		// if one conjecture fails, we fail overall
260		ret = false;
261		break;
262		}
263		}
264		}
265	253	return ret;
266		}
267
268	3489	void SynthEngine::preregisterAssertion(Node n)
269		{
270		// check if it sygus conjecture
271	3489	if (QuantAttributes::checkSygusConjecture(n))
272		{
273		// this is a sygus conjecture
274	327	Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
275	327	d_conj->preregisterConjecture(n);
276		}
277	3489	}
278
279		} // namespace quantifiers
280		} // namespace theory
281	28191	} // namespace cvc5