Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/synth_engine.cpp	Lines:	120	126	95.2 %
Date:	2021-09-10	Branches:	197	356	55.3 %


/******************************************************************************
 * 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))
      {
        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_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;
  }

  if (!conj->needsRefinement())
  {
    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;
    }
    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	1228	SynthEngine::SynthEngine(Env& env,
30		QuantifiersState& qs,
31		QuantifiersInferenceManager& qim,
32		QuantifiersRegistry& qr,
33	1228	TermRegistry& tr)
34	1228	: QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env)
35		{
36	2456	d_conjs.push_back(std::unique_ptr<SynthConjecture>(
37	1228	new SynthConjecture(env, qs, qim, qr, tr, d_statistics)));
38	1228	d_conj = d_conjs.back().get();
39	1228	}
40
41	2452	SynthEngine::~SynthEngine() {}
42
43	1210	void SynthEngine::presolve()
44		{
45	1210	Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
46	2420	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
47		{
48	1210	d_conjs[i]->presolve();
49		}
50	1210	Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
51	1210	}
52
53	11705	bool SynthEngine::needsCheck(Theory::Effort e)
54		{
55	11705	return e >= Theory::EFFORT_LAST_CALL;
56		}
57
58	4971	QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
59		{
60	4971	return QEFFORT_MODEL;
61		}
62
63	16307	void SynthEngine::check(Theory::Effort e, QEffort quant_e)
64		{
65		// are we at the proper effort level?
66	16307	if (quant_e != QEFFORT_MODEL)
67		{
68	23470	return;
69		}
70
71		// if we are waiting to assign the conjecture, do it now
72	4574	bool assigned = !d_waiting_conj.empty();
73	4588	while (!d_waiting_conj.empty())
74		{
75	14	Node q = d_waiting_conj.back();
76	7	d_waiting_conj.pop_back();
77	14	Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
78	7	<< std::endl;
79	7	assignConjecture(q);
80		}
81	4574	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	4	return;
87		}
88
89	9140	Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
90	4570	<< std::endl;
91	4570	Trace("sygus-engine-debug") << std::endl;
92	4570	Valuation& valuation = d_qstate.getValuation();
93	9140	std::vector<SynthConjecture*> activeCheckConj;
94	9140	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
95		{
96	4570	SynthConjecture* sc = d_conjs[i].get();
97	4570	bool active = false;
98		bool value;
99	4570	if (valuation.hasSatValue(sc->getConjecture(), value))
100		{
101	4519	active = value;
102		}
103		else
104		{
105	102	Trace("sygus-engine-debug") << "...no value for quantified formula."
106	51	<< std::endl;
107		}
108	9140	Trace("sygus-engine-debug")
109	4570	<< "Current conjecture status : active : " << active << std::endl;
110	4570	if (active && sc->needsCheck())
111		{
112	4511	activeCheckConj.push_back(sc);
113		}
114		}
115	9140	std::vector<SynthConjecture*> acnext;
116	34311	do
117		{
118	77762	Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
119	38881	<< " active conjectures..." << std::endl;
120	77694	for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
121		{
122	38822	SynthConjecture* sc = activeCheckConj[i];
123	38822	if (!checkConjecture(sc))
124		{
125	34483	if (!sc->needsRefinement())
126		{
127	34483	acnext.push_back(sc);
128		}
129		}
130		}
131	38872	activeCheckConj.clear();
132	38872	activeCheckConj = acnext;
133	38872	acnext.clear();
134	38872	} while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
135	9122	Trace("sygus-engine")
136	4561	<< "Finished Counterexample Guided Instantiation engine." << std::endl;
137		}
138
139	333	void SynthEngine::assignConjecture(Node q)
140		{
141	333	Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
142	333	if (options::sygusQePreproc())
143		{
144	11	Node lem = d_sqp.preprocess(q);
145	7	if (!lem.isNull())
146		{
147	6	Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
148	3	<< std::endl;
149	3	d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
150		// we've reduced the original to a preprocessed version, return
151	3	return;
152		}
153		}
154		// allocate a new synthesis conjecture if not assigned
155	330	if (d_conjs.back()->isAssigned())
156		{
157		d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture(
158		d_env, d_qstate, d_qim, d_qreg, d_treg, d_statistics)));
159		}
160	330	d_conjs.back()->assign(q);
161		}
162
163	784	void SynthEngine::checkOwnership(Node q)
164		{
165		// take ownership of quantified formulas with sygus attribute, and function
166		// definitions when options::sygusRecFun is true.
167	784	QuantAttributes& qa = d_qreg.getQuantAttributes();
168	784	if (qa.isSygus(q) \|\| (qa.isFunDef(q) && options::sygusRecFun()))
169		{
170	368	d_qreg.setOwner(q, this, 2);
171		}
172	784	}
173
174	784	void SynthEngine::registerQuantifier(Node q)
175		{
176	1568	Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
177	784	<< std::endl;
178	784	if (d_qreg.getOwner(q) != this)
179		{
180	416	return;
181		}
182	368	if (d_qreg.getQuantAttributes().isFunDef(q))
183		{
184	33	Assert(options::sygusRecFun());
185		// If it is a recursive function definition, add it to the function
186		// definition evaluator class.
187	33	Trace("cegqi") << "Registering function definition : " << q << "\n";
188	33	FunDefEvaluator* fde = d_treg.getTermDatabaseSygus()->getFunDefEvaluator();
189	33	fde->assertDefinition(q);
190	33	return;
191		}
192	335	Trace("cegqi") << "Register conjecture : " << q << std::endl;
193	335	if (options::sygusQePreproc())
194		{
195	9	d_waiting_conj.push_back(q);
196		}
197		else
198		{
199		// assign it now
200	326	assignConjecture(q);
201		}
202		}
203
204	38822	bool SynthEngine::checkConjecture(SynthConjecture* conj)
205		{
206	38822	if (Trace.isOn("sygus-engine-debug"))
207		{
208		conj->debugPrint("sygus-engine-debug");
209		Trace("sygus-engine-debug") << std::endl;
210		}
211
212	38822	if (!conj->needsRefinement())
213		{
214	38814	Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
215	77628	Trace("sygus-engine-debug")
216	38814	<< " *** Check candidate phase..." << std::endl;
217	38814	size_t prevPending = d_qim.numPendingLemmas();
218	38814	bool ret = conj->doCheck();
219		// if we added a lemma, return true
220	38805	if (d_qim.numPendingLemmas() > prevPending)
221		{
222	4618	Trace("sygus-engine-debug")
223	2309	<< " ...check for counterexample." << std::endl;
224	2309	return true;
225		}
226	36496	if (!conj->needsRefinement())
227		{
228	36102	return ret;
229		}
230		// otherwise, immediately go to refine candidate
231		}
232	402	Trace("sygus-engine-debug") << " *** Refine candidate phase..." << std::endl;
233	402	return conj->doRefine();
234		}
235
236	257	bool SynthEngine::getSynthSolutions(
237		std::map<Node, std::map<Node, Node> >& sol_map)
238		{
239	257	bool ret = true;
240	514	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
241		{
242	257	if (d_conjs[i]->isAssigned())
243		{
244	253	if (!d_conjs[i]->getSynthSolutions(sol_map))
245		{
246		// if one conjecture fails, we fail overall
247		ret = false;
248		break;
249		}
250		}
251		}
252	257	return ret;
253		}
254
255	2581	void SynthEngine::preregisterAssertion(Node n)
256		{
257		// check if it sygus conjecture
258	2581	if (QuantAttributes::checkSygusConjecture(n))
259		{
260		// this is a sygus conjecture
261	332	Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
262	332	d_conj->preregisterConjecture(n);
263		}
264	2581	}
265
266		} // namespace quantifiers
267		} // namespace theory
268	29502	} // namespace cvc5