diff options
Diffstat (limited to 'src/theory')
29 files changed, 93 insertions, 46 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 9d13dccb7..aa2b2a557 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -63,7 +63,7 @@ #include "theory/arith/constraint.h" #include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/arith/options.h" diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 22fc8d4a7..86de3c1a9 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -71,7 +71,7 @@ #include "theory/arith/constraint.h" #include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/arith/options.h" diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 45e18fe0d..0d3a578a6 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -100,7 +100,6 @@ public: if( check ) { TypeNode lhsType = n[0].getType(check); if (!lhsType.isReal()) { - Message() << lhsType << " : " << n[0] << std::endl; throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side"); } TypeNode rhsType = n[1].getType(check); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 76e48aa1d..3aee02316 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -21,7 +21,7 @@ #include <map> #include "theory/rewriter.h" #include "expr/command.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/arrays/options.h" #include "smt/logic_exception.h" diff --git a/src/theory/atom_requests.cpp b/src/theory/atom_requests.cpp index 3d111f9f8..6070004d2 100644 --- a/src/theory/atom_requests.cpp +++ b/src/theory/atom_requests.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file atom_requests.cpp + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/atom_requests.h" using namespace CVC4; diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h index 99878125a..b54ece638 100644 --- a/src/theory/atom_requests.h +++ b/src/theory/atom_requests.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file atom_requests.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + #pragma once #include "expr/node.h" diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 895f4a279..a809ad0e8 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -38,7 +38,7 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti return PP_ASSERT_STATUS_CONFLICT; } - // Add the substitution from the variable to it's value + // Add the substitution from the variable to its value if (in.getKind() == kind::NOT) { if (in[0].getKind() == kind::VARIABLE) { outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false)); diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 1caa4b429..00f183eb5 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -147,7 +147,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if ((*i).getKind() == kind::OR) done = false; } if (!done) { - return flattenNode(n, /*trivialNode = */ tt, /* skipNode = */ ff); + return flattenNode(n, /* trivialNode = */ tt, /* skipNode = */ ff); } break; } @@ -160,7 +160,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if ((*i).getKind() == kind::AND) done = false; } if (!done) { - RewriteResponse ret = flattenNode(n, /*trivialNode = */ ff, /* skipNode = */ tt); + RewriteResponse ret = flattenNode(n, /* trivialNode = */ ff, /* skipNode = */ tt); Debug("bool-flatten") << n << ": " << ret.node << std::endl; return ret; } diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 49908c5db..60199c09a 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -17,7 +17,7 @@ #include "theory/builtin/theory_builtin.h" #include "theory/valuation.h" #include "expr/kind.h" -#include "theory/model.h" +#include "theory/theory_model.h" using namespace std; diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index d17dd588f..1712509b5 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -24,7 +24,7 @@ #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/bv/theory_bv.h" #include "theory/bv/options.h" -#include "theory/model.h" +#include "theory/theory_model.h" using namespace std; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 45946b8c8..6d11364d9 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -19,7 +19,7 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/bv/slicer.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/bv/options.h" using namespace std; diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index a3970c9e3..0eac4c035 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -17,7 +17,7 @@ #include "theory/bv/bv_subtheory_inequality.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/model.h" +#include "theory/theory_model.h" using namespace std; using namespace CVC4; diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index aeae1073e..cf83150e1 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -167,6 +167,7 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index a2de951aa..ce44b312d 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -25,7 +25,7 @@ #include "theory/bv/bv_subtheory_core.h" #include "theory/bv/bv_subtheory_inequality.h" #include "theory/bv/bv_subtheory_bitblast.h" -#include "theory/model.h" +#include "theory/theory_model.h" using namespace CVC4; using namespace CVC4::theory; diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 67dae0cfa..b51c56b18 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -140,6 +140,15 @@ public: } }; +class BitVectorExtractOpTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP); + return nodeManager->builtinOperatorType(); + } +}; + class BitVectorConcatRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 686695f98..3c9fd7bd2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -22,7 +22,7 @@ #include "util/cvc4_assert.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "smt/options.h" #include "smt/boolean_terms.h" #include "theory/quantifiers/options.h" @@ -1399,4 +1399,4 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { }else{ return NodeManager::currentNM()->mkNode( AND, assumptions ); } -}
\ No newline at end of file +} diff --git a/src/theory/decision_attributes.h b/src/theory/decision_attributes.h index 204362a2a..79f58feb1 100644 --- a/src/theory/decision_attributes.h +++ b/src/theory/decision_attributes.h @@ -14,8 +14,10 @@ ** Rewriter attributes. **/ -#ifndef __CVC4__THEORY__DECISION_ATRRIBUTES -#define __CVC4__THEORY__DECISION_ATRRIBUTES +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__DECISION_ATTRIBUTES +#define __CVC4__THEORY__DECISION_ATTRIBUTES #include "expr/attribute.h" @@ -33,4 +35,4 @@ typedef expr::Attribute<attr::DecisionWeightTag, decision::DecisionWeight> Decis }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__DECISION_ATRRIBUTES */ +#endif /* __CVC4__THEORY__DECISION_ATTRIBUTES */ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index f6e012660..b5bdff9ee 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -17,7 +17,7 @@ #ifndef __CVC4__FIRST_ORDER_MODEL_H #define __CVC4__FIRST_ORDER_MODEL_H -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" namespace CVC4 { diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index b96c58767..93cc1205e 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -18,7 +18,7 @@ #define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H #include "theory/quantifiers_engine.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" namespace CVC4 { diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 1c2c38c51..0c3c74b5f 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -19,7 +19,7 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/model_builder.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/relevant_domain.h" diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 944df63b2..f5724f488 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -13,10 +13,10 @@ ** \todo document this file **/ -#pragma once - #include "cvc4_private.h" +#pragma once + #include "expr/node.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b7576659a..66cc2a434 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -20,7 +20,7 @@ #include "expr/kind.h" #include "theory/rewriter.h" #include "expr/command.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "smt/logic_exception.h" #include "theory/strings/options.h" #include "theory/strings/type_enumerator.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 93b3f0d7e..af4dea293 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -40,7 +40,8 @@ #include "theory/ite_utilities.h" #include "theory/unconstrained_simplifier.h" -#include "theory/model.h" +#include "theory/theory_model.h" + #include "theory/quantifiers_engine.h" #include "theory/quantifiers/theory_quantifiers.h" #include "theory/quantifiers/options.h" @@ -1218,7 +1219,7 @@ public: bool alreadyVisited(TNode current, TNode parent) { // Check if already visited - d_visited.find(current) != d_visited.end(); + if (d_visited.find(current) != d_visited.end()) return true; // Don't visit non-boolean if (!current.getType().isBoolean()) return true; // New node diff --git a/src/theory/model.cpp b/src/theory/theory_model.cpp index b6ef924d7..73ff068b4 100644 --- a/src/theory/model.cpp +++ b/src/theory/theory_model.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file model.cpp +/*! \file theory_model.cpp ** \verbatim ** Original author: Andrew Reynolds ** Major contributors: Morgan Deters, Clark Barrett @@ -12,7 +12,7 @@ ** \brief Implementation of model class **/ -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "theory/type_enumerator.h" diff --git a/src/theory/model.h b/src/theory/theory_model.h index 8192274b5..9da9cb5e2 100644 --- a/src/theory/model.h +++ b/src/theory/theory_model.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file model.h +/*! \file theory_model.h ** \verbatim ** Original author: Andrew Reynolds ** Major contributors: Morgan Deters, Clark Barrett @@ -14,22 +14,21 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY_MODEL_H -#define __CVC4__THEORY_MODEL_H +#ifndef __CVC4__THEORY__THEORY_MODEL_H +#define __CVC4__THEORY__THEORY_MODEL_H -#include "util/util_model.h" +#include "util/model.h" #include "theory/uf/equality_engine.h" #include "theory/rep_set.h" #include "theory/substitutions.h" #include "theory/type_enumerator.h" namespace CVC4 { - namespace theory { - -/** Theory Model class - * For Model m, should call m.initialize() before using +/** + * Theory Model class. + * For Model m, should call m.initialize() before using. */ class TheoryModel : public Model { @@ -127,7 +126,7 @@ public: //necessary information for function models std::map< Node, std::vector< Node > > d_uf_terms; std::map< Node, Node > d_uf_models; -}; +};/* class TheoryModel */ /* * Class that encapsulates a map from types to sets of nodes @@ -246,7 +245,7 @@ private: return *(*it).second; } -}; +};/* class TypeSet */ /** TheoryEngineModelBuilder class * This model builder will consult all theories in a theory engine for @@ -275,9 +274,9 @@ public: * Should be called only on TheoryModels m */ void buildModel(Model* m, bool fullModel); -}; +};/* class TheoryEngineModelBuilder */ -} -} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__THEORY_MODEL_H */ diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index 326c6c913..6d1a4c9af 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -17,9 +17,10 @@ ** kinds files to produce the final header. **/ +#include "cvc4_private.h" + #pragma once -#include "cvc4_private.h" #include "theory/theory.h" #include "theory/options.h" diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0ee7a2bdd..1045c5a24 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -19,7 +19,7 @@ #include "theory/uf/options.h" #include "theory/quantifiers/options.h" #include "theory/uf/theory_uf_strong_solver.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/type_enumerator.h" using namespace std; diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 133cd2cf2..e3ab24efa 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -17,7 +17,7 @@ #ifndef __CVC4__THEORY_UF_MODEL_H #define __CVC4__THEORY_UF_MODEL_H -#include "theory/model.h" +#include "theory/theory_model.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index dab105d20..052b2f568 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -19,10 +19,9 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" #include "theory/uf/options.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/quantifiers/symmetry_breaking.h" - //#define ONE_SPLIT_REGION //#define DISABLE_QUICK_CLIQUE_CHECKS //#define COMBINE_REGIONS_SMALL_INTO_LARGE |