diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-06-30 11:12:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-06-30 11:12:14 +0000 |
commit | 4375b60d5df794b2c6193f3892185ea181a0748d (patch) | |
tree | d346f9dc6bde42c3def6e0aac3b2711418e3d491 /src/theory/builtin | |
parent | 4206a75e7a1635d04bb69084404a75670e164b62 (diff) |
* theory "tree" rewriting implemented and works
* added TheoryArith::preRewrite() to test and demonstrate
the use of pre-rewriting.
* array types and type checking now supported
* array type checking now supported
* theoryOf() dispatching properly to arrays now
* theories now required to implement a (simple) identify()
function that returns a string identifying them for
debugging/user output purposes
* added "builtin" theory to hold all built-in kinds and their
type rules and rewriting (currently only exploding distinct)
* fixed production build failure (regarding NodeSetDepth)
* removed an errant "using namespace std" in util/bitvector.h
(and made associated trivial fixes elsewhere)
* fixes to make unexpected exceptions more verbose in debug builds
* fixes to make multiple, cascading assertion fails simpler
* minor other fixes to comments etc.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/Makefile | 4 | ||||
-rw-r--r-- | src/theory/builtin/Makefile.am | 13 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 130 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 69 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 48 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 60 |
6 files changed, 324 insertions, 0 deletions
diff --git a/src/theory/builtin/Makefile b/src/theory/builtin/Makefile new file mode 100644 index 000000000..1dfd8a113 --- /dev/null +++ b/src/theory/builtin/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/builtin + +include $(topdir)/Makefile.subdir diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am new file mode 100644 index 000000000..5694dea84 --- /dev/null +++ b/src/theory/builtin/Makefile.am @@ -0,0 +1,13 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../include -I@srcdir@/../.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libbuiltin.la + +libbuiltin_la_SOURCES = \ + theory_builtin_type_rules.h \ + theory_builtin.h \ + theory_builtin.cpp + +EXTRA_DIST = kinds diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds new file mode 100644 index 000000000..1f22ebef1 --- /dev/null +++ b/src/theory/builtin/kinds @@ -0,0 +1,130 @@ +# kinds [for builtin theory] -*- sh -*- +# +# This "kinds" file is written in a domain-specific language for +# declaring CVC4 kinds. Comments are marked with #, as this line is. +# +# The first non-blank, non-comment line in this file must be a theory +# declaration: +# +# theory [builtin] T header +# +# The special tag "builtin" declares that this is the builtin theory. +# There can be only one and it should be processed first. +# +# There are four basic commands for declaring kinds: +# +# variable K ["comment"] +# +# This declares a kind K that has no operator (it's conceptually a +# VARIABLE). This is appropriate for things like VARIABLE and +# SKOLEM. +# +# operator K #children ["comment"] +# +# Declares a "built-in" operator kind K. Really this is the same +# as "variable" except that it has an operator (automatically +# generated by NodeManager). +# +# You can specify an exact # of children required as the second +# argument to the operator command. In debug mode, assertions are +# automatically included to ensure that no Nodes can ever be +# created violating this. (FIXME: the public Expr stuff should +# enforce them regardless of whether debugging or not.) For +# example, a binary operator could be specified as: +# +# operator LESS_THAN 2 "arithmetic comparison, x < y" +# +# Alternatively, a range can be specified for #children as +# "LB:[UB]", LB and UB representing lower and upper bounds on the +# number of children (inclusive). If there is no lower bound, put +# a "0". If there is no upper bound, leave the colon after LB, +# but omit UB. For example, an N-ary operator might be defined +# as: +# +# operator PLUS 2: "addition on two or more arguments" +# +# parameterized K #children ["comment"] +# +# Declares a "built-in" parameterized operator kind K. This is a +# theory-specific APPLY, e.g., APPLY_UF, which applies its first +# parameter (say, "f"), to its operands (say, "x" and "y", making +# the full application "f(x,y)"). Nodes with such a kind will +# have an operator (Node::hasOperator() returns true, and +# Node::getOperator() returns the Node of functional type +# representing "f" here), and the "children" are defined to be +# this operator's parameters, and don't include the operator +# itself (here, there are only two children "x" and "y"). +# +# LB and UB are the same as documented for the operator command. +# The first parameter (the function being applied) does not count +# as a child. +# +# For consistency these should start with "APPLY_", but this is +# not enforced. +# +# constant K T Hasher header ["comment"] +# +# Declares a constant kind K. T is the C++ type representing the +# constant internally (and it should be +# ::fully::qualified::like::this), and header is the header needed +# to define it. Hasher is a hash functor type defined like this: +# +# struct MyHashFcn { +# static size_t hash(const T& val); +# }; +# +# For consistency, constants taking a non-void payload should +# start with "CONST_", but this is not enforced. +# +# Lines may be broken with a backslash between arguments; for example: +# +# constant CONST_INT \ +# int IntHash \ +# "" \ +# "This is a constant representing an INT. +# Its payload is the C++ int type. +# It is used by the theory of arithmetic." +# +# As shown in the example, ["comment"] fields may be broken across +# multiple lines too. +# +# The expr package guarantees that Nodes built with kinds have the +# following constraints imposed on them. (The #children guarantee +# only holds when assertions are turned on.) +# +# Node meta-kind has operator? # children +# ================== ================= ======================= +# variable no zero +# operator yes as documented above +# parameterized yes as documented above +# constant no zero +# +# NOTE THAT This file is actually an executable Bourne shell script +# (sourced by the processing scripts after defining functions called +# "theory," "variable," "operator," "parameterized," and "constant"). +# Please don't do anything else in this file other than using these +# commands. +# + +theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h" + +# 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), +# you'll get a special, singleton (BUILTIN EQUAL) Node. +constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \ + "expr/kind.h" "The kind of nodes representing built-in operators" + +operator EQUAL 2 "equality" +operator DISTINCT 2: "disequality" +variable SKOLEM "skolem var" +variable VARIABLE "variable" +operator TUPLE 2: "a tuple" + +constant TYPE_CONSTANT \ + ::CVC4::TypeConstant \ + ::CVC4::TypeConstantHashStrategy \ + "expr/type_constant.h" \ + "basic types" +operator FUNCTION_TYPE 2: "function type" +variable SORT_TYPE "sort type" diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp new file mode 100644 index 000000000..1951e438c --- /dev/null +++ b/src/theory/builtin/theory_builtin.cpp @@ -0,0 +1,69 @@ +/********************* */ +/*! \file theory_builtin.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, 2010 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 Implementation of the builtin theory. + ** + ** Implementation of the builtin theory. + **/ + +#include "theory/builtin/theory_builtin.h" +#include "expr/kind.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::theory::builtin; + +namespace CVC4 { +namespace theory { +namespace builtin { + +Node blastDistinct(TNode in) { + Debug("theory-rewrite") << "blastDistinct: " << in << std::endl; + Assert(in.getKind() == kind::DISTINCT); + if(in.getNumChildren() == 2) { + // if this is the case exactly 1 != pair will be generated so the + // AND is not required + Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]); + Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); + return neq; + } + // assume that in.getNumChildren() > 2 => diseqs.size() > 1 + vector<Node> diseqs; + for(TNode::iterator i = in.begin(); i != in.end(); ++i) { + TNode::iterator j = i; + while(++j != in.end()) { + Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j); + Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); + diseqs.push_back(neq); + } + } + Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs); + return out; +} + +RewriteResponse TheoryBuiltin::postRewrite(TNode in, bool topLevel) { + if(topLevel) { + if(in.getKind() == kind::DISTINCT) { + return RewritingComplete(blastDistinct(in)); + } + } + + // EQUAL is a special case that should never end up here + Assert(in.getKind() != kind::EQUAL); + + return RewritingComplete(in); +} + +}/* CVC4::theory::builtin namespace */ +}/* CVC4::theory */ +}/* CVC4 namespace */ diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h new file mode 100644 index 000000000..5c0a70dea --- /dev/null +++ b/src/theory/builtin/theory_builtin.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file theory_builtin.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, 2010 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 Built-in theory. + ** + ** Built-in theory. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H +#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H + +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace builtin { + +class TheoryBuiltin : public Theory { +public: + TheoryBuiltin(context::Context* c, OutputChannel& out) : Theory(c, out) { } + ~TheoryBuiltin() { } + void preRegisterTerm(TNode n) { Unreachable(); } + void registerTerm(TNode n) { Unreachable(); } + void check(Effort e) { Unreachable(); } + void propagate(Effort e) { Unreachable(); } + void explain(TNode n, Effort e) { Unreachable(); } + void shutdown() { } + RewriteResponse postRewrite(TNode n, bool topLevel); + std::string identify() const { return std::string("TheoryBuiltin"); } +};/* class TheoryBuiltin */ + +}/* CVC4::theory::builtin namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h new file mode 100644 index 000000000..0f4fda1a6 --- /dev/null +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -0,0 +1,60 @@ +/********************* */ +/*! \file builtin_type_rules.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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 Type rules for the builtin theory + ** + ** Type rules for the builtin theory. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_ +#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_ + +#include "expr/node.h" +#include "expr/type_node.h" +#include "expr/expr.h" + +namespace CVC4 { +namespace theory { +namespace builtin { + +class EqualityTypeRule { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) { + if (n[0].getType() != n[1].getType()) { + throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type"); + } + return nodeManager->booleanType(); + } +}; + +class DistinctTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) { + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + TypeNode firstType = (*child_it).getType(); + for (++child_it; child_it != child_it_end; ++child_it) { + if ((*child_it).getType() != firstType) { + throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type"); + } + } + return nodeManager->booleanType(); + } +}; + +}/* CVC4::theory::builtin namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_ */ |