diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-03-05 14:05:26 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-05 14:05:26 -0800 |
commit | d51c8347a3c6bf7857c474bd3493377f9fed58e5 (patch) | |
tree | 56da229cd8fcbe6988937514820c13c3894f2558 /src/printer | |
parent | d1aa4ae101987093a06208650e2ea4878f7437ca (diff) |
Add support for check-sat-assuming. (#1637)
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 11 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 30 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 32 |
3 files changed, 62 insertions, 11 deletions
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index be95c947d..31f9b9c41 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -147,6 +147,7 @@ void AstPrinter::toStream(std::ostream& out, tryToStream<PushCommand>(out, c) || tryToStream<PopCommand>(out, c) || tryToStream<CheckSatCommand>(out, c) || + tryToStream<CheckSatAssumingCommand>(out, c) || tryToStream<QueryCommand>(out, c) || tryToStream<ResetCommand>(out, c) || tryToStream<ResetAssertionsCommand>(out, c) || @@ -237,6 +238,14 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) } } +static void toStream(std::ostream& out, const CheckSatAssumingCommand* c) +{ + const vector<Expr>& terms = c->getTerms(); + out << "CheckSatAssuming( << "; + copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", ")); + out << ">> )"; +} + static void toStream(std::ostream& out, const QueryCommand* c) { out << "Query(" << c->getExpr() << ')'; @@ -333,7 +342,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c) out << "GetValue( << "; const vector<Expr>& terms = c->getTerms(); copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", ")); - out << " >> )"; + out << ">> )"; } static void toStream(std::ostream& out, const GetModelCommand* c) diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 27105c3b4..d778ccc2b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -2,9 +2,9 @@ /*! \file cvc_printer.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds + ** Morgan Deters, Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -955,6 +955,7 @@ void CvcPrinter::toStream(std::ostream& out, tryToStream<PushCommand>(out, c, d_cvc3Mode) || tryToStream<PopCommand>(out, c, d_cvc3Mode) || tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) || + tryToStream<CheckSatAssumingCommand>(out, c, d_cvc3Mode) || tryToStream<QueryCommand>(out, c, d_cvc3Mode) || tryToStream<ResetCommand>(out, c, d_cvc3Mode) || tryToStream<ResetAssertionsCommand>(out, c, d_cvc3Mode) || @@ -1159,6 +1160,31 @@ static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode) } } +static void toStream(std::ostream& out, + const CheckSatAssumingCommand* c, + bool cvc3Mode) +{ + const vector<Expr>& exprs = c->getTerms(); + if (cvc3Mode) + { + out << "PUSH; "; + } + out << "CHECKSAT"; + if (exprs.size() > 0) + { + out << " " << exprs[0]; + for (size_t i = 1, n = exprs.size(); i < n; ++i) + { + out << " AND " << exprs[i]; + } + } + out << ";"; + if (cvc3Mode) + { + out << " POP;"; + } +} + static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) { Expr e = c->getExpr(); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e06f8c062..e025c64f1 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -2,9 +2,9 @@ /*! \file smt2_printer.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Martin Brain + ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -1191,7 +1191,8 @@ void Smt2Printer::toStream(std::ostream& out, if (tryToStream<AssertCommand>(out, c) || tryToStream<PushCommand>(out, c) || tryToStream<PopCommand>(out, c) || tryToStream<CheckSatCommand>(out, c) - || tryToStream<QueryCommand>(out, c) + || tryToStream<CheckSatAssumingCommand>(out, c) + || tryToStream<QueryCommand>(out, c, d_variant) || tryToStream<ResetCommand>(out, c) || tryToStream<ResetAssertionsCommand>(out, c) || tryToStream<QuitCommand>(out, c) @@ -1511,14 +1512,29 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) } } -static void toStream(std::ostream& out, const QueryCommand* c) +static void toStream(std::ostream& out, const CheckSatAssumingCommand* c) +{ + out << "(check-sat-assuming ( "; + const vector<Expr>& terms = c->getTerms(); + copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " ")); + out << "))"; +} + +static void toStream(std::ostream& out, const QueryCommand* c, Variant v) { Expr e = c->getExpr(); if(!e.isNull()) { - out << PushCommand() << endl - << AssertCommand(BooleanSimplification::negate(e)) << endl - << CheckSatCommand() << endl - << PopCommand(); + if (v == smt2_0_variant) + { + out << PushCommand() << endl + << AssertCommand(BooleanSimplification::negate(e)) << endl + << CheckSatCommand() << endl + << PopCommand(); + } + else + { + out << CheckSatAssumingCommand(e.notExpr()) << endl; + } } else { out << "(check-sat)"; } |