Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/model_manager.cpp	Lines:	68	73	93.2 %
Date:	2021-08-19	Branches:	82	184	44.6 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * 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.
 * ****************************************************************************
 *
 * Abstract management of models for TheoryEngine.
 */

#include "theory/model_manager.h"

#include "options/smt_options.h"
#include "options/theory_options.h"
#include "prop/prop_engine.h"
#include "smt/env.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_builder.h"
#include "theory/quantifiers_engine.h"
#include "theory/theory_engine.h"

namespace cvc5 {
namespace theory {

ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem)
    : d_te(te),
      d_env(env),
      d_eem(eem),
      d_modelEqualityEngine(nullptr),
      d_modelEqualityEngineAlloc(nullptr),
      d_model(new TheoryModel(
          env, "DefaultModel", options::assignFunctionValues())),
      d_modelBuilder(nullptr),
      d_modelBuilt(false),
      d_modelBuiltSuccess(false)
{
}

ModelManager::~ModelManager() {}

void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
{
  // construct the model
  const LogicInfo& logicInfo = d_env.getLogicInfo();
  // Initialize the model and model builder.
  if (logicInfo.isQuantified())
  {
    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
    Assert(qe != nullptr);
    d_modelBuilder = qe->getModelBuilder();
  }

  // make the default builder, e.g. in the case that the quantifiers engine does
  // not have a model builder
  if (d_modelBuilder == nullptr)
  {
    d_alocModelBuilder.reset(new TheoryEngineModelBuilder);
    d_modelBuilder = d_alocModelBuilder.get();
  }
  // notice that the equality engine of the model has yet to be assigned.
  initializeModelEqEngine(notify);
}

void ModelManager::resetModel()
{
  d_modelBuilt = false;
  d_modelBuiltSuccess = false;
  // Reset basic information on the model object
  d_model->reset();
}

bool ModelManager::buildModel()
{
  if (d_modelBuilt)
  {
    // already computed
    return d_modelBuiltSuccess;
  }
  // reset the flags now
  d_modelBuilt = true;
  d_modelBuiltSuccess = false;

  // prepare the model, which is specific to the manager
  if (!prepareModel())
  {
    Trace("model-builder") << "ModelManager: fail prepare model" << std::endl;
    return false;
  }

  // now, finish building the model
  d_modelBuiltSuccess = finishBuildModel();

  if (Trace.isOn("model-final"))
  {
    Trace("model-final") << "Final model:" << std::endl;
    Trace("model-final") << d_model->debugPrintModelEqc() << std::endl;
  }

  Trace("model-builder") << "ModelManager: model built success is "
                         << d_modelBuiltSuccess << std::endl;

  return d_modelBuiltSuccess;
}

bool ModelManager::isModelBuilt() const { return d_modelBuilt; }

void ModelManager::postProcessModel(bool incomplete)
{
  if (!d_modelBuilt)
  {
    // model not built, nothing to do
    return;
  }
  Trace("model-builder") << "ModelManager: post-process model..." << std::endl;
  // model construction should always succeed unless lemmas were added
  AlwaysAssert(d_modelBuiltSuccess);
  if (!options::produceModels())
  {
    return;
  }
  // Do post-processing of model from the theories (used for THEORY_SEP
  // to construct heap model)
  for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
       ++theoryId)
  {
    Theory* t = d_te.theoryOf(theoryId);
    if (t == nullptr)
    {
      // theory not active, skip
      continue;
    }
    Trace("model-builder-debug")
        << "  PostProcessModel on theory: " << theoryId << std::endl;
    t->postProcessModel(d_model.get());
  }
  // also call the model builder's post-process model
  d_modelBuilder->postProcessModel(incomplete, d_model.get());
}

theory::TheoryModel* ModelManager::getModel() { return d_model.get(); }

