From: yoni206 Date: Fri, 4 Jun 2021 17:01:45 +0000 (-0700) Subject: pow2: header file for pow2 solver (#6676) X-Git-Tag: cvc5-1.0.0~1640 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d5b5b32ffe14c0f0d68d0b9a5ac36147588bfae;p=cvc5.git pow2: header file for pow2 solver (#6676) This PR adds a header file for the pow2 solver. It also includes an empty test file, to trigger compilation of the header file. The next PR will include implementations and tests. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5faeddbed..775e04b9c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -437,6 +437,7 @@ libcvc5_add_sources( theory/arith/nl/nonlinear_extension.h theory/arith/nl/poly_conversion.cpp theory/arith/nl/poly_conversion.h + theory/arith/nl/pow2_solver.h theory/arith/nl/stats.cpp theory/arith/nl/stats.h theory/arith/nl/strategy.cpp diff --git a/src/theory/arith/nl/pow2_solver.h b/src/theory/arith/nl/pow2_solver.h new file mode 100644 index 000000000..4796b2147 --- /dev/null +++ b/src/theory/arith/nl/pow2_solver.h @@ -0,0 +1,109 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * 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. + * **************************************************************************** + * + * Solver for pow2 constraints. + */ + +#ifndef CVC5__THEORY__ARITH__NL__POW2_SOLVER_H +#define CVC5__THEORY__ARITH__NL__POW2_SOLVER_H + +#include + +#include "context/cdhashset.h" +#include "expr/node.h" + +namespace cvc5 { +namespace theory { +namespace arith { + +class ArithState; +class InferenceManager; + +namespace nl { + +class NlModel; + +/** pow2 solver class + * + */ +class Pow2Solver +{ + using NodeSet = context::CDHashSet; + + public: + Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model); + ~Pow2Solver(); + + /** init last call + * + * This is called at the beginning of last call effort check, where + * assertions are the set of assertions belonging to arithmetic, + * false_asserts is the subset of assertions that are false in the current + * model, and xts is the set of extended function terms that are active in + * the current context. + */ + void initLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts); + //-------------------------------------------- lemma schemas + /** check initial refine + * + * Returns a set of valid theory lemmas, based on simple facts about pow2. + * + * Examples + * + * x>=0 --> x < pow2(x) + * + * This should be a heuristic incomplete check that only introduces a + * small number of new terms in the lemmas it returns. + */ + void checkInitialRefine(); + /** check full refine + * + * This should be a complete check that returns at least one lemma to + * rule out the current model. + */ + void checkFullRefine(); + + //-------------------------------------------- end lemma schemas + private: + // The inference manager that we push conflicts and lemmas to. + InferenceManager& d_im; + /** Reference to the non-linear model object */ + NlModel& d_model; + /** commonly used terms */ + Node d_false; + Node d_true; + Node d_zero; + Node d_one; + Node d_two; + + NodeSet d_initRefine; + /** all pow2 terms + * Cleared at each last call effort check. + * */ + std::vector d_pow2s; + + /** + * Value-based refinement lemma for i of the form (pow2 x). Returns: + * x = M(x) /\ x>= 0 ----> + * (pow2 x) = Rewriter::rewrite((pow2 M(x))) + */ + Node valueBasedLemma(Node i); +}; /* class Pow2Solver */ + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__ARITH__POW2_SOLVER_H */ diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 5d5f4c680..12663838d 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -20,6 +20,7 @@ cvc5_add_unit_test_white(evaluator_white theory) cvc5_add_unit_test_white(logic_info_white theory) cvc5_add_unit_test_white(sequences_rewriter_white theory) cvc5_add_unit_test_white(strings_rewriter_white theory) +cvc5_add_unit_test_white(theory_arith_pow2_white theory) cvc5_add_unit_test_white(theory_arith_white theory) cvc5_add_unit_test_white(theory_bags_normal_form_white theory) cvc5_add_unit_test_white(theory_bags_rewriter_white theory) diff --git a/test/unit/theory/theory_arith_pow2_white.cpp b/test/unit/theory/theory_arith_pow2_white.cpp new file mode 100644 index 000000000..db601e2ab --- /dev/null +++ b/test/unit/theory/theory_arith_pow2_white.cpp @@ -0,0 +1,46 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yoni Zohar + * + * 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. + * **************************************************************************** + * + * Unit tests for pow2 operator. + */ + +#include +#include +#include + +#include "test_smt.h" +#include "theory/arith/nl/pow2_solver.h" +#include "util/rational.h" + +namespace cvc5 { + +using namespace kind; +using namespace theory; + +namespace test { + +class TestTheoryWhiteArithPow2 : public TestSmtNoFinishInit +{ + protected: + void SetUp() override + { + TestSmtNoFinishInit::SetUp(); + d_smtEngine->setOption("produce-models", "true"); + d_smtEngine->finishInit(); + d_true = d_nodeManager->mkConst(true); + d_one = d_nodeManager->mkConst(Rational(1)); + } + Node d_true; + Node d_one; +}; +} // namespace test +} // namespace cvc5