* re-enable some Z3 extended commands:

  declare-const
  declare-funs
  declare-preds
  define
  simplify

* don't output --help on bad options, just invite user to try --help

* Datatypes from SMT2 parser now name the tester is-cons (e.g.)

* unknown results produce models, --check-model doesn't fail hard for
  incorrect unknown models.  removed the assert that kept arithmetic
  from producing models if it saw nonlinear


(this commit was certified error- and warning-free by the test-and-commit script.)

6 files changed, 135 insertions, 18 deletions

diff --git a/RELEASE-NOTES b/RELEASE-NOTES
index 9eadf916a..9ad246a9c 100644
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -28,8 +28,9 @@ but may produce strange results.  For example:
   COUNTEREXAMPLE;
   % f : (INT) -> INT = LAMBDA(x1:INT) : 0;
 
-CVC3 can be used to produce TCCs for this input (with the +dump-tcc option),
-and the TCC can be checked with CVC4.
+CVC3 can be used to produce TCCs for this input (with the +dump-tcc option).
+The TCC can be checked by CVC3 or another solver.  (CVC3 can also check
+TCCs while solving with +tcc.)
 
 ** Changes in CVC's Presentation Language
 
@@ -75,7 +76,8 @@ processed.
 
 ** Getting statistics
 
-Statistics can be dumped on exit (both normal and abnormal exits)
+Statistics can be dumped on exit (both normal and abnormal exits) with
+the --statistics command line option.
 
 ** Time and resource limits
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index e3196bb4e..9fa1db7bc 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -59,8 +59,9 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts[options::out] << "unknown" << endl;
 #endif
-    cerr << "CVC4 Error:" << endl << e << endl;
-    printUsage(opts);
+    cerr << "CVC4 Error:" << endl << e << endl << endl
+         << "Please use --help to get help on command-line options."
+         << endl;
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
     *opts[options::out] << "unknown" << endl;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 1b778f87a..37b926c34 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -375,7 +375,9 @@ extendedCommand[CVC4::Command*& cmd]
   SExpr sexpr;
   std::string name;
   std::vector<std::string> names;
+  std::vector<Expr> terms;
   std::vector<Type> sorts;
+  std::vector<std::pair<std::string, Type> > sortedVarNames;
 }
     /* Extended SMT-LIBv2 set of commands syntax, not permitted in
      * --smtlib2 compliance mode. */
@@ -388,7 +390,7 @@ extendedCommand[CVC4::Command*& cmd]
       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
   | /* get model */
     GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetModelCommand; }      
+    { cmd = new GetModelCommand; }
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
       { std::stringstream ss;
@@ -398,6 +400,107 @@ extendedCommand[CVC4::Command*& cmd]
     | { cmd = new EchoCommand(); }
     )
   | rewriterulesCommand[cmd]
+
+    /* Support some of Z3's extended SMT-LIBv2 commands */
+
+  | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    sortSymbol[t,CHECK_DECLARED]
+    { Expr c = PARSER_STATE->mkVar(name, t);
+      $cmd = new DeclareFunctionCommand(name, c, t); }
+
+  | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { $cmd = new CommandSequence(); }
+    LPAREN_TOK
+    ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
+      { PARSER_STATE->checkUserSymbol(name);
+        Type type = PARSER_STATE->mkSort(name);
+        static_cast<CommandSequence*>($cmd)->addCommand(new DeclareTypeCommand(name, 0, type));
+      }
+    )+
+    RPAREN_TOK
+
+  | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { $cmd = new CommandSequence(); }
+    LPAREN_TOK
+    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+      { PARSER_STATE->checkUserSymbol(name); }
+      nonemptySortList[sorts] RPAREN_TOK
+      { Type t;
+        if(sorts.size() > 1) {
+          t = EXPR_MANAGER->mkFunctionType(sorts);
+        } else {
+          t = sorts[0];
+        }
+        Expr func = PARSER_STATE->mkVar(name, t);
+        static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(name, func, t));
+      }
+    )+
+    RPAREN_TOK
+
+  | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { $cmd = new CommandSequence(); }
+    LPAREN_TOK
+    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+      { PARSER_STATE->checkUserSymbol(name); }
+      sortList[sorts] RPAREN_TOK
+      { Type t = EXPR_MANAGER->booleanType();
+        if(sorts.size() > 0) {
+          t = EXPR_MANAGER->mkFunctionType(sorts, t);
+        }
+        Expr func = PARSER_STATE->mkVar(name, t);
+        static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(name, func, t));
+      }
+    )+
+    RPAREN_TOK
+
+  | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+      { PARSER_STATE->checkUserSymbol(name); }
+      term[e,e2]
+      { Expr func = PARSER_STATE->mkFunction(name, e.getType());
+        $cmd = new DefineFunctionCommand(name, func, e);
+      }
+    | LPAREN_TOK
+      symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+      { PARSER_STATE->checkUserSymbol(name); }
+      sortedVarList[sortedVarNames] RPAREN_TOK
+      { /* add variables to parser state before parsing term */
+        Debug("parser") << "define fun: '" << name << "'" << std::endl;
+        PARSER_STATE->pushScope();
+        for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+              sortedVarNames.begin(), iend = sortedVarNames.end();
+            i != iend;
+            ++i) {
+          terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+        }
+      }
+      term[e,e2]
+      { PARSER_STATE->popScope();
+        // declare the name down here (while parsing term, signature
+        // must not be extended with the name itself; no recursion
+        // permitted)
+        Type t = e.getType();
+        if( sortedVarNames.size() > 0 ) {
+          std::vector<CVC4::Type> sorts;
+          sorts.reserve(sortedVarNames.size());
+          for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+                sortedVarNames.begin(), iend = sortedVarNames.end();
+              i != iend;
+              ++i) {
+            sorts.push_back((*i).second);
+          }
+          t = EXPR_MANAGER->mkFunctionType(sorts, t);
+        }
+        Expr func = PARSER_STATE->mkFunction(name, t);
+        $cmd = new DefineFunctionCommand(name, func, terms, e);
+      }
+    )
+
+  | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    term[e,e2]
+    { cmd = new SimplifyCommand(e); }
   ;
 
 rewriterulesCommand[CVC4::Command*& cmd]
