Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/enum_value_manager.cpp	Lines:	91	109	83.5 %
Date:	2021-09-11	Branches:	180	442	40.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Haniel Barbosa
 *
 * 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.
 * ****************************************************************************
 *
 * Management of current value for an enumerator
 */
#include "theory/quantifiers/sygus/enum_value_manager.h"

#include "options/base_options.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
#include "theory/quantifiers/sygus/enum_stream_substitution.h"
#include "theory/quantifiers/sygus/sygus_enumerator.h"
#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_registry.h"

using namespace cvc5::kind;
using namespace std;

namespace cvc5 {
namespace theory {
namespace quantifiers {

EnumValueManager::EnumValueManager(Env& env,
                                   QuantifiersState& qs,
                                   QuantifiersInferenceManager& qim,
                                   TermRegistry& tr,
                                   SygusStatistics& s,
                                   Node e,
                                   bool hasExamples)
    : EnvObj(env),
      d_enum(e),
      d_qstate(qs),
      d_qim(qim),
      d_treg(tr),
      d_stats(s),
      d_tds(tr.getTermDatabaseSygus()),
      d_eec(hasExamples ? new ExampleEvalCache(d_tds, e) : nullptr)
{
}

EnumValueManager::~EnumValueManager() {}

Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
{
  Node e = d_enum;
  bool isEnum = d_tds->isEnumerator(e);

  if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
  {
    // if the current model value of e was not registered by the datatypes
    // sygus solver, or was excluded by symmetry breaking, then it does not
    // have a proper model value that we should consider, thus we return null.
    Trace("sygus-engine-debug")
        << "Enumerator " << e << " does not have proper model value."
        << std::endl;
    return Node::null();
  }

  if (!isEnum || d_tds->isPassiveEnumerator(e))
  {
    return getModelValue(e);
  }

  // management of actively generated enumerators goes here

  // initialize the enumerated value generator for e
  if (d_evg == nullptr)
  {
    if (d_tds->isVariableAgnosticEnumerator(e))
    {
      d_evg.reset(new EnumStreamConcrete(d_tds));
    }
    else
    {
      // Actively-generated enumerators are currently either variable agnostic
      // or basic. The auto mode always prefers the optimized enumerator over
      // the basic one.
      Assert(d_tds->isBasicEnumerator(e));
      if (options::sygusActiveGenMode()
          == options::SygusActiveGenMode::ENUM_BASIC)
      {
        d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType()));
      }
      else
      {
        Assert(options::sygusActiveGenMode()
                   == options::SygusActiveGenMode::ENUM
               || options::sygusActiveGenMode()
                      == options::SygusActiveGenMode::AUTO);
        // create the enumerator callback
        if (options::sygusSymBreakDynamic())
        {
          std::ostream* out = nullptr;
          if (options::sygusRewVerify())
          {
            d_samplerRrV.reset(new SygusSampler);
            d_samplerRrV->initializeSygus(
                d_tds, e, options::sygusSamples(), false);
            // use the default output for the output of sygusRewVerify
            out = options().base.out;
          }
          d_secd.reset(new SygusEnumeratorCallbackDefault(
              e, &d_stats, d_eec.get(), d_samplerRrV.get(), out));
        }
        // if sygus repair const is enabled, we enumerate terms with free
        // variables as arguments to any-constant constructors
        d_evg.reset(new SygusEnumerator(
            d_tds, d_secd.get(), &d_stats, false, options::sygusRepairConst()));
      }
    }
    Trace("sygus-active-gen")
        << "Active-gen: initialize for " << e << std::endl;
    d_evg->initialize(e);
    d_ev_curr_active_gen = Node::null();
    Trace("sygus-active-gen-debug") << "...finish" << std::endl;
  }
  // if we have a waiting value, return it
  if (!d_evActiveGenWaiting.isNull())
  {
    Trace("sygus-active-gen-debug")
        << "Active-gen: return waiting " << d_evActiveGenWaiting << std::endl;
    return d_evActiveGenWaiting;
  }
  // Check if there is an (abstract) value absE we were actively generating
  // values based on.
  Node absE = d_ev_curr_active_gen;
  bool firstTime = false;
  if (absE.isNull())
  {
    // None currently exist. The next abstract value is the model value for e.
    absE = getModelValue(e);
    if (Trace.isOn("sygus-active-gen"))
    {
      Trace("sygus-active-gen") << "Active-gen: new abstract value : ";
      TermDbSygus::toStreamSygus("sygus-active-gen", e);
      Trace("sygus-active-gen") << " -> ";
      TermDbSygus::toStreamSygus("sygus-active-gen", absE);
      Trace("sygus-active-gen") << std::endl;
    }
    d_ev_curr_active_gen = absE;
    d_evg->addValue(absE);
    firstTime = true;
  }
  bool inc = true;
  if (!firstTime)
  {
    inc = d_evg->increment();
  }
  Node v;
  if (inc)
  {
    v = d_evg->getCurrent();
  }
  Trace("sygus-active-gen-debug")
      << "...generated " << v << ", with increment success : " << inc
      << std::endl;
  if (!inc)
  {
    // No more concrete values generated from absE.
    NodeManager* nm = NodeManager::currentNM();
    d_ev_curr_active_gen = Node::null();
    std::vector<Node> exp;
    // If we are a basic enumerator, a single abstract value maps to *all*
    // concrete values of its type, thus we don't depend on the current
    // solution.
    if (!d_tds->isBasicEnumerator(e))
    {
      // We must block e = absE
      d_tds->getExplain()->getExplanationForEquality(e, absE, exp);
      for (unsigned i = 0, size = exp.size(); i < size; i++)
      {
        exp[i] = exp[i].negate();
      }
    }
    Node g = d_tds->getActiveGuardForEnumerator(e);
    if (!g.isNull())
    {
      if (d_evActiveGenFirstVal.isNull())
      {
        exp.push_back(g.negate());
        d_evActiveGenFirstVal = absE;
      }
    }
    else
    {
      Assert(false);
    }
    Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp);
    Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator "
                            "exclude current solution : "
                         << lem << std::endl;
    if (Trace.isOn("sygus-active-gen-debug"))
    {
      Trace("sygus-active-gen-debug") << "Active-gen: block ";
      TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
      Trace("sygus-active-gen-debug") << std::endl;
    }
    d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
  }
  else
  {
    // We are waiting to send e -> v to the module that requested it.
    if (v.isNull())
    {
      activeIncomplete = true;
    }
    else
    {
      d_evActiveGenWaiting = v;
    }
    if (Trace.isOn("sygus-active-gen"))
    {
      Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
      TermDbSygus::toStreamSygus("sygus-active-gen", absE);
      Trace("sygus-active-gen") << " -> ";
      TermDbSygus::toStreamSygus("sygus-active-gen", v);
      Trace("sygus-active-gen") << std::endl;
    }
  }