bool ModelManager::collectModelBooleanVariables()
{
  Trace("model-builder") << "  CollectModelInfo boolean variables" << std::endl;
  // Get value of the Boolean variables
  prop::PropEngine* propEngine = d_te.getPropEngine();
  std::vector<TNode> boolVars;
  propEngine->getBooleanVariables(boolVars);
  std::vector<TNode>::iterator it, iend = boolVars.end();
  bool hasValue, value;
  for (it = boolVars.begin(); it != iend; ++it)
  {
    TNode var = *it;
    hasValue = propEngine->hasValue(var, value);
    // Should we assert that hasValue is true?
    if (!hasValue)
    {
      Trace("model-builder-assertions")
          << "    has no value : " << var << std::endl;
      value = false;
    }
    Trace("model-builder-assertions")
        << "(assert" << (value ? " " : " (not ") << var
        << (value ? ");" : "));") << std::endl;
    if (!d_model->assertPredicate(var, value))
    {
      return false;
    }
  }
  return true;
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds
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		* Abstract management of models for TheoryEngine.
14		*/
15
16		#include "theory/model_manager.h"
17
18		#include "options/smt_options.h"
19		#include "options/theory_options.h"
20		#include "prop/prop_engine.h"
21		#include "smt/env.h"
22		#include "theory/quantifiers/first_order_model.h"
23		#include "theory/quantifiers/fmf/model_builder.h"
24		#include "theory/quantifiers_engine.h"
25		#include "theory/theory_engine.h"
26
27		namespace cvc5 {
28		namespace theory {
29
30	9854	ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem)
31		: d_te(te),
32		d_env(env),
33		d_eem(eem),
34		d_modelEqualityEngine(nullptr),
35		d_modelEqualityEngineAlloc(nullptr),
36		d_model(new TheoryModel(
37	9854	env, "DefaultModel", options::assignFunctionValues())),
38		d_modelBuilder(nullptr),
39		d_modelBuilt(false),
40	19708	d_modelBuiltSuccess(false)
41		{
42	9854	}
43
44	9854	ModelManager::~ModelManager() {}
45
46	9854	void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
47		{
48		// construct the model
49	9854	const LogicInfo& logicInfo = d_env.getLogicInfo();
50		// Initialize the model and model builder.
51	9854	if (logicInfo.isQuantified())
52		{
53	6766	QuantifiersEngine* qe = d_te.getQuantifiersEngine();
54	6766	Assert(qe != nullptr);
55	6766	d_modelBuilder = qe->getModelBuilder();
56		}
57
58		// make the default builder, e.g. in the case that the quantifiers engine does
59		// not have a model builder
60	9854	if (d_modelBuilder == nullptr)
61		{
62	3088	d_alocModelBuilder.reset(new TheoryEngineModelBuilder);
63	3088	d_modelBuilder = d_alocModelBuilder.get();
64		}
65		// notice that the equality engine of the model has yet to be assigned.
66	9854	initializeModelEqEngine(notify);
67	9854	}
68
69	21068	void ModelManager::resetModel()
70		{
71	21068	d_modelBuilt = false;
72	21068	d_modelBuiltSuccess = false;
73		// Reset basic information on the model object
74	21068	d_model->reset();
75	21068	}
76
77	25431	bool ModelManager::buildModel()
78		{
79	25431	if (d_modelBuilt)
80		{
81		// already computed
82	8941	return d_modelBuiltSuccess;
83		}
84		// reset the flags now
85	16490	d_modelBuilt = true;
86	16490	d_modelBuiltSuccess = false;
87
88		// prepare the model, which is specific to the manager
89	16490	if (!prepareModel())
90		{
91	2	Trace("model-builder") << "ModelManager: fail prepare model" << std::endl;
92	2	return false;
93		}
94
95		// now, finish building the model
96	16487	d_modelBuiltSuccess = finishBuildModel();
97
98	16487	if (Trace.isOn("model-final"))
99		{
100		Trace("model-final") << "Final model:" << std::endl;
101		Trace("model-final") << d_model->debugPrintModelEqc() << std::endl;
102		}
103
104	32974	Trace("model-builder") << "ModelManager: model built success is "
105	16487	<< d_modelBuiltSuccess << std::endl;
106
107	16487	return d_modelBuiltSuccess;
108		}
109
110		bool ModelManager::isModelBuilt() const { return d_modelBuilt; }
111
112	7482	void ModelManager::postProcessModel(bool incomplete)
113		{
114	7482	if (!d_modelBuilt)
115		{
116		// model not built, nothing to do
117	6494	return;
118		}
119	988	Trace("model-builder") << "ModelManager: post-process model..." << std::endl;
120		// model construction should always succeed unless lemmas were added
121	988	AlwaysAssert(d_modelBuiltSuccess);
122	988	if (!options::produceModels())
123		{
124	378	return;
125		}
126		// Do post-processing of model from the theories (used for THEORY_SEP
127		// to construct heap model)
128	8540	for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
129		++theoryId)
130		{
131	7930	Theory* t = d_te.theoryOf(theoryId);
132	7930	if (t == nullptr)
133		{
134		// theory not active, skip
135		continue;
136		}
137	15860	Trace("model-builder-debug")
138	7930	<< " PostProcessModel on theory: " << theoryId << std::endl;
139	7930	t->postProcessModel(d_model.get());
140		}
141		// also call the model builder's post-process model
142	610	d_modelBuilder->postProcessModel(incomplete, d_model.get());
143		}
144
145	3117750	theory::TheoryModel* ModelManager::getModel() { return d_model.get(); }
146
147	16487	bool ModelManager::collectModelBooleanVariables()
148		{
149	16487	Trace("model-builder") << " CollectModelInfo boolean variables" << std::endl;
150		// Get value of the Boolean variables
151	16487	prop::PropEngine* propEngine = d_te.getPropEngine();
152	32974	std::vector<TNode> boolVars;
153	16487	propEngine->getBooleanVariables(boolVars);
154	16487	std::vector<TNode>::iterator it, iend = boolVars.end();
155		bool hasValue, value;
156	87578	for (it = boolVars.begin(); it != iend; ++it)
157		{
158	142182	TNode var = *it;
159	71091	hasValue = propEngine->hasValue(var, value);
160		// Should we assert that hasValue is true?
161	71091	if (!hasValue)
162		{
163	23932	Trace("model-builder-assertions")
164	11966	<< " has no value : " << var << std::endl;
165	11966	value = false;
166		}
167	142182	Trace("model-builder-assertions")
168	142182	<< "(assert" << (value ? " " : " (not ") << var
169	71091	<< (value ? ");" : "));") << std::endl;
170	71091	if (!d_model->assertPredicate(var, value))
171		{
172		return false;
173		}
174		}
175	16487	return true;
176		}
177
178		} // namespace theory
179	29349	} // namespace cvc5