GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/solution_filter.cpp Lines: 28 45 62.2 %
Date: 2021-03-23 Branches: 48 172 27.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file solution_filter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Utilities for filtering solutions.
13
 **/
14
15
#include "theory/quantifiers/solution_filter.h"
16
17
#include <fstream>
18
#include "options/quantifiers_options.h"
19
#include "smt/smt_engine.h"
20
#include "smt/smt_engine_scope.h"
21
#include "util/random.h"
22
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
12
SolutionFilterStrength::SolutionFilterStrength() : d_isStrong(true) {}
30
4
void SolutionFilterStrength::initialize(const std::vector<Node>& vars,
31
                                        SygusSampler* ss)
32
{
33
4
  ExprMiner::initialize(vars, ss);
34
4
}
35
36
4
void SolutionFilterStrength::setLogicallyStrong(bool isStrong)
37
{
38
4
  d_isStrong = isStrong;
39
4
}
40
41
112
bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
42
{
43
112
  if (!n.getType().isBoolean())
44
  {
45
    // currently, should not register non-Boolean terms here
46
    Assert(false);
47
    return true;
48
  }
49
224
  Node basen = d_isStrong ? n : n.negate();
50
112
  NodeManager* nm = NodeManager::currentNM();
51
  // Do i subsume the disjunction of all previous solutions? If so, we discard
52
  // this immediately
53
224
  Node curr;
54
112
  if (!d_curr_sols.empty())
55
  {
56
216
    curr = d_curr_sols.size() == 1
57
320
               ? d_curr_sols[0]
58
104
               : nm->mkNode(d_isStrong ? OR : AND, d_curr_sols);
59
146
    Node imp = nm->mkNode(AND, basen.negate(), curr);
60
216
    Trace("sygus-sol-implied")
61
108
        << "  implies: check subsumed (strong=" << d_isStrong << ") " << imp
62
108
        << "..." << std::endl;
63
    // check the satisfiability query
64
146
    Result r = doCheck(imp);
65
108
    Trace("sygus-sol-implied") << "  implies: ...got : " << r << std::endl;
66
108
    if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
67
    {
68
      // it is subsumed by the current, discard this
69
70
      return false;
70
    }
71
  }
72
  // check which solutions would have been filtered if the current had come
73
  // first
74
84
  if (options::sygusFilterSolRevSubsume())
75
  {
76
    std::vector<Node> nsubsume;
77
    for (const Node& s : d_curr_sols)
78
    {
79
      Node imp = nm->mkNode(AND, s.negate(), basen);
80
      Trace("sygus-sol-implied")
81
          << "  implies: check subsuming " << imp << "..." << std::endl;
82
      // check the satisfiability query
83
      Result r = doCheck(imp);
84
      Trace("sygus-sol-implied") << "  implies: ...got : " << r << std::endl;
85
      if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
86
      {
87
        nsubsume.push_back(s);
88
      }
89
      else
90
      {
91
        Options& opts = smt::currentSmtEngine()->getOptions();
92
        std::ostream* smtOut = opts.getOut();
93
        (*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")"
94
                  << std::endl;
95
      }
96
    }
97
    d_curr_sols.clear();
98
    d_curr_sols.insert(d_curr_sols.end(), nsubsume.begin(), nsubsume.end());
99
  }
100
42
  d_curr_sols.push_back(basen);
101
42
  return true;
102
}
103
104
}  // namespace quantifiers
105
}  // namespace theory
106
26727
}  // namespace CVC4