diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-15 15:44:52 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-15 22:44:52 +0000 |
commit | 4ca14e808d788ef9570dda1188645783c6a11e70 (patch) | |
tree | da87ecaf3a9aa5d789eebda94923829652fff935 /src/theory/arith | |
parent | 3fb45e059eff665ed5aaf23915f3434db1e60299 (diff) |
pow2: adding a kind, inference rules, and some implementations in the pow2 solver (#6736)
This PR is the sequel of #6676 .
It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/kinds | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/pow2_solver.cpp | 73 |
2 files changed, 75 insertions, 0 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 396befb35..0c93db90f 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -26,6 +26,7 @@ operator INTS_MODULUS_TOTAL 2 "integer modulus with interpreted division by 0 (i operator ABS 1 "absolute value" parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term" operator POW 2 "arithmetic power" +operator POW2 1 "arithmetic power of 2" operator EXPONENTIAL 1 "exponential" operator SINE 1 "sine" @@ -148,6 +149,7 @@ typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>" typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>" typerule ARCSECANT "SimpleTypeRule<RReal, AReal>" typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>" +typerule POW2 "SimpleTypeRule<RInteger, AInteger>" typerule SQRT "SimpleTypeRule<RReal, AReal>" diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp new file mode 100644 index 000000000..534895c7f --- /dev/null +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -0,0 +1,73 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Makai Mann, Gereon Kremer + * + * 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 pow2 solver. + */ + +#include "theory/arith/nl/pow2_solver.h" + +#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_state.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace arith { +namespace nl { + +Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model) + : d_im(im), d_model(model), d_initRefine(state.getUserContext()) +{ + NodeManager* nm = NodeManager::currentNM(); + d_false = nm->mkConst(false); + d_true = nm->mkConst(true); + d_zero = nm->mkConst(Rational(0)); + d_one = nm->mkConst(Rational(1)); + d_two = nm->mkConst(Rational(2)); +} + +Pow2Solver::~Pow2Solver() {} + +void Pow2Solver::initLastCall(const std::vector<Node>& assertions, + const std::vector<Node>& false_asserts, + const std::vector<Node>& xts) +{ + d_pow2s.clear(); + Trace("pow2-mv") << "POW2 terms : " << std::endl; + for (const Node& a : xts) + { + Kind ak = a.getKind(); + if (ak != POW2) + { + // don't care about other terms + continue; + } + d_pow2s.push_back(a); + } + Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl; +} + +void Pow2Solver::checkInitialRefine() {} + +void Pow2Solver::checkFullRefine() {} + +Node Pow2Solver::valueBasedLemma(Node i) { return Node(); } + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace cvc5 |