From 842e581321bcd9f30c60b9dacc671843ca776fed Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 3 Nov 2009 03:37:08 +0000 Subject: [PATCH] additional headers and modifications; now passes syntax check --- DESIGN_QUESTIONS | 19 +++++++++++++++++++ src/include/attr_type.h | 8 ++++++-- src/include/context.h | 14 ++++++++++++++ src/include/decision_engine.h | 2 ++ src/include/expr_attribute.h | 34 +++++++++++++++++++++++----------- src/include/expr_builder.h | 21 ++++++++++++++------- src/include/expr_manager.h | 14 ++++++++++---- src/include/kind.h | 2 ++ src/include/literal.h | 19 +++++++++++++++++++ src/include/model.h | 20 ++++++++++++++++++++ src/include/parser.h | 4 ++++ src/include/prop_engine.h | 4 ++++ src/include/prover.h | 5 +++++ src/include/result.h | 34 ++++++++++++++++++---------------- src/include/theory.h | 12 +++++++++++- src/include/vc.h | 3 +++ 16 files changed, 174 insertions(+), 41 deletions(-) create mode 100644 src/include/literal.h create mode 100644 src/include/model.h diff --git a/DESIGN_QUESTIONS b/DESIGN_QUESTIONS index 12704c6bf..670089c34 100644 --- a/DESIGN_QUESTIONS +++ b/DESIGN_QUESTIONS @@ -25,6 +25,13 @@ expr_builder.h // the expr is created? (we'd have to do that since we don't know // it's hash code yet) +expr_builder.h + + /* TODO design: these modify ExprBuilder */ + ExprBuilder& operator!() { return notExpr(); } + ExprBuilder& operator&&(const Expr& right) { return andExpr(right); } + ExprBuilder& operator||(const Expr& right) { return orExpr(right); } + prover.h // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the @@ -47,3 +54,15 @@ prover.h * preprocessing (certain contexts need more/less ?). */ +theory.h + + // TODO: these use the current EM (but must be renamed) + + // TODO design decisoin: instead of returning a set of literals + // here, perhaps we have an interface back into the prop engine + // where we assert directly. we might sometimes unknowingly assert + // something clearly inconsistent (esp. in a parallel context). + // This would allow the PropEngine to cancel our further work since + // we're already inconsistent---also could strategize dynamically on + // whether enough theory prop work has occurred. + virtual void propagate(Effort level = FULL_EFFORT) = 0; diff --git a/src/include/attr_type.h b/src/include/attr_type.h index a546d7dab..e5eb222fe 100644 --- a/src/include/attr_type.h +++ b/src/include/attr_type.h @@ -10,18 +10,22 @@ #ifndef __CVC4_ATTR_TYPE_H #define __CVC4_ATTR_TYPE_H +#include "expr_attribute.h" + namespace CVC4 { +class Type; + // an "attribute type" for types // this is essentially a traits structure class Type_attr { public: enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles - typedef value_type Type;//Expr? + typedef Type value_type;//Expr? static const Type_attr marker; }; -AttributeTable +extern AttrTable type_table; } /* CVC4 namespace */ diff --git a/src/include/context.h b/src/include/context.h index 845660ed7..1997e63d6 100644 --- a/src/include/context.h +++ b/src/include/context.h @@ -12,6 +12,8 @@ namespace CVC4 { +class Context; + class ContextManager { public: void switchContext(Context); @@ -24,6 +26,18 @@ public: void restore(); };/* class ContextObject */ +template +class CDO; + +template +class CDMap; + +template +class CDList; + +template +class CDSet; + }/* CVC4 namespace */ #endif /* __CVC4_CONTEXT_H */ diff --git a/src/include/decision_engine.h b/src/include/decision_engine.h index 6ff8d7f29..8745adad5 100644 --- a/src/include/decision_engine.h +++ b/src/include/decision_engine.h @@ -7,6 +7,8 @@ ** New York University **/ +#include "literal.h" + #ifndef __CVC4_DECISION_ENGINE_H #define __CVC4_DECISION_ENGINE_H diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h index b5f7dfe13..1c10a6663 100644 --- a/src/include/expr_attribute.h +++ b/src/include/expr_attribute.h @@ -10,17 +10,27 @@ #ifndef __CVC4_EXPR_ATTRIBUTE_H #define __CVC4_EXPR_ATTRIBUTE_H +// TODO WARNING this file needs work ! + +#include +#include "config.h" +#include "context.h" +#include "expr.h" + namespace CVC4 { template class AttrTables; // global (or TSS) -extern CDMap g_hash_bool; -extern CDMap g_hash_int; +extern CDMap g_hash_bool; +extern CDMap g_hash_int; extern CDMap g_hash_expr; extern CDMap g_hash_ptr; +template +class AttrTable; + template <> class AttrTable { public: @@ -33,7 +43,7 @@ public: }; // bool specialization - static CDMap *s_hash; + static CDMap *s_hash; template BitAccessor& find(Expr e, const Attr&); @@ -43,12 +53,12 @@ public: }; template <> -class AttrTable { +class AttrTable { public: // int(egral) specialization static CDMap *s_hash; - uint_64t& find(x); - uint_64t& find(x) const; + uint64_t& find(Expr); + uint64_t& find(Expr) const; }; template @@ -63,13 +73,15 @@ class AttrTable { public: // Expr specialization static CDMap *s_hash; - find(x) + Expr find(Expr); }; -template <> AttrTable::s_hash = &g_hash_bool; -template <> AttrTable::s_hash = &g_hash_int; -template <> AttrTable::s_hash = &g_hash_expr; -template <> AttrTable::s_hash = &g_hash_ptr; +CDMap* AttrTable::s_hash = &g_hash_bool; +CDMap* AttrTable::s_hash = &g_hash_int; +CDMap* AttrTable::s_hash = &g_hash_expr; + +template +CDMap* AttrTable::s_hash = &g_hash_ptr; template class AttributeTable { diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h index 2e9bf49a4..59503aa4f 100644 --- a/src/include/expr_builder.h +++ b/src/include/expr_builder.h @@ -10,6 +10,10 @@ #ifndef __CVC4_EXPR_BUILDER_H #define __CVC4_EXPR_BUILDER_H +#include +#include "expr_manager.h" +#include "kind.h" + namespace CVC4 { class AndExprBuilder; @@ -33,8 +37,8 @@ class ExprBuilder { unsigned d_nchildren; union { - Expr u_arr[10]; - vector u_vec; + ExprValue* u_arr[10]; + std::vector* u_vec; } d_children; public: @@ -52,18 +56,21 @@ public: ExprBuilder& skolemExpr(int i); ExprBuilder& substExpr(const std::vector& oldTerms, const std::vector& newTerms); + /* ExprBuilder& substExpr(const ExprHashMap& oldToNew); + */ - ExprBuilder& operator!() const { return notExpr(); } - ExprBuilder& operator&&(const Expr& right) const { return andExpr(right); } - ExprBuilder& operator||(const Expr& right) const { return orExpr(right); } + /* TODO design: these modify ExprBuilder */ + ExprBuilder& operator!() { return notExpr(); } + ExprBuilder& operator&&(const Expr& right) { return andExpr(right); } + ExprBuilder& operator||(const Expr& right) { return orExpr(right); } // "Stream" expression constructor syntax - ExprBuilder& operator<<(const Op& op); + ExprBuilder& operator<<(const Kind& op); ExprBuilder& operator<<(const Expr& child); // For pushing sequences of children - ExprBuilder& append(const vector& children) { return append(children.begin(), children.end()); } + ExprBuilder& append(const std::vector& children) { return append(children.begin(), children.end()); } template ExprBuilder& append(const Iterator& begin, const Iterator& end); operator Expr();// not const diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h index f49235831..0c265f57f 100644 --- a/src/include/expr_manager.h +++ b/src/include/expr_manager.h @@ -10,13 +10,17 @@ #ifndef __CVC4_EXPR_MANAGER_H #define __CVC4_EXPR_MANAGER_H +#include +#include "expr.h" +#include "kind.h" + namespace CVC4 { class ExprManager { - static __thread ExprManager* current; + static __thread ExprManager* s_current; public: - static ExprManager* currentEM() { return d_current; } + static ExprManager* currentEM() { return s_current; } // general expression-builders Expr build(Kind kind); @@ -31,9 +35,10 @@ public: Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9); Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10); // N-ary version - Expr build(Kind kind, vector children); + Expr build(Kind kind, std::vector children); - // these use the current EM + // TODO: these use the current EM (but must be renamed) + /* static Expr build(Kind kind) { currentEM()->build(kind); } static Expr build(Kind kind, Expr child1); @@ -59,6 +64,7 @@ public: // N-ary version static Expr build(Kind kind, vector children) { currentEM()->build(kind, children); } + */ // do we want a varargs one? perhaps not.. }; diff --git a/src/include/kind.h b/src/include/kind.h index f45495bb0..9307cc677 100644 --- a/src/include/kind.h +++ b/src/include/kind.h @@ -26,3 +26,5 @@ enum Kind { };/* enum Kind */ }/* CVC4 namespace */ + +#endif /* __CVC4_KIND_H */ diff --git a/src/include/literal.h b/src/include/literal.h new file mode 100644 index 000000000..93855edb8 --- /dev/null +++ b/src/include/literal.h @@ -0,0 +1,19 @@ +/********************* -*- C++ -*- */ +/** literal.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_LITERAL_H +#define __CVC4_LITERAL_H + +namespace CVC4 { + +class Literal; + +}/* CVC4 namespace */ + +#endif /* __CVC4_LITERAL_H */ diff --git a/src/include/model.h b/src/include/model.h new file mode 100644 index 000000000..205dcf18f --- /dev/null +++ b/src/include/model.h @@ -0,0 +1,20 @@ +/********************* -*- C++ -*- */ +/** model.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_MODEL_H +#define __CVC4_MODEL_H + +namespace CVC4 { + +class Model { +};/* class Model */ + +}/* CVC4 namespace */ + +#endif /* __CVC4_MODEL_H */ diff --git a/src/include/parser.h b/src/include/parser.h index 8f1032286..c5af769e3 100644 --- a/src/include/parser.h +++ b/src/include/parser.h @@ -10,6 +10,10 @@ #ifndef __CVC4_PARSER_H #define __CVC4_PARSER_H +#include +#include "vc.h" +#include "expr.h" + namespace CVC4 { // In terms of abstraction, this is below (and provides services to) diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h index 1ec0316a9..90d07a47b 100644 --- a/src/include/prop_engine.h +++ b/src/include/prop_engine.h @@ -10,6 +10,10 @@ #ifndef __CVC4_PROP_ENGINE_H #define __CVC4_PROP_ENGINE_H +#include "expr.h" +#include "decision_engine.h" +#include "theory_engine.h" + namespace CVC4 { // In terms of abstraction, this is below (and provides services to) diff --git a/src/include/prover.h b/src/include/prover.h index 7abfafe63..e48d6336c 100644 --- a/src/include/prover.h +++ b/src/include/prover.h @@ -10,6 +10,11 @@ #ifndef __CVC4_PROVER_H #define __CVC4_PROVER_H +#include +#include "expr.h" +#include "result.h" +#include "model.h" + // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) // PropEngine. diff --git a/src/include/result.h b/src/include/result.h index 1cecc5301..cfabd3be2 100644 --- a/src/include/result.h +++ b/src/include/result.h @@ -23,39 +23,41 @@ namespace CVC4 { */ class Result { public: - enum { + enum SAT { UNSAT = 0, SAT = 1, - UNKNOWN = 2 - } SAT; + SAT_UNKNOWN = 2 + }; - enum { + enum Validity { INVALID = 0, VALID = 1, - UNKNOWN = 2 - } Validity; + VALIDITY_UNKNOWN = 2 + }; - enum { + enum UnknownExplanation { REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT, BAIL, OTHER - } UnknownExplanation; + }; private: - SAT d_sat; - Validity d_validity; - enum { SAT, VALIDITY } d_which; + enum SAT d_sat; + enum Validity d_validity; + enum { TYPE_SAT, TYPE_VALIDITY } d_which; public: - Result(SAT); - Result(Validity); + Result(enum SAT); + Result(enum Validity); - SAT isSAT(); - Validity isValid(); - UnknownExplanation whyUnknown(); + enum SAT isSAT(); + enum Validity isValid(); + enum UnknownExplanation whyUnknown(); };/* class Result */ }/* CVC4 namespace */ + +#endif /* __CVC4_RESULT_H */ diff --git a/src/include/theory.h b/src/include/theory.h index b08e9e7ba..6659dc680 100644 --- a/src/include/theory.h +++ b/src/include/theory.h @@ -10,6 +10,9 @@ #ifndef __CVC4_THEORY_H #define __CVC4_THEORY_H +#include "expr.h" +#include "literal.h" + namespace CVC4 { /** @@ -57,7 +60,14 @@ public: /** * T-propagate new literal assignments in the current context. */ - virtual LiteralSet propagate(); + // TODO design decisoin: instead of returning a set of literals + // here, perhaps we have an interface back into the prop engine + // where we assert directly. we might sometimes unknowingly assert + // something clearly inconsistent (esp. in a parallel context). + // This would allow the PropEngine to cancel our further work since + // we're already inconsistent---also could strategize dynamically on + // whether enough theory prop work has occurred. + virtual void propagate(Effort level = FULL_EFFORT) = 0; /** * Return an explanation for the literal (which was previously propagated by this theory).. diff --git a/src/include/vc.h b/src/include/vc.h index a75aa0548..57d8a957e 100644 --- a/src/include/vc.h +++ b/src/include/vc.h @@ -10,6 +10,9 @@ #ifndef __CVC4_VC_H #define __CVC4_VC_H +#include "command.h" +#include "expr.h" + /* TODO provide way of querying whether you fall into a fragment / * returning what fragment you're in */ -- 2.30.2