diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
| commit | 65798541fa437278cde0c759ab70fd9fa4fe9638 (patch) | |
| tree | 27341327b8159e58a5ce6371bede6129bf67beb3 /src/theory/quantifiers/relevant_domain.h | |
| parent | 78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788 (diff) | |
merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.h')
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.h | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h new file mode 100644 index 000000000..362a39d6a --- /dev/null +++ b/src/theory/quantifiers/relevant_domain.h @@ -0,0 +1,54 @@ +/********************* */
+/*! \file relevant_domain.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief relevant domain class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__RELEVANT_DOMAIN_H
+#define __CVC4__RELEVANT_DOMAIN_H
+
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class RelevantDomain
+{
+private:
+ FirstOrderModel* d_model;
+
+ //the domain of the arguments for each operator
+ std::map< Node, std::map< int, RepDomain > > d_active_domain;
+ //the range for each operator
+ std::map< Node, RepDomain > d_active_range;
+ //for computing relevant instantiation domain, return true if changed
+ bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd );
+ //for computing extended
+ bool extendFunctionDomains( Node n, RepDomain& range );
+public:
+ RelevantDomain( FirstOrderModel* m );
+ virtual ~RelevantDomain(){}
+ //compute the relevant domain
+ void compute();
+ //relevant instantiation domain for each quantifier
+ std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
+};
+
+}
+}
+}
+
+#endif
|