diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
| commit | 65798541fa437278cde0c759ab70fd9fa4fe9638 (patch) | |
| tree | 27341327b8159e58a5ce6371bede6129bf67beb3 /src/printer | |
| parent | 78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788 (diff) | |
merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e032a9426..7fa00a6e4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -126,8 +126,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, const Integer& x = bv.getValue(); unsigned n = bv.getSize(); out << "(_ "; - out << "bv" << x <<" " << n; - out << ")"; + out << "bv" << x <<" " << n; + out << ")"; // //out << "#b"; // while(n-- > 0) { @@ -307,6 +307,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // TODO user patterns break; + //function models + case kind::FUNCTION_MODEL: + break; + case kind::FUNCTION_CASE_SPLIT: + break; + case kind::FUNCTION_CASE: + out << "if "; + break; default: // fall back on however the kind prints itself; this probably // won't be SMT-LIB v2 compliant, but it will be clear from the |