* make Model class private (as discussed at meeting today)

* fix minor issue with s-expr parsing in CVC and SMT grammars
* other minor things

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

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 9df4dba85ffb2e7baf1a037136d1c3ef4b5f3a54..20967b733b845df149a7451d379ab872ba48ac52 100644 (file)
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -31,6 +31,7 @@
 #include "util/output.h"
 #include "util/dump.h"
 #include "util/sexpr.h"
+#include "util/util_model.h"
 #include "expr/node.h"
 #include "printer/printer.h"
 
@@ -882,9 +883,11 @@ void GetModelCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+/* Model is private to the library -- for now
 Model* GetModelCommand::getResult() const throw() {
   return d_result;
 }
+*/
 
 void GetModelCommand::printResult(std::ostream& out) const throw() {
   if(! ok()) {

diff --git a/src/expr/command.h b/src/expr/command.h
index 9fabf129e8cb353dbc7fde0cbdbe29e2fe95e774..2895f1d51b2d9f99a7d8a28c07aaa50234cac9ab 100644 (file)
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -37,13 +37,13 @@
 #include "util/sexpr.h"
 #include "util/datatype.h"
 #include "util/proof.h"
-#include "util/util_model.h"
 
 namespace CVC4 {
 
 class SmtEngine;
 class Command;
 class CommandStatus;
+class Model;
 
 std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
@@ -520,7 +520,8 @@ public:
   GetModelCommand() throw();
   ~GetModelCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
-  Model* getResult() const throw();
+  // Model is private to the library -- for now
+  //Model* getResult() const throw();
   void printResult(std::ostream& out) const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
   Command* clone() const;

diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 214ae0d02b8823f5ccc071850f26b9771702f450..9a783c48466ef69a5df800af75736131f21b5f71 100644 (file)
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** 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
@@ -72,4 +72,3 @@ public:
 }/* CVC4 namespace */
 
 #endif /* __CVC4__INTERACTIVE_SHELL_H */
-

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 22459037d5c2b561d98dd553efd18e347c189c24..40f35093f93885434c49f5114e098c367be1e0a2 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -320,7 +320,7 @@ Kind getOperatorKind(int type, bool& negate) {
   case INTDIV_TOK: return kind::INTS_DIVISION;
   case MOD_TOK: return kind::INTS_MODULUS;
   case DIV_TOK: return kind::DIVISION;
-  case EXP_TOK: break;
+  case EXP_TOK: return kind::POW;
 
     // bvBinop
   case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
@@ -570,8 +570,9 @@ parseCommand returns [CVC4::Command* cmd = NULL]
     { std::string s = AntlrInput::tokenText($IDENTIFIER);
       if(s == "benchmark") {
         PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected.  Use --lang smt1 for SMT-LIBv1 support.");
-      } else if(s == "set" || s == "get") {
-        PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv2 format detected.  Use --lang smt2 for SMT-LIBv2 support.");
+      } else if(s == "set" || s == "get" || s == "declare" ||
+                s == "define" || s == "assert") {
+        PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIB format detected.  Use --lang smt for SMT-LIB support.");
       } else {
         PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name.");
       }
@@ -782,7 +783,9 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
   CVC4::Rational r;
 }
   : INTEGER_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
+    { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
+  | MINUS_TOK INTEGER_LITERAL
+    { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
   | DECIMAL_LITERAL
     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | HEX_LITERAL
@@ -1784,15 +1787,15 @@ bvTerm[CVC4::Expr& f]
     /* BV sign extension */
   | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN
     { unsigned n = BitVectorType(f.getType()).getSize();
-      // Sign extension in TheoryBitVector is defined as in SMT-LIBv2
+      // Sign extension in TheoryBitVector is defined as in SMT-LIB
       // which is different than in the CVC language
       // SX(BITVECTOR(k), n) in CVC language extends to n bits
-      // In SMT-LIBv2, such a thing expands to k + n bits
+      // In SMT-LIB, such a thing expands to k + n bits
       f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); }
     /* BV zero extension */
   | BVZEROEXTEND_TOK LPAREN formula[f] COMMA k=numeral RPAREN
     { unsigned n = BitVectorType(f.getType()).getSize();
-      // Zero extension in TheoryBitVector is defined as in SMT-LIBv2
+      // Zero extension in TheoryBitVector is defined as in SMT-LIB
       // which is the same as in CVC3, but different than SX!
       // SX(BITVECTOR(k), n) in CVC language extends to n bits
       // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dbefc03051601a55be9af73e3e12118110e3723b..a49ae35c50ab1a38693104352cb5edca473335a4 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** 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
@@ -34,7 +34,7 @@ options {
 @header {
 /**
  ** 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
@@ -124,8 +124,9 @@ namespace CVC4 {
 using namespace CVC4;
 using namespace CVC4::parser;
 
-/* These need to be macros so they can refer to the PARSER macro, which will be defined
- * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
+/* These need to be macros so they can refer to the PARSER macro, which
+ * will be defined by ANTLR *after* this section. (If they were functions,
+ * PARSER would be undefined.) */
 #undef PARSER_STATE
 #define PARSER_STATE ((Smt2*)PARSER->super)
 #undef EXPR_MANAGER
@@ -140,7 +141,8 @@ using namespace CVC4::parser;
 
 /**
  * Parses an expression.
- * @return the parsed expression, or the Null Expr if we've reached the end of the input
+ * @return the parsed expression, or the Null Expr if we've reached the
+ * end of the input
  */
 parseExpr returns [CVC4::parser::smt2::myExpr expr]
 @declarations {
@@ -160,7 +162,8 @@ parseCommand returns [CVC4::Command* cmd = NULL]
   ;
 
 /**
- * Parse the internal portion of the command, ignoring the surrounding parentheses.
+ * Parse the internal portion of the command, ignoring the surrounding
+ * parentheses.
  */
 command returns [CVC4::Command* cmd = NULL]
 @declarations {
@@ -631,7 +634,7 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
   std::string s;
 }
   : INTEGER_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
+    { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
   | DECIMAL_LITERAL
     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | str[s]

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3ede00510182904a6d741d4ecde8145b2698ac59..93608ec591a2fba80c85dc772e18ee6e96029707 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -29,7 +29,6 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/proof.h"
-#include "util/util_model.h"
 #include "smt/modal_exception.h"
 #include "util/hash.h"
 #include "options/options.h"
@@ -50,11 +49,13 @@ typedef NodeTemplate<false> TNode;
 class NodeHashFunction;
 
 class Command;
+class GetModelCommand;
 
 class SmtEngine;
 class DecisionEngine;
 class TheoryEngine;
 
+class Model;
 class StatisticsRegistry;
 
 namespace context {
@@ -282,8 +283,9 @@ class CVC4_PUBLIC SmtEngine {
   friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
   friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
   // to access d_modelCommands
-  friend size_t ::CVC4::Model::getNumCommands() const;
-  friend const Command* ::CVC4::Model::getCommand(size_t) const;
+  friend class ::CVC4::Model;
+  // to access getModel(), which is private (for now)
+  friend class GetModelCommand;
 
   StatisticsRegistry* d_statisticsRegistry;
 
@@ -295,6 +297,13 @@ class CVC4_PUBLIC SmtEngine {
    */
   void addToModelCommand(Command* c);
 
+  /**
+   * Get the model (only if immediately preceded by a SAT
+   * or INVALID query).  Only permitted if CVC4 was built with model
+   * support and produce-models is on.
+   */
+  Model* getModel() throw(ModalException);
+
 public:
 
   /**
@@ -419,13 +428,6 @@ public:
    */
   CVC4::SExpr getAssignment() throw(ModalException);
 
-  /**
-   * Get the model (only if immediately preceded by a SAT
-   * or INVALID query).  Only permitted if CVC4 was built with model
-   * support and produce-models is on.
-   */
-  Model* getModel() throw(ModalException);
-
   /**
    * Get the last proof (only if immediately preceded by an UNSAT
    * or VALID query).  Only permitted if CVC4 was built with proof

diff --git a/src/util/util_model.h b/src/util/util_model.h
index 488563b54606f29e1bbf0ab08d4ca11c748fe0d1..bb40c9ba4ec2b181eb2a2f3f287531033980ee4d 100644 (file)
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -14,10 +14,10 @@
  ** \brief Model class
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
-#ifndef __CVC4__MODEL_H
-#define __CVC4__MODEL_H
+#ifndef __CVC4__UTIL_MODEL_H
+#define __CVC4__UTIL_MODEL_H
 
 #include <iostream>
 #include <vector>
@@ -27,13 +27,13 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC Command;
-class CVC4_PUBLIC SmtEngine;
-class CVC4_PUBLIC Model;
+class Command;
+class SmtEngine;
+class Model;
 
-std::ostream& operator<<(std::ostream&, Model&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, Model&);
 
-class CVC4_PUBLIC Model {
+class Model {
   friend std::ostream& operator<<(std::ostream&, Model&);
 
 protected:
@@ -50,6 +50,7 @@ public:
   size_t getNumCommands() const;
   /** get command */
   const Command* getCommand(size_t i) const;
+
 public:
   /** get value for expression */
   virtual Expr getValue(Expr expr) = 0;
@@ -57,14 +58,13 @@ public:
   virtual Cardinality getCardinality(Type t) = 0;
 };/* class Model */
 
-class ModelBuilder
-{
+class ModelBuilder {
 public:
-  ModelBuilder(){}
-  virtual ~ModelBuilder(){}
-  virtual void buildModel( Model* m, bool fullModel ) = 0;
+  ModelBuilder() { }
+  virtual ~ModelBuilder() { }
+  virtual void buildModel(Model* m, bool fullModel) = 0;
 };/* class ModelBuilder */
 
 }/* CVC4 namespace */
 
-#endif  /* __CVC4__MODEL_H */
+#endif  /* __CVC4__UTIL_MODEL_H */

diff --git a/test/regress/regress0/subranges.cvc b/test/regress/regress0/subranges.cvc
index d8351c7f1878c743e252bf34cf8665a2dc4294c6..5c1967344849c3fcdd712f6c20db8e11d6c39029 100644 (file)
--- a/test/regress/regress0/subranges.cvc
+++ b/test/regress/regress0/subranges.cvc
@@ -1,6 +1,5 @@
-% COMMAND-LINE: --parse-only
-% EXPECT: 
-% EXIT: 0
+% EXPECT: valid
+% EXIT: 20
 
 A : [0..0];
 B : [ -5 .. 8];
@@ -12,6 +11,6 @@ G : [-100 ..1];
 H : [-1 ..1];
 I : [0..10];
 J : [-10..-9];
-J : [-10..-10];
+K : [-10..-10];
 
 QUERY TRUE;