diff options
41 files changed, 117 insertions, 71 deletions
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT index 31ff2d47a..17affade4 100644 --- a/contrib/theoryskel/README.WHATS-NEXT +++ b/contrib/theoryskel/README.WHATS-NEXT @@ -6,7 +6,9 @@ Your next steps will likely be: * to add typing rules to theory_$dir_type_rules.h for your operators and constants * to write code in theory_$dir_rewriter.h to implement a normal form - for your theory's terms + for your theory's terms; in particular, you should ensure that you + rewrite (= X X) to "true" for terms X of your theory's sorts, and + evaluate any constant terms * for any new types that you have introduced, add "mk*Type()" functions to the NodeManager and ExprManager in src/expr/node_manager.{h,cpp} and src/expr/expr_manager_template.{h,cpp}. You may also want "is*()" testers diff --git a/src/Makefile.am b/src/Makefile.am index d6a0ffe0a..3637cb089 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -148,8 +148,8 @@ libcvc4_la_SOURCES = \ theory/unconstrained_simplifier.cpp \ theory/quantifiers_engine.h \ theory/quantifiers_engine.cpp \ - theory/model.h \ - theory/model.cpp \ + theory/theory_model.h \ + theory/theory_model.cpp \ theory/rep_set.h \ theory/rep_set.cpp \ theory/atom_requests.h \ diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8ae448657..3d5cec19b 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -29,7 +29,7 @@ #include "util/output.h" #include "util/dump.h" #include "util/sexpr.h" -#include "util/util_model.h" +#include "util/model.h" #include "expr/node.h" #include "printer/printer.h" diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 4e476f4d9..cf72d4e4e 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -40,13 +40,10 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) case kind::BUILTIN: typeNode = nodeManager->builtinOperatorType(); break; - case kind::BITVECTOR_EXTRACT_OP : - typeNode = nodeManager->builtinOperatorType(); - break; ${typerules} -#line 50 "${template}" +#line 47 "${template}" default: Debug("getType") << "FAILURE" << std::endl; @@ -69,7 +66,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) switch(n.getKind()) { ${construles} -#line 73 "${template}" +#line 70 "${template}" default:; } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 7667acdd0..786238492 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -22,7 +22,7 @@ #include "theory/substitutions.h" #include "smt/smt_engine.h" #include "smt/options.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "printer/dagification_visitor.h" #include "util/node_visitor.h" diff --git a/src/printer/printer.h b/src/printer/printer.h index 6fe1ec279..f73441966 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -21,7 +21,7 @@ #include "util/language.h" #include "util/sexpr.h" -#include "util/util_model.h" +#include "util/model.h" #include "expr/node.h" #include "expr/command.h" diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d086caf38..869e02326 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -30,7 +30,7 @@ #include "smt/options.h" #include "expr/node_manager_attributes.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/arrays/theory_arrays_rewriter.h" using namespace std; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 1157c464e..108c88829 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -18,7 +18,7 @@ #include "smt/boolean_terms.h" #include "smt/smt_engine.h" #include "theory/theory_engine.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/booleans/boolean_term_conversion_mode.h" #include "theory/booleans/options.h" #include "expr/kind.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2cc606fa9..2e1d5de3c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -70,7 +70,7 @@ #include "theory/booleans/boolean_term_conversion_mode.h" #include "theory/booleans/options.h" #include "util/ite_removal.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "printer/printer.h" #include "prop/options.h" #include "theory/arrays/options.h" @@ -1815,7 +1815,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { return false; } - // No, conflict, go through the literals and solve them + // No conflict, go through the literals and solve them SubstitutionMap constantPropagations(d_smt.d_context); SubstitutionMap newSubstitutions(d_smt.d_context); SubstitutionMap::iterator pos; @@ -1904,7 +1904,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Assert(d_topLevelSubstitutions.apply(t) == t); Assert(newSubstitutions.apply(t) == t); constantPropagations.addSubstitution(t, c); - // vector<pair<Node,Node> > equations;a + // vector<pair<Node,Node> > equations; // constantPropagations.simplifyLHS(t, c, equations, true); // if (!equations.empty()) { // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); @@ -1951,7 +1951,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { // } Assert(constantPropagations.apply((*pos).second) == (*pos).second); } -#endif +#endif /* CVC4_ASSERTIONS */ } // Resize the learnt d_nonClausalLearnedLiterals.resize(j); 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 diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 5b8da8828..2f278625a 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -87,8 +87,8 @@ libutil_la_SOURCES = \ abstract_value.cpp \ array_store_all.h \ array_store_all.cpp \ - util_model.h \ - util_model.cpp \ + model.h \ + model.cpp \ sort_inference.h \ sort_inference.cpp \ regexp.h diff --git a/src/util/util_model.cpp b/src/util/model.cpp index 1c2dc2edf..1d14a7c4f 100644 --- a/src/util/util_model.cpp +++ b/src/util/model.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file util_model.cpp +/*! \file model.cpp ** \verbatim ** Original author: Clark Barrett ** Major contributors: Morgan Deters @@ -12,7 +12,7 @@ ** \brief implementation of Model class **/ -#include "util/util_model.h" +#include "util/model.h" #include "expr/command.h" #include "smt/smt_engine_scope.h" #include "smt/command_list.h" diff --git a/src/util/util_model.h b/src/util/model.h index e5bd1f955..2224f74db 100644 --- a/src/util/util_model.h +++ b/src/util/model.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file util_model.h +/*! \file model.h ** \verbatim ** Original author: Clark Barrett ** Major contributors: Andrew Reynolds, Morgan Deters @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__UTIL_MODEL_H -#define __CVC4__UTIL_MODEL_H +#ifndef __CVC4__MODEL_H +#define __CVC4__MODEL_H #include <iostream> #include <vector> @@ -75,4 +75,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__UTIL_MODEL_H */ +#endif /* __CVC4__MODEL_H */ |