diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/theory/builtin | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 26 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 2 |
5 files changed, 30 insertions, 6 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index d170469e0..83a372726 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -36,7 +36,6 @@ # check the theory supports the check() function # propagate the theory supports propagate() (and explain()) # staticLearning the theory supports staticLearning() -# registerTerm the theory supports registerTerm() # notifyRestart the theory supports notifyRestart() # presolve the theory supports presolve() # @@ -59,6 +58,12 @@ # future, so if possible, do not rely on them being called (and # implement them as a no-op). # +# typechecker header +# +# Declare that this theory's typechecker class is defined in the +# given header. (#include'd by the TypeChecker class in the expr +# package.) +# # variable K ["comment"] # # This declares a kind K that has no operator (it's conceptually a @@ -122,6 +127,19 @@ # For consistency, constants taking a non-void payload should # start with "CONST_", but this is not enforced. # +# typerule K typechecker-class +# +# Declares that a (previously-declared) kind K is typechecked by +# the typechecker-class. This class should be defined by the +# header given to the "typechecker" command, above. The +# typechecker-class is used this way by the main TypeChecker code: +# +# typechecker-class::computeType(NodeManager* nm, TNode n, bool check) +# +# It returns TypeNode. It should compute the type of n and return it, +# and if "check" is true, should actually perform type checking instead +# of simply type computation. +# # sort K cardinality [well-founded ground-term header | not-well-founded] ["comment"] # # This creates a kind K that represents a sort (a "type constant"). @@ -217,6 +235,7 @@ # theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h" +typechecker "theory/builtin/theory_builtin_type_rules.h" properties stable-infinite @@ -282,4 +301,9 @@ well-founded TUPLE_TYPE \ "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" +typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule +typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule +typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule +typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule + endtheory diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 1c779bd79..e955539d5 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -5,7 +5,7 @@ ** 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) + ** Copyright (c) 2009, 2010, 2011 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/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 4e62401ff..5c3c70443 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): barrett + ** 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) + ** Copyright (c) 2009, 2010, 2011 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/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index b71d66c03..f62140263 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -2,7 +2,7 @@ /*! \file theory_builtin_rewriter.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 3bfb7fdc5..ce06b4259 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -5,7 +5,7 @@ ** Major contributors: cconway, mdeters ** 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) + ** Copyright (c) 2009, 2010, 2011 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 |