/******************************************************************************

 * Top contributors (to current version):

 *   Andrew Reynolds, Morgan Deters, Andres Noetzli

 *

 * 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.

 * ****************************************************************************

 *

 * Utility for constructing and maintaining abstract values.

 */

#include "smt/check_models.h"

#include "base/modal_exception.h"

#include "options/smt_options.h"

#include "smt/env.h"

#include "smt/node_command.h"

#include "smt/preprocessor.h"

#include "smt/smt_solver.h"

#include "theory/rewriter.h"

#include "theory/substitutions.h"

#include "theory/theory_engine.h"

#include "theory/theory_model.h"

using namespace cvc5::theory;

namespace cvc5 {

namespace smt {

                             context::CDList<Node>* al,

                             bool hardFailure)

{

  // Throughout, we use Notice() to give diagnostic output.

  //

  // If this function is running, the user gave --check-model (or equivalent),

  // and if Notice() is on, the user gave --verbose (or equivalent).

  // check-model is not guaranteed to succeed if approximate values were used.

  // Thus, we intentionally abort here.

  {

    throw RecoverableModalException(

  }

  // the list of assertions that did not rewrite to true

  // Now go through all our user assertions checking if they're satisfied.

  {

    // Apply any define-funs from the problem. We do not expand theory symbols

    // like integer division here. Hence, the code below is not able to properly

    // evaluate e.g. divide-by-zero. This is intentional since the evaluation

    // is not trustworthy, since the UF introduced by expanding definitions may

    // not be properly constrained.

    // We look up the value before simplifying. If n contains quantifiers,

    // this may increases the chance of finding its value before the node is

    // altered by simplification below.

    {

      // assertion is true, everything is fine

    }

    // Otherwise, we did not succeed in showing the current assertion to be

    // true. This may either indicate that our model is wrong, or that we cannot

    // check it. The latter may be the case for several reasons.

    // One example is the occurrence of partial operators. Another example

    // are quantified formulas, which are not checkable, although we assign

    // them to true/false based on the satisfying assignment. However,

    // quantified formulas can be modified during preprocess, so they may not

    // correspond to those in the satisfying assignment. Hence we throw

    // warnings for assertions that do not simplify to either true or false.

    // Other theories such as non-linear arithmetic (in particular,

    // transcendental functions) also have the property of not being able to

    // be checked precisely here.

    // Note that warnings like these can be avoided for quantified formulas

    // by making preprocessing passes explicitly record how they

    // rewrite quantified formulas (see cvc4-wishues#43).

    {

      // Not constant, print a less severe warning message here.

    }

    // Assertions that simplify to false result in an InternalError or

    // Warning being thrown below (when hardFailure is false).

    ss << "SmtEngine::checkModel(): "

    {

      // internal error if hardFailure is true

    }

    else

    {

    }

  }

  {

  }

  // if the noCheckList is non-empty, we could expand definitions on this list

  // and check satisfiability

}

}  // namespace smt