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.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 127f83c60..72447fd66 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -92,8 +92,11 @@ public:
   void erase(Node node){ d_map.erase(node); }
   /** get */
   Node get( TNode var ) { return d_map[var]; }
+  Node get( QuantifiersEngine* qe, Node f, int i );
   /** set */
   void set(TNode var, TNode n);
+  void set( QuantifiersEngine* qe, Node f, int i, TNode n );
+  /** size */
   size_t size(){ return d_map.size(); }
   /* iterator */
   std::map< Node, Node >::iterator begin(){ return d_map.begin(); };