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, 15 insertions, 6 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index f6a0dad11..d4988f223 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -134,18 +134,27 @@ Node InstMatch::getValue( Node var ) const{
   }
 }
 
+Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) {
+  return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) );
+}
+
 void InstMatch::set(TNode var, TNode n){
   Assert( !var.isNull() );
-  if( !n.isNull() &&// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
-  	//var.getType() == n.getType()
-  	!n.getType().isSubtypeOf( var.getType() ) ){
-    Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
-    Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
-    Assert(false);
+  if (Trace.isOn("inst-match-warn")) {
+    // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
+    if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){
+      Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
+      Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
+    }
   }
+  Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) );
   d_map[var] = n;
 }
 
+void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) {
+  set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n );
+}
+
 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
   if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){