diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/Makefile.am | 7 | ||||
-rw-r--r-- | src/theory/arith/kinds | 10 | ||||
-rw-r--r-- | src/theory/booleans/kinds | 22 | ||||
-rwxr-xr-x | src/theory/mktheoryof | 14 | ||||
-rw-r--r-- | src/theory/theory.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 4 |
7 files changed, 39 insertions, 22 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 32ea1d2be..2891e64cf 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -23,12 +23,13 @@ EXTRA_DIST = \ @srcdir@/theoryof_table.h \ theoryof_table_template.h -@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_template.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds +@srcdir@/theoryof_table.h: theoryof_table_template.h mktheoryof @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mktheoryof + $(AM_V_at)mv -f $@ $@~ 2>/dev/null || true $(AM_V_GEN)(@srcdir@/mktheoryof \ - @srcdir@/theoryof_table_template.h \ + $< \ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \ - > @srcdir@/theoryof_table.h) || (rm -f @srcdir@/theoryof_table.h && exit 1) + > $@) || (rm -f $@ && exit 1) BUILT_SOURCES = @srcdir@/theoryof_table.h dist-hook: @srcdir@/theoryof_table.h diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 2f2c77d36..3b79192d2 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -10,16 +10,14 @@ operator PLUS 2: "arithmetic addition" operator MULT 2: "arithmetic multiplication" operator UMINUS 1 "arithmetic negation" -constant \ - CONST_RATIONAL \ +constant CONST_RATIONAL \ ::CVC4::Rational \ - ::CVC4::RationalHashFcn \ + ::CVC4::RationalHashStrategy \ "util/rational.h" \ "a multiple-precision rational constant" -constant \ - CONST_INTEGER \ +constant CONST_INTEGER \ ::CVC4::Integer \ - ::CVC4::IntegerHashFcn \ + ::CVC4::IntegerHashStrategy \ "util/integer.h" \ "a multiple-precision integer constant" diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 12869aad0..5fcf9299a 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -6,12 +6,18 @@ theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h" -operator FALSE 0 "falsity" -operator TRUE 0 "truth" +constant CONST_BOOLEAN \ + bool \ + ::CVC4::BoolHashStrategy \ + "util/bool.h" \ + "truth and falsity" -operator NOT 1 "logical not" -operator AND 2: "logical and" -operator IFF 2 "logical equivalence" -operator IMPLIES 2 "logical implication" -operator OR 2: "logical or" -operator XOR 2: "exclusive or" +# these are nonatomic because they have boolean structure. +# i.e. nodes n with this kind return false for n.isAtomic() +nonatomic_operator NOT 1 "logical not" +nonatomic_operator AND 2: "logical and" +nonatomic_operator IFF 2 "logical equivalence" +nonatomic_operator IMPLIES 2 "logical implication" +nonatomic_operator OR 2: "logical or" +nonatomic_operator XOR 2: "exclusive or" +nonatomic_operator ITE 3 "if-then-else" diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof index ef967342b..842e02a07 100755 --- a/src/theory/mktheoryof +++ b/src/theory/mktheoryof @@ -5,11 +5,11 @@ # Copyright (c) 2010 The CVC4 Project # # The purpose of this script is to create theoryof_table.h from a -# prologue, epilogue, and a list of theory kinds. +# template and a list of theory kinds. # # Invocation: # -# mktheoryof prologue-file epilogue-file theory-kind-files... +# mktheoryof template-file theory-kind-files... # # Output is to standard out. # @@ -17,7 +17,7 @@ copyright=2010 cat <<EOF -/********************* -*- C++ -*- */ +/********************* */ /** theoryof_table.h ** ** Copyright $copyright The AcSys Group, New York University, and as below. @@ -84,6 +84,14 @@ function operator { do_theoryof "$1" } +function nonatomic_operator { + # nonatomic_operator K #children ["comment"] + + lineno=${BASH_LINENO[0]} + + do_theoryof "$1" +} + function parameterized { # parameterized K #children ["comment"] diff --git a/src/theory/theory.h b/src/theory/theory.h index 42bdaf2dd..4c3a43061 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -36,7 +36,7 @@ namespace theory { // rewrite cache support struct RewriteCacheTag {}; -typedef expr::Attribute<RewriteCacheTag, Node> RewriteCache; +typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache; template <class T> class TheoryImpl; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f953f97b9..d29195011 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -111,7 +111,7 @@ Node TheoryEngine::rewrite(TNode in) { if(in.getKind() == kind::EQUAL) { Assert(in.getNumChildren() == 2); if(in[0] == in[1]) { - Node out = NodeManager::currentNM()->mkNode(kind::TRUE); + Node out = NodeManager::currentNM()->mkConst(true); //setRewriteCache(in, out); return out; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b8c2d5a75..1d5daf7bd 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -129,6 +129,10 @@ class TheoryEngine { * while leaving the Node's kind alone. */ Node rewriteChildren(TNode in) { + if(in.getMetaKind() == kind::metakind::CONSTANT) { + return in; + } + NodeBuilder<> b(in.getKind()); for(TNode::iterator c = in.begin(); c != in.end(); ++c) { b << rewrite(*c); |