diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-08 20:02:10 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-08 20:02:22 -0500 |
commit | 85377f73a331b334437aa0d50d15c81e905869c1 (patch) | |
tree | bb98f8ec511f9314731fe4545b6e9b8f64d18b33 /src/theory/quantifiers/bounded_integers.h | |
parent | 75d3b086d2cbcb4508446e405e0599788a3a25a5 (diff) |
Add new method for checking candidate models, --fmf-fmc. Add infrastructure for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.h')
-rwxr-xr-x | src/theory/quantifiers/bounded_integers.h | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h new file mode 100755 index 000000000..570e27a10 --- /dev/null +++ b/src/theory/quantifiers/bounded_integers.h @@ -0,0 +1,47 @@ +/********************* */
+/*! \file bounded_integers.h
+** \verbatim
+** Original author: Andrew Reynolds
+** 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 This class manages integer bounds for quantifiers
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BOUNDED_INTEGERS_H
+#define __CVC4__BOUNDED_INTEGERS_H
+
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class BoundedIntegers : public QuantifiersModule
+{
+private:
+ std::map< Node, std::map< Node, Node > > d_lowers;
+ std::map< Node, std::map< Node, Node > > d_uppers;
+ std::map< Node, std::map< Node, bool > > d_set;
+ void hasFreeVar( Node f, Node n );
+ void process( Node f, Node n, bool pol );
+ void processLiteral( Node f, Node lit, bool pol );
+public:
+ BoundedIntegers( QuantifiersEngine* qe );
+
+ void check( Theory::Effort e );
+ void registerQuantifier( Node f );
+ void assertNode( Node n );
+ Node getNextDecisionRequest();
+};
+
+}
+}
+}
+
+#endif
\ No newline at end of file |