@@ -801,7 +904,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
   Expr e2;
 }
 : KEYWORD
-  {   
+  {
     attr = AntlrInput::tokenText($KEYWORD);
     //EXPR_MANAGER->setNamedAttribute( expr, attr );
     if( attr==":rewrite-rule" ){
@@ -823,7 +926,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
     }
   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
-    { 
+    {
       attr = std::string(":named");
       std::string name = sexpr.getValue();
       // FIXME ensure expr is a closed subterm
@@ -1160,7 +1263,7 @@ constructorDef[CVC4::Datatype& type]
 }
   : symbol[id,CHECK_UNDECLARED,SYM_SORT]
     { // make the tester
-      std::string testerId("is_");
+      std::string testerId("is-");
       testerId.append(id);
       PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
       ctor = new CVC4::DatatypeConstructor(id, testerId);
@@ -1218,6 +1321,12 @@ ECHO_TOK : 'echo';
 REWRITE_RULE_TOK : 'assert-rewrite';
 REDUCTION_RULE_TOK : 'assert-reduction';
 PROPAGATION_RULE_TOK : 'assert-propagation';
+DECLARE_SORTS_TOK : 'declare-sorts';
+DECLARE_FUNS_TOK : 'declare-funs';
+DECLARE_PREDS_TOK : 'declare-preds';
+DEFINE_TOK : 'define';
+DECLARE_CONST_TOK : 'declare-const';
+SIMPLIFY_TOK : 'simplify';
 
 // attributes
 ATTRIBUTE_PATTERN_TOK : ':pattern';
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 08fdbec95..a857351a5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1884,8 +1884,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
   Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl;
 
   // Check that SAT results generate a model correctly.
-  if(options::checkModels() && r.asSatisfiabilityResult() == Result::SAT) {
-    checkModel();
+  if(options::checkModels() && r.asSatisfiabilityResult() != Result::UNSAT) {
+    checkModel(/* hard failure iff */ ! r.isUnknown());
   }
 
   return r;
@@ -1948,8 +1948,8 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
   Trace("smt") << "SMT query(" << e << ") ==> " << r << endl;
 
   // Check that SAT results generate a model correctly.
-  if(options::checkModels() && r.asSatisfiabilityResult() == Result::SAT) {
-    checkModel();
+  if(options::checkModels() && r.asSatisfiabilityResult() != Result::UNSAT) {
+    checkModel(/* hard failure iff */ ! r.isUnknown());
   }
 
   return r;
@@ -2179,7 +2179,7 @@ Model* SmtEngine::getModel() throw(ModalException) {
   return d_theoryEngine->getModel();
 }
 
-void SmtEngine::checkModel() {
+void SmtEngine::checkModel(bool hardFailure) {
   // --check-model implies --interactive, which enables the assertion list,
   // so we should be ok.
   Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()");
@@ -2285,12 +2285,17 @@ void SmtEngine::checkModel() {
     if(n != NodeManager::currentNM()->mkConst(true)) {
       Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" << endl;
       stringstream ss;
-      ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
+      ss << "SmtEngine::checkModel(): "
+         << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
          << "assertion:     " << *i << endl
          << "simplifies to: " << n << endl
          << "expected `true'." << endl
          << "Run with `--check-models -v' for additional diagnostics.";
-      InternalError(ss.str());
+      if(hardFailure) {
+        InternalError(ss.str());
+      } else {
+        Warning() << ss.str() << endl;
+      }
     }
   }
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index fb456a4a4..096708f53 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -219,7 +219,7 @@ class CVC4_PUBLIC SmtEngine {
    * Check that a generated Model (via getModel()) actually satisfies
    * all user assertions.
    */
-  void checkModel();
+  void checkModel(bool hardFailure = true);
 
   /**
    * This is something of an "init" procedure, but is idempotent; call
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 17c2b51f3..f8f0756c7 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -2075,7 +2075,7 @@ DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) {
 
 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
   AlwaysAssert(d_qflraStatus ==  Result::SAT);
-  AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
+  //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
 
   Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;