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-2019 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
SolutionFilterStrength()29 SolutionFilterStrength::SolutionFilterStrength() : d_isStrong(true) {}
initialize(const std::vector<Node> & vars,SygusSampler * ss)30 void SolutionFilterStrength::initialize(const std::vector<Node>& vars,
31 SygusSampler* ss)
32 {
33 ExprMiner::initialize(vars, ss);
34 }
35
setLogicallyStrong(bool isStrong)36 void SolutionFilterStrength::setLogicallyStrong(bool isStrong)
37 {
38 d_isStrong = isStrong;
39 }
40
addTerm(Node n,std::ostream & out)41 bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
42 {
43 if (!n.getType().isBoolean())
44 {
45 // currently, should not register non-Boolean terms here
46 Assert(false);
47 return true;
48 }
49 Node basen = d_isStrong ? n : n.negate();
50 NodeManager* nm = NodeManager::currentNM();
51 // Do i subsume the disjunction of all previous solutions? If so, we discard
52 // this immediately
53 Node curr;
54 if (!d_curr_sols.empty())
55 {
56 curr = d_curr_sols.size() == 1
57 ? d_curr_sols[0]
58 : nm->mkNode(d_isStrong ? AND : OR, d_curr_sols);
59 Node imp = nm->mkNode(AND, basen.negate(), curr);
60 Trace("sygus-sol-implied")
61 << " implies: check subsumed " << imp << "..." << std::endl;
62 // check the satisfiability query
63 Result r = doCheck(imp);
64 Trace("sygus-sol-implied") << " implies: ...got : " << r << std::endl;
65 if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
66 {
67 // it is subsumed by the current, discard this
68 return false;
69 }
70 }
71 // check which solutions would have been filtered if the current had come
72 // first
73 if (options::sygusFilterSolRevSubsume())
74 {
75 std::vector<Node> nsubsume;
76 for (const Node& s : d_curr_sols)
77 {
78 Node imp = nm->mkNode(AND, s.negate(), basen);
79 Trace("sygus-sol-implied")
80 << " implies: check subsuming " << imp << "..." << std::endl;
81 // check the satisfiability query
82 Result r = doCheck(imp);
83 Trace("sygus-sol-implied") << " implies: ...got : " << r << std::endl;
84 if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
85 {
86 nsubsume.push_back(s);
87 }
88 else
89 {
90 Options& nodeManagerOptions = nm->getOptions();
91 std::ostream* out = nodeManagerOptions.getOut();
92 (*out) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")"
93 << std::endl;
94 }
95 }
96 d_curr_sols.clear();
97 d_curr_sols.insert(d_curr_sols.end(), nsubsume.begin(), nsubsume.end());
98 }
99 d_curr_sols.push_back(basen);
100 return true;
101 }
102
103 } // namespace quantifiers
104 } // namespace theory
105 } // namespace CVC4
106