// 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
* 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;
#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<Type_attr>
+extern AttrTable<Type_attr> type_table;
} /* CVC4 namespace */
namespace CVC4 {
+class Context;
+
class ContextManager {
public:
void switchContext(Context);
void restore();
};/* class ContextObject */
+template <class T>
+class CDO;
+
+template <class T>
+class CDMap;
+
+template <class T>
+class CDList;
+
+template <class T>
+class CDSet;
+
}/* CVC4 namespace */
#endif /* __CVC4_CONTEXT_H */
** New York University
**/
+#include "literal.h"
+
#ifndef __CVC4_DECISION_ENGINE_H
#define __CVC4_DECISION_ENGINE_H
#ifndef __CVC4_EXPR_ATTRIBUTE_H
#define __CVC4_EXPR_ATTRIBUTE_H
+// TODO WARNING this file needs work !
+
+#include <stdint.h>
+#include "config.h"
+#include "context.h"
+#include "expr.h"
+
namespace CVC4 {
template <class value_type>
class AttrTables;
// global (or TSS)
-extern CDMap<uint_64t> g_hash_bool;
-extern CDMap<uint_64t> g_hash_int;
+extern CDMap<uint64_t> g_hash_bool;
+extern CDMap<uint64_t> g_hash_int;
extern CDMap<Expr> g_hash_expr;
extern CDMap<void*> g_hash_ptr;
+template <class T>
+class AttrTable;
+
template <>
class AttrTable<bool> {
public:
};
// bool specialization
- static CDMap<uint_64t> *s_hash;
+ static CDMap<uint64_t> *s_hash;
template <class Attr>
BitAccessor& find(Expr e, const Attr&);
};
template <>
-class AttrTable<uint_64t> {
+class AttrTable<uint64_t> {
public:
// int(egral) specialization
static CDMap<uint64_t> *s_hash;
- uint_64t& find(x);
- uint_64t& find(x) const;
+ uint64_t& find(Expr);
+ uint64_t& find(Expr) const;
};
template <class T>
public:
// Expr specialization
static CDMap<Expr> *s_hash;
- find(x)
+ Expr find(Expr);
};
-template <> AttrTable<bool>::s_hash = &g_hash_bool;
-template <> AttrTable<uint_64t>::s_hash = &g_hash_int;
-template <> AttrTable<Expr>::s_hash = &g_hash_expr;
-template <> AttrTable<void*>::s_hash = &g_hash_ptr;
+CDMap<uint64_t>* AttrTable<bool>::s_hash = &g_hash_bool;
+CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int;
+CDMap<Expr>* AttrTable<Expr>::s_hash = &g_hash_expr;
+
+template <class T>
+CDMap<void*>* AttrTable<T*>::s_hash = &g_hash_ptr;
template <class Attr>
class AttributeTable {
#ifndef __CVC4_EXPR_BUILDER_H
#define __CVC4_EXPR_BUILDER_H
+#include <vector>
+#include "expr_manager.h"
+#include "kind.h"
+
namespace CVC4 {
class AndExprBuilder;
unsigned d_nchildren;
union {
- Expr u_arr[10];
- vector<Expr> u_vec;
+ ExprValue* u_arr[10];
+ std::vector<Expr>* u_vec;
} d_children;
public:
ExprBuilder& skolemExpr(int i);
ExprBuilder& substExpr(const std::vector<Expr>& oldTerms,
const std::vector<Expr>& newTerms);
+ /*
ExprBuilder& substExpr(const ExprHashMap<Expr>& 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<Expr>& children) { return append(children.begin(), children.end()); }
+ ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
operator Expr();// not const
#ifndef __CVC4_EXPR_MANAGER_H
#define __CVC4_EXPR_MANAGER_H
+#include <vector>
+#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);
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<Expr> children);
+ Expr build(Kind kind, std::vector<Expr> 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);
// N-ary version
static Expr build(Kind kind, vector<Expr> children)
{ currentEM()->build(kind, children); }
+ */
// do we want a varargs one? perhaps not..
};
};/* enum Kind */
}/* CVC4 namespace */
+
+#endif /* __CVC4_KIND_H */
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
#ifndef __CVC4_PARSER_H
#define __CVC4_PARSER_H
+#include <iostream>
+#include "vc.h"
+#include "expr.h"
+
namespace CVC4 {
// In terms of abstraction, this is below (and provides services to)
#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)
#ifndef __CVC4_PROVER_H
#define __CVC4_PROVER_H
+#include <vector>
+#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.
*/
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 */
#ifndef __CVC4_THEORY_H
#define __CVC4_THEORY_H
+#include "expr.h"
+#include "literal.h"
+
namespace CVC4 {
/**
/**
* 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)..
#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 */
projects / cvc5.git / commitdiff