  return v;
}

void EnumValueManager::notifyCandidate(bool modelSuccess)
{
  d_evActiveGenWaiting = Node::null();
  // clear evaluation
  if (modelSuccess && d_eec != nullptr)
  {
    d_eec->clearEvaluationAll();
  }
}

ExampleEvalCache* EnumValueManager::getExampleEvalCache()
{
  return d_eec.get();
}

Node EnumValueManager::getModelValue(Node n)
{
  return d_treg.getModel()->getValue(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, Mathias Preiner, Haniel Barbosa
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		* Management of current value for an enumerator
14		*/
15		#include "theory/quantifiers/sygus/enum_value_manager.h"
16
17		#include "options/base_options.h"
18		#include "options/datatypes_options.h"
19		#include "options/quantifiers_options.h"
20		#include "theory/datatypes/sygus_datatype_utils.h"
21		#include "theory/quantifiers/first_order_model.h"
22		#include "theory/quantifiers/quantifiers_inference_manager.h"
23		#include "theory/quantifiers/sygus/enum_stream_substitution.h"
24		#include "theory/quantifiers/sygus/sygus_enumerator.h"
25		#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
26		#include "theory/quantifiers/sygus/term_database_sygus.h"
27		#include "theory/quantifiers/term_registry.h"
28
29		using namespace cvc5::kind;
30		using namespace std;
31
32		namespace cvc5 {
33		namespace theory {
34		namespace quantifiers {
35
36	331	EnumValueManager::EnumValueManager(Env& env,
37		QuantifiersState& qs,
38		QuantifiersInferenceManager& qim,
39		TermRegistry& tr,
40		SygusStatistics& s,
41		Node e,
42	331	bool hasExamples)
43		: EnvObj(env),
44		d_enum(e),
45		d_qstate(qs),
46		d_qim(qim),
47		d_treg(tr),
48		d_stats(s),
49	331	d_tds(tr.getTermDatabaseSygus()),
50	662	d_eec(hasExamples ? new ExampleEvalCache(d_tds, e) : nullptr)
51		{
52	331	}
53
54	662	EnumValueManager::~EnumValueManager() {}
55
56	43886	Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
57		{
58	87772	Node e = d_enum;
59	43886	bool isEnum = d_tds->isEnumerator(e);
60
61	43886	if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
62		{
63		// if the current model value of e was not registered by the datatypes
64		// sygus solver, or was excluded by symmetry breaking, then it does not
65		// have a proper model value that we should consider, thus we return null.
66	3844	Trace("sygus-engine-debug")
67	1922	<< "Enumerator " << e << " does not have proper model value."
68	1922	<< std::endl;
69	1922	return Node::null();
70		}
71
72	41964	if (!isEnum \|\| d_tds->isPassiveEnumerator(e))
73		{
74	6993	return getModelValue(e);
75		}
76
77		// management of actively generated enumerators goes here
78
79		// initialize the enumerated value generator for e
80	34971	if (d_evg == nullptr)
81		{
82	114	if (d_tds->isVariableAgnosticEnumerator(e))
83		{
84	1	d_evg.reset(new EnumStreamConcrete(d_tds));
85		}
86		else
87		{
88		// Actively-generated enumerators are currently either variable agnostic
89		// or basic. The auto mode always prefers the optimized enumerator over
90		// the basic one.
91	113	Assert(d_tds->isBasicEnumerator(e));
92	226	if (options::sygusActiveGenMode()
93	113	== options::SygusActiveGenMode::ENUM_BASIC)
94		{
95		d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType()));
96		}
97		else
98		{
99	113	Assert(options::sygusActiveGenMode()
100		== options::SygusActiveGenMode::ENUM
101		\|\| options::sygusActiveGenMode()
102		== options::SygusActiveGenMode::AUTO);
103		// create the enumerator callback
104	113	if (options::sygusSymBreakDynamic())
105		{
106	113	std::ostream* out = nullptr;
107	113	if (options::sygusRewVerify())
108		{
109	6	d_samplerRrV.reset(new SygusSampler);
110	12	d_samplerRrV->initializeSygus(
111	6	d_tds, e, options::sygusSamples(), false);
112		// use the default output for the output of sygusRewVerify
113	6	out = options().base.out;
114		}
115	226	d_secd.reset(new SygusEnumeratorCallbackDefault(
116	113	e, &d_stats, d_eec.get(), d_samplerRrV.get(), out));
117		}
118		// if sygus repair const is enabled, we enumerate terms with free
119		// variables as arguments to any-constant constructors
120	226	d_evg.reset(new SygusEnumerator(
121	113	d_tds, d_secd.get(), &d_stats, false, options::sygusRepairConst()));
122		}
123		}
124	228	Trace("sygus-active-gen")
125	114	<< "Active-gen: initialize for " << e << std::endl;
126	114	d_evg->initialize(e);
127	114	d_ev_curr_active_gen = Node::null();
128	114	Trace("sygus-active-gen-debug") << "...finish" << std::endl;
129		}
130		// if we have a waiting value, return it
131	34971	if (!d_evActiveGenWaiting.isNull())
132		{
133		Trace("sygus-active-gen-debug")
134		<< "Active-gen: return waiting " << d_evActiveGenWaiting << std::endl;
135		return d_evActiveGenWaiting;
136		}
137		// Check if there is an (abstract) value absE we were actively generating
138		// values based on.
139	69942	Node absE = d_ev_curr_active_gen;
140	34971	bool firstTime = false;
141	34971	if (absE.isNull())
142		{
143		// None currently exist. The next abstract value is the model value for e.
144	114	absE = getModelValue(e);
145	114	if (Trace.isOn("sygus-active-gen"))
146		{
147		Trace("sygus-active-gen") << "Active-gen: new abstract value : ";
148		TermDbSygus::toStreamSygus("sygus-active-gen", e);
149		Trace("sygus-active-gen") << " -> ";
150		TermDbSygus::toStreamSygus("sygus-active-gen", absE);
151		Trace("sygus-active-gen") << std::endl;
152		}
153	114	d_ev_curr_active_gen = absE;
154	114	d_evg->addValue(absE);
155	114	firstTime = true;
156		}
157	34971	bool inc = true;
158	34971	if (!firstTime)
159		{
160	34857	inc = d_evg->increment();
161		}
162	69942	Node v;
163	34971	if (inc)
164		{
165	34966	v = d_evg->getCurrent();
166		}
167	69924	Trace("sygus-active-gen-debug")
168	34962	<< "...generated " << v << ", with increment success : " << inc
169	34962	<< std::endl;
170	34962	if (!inc)
171		{
172		// No more concrete values generated from absE.
173	5	NodeManager* nm = NodeManager::currentNM();
174	5	d_ev_curr_active_gen = Node::null();
175	10	std::vector<Node> exp;
176		// If we are a basic enumerator, a single abstract value maps to all
177		// concrete values of its type, thus we don't depend on the current
178		// solution.
179	5	if (!d_tds->isBasicEnumerator(e))
180		{
181		// We must block e = absE
182	1	d_tds->getExplain()->getExplanationForEquality(e, absE, exp);
183	2	for (unsigned i = 0, size = exp.size(); i < size; i++)
184		{
185	1	exp[i] = exp[i].negate();
186		}
187		}
188	10	Node g = d_tds->getActiveGuardForEnumerator(e);
189	5	if (!g.isNull())
190		{
191	5	if (d_evActiveGenFirstVal.isNull())
192		{
193	5	exp.push_back(g.negate());
194	5	d_evActiveGenFirstVal = absE;
195		}
196		}
197		else
198		{
199		Assert(false);
200		}
201	10	Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp);
202	10	Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator "
203	5	"exclude current solution : "
204	5	<< lem << std::endl;
205	5	if (Trace.isOn("sygus-active-gen-debug"))
206		{
207		Trace("sygus-active-gen-debug") << "Active-gen: block ";
208		TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
209		Trace("sygus-active-gen-debug") << std::endl;
210		}
211	5	d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
212		}
213		else
214		{
215		// We are waiting to send e -> v to the module that requested it.
216	34957	if (v.isNull())
217		{
218	20844	activeIncomplete = true;
219		}
220		else
221		{
222	14113	d_evActiveGenWaiting = v;
223		}
224	34957	if (Trace.isOn("sygus-active-gen"))
225		{
226		Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
227		TermDbSygus::toStreamSygus("sygus-active-gen", absE);
228		Trace("sygus-active-gen") << " -> ";
229		TermDbSygus::toStreamSygus("sygus-active-gen", v);
230		Trace("sygus-active-gen") << std::endl;
231		}
232		}
233
234	34962	return v;
235		}
236
237	23675	void EnumValueManager::notifyCandidate(bool modelSuccess)
238		{
239	23675	d_evActiveGenWaiting = Node::null();
240		// clear evaluation
241	23675	if (modelSuccess && d_eec != nullptr)
242		{
243	3394	d_eec->clearEvaluationAll();
244		}
245	23675	}
246
247	18232	ExampleEvalCache* EnumValueManager::getExampleEvalCache()
248		{
249	18232	return d_eec.get();
250		}
251
252	7107	Node EnumValueManager::getModelValue(Node n)
253		{
254	7107	return d_treg.getModel()->getValue(n);
255		}
256
257		} // namespace quantifiers
258		} // namespace theory
259	29511	} // namespace cvc5