src/smt/assertions.cpp

   1 /*********************                                                        */
   2 /*! \file assertions.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 The module for storing assertions for an SMT engine.
  13  **/
  14
  15 #include "smt/assertions.h"
  16
  17 #include "expr/node_algorithm.h"
  18 #include "options/base_options.h"
  19 #include "options/language.h"
  20 #include "options/smt_options.h"
  21 #include "proof/proof_manager.h"
  22 #include "smt/smt_engine.h"
  23
  24 using namespace CVC4::theory;
  25 using namespace CVC4::kind;
  26
  27 namespace CVC4 {
  28 namespace smt {
  29
  30 Assertions::Assertions(context::UserContext* u, AbstractValues& absv)
  31     : d_userContext(u),
  32       d_absValues(absv),
  33       d_assertionList(nullptr),
  34       d_globalNegation(false),
  35       d_assertions()
  36 {
  37 }
  38
  39 Assertions::~Assertions()
  40 {
  41   if (d_assertionList != nullptr)
  42   {
  43     d_assertionList->deleteSelf();
  44   }
  45 }
  46
  47 void Assertions::finishInit()
  48 {
  49   // [MGD 10/20/2011] keep around in incremental mode, due to a
  50   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
  51   // first, some user-context-dependent TNodes might still exist
  52   // with rc == 0.
  53   if (options::produceAssertions() || options::incrementalSolving())
  54   {
  55     // In the case of incremental solving, we appear to need these to
  56     // ensure the relevant Nodes remain live.
  57     d_assertionList = new (true) AssertionList(d_userContext);
  58     d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
  59   }
  60 }
  61
  62 void Assertions::clearCurrent()
  63 {
  64   d_assertions.clear();
  65   d_assertions.getIteSkolemMap().clear();
  66 }
  67
  68 void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
  69                                     bool inUnsatCore,
  70                                     bool isEntailmentCheck)
  71 {
  72   NodeManager* nm = NodeManager::currentNM();
  73   // reset global negation
  74   d_globalNegation = false;
  75   // clear the assumptions
  76   d_assumptions.clear();
  77   if (isEntailmentCheck)
  78   {
  79     size_t size = assumptions.size();
  80     if (size > 1)
  81     {
  82       /* Assume: not (BIGAND assumptions)  */
  83       d_assumptions.push_back(nm->mkNode(AND, assumptions).notNode());
  84     }
  85     else if (size == 1)
  86     {
  87       /* Assume: not expr  */
  88       d_assumptions.push_back(assumptions[0].notNode());
  89     }
  90   }
  91   else
  92   {
  93     /* Assume: BIGAND assumptions  */
  94     d_assumptions = assumptions;
  95   }
  96
  97   Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
  98   for (const Node& e : d_assumptions)
  99   {
 100     // Substitute out any abstract values in ex.
 101     Node n = d_absValues.substituteAbstractValues(e);
 102     // Ensure expr is type-checked at this point.
 103     ensureBoolean(n);
 104     addFormula(n, inUnsatCore, true, true, false);
 105   }
 106   if (d_globalDefineFunRecLemmas != nullptr)
 107   {
 108     // Global definitions are asserted at check-sat-time because we have to
 109     // make sure that they are always present (they are essentially level
 110     // zero assertions)
 111     for (const Node& lemma : *d_globalDefineFunRecLemmas)
 112     {
 113       addFormula(lemma, false, true, false, false);
 114     }
 115   }
 116 }
 117
 118 void Assertions::assertFormula(const Node& n, bool inUnsatCore)
 119 {
 120   ensureBoolean(n);
 121   bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
 122   addFormula(n, inUnsatCore, true, false, maybeHasFv);
 123 }
 124
 125 std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
 126 bool Assertions::isGlobalNegated() const { return d_globalNegation; }
 127 void Assertions::flipGlobalNegated() { d_globalNegation = !d_globalNegation; }
 128
 129 preprocessing::AssertionPipeline& Assertions::getAssertionPipeline()
 130 {
 131   return d_assertions;
 132 }
 133
 134 context::CDList<Node>* Assertions::getAssertionList()
 135 {
 136   return d_assertionList;
 137 }
 138
 139 void Assertions::addFormula(
 140     TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
 141 {
 142   // add to assertion list if it exists
 143   if (d_assertionList != nullptr)
 144   {
 145     d_assertionList->push_back(n);
 146   }
 147   if (n.isConst() && n.getConst<bool>())
 148   {
 149     // true, nothing to do
 150     return;
 151   }
 152
 153   Trace("smt") << "SmtEnginePrivate::addFormula(" << n
 154                << "), inUnsatCore = " << inUnsatCore
 155                << ", inInput = " << inInput
 156                << ", isAssumption = " << isAssumption << std::endl;
 157
 158   // Ensure that it does not contain free variables
 159   if (maybeHasFv)
 160   {
 161     if (expr::hasFreeVar(n))
 162     {
 163       std::stringstream se;
 164       se << "Cannot process assertion with free variable.";
 165       if (language::isInputLangSygus(options::inputLanguage()))
 166       {
 167         // Common misuse of SyGuS is to use top-level assert instead of
 168         // constraint when defining the synthesis conjecture.
 169         se << " Perhaps you meant `constraint` instead of `assert`?";
 170       }
 171       throw ModalException(se.str().c_str());
 172     }
 173   }
 174
 175   // Give it to proof manager
 176   if (options::unsatCores())
 177   {
 178     if (inInput)
 179     {  // n is an input assertion
 180       if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores()
 181           || options::checkUnsatCores())
 182       {
 183         ProofManager::currentPM()->addCoreAssertion(n.toExpr());
 184       }
 185     }
 186     else
 187     {
 188       // n is the result of an unknown preprocessing step, add it to dependency
 189       // map to null
 190       ProofManager::currentPM()->addDependence(n, Node::null());
 191     }
 192   }
 193
 194   // Add the normalized formula to the queue
 195   d_assertions.push_back(n, isAssumption, true);
 196 }
 197
 198 void Assertions::addDefineFunRecDefinition(Node n, bool global)
 199 {
 200   n = d_absValues.substituteAbstractValues(n);
 201   if (d_assertionList != nullptr)
 202   {
 203     d_assertionList->push_back(n);
 204   }
 205   if (global && d_globalDefineFunRecLemmas != nullptr)
 206   {
 207     // Global definitions are asserted at check-sat-time because we have to
 208     // make sure that they are always present
 209     Assert(!language::isInputLangSygus(options::inputLanguage()));
 210     d_globalDefineFunRecLemmas->emplace_back(n);
 211   }
 212   else
 213   {
 214     bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
 215     addFormula(n, false, true, false, maybeHasFv);
 216   }
 217 }
 218
 219 void Assertions::ensureBoolean(const Node& n)
 220 {
 221   TypeNode type = n.getType(options::typeChecking());
 222   if (!type.isBoolean())
 223   {
 224     std::stringstream ss;
 225     ss << "Expected Boolean type\n"
 226        << "The assertion : " << n << "\n"
 227        << "Its type      : " << type;
 228     throw TypeCheckingException(n.toExpr(), ss.str());
 229   }
 230 }
 231
 232 void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
 233 {
 234   d_assertions.setProofGenerator(pppg);
 235 }
 236
 237 bool Assertions::isProofEnabled() const
 238 {
 239   return d_assertions.isProofEnabled();
 240 }
 241
 242 }  // namespace smt
 243 }  // namespace CVC4