From 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 12 Jul 2017 08:35:03 -0500
Subject: Make type rules more strict for operators whose type rules involve
 subtypes. Disable support for subrange and predicate subtypes (which were
 only partially supported previously).

---
 src/smt/smt_engine.cpp | 88 +-------------------------------------------------
 1 file changed, 1 insertion(+), 87 deletions(-)

(limited to 'src/smt')

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f6b17e4cb..327f978e4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -545,8 +545,6 @@ class SmtEnginePrivate : public NodeManagerListener {
 
   /** TODO: whether certain preprocess steps are necessary */
   //bool d_needsExpandDefs;
-  //bool d_needsRewriteBoolTerms;
-  //bool d_needsConstrainSubTypes;
 
 public:
   /**
@@ -624,14 +622,6 @@ private:
    */
   void compressBeforeRealAssertions(size_t before);
 
-  /**
-   * Any variable in an assertion that is declared as a subtype type
-   * (predicate subtype or integer subrange type) must be constrained
-   * to be in that type.
-   */
-  void constrainSubtypes(TNode n, AssertionPipeline& assertions)
-    throw();
-
   /**
    * Trace nodes back to their assertions using CircuitPropagator's
    * BackEdgesMap.
@@ -679,9 +669,7 @@ public:
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
     d_simplifyAssertionsDepth(0),
-    //d_needsExpandDefs(true),
-    //d_needsRewriteBoolTerms(true),
-    //d_needsConstrainSubTypes(true), //TODO
+    //d_needsExpandDefs(true),  //TODO?
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
     d_pbsProcessor(smt.d_userContext),
@@ -3270,64 +3258,6 @@ void SmtEnginePrivate::unconstrainedSimp() {
   d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
 }
 
-
-void SmtEnginePrivate::constrainSubtypes(TNode top, AssertionPipeline& assertions)
-  throw() {
-
-  Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
-
-  set<TNode> done;
-  stack<TNode> worklist;
-  worklist.push(top);
-  done.insert(top);
-
-  do {
-    TNode n = worklist.top();
-    worklist.pop();
-
-    TypeNode t = n.getType();
-    if(t.isPredicateSubtype()) {
-      WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl;
-      Node pred = t.getSubtypePredicate();
-      Kind k;
-      // pred can be a LAMBDA, a function constant, or a datatype tester
-      Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl;
-      if(d_smt.d_definedFunctions->find(pred) != d_smt.d_definedFunctions->end()) {
-        k = kind::APPLY;
-      } else if(pred.getType().isTester()) {
-        k = kind::APPLY_TESTER;
-      } else {
-        k = kind::APPLY_UF;
-      }
-      Node app = NodeManager::currentNM()->mkNode(k, pred, n);
-      Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl;
-      assertions.push_back(app);
-    } else if(t.isSubrange()) {
-      SubrangeBounds bounds = t.getSubrangeBounds();
-      Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl;
-      if(bounds.lower.hasBound()) {
-        Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
-        Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n);
-        Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl;
-        assertions.push_back(lb);
-      }
-      if(bounds.upper.hasBound()) {
-        Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
-        Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c);
-        Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl;
-        assertions.push_back(ub);
-      }
-    }
-
-    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
-      if(done.find(*i) == done.end()) {
-        worklist.push(*i);
-        done.insert(*i);
-      }
-    }
-  } while(! worklist.empty());
-}
-
 void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) {
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
   for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) {
@@ -4080,22 +4010,6 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-  dumpAssertions("pre-constrain-subtypes", d_assertions);
-  {
-    // Any variables of subtype types need to be constrained properly.
-    // Careful, here: constrainSubtypes() adds to the back of
-    // d_assertions, but we don't need to reprocess those.
-    // We also can't use an iterator, because the vector may be moved in
-    // memory during this loop.
-    Chat() << "constraining subtypes..." << endl;
-    for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
-      constrainSubtypes(d_assertions[i], d_assertions);
-    }
-  }
-  dumpAssertions("post-constrain-subtypes", d_assertions);
-
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
   bool noConflict = true;
 
   // Unconstrained simplification
-- 
cgit v1.2.3