1 /********************* */ 2 /*! \file theory_engine_white.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Dejan Jovanovic, Andres Noetzli 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 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.\endverbatim 11 ** 12 ** \brief White box testing of CVC4::theory::Theory. 13 ** 14 ** White box testing of CVC4::theory::Theory. This test creates 15 ** "fake" theory interfaces and injects them into TheoryEngine, so we 16 ** can test TheoryEngine's behavior without relying on independent 17 ** theory behavior. This is done in TheoryEngineWhite::setUp() by 18 ** means of the TheoryEngineWhite::registerTheory() interface. 19 **/ 20 21 #include <cxxtest/TestSuite.h> 22 23 #include <deque> 24 #include <iostream> 25 #include <memory> 26 #include <string> 27 28 #include "base/cvc4_assert.h" 29 #include "context/context.h" 30 #include "expr/kind.h" 31 #include "expr/node.h" 32 #include "expr/node_manager.h" 33 #include "options/options.h" 34 #include "smt/smt_engine.h" 35 #include "smt/smt_engine_scope.h" 36 #include "theory/bv/theory_bv_rewrite_rules_normalization.h" 37 #include "theory/bv/theory_bv_rewrite_rules_simplification.h" 38 #include "theory/rewriter.h" 39 #include "theory/theory.h" 40 #include "theory/theory_engine.h" 41 #include "theory/valuation.h" 42 #include "util/integer.h" 43 #include "util/proof.h" 44 #include "util/rational.h" 45 46 using namespace CVC4; 47 using namespace CVC4::theory; 48 using namespace CVC4::expr; 49 using namespace CVC4::context; 50 using namespace CVC4::kind; 51 using namespace CVC4::smt; 52 using namespace CVC4::theory::bv; 53 54 using namespace std; 55 56 class FakeOutputChannel : public OutputChannel { conflict(TNode n,std::unique_ptr<Proof> pf)57 void conflict(TNode n, std::unique_ptr<Proof> pf) override 58 { 59 Unimplemented(); 60 } propagate(TNode n)61 bool propagate(TNode n) override { Unimplemented(); } lemma(TNode n,ProofRule rule,bool removable,bool preprocess,bool sendAtoms)62 LemmaStatus lemma(TNode n, ProofRule rule, bool removable, bool preprocess, 63 bool sendAtoms) override { 64 Unimplemented(); 65 } requirePhase(TNode,bool)66 void requirePhase(TNode, bool) override { Unimplemented(); } setIncomplete()67 void setIncomplete() override { Unimplemented(); } handleUserAttribute(const char * attr,Theory * t)68 void handleUserAttribute(const char* attr, Theory* t) override { 69 Unimplemented(); 70 } splitLemma(TNode n,bool removable)71 LemmaStatus splitLemma(TNode n, bool removable) override { Unimplemented(); } 72 }; /* class FakeOutputChannel */ 73 74 template<TheoryId theory> 75 class FakeTheory; 76 77 /** Expected rewrite calls can be PRE- or POST-rewrites */ 78 enum RewriteType { 79 PRE, 80 POST 81 };/* enum RewriteType */ 82 83 /** 84 * Stores an "expected" rewrite call. The main test class will set up a sequence 85 * of these RewriteItems, then do a rewrite, ensuring that the actual call sequence 86 * matches the sequence of expected RewriteItems. */ 87 struct RewriteItem { 88 RewriteType d_type; 89 // FakeTheory* d_theory; 90 Node d_node; 91 bool d_topLevel; 92 };/* struct RewriteItem */ 93 94 /** 95 * Fake Theory interface. Looks like a Theory, but really all it does is note when and 96 * how rewriting behavior is requested. 97 */ 98 template<TheoryId theoryId> 99 class FakeTheory : public Theory { 100 /** 101 * This fake theory class is equally useful for bool, uf, arith, etc. It keeps an 102 * identifier to identify itself. 103 */ 104 std::string d_id; 105 106 /** 107 * The expected sequence of rewrite calls. Filled by FakeTheory::expect() and consumed 108 * by FakeTheory::preRewrite() and FakeTheory::postRewrite(). 109 */ 110 // static std::deque<RewriteItem> s_expected; 111 112 public: FakeTheory(context::Context * ctxt,context::UserContext * uctxt,OutputChannel & out,Valuation valuation,const LogicInfo & logicInfo)113 FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : 114 Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo) 115 { } 116 117 /** Register an expected rewrite call */ expect(RewriteType type,FakeTheory * thy,TNode n,bool topLevel)118 static void expect(RewriteType type, FakeTheory* thy, TNode n, bool topLevel) 119 throw() 120 { 121 RewriteItem item = { type, thy, n, topLevel }; 122 //s_expected.push_back(item); 123 } 124 125 /** 126 * Returns whether the expected queue is empty. This is done after a call into 127 * the rewriter to ensure that the actual set of observed rewrite calls completed 128 * the sequence of expected rewrite calls. 129 */ nothingMoreExpected()130 static bool nothingMoreExpected() throw() { 131 return true; // s_expected.empty(); 132 } 133 134 /** 135 * Overrides Theory::preRewrite(). This "fake theory" version ensures that 136 * this actual, observed pre-rewrite call matches the next "expected" call set up 137 * by the test. 138 */ preRewrite(TNode n,bool topLevel)139 RewriteResponse preRewrite(TNode n, bool topLevel) { 140 // if(false) { //s_expected.empty()) { 141 // cout << std::endl 142 // << "didn't expect anything more, but got" << std::endl 143 // << " PRE " << topLevel << " " << identify() << " " << n 144 // << std::endl; 145 // } 146 // TS_ASSERT(!s_expected.empty()); 147 // 148 // RewriteItem expected = s_expected.front(); 149 // s_expected.pop_front(); 150 // 151 // if(expected.d_type != PRE || 152 //// expected.d_theory != this || 153 // expected.d_node != n || 154 // expected.d_topLevel != topLevel) { 155 // cout << std::endl 156 // << "HAVE PRE " << topLevel << " " << identify() << " " << n 157 // << std::endl 158 // << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ") 159 // // << expected.d_topLevel << " " << expected.d_theory->identify() 160 // << " " << expected.d_node << std::endl << std::endl; 161 // } 162 // 163 // TS_ASSERT_EQUALS(expected.d_type, PRE); 164 //// TS_ASSERT_EQUALS(expected.d_theory, this); 165 // TS_ASSERT_EQUALS(expected.d_node, n); 166 // TS_ASSERT_EQUALS(expected.d_topLevel, topLevel); 167 168 return RewriteResponse(REWRITE_DONE, n); 169 } 170 171 /** 172 * Overrides Theory::postRewrite(). This "fake theory" version ensures that 173 * this actual, observed post-rewrite call matches the next "expected" call set up 174 * by the test. 175 */ postRewrite(TNode n,bool topLevel)176 RewriteResponse postRewrite(TNode n, bool topLevel) { 177 // if(s_expected.empty()) { 178 // cout << std::endl 179 // << "didn't expect anything more, but got" << std::endl 180 // << " POST " << topLevel << " " << identify() << " " << n 181 // << std::endl; 182 // } 183 // TS_ASSERT(!s_expected.empty()); 184 // 185 // RewriteItem expected = s_expected.front(); 186 // s_expected.pop_front(); 187 // 188 // if(expected.d_type != POST || 189 //// expected.d_theory != this || 190 // expected.d_node != n || 191 // expected.d_topLevel != topLevel) { 192 // cout << std::endl 193 // << "HAVE POST " << topLevel << " " << identify() << " " << n 194 // << std::endl 195 // << "WANT " << (expected.d_type == PRE ? "PRE " : "POST ") 196 //// << expected.d_topLevel << " " << expected.d_theory->identify() 197 // << " " << expected.d_node << std::endl << std::endl; 198 // } 199 // 200 // TS_ASSERT_EQUALS(expected.d_type, POST); 201 // TS_ASSERT_EQUALS(expected.d_theory, this); 202 // TS_ASSERT_EQUALS(expected.d_node, n); 203 // TS_ASSERT_EQUALS(expected.d_topLevel, topLevel); 204 205 return RewriteResponse(REWRITE_DONE, n); 206 } 207 identify()208 std::string identify() const override { 209 return "Fake" + d_id; 210 } 211 presolve()212 void presolve() override { Unimplemented(); } 213 preRegisterTerm(TNode)214 void preRegisterTerm(TNode) override { Unimplemented(); } registerTerm(TNode)215 void registerTerm(TNode) { Unimplemented(); } check(Theory::Effort)216 void check(Theory::Effort) override { Unimplemented(); } propagate(Theory::Effort)217 void propagate(Theory::Effort) override { Unimplemented(); } explain(TNode)218 Node explain(TNode) override { Unimplemented(); } getValue(TNode n)219 Node getValue(TNode n) { return Node::null(); } 220 };/* class FakeTheory */ 221 222 223 /* definition of the s_expected static field in FakeTheory; see above */ 224 // std::deque<RewriteItem> FakeTheory::s_expected; 225 226 227 /** 228 * Test the TheoryEngine. 229 */ 230 class TheoryEngineWhite : public CxxTest::TestSuite { 231 Context* d_ctxt; 232 UserContext* d_uctxt; 233 234 ExprManager* d_em; 235 NodeManager* d_nm; 236 SmtEngine* d_smt; 237 SmtScope* d_scope; 238 FakeOutputChannel *d_nullChannel; 239 TheoryEngine* d_theoryEngine; 240 241 public: 242 setUp()243 void setUp() override { 244 d_em = new ExprManager(); 245 d_smt = new SmtEngine(d_em); 246 d_nm = NodeManager::fromExprManager(d_em); 247 d_scope = new SmtScope(d_smt); 248 249 d_ctxt = d_smt->d_context; 250 d_uctxt = d_smt->d_userContext; 251 252 d_nullChannel = new FakeOutputChannel(); 253 254 // Notice that this unit test uses the theory engine of a created SMT 255 // engine d_smt. We must ensure that d_smt is properly initialized via 256 // the following call, which constructs its underlying theory engine. 257 d_smt->finalOptionsAreSet(); 258 d_theoryEngine = d_smt->d_theoryEngine; 259 for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) { 260 delete d_theoryEngine->d_theoryOut[id]; 261 delete d_theoryEngine->d_theoryTable[id]; 262 d_theoryEngine->d_theoryOut[id] = NULL; 263 d_theoryEngine->d_theoryTable[id] = NULL; 264 } 265 d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN); 266 d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL); 267 d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(THEORY_UF); 268 d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(THEORY_ARITH); 269 d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAYS> >(THEORY_ARRAYS); 270 d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(THEORY_BV); 271 } 272 tearDown()273 void tearDown() override { 274 delete d_nullChannel; 275 276 delete d_scope; 277 delete d_smt; 278 delete d_em; 279 } 280 testRewriterSimple()281 void testRewriterSimple() { 282 Node x = d_nm->mkVar("x", d_nm->integerType()); 283 Node y = d_nm->mkVar("y", d_nm->integerType()); 284 Node z = d_nm->mkVar("z", d_nm->integerType()); 285 286 // make the expression (PLUS x y (MULT z 0)) 287 Node zero = d_nm->mkConst(Rational("0")); 288 Node zTimesZero = d_nm->mkNode(MULT, z, zero); 289 Node n = d_nm->mkNode(PLUS, x, y, zTimesZero); 290 291 Node nExpected = n; 292 Node nOut; 293 294 // // set up the expected sequence of calls 295 // FakeTheory::expect(PRE, d_arith, n, true); 296 // FakeTheory::expect(PRE, d_arith, x, false); 297 // FakeTheory::expect(POST, d_arith, x, false); 298 // FakeTheory::expect(PRE, d_arith, y, false); 299 // FakeTheory::expect(POST, d_arith, y, false); 300 // FakeTheory::expect(PRE, d_arith, zTimesZero, false); 301 // FakeTheory::expect(PRE, d_arith, z, false); 302 // FakeTheory::expect(POST, d_arith, z, false); 303 // FakeTheory::expect(PRE, d_arith, zero, false); 304 // FakeTheory::expect(POST, d_arith, zero, false); 305 // FakeTheory::expect(POST, d_arith, zTimesZero, false); 306 // FakeTheory::expect(POST, d_arith, n, true); 307 308 // do a full rewrite; FakeTheory::preRewrite() and FakeTheory::postRewrite() 309 // assert that the rewrite calls that are made match the expected sequence 310 // set up above 311 nOut = Rewriter::rewrite(n); 312 313 // assert that we consumed the sequence of expected calls completely 314 // TS_ASSERT(FakeTheory::nothingMoreExpected()); 315 316 // assert that the rewritten node is what we expect 317 // TS_ASSERT_EQUALS(nOut, nExpected); 318 } 319 testRewriterComplicated()320 void testRewriterComplicated() { 321 Node x = d_nm->mkVar("x", d_nm->integerType()); 322 Node y = d_nm->mkVar("y", d_nm->realType()); 323 TypeNode u = d_nm->mkSort("U"); 324 Node z1 = d_nm->mkVar("z1", u); 325 Node z2 = d_nm->mkVar("z2", u); 326 Node f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->integerType(), 327 d_nm->integerType())); 328 Node g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->realType(), 329 d_nm->integerType())); 330 Node one = d_nm->mkConst(Rational("1")); 331 Node two = d_nm->mkConst(Rational("2")); 332 333 Node f1 = d_nm->mkNode(APPLY_UF, f, one); 334 Node f2 = d_nm->mkNode(APPLY_UF, f, two); 335 Node fx = d_nm->mkNode(APPLY_UF, f, x); 336 Node ffx = d_nm->mkNode(APPLY_UF, f, fx); 337 Node gy = d_nm->mkNode(APPLY_UF, g, y); 338 Node z1eqz2 = d_nm->mkNode(EQUAL, z1, z2); 339 Node f1eqf2 = d_nm->mkNode(EQUAL, f1, f2); 340 Node ffxeqgy = d_nm->mkNode(EQUAL, ffx, gy); 341 Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2); 342 Node ffxeqf1 = d_nm->mkNode(EQUAL, ffx, f1); 343 Node or1 = d_nm->mkNode(OR, and1, ffxeqf1); 344 // make the expression: 345 // (IMPLIES (EQUAL (f 1) (f 2)) 346 // (OR (AND (EQUAL (f (f x)) (g y)) 347 // (EQUAL z1 z2)) 348 // (EQUAL (f (f x)) (f 1)))) 349 Node n = d_nm->mkNode(IMPLIES, f1eqf2, or1); 350 Node nExpected = n; 351 Node nOut; 352 353 // set up the expected sequence of calls 354 // FakeTheory::expect(PRE, d_bool, n, true); 355 // FakeTheory::expect(PRE, d_uf, f1eqf2, true); 356 // FakeTheory::expect(PRE, d_uf, f1, false); 357 //FakeTheory::expect(PRE, d_builtin, f, true); 358 //FakeTheory::expect(POST, d_builtin, f, true); 359 // FakeTheory::expect(PRE, d_arith, one, true); 360 // FakeTheory::expect(POST, d_arith, one, true); 361 // FakeTheory::expect(POST, d_uf, f1, false); 362 // FakeTheory::expect(PRE, d_uf, f2, false); 363 // these aren't called because they're in the rewrite cache 364 //FakeTheory::expect(PRE, d_builtin, f, true); 365 //FakeTheory::expect(POST, d_builtin, f, true); 366 // FakeTheory::expect(PRE, d_arith, two, true); 367 // FakeTheory::expect(POST, d_arith, two, true); 368 // FakeTheory::expect(POST, d_uf, f2, false); 369 // FakeTheory::expect(POST, d_uf, f1eqf2, true); 370 // FakeTheory::expect(PRE, d_bool, or1, false); 371 // FakeTheory::expect(PRE, d_bool, and1, false); 372 // FakeTheory::expect(PRE, d_uf, ffxeqgy, true); 373 // FakeTheory::expect(PRE, d_uf, ffx, false); 374 // FakeTheory::expect(PRE, d_uf, fx, false); 375 // these aren't called because they're in the rewrite cache 376 //FakeTheory::expect(PRE, d_builtin, f, true); 377 //FakeTheory::expect(POST, d_builtin, f, true); 378 // FakeTheory::expect(PRE, d_arith, x, true); 379 // FakeTheory::expect(POST, d_arith, x, true); 380 // FakeTheory::expect(POST, d_uf, fx, false); 381 // FakeTheory::expect(POST, d_uf, ffx, false); 382 // FakeTheory::expect(PRE, d_uf, gy, false); 383 //FakeTheory::expect(PRE, d_builtin, g, true); 384 //FakeTheory::expect(POST, d_builtin, g, true); 385 // FakeTheory::expect(PRE, d_arith, y, true); 386 // FakeTheory::expect(POST, d_arith, y, true); 387 // FakeTheory::expect(POST, d_uf, gy, false); 388 // FakeTheory::expect(POST, d_uf, ffxeqgy, true); 389 // FakeTheory::expect(PRE, d_uf, z1eqz2, true); 390 // FakeTheory::expect(PRE, d_uf, z1, false); 391 // FakeTheory::expect(POST, d_uf, z1, false); 392 // FakeTheory::expect(PRE, d_uf, z2, false); 393 // FakeTheory::expect(POST, d_uf, z2, false); 394 // FakeTheory::expect(POST, d_uf, z1eqz2, true); 395 // FakeTheory::expect(POST, d_bool, and1, false); 396 // FakeTheory::expect(PRE, d_uf, ffxeqf1, true); 397 // these aren't called because they're in the rewrite cache 398 //FakeTheory::expect(PRE, d_uf, ffx, false); 399 //FakeTheory::expect(POST, d_uf, ffx, false); 400 //FakeTheory::expect(PRE, d_uf, f1, false); 401 //FakeTheory::expect(POST, d_uf, f1, false); 402 // FakeTheory::expect(POST, d_uf, ffxeqf1, true); 403 // FakeTheory::expect(POST, d_bool, or1, false); 404 // FakeTheory::expect(POST, d_bool, n, true); 405 406 // do a full rewrite; FakeTheory::preRewrite() and FakeTheory::postRewrite() 407 // assert that the rewrite calls that are made match the expected sequence 408 // set up above 409 nOut = Rewriter::rewrite(n); 410 411 // assert that we consumed the sequence of expected calls completely 412 // TS_ASSERT(FakeTheory::nothingMoreExpected()); 413 414 // assert that the rewritten node is what we expect 415 // TS_ASSERT_EQUALS(nOut, nExpected); 416 } 417 testRewriterRules()418 void testRewriterRules() { 419 TypeNode t = d_nm->mkBitVectorType(8); 420 Node x = d_nm->mkVar("x", t); 421 Node y = d_nm->mkVar("y", t); 422 Node z = d_nm->mkVar("z", t); 423 424 // (x - y) * z --> (x * z) - (y * z) 425 Node expr = 426 d_nm->mkNode(BITVECTOR_MULT, d_nm->mkNode(BITVECTOR_SUB, x, y), z); 427 Node result = expr; 428 if (RewriteRule<MultDistrib>::applies(expr)) { 429 result = RewriteRule<MultDistrib>::apply(expr); 430 } 431 Node expected = 432 d_nm->mkNode(BITVECTOR_SUB, d_nm->mkNode(BITVECTOR_MULT, x, z), 433 d_nm->mkNode(BITVECTOR_MULT, y, z)); 434 TS_ASSERT_EQUALS(result, expected); 435 436 // Try to apply MultSlice to a multiplication of two and three different 437 // variables, expect different results (x * y and x * y * z should not get 438 // rewritten to the same term). 439 expr = d_nm->mkNode(BITVECTOR_MULT, x, y, z); 440 result = expr; 441 Node expr2 = d_nm->mkNode(BITVECTOR_MULT, x, y); 442 Node result2 = expr; 443 if (RewriteRule<MultSlice>::applies(expr)) { 444 result = RewriteRule<MultSlice>::apply(expr); 445 } 446 if (RewriteRule<MultSlice>::applies(expr2)) { 447 result2 = RewriteRule<MultSlice>::apply(expr2); 448 } 449 TS_ASSERT_DIFFERS(result, result2); 450 } 451 }; 452