From 7b2dd1927731b894f5ef610528649a2d1fc555f2 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 10 Oct 2012 21:20:40 +0000 Subject: [PATCH] Abstract values for SMT-LIB. Also fix bug 421 relating to incrementality and models. (this commit was certified error- and warning-free by the test-and-commit script.) --- src/expr/node.cpp | 5 + src/expr/node.h | 7 + src/expr/node_builder.h | 9 +- src/options/base_options | 2 +- src/parser/smt2/Smt2.g | 25 ++- src/parser/smt2/smt2.h | 17 +- src/smt/options | 3 + src/smt/smt_engine.cpp | 175 +++++++++++++----- src/smt/smt_engine.h | 1 + src/theory/builtin/kinds | 11 +- .../builtin/theory_builtin_type_rules.h | 11 ++ src/theory/substitutions.cpp | 6 +- src/util/Makefile.am | 2 + src/util/abstract_value.cpp | 32 ++++ src/util/abstract_value.h | 78 ++++++++ test/regress/regress0/Makefile.am | 3 +- test/regress/regress0/bug421.smt2 | 11 ++ 17 files changed, 331 insertions(+), 67 deletions(-) create mode 100644 src/util/abstract_value.cpp create mode 100644 src/util/abstract_value.h create mode 100644 test/regress/regress0/bug421.smt2 diff --git a/src/expr/node.cpp b/src/expr/node.cpp index e303a9e58..f6c2250b1 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -43,4 +43,9 @@ NodeTemplate TypeCheckingExceptionPrivate::getNode() const throw() { return *d_node; } +UnknownTypeException::UnknownTypeException(TNode n) throw() : + TypeCheckingExceptionPrivate(n, "this expression contains an element of unknown type (such as an abstract value);" + " its type cannot be computed until it is substituted away") { +} + }/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index b7c4b3ad8..1c0646556 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -100,6 +100,13 @@ public: };/* class TypeCheckingExceptionPrivate */ +class UnknownTypeException : public TypeCheckingExceptionPrivate { +public: + + UnknownTypeException(NodeTemplate node) throw(); + +};/* class UnknownTypeException */ + /** * \typedef NodeTemplate Node; * diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 0c8ac40f8..351cf3639 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1305,7 +1305,14 @@ inline void NodeBuilder::maybeCheckType(const TNode n) const kind::MetaKind mk = n.getMetaKind(); if( mk != kind::metakind::VARIABLE && mk != kind::metakind::CONSTANT ) { - d_nm->getType(n, true); + try { + d_nm->getType(n, true); + } catch(UnknownTypeException&) { + // Ignore the error; this expression doesn't have a type, + // because it has an abstract value in it. If the user + // depends on the type of this expression, he should get an + // exception, but so far he's only constructed it. + } } } } diff --git a/src/options/base_options b/src/options/base_options index 573a11d29..d19c3b812 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -125,7 +125,7 @@ option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h" print the "success" output required of SMT-LIBv2 -alias --smtlib = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental +alias --smtlib = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values SMT-LIBv2 compliance mode (implies other options) undocumented-alias --smtlib2 = --smtlib diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a49ae35c5..915113dbc 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Parser for SMT-LIB v2 input language. + ** \brief Parser for SMT-LIB v2 input language ** ** Parser for SMT-LIB v2 input language. **/ @@ -355,7 +355,7 @@ command returns [CVC4::Command* cmd = NULL] | EXIT_TOK { cmd = new QuitCommand; } - /* CVC4-extended SMT-LIBv2 commands */ + /* CVC4-extended SMT-LIB commands */ | extendedCommand[cmd] { if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); @@ -385,7 +385,7 @@ extendedCommand[CVC4::Command*& cmd] std::vector sorts; std::vector > sortedVarNames; } - /* Extended SMT-LIBv2 set of commands syntax, not permitted in + /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } { /* open a scope to keep the UnresolvedTypes contained */ @@ -407,7 +407,7 @@ extendedCommand[CVC4::Command*& cmd] ) | rewriterulesCommand[cmd] - /* Support some of Z3's extended SMT-LIBv2 commands */ + /* Support some of Z3's extended SMT-LIB commands */ | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] @@ -624,7 +624,6 @@ pattern[CVC4::Expr& expr] : LPAREN_TOK termList[patexpr,expr] RPAREN_TOK { expr = MK_EXPR(kind::INST_PATTERN, patexpr); - //std::cout << "parsed pattern expr " << retExpr << std::endl; } ; @@ -811,7 +810,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { const bool isDefinedFunction = PARSER_STATE->isDefinedFunction(name); - if(isDefinedFunction) { + if(PARSER_STATE->isAbstractValue(name)) { + expr = PARSER_STATE->mkAbstractValue(name); + } else if(isDefinedFunction) { expr = MK_EXPR(CVC4::kind::APPLY, PARSER_STATE->getFunction(name)); } else { @@ -1206,13 +1207,19 @@ symbol[std::string& id, CVC4::parser::SymbolType type] : SIMPLE_SYMBOL { id = AntlrInput::tokenText($SIMPLE_SYMBOL); - PARSER_STATE->checkDeclaration(id, check, type); + if(!PARSER_STATE->isAbstractValue(id)) { + // if an abstract value, SmtEngine handles declaration + PARSER_STATE->checkDeclaration(id, check, type); + } } | QUOTED_SYMBOL { id = AntlrInput::tokenText($QUOTED_SYMBOL); /* strip off the quotes */ id = id.substr(1, id.size() - 2); - PARSER_STATE->checkDeclaration(id, check, type); + if(!PARSER_STATE->isAbstractValue(id)) { + // if an abstract value, SmtEngine handles declaration + PARSER_STATE->checkDeclaration(id, check, type); + } } ; @@ -1521,7 +1528,7 @@ fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; /** * Matches the characters that may appear as a one-character "symbol" - * (which excludes _ and !, which are reserved words in SMT-LIBv2). + * (which excludes _ and !, which are reserved words in SMT-LIB). */ fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~' diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 48942265a..e9c18bc97 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -23,6 +23,7 @@ #include "parser/parser.h" #include "parser/smt1/smt1.h" +#include "util/abstract_value.h" #include @@ -78,15 +79,23 @@ public: void checkThatLogicIsSet(); void checkUserSymbol(const std::string& name) { - if( strictModeEnabled() && - name.length() > 0 && - ( name[0] == '.' || name[0] == '@' ) ) { + if(name.length() > 0 && (name[0] == '.' || name[0] == '@')) { std::stringstream ss; - ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIBv2"; + ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIB"; parseError(ss.str()); } } + bool isAbstractValue(const std::string& name) { + return name.length() >= 2 && name[0] == '@' && name[1] != '0' && + name.find_first_not_of("0123456789", 1) == std::string::npos; + } + + Expr mkAbstractValue(const std::string& name) { + assert(isAbstractValue(name)); + return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1)))); + } + private: void addArithmeticOperators(); diff --git a/src/smt/options b/src/smt/options index ab5f9330a..ab903c951 100644 --- a/src/smt/options +++ b/src/smt/options @@ -49,6 +49,9 @@ option repeatSimp --repeat-simp bool :read-write common-option incrementalSolving incremental -i --incremental bool enable incremental solving +option abstractValues abstract-values --abstract-values bool :default false + in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard + option - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h" set the regular output channel of the solver option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cc126d6cd..734236d8a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -37,6 +37,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_builder.h" +#include "expr/node.h" #include "prop/prop_engine.h" #include "smt/modal_exception.h" #include "smt/smt_engine.h" @@ -199,6 +200,26 @@ class SmtEnginePrivate : public NodeManagerListener { /** Assertions to push to sat */ vector d_assertionsToCheck; + /** + * A context that never pushes/pops, for use by CD structures (like + * SubstitutionMaps) that should be "global". + */ + context::Context d_fakeContext; + + /** + * A map of AbsractValues to their actual constants. Only used if + * options::abstractValues() is on. + */ + theory::SubstitutionMap d_abstractValueMap; + + /** + * A mapping of all abstract values (actual value |-> abstract) that + * we've handed out. This is necessary to ensure that we give the + * same AbstractValues for the same real constants. Only used if + * options::abstractValues() is on. + */ + hash_map d_abstractValues; + /** * Map from skolem variables to index in d_assertionsToCheck containing * corresponding introduced Boolean ite @@ -206,6 +227,7 @@ class SmtEnginePrivate : public NodeManagerListener { IteSkolemMap d_iteSkolemMap; public: + /** Instance of the ITE remover */ RemoveITE d_iteRemover; @@ -277,6 +299,9 @@ public: d_realAssertionsEnd(0), d_propagator(d_nonClausalLearnedLiterals, true, true), d_assertionsToCheck(), + d_fakeContext(), + d_abstractValueMap(&d_fakeContext), + d_abstractValues(), d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_topLevelSubstitutions(smt.d_userContext), @@ -369,7 +394,31 @@ public: /** * pre-skolemize quantifiers */ - Node preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ); + Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector& fvs); + + /** + * Substitute away all AbstractValues in a node. + */ + Node substituteAbstractValues(TNode n) { + // We need to do this even if options::abstractValues() is off, + // since the setting might have changed after we already gave out + // some abstract values. + return d_abstractValueMap.apply(n); + } + + /** + * Make a new (or return an existing) abstract value for a node. + * Can only use this if options::abstractValues() is on. + */ + Node mkAbstractValue(TNode n) { + Assert(options::abstractValues()); + Node& val = d_abstractValues[n]; + if(val.isNull()) { + val = d_smt.d_nodeManager->mkConst(AbstractValue(d_abstractValues.size())); + d_abstractValueMap.addSubstitution(val, n); + } + return val; + } };/* class SmtEnginePrivate */ @@ -910,8 +959,11 @@ void SmtEngine::defineFunction(Expr func, } SmtScope smts(this); + // Substitute out any abstract values in formula + Expr form = d_private->substituteAbstractValues(Node::fromExpr(formula)).toExpr(); + // type check body - Type formulaType = formula.getType(options::typeChecking()); + Type formulaType = form.getType(options::typeChecking()); Type funcType = func.getType(); // We distinguish here between definitions of constants and functions, @@ -949,12 +1001,12 @@ void SmtEngine::defineFunction(Expr func, ++i) { formalsNodes.push_back((*i).getNode()); } - TNode formulaNode = formula.getTNode(); - DefinedFunction def(funcNode, formalsNodes, formulaNode); + TNode formNode = form.getTNode(); + DefinedFunction def(funcNode, formalsNodes, formNode); // Permit (check-sat) (define-fun ...) (get-value ...) sequences. // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks // d_haveAdditions = true; - Debug("smt") << "definedFunctions insert " << funcNode << " " << formulaNode << std::endl; + Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << std::endl; d_definedFunctions->insert(funcNode, def); } @@ -1582,7 +1634,7 @@ bool SmtEnginePrivate::simplifyAssertions() unconstrainedSimp(); } - Trace("smt") << "POST unconstraintedSimp" << std::endl; + Trace("smt") << "POST unconstrainedSimp" << std::endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; @@ -1884,15 +1936,12 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { } } -Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException, ModalException) { - - Assert(e.isNull() || e.getExprManager() == d_exprManager); - +Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException) { + Assert(ex.isNull() || ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - - Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl; + Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { throw ModalException("Cannot make multiple queries unless " @@ -1900,8 +1949,11 @@ Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException, ModalExce "(try --incremental)"); } - // Ensure that the expression is type-checked at this point, and Boolean - if(!e.isNull()) { + 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); } @@ -1951,16 +2003,13 @@ Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException, ModalExce return r; }/* SmtEngine::checkSat() */ -Result SmtEngine::query(const Expr& e) throw(TypeCheckingException, ModalException) { - - Assert(!e.isNull()); - Assert(e.getExprManager() == d_exprManager); - +Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalException) { + Assert(!ex.isNull()); + Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - - Trace("smt") << "SMT query(" << e << ")" << endl; + Trace("smt") << "SMT query(" << ex << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { throw ModalException("Cannot make multiple queries unless " @@ -1968,6 +2017,9 @@ Result SmtEngine::query(const Expr& e) throw(TypeCheckingException, ModalExcepti "(try --incremental)"); } + // Substitute out any abstract values in ex + Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); + // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); @@ -2015,12 +2067,16 @@ Result SmtEngine::query(const Expr& e) throw(TypeCheckingException, ModalExcepti return r; }/* SmtEngine::query() */ -Result SmtEngine::assertFormula(const Expr& e) throw(TypeCheckingException) { - Assert(e.getExprManager() == d_exprManager); +Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException) { + Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl; + Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; + + // Substitute out any abstract values in ex + Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); + ensureBoolean(e); if(d_assertionList != NULL) { d_assertionList->push_back(e); @@ -2029,33 +2085,44 @@ Result SmtEngine::assertFormula(const Expr& e) throw(TypeCheckingException) { return quickCheck().asValidityResult(); } -Expr SmtEngine::simplify(const Expr& e) throw(TypeCheckingException) { - Assert(e.getExprManager() == d_exprManager); +Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException) { + Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); + Trace("smt") << "SMT simplify(" << ex << ")" << endl; + + if(Dump.isOn("benchmark")) { + Dump("benchmark") << SimplifyCommand(ex); + } + + // Substitute out any abstract values in ex. + Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); if( options::typeChecking() ) { e.getType(true);// ensure expr is type-checked at this point } - Trace("smt") << "SMT simplify(" << e << ")" << endl; - if(Dump.isOn("benchmark")) { - Dump("benchmark") << SimplifyCommand(e); - } + // Expand definitions. + hash_map cache; + e = d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr(); // Make sure we've done simple preprocessing, unit detection, etc. Trace("smt") << "SmtEngine::check(): processing assertions" << endl; d_private->processAssertions(); return d_private->applySubstitutions(e).toExpr(); } -Expr SmtEngine::expandDefinitions(const Expr& e) throw(TypeCheckingException) { - Assert(e.getExprManager() == d_exprManager); +Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException) { + Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - if( options::typeChecking() ) { - e.getType(true);// ensure expr is type-checked at this point + Trace("smt") << "SMT expandDefinitions(" << ex << ")" << endl; + + // Substitute out any abstract values in ex. + Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); + if(options::typeChecking()) { + // Ensure expr is type-checked at this point. + e.getType(true); } - Trace("smt") << "SMT expandDefinitions(" << e << ")" << endl; if(Dump.isOn("benchmark")) { Dump("benchmark") << ExpandDefinitionsCommand(e); } @@ -2063,17 +2130,15 @@ Expr SmtEngine::expandDefinitions(const Expr& e) throw(TypeCheckingException) { return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr(); } -Expr SmtEngine::getValue(const Expr& e) throw(ModalException) { - Assert(e.getExprManager() == d_exprManager); +Expr SmtEngine::getValue(const Expr& ex) throw(ModalException) { + Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); - // ensure expr is type-checked at this point - Type type = e.getType(options::typeChecking()); - - Trace("smt") << "SMT getValue(" << e << ")" << endl; + Trace("smt") << "SMT getValue(" << ex << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetValueCommand(e); + Dump("benchmark") << GetValueCommand(ex); } + if(!options::produceModels()) { const char* msg = "Cannot get value when produce-models options is off."; @@ -2087,11 +2152,18 @@ Expr SmtEngine::getValue(const Expr& e) throw(ModalException) { throw ModalException(msg); } + // Substitute out any abstract values in ex. + Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); + + // Ensure expr is type-checked at this point. + e.getType(options::typeChecking()); + // do not need to apply preprocessing substitutions (should be recorded // in model already) // Expand, then normalize - Node n = expandDefinitions(e).getNode(); + hash_map cache; + Node n = d_private->expandDefinitions(Node::fromExpr(e), cache); n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; @@ -2101,15 +2173,26 @@ Expr SmtEngine::getValue(const Expr& e) throw(ModalException) { resultNode = m->getValue( n ); } Trace("smt") << "--- got value " << n << " = " << resultNode << endl; + // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf( n.getType() )); - return Expr(d_exprManager, new Node(resultNode)); + Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType())); + + // ensure it's a constant + Assert(resultNode.isConst()); + + if(options::abstractValues() && resultNode.getType().isArray()) { + resultNode = d_private->mkAbstractValue(resultNode); + } + + return resultNode.toExpr(); } -bool SmtEngine::addToAssignment(const Expr& e) throw() { +bool SmtEngine::addToAssignment(const Expr& ex) throw() { SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); + // Substitute out any abstract values in ex + Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); Type type = e.getType(options::typeChecking()); // must be Boolean CheckArgument( type.isBoolean(), e, diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 93608ec59..b6eacea4c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -34,6 +34,7 @@ #include "options/options.h" #include "util/result.h" #include "util/sexpr.h" +#include "util/hash.h" #include "util/statistics.h" #include "theory/logic_info.h" diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 86efac2f0..bcf787f6b 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -265,12 +265,19 @@ constant UNINTERPRETED_CONSTANT \ ::CVC4::UninterpretedConstant \ ::CVC4::UninterpretedConstantHashFunction \ "util/uninterpreted_constant.h" \ - "The kind of nodes representing uninterpreted constants" + "The kind of expressions representing uninterpreted constants" typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule enumerator SORT_TYPE \ ::CVC4::theory::builtin::UninterpretedSortEnumerator \ "theory/builtin/type_enumerator.h" +constant ABSTRACT_VALUE \ + ::CVC4::AbstractValue \ + ::CVC4::AbstractValueHashFunction \ + "util/abstract_value.h" \ + "The kind of expressions representing abstract values (other than uninterpreted sort constants)" +typerule ABSTRACT_VALUE ::CVC4::theory::builtin::AbstractValueTypeRule + # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's # not stored that way. If you ask for the operator of (EQUAL a b), @@ -279,7 +286,7 @@ constant BUILTIN \ ::CVC4::Kind \ ::CVC4::kind::KindHashFunction \ "expr/kind.h" \ - "The kind of nodes representing built-in operators" + "The kind of expressions representing built-in operators" variable FUNCTION "function" parameterized APPLY FUNCTION 0: "defined function application" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index a2e8e8179..3cd2f6282 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -150,6 +150,17 @@ public: } };/* class UninterpretedConstantTypeRule */ +class AbstractValueTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + // An UnknownTypeException means that this node has no type. For now, + // only abstract values are like this. Assigning them a type in all + // cases is difficult, since then the parser and the SmtEngine must be + // more tightly coupled. + throw UnknownTypeException(n); + } +};/* class AbstractValueTypeRule */ + class StringConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index b5f846735..fa4acf3fb 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -2,10 +2,10 @@ /*! \file substitutions.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: barrett + ** Minor contributors (to current version): mdeters ** 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 diff --git a/src/util/Makefile.am b/src/util/Makefile.am index d69f0edf0..098024912 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -79,6 +79,8 @@ libutil_la_SOURCES = \ index.h \ uninterpreted_constant.h \ uninterpreted_constant.cpp \ + abstract_value.h \ + abstract_value.cpp \ array_store_all.h \ array_store_all.cpp \ util_model.h \ diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp new file mode 100644 index 000000000..a5cb40a83 --- /dev/null +++ b/src/util/abstract_value.cpp @@ -0,0 +1,32 @@ +/********************* */ +/*! \file abstract_value.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief Representation of abstract values + ** + ** Representation of abstract values. + **/ + +#include "util/abstract_value.h" +#include +#include +#include + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const AbstractValue& val) { + return out << "@" << val.getIndex(); +} + +}/* CVC4 namespace */ diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h new file mode 100644 index 000000000..1fc2f42e1 --- /dev/null +++ b/src/util/abstract_value.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \file abstract_value.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief Representation of abstract values + ** + ** Representation of abstract values. + **/ + +#include "cvc4_public.h" + +#pragma once + +#include "expr/type.h" +#include + +namespace CVC4 { + +class CVC4_PUBLIC AbstractValue { + const Integer d_index; + +public: + + AbstractValue(Integer index) throw(IllegalArgumentException) : + d_index(index) { + CheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str()); + } + + ~AbstractValue() throw() { + } + + const Integer& getIndex() const throw() { + return d_index; + } + + bool operator==(const AbstractValue& val) const throw() { + return d_index == val.d_index; + } + bool operator!=(const AbstractValue& val) const throw() { + return !(*this == val); + } + + bool operator<(const AbstractValue& val) const throw() { + return d_index < val.d_index; + } + bool operator<=(const AbstractValue& val) const throw() { + return d_index <= val.d_index; + } + bool operator>(const AbstractValue& val) const throw() { + return !(*this <= val); + } + bool operator>=(const AbstractValue& val) const throw() { + return !(*this < val); + } + +};/* class AbstractValue */ + +std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC; + +/** + * Hash function for the BitVector constants. + */ +struct CVC4_PUBLIC AbstractValueHashFunction { + inline size_t operator()(const AbstractValue& val) const { + return IntegerHashFunction()(val.getIndex()); + } +};/* struct AbstractValueHashFunction */ + +}/* CVC4 namespace */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 8b2f05ca7..de1c8eca5 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -131,7 +131,8 @@ BUG_TESTS = \ bug365.smt2 \ bug382.smt2 \ bug383.smt2 \ - bug398.smt2 + bug398.smt2 \ + bug421.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug421.smt2 b/test/regress/regress0/bug421.smt2 new file mode 100644 index 000000000..5776d2fc1 --- /dev/null +++ b/test/regress/regress0/bug421.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --incremental --abstract-values +; EXPECT: sat +; EXPECT: ((a @1) (b @2)) +; EXIT: 10 +(set-logic QF_AUFLIA) +(set-option :produce-models true) +(declare-fun a () (Array Int Int)) +(declare-fun b () (Array Int Int)) +(assert (not (= a b))) +(check-sat) +(get-value (a b)) -- 2.30.2