Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/synth_engine.cpp	Lines:	114	120	95.0 %
Date:	2021-11-07	Branches:	187	340	55.0 %


/******************************************************************************
 * 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(Env& env,
                         QuantifiersState& qs,
                         QuantifiersInferenceManager& qim,
                         QuantifiersRegistry& qr,
                         TermRegistry& tr)
    : QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env)
{
  d_conjs.push_back(std::unique_ptr<SynthConjecture>(
      new SynthConjecture(env, 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))
      {
        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_env, 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) || (qa.isFunDef(q) && options::sygusRecFun()))
  {
    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;
  }
  Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
  Trace("sygus-engine-debug") << "  *** Check candidate phase..." << std::endl;
  size_t prevPending = d_qim.numPendingLemmas();
  bool ret = conj->doCheck();
  // if we added a lemma, return true
  if (d_qim.numPendingLemmas() > prevPending)
  {
    Trace("sygus-engine-debug")
        << "  ...check for counterexample." << std::endl;
    return true;
  }
  return ret;
}

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	1900	SynthEngine::SynthEngine(Env& env,
30		QuantifiersState& qs,
31		QuantifiersInferenceManager& qim,
32		QuantifiersRegistry& qr,
33	1900	TermRegistry& tr)
34	1900	: QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env)
35		{
36	3800	d_conjs.push_back(std::unique_ptr<SynthConjecture>(
37	1900	new SynthConjecture(env, qs, qim, qr, tr, d_statistics)));
38	1900	d_conj = d_conjs.back().get();
39	1900	}
40
41	3792	SynthEngine::~SynthEngine() {}
42
43	1846	void SynthEngine::presolve()
44		{
45	1846	Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
46	3692	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
47		{
48	1846	d_conjs[i]->presolve();
49		}
50	1846	Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
51	1846	}
52
53	24923	bool SynthEngine::needsCheck(Theory::Effort e)
54		{
55	24923	return e >= Theory::EFFORT_LAST_CALL;
56		}
57
58	11095	QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
59		{
60	11095	return QEFFORT_MODEL;
61		}
62
63	37441	void SynthEngine::check(Theory::Effort e, QEffort quant_e)
64		{
65		// are we at the proper effort level?
66	37441	if (quant_e != QEFFORT_MODEL)
67		{
68	53646	return;
69		}
70
71		// if we are waiting to assign the conjecture, do it now
72	10621	bool assigned = !d_waiting_conj.empty();
73	10641	while (!d_waiting_conj.empty())
74		{
75	20	Node q = d_waiting_conj.back();
76	10	d_waiting_conj.pop_back();
77	20	Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
78	10	<< std::endl;
79	10	assignConjecture(q);
80		}
81	10621	if (assigned)
82		{
83		// assign conjecture always uses the output channel, either by reducing a
84		// quantified formula to another, or adding initial lemmas during
85		// SynthConjecture::assign. Thus, we return here and re-check.
86	6	return;
87		}
88
89	21230	Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
90	10615	<< std::endl;
91	10615	Trace("sygus-engine-debug") << std::endl;
92	10615	Valuation& valuation = d_qstate.getValuation();
93	21230	std::vector<SynthConjecture*> activeCheckConj;
94	21230	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
95		{
96	10615	SynthConjecture* sc = d_conjs[i].get();
97	10615	bool active = false;
98		bool value;
99	10615	if (valuation.hasSatValue(sc->getConjecture(), value))
100		{
101	10590	active = value;
102		}
103		else
104		{
105	50	Trace("sygus-engine-debug") << "...no value for quantified formula."
106	25	<< std::endl;
107		}
108	21230	Trace("sygus-engine-debug")
109	10615	<< "Current conjecture status : active : " << active << std::endl;
110	10615	if (active && sc->needsCheck())
111		{
112	10582	activeCheckConj.push_back(sc);
113		}
114		}
115	21230	std::vector<SynthConjecture*> acnext;
116	49520	do
117		{
118	120270	Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
119	60135	<< " active conjectures..." << std::endl;
120	120223	for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
121		{
122	60102	SynthConjecture* sc = activeCheckConj[i];
123	60102	if (!checkConjecture(sc))
124		{
125	49750	acnext.push_back(sc);
126		}
127		}
128	60121	activeCheckConj.clear();
129	60121	activeCheckConj = acnext;
130	60121	acnext.clear();
131	60121	} while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
132	21202	Trace("sygus-engine")
133	10601	<< "Finished Counterexample Guided Instantiation engine." << std::endl;
134		}
135
136	546	void SynthEngine::assignConjecture(Node q)
137		{
138	546	Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
139	546	if (options::sygusQePreproc())
140		{
141	16	Node lem = d_sqp.preprocess(q);
142	10	if (!lem.isNull())
143		{
144	8	Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
145	4	<< std::endl;
146	4	d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
147		// we've reduced the original to a preprocessed version, return
148	4	return;
149		}
150		}
151		// allocate a new synthesis conjecture if not assigned
152	542	if (d_conjs.back()->isAssigned())
153		{
154		d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture(
155		d_env, d_qstate, d_qim, d_qreg, d_treg, d_statistics)));
156		}
157	542	d_conjs.back()->assign(q);
158		}
159
160	1263	void SynthEngine::checkOwnership(Node q)
161		{
162		// take ownership of quantified formulas with sygus attribute, and function
163		// definitions when options::sygusRecFun is true.
164	1263	QuantAttributes& qa = d_qreg.getQuantAttributes();
165	1263	if (qa.isSygus(q) \|\| (qa.isFunDef(q) && options::sygusRecFun()))
166		{
167	584	d_qreg.setOwner(q, this, 2);
168		}
169	1263	}
170
171	1263	void SynthEngine::registerQuantifier(Node q)
172		{
173	2526	Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
174	1263	<< std::endl;
175	1263	if (d_qreg.getOwner(q) != this)
176		{
177	679	return;
178		}
179	584	if (d_qreg.getQuantAttributes().isFunDef(q))
180		{
181	36	Assert(options::sygusRecFun());
182		// If it is a recursive function definition, add it to the function
183		// definition evaluator class.
184	36	Trace("cegqi") << "Registering function definition : " << q << "\n";
185	36	FunDefEvaluator* fde = d_treg.getTermDatabaseSygus()->getFunDefEvaluator();
186	36	fde->assertDefinition(q);
187	36	return;
188		}
189	548	Trace("cegqi") << "Register conjecture : " << q << std::endl;
190	548	if (options::sygusQePreproc())
191		{
192	12	d_waiting_conj.push_back(q);
193		}
194		else
195		{
196		// assign it now
197	536	assignConjecture(q);
198		}
199		}
200
201	60102	bool SynthEngine::checkConjecture(SynthConjecture* conj)
202		{
203	60102	if (Trace.isOn("sygus-engine-debug"))
204		{
205		conj->debugPrint("sygus-engine-debug");
206		Trace("sygus-engine-debug") << std::endl;
207		}
208	60102	Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
209	60102	Trace("sygus-engine-debug") << " *** Check candidate phase..." << std::endl;
210	60102	size_t prevPending = d_qim.numPendingLemmas();
211	60102	bool ret = conj->doCheck();
212		// if we added a lemma, return true
213	60088	if (d_qim.numPendingLemmas() > prevPending)
214		{
215	11446	Trace("sygus-engine-debug")
216	5723	<< " ...check for counterexample." << std::endl;
217	5723	return true;
218		}
219	54365	return ret;
220		}
221
222	288	bool SynthEngine::getSynthSolutions(
223		std::map<Node, std::map<Node, Node> >& sol_map)
224		{
225	288	bool ret = true;
226	576	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
227		{
228	288	if (d_conjs[i]->isAssigned())
229		{
230	284	if (!d_conjs[i]->getSynthSolutions(sol_map))
231		{
232		// if one conjecture fails, we fail overall
233		ret = false;
234		break;
235		}
236		}
237		}
238	288	return ret;
239		}
240
241	3798	void SynthEngine::preregisterAssertion(Node n)
242		{
243		// check if it sygus conjecture
244	3798	if (QuantAttributes::checkSygusConjecture(n))
245		{
246		// this is a sygus conjecture
247	544	Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
248	544	d_conj->preregisterConjecture(n);
249		}
250	3798	}
251
252		} // namespace quantifiers
253		} // namespace theory
254	31137	} // namespace cvc5