test/unit/theory/theory_arith_cad_white.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Unit tests for the CAD module for nonlinear arithmetic.
  14  */
  15
  16 #ifdef CVC5_USE_POLY
  17
  18 #include <poly/polyxx.h>
  19
  20 #include <iostream>
  21 #include <memory>
  22 #include <vector>
  23
  24 #include "test_smt.h"
  25 #include "theory/arith/nl/cad/cdcac.h"
  26 #include "theory/arith/nl/cad/lazard_evaluation.h"
  27 #include "theory/arith/nl/cad/projections.h"
  28 #include "theory/arith/nl/cad_solver.h"
  29 #include "theory/arith/nl/nl_lemma_utils.h"
  30 #include "theory/arith/nl/poly_conversion.h"
  31 #include "theory/arith/theory_arith.h"
  32 #include "theory/quantifiers/extended_rewrite.h"
  33 #include "theory/theory.h"
  34 #include "theory/theory_engine.h"
  35 #include "util/poly_util.h"
  36
  37 namespace cvc5::test {
  38
  39 using namespace cvc5;
  40 using namespace cvc5::theory;
  41 using namespace cvc5::theory::arith;
  42 using namespace cvc5::theory::arith::nl;
  43
  44 NodeManager* nodeManager;
  45 class TestTheoryWhiteArithCAD : public TestSmt
  46 {
  47  protected:
  48   void SetUp() override
  49   {
  50     TestSmt::SetUp();
  51     d_realType.reset(new TypeNode(d_nodeManager->realType()));
  52     d_intType.reset(new TypeNode(d_nodeManager->integerType()));
  53     Trace.on("cad-check");
  54     nodeManager = d_nodeManager.get();
  55   }
  56
  57   Node dummy(int i) const { return d_nodeManager->mkConst(Rational(i)); }
  58
  59   Theory::Effort d_level = Theory::EFFORT_FULL;
  60   std::unique_ptr<TypeNode> d_realType;
  61   std::unique_ptr<TypeNode> d_intType;
  62   const Rational d_zero = 0;
  63   const Rational d_one = 1;
  64 };
  65
  66 poly::AlgebraicNumber get_ran(std::initializer_list<long> init,
  67                               int lower,
  68                               int upper)
  69 {
  70   return poly::AlgebraicNumber(poly::UPolynomial(init),
  71                                poly::DyadicInterval(lower, upper));
  72 }
  73
  74 Node operator==(const Node& a, const Node& b)
  75 {
  76   return nodeManager->mkNode(Kind::EQUAL, a, b);
  77 }
  78 Node operator>=(const Node& a, const Node& b)
  79 {
  80   return nodeManager->mkNode(Kind::GEQ, a, b);
  81 }
  82 Node operator+(const Node& a, const Node& b)
  83 {
  84   return nodeManager->mkNode(Kind::PLUS, a, b);
  85 }
  86 Node operator*(const Node& a, const Node& b)
  87 {
  88   return nodeManager->mkNode(Kind::NONLINEAR_MULT, a, b);
  89 }
  90 Node operator!(const Node& a) { return nodeManager->mkNode(Kind::NOT, a); }
  91 Node make_real_variable(const std::string& s)
  92 {
  93   return nodeManager->mkSkolem(
  94       s, nodeManager->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
  95 }
  96 Node make_int_variable(const std::string& s)
  97 {
  98   return nodeManager->mkSkolem(
  99       s, nodeManager->integerType(), "", NodeManager::SKOLEM_EXACT_NAME);
 100 }
 101
 102 TEST_F(TestTheoryWhiteArithCAD, test_univariate_isolation)
 103 {
 104   poly::UPolynomial poly({-2, 2, 3, -3, -1, 1});
 105   auto roots = poly::isolate_real_roots(poly);
 106
 107   EXPECT_TRUE(roots.size() == 4);
 108   EXPECT_TRUE(roots[0] == get_ran({-2, 0, 1}, -2, -1));
 109   EXPECT_TRUE(roots[1] == poly::Integer(-1));
 110   EXPECT_TRUE(roots[2] == poly::Integer(1));
 111   EXPECT_TRUE(roots[3] == get_ran({-2, 0, 1}, 1, 2));
 112 }
 113
 114 TEST_F(TestTheoryWhiteArithCAD, test_multivariate_isolation)
 115 {
 116   poly::Variable x("x");
 117   poly::Variable y("y");
 118   poly::Variable z("z");
 119
 120   poly::Assignment a;
 121   a.set(x, get_ran({-2, 0, 1}, 1, 2));
 122   a.set(y, get_ran({-2, 0, 0, 0, 1}, 1, 2));
 123
 124   poly::Polynomial poly = (y * y + x) - z;
 125
 126   auto roots = poly::isolate_real_roots(poly, a);
 127
 128   EXPECT_TRUE(roots.size() == 1);
 129   EXPECT_TRUE(roots[0] == get_ran({-8, 0, 1}, 2, 3));
 130 }
 131
 132 TEST_F(TestTheoryWhiteArithCAD, test_univariate_factorization)
 133 {
 134   poly::UPolynomial poly({-24, 44, -18, -1, 1, -3, 1});
 135
 136   auto factors = square_free_factors(poly);
 137   std::sort(factors.begin(), factors.end());
 138   EXPECT_EQ(factors[0], poly::UPolynomial({-1, 1}));
 139   EXPECT_EQ(factors[1], poly::UPolynomial({-24, -4, -2, -1, 1}));
 140 }
 141
 142 TEST_F(TestTheoryWhiteArithCAD, test_projection)
 143 {
 144   // Gereon's thesis, Ex 5.1
 145   poly::Variable x("x");
 146   poly::Variable y("y");
 147
 148   poly::Polynomial p = (y + 1) * (y + 1) - x * x * x + 3 * x - 2;
 149   poly::Polynomial q = (x + 1) * y - 3;
 150
 151   auto res = cad::projectionMcCallum({p, q});
 152   std::sort(res.begin(), res.end());
 153   EXPECT_EQ(res[0], x - 1);
 154   EXPECT_EQ(res[1], x + 1);
 155   EXPECT_EQ(res[2], x + 2);
 156   EXPECT_EQ(res[3], x * x * x - 3 * x + 1);
 157   EXPECT_EQ(res[4],
 158             x * x * x * x * x + 2 * x * x * x * x - 2 * x * x * x - 5 * x * x
 159                 - 7 * x - 14);
 160 }
 161
 162 poly::Polynomial up_to_poly(const poly::UPolynomial& p, poly::Variable var)
 163 {
 164   poly::Polynomial res;
 165   poly::Polynomial mult = 1;
 166   for (const auto& coeff : coefficients(p))
 167   {
 168     if (!is_zero(coeff))
 169     {
 170       res += mult * coeff;
 171     }
 172     mult *= var;
 173   }
 174   return res;
 175 }
 176
 177 TEST_F(TestTheoryWhiteArithCAD, lazard_simp)
 178 {
 179   Node a = d_nodeManager->mkVar(*d_realType);
 180   Node c = d_nodeManager->mkVar(*d_realType);
 181   Node orig = d_nodeManager->mkAnd(std::vector<Node>{
 182       d_nodeManager->mkNode(Kind::EQUAL, a, d_nodeManager->mkConst(d_zero)),
 183       d_nodeManager->mkNode(
 184           Kind::EQUAL,
 185           d_nodeManager->mkNode(
 186               Kind::PLUS,
 187               d_nodeManager->mkNode(Kind::NONLINEAR_MULT, a, c),
 188               d_nodeManager->mkConst(d_one)),
 189           d_nodeManager->mkConst(d_zero))});
 190
 191   {
 192     Node rewritten = Rewriter::rewrite(orig);
 193     EXPECT_NE(rewritten, d_nodeManager->mkConst(false));
 194   }
 195   {
 196     quantifiers::ExtendedRewriter extrew;
 197     Node rewritten = extrew.extendedRewrite(orig);
 198     EXPECT_EQ(rewritten, d_nodeManager->mkConst(false));
 199   }
 200 }
 201
 202 #ifdef CVC5_USE_COCOA
 203 TEST_F(TestTheoryWhiteArithCAD, lazard_eval)
 204 {
 205   poly::Variable x("x");
 206   poly::Variable y("y");
 207   poly::Variable z("z");
 208   poly::Variable f("f");
 209   poly::AlgebraicNumber ax = get_ran({-2, 0, 1}, 1, 2);
 210   poly::AlgebraicNumber ay = get_ran({-2, 0, 0, 0, 1}, 1, 2);
 211   poly::AlgebraicNumber az = get_ran({-3, 0, 1}, 1, 2);
 212
 213   cad::LazardEvaluation lazard;
 214   lazard.add(x, ax);
 215   lazard.add(y, ay);
 216   lazard.add(z, az);
 217
 218   poly::Polynomial q = (x * x - 2) * (y * y * y * y - 2) * z * f;
 219   lazard.addFreeVariable(f);
 220   auto qred = lazard.reducePolynomial(q);
 221   EXPECT_EQ(qred, std::vector<poly::Polynomial>{f});
 222 }
 223 #endif
 224
 225 TEST_F(TestTheoryWhiteArithCAD, test_cdcac_1)
 226 {
 227   Options opts;
 228   Env env(NodeManager::currentNM(), &opts);
 229   cad::CDCAC cac(env, {});
 230   poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
 231   poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
 232
 233   cac.getConstraints().addConstraint(
 234       4 * y - x * x + 4, poly::SignCondition::LT, dummy(1));
 235   cac.getConstraints().addConstraint(
 236       4 * y - 4 + (x - 1) * (x - 1), poly::SignCondition::GT, dummy(2));
 237   cac.getConstraints().addConstraint(
 238       4 * y - x - 2, poly::SignCondition::GT, dummy(3));
 239
 240   cac.computeVariableOrdering();
 241
 242   auto cover = cac.getUnsatCover();
 243   EXPECT_TRUE(cover.empty());
 244   std::cout << "SAT: " << cac.getModel() << std::endl;
 245 }
 246
 247 TEST_F(TestTheoryWhiteArithCAD, test_cdcac_2)
 248 {
 249   Options opts;
 250   Env env(NodeManager::currentNM(), &opts);
 251   cad::CDCAC cac(env, {});
 252   poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
 253   poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
 254
 255   cac.getConstraints().addConstraint(y - pow(-x - 3, 11) + pow(-x - 3, 10) + 1,
 256                                      poly::SignCondition::GT,
 257                                      dummy(1));
 258   cac.getConstraints().addConstraint(
 259       2 * y - x + 2, poly::SignCondition::LT, dummy(2));
 260   cac.getConstraints().addConstraint(
 261       2 * y - 1 + x * x, poly::SignCondition::GT, dummy(3));
 262   cac.getConstraints().addConstraint(
 263       3 * y + x + 2, poly::SignCondition::LT, dummy(4));
 264   cac.getConstraints().addConstraint(
 265       y * y * y - pow(x - 2, 11) + pow(x - 2, 10) + 1,
 266       poly::SignCondition::GT,
 267       dummy(5));
 268
 269   cac.computeVariableOrdering();
 270
 271   auto cover = cac.getUnsatCover();
 272   EXPECT_TRUE(!cover.empty());
 273   auto nodes = cad::collectConstraints(cover);
 274   std::vector<Node> ref{dummy(1), dummy(2), dummy(3), dummy(4), dummy(5)};
 275   EXPECT_EQ(nodes, ref);
 276 }
 277
 278 TEST_F(TestTheoryWhiteArithCAD, test_cdcac_3)
 279 {
 280   Options opts;
 281   Env env(NodeManager::currentNM(), &opts);
 282   cad::CDCAC cac(env, {});
 283   poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
 284   poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
 285   poly::Variable z = cac.getConstraints().varMapper()(make_real_variable("z"));
 286
 287   cac.getConstraints().addConstraint(
 288       x * x + y * y + z * z - 1, poly::SignCondition::LT, dummy(1));
 289   cac.getConstraints().addConstraint(
 290       4 * x * x + (2 * y - 3) * (2 * y - 3) + 4 * z * z - 4,
 291       poly::SignCondition::LT,
 292       dummy(2));
 293
 294   cac.computeVariableOrdering();
 295
 296   auto cover = cac.getUnsatCover();
 297   EXPECT_TRUE(cover.empty());
 298   std::cout << "SAT: " << cac.getModel() << std::endl;
 299 }
 300
 301 TEST_F(TestTheoryWhiteArithCAD, test_cdcac_4)
 302 {
 303   Options opts;
 304   Env env(NodeManager::currentNM(), &opts);
 305   cad::CDCAC cac(env, {});
 306   poly::Variable x = cac.getConstraints().varMapper()(make_real_variable("x"));
 307   poly::Variable y = cac.getConstraints().varMapper()(make_real_variable("y"));
 308   poly::Variable z = cac.getConstraints().varMapper()(make_real_variable("z"));
 309
 310   cac.getConstraints().addConstraint(
 311       -z * z + y * y + x * x - 25, poly::SignCondition::GT, dummy(1));
 312   cac.getConstraints().addConstraint(
 313       (y - x - 6) * z * z - 9 * y * y + x * x - 1,
 314       poly::SignCondition::GT,
 315       dummy(2));
 316   cac.getConstraints().addConstraint(
 317       y * y - 100, poly::SignCondition::LT, dummy(3));
 318
 319   cac.computeVariableOrdering();
 320
 321   auto cover = cac.getUnsatCover();
 322   EXPECT_TRUE(cover.empty());
 323   std::cout << "SAT: " << cac.getModel() << std::endl;
 324 }
 325
 326 void test_delta(const std::vector<Node>& a)
 327 {
 328   Options opts;
 329   Env env(NodeManager::currentNM(), &opts);
 330   cad::CDCAC cac(env, {});
 331   cac.reset();
 332   for (const Node& n : a)
 333   {
 334     cac.getConstraints().addConstraint(n);
 335   }
 336   cac.computeVariableOrdering();
 337
 338   // Do full theory check here
 339
 340   auto covering = cac.getUnsatCover();
 341   if (covering.empty())
 342   {
 343     std::cout << "SAT: " << cac.getModel() << std::endl;
 344   }
 345   else
 346   {
 347     auto mis = cad::collectConstraints(covering);
 348     std::cout << "Collected MIS: " << mis << std::endl;
 349     Assert(!mis.empty()) << "Infeasible subset can not be empty";
 350     Node lem = NodeManager::currentNM()->mkAnd(mis).negate();
 351     Notice() << "UNSAT with MIS: " << lem << std::endl;
 352   }
 353 }
 354
 355 TEST_F(TestTheoryWhiteArithCAD, test_delta_one)
 356 {
 357   std::vector<Node> a;
 358   Node zero = d_nodeManager->mkConst(Rational(0));
 359   Node one = d_nodeManager->mkConst(Rational(1));
 360   Node mone = d_nodeManager->mkConst(Rational(-1));
 361   Node fifth = d_nodeManager->mkConst(Rational(1, 2));
 362   Node g = make_real_variable("g");
 363   Node l = make_real_variable("l");
 364   Node q = make_real_variable("q");
 365   Node s = make_real_variable("s");
 366   Node u = make_real_variable("u");
 367
 368   a.emplace_back(l == mone);
 369   a.emplace_back(!(g * s == zero));
 370   a.emplace_back(q * s == zero);
 371   a.emplace_back(u == zero);
 372   a.emplace_back(q == (one + (fifth * g * s)));
 373   a.emplace_back(l == u + q * s + (fifth * g * s * s));
 374
 375   test_delta(a);
 376 }
 377
 378 TEST_F(TestTheoryWhiteArithCAD, test_delta_two)
 379 {
 380   std::vector<Node> a;
 381   Node zero = d_nodeManager->mkConst(Rational(0));
 382   Node one = d_nodeManager->mkConst(Rational(1));
 383   Node mone = d_nodeManager->mkConst(Rational(-1));
 384   Node fifth = d_nodeManager->mkConst(Rational(1, 2));
 385   Node g = make_real_variable("g");
 386   Node l = make_real_variable("l");
 387   Node q = make_real_variable("q");
 388   Node s = make_real_variable("s");
 389   Node u = make_real_variable("u");
 390
 391   a.emplace_back(l == mone);
 392   a.emplace_back(!(g * s == zero));
 393   a.emplace_back(u == zero);
 394   a.emplace_back(q * s == zero);
 395   a.emplace_back(q == (one + (fifth * g * s)));
 396   a.emplace_back(l == u + q * s + (fifth * g * s * s));
 397
 398   test_delta(a);
 399 }
 400
 401 TEST_F(TestTheoryWhiteArithCAD, test_ran_conversion)
 402 {
 403   RealAlgebraicNumber ran(
 404       std::vector<Rational>({-2, 0, 1}), Rational(1, 3), Rational(7, 3));
 405   {
 406     Node x = make_real_variable("x");
 407     Node n = nl::ran_to_node(ran, x);
 408     RealAlgebraicNumber back = nl::node_to_ran(n, x);
 409     EXPECT_TRUE(ran == back);
 410   }
 411 }
 412 }  // namespace cvc5::test
 413
 414 #endif