summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node.cpp5
-rw-r--r--src/expr/node.h7
-rw-r--r--src/expr/node_builder.h9
-rw-r--r--src/options/base_options2
-rw-r--r--src/parser/smt2/Smt2.g25
-rw-r--r--src/parser/smt2/smt2.h17
-rw-r--r--src/smt/options3
-rw-r--r--src/smt/smt_engine.cpp175
-rw-r--r--src/smt/smt_engine.h1
-rw-r--r--src/theory/builtin/kinds11
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h11
-rw-r--r--src/theory/substitutions.cpp6
-rw-r--r--src/util/Makefile.am2
-rw-r--r--src/util/abstract_value.cpp32
-rw-r--r--src/util/abstract_value.h78
-rw-r--r--test/regress/regress0/Makefile.am3
-rw-r--r--test/regress/regress0/bug421.smt211
17 files changed, 331 insertions, 67 deletions
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<true> 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<false> node) throw();
+
+};/* class UnknownTypeException */
+
/**
* \typedef NodeTemplate<true> 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<nchild_thresh>::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<Type> sorts;
std::vector<std::pair<std::string, Type> > 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 <sstream>
@@ -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"
@@ -200,12 +201,33 @@ class SmtEnginePrivate : public NodeManagerListener {
vector<Node> 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<Node, Node, NodeHashFunction> d_abstractValues;
+
+ /**
* Map from skolem variables to index in d_assertionsToCheck containing
* corresponding introduced Boolean ite
*/
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<Node>& 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<Node, Node, NodeHashFunction> 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<Node, Node, NodeHashFunction> 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 <iostream>
+#include <sstream>
+#include <string>
+
+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 <iostream>
+
+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))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback