From dba60e91f02ae9ca3c3126c76d79a09c95f95a45 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 9 Oct 2012 20:22:01 +0000 Subject: [PATCH] * 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.) --- src/expr/command.cpp | 3 +++ src/expr/command.h | 5 +++-- src/main/interactive_shell.h | 3 +-- src/parser/cvc/Cvc.g | 17 ++++++++++------- src/parser/smt2/Smt2.g | 17 ++++++++++------- src/smt/smt_engine.h | 22 ++++++++++++---------- src/util/util_model.h | 28 ++++++++++++++-------------- test/regress/regress0/subranges.cvc | 7 +++---- 8 files changed, 56 insertions(+), 46 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 9df4dba85..20967b733 100644 --- 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 9fabf129e..2895f1d51 100644 --- 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 214ae0d02..9a783c484 100644 --- 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 22459037d..40f35093f 100644 --- 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 dbefc0305..a49ae35c5 100644 --- 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 3ede00510..93608ec59 100644 --- 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 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 488563b54..bb40c9ba4 100644 --- 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 #include @@ -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 d8351c7f1..5c1967344 100644 --- 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; -- 2.30.2