diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/expr | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/kind_template.h | 2 | ||||
-rwxr-xr-x | src/expr/mkexpr | 10 | ||||
-rwxr-xr-x | src/expr/mkkind | 10 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 10 | ||||
-rw-r--r-- | src/expr/node.h | 40 | ||||
-rw-r--r-- | src/expr/node_manager.h | 34 |
6 files changed, 73 insertions, 33 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 74641513b..6313aa30b 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -124,8 +124,6 @@ namespace theory { enum TheoryId { ${theory_enum} - THEORY_QUANTIFIERS, - THEORY_REWRITERULES, THEORY_LAST }; diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 0cae68ed0..e113a1e8f 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -2,7 +2,7 @@ # # mkexpr # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010-2011 The CVC4 Project +# Copyright (c) 2010-2012 The CVC4 Project # # The purpose of this script is to create {expr,expr_manager}.{h,cpp} # from template files and a list of theory kinds. Basically it just @@ -15,7 +15,7 @@ # Output is to standard out. # -copyright=2010-2011 +copyright=2010-2012 filename=`basename "$1" | sed 's,_template,,'` @@ -95,6 +95,12 @@ function rewriter { check_theory_seen } +function instantiator { + # instantiator class header + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function properties { # properties prop* lineno=${BASH_LINENO[0]} diff --git a/src/expr/mkkind b/src/expr/mkkind index abb238f1a..2f361cb63 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -2,7 +2,7 @@ # # mkkind # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010-2011 The CVC4 Project +# Copyright (c) 2010-2012 The CVC4 Project # # The purpose of this script is to create kind.h (and also # type_properties.h) from a template and a list of theory kinds. @@ -14,7 +14,7 @@ # Output is to standard out. # -copyright=2010-2011 +copyright=2010-2012 filename=`basename "$1" | sed 's,_template,,'` @@ -105,6 +105,12 @@ function theory { " } +function instantiator { + # instantiator class header + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function properties { # rewriter class header lineno=${BASH_LINENO[0]} diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index d84691e14..2e94e41be 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -2,7 +2,7 @@ # # mkmetakind # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# Copyright (c) 2010-2011 The CVC4 Project +# Copyright (c) 2010-2012 The CVC4 Project # # The purpose of this script is to create metakind.h from a template # and a list of theory kinds. @@ -17,7 +17,7 @@ # Output is to standard out. # -copyright=2010-2011 +copyright=2010-2012 cat <<EOF /********************* */ @@ -80,6 +80,12 @@ function theory { // #include \"theory/$b/$2\"" } +function instantiator { + # instantiator class header + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function properties { # properties prop* lineno=${BASH_LINENO[0]} diff --git a/src/expr/node.h b/src/expr/node.h index a61944433..e56774d7e 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -159,6 +159,14 @@ namespace kind { }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ +// for hash_maps, hash_sets.. +struct NodeHashFunction { + inline size_t operator()(Node node) const; +};/* struct NodeHashFunction */ +struct TNodeHashFunction { + inline size_t operator()(TNode node) const; +};/* struct TNodeHashFunction */ + /** * Encapsulation of an NodeValue pointer. The reference count is * maintained in the NodeValue if ref_count is true. @@ -166,17 +174,6 @@ namespace kind { */ template <bool ref_count> class NodeTemplate { - - // for hash_maps, hash_sets.. - template <bool ref_count1> - struct HashFunction { - size_t operator()(CVC4::NodeTemplate<ref_count1> node) const { - return (size_t) node.getId(); - } - };/* struct HashFunction */ - - typedef HashFunction<false> TNodeHashFunction; - /** * The NodeValue has access to the private constructors, so that the * iterators can can create new nodes. @@ -233,7 +230,7 @@ class NodeTemplate { Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); } } - +public: /** * Cache-aware, recursive version of substitute() used by the public * member function with a similar signature. @@ -904,19 +901,12 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) { namespace CVC4 { -// for hash_maps, hash_sets.. -struct NodeHashFunction { - size_t operator()(CVC4::Node node) const { - return (size_t) node.getId(); - } -};/* struct NodeHashFunction */ - -// for hash_maps, hash_sets.. -struct TNodeHashFunction { - size_t operator()(CVC4::TNode node) const { - return (size_t) node.getId(); - } -};/* struct TNodeHashFunction */ +inline size_t NodeHashFunction::operator()(Node node) const { + return node.getId(); +} +inline size_t TNodeHashFunction::operator()(TNode node) const { + return node.getId(); +} struct TNodePairHashFunction { size_t operator()(const std::pair<CVC4::TNode, CVC4::TNode>& pair ) const { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 00fe6baa8..e763a1f10 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -362,6 +362,9 @@ public: /** Create a skolem constant with the given type. */ Node mkSkolem(const TypeNode& type); + /** Create a instantiation constant with the given type. */ + Node mkInstConstant(const TypeNode& type); + /** * Create a constant of type T. It will have the appropriate * CONST_* kind defined for T. @@ -579,6 +582,15 @@ public: /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); + /** Get the bound var list type. */ + inline TypeNode boundVarListType(); + + /** Get the instantiation pattern type. */ + inline TypeNode instPatternType(); + + /** Get the instantiation pattern type. */ + inline TypeNode instPatternListType(); + /** * Get the (singleton) type for builtin operators (that is, the type * of the Node returned from Node::getOperator() when the operator @@ -897,6 +909,21 @@ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE)); } +/** Get the bound var list type. */ +inline TypeNode NodeManager::boundVarListType(){ + return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE)); +} + +/** Get the instantiation pattern type. */ +inline TypeNode NodeManager::instPatternType(){ + return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE)); +} + +/** Get the instantiation pattern type. */ +inline TypeNode NodeManager::instPatternListType(){ + return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE)); +} + /** Get the (singleton) type for builtin operators. */ inline TypeNode NodeManager::builtinOperatorType() { return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE)); @@ -1366,6 +1393,13 @@ inline Node NodeManager::mkSkolem(const TypeNode& type) { return n; } +inline Node NodeManager::mkInstConstant(const TypeNode& type) { + Node n = NodeBuilder<0>(this, kind::INST_CONSTANT); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + template <class T> Node NodeManager::mkConst(const T& val) { return mkConstInternal<Node, T>(val); |