diff options
Diffstat (limited to 'src/theory')
26 files changed, 983 insertions, 210 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index d0d2f23d7..bb9d19b25 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -14,6 +14,7 @@ libtheory_la_SOURCES = \ theory.cpp libtheory_la_LIBADD = \ + @builddir@/builtin/libbuiltin.la \ @builddir@/booleans/libbooleans.la \ @builddir@/uf/libuf.la \ @builddir@/arith/libarith.la \ @@ -38,4 +39,4 @@ BUILT_SOURCES = @srcdir@/theoryof_table.h dist-hook: @srcdir@/theoryof_table.h MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h -SUBDIRS = booleans uf arith arrays bv +SUBDIRS = builtin booleans uf arith arrays bv diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 4e4088bb0..f270dacb4 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -148,7 +148,7 @@ public: } }else{ d_nonbasic.insert(x_j); - d_coeffs.insert(make_pair(x_j,a_sj)); + d_coeffs.insert(std::make_pair(x_j,a_sj)); } } } @@ -289,7 +289,7 @@ public: d_activeRows.erase(basic); d_activeBasicVars.erase(basic); - d_inactiveRows.insert(make_pair(basic, row)); + d_inactiveRows.insert(std::make_pair(basic, row)); } void reinjectBasic(TNode basic){ @@ -299,7 +299,7 @@ public: d_inactiveRows.erase(basic); d_activeBasicVars.insert(basic); - d_activeRows.insert(make_pair(basic, row)); + d_activeRows.insert(std::make_pair(basic, row)); updateRow(row); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 26d554356..cb9dc85f7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -315,6 +315,34 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){ return sum; } +RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { + // Look for multiplications with a 0 argument and rewrite the whole + // thing as 0 + if(n.getKind() == MULT) { + Rational ratZero; + Integer intZero; + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + if((*i).getKind() == CONST_RATIONAL) { + if((*i).getConst<Rational>() == ratZero) { + n = NodeManager::currentNM()->mkConst(ratZero); + break; + } + } else if((*i).getKind() == CONST_INTEGER) { + if((*i).getConst<Integer>() == intZero) { + if(n.getType().isInteger()) { + n = NodeManager::currentNM()->mkConst(intZero); + break; + } else { + n = NodeManager::currentNM()->mkConst(ratZero); + break; + } + } + } + } + } + return RewritingComplete(Node(n)); +} + Node TheoryArith::rewrite(TNode n){ Debug("arith") << "rewrite(" << n << ")" << endl; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ba9b5329d..465adacbc 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -41,7 +41,6 @@ namespace CVC4 { namespace theory { namespace arith { - /** * Implementation of QF_LRA. * Based upon: @@ -109,6 +108,18 @@ public: Node rewrite(TNode n); /** + * Rewriting optimizations. + */ + RewriteResponse preRewrite(TNode n, bool topLevel); + + /** + * Plug in old rewrite to the new (pre,post)rewrite interface. + */ + RewriteResponse postRewrite(TNode n, bool topLevel) { + return RewritingComplete(topLevel ? rewrite(n) : Node(n)); + } + + /** * Does non-context dependent setup for a node connected to a theory. */ void preRegisterTerm(TNode n); @@ -122,6 +133,7 @@ public: void shutdown(){ } + std::string identify() const { return std::string("TheoryArith"); } private: /** @@ -254,7 +266,7 @@ private: Statistics d_statistics; -}; +};/* class TheoryArith */ }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index a995f90af..9b22b14bb 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY_ARITH_TYPE_RULES_H_ -#define __CVC4__THEORY_ARITH_TYPE_RULES_H_ +#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H +#define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H namespace CVC4 { namespace theory { @@ -72,8 +72,8 @@ public: } }; -} -} -} +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif /* THEORY_ARITH_TYPE_RULES_H_ */ +#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */ diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 84b9faaf4..0c6e9006f 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarrays.la libarrays_la_SOURCES = \ + theory_arrays_type_rules.h \ theory_arrays.h \ theory_arrays.cpp diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 742b924c6..68daa8cb5 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -5,5 +5,11 @@ # theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h" + +operator ARRAY_TYPE 2 "array type" + +# select a i is a[i] operator SELECT 2 "array select" + +# store a i e is a[i] <= e operator STORE 3 "array store" diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 52e63831c..69498cfb2 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -23,9 +23,7 @@ #include "theory/theory.h" -namespace context { -class Context; -} +#include <iostream> namespace CVC4 { namespace theory { @@ -37,10 +35,25 @@ public: ~TheoryArrays(); void preRegisterTerm(TNode n) { } void registerTerm(TNode n) { } + + RewriteResponse preRewrite(TNode in, bool topLevel) { + Debug("arrays-rewrite") << "pre-rewriting " << in + << " topLevel==" << topLevel << std::endl; + return RewritingComplete(in); + } + + RewriteResponse postRewrite(TNode in, bool topLevel) { + Debug("arrays-rewrite") << "post-rewriting " << in + << " topLevel==" << topLevel << std::endl; + return RewritingComplete(in); + } + void check(Effort e); void propagate(Effort e) { } void explain(TNode n, Effort e) { } -}; + void shutdown() { } + std::string identify() const { return std::string("TheoryArrays"); } +};/* class TheoryArrays */ }/* CVC4::theory::arrays namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h new file mode 100644 index 000000000..0eb88d800 --- /dev/null +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \file theory_arrays_type_rules.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 Theory of arrays. + ** + ** Theory of arrays. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ +#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace arrays { + +struct ArraySelectTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::SELECT); + TypeNode arrayType = n[0].getType(); + TypeNode indexType = n[1].getType(); + if(arrayType.getArrayIndexType() != indexType) { + throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array"); + } + return arrayType.getArrayConstituentType(); + } +};/* struct ArraySelectTypeRule */ + +struct ArrayStoreTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::STORE); + TypeNode arrayType = n[0].getType(); + TypeNode indexType = n[1].getType(); + TypeNode valueType = n[2].getType(); + if(arrayType.getArrayIndexType() != indexType) { + throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); + } + if(arrayType.getArrayConstituentType() != valueType) { + throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); + } + return arrayType; + } +};/* struct ArrayStoreTypeRule */ + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 83effa005..512dfebcc 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -45,7 +45,7 @@ public: void check(Effort e) { Unimplemented(); } void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } - + std::string identify() const { return std::string("TheoryBool"); } }; }/* CVC4::theory::booleans namespace */ 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_ */ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index ba8fc4efd..f1b926d24 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -6,6 +6,12 @@ theory ::CVC4::theory::bv::TheoryBV "theory_bv.h" +constant BITVECTOR_TYPE \ + ::CVC4::BitVectorSize \ + "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \ + "util/bitvector.h" \ + "bit-vector type" + constant BITVECTOR_CONST \ ::CVC4::BitVector \ ::CVC4::BitVectorHashStrategy \ diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index dc29183ea..17d0779ca 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -39,7 +39,8 @@ public: void check(Effort e) { Unimplemented(); } void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } -}; + std::string identify() const { return std::string("TheoryBV"); } +};/* class TheoryBV */ }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 142c9c963..7dd6c3e60 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ -#define __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ +#ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H +#define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H namespace CVC4 { namespace theory { @@ -29,7 +29,7 @@ class BitVectorConstantTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) { - return nodeManager->bitVectorType(n.getConst<BitVector>().getSize()); + return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize()); } }; @@ -42,7 +42,7 @@ public: if (!lhs.isBitVector() || lhs != rhs) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); } - return nodeManager->bitVectorType(1); + return nodeManager->mkBitVectorType(1); } }; @@ -61,7 +61,7 @@ public: } if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize(); } - return nodeManager->bitVectorType(maxWidth); + return nodeManager->mkBitVectorType(maxWidth); } }; @@ -115,7 +115,7 @@ public: if (extractInfo.high >= t.getBitVectorSize()) { throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector"); } - return nodeManager->bitVectorType(extractInfo.high - extractInfo.low + 1); + return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1); } }; @@ -133,7 +133,7 @@ public: } size += t.getBitVectorSize(); } - return nodeManager->bitVectorType(size); + return nodeManager->mkBitVectorType(size); } }; @@ -146,7 +146,7 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>(); - return nodeManager->bitVectorType(repeatAmount * t.getBitVectorSize()); + return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize()); } }; @@ -162,12 +162,12 @@ public: (unsigned) n.getOperator().getConst<BitVectorSignExtend>() : (unsigned) n.getOperator().getConst<BitVectorZeroExtend>(); - return nodeManager->bitVectorType(extendAmount + t.getBitVectorSize()); + return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize()); } }; -} -} -} +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ */ +#endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */ diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof index 227831451..4b7dfcef5 100755 --- a/src/theory/mktheoryof +++ b/src/theory/mktheoryof @@ -51,6 +51,7 @@ function theory { exit 1 fi seen_theory_builtin=true + shift elif [ -z "$1" -o -z "$2" ]; then echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 exit 1 @@ -113,6 +114,12 @@ function check_theory_seen { fi } +function check_builtin_theory_seen { + if ! $seen_theory_builtin; then + echo "$me: warning: no declaration for the builtin theory found" >&2 + fi +} + while [ $# -gt 0 ]; do kf=$1 seen_theory=false @@ -123,6 +130,7 @@ while [ $# -gt 0 ]; do " shift done +check_builtin_theory_seen ## output diff --git a/src/theory/theory.h b/src/theory/theory.h index 6f4effe78..bb598d410 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -29,7 +29,8 @@ #include <deque> #include <list> -#include <typeinfo> +#include <string> +#include <iostream> namespace CVC4 { @@ -37,9 +38,43 @@ class TheoryEngine; namespace theory { -// rewrite cache support -struct RewriteCacheTag {}; -typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache; +/** + * Instances of this class serve as response codes from + * Theory::preRewrite() and Theory::postRewrite(). Instances of + * derived classes RewritingComplete(n) and RewriteAgain(n) should + * be used for better self-documenting behavior. + */ +class RewriteResponse { +protected: + enum Status { DONE, REWRITE }; + + RewriteResponse(Status s, Node n) : d_status(s), d_node(n) {} + +private: + const Status d_status; + const Node d_node; + +public: + bool isDone() const { return d_status == DONE; } + bool needsMoreRewriting() const { return d_status == REWRITE; } + Node getNode() const { return d_node; } +}; + +/** + * Return n, but request additional (pre,post)rewriting of it. + */ +class RewriteAgain : public RewriteResponse { +public: + RewriteAgain(Node n) : RewriteResponse(REWRITE, n) {} +}; + +/** + * Signal that (pre,post)rewriting of the node is complete at n. + */ +class RewritingComplete : public RewriteResponse { +public: + RewritingComplete(Node n) : RewriteResponse(DONE, n) {} +}; /** * Base class for T-solvers. Abstract DPLL(T). @@ -121,6 +156,9 @@ protected: d_facts.clear(); } + /** + * Get the context associated to this Theory. + */ context::Context* getContext() const { return d_context; } @@ -142,21 +180,6 @@ protected: */ bool isShared(TNode n) throw(); - /** - * Check whether a node is in the rewrite cache or not. - */ - static bool inRewriteCache(TNode n) throw() { - return n.hasAttribute(RewriteCache()); - } - - /** - * Get the value of the rewrite cache (or Node::null()) if there is - * none). - */ - static Node getRewriteCache(TNode n) throw() { - return n.getAttribute(RewriteCache()); - } - /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ struct Registered {}; /** The "registerTerm()-has-been-called" flag on Nodes */ @@ -230,15 +253,31 @@ public: /** * Pre-register a term. Done one time for a Node, ever. - * */ virtual void preRegisterTerm(TNode) = 0; /** - * Rewrite a term. Done one time for a Node, ever. + * Pre-rewrite a term. This default base-class implementation + * simply returns RewritingComplete(n). A theory should never + * rewrite a term to a strictly larger term that contains itself, as + * this will cause a loop of hard Node links in the cache (and thus + * memory leakage). */ - virtual Node rewrite(TNode n) { - return n; + virtual RewriteResponse preRewrite(TNode n, bool topLevel) { + Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl; + return RewritingComplete(n); + } + + /** + * Post-rewrite a term. This default base-class implementation + * simply returns RewritingComplete(n). A theory should never + * rewrite a term to a strictly larger term that contains itself, as + * this will cause a loop of hard Node links in the cache (and thus + * memory leakage). + */ + virtual RewriteResponse postRewrite(TNode n, bool topLevel) { + Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl; + return RewritingComplete(n); } /** @@ -285,6 +324,12 @@ public: */ virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0; + /** + * Identify this theory (for debugging, dynamic configuration, + * etc..) + */ + virtual std::string identify() const = 0; + // // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS) // @@ -334,6 +379,11 @@ protected: std::ostream& operator<<(std::ostream& os, Theory::Effort level); }/* CVC4::theory namespace */ + +inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) { + return out << theory.identify(); +} + }/* CVC4 namespace */ #endif /* __CVC4__THEORY__THEORY_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9dfaed68b..e41df92d0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -19,13 +19,18 @@ #include "theory/theory_engine.h" #include "expr/node.h" #include "expr/attribute.h" +#include "theory/theory.h" +#include "expr/node_builder.h" +#include <vector> #include <list> using namespace std; -namespace CVC4 { +using namespace CVC4; +using namespace CVC4::theory; +namespace CVC4 { namespace theory { struct PreRegisteredTag {}; @@ -36,6 +41,50 @@ typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr; }/* CVC4::theory namespace */ +Theory* TheoryEngine::theoryOf(TNode n) { + Kind k = n.getKind(); + + Assert(k >= 0 && k < kind::LAST_KIND); + + if(n.getMetaKind() == kind::metakind::VARIABLE) { + TypeNode t = n.getType(); + if(t.isBoolean()) { + return &d_bool; + } else if(t.isReal()) { + return &d_arith; + } else if(t.isArray()) { + return &d_arrays; + } else { + return &d_uf; + } + //Unimplemented(); + } else if(k == kind::EQUAL) { + // if LHS is a variable, use theoryOf(LHS.getType()) + // otherwise, use theoryOf(LHS) + TNode lhs = n[0]; + if(lhs.getMetaKind() == kind::metakind::VARIABLE) { + // FIXME: we don't yet have a Type-to-Theory map. When we do, + // look up the type of the LHS and return that Theory (?) + + //The following JUST hacks around this lack of a table + TypeNode type_of_n = lhs.getType(); + if(type_of_n.isReal()) { + return &d_arith; + } else if(type_of_n.isArray()) { + return &d_arrays; + } else { + return &d_uf; + //Unimplemented(); + } + } else { + return theoryOf(lhs); + } + } else { + // use our Kind-to-Theory mapping + return d_theoryOfTable[k]; + } +} + Node TheoryEngine::preprocess(TNode t) { Node top = rewrite(t); Debug("rewrite") << "rewrote: " << t << endl << "to : " << top << endl; @@ -70,7 +119,7 @@ Node TheoryEngine::preprocess(TNode t) { * and the above registration of leaves, this should ensure that * all subterms in the entire tree were registered in * reverse-topological order. */ - for(std::list<TNode>::reverse_iterator i = toReg.rbegin(); + for(list<TNode>::reverse_iterator i = toReg.rbegin(); i != toReg.rend(); ++i) { @@ -128,9 +177,11 @@ Node TheoryEngine::removeITEs(TNode node) { return skolem; } } - std::vector<Node> newChildren; + vector<Node> newChildren; bool somethingChanged = false; - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + for(TNode::const_iterator it = node.begin(), end = node.end(); + it != end; + ++it) { Node newChild = removeITEs(*it); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); @@ -145,66 +196,243 @@ Node TheoryEngine::removeITEs(TNode node) { nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null()); return node; } - } -Node blastDistinct(TNode in){ - 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); - } +namespace theory { +namespace rewrite { + +/** + * TheoryEngine::rewrite() keeps a stack of things that are being pre- + * and post-rewritten. Each element of the stack is a + * RewriteStackElement. + */ +struct RewriteStackElement { + /** + * The node at this rewrite level. For example (AND (OR x y) z) + * will have, as it's rewriting x, the stack: + * x + * (OR x y) + * (AND (OR x y) z) + */ + Node d_node; + + /** + * The theory associated to d_node. Cached here to avoid having to + * look it up again. + */ + Theory* d_theory; + + /** + * Whether or not this was a top-level rewrite. Note that at theory + * boundaries, topLevel is forced to true, so it's not the case that + * this is true only at the lowest stack level. + */ + bool d_topLevel; + + /** + * A saved index to the "next child" to pre- and post-rewrite. In + * the case when (AND (OR x y) z) is being rewritten, the AND, OR, + * and x are pre-rewritten, then (assuming they don't change), x is + * post-rewritten, then y is pre- and post-rewritten, then the OR is + * post-rewritten, then z is pre-rewritten, then the AND is + * post-rewritten. At each stack level, we need to remember the + * child index we're currently processing. + */ + int d_nextChild; + + /** + * A (re)builder for this node. As this node's children are + * post-rewritten, in order, they append to this builder. When this + * node is post-rewritten, it is reformed from d_builder since the + * children may have changed. Note Nodes aren't rebuilt if they + * have metakinds CONSTANT (which is illegal) or VARIABLE (which + * would create a fresh variable, not what we want)---which is fine, + * since those types don't have children anyway. + */ + NodeBuilder<> d_builder; + + /** + * Construct a fresh stack element. + */ + RewriteStackElement(Node n, Theory* thy, bool top) : + d_node(n), + d_theory(thy), + d_topLevel(top), + d_nextChild(0) { } - Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs); - return out; -} +}; + +}/* CVC4::theory::rewrite namespace */ +}/* CVC4::theory namespace */ Node TheoryEngine::rewrite(TNode in) { - if(inRewriteCache(in)) { - return getRewriteCache(in); - } + using theory::rewrite::RewriteStackElement; + + Node noItes = removeITEs(in); + Node out; + + // descend top-down into the theory rewriters + vector<RewriteStackElement> stack; + stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), true)); + Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl + << " " << noItes << " " << theoryOf(noItes) + << " TOP-LEVEL 0" << endl; + // This whole thing is essentially recursive, but we avoid actually + // doing any recursion. + do {// do until the stack is empty.. + RewriteStackElement& rse = stack.back(); + bool done; + + Debug("theory-rewrite") << "rewriter looking at level " << stack.size() + << endl + << " " << rse.d_node << " " << rse.d_theory + << "[" << *rse.d_theory << "]" + << " " << (rse.d_topLevel ? "TOP-LEVEL " : "") + << rse.d_nextChild << endl; + + if(rse.d_nextChild == 0) { + Node original = rse.d_node; + bool wasTopLevel = rse.d_topLevel; + Node cached = getPreRewriteCache(original, wasTopLevel); + if(cached.isNull()) { + do { + Debug("theory-rewrite") << "doing pre-rewrite in " << *rse.d_theory + << " topLevel==" << rse.d_topLevel << endl; + RewriteResponse response = + rse.d_theory->preRewrite(rse.d_node, rse.d_topLevel); + rse.d_node = response.getNode(); + Assert(!rse.d_node.isNull(), "node illegally rewritten to null"); + Theory* thy2 = theoryOf(rse.d_node); + Assert(thy2 != NULL, "node illegally rewritten to null theory"); + Debug("theory-rewrite") << "got back " << rse.d_node << " " + << thy2 << "[" << *thy2 << "]" + << (response.needsMoreRewriting() ? + " MORE-REWRITING" : " DONE") + << endl; + if(rse.d_theory != thy2) { + Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory + << " into " << *thy2 + << ", marking top-level and !done" << endl; + rse.d_theory = thy2; + done = false; + // FIXME how to handle the "top-levelness" of a node that's + // rewritten from theory T1 into T2, then back to T1 ? + rse.d_topLevel = true; + } else { + done = !response.needsMoreRewriting(); + } + } while(!done); + setPreRewriteCache(original, wasTopLevel, rse.d_node); + } else {// is in pre-rewrite cache + Debug("theory-rewrite") << "in pre-cache: " << cached << endl; + rse.d_node = cached; + Theory* thy2 = theoryOf(cached); + if(rse.d_theory != thy2) { + Debug("theory-rewrite") << "[cache-]pre-rewritten from " + << *rse.d_theory << " into " << *thy2 + << ", marking top-level" << endl; + rse.d_theory = thy2; + rse.d_topLevel = true; + } + } + } - if(in.getMetaKind() == kind::metakind::VARIABLE) { - return in; - } + // children + Node original = rse.d_node; + bool wasTopLevel = rse.d_topLevel; + Node cached = getPostRewriteCache(original, wasTopLevel); + + if(cached.isNull()) { + if(rse.d_nextChild == 0 && + rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { + ++rse.d_nextChild; + Node op = rse.d_node.getOperator(); + Theory* t = theoryOf(op); + Debug("theory-rewrite") << "pushing operator of " << rse.d_node << endl; + stack.push_back(RewriteStackElement(op, t, t != rse.d_theory)); + continue;// break out of this node, do its operator + } else { + unsigned nch = rse.d_nextChild++; + if(rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) { + --nch; + } + if(nch < rse.d_node.getNumChildren()) { + Debug("theory-rewrite") << "pushing child " << nch + << " of " << rse.d_node << endl; + Node c = rse.d_node[nch]; + Theory* t = theoryOf(c); + stack.push_back(RewriteStackElement(c, t, t != rse.d_theory)); + continue;// break out of this node, do its child + } + } - Node intermediate = removeITEs(in); + // incorporate the children's rewrites + if(rse.d_node.getMetaKind() != kind::metakind::VARIABLE && + rse.d_node.getMetaKind() != kind::metakind::CONSTANT) { + Debug("theory-rewrite") << "builder here is " << &rse.d_builder + << " and it gets " << rse.d_node.getKind() + << endl; + rse.d_builder << rse.d_node.getKind(); + rse.d_node = Node(rse.d_builder); + } - // these special cases should go away when theory rewriting comes online - if(intermediate.getKind() == kind::DISTINCT) { - Node out = blastDistinct(intermediate); - //setRewriteCache(intermediate, out); - return rewrite(out); //TODO let this fall through? - } + // post-rewriting + do { + Debug("theory-rewrite") << "doing post-rewrite of " + << rse.d_node << endl + << " in " << *rse.d_theory + << " topLevel==" << rse.d_topLevel << endl; + RewriteResponse response = + rse.d_theory->postRewrite(rse.d_node, rse.d_topLevel); + rse.d_node = response.getNode(); + Assert(!rse.d_node.isNull(), "node illegally rewritten to null"); + Theory* thy2 = theoryOf(rse.d_node); + Assert(thy2 != NULL, "node illegally rewritten to null theory"); + Debug("theory-rewrite") << "got back " << rse.d_node << " " + << thy2 << "[" << *thy2 << "]" + << (response.needsMoreRewriting() ? + " MORE-REWRITING" : " DONE") + << endl; + if(rse.d_theory != thy2) { + Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory + << " into " << *thy2 + << ", marking top-level and !done" << endl; + rse.d_theory = thy2; + done = false; + // FIXME how to handle the "top-levelness" of a node that's + // rewritten from theory T1 into T2, then back to T1 ? + rse.d_topLevel = true; + } else { + done = !response.needsMoreRewriting(); + } + } while(!done); + + setPostRewriteCache(original, wasTopLevel, rse.d_node); + + out = rse.d_node; + } else { + Debug("theory-rewrite") << "in post-cache: " << cached << endl; + out = cached; + Theory* thy2 = theoryOf(cached); + if(rse.d_theory != thy2) { + Debug("theory-rewrite") << "[cache-]post-rewritten from " + << *rse.d_theory << " into " << *thy2 << endl; + rse.d_theory = thy2; + } + } - theory::Theory* thy = theoryOf(intermediate); - if(thy == NULL) { - Node out = rewriteBuiltins(intermediate); - //setRewriteCache(intermediate, out); - return out; - } else if(thy != &d_bool){ - Node out = thy->rewrite(intermediate); - //setRewriteCache(intermediate, out); - return out; - }else{ - Node out = rewriteChildren(intermediate); - //setRewriteCache(intermediate, out); - return out; - } + stack.pop_back(); + if(!stack.empty()) { + Debug("theory-rewrite") << "asserting " << out << " to previous builder " + << &stack.back().d_builder << endl; + stack.back().d_builder << out; + } + } while(!stack.empty()); - Unreachable(); -} + Debug("theory-rewrite") << "DONE with theory rewriter." << endl; + Debug("theory-rewrite") << "result is:" << endl << out << endl; + + return out; +}/* TheoryEngine::rewrite(TNode in) */ }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 15b406cdd..2575c4c2d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -26,6 +26,7 @@ #include "theory/theoryof_table.h" #include "prop/prop_engine.h" +#include "theory/builtin/theory_builtin.h" #include "theory/booleans/theory_bool.h" #include "theory/uf/theory_uf.h" #include "theory/arith/theory_arith.h" @@ -36,6 +37,18 @@ namespace CVC4 { +namespace theory { + +// rewrite cache support +template <bool topLevel> struct PreRewriteCacheTag {}; +typedef expr::Attribute<PreRewriteCacheTag<true>, Node> PreRewriteCacheTop; +typedef expr::Attribute<PreRewriteCacheTag<false>, Node> PreRewriteCache; +template <bool topLevel> struct PostRewriteCacheTag {}; +typedef expr::Attribute<PostRewriteCacheTag<true>, Node> PostRewriteCacheTop; +typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache; + +}/* CVC4::theory namespace */ + // In terms of abstraction, this is below (and provides services to) // PropEngine. @@ -116,6 +129,7 @@ class TheoryEngine { EngineOutputChannel d_theoryOut; + theory::builtin::TheoryBuiltin d_builtin; theory::booleans::TheoryBool d_bool; theory::uf::TheoryUF d_uf; theory::arith::TheoryArith d_arith; @@ -124,81 +138,101 @@ class TheoryEngine { /** - * Check whether a node is in the rewrite cache or not. + * Check whether a node is in the pre-rewrite cache or not. */ - static bool inRewriteCache(TNode n) throw() { - return n.hasAttribute(theory::RewriteCache()); + static bool inPreRewriteCache(TNode n, bool topLevel) throw() { + if(topLevel) { + return n.hasAttribute(theory::PreRewriteCacheTop()); + } else { + return n.hasAttribute(theory::PreRewriteCache()); + } } /** - * Get the value of the rewrite cache (or Node::null()) if there is + * Get the value of the pre-rewrite cache (or Node::null()) if there is * none). */ - static Node getRewriteCache(TNode n) throw() { - return n.getAttribute(theory::RewriteCache()); + static Node getPreRewriteCache(TNode in, bool topLevel) throw() { + if(topLevel) { + Node out; + if(in.getAttribute(theory::PreRewriteCacheTop(), out)) { + return out.isNull() ? Node(in) : out; + } + } else { + Node out; + if(in.getAttribute(theory::PreRewriteCache(), out)) { + return out.isNull() ? Node(in) : out; + } + } + return Node::null(); } /** - * Get the value of the rewrite cache (or Node::null()) if there is - * none). + * Set the value of the pre-rewrite cache. v cannot be a null Node. */ - static void setRewriteCache(TNode n, TNode v) throw() { - return n.setAttribute(theory::RewriteCache(), v); + static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() { + AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()"); + AssertArgument(!v.isNull(), v, "v cannot be null in setPreRewriteCache()"); + // mappings from n -> n are actually stored as n -> null as a + // special case, to avoid cycles in the reference-counting of Nodes + if(topLevel) { + n.setAttribute(theory::PreRewriteCacheTop(), n == v ? TNode::null() : v); + } else { + n.setAttribute(theory::PreRewriteCache(), n == v ? TNode::null() : v); + } } /** - * This is the top rewrite entry point, called during preprocessing. - * It dispatches to the proper theories to rewrite the given Node. + * Check whether a node is in the post-rewrite cache or not. */ - Node rewrite(TNode in); + static bool inPostRewriteCache(TNode n, bool topLevel) throw() { + if(topLevel) { + return n.hasAttribute(theory::PostRewriteCacheTop()); + } else { + return n.hasAttribute(theory::PostRewriteCache()); + } + } /** - * Convenience function to recurse through the children, rewriting, - * while leaving the Node's kind alone. + * Get the value of the post-rewrite cache (or Node::null()) if there is + * none). */ - Node rewriteChildren(TNode in) { - if(in.getMetaKind() == kind::metakind::CONSTANT) { - return in; - } - - NodeBuilder<> b(in.getKind()); - if(in.getMetaKind() == kind::metakind::PARAMETERIZED){ - Assert(in.hasOperator()); - b << in.getOperator(); - } - for(TNode::iterator c = in.begin(); c != in.end(); ++c) { - b << rewrite(*c); + static Node getPostRewriteCache(TNode in, bool topLevel) throw() { + if(topLevel) { + Node out; + if(in.getAttribute(theory::PostRewriteCacheTop(), out)) { + return out.isNull() ? Node(in) : out; + } + } else { + Node out; + if(in.getAttribute(theory::PostRewriteCache(), out)) { + return out.isNull() ? Node(in) : out; + } } - Debug("rewrite") << "rewrote-children of " << in << std::endl - << "got " << b << std::endl; - Node ret = b; - return ret; + return Node::null(); } /** - * Rewrite Nodes with builtin kind (that is, those Nodes n for which - * theoryOf(n) == NULL). The master list is in expr/builtin_kinds. + * Set the value of the post-rewrite cache. v cannot be a null Node. */ - Node rewriteBuiltins(TNode in) { - switch(Kind k = in.getKind()) { - case kind::EQUAL: - return rewriteChildren(in); - - case kind::ITE: - Unhandled(k); - - case kind::SKOLEM: - case kind::VARIABLE: - return in; - - case kind::TUPLE: - return rewriteChildren(in); - - default: - Unhandled(k); + static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() { + AssertArgument(!n.isNull(), n, "n cannot be null in setPostRewriteCache()"); + AssertArgument(!v.isNull(), v, "v cannot be null in setPostRewriteCache()"); + // mappings from n -> n are actually stored as n -> null as a + // special case, to avoid cycles in the reference-counting of Nodes + if(topLevel) { + n.setAttribute(theory::PostRewriteCacheTop(), n == v ? TNode::null() : v); + } else { + n.setAttribute(theory::PostRewriteCache(), n == v ? TNode::null() : v); } } + /** + * This is the top rewrite entry point, called during preprocessing. + * It dispatches to the proper theories to rewrite the given Node. + */ + Node rewrite(TNode in); + Node removeITEs(TNode t); public: @@ -209,6 +243,7 @@ public: TheoryEngine(context::Context* ctxt) : d_propEngine(NULL), d_theoryOut(this, ctxt), + d_builtin(ctxt, d_theoryOut), d_bool(ctxt, d_theoryOut), d_uf(ctxt, d_theoryOut), d_arith(ctxt, d_theoryOut), @@ -216,6 +251,7 @@ public: d_bv(ctxt, d_theoryOut), d_statistics() { + d_theoryOfTable.registerTheory(&d_builtin); d_theoryOfTable.registerTheory(&d_bool); d_theoryOfTable.registerTheory(&d_uf); d_theoryOfTable.registerTheory(&d_arith); @@ -235,6 +271,7 @@ public: * ordering issues between PropEngine and Theory. */ void shutdown() { + d_builtin.shutdown(); d_bool.shutdown(); d_uf.shutdown(); d_arith.shutdown(); @@ -248,45 +285,7 @@ public: * @returns the theory, or NULL if the TNode is * of built-in type. */ - theory::Theory* theoryOf(TNode n) { - Kind k = n.getKind(); - - Assert(k >= 0 && k < kind::LAST_KIND); - - if(k == kind::VARIABLE) { - TypeNode t = n.getType(); - if(t.isBoolean()){ - return &d_bool; - }else if(t.isReal()){ - return &d_arith; - }else{ - return &d_uf; - } - //Unimplemented(); - } else if(k == kind::EQUAL) { - // if LHS is a VARIABLE, use theoryOf(LHS.getType()) - // otherwise, use theoryOf(LHS) - TNode lhs = n[0]; - if(lhs.getKind() == kind::VARIABLE) { - // FIXME: we don't yet have a Type-to-Theory map. When we do, - // look up the type of the LHS and return that Theory (?) - - //The following JUST hacks around this lack of a table - TypeNode type_of_n = lhs.getType(); - if(type_of_n.isReal()){ - return &d_arith; - }else{ - return &d_uf; - //Unimplemented(); - } - } else { - return theoryOf(lhs); - } - } else { - // use our Kind-to-Theory mapping - return d_theoryOfTable[k]; - } - } + theory::Theory* theoryOf(TNode n); /** * Preprocess a node. This involves theory-specific rewriting, then @@ -318,6 +317,7 @@ public: d_theoryOut.d_propagatedLiterals.clear(); // Do the checking try { + //d_builtin.check(effort); //d_bool.check(effort); d_uf.check(effort); d_arith.check(effort); diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index dc08788f3..cd0b4ef66 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -12,8 +12,10 @@ #include "theory/interrupted.h" #include <vector> +#include <utility> +#include <iostream> -namespace CVC4{ +namespace CVC4 { namespace theory { @@ -21,12 +23,32 @@ namespace theory { * Very basic OutputChannel for testing simple Theory Behaviour. * Stores a call sequence for the output channel */ -enum OutputChannelCallType { CONFLICT, PROPOGATE, AUG_LEMMA, LEMMA, EXPLANATION }; +enum OutputChannelCallType { + CONFLICT, + PROPAGATE, + AUG_LEMMA, + LEMMA, + EXPLANATION +}; + +}/* CVC4::theory namespace */ + +inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType type) { + switch(type) { + case theory::CONFLICT: return out << "CONFLICT"; + case theory::PROPAGATE: return out << "PROPAGATE"; + case theory::AUG_LEMMA: return out << "AUG_LEMMA"; + case theory::LEMMA: return out << "LEMMA"; + case theory::EXPLANATION: return out << "EXPLANATION"; + default: return out << "UNDEFINED-OutputChannelCallType!" << int(type); + } +} +namespace theory { class TestOutputChannel : public theory::OutputChannel { public: - std::vector< pair<enum OutputChannelCallType, Node> > d_callHistory; + std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory; TestOutputChannel() {} @@ -34,12 +56,14 @@ public: void safePoint() throw(Interrupted, AssertionException) {} - void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) { + void conflict(TNode n, bool safe = false) + throw(Interrupted, AssertionException) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) { - push(PROPOGATE, n); + void propagate(TNode n, bool safe = false) + throw(Interrupted, AssertionException) { + push(PROPAGATE, n); } void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException) { @@ -71,11 +95,11 @@ public: private: void push(OutputChannelCallType call, TNode n) { - d_callHistory.push_back(make_pair(call,n)); + d_callHistory.push_back(std::make_pair(call,n)); } };/* class TestOutputChannel */ -}/* namespace theory */ -}/* namespace CVC4 */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__THEORY_TEST_UTILS_H */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 5add2e92a..108102b9f 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -132,6 +132,13 @@ public: Node rewrite(TNode n); /** + * Plug in old rewrite to the new (pre,post)rewrite interface. + */ + RewriteResponse postRewrite(TNode n, bool topLevel) { + return RewritingComplete(topLevel ? rewrite(n) : Node(n)); + } + + /** * Propagates theory literals. Currently does nothing. * * Overloads void propagate(Effort level); from theory.h. @@ -147,6 +154,8 @@ public: */ void explain(TNode n, Effort level) {} + std::string identify() const { return std::string("TheoryUF"); } + private: /** * Checks whether 2 nodes are already in the same equivalence class tree. diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 33123cd8f..419e3d078 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY_UF_TYPE_RULES_H_ -#define __CVC4__THEORY_UF_TYPE_RULES_H_ +#ifndef __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ +#define __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ namespace CVC4 { namespace theory { @@ -49,4 +49,4 @@ public: } -#endif /* THEORY_UF_TYPE_RULES_H_ */ +#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ */ |