diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/printer | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 53 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 26 |
2 files changed, 73 insertions, 6 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index d20ba0354..76c4f0abc 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -5,7 +5,7 @@ ** 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) + ** Copyright (c) 2009-2012 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 @@ -253,6 +253,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo case kind::APPLY_UF: toStream(op, n.getOperator(), depth, types, false); break; + case kind::CARDINALITY_CONSTRAINT: + out << "CARDINALITY_CONSTRAINT"; + break; case kind::FUNCTION_TYPE: if (n.getNumChildren() > 1) { @@ -548,6 +551,44 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo out << ", " << n.getOperator().getConst<BitVectorRotateRight>() << ')'; return; break; + + // Quantifiers + case kind::FORALL: + out << "(FORALL"; + toStream(out, n[0], depth, types, false); + out << " : "; + toStream(out, n[1], depth, types, false); + out << ')'; + // TODO: user patterns? + return; + case kind::EXISTS: + out << "(EXISTS"; + toStream(out, n[0], depth, types, false); + out << " : "; + toStream(out, n[1], depth, types, false); + out << ')'; + // TODO: user patterns? + break; + case kind::INST_CONSTANT: + out << "INST_CONSTANT"; + break; + case kind::BOUND_VAR_LIST: + out << '('; + for(size_t i = 0; i < n.getNumChildren(); ++i) { + if(i > 0) { + out << ", "; + } + toStream(out, n[i], -1, true, false); // ascribe types + } + out << ')'; + return; + case kind::INST_PATTERN: + out << "INST_PATTERN"; + break; + case kind::INST_PATTERN_LIST: + out << "INST_PATTERN_LIST"; + break; + default: Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl; break; @@ -662,12 +703,12 @@ static void toStream(std::ostream& out, const SExpr& sexpr) throw() { } else if(sexpr.isString()) { string s = sexpr.getValue(); // escape backslash and quote - for(string::iterator i = s.begin(); i != s.end(); ++i) { - if(*i == '"') { - s.replace(i, i + 1, "\\\""); + for(size_t i = 0; i < s.size(); ++i) { + if(s[i] == '"') { + s.replace(i, 1, "\\\""); ++i; - } else if(*i == '\\') { - s.replace(i, i + 1, "\\\\"); + } else if(s[i] == '\\') { + s.replace(i, 1, "\\\\"); ++i; } } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 72ce3804d..ebec37031 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -281,6 +281,32 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::APPLY_SELECTOR: break; + // quantifiers + case kind::FORALL: out << "forall "; break; + case kind::EXISTS: out << "exists "; break; + case kind::BOUND_VAR_LIST: + out << '('; + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; ) { + out << '('; + (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1, + types, language::output::LANG_SMTLIB_V2); + out << ' '; + (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, + false, language::output::LANG_SMTLIB_V2); + out << ')'; + if(++i != iend) { + out << ' '; + } + } + out << ')'; + return; + case kind::INST_PATTERN: + case kind::INST_PATTERN_LIST: + // TODO user patterns + 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 |