-/********************* */
-/*! \file expr_miner.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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.\endverbatim
- **
- ** \brief Implementation of expr_miner
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Andres Noetzli, Aina Niemetz
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of expr_miner.
+ */
#include "theory/quantifiers/expr_miner.h"
-#include "api/cvc4cpp.h"
+#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/smt_engine_subsolver.h"
+#include "theory/rewriter.h"
using namespace std;
-using namespace CVC4::kind;
+using namespace cvc5::kind;
-namespace CVC4 {
+namespace cvc5 {
namespace theory {
namespace quantifiers {
Node ExprMiner::convertToSkolem(Node n)
{
- std::vector<Node> fvs;
- TermUtil::computeVarContains(n, fvs);
- if (fvs.empty())
+ if (d_skolems.empty())
{
- return n;
- }
- std::vector<Node> sfvs;
- std::vector<Node> sks;
- // map to skolems
- NodeManager* nm = NodeManager::currentNM();
- for (unsigned i = 0, size = fvs.size(); i < size; i++)
- {
- Node v = fvs[i];
- // only look at the sampler variables
- if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end())
+ NodeManager* nm = NodeManager::currentNM();
+ SkolemManager* sm = nm->getSkolemManager();
+ for (const Node& v : d_vars)
{
- sfvs.push_back(v);
- std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
- if (itf == d_fv_to_skolem.end())
- {
- Node sk = nm->mkSkolem("rrck", v.getType());
- d_fv_to_skolem[v] = sk;
- sks.push_back(sk);
- }
- else
- {
- sks.push_back(itf->second);
- }
+ Node sk = sm->mkDummySkolem("rrck", v.getType());
+ d_skolems.push_back(sk);
+ d_fv_to_skolem[v] = sk;
}
}
- return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
+ return n.substitute(
+ d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end());
}
-void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
+void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
Node query)
+{
+ initializeChecker(checker, query, options(), logicInfo());
+}
+
+void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker,
+ Node query,
+ const Options& opts,
+ const LogicInfo& logicInfo)
{
Assert (!query.isNull());
- initializeSubsolver(checker);
+ if (options().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
+ {
+ initializeSubsolver(checker,
+ opts,
+ logicInfo,
+ true,
+ options().quantifiers.sygusExprMinerCheckTimeout);
+ }
+ else
+ {
+ initializeSubsolver(checker, opts, logicInfo);
+ }
// also set the options
- checker->setOption("sygus-rr-synth-input", false);
+ checker->setOption("sygus-rr-synth-input", "false");
checker->setOption("input-language", "smt2");
// Convert bound variables to skolems. This ensures the satisfiability
// check is ground.
return Result(Result::SAT);
}
}
- std::unique_ptr<SmtEngine> smte;
+ std::unique_ptr<SolverEngine> smte;
initializeChecker(smte, query);
return smte->checkSat();
}
} // namespace quantifiers
} // namespace theory
-} // namespace CVC4
+} // namespace cvc5