Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/query_generator_unsat.cpp	Lines:	86	89	96.6 %
Date:	2021-11-05	Branches:	136	348	39.1 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * A class for mining interesting unsat queries from a stream of generated
 * expressions.
 */

#include "theory/quantifiers/query_generator_unsat.h"

#include "options/smt_options.h"
#include "smt/env.h"
#include "util/random.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

QueryGeneratorUnsat::QueryGeneratorUnsat(Env& env)
    : ExprMiner(env), d_queryCount(0)
{
  d_true = NodeManager::currentNM()->mkConst(true);
  d_false = NodeManager::currentNM()->mkConst(false);
  // determine the options to use for the verification subsolvers we spawn
  // we start with the provided options
  d_subOptions.copyValues(d_env.getOriginalOptions());
  d_subOptions.smt.produceProofs = true;
  d_subOptions.smt.checkProofs = true;
  d_subOptions.smt.produceModels = true;
  d_subOptions.smt.checkModels = true;
}

void QueryGeneratorUnsat::initialize(const std::vector<Node>& vars,
                                     SygusSampler* ss)
{
  Assert(ss != nullptr);
  d_queryCount = 0;
  ExprMiner::initialize(vars, ss);
}

bool QueryGeneratorUnsat::addTerm(Node n, std::ostream& out)
{
  d_terms.push_back(n);
  Trace("sygus-qgen") << "Add term: " << n << std::endl;
  Assert(n.getType().isBoolean());

  // the loop below conjoins a random subset of predicates we have enumerated
  // so far C1 ^ ... ^ Cn such that no subset of C1 ... Cn is an unsat core
  // we have encountered so far, and each appended Ci is false on a model for
  // C1 ^ ... ^ C_{i-1}.
  std::vector<Node> currModel;
  std::unordered_set<size_t> processed;
  std::vector<Node> activeTerms;
  // always start with the new term
  processed.insert(d_terms.size() - 1);
  activeTerms.push_back(n);
  bool addSuccess = true;
  size_t checkCount = 0;
  while (checkCount < 10)
  {
    Assert(!activeTerms.empty());
    // if we just successfully added a term, do a satisfiability check
    if (addSuccess)
    {
      checkCount++;
      // check the current for satisfiability
      currModel.clear();
      // Shuffle active terms to maximize the different possible behaviors
      // in the subsolver. This is instead of making multiple queries with
      // the same assertion order for a subsequence.
      std::shuffle(activeTerms.begin(), activeTerms.end(), Random::getRandom());
      Result r = checkCurrent(activeTerms, out, currModel);
      if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
      {
        // exclude the last active term
        activeTerms.pop_back();
      }
    }
    if (processed.size() == d_terms.size())
    {
      break;
    }
    // activeTerms is satisfiable, add a new term
    size_t rindex = getNextRandomIndex(processed);
    Assert(rindex < d_terms.size());
    processed.insert(rindex);
    Node nextTerm = d_terms[rindex];
    // immediately check if is satisfied by the current model using the
    // evaluator, if so, don't conjoin the term.
    Node newTermEval;
    if (!currModel.empty())
    {
      Node nextTermSk = convertToSkolem(nextTerm);
      newTermEval = evaluate(nextTermSk, d_skolems, currModel);
    }
    if (newTermEval == d_true)
    {
      Trace("sygus-qgen-check-debug")
          << "...already satisfied " << convertToSkolem(nextTerm)
          << " for model " << d_skolems << " " << currModel << std::endl;
      addSuccess = false;
    }
    else
    {
      Trace("sygus-qgen-check-debug")
          << "...not satisfied " << convertToSkolem(nextTerm) << " for model "
          << d_skolems << " " << currModel << std::endl;
      activeTerms.push_back(nextTerm);
      addSuccess = !d_cores.hasSubset(activeTerms);
      if (!addSuccess)
      {
        Trace("sygus-qgen-check-debug")
            << "...already has unsat core " << nextTerm << std::endl;
        activeTerms.pop_back();
      }
    }
  }

  return true;
}

Result QueryGeneratorUnsat::checkCurrent(const std::vector<Node>& activeTerms,
                                         std::ostream& out,
                                         std::vector<Node>& currModel)
{
  NodeManager* nm = NodeManager::currentNM();
  Node qy = nm->mkAnd(activeTerms);
  Trace("sygus-qgen-check") << "Check: " << qy << std::endl;
  out << "(query " << qy << ")" << std::endl;
  std::unique_ptr<SolverEngine> queryChecker;
  initializeChecker(queryChecker, qy, d_subOptions, logicInfo());
  Result r = queryChecker->checkSat();
  Trace("sygus-qgen-check") << "..finished check got " << r << std::endl;
  if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
  {
    // if unsat, get the unsat core
    std::vector<Node> unsatCore;
    getUnsatCoreFromSubsolver(*queryChecker.get(), unsatCore);
    Assert(!unsatCore.empty());
    Trace("sygus-qgen-check") << "...unsat core: " << unsatCore << std::endl;
    d_cores.add(d_false, unsatCore);
  }
  else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
  {
    getModelFromSubsolver(*queryChecker.get(), d_skolems, currModel);
    Trace("sygus-qgen-check") << "...model: " << currModel << std::endl;
  }
  return r;
}

size_t QueryGeneratorUnsat::getNextRandomIndex(
    const std::unordered_set<size_t>& processed) const
{
  Assert(!d_terms.empty());
  Assert(processed.size() < d_terms.size());
  size_t rindex = Random::getRandom().pick(0, d_terms.size() - 1);
  while (processed.find(rindex) != processed.end())
  {
    rindex++;
    if (rindex == d_terms.size())
    {
      rindex = 0;
    }
  }
  return rindex;
}

}  // 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
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		* A class for mining interesting unsat queries from a stream of generated
14		* expressions.
15		*/
16
17		#include "theory/quantifiers/query_generator_unsat.h"
18
19		#include "options/smt_options.h"
20		#include "smt/env.h"
21		#include "util/random.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace quantifiers {
26
27	2	QueryGeneratorUnsat::QueryGeneratorUnsat(Env& env)
28	2	: ExprMiner(env), d_queryCount(0)
29		{
30	2	d_true = NodeManager::currentNM()->mkConst(true);
31	2	d_false = NodeManager::currentNM()->mkConst(false);
32		// determine the options to use for the verification subsolvers we spawn
33		// we start with the provided options
34	2	d_subOptions.copyValues(d_env.getOriginalOptions());
35	2	d_subOptions.smt.produceProofs = true;
36	2	d_subOptions.smt.checkProofs = true;
37	2	d_subOptions.smt.produceModels = true;
38	2	d_subOptions.smt.checkModels = true;
39	2	}
40
41	2	void QueryGeneratorUnsat::initialize(const std::vector<Node>& vars,
42		SygusSampler* ss)
43		{
44	2	Assert(ss != nullptr);
45	2	d_queryCount = 0;
46	2	ExprMiner::initialize(vars, ss);
47	2	}
48
49	418	bool QueryGeneratorUnsat::addTerm(Node n, std::ostream& out)
50		{
51	418	d_terms.push_back(n);
52	418	Trace("sygus-qgen") << "Add term: " << n << std::endl;
53	418	Assert(n.getType().isBoolean());
54
55		// the loop below conjoins a random subset of predicates we have enumerated
56		// so far C1 ^ ... ^ Cn such that no subset of C1 ... Cn is an unsat core
57		// we have encountered so far, and each appended Ci is false on a model for
58		// C1 ^ ... ^ C_{i-1}.
59	836	std::vector<Node> currModel;
60	836	std::unordered_set<size_t> processed;
61	836	std::vector<Node> activeTerms;
62		// always start with the new term
63	418	processed.insert(d_terms.size() - 1);
64	418	activeTerms.push_back(n);
65	418	bool addSuccess = true;
66	418	size_t checkCount = 0;
67	14742	while (checkCount < 10)
68		{
69	7196	Assert(!activeTerms.empty());
70		// if we just successfully added a term, do a satisfiability check
71	7196	if (addSuccess)
72		{
73	4042	checkCount++;
74		// check the current for satisfiability
75	4042	currModel.clear();
76		// Shuffle active terms to maximize the different possible behaviors
77		// in the subsolver. This is instead of making multiple queries with
78		// the same assertion order for a subsequence.
79	4042	std::shuffle(activeTerms.begin(), activeTerms.end(), Random::getRandom());
80	8084	Result r = checkCurrent(activeTerms, out, currModel);
81	4042	if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
82		{
83		// exclude the last active term
84	2380	activeTerms.pop_back();
85		}
86		}
87	7196	if (processed.size() == d_terms.size())
88		{
89	34	break;
90		}
91		// activeTerms is satisfiable, add a new term
92	7162	size_t rindex = getNextRandomIndex(processed);
93	7162	Assert(rindex < d_terms.size());
94	7162	processed.insert(rindex);
95	14324	Node nextTerm = d_terms[rindex];
96		// immediately check if is satisfied by the current model using the
97		// evaluator, if so, don't conjoin the term.
98	14324	Node newTermEval;
99	7162	if (!currModel.empty())
100		{
101	9592	Node nextTermSk = convertToSkolem(nextTerm);
102	4796	newTermEval = evaluate(nextTermSk, d_skolems, currModel);
103		}
104	7162	if (newTermEval == d_true)
105		{
106	6360	Trace("sygus-qgen-check-debug")
107	6360	<< "...already satisfied " << convertToSkolem(nextTerm)
108	3180	<< " for model " << d_skolems << " " << currModel << std::endl;
109	3180	addSuccess = false;
110		}
111		else
112		{
113	7964	Trace("sygus-qgen-check-debug")
114	7964	<< "...not satisfied " << convertToSkolem(nextTerm) << " for model "
115	3982	<< d_skolems << " " << currModel << std::endl;
116	3982	activeTerms.push_back(nextTerm);
117	3982	addSuccess = !d_cores.hasSubset(activeTerms);
118	3982	if (!addSuccess)
119		{
120		Trace("sygus-qgen-check-debug")
121		<< "...already has unsat core " << nextTerm << std::endl;
122		activeTerms.pop_back();
123		}
124		}
125		}
126
127	836	return true;
128		}
129
130	4042	Result QueryGeneratorUnsat::checkCurrent(const std::vector<Node>& activeTerms,
131		std::ostream& out,
132		std::vector<Node>& currModel)
133		{
134	4042	NodeManager* nm = NodeManager::currentNM();
135	8084	Node qy = nm->mkAnd(activeTerms);
136	4042	Trace("sygus-qgen-check") << "Check: " << qy << std::endl;
137	4042	out << "(query " << qy << ")" << std::endl;
138	8084	std::unique_ptr<SolverEngine> queryChecker;
139	4042	initializeChecker(queryChecker, qy, d_subOptions, logicInfo());
140	4042	Result r = queryChecker->checkSat();
141	4042	Trace("sygus-qgen-check") << "..finished check got " << r << std::endl;
142	4042	if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
143		{
144		// if unsat, get the unsat core
145	4760	std::vector<Node> unsatCore;
146	2380	getUnsatCoreFromSubsolver(*queryChecker.get(), unsatCore);
147	2380	Assert(!unsatCore.empty());
148	2380	Trace("sygus-qgen-check") << "...unsat core: " << unsatCore << std::endl;
149	2380	d_cores.add(d_false, unsatCore);
150		}
151	1662	else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
152		{
153	1662	getModelFromSubsolver(*queryChecker.get(), d_skolems, currModel);
154	1662	Trace("sygus-qgen-check") << "...model: " << currModel << std::endl;
155		}
156	8084	return r;
157		}
158
159	7162	size_t QueryGeneratorUnsat::getNextRandomIndex(
160		const std::unordered_set<size_t>& processed) const
161		{
162	7162	Assert(!d_terms.empty());
163	7162	Assert(processed.size() < d_terms.size());
164	7162	size_t rindex = Random::getRandom().pick(0, d_terms.size() - 1);
165	54430	while (processed.find(rindex) != processed.end())
166		{
167	23634	rindex++;
168	23634	if (rindex == d_terms.size())
169		{
170	334	rindex = 0;
171		}
172		}
173	7162	return rindex;
174		}
175
176		} // namespace quantifiers
177		} // namespace theory
178	31125	} // namespace cvc5