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)).

diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index 90b69b10abd78f605b7a1a8d00fbcf7e2b3b7c2a..a245d489069a5d124269ca87d948cae2ec6184de 100644 (file)
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -2,9 +2,9 @@
 /*! \file bitvectors.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Morgan Deters, Paul Meng
+ **   Liana Hadarean, Morgan Deters, Aina Niemetz
  ** 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
@@ -107,5 +107,10 @@ int main() {
   cout << " Expect valid. " << endl;
   cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl;
 
+  Expr x_neq_x = em.mkExpr(kind::EQUAL, x, x).notExpr();
+  std::vector<Expr> v{new_x_eq_new_x_, x_neq_x};
+  cout << " Querying: " << v << endl;
+  cout << " Expect invalid. " << endl;
+  cout << " CVC4: " << smt.query(v) << endl;
   return 0;
 }

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 6bcd1502767b8a4d857253c85bce81d91510db5f..010b36e94c7a79850d311295855ac4a0966545a0 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Kshitij Bansal, 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

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 8cc87cfff58d80262ffbe8bcf4ecccd6edebaeb6..cb4534c08af134180eb478cd1731e78cfa25e08d 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -2,9 +2,9 @@
 /*! \file expr_template.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Christopher L. Conway
+ **   Morgan Deters, Dejan Jovanovic, 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

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b9a2a880568fc6c0cf2edf029ee5a067b2b0eece..8893522995982b7a7d6fe4818018fcff202c48b1 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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
@@ -431,7 +431,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       }
     }
   | /* check-sat */
-    CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { if( PARSER_STATE->sygus() ){
         PARSER_STATE->parseError("Sygus does not support check-sat command.");
       }
@@ -446,6 +446,16 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     | { expr = MK_CONST(bool(true)); }
     )
     { cmd->reset(new CheckSatCommand(expr)); }
+  | /* check-sat-assuming */
+    CHECK_SAT_ASSUMING_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
+      { cmd->reset(new CheckSatAssumingCommand(terms)); }
+    | ~LPAREN_TOK
+      { PARSER_STATE->parseError("The check-sat-assuming command expects a "
+                                 "list of terms.  Perhaps you forgot a pair of "
+                                 "parentheses?");
+      }
+    )
   | /* get-assertions */
     GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd->reset(new GetAssertionsCommand()); }
@@ -1276,7 +1286,6 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       }
       cmd->reset( new DefineFunctionRecCommand(funcs,formals,func_defs));
     }
-  // CHECK_SAT_ASSUMING still being discussed
   // GET_UNSAT_ASSUMPTIONS
   ;
 
@@ -1713,7 +1722,8 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
 //  }
   | symbol[s,CHECK_NONE,SYM_SORT]
     { sexpr = SExpr(SExpr::Keyword(s)); }
-  | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK
+  | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
+        | DECLARE_SORT_TOK
         | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
         | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK
         | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK
@@ -3064,7 +3074,8 @@ selector[CVC4::DatatypeConstructor& ctor]
 
 // Base SMT-LIB tokens
 ASSERT_TOK : 'assert';
-CHECKSAT_TOK : 'check-sat';
+CHECK_SAT_TOK : 'check-sat';
+CHECK_SAT_ASSUMING_TOK : 'check-sat-assuming';
 DECLARE_FUN_TOK : 'declare-fun';
 DECLARE_SORT_TOK : 'declare-sort';
 DEFINE_FUN_TOK : 'define-fun';

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index be95c947dd537f31fa27f2cbff92e56d1b5652b6..31f9b9c41dc0fbb831e8bd50d4758f6898b81041 100644 (file)
--- 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 27105c3b4693df70cad9a809c86d577bcc58b01d..d778ccc2b1db39e8b9869db1d1ac8dbfeec841fa 100644 (file)
--- 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 e06f8c0625185a7d1d78c8879542a54290c03b84..e025c64f1bfa2b8737ce1dc028054fdf5e66de30 100644 (file)
--- 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)";
   }

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 040d8725035723796bd7de7e8d05191b5f690091..e61ea868f10ab80da140bf25d73dd22d09e3fdc0 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2,9 +2,9 @@
 /*! \file command.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Francois Bobot
+ **   Tim King, Morgan Deters, Aina Niemetz
  ** 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
@@ -104,7 +104,25 @@ ostream& operator<<(ostream& out, const CommandStatus* s)
   return out;
 }
 
-/* class CommandPrintSuccess */
+
+/* output stream insertion operator for benchmark statuses */
+std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
+{
+  switch (status)
+  {
+    case SMT_SATISFIABLE: return out << "sat";
+
+    case SMT_UNSATISFIABLE: return out << "unsat";
+
+    case SMT_UNKNOWN: return out << "unknown";
+
+    default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
+  }
+}
+
+/* -------------------------------------------------------------------------- */
+/* class CommandPrintSuccess                                                  */
+/* -------------------------------------------------------------------------- */
 
 void CommandPrintSuccess::applyPrintSuccess(std::ostream& out)
 {
@@ -127,7 +145,9 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
   return out;
 }
 
-/* class Command */
+/* -------------------------------------------------------------------------- */
+/* class Command                                                              */
+/* -------------------------------------------------------------------------- */
 
 Command::Command() : d_commandStatus(NULL), d_muted(false) {}
 Command::Command(const Command& cmd)
@@ -208,7 +228,9 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const
   }
 }
 
-/* class EmptyCommand */
+/* -------------------------------------------------------------------------- */
+/* class EmptyCommand                                                         */
+/* -------------------------------------------------------------------------- */
 
 EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
 std::string EmptyCommand::getName() const { return d_name; }
@@ -226,7 +248,10 @@ Command* EmptyCommand::exportTo(ExprManager* exprManager,
 
 Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
 std::string EmptyCommand::getCommandName() const { return "empty"; }
-/* class EchoCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class EchoCommand                                                          */
+/* -------------------------------------------------------------------------- */
 
 EchoCommand::EchoCommand(std::string output) : d_output(output) {}
 std::string EchoCommand::getOutput() const { return d_output; }
@@ -254,7 +279,10 @@ Command* EchoCommand::exportTo(ExprManager* exprManager,
 
 Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
 std::string EchoCommand::getCommandName() const { return "echo"; }
-/* class AssertCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class AssertCommand                                                        */
+/* -------------------------------------------------------------------------- */
 
 AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore)
     : d_expr(e), d_inUnsatCore(inUnsatCore)
@@ -292,7 +320,10 @@ Command* AssertCommand::clone() const
 }
 
 std::string AssertCommand::getCommandName() const { return "assert"; }
-/* class PushCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class PushCommand                                                          */
+/* -------------------------------------------------------------------------- */
 
 void PushCommand::invoke(SmtEngine* smtEngine)
 {
@@ -319,7 +350,10 @@ Command* PushCommand::exportTo(ExprManager* exprManager,
 
 Command* PushCommand::clone() const { return new PushCommand(); }
 std::string PushCommand::getCommandName() const { return "push"; }
-/* class PopCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class PopCommand                                                           */
+/* -------------------------------------------------------------------------- */
 
 void PopCommand::invoke(SmtEngine* smtEngine)
 {
@@ -346,7 +380,10 @@ Command* PopCommand::exportTo(ExprManager* exprManager,
 
 Command* PopCommand::clone() const { return new PopCommand(); }
 std::string PopCommand::getCommandName() const { return "pop"; }
-/* class CheckSatCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class CheckSatCommand                                                      */
+/* -------------------------------------------------------------------------- */
 
 CheckSatCommand::CheckSatCommand() : d_expr() {}
 CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore)
@@ -398,7 +435,90 @@ Command* CheckSatCommand::clone() const
 }
 
 std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
-/* class QueryCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class CheckSatAssumingCommand                                              */
+/* -------------------------------------------------------------------------- */
+
+CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms()
+{
+  d_terms.push_back(term);
+}
+
+CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms,
+                                                 bool inUnsatCore)
+    : d_terms(terms), d_inUnsatCore(inUnsatCore)
+{
+  PrettyCheckArgument(
+      terms.size() >= 1, terms, "cannot get-value of an empty set of terms");
+}
+
+const std::vector<Expr>& CheckSatAssumingCommand::getTerms() const
+{
+  return d_terms;
+}
+
+void CheckSatAssumingCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    d_result = smtEngine->checkSat(d_terms);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Result CheckSatAssumingCommand::getResult() const
+{
+  return d_result;
+}
+
+void CheckSatAssumingCommand::printResult(std::ostream& out,
+                                          uint32_t verbosity) const
+{
+  if (!ok())
+  {
+    this->Command::printResult(out, verbosity);
+  }
+  else
+  {
+    out << d_result << endl;
+  }
+}
+
+Command* CheckSatAssumingCommand::exportTo(
+    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+  vector<Expr> exportedTerms;
+  for (const Expr& e : d_terms)
+  {
+    exportedTerms.push_back(e.exportTo(exprManager, variableMap));
+  }
+  CheckSatAssumingCommand* c =
+      new CheckSatAssumingCommand(exportedTerms, d_inUnsatCore);
+  c->d_result = d_result;
+  return c;
+}
+
+Command* CheckSatAssumingCommand::clone() const
+{
+  CheckSatAssumingCommand* c =
+      new CheckSatAssumingCommand(d_terms, d_inUnsatCore);
+  c->d_result = d_result;
+  return c;
+}
+
+std::string CheckSatAssumingCommand::getCommandName() const
+{
+  return "check-sat-assuming";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class QueryCommand                                                         */
+/* -------------------------------------------------------------------------- */
 
 QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore)
     : d_expr(e), d_inUnsatCore(inUnsatCore)
@@ -449,7 +569,10 @@ Command* QueryCommand::clone() const
 }
 
 std::string QueryCommand::getCommandName() const { return "query"; }
-/* class CheckSynthCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class CheckSynthCommand                                                    */
+/* -------------------------------------------------------------------------- */
 
 CheckSynthCommand::CheckSynthCommand() : d_expr() {}
 CheckSynthCommand::CheckSynthCommand(const Expr& expr) : d_expr(expr) {}
@@ -524,7 +647,10 @@ Command* CheckSynthCommand::clone() const
 }
 
 std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
-/* class ResetCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class ResetCommand                                                         */
+/* -------------------------------------------------------------------------- */
 
 void ResetCommand::invoke(SmtEngine* smtEngine)
 {
@@ -547,7 +673,10 @@ Command* ResetCommand::exportTo(ExprManager* exprManager,
 
 Command* ResetCommand::clone() const { return new ResetCommand(); }
 std::string ResetCommand::getCommandName() const { return "reset"; }
-/* class ResetAssertionsCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class ResetAssertionsCommand                                               */
+/* -------------------------------------------------------------------------- */
 
 void ResetAssertionsCommand::invoke(SmtEngine* smtEngine)
 {
@@ -578,7 +707,9 @@ std::string ResetAssertionsCommand::getCommandName() const
   return "reset-assertions";
 }
 
-/* class QuitCommand */
+/* -------------------------------------------------------------------------- */
+/* class QuitCommand                                                          */
+/* -------------------------------------------------------------------------- */
 
 void QuitCommand::invoke(SmtEngine* smtEngine)
 {
@@ -594,7 +725,10 @@ Command* QuitCommand::exportTo(ExprManager* exprManager,
 
 Command* QuitCommand::clone() const { return new QuitCommand(); }
 std::string QuitCommand::getCommandName() const { return "exit"; }
-/* class CommentCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class CommentCommand                                                       */
+/* -------------------------------------------------------------------------- */
 
 CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
 std::string CommentCommand::getComment() const { return d_comment; }
@@ -612,7 +746,10 @@ Command* CommentCommand::exportTo(ExprManager* exprManager,
 
 Command* CommentCommand::clone() const { return new CommentCommand(d_comment); }
 std::string CommentCommand::getCommandName() const { return "comment"; }
-/* class CommandSequence */
+
+/* -------------------------------------------------------------------------- */
+/* class CommandSequence                                                      */
+/* -------------------------------------------------------------------------- */
 
 CommandSequence::CommandSequence() : d_index(0) {}
 CommandSequence::~CommandSequence()
@@ -712,9 +849,10 @@ CommandSequence::iterator CommandSequence::end()
 }
 
 std::string CommandSequence::getCommandName() const { return "sequence"; }
-/* class DeclarationSequenceCommand */
 
-/* class DeclarationDefinitionCommand */
+/* -------------------------------------------------------------------------- */
+/* class DeclarationDefinitionCommand                                         */
+/* -------------------------------------------------------------------------- */
 
 DeclarationDefinitionCommand::DeclarationDefinitionCommand(
     const std::string& id)
@@ -723,7 +861,10 @@ DeclarationDefinitionCommand::DeclarationDefinitionCommand(
 }
 
 std::string DeclarationDefinitionCommand::getSymbol() const { return d_symbol; }
-/* class DeclareFunctionCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareFunctionCommand                                               */
+/* -------------------------------------------------------------------------- */
 
 DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id,
                                                Expr func,
@@ -781,7 +922,9 @@ std::string DeclareFunctionCommand::getCommandName() const
   return "declare-fun";
 }
 
-/* class DeclareTypeCommand */
+/* -------------------------------------------------------------------------- */
+/* class DeclareTypeCommand                                                   */
+/* -------------------------------------------------------------------------- */
 
 DeclareTypeCommand::DeclareTypeCommand(const std::string& id,
                                        size_t arity,
@@ -814,7 +957,9 @@ std::string DeclareTypeCommand::getCommandName() const
   return "declare-sort";
 }
 
-/* class DefineTypeCommand */
+/* -------------------------------------------------------------------------- */
+/* class DefineTypeCommand                                                    */
+/* -------------------------------------------------------------------------- */
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id, Type t)
     : DeclarationDefinitionCommand(id), d_params(), d_type(t)
@@ -857,7 +1002,10 @@ Command* DefineTypeCommand::clone() const
 }
 
 std::string DefineTypeCommand::getCommandName() const { return "define-sort"; }
-/* class DefineFunctionCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class DefineFunctionCommand                                                */
+/* -------------------------------------------------------------------------- */
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                              Expr func,
@@ -927,7 +1075,9 @@ std::string DefineFunctionCommand::getCommandName() const
   return "define-fun";
 }
 
-/* class DefineNamedFunctionCommand */
+/* -------------------------------------------------------------------------- */
+/* class DefineNamedFunctionCommand                                           */
+/* -------------------------------------------------------------------------- */
 
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(
     const std::string& id,
@@ -967,7 +1117,9 @@ Command* DefineNamedFunctionCommand::clone() const
   return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula);
 }
 
-/* class DefineFunctionRecCommand */
+/* -------------------------------------------------------------------------- */
+/* class DefineFunctionRecCommand                                             */
+/* -------------------------------------------------------------------------- */
 
 DefineFunctionRecCommand::DefineFunctionRecCommand(
     Expr func, const std::vector<Expr>& formals, Expr formula)
@@ -979,7 +1131,7 @@ DefineFunctionRecCommand::DefineFunctionRecCommand(
 
 DefineFunctionRecCommand::DefineFunctionRecCommand(
     const std::vector<Expr>& funcs,
-    const std::vector<std::vector<Expr> >& formals,
+    const std::vector<std::vector<Expr>>& formals,
     const std::vector<Expr>& formulas)
 {
   d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end());
@@ -992,7 +1144,7 @@ const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const
   return d_funcs;
 }
 
-const std::vector<std::vector<Expr> >& DefineFunctionRecCommand::getFormals()
+const std::vector<std::vector<Expr>>& DefineFunctionRecCommand::getFormals()
     const
 {
   return d_formals;
@@ -1026,7 +1178,7 @@ Command* DefineFunctionRecCommand::exportTo(
         exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED);
     funcs.push_back(func);
   }
-  std::vector<std::vector<Expr> > formals;
+  std::vector<std::vector<Expr>> formals;
   for (unsigned i = 0, size = d_formals.size(); i < size; i++)
   {
     std::vector<Expr> formals_c;
@@ -1055,7 +1207,9 @@ std::string DefineFunctionRecCommand::getCommandName() const
   return "define-fun-rec";
 }
 
-/* class SetUserAttribute */
+/* -------------------------------------------------------------------------- */
+/* class SetUserAttribute                                                     */
+/* -------------------------------------------------------------------------- */
 
 SetUserAttributeCommand::SetUserAttributeCommand(
     const std::string& attr,
@@ -1122,7 +1276,9 @@ std::string SetUserAttributeCommand::getCommandName() const
   return "set-user-attribute";
 }
 
-/* class SimplifyCommand */
+/* -------------------------------------------------------------------------- */
+/* class SimplifyCommand                                                      */
+/* -------------------------------------------------------------------------- */
 
 SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) {}
 Expr SimplifyCommand::getTerm() const { return d_term; }
@@ -1173,7 +1329,10 @@ Command* SimplifyCommand::clone() const
 }
 
 std::string SimplifyCommand::getCommandName() const { return "simplify"; }
-/* class ExpandDefinitionsCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class ExpandDefinitionsCommand                                             */
+/* -------------------------------------------------------------------------- */
 
 ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) : d_term(term) {}
 Expr ExpandDefinitionsCommand::getTerm() const { return d_term; }
@@ -1218,7 +1377,9 @@ std::string ExpandDefinitionsCommand::getCommandName() const
   return "expand-definitions";
 }
 
-/* class GetValueCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetValueCommand                                                      */
+/* -------------------------------------------------------------------------- */
 
 GetValueCommand::GetValueCommand(Expr term) : d_terms()
 {
@@ -1240,15 +1401,13 @@ void GetValueCommand::invoke(SmtEngine* smtEngine)
     vector<Expr> result;
     ExprManager* em = smtEngine->getExprManager();
     NodeManager* nm = NodeManager::fromExprManager(em);
-    for (std::vector<Expr>::const_iterator i = d_terms.begin();
-         i != d_terms.end();
-         ++i)
+    for (const Expr& e : d_terms)
     {
-      Assert(nm == NodeManager::fromExprManager((*i).getExprManager()));
+      Assert(nm == NodeManager::fromExprManager(e.getExprManager()));
       smt::SmtScope scope(smtEngine);
       Node request = Node::fromExpr(
-          options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
-      Node value = Node::fromExpr(smtEngine->getValue(*i));
+          options::expandDefinitions() ? smtEngine->expandDefinitions(e) : e);
+      Node value = Node::fromExpr(smtEngine->getValue(e));
       if (value.getType().isInteger() && request.getType() == nm->realType())
       {
         // Need to wrap in special marker so that output printers know this
@@ -1314,14 +1473,17 @@ Command* GetValueCommand::clone() const
 }
 
 std::string GetValueCommand::getCommandName() const { return "get-value"; }
-/* class GetAssignmentCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class GetAssignmentCommand                                                 */
+/* -------------------------------------------------------------------------- */
 
 GetAssignmentCommand::GetAssignmentCommand() {}
 void GetAssignmentCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    std::vector<std::pair<Expr,Expr>> assignments  = smtEngine->getAssignment();
+    std::vector<std::pair<Expr, Expr>> assignments = smtEngine->getAssignment();
     vector<SExpr> sexprs;
     for (const auto& p : assignments)
     {
@@ -1388,7 +1550,9 @@ std::string GetAssignmentCommand::getCommandName() const
   return "get-assignment";
 }
 
-/* class GetModelCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetModelCommand                                                      */
+/* -------------------------------------------------------------------------- */
 
 GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
 void GetModelCommand::invoke(SmtEngine* smtEngine)
@@ -1449,7 +1613,10 @@ Command* GetModelCommand::clone() const
 }
 
 std::string GetModelCommand::getCommandName() const { return "get-model"; }
-/* class GetProofCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class GetProofCommand                                                      */
+/* -------------------------------------------------------------------------- */
 
 GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {}
 void GetProofCommand::invoke(SmtEngine* smtEngine)
@@ -1506,7 +1673,10 @@ Command* GetProofCommand::clone() const
 }
 
 std::string GetProofCommand::getCommandName() const { return "get-proof"; }
-/* class GetInstantiationsCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class GetInstantiationsCommand                                             */
+/* -------------------------------------------------------------------------- */
 
 GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
 void GetInstantiationsCommand::invoke(SmtEngine* smtEngine)
@@ -1557,7 +1727,9 @@ std::string GetInstantiationsCommand::getCommandName() const
   return "get-instantiations";
 }
 
-/* class GetSynthSolutionCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetSynthSolutionCommand                                              */
+/* -------------------------------------------------------------------------- */
 
 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
 void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine)
@@ -1606,7 +1778,9 @@ std::string GetSynthSolutionCommand::getCommandName() const
   return "get-instantiations";
 }
 
-/* class GetQuantifierEliminationCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetQuantifierEliminationCommand                                      */
+/* -------------------------------------------------------------------------- */
 
 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() : d_expr() {}
 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
@@ -1666,7 +1840,9 @@ std::string GetQuantifierEliminationCommand::getCommandName() const
   return d_doFull ? "get-qe" : "get-qe-disjunct";
 }
 
-/* class GetUnsatCoreCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetUnsatCoreCommand                                                  */
+/* -------------------------------------------------------------------------- */
 
 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine)
@@ -1725,7 +1901,9 @@ std::string GetUnsatCoreCommand::getCommandName() const
   return "get-unsat-core";
 }
 
-/* class GetAssertionsCommand */
+/* -------------------------------------------------------------------------- */
+/* class GetAssertionsCommand                                                 */
+/* -------------------------------------------------------------------------- */
 
 GetAssertionsCommand::GetAssertionsCommand() {}
 void GetAssertionsCommand::invoke(SmtEngine* smtEngine)
@@ -1780,7 +1958,9 @@ std::string GetAssertionsCommand::getCommandName() const
   return "get-assertions";
 }
 
-/* class SetBenchmarkStatusCommand */
+/* -------------------------------------------------------------------------- */
+/* class SetBenchmarkStatusCommand                                            */
+/* -------------------------------------------------------------------------- */
 
 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status)
     : d_status(status)
@@ -1824,7 +2004,9 @@ std::string SetBenchmarkStatusCommand::getCommandName() const
   return "set-info";
 }
 
-/* class SetBenchmarkLogicCommand */
+/* -------------------------------------------------------------------------- */
+/* class SetBenchmarkLogicCommand                                             */
+/* -------------------------------------------------------------------------- */
 
 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
     : d_logic(logic)
@@ -1861,7 +2043,9 @@ std::string SetBenchmarkLogicCommand::getCommandName() const
   return "set-logic";
 }
 
-/* class SetInfoCommand */
+/* -------------------------------------------------------------------------- */
+/* class SetInfoCommand                                                       */
+/* -------------------------------------------------------------------------- */
 
 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
     : d_flag(flag), d_sexpr(sexpr)
@@ -1900,7 +2084,10 @@ Command* SetInfoCommand::clone() const
 }
 
 std::string SetInfoCommand::getCommandName() const { return "set-info"; }
-/* class GetInfoCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class GetInfoCommand                                                       */
+/* -------------------------------------------------------------------------- */
 
 GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
 std::string GetInfoCommand::getFlag() const { return d_flag; }
@@ -1959,7 +2146,10 @@ Command* GetInfoCommand::clone() const
 }
 
 std::string GetInfoCommand::getCommandName() const { return "get-info"; }
-/* class SetOptionCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class SetOptionCommand                                                     */
+/* -------------------------------------------------------------------------- */
 
 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
     : d_flag(flag), d_sexpr(sexpr)
@@ -1997,7 +2187,10 @@ Command* SetOptionCommand::clone() const
 }
 
 std::string SetOptionCommand::getCommandName() const { return "set-option"; }
-/* class GetOptionCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class GetOptionCommand                                                     */
+/* -------------------------------------------------------------------------- */
 
 GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
 std::string GetOptionCommand::getFlag() const { return d_flag; }
@@ -2048,7 +2241,10 @@ Command* GetOptionCommand::clone() const
 }
 
 std::string GetOptionCommand::getCommandName() const { return "get-option"; }
-/* class SetExpressionNameCommand */
+
+/* -------------------------------------------------------------------------- */
+/* class SetExpressionNameCommand                                             */
+/* -------------------------------------------------------------------------- */
 
 SetExpressionNameCommand::SetExpressionNameCommand(Expr expr, std::string name)
     : d_expr(expr), d_name(name)
@@ -2080,7 +2276,9 @@ std::string SetExpressionNameCommand::getCommandName() const
   return "set-expr-name";
 }
 
-/* class DatatypeDeclarationCommand */
+/* -------------------------------------------------------------------------- */
+/* class DatatypeDeclarationCommand                                           */
+/* -------------------------------------------------------------------------- */
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
     const DatatypeType& datatype)
@@ -2123,7 +2321,9 @@ std::string DatatypeDeclarationCommand::getCommandName() const
   return "declare-datatypes";
 }
 
-/* class RewriteRuleCommand */
+/* -------------------------------------------------------------------------- */
+/* class RewriteRuleCommand                                                   */
+/* -------------------------------------------------------------------------- */
 
 RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars,
                                        const std::vector<Expr>& guards,
@@ -2235,7 +2435,9 @@ std::string RewriteRuleCommand::getCommandName() const
   return "rewrite-rule";
 }
 
-/* class PropagateRuleCommand */
+/* -------------------------------------------------------------------------- */
+/* class PropagateRuleCommand                                                 */
+/* -------------------------------------------------------------------------- */
 
 PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars,
                                            const std::vector<Expr>& guards,
@@ -2366,20 +2568,4 @@ std::string PropagateRuleCommand::getCommandName() const
 {
   return "propagate-rule";
 }
-
-/* output stream insertion operator for benchmark statuses */
-std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
-{
-  switch (status)
-  {
-    case SMT_SATISFIABLE: return out << "sat";
-
-    case SMT_UNSATISFIABLE: return out << "unsat";
-
-    case SMT_UNKNOWN: return out << "unknown";
-
-    default: return out << "BenchmarkStatus::[UNKNOWNSTATUS!]";
-  }
-}
-
-} /* CVC4 namespace */
+}  // namespace CVC4

diff --git a/src/smt/command.h b/src/smt/command.h
index 9573e1c220065985aa25485f038501414089cc47..19bf9fddd60cb828e33a836c9140d35a5d7b6a56 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -2,9 +2,9 @@
 /*! \file command.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Andres Noetzli
+ **   Tim King, Morgan Deters, Andrew Reynolds
  ** 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
@@ -544,13 +544,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command
   const std::string d_str_value;
 }; /* class SetUserAttributeCommand */
 
+/**
+ * The command when parsing check-sat.
+ * This command will check satisfiability of the input formula.
+ */
 class CVC4_PUBLIC CheckSatCommand : public Command
 {
- protected:
-  Expr d_expr;
-  Result d_result;
-  bool d_inUnsatCore;
-
  public:
   CheckSatCommand();
   CheckSatCommand(const Expr& expr, bool inUnsatCore = true);
@@ -563,8 +562,40 @@ class CVC4_PUBLIC CheckSatCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+
+ private:
+  Expr d_expr;
+  Result d_result;
+  bool d_inUnsatCore;
 }; /* class CheckSatCommand */
 
+/**
+ * The command when parsing check-sat-assuming.
+ * This command will assume a set of formulas and check satisfiability of the
+ * input formula under these assumptions.
+ */
+class CVC4_PUBLIC CheckSatAssumingCommand : public Command
+{
+ public:
+  CheckSatAssumingCommand(Expr term);
+  CheckSatAssumingCommand(const std::vector<Expr>& terms,
+                          bool inUnsatCore = true);
+
+  const std::vector<Expr>& getTerms() const;
+  Result getResult() const;
+  void invoke(SmtEngine* smtEngine) override;
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+
+ private:
+  std::vector<Expr> d_terms;
+  Result d_result;
+  bool d_inUnsatCore;
+}; /* class CheckSatAssumingCommand */
+
 class CVC4_PUBLIC QueryCommand : public Command
 {
  protected:

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 19236f8815d23082141794d3d89c94a2bb388a65..6e90ab1524e5ef01bc214e82e440a6969db430b5 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2,9 +2,9 @@
 /*! \file smt_engine.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Andrew Reynolds
+ **   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
@@ -4683,22 +4683,46 @@ void SmtEngine::ensureBoolean(const Expr& e)
 Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore)
 {
   return checkSatisfiability(ex, inUnsatCore, false);
-} /* SmtEngine::checkSat() */
+}
+
+Result SmtEngine::checkSat(const vector<Expr>& exprs, bool inUnsatCore)
+{
+  return checkSatisfiability(exprs, inUnsatCore, false);
+}
 
 Result SmtEngine::query(const Expr& ex, bool inUnsatCore)
 {
   Assert(!ex.isNull());
   return checkSatisfiability(ex, inUnsatCore, true);
-} /* SmtEngine::query() */
+}
 
-Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQuery) {
-  try {
-    Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
+Result SmtEngine::query(const vector<Expr>& exprs, bool inUnsatCore)
+{
+  return checkSatisfiability(exprs, inUnsatCore, true);
+}
+
+Result SmtEngine::checkSatisfiability(const Expr& expr,
+                                      bool inUnsatCore,
+                                      bool isQuery)
+{
+  return checkSatisfiability(
+      expr.isNull() ? vector<Expr>() : vector<Expr>{expr},
+      inUnsatCore,
+      isQuery);
+}
+
+Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs,
+                                      bool inUnsatCore,
+                                      bool isQuery)
+{
+  try
+  {
     SmtScope smts(this);
     finalOptionsAreSet();
     doPendingPops();
 
-    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << ex << ")" << endl;
+    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
+                 << exprs << ")" << endl;
 
     if(d_queryMade && !options::incrementalSolving()) {
       throw ModalException("Cannot make multiple queries unless "
@@ -4706,45 +4730,64 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ
                            "(try --incremental)");
     }
 
-    Expr e;
-    if(!ex.isNull()) {
-      // Substitute out any abstract values in ex.
-      e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-      // Ensure expr is type-checked at this point.
-      ensureBoolean(e);
-    }
-
     // check to see if a postsolve() is pending
     if(d_needPostsolve) {
       d_theoryEngine->postsolve();
       d_needPostsolve = false;
     }
-
     // Note that a query has been made
     d_queryMade = true;
-
     // reset global negation
     d_globalNegation = false;
 
     bool didInternalPush = false;
-    // Add the formula
-    if(!e.isNull()) {
-      // Push the context
+
+    vector<Expr> t_exprs;
+    if (isQuery)
+    {
+      size_t size = exprs.size();
+      if (size > 1)
+      {
+        /* Assume: not (BIGAND exprs)  */
+        t_exprs.push_back(d_exprManager->mkExpr(kind::AND, exprs).notExpr());
+      }
+      else if (size == 1)
+      {
+        /* Assume: not expr  */
+        t_exprs.push_back(exprs[0].notExpr());
+      }
+    }
+    else
+    {
+      /* Assume: BIGAND exprs  */
+      t_exprs = exprs;
+    }
+
+    Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+    for (Expr e : t_exprs)
+    {
+      // Substitute out any abstract values in ex.
+      e = d_private->substituteAbstractValues(Node::fromExpr(e)).toExpr();
+      Assert(e.getExprManager() == d_exprManager);
+      // Ensure expr is type-checked at this point.
+      ensureBoolean(e);
+
+      /* Add assumption  */
       internalPush();
       didInternalPush = true;
-
       d_problemExtended = true;
-      Expr ea = isQuery ? e.notExpr() : e;
-      if(d_assertionList != NULL) {
-        d_assertionList->push_back(ea);
+      if (d_assertionList != NULL)
+      {
+        d_assertionList->push_back(e);
       }
-      d_private->addFormula(ea.getNode(), inUnsatCore);
+      d_private->addFormula(e.getNode(), inUnsatCore);
     }
 
-    Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
     r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult();
 
-    if ( ( options::solveRealAsInt() || options::solveIntAsBV() > 0 ) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+    if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
+        && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    {
       r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
     }
     // flipped if we did a global negation
@@ -4773,12 +4816,16 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ
     d_needPostsolve = true;
 
     // Dump the query if requested
-    if(Dump.isOn("benchmark")) {
+    if (Dump.isOn("benchmark"))
+    {
       // the expr already got dumped out if assertion-dumping is on
-      if( isQuery ){
-        Dump("benchmark") << QueryCommand(ex);
-      }else{
-        Dump("benchmark") << CheckSatCommand(ex);
+      if (isQuery && exprs.size() == 1)
+      {
+        Dump("benchmark") << QueryCommand(exprs[0]);
+      }
+      else
+      {
+        Dump("benchmark") << CheckSatAssumingCommand(t_exprs, inUnsatCore);
       }
     }
 
@@ -4793,7 +4840,8 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ
 
     d_problemExtended = false;
 
-    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << e << ") => " << r << endl;
+    Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "("
+                 << exprs << ") => " << r << endl;
 
     // Check that SAT results generate a model correctly.
     if(options::checkModels()) {

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 16cf90de144abeb1bddb53c5021b79ac85571ffa..bba6b1cef849fa6e0bb56bf1598a3662cfd5aa8d 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -400,7 +400,12 @@ class CVC4_PUBLIC SmtEngine {
   SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
 
   //check satisfiability (for query and check-sat)
-  Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery);
+  Result checkSatisfiability(const Expr& expr,
+                             bool inUnsatCore,
+                             bool isQuery);
+  Result checkSatisfiability(const std::vector<Expr>& exprs,
+                             bool inUnsatCore,
+                             bool isQuery);
 
   /**
    * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
@@ -535,7 +540,10 @@ class CVC4_PUBLIC SmtEngine {
    * of assertions by asserting the query expression's negation and
    * calling check().  Returns valid, invalid, or unknown result.
    */
-  Result query(const Expr& e, bool inUnsatCore = true) /* throw(Exception) */;
+  Result query(const Expr& e = Expr(),
+               bool inUnsatCore = true) /* throw(Exception) */;
+  Result query(const std::vector<Expr>& exprs,
+               bool inUnsatCore = true) /* throw(Exception) */;
 
   /**
    * Assert a formula (if provided) to the current context and call
@@ -543,6 +551,8 @@ class CVC4_PUBLIC SmtEngine {
    */
   Result checkSat(const Expr& e = Expr(),
                   bool inUnsatCore = true) /* throw(Exception) */;
+  Result checkSat(const std::vector<Expr>& exprs,
+                  bool inUnsatCore = true) /* throw(Exception) */;
 
   /**
    * Assert a synthesis conjecture to the current context and call

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 06225dfb687266e24e64964681ff2dff9df646ef..b78c48549309bfbdbe6b898935fe5eaec23e3aff 100644 (file)
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -39,7 +39,8 @@ BUG_TESTS = \
        inc-define.smt2 \
        bug691.smt2 \
        simple_unsat_cores.smt2 \
-       bug821.smt2
+       bug821.smt2 \
+       bug821-check_sat_assuming.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2 b/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2
new file mode 100644 (file)
index 0000000..50e4406
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic UF)
+(declare-fun _substvar_4_ () Bool)
+(check-sat-assuming (_substvar_4_ _substvar_4_))
+(check-sat-assuming (_substvar_4_ false))
+(check-sat-assuming ((= _substvar_4_ _substvar_4_)))