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-29	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	1193	SynthEngine::SynthEngine(Env& env,
30		QuantifiersState& qs,
31		QuantifiersInferenceManager& qim,
32		QuantifiersRegistry& qr,
33	1193	TermRegistry& tr)
34	1193	: QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env)
35		{
36	2386	d_conjs.push_back(std::unique_ptr<SynthConjecture>(
37	1193	new SynthConjecture(env, qs, qim, qr, tr, d_statistics)));
38	1193	d_conj = d_conjs.back().get();
39	1193	}
40
41	2382	SynthEngine::~SynthEngine() {}
42
43	1174	void SynthEngine::presolve()
44		{
45	1174	Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
46	2348	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
47		{
48	1174	d_conjs[i]->presolve();
49		}
50	1174	Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
51	1174	}
52
53	11206	bool SynthEngine::needsCheck(Theory::Effort e)
54		{
55	11206	return e >= Theory::EFFORT_LAST_CALL;
56		}
57
58	4837	QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e)
59		{
60	4837	return QEFFORT_MODEL;
61		}
62
63	16000	void SynthEngine::check(Theory::Effort e, QEffort quant_e)
64		{
65		// are we at the proper effort level?
66	16000	if (quant_e != QEFFORT_MODEL)
67		{
68	22919	return;
69		}
70
71		// if we are waiting to assign the conjecture, do it now
72	4542	bool assigned = !d_waiting_conj.empty();
73	4552	while (!d_waiting_conj.empty())
74		{
75	10	Node q = d_waiting_conj.back();
76	5	d_waiting_conj.pop_back();
77	10	Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
78	5	<< std::endl;
79	5	assignConjecture(q);
80		}
81	4542	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	3	return;
87		}
88
89	9078	Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
90	4539	<< std::endl;
91	4539	Trace("sygus-engine-debug") << std::endl;
92	4539	Valuation& valuation = d_qstate.getValuation();
93	9078	std::vector<SynthConjecture*> activeCheckConj;
94	9078	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
95		{
96	4539	SynthConjecture* sc = d_conjs[i].get();
97	4539	bool active = false;
98		bool value;
99	4539	if (valuation.hasSatValue(sc->getConjecture(), value))
100		{
101	4513	active = value;
102		}
103		else
104		{
105	52	Trace("sygus-engine-debug") << "...no value for quantified formula."
106	26	<< std::endl;
107		}
108	9078	Trace("sygus-engine-debug")
109	4539	<< "Current conjecture status : active : " << active << std::endl;
110	4539	if (active && sc->needsCheck())
111		{
112	4507	activeCheckConj.push_back(sc);
113		}
114		}
115	9078	std::vector<SynthConjecture*> acnext;
116	34311	do
117		{
118	77700	Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
119	38850	<< " active conjectures..." << std::endl;
120	77659	for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
121		{
122	38818	SynthConjecture* sc = activeCheckConj[i];
123	38818	if (!checkConjecture(sc))
124		{
125	34483	if (!sc->needsRefinement())
126		{
127	34483	acnext.push_back(sc);
128		}
129		}
130		}
131	38841	activeCheckConj.clear();
132	38841	activeCheckConj = acnext;
133	38841	acnext.clear();
134	38841	} while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
135	9060	Trace("sygus-engine")
136	4530	<< "Finished Counterexample Guided Instantiation engine." << std::endl;
137		}
138
139	329	void SynthEngine::assignConjecture(Node q)
140		{
141	329	Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
142	329	if (options::sygusQePreproc())
143		{
144	8	Node lem = d_sqp.preprocess(q);
145	5	if (!lem.isNull())
146		{
147	4	Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
148	2	<< std::endl;
149	2	d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
150		// we've reduced the original to a preprocessed version, return
151	2	return;
152		}
153		}
154		// allocate a new synthesis conjecture if not assigned
155	327	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	327	d_conjs.back()->assign(q);
161		}
162
163	741	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	741	QuantAttributes& qa = d_qreg.getQuantAttributes();
168	741	if (qa.isSygus(q) \|\| (qa.isFunDef(q) && options::sygusRecFun()))
169		{
170	364	d_qreg.setOwner(q, this, 2);
171		}
172	741	}
173
174	741	void SynthEngine::registerQuantifier(Node q)
175		{
176	1482	Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
177	741	<< std::endl;
178	741	if (d_qreg.getOwner(q) != this)
179		{
180	377	return;
181		}
182	364	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	331	Trace("cegqi") << "Register conjecture : " << q << std::endl;
193	331	if (options::sygusQePreproc())
194		{
195	7	d_waiting_conj.push_back(q);
196		}
197		else
198		{
199		// assign it now
200	324	assignConjecture(q);
201		}
202		}
203
204	38818	bool SynthEngine::checkConjecture(SynthConjecture* conj)
205		{
206	38818	if (Trace.isOn("sygus-engine-debug"))
207		{
208		conj->debugPrint("sygus-engine-debug");
209		Trace("sygus-engine-debug") << std::endl;
210		}
211
212	38818	if (!conj->needsRefinement())
213		{
214	38810	Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
215	77620	Trace("sygus-engine-debug")
216	38810	<< " *** Check candidate phase..." << std::endl;
217	38810	size_t prevPending = d_qim.numPendingLemmas();
218	38810	bool ret = conj->doCheck();
219		// if we added a lemma, return true
220	38801	if (d_qim.numPendingLemmas() > prevPending)
221		{
222	4622	Trace("sygus-engine-debug")
223	2311	<< " ...check for counterexample." << std::endl;
224	2311	return true;
225		}
226	36490	if (!conj->needsRefinement())
227		{
228	36098	return ret;
229		}
230		// otherwise, immediately go to refine candidate
231		}
232	400	Trace("sygus-engine-debug") << " *** Refine candidate phase..." << std::endl;
233	400	return conj->doRefine();
234		}
235
236	259	bool SynthEngine::getSynthSolutions(
237		std::map<Node, std::map<Node, Node> >& sol_map)
238		{
239	259	bool ret = true;
240	518	for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
241		{
242	259	if (d_conjs[i]->isAssigned())
243		{
244	255	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	259	return ret;
253		}
254
255	2509	void SynthEngine::preregisterAssertion(Node n)
256		{
257		// check if it sygus conjecture
258	2509	if (QuantAttributes::checkSygusConjecture(n))
259		{
260		// this is a sygus conjecture
261	329	Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
262	329	d_conj->preregisterConjecture(n);
263		}
264	2509	}
265
266		} // namespace quantifiers
267		} // namespace theory
268	22746	} // namespace cvc5