diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-03-25 05:32:31 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-03-25 05:32:31 +0000 |
commit | a2472774f053ed0ab98f1508ebb313466b0fe29a (patch) | |
tree | 2241c713acff99b23b1b51cb33c8a7a63c5afac4 /test/system/ouroborous.cpp | |
parent | ee36b95b8f722fe6501cc6ac635efd49ca673791 (diff) |
This is a merge from the "theoryfixes+cdattrhash" branch. The changes
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development). Dejan has now given me the go-ahead
for a merge.
=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================
Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor. The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead). This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.
TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.
Specifically:
* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
1. As described above.
2. Theories now have const access to the fact queue through base
class functions facts_begin() and facts_end(); useful for
debugging.
* Added an "Asserted" attribute so that theories can check if something
has been asserted or not (and therefore not propagate it). However, this
has been disabled for now, pending more data on the overhead of it, and
pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived! So far mainly infrastructure for having
system tests, but there is a system test aimed at improving code
coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
conformant to CVC4 policy.
Tests have been performed to demonstrate that these changes have no or
negligible effect on performance. In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).
Diffstat (limited to 'test/system/ouroborous.cpp')
-rw-r--r-- | test/system/ouroborous.cpp | 103 |
1 files changed, 103 insertions, 0 deletions
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp new file mode 100644 index 000000000..4473b42bb --- /dev/null +++ b/test/system/ouroborous.cpp @@ -0,0 +1,103 @@ +/********************* */ +/*! \file ouroborous.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief "Ouroborous" test: does CVC4 read its own output? + ** + ** The "Ouroborous" test, named after the serpent that swallows its own + ** tail, ensures that CVC4 can parse some input, output it again (in any + ** of its languages) and then parse it again. The result of the first + ** parse must be equal to the result of the second parse (up to renaming + ** variables), or the test fails. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" + +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::language; +using namespace std; + +const string declarations = "\ +(declare-sort U 0)\n\ +(declare-fun f (U) U)\n\ +(declare-fun x () U)\n\ +(declare-fun y () U)\n\ +(assert (= (f x) x))\n\ +"; + +int runTest(); + +int main() { + try { + return runTest(); + } catch(Exception& e) { + cerr << e << endl; + } catch(...) { + cerr << "non-cvc4 exception thrown." << endl; + } + return 1; +} + +string translate(Parser* parser, string in, InputLanguage inlang, OutputLanguage outlang) { + cout << "==============================================" << endl + << "translating from " << inlang << " to " << outlang << " this string:" << endl + << in << endl; + parser->setInput(Input::newStringInput(inlang, in, "internal-buffer")); + stringstream ss; + ss << Expr::setlanguage(outlang) << parser->nextExpression(); + AlwaysAssert(parser->nextExpression().isNull(), "next expr should be null"); + AlwaysAssert(parser->done(), "parser should be done"); + string s = ss.str(); + cout << "got this:" << endl + << s << endl + << "==============================================" << endl; + return s; +} + +int runTest() { + ExprManager em; + Parser* parser = + ParserBuilder(em, "internal-buffer") + .withStringInput(declarations) + .withInputLanguage(input::LANG_SMTLIB_V2) + .build(); + + // we don't need to execute them, but we DO need to parse them to + // get the declarations + while(Command* c = parser->nextCommand()) { + delete c; + } + + AlwaysAssert(parser->done(), "parser should be done"); + + string instr = "(= (f (f y)) x)"; + string smt2 = translate(parser, instr, input::LANG_SMTLIB_V2, output::LANG_SMTLIB_V2); + string smt1 = translate(parser, smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB); + //string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4); + //string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2); + string out = smt1; + + AlwaysAssert(out == smt2, "differences in output"); + + delete parser; + + return 0; +} + |