ContrainSubtypes and ExpandingDefinitions classes

1 files changed, 25 insertions, 17 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d61639ad0..f43e6533e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -144,7 +144,8 @@ public:
  * support getValue() over defined functions, to support user output
  * in terms of defined functions, etc.
  */
-class DefinedFunction {
+
+/*class DefinedFunction {
   Node d_func;
   vector<Node> d_formals;
   Node d_formula;
@@ -158,7 +159,8 @@ public:
   Node getFunction() const { return d_func; }
   vector<Node> getFormals() const { return d_formals; }
   Node getFormula() const { return d_formula; }
-};/* class DefinedFunction */
+};*/
+/* class DefinedFunction */
 
 /*class AssertionPipeline {
   vector<Node> d_nodes;
@@ -1014,7 +1016,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_userContext->push();
   d_context->push();
 
-  d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
+  d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); 
   d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext);
   d_modelCommands = new(true) smt::CommandList(d_userContext);
 }
@@ -3498,16 +3500,10 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl;
   dumpAssertions("pre-definition-expansion", d_assertions);
   {
-/*   preproc::ExpandingDefinitionsPass pass(d_resourceManager, d_smt.d_stats->d_definitionExpansionTime);
-   pass.apply(&d_assertions);*/
-    Chat() << "expanding definitions..." << endl;
-    Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
-    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
-    unordered_map<Node, Node, NodeHashFunction> cache;
-    for(unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
-    }
-  }
+  preproc::ExpandingDefinitionsPass pass(d_resourceManager, &d_smt, d_smt.d_stats->d_definitionExpansionTime);
+   pass.apply(&d_assertions);
+ }
+
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
   dumpAssertions("post-definition-expansion", d_assertions);
 
@@ -3567,6 +3563,18 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+<<<<<<< e79fa19f8eacdeab55089cdfec717574b9b7af34
+=======
+  dumpAssertions("pre-constrain-subtypes", d_assertions);
+  {
+    preproc::ConstrainSubtypesPass pass(d_resourceManager, &d_smt);
+    pass.apply(&d_assertions);
+ }
+  dumpAssertions("post-constrain-subtypes", d_assertions);
+
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
+
+>>>>>>> ContrainSubtypes and ExpandingDefinitions classes
   bool noConflict = true;
 
   // Unconstrained simplification
@@ -3690,12 +3698,12 @@ void SmtEnginePrivate::processAssertions() {
 
   dumpAssertions("pre-repeat-simplify", d_assertions);
   if(options::repeatSimp()) {
-     preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth);
+/*     preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth, &d_smt, d_propagatorNeedsFinish, d_propagator, d_substitutionsIndex, d_nonClausalLearnedLiterals, d_true, d_smt.d_stats->d_nonclausalSimplificationTime);
      noConflict &= pass.apply(&d_assertions).d_noConflict;
 
      preproc::RepeatSimpPass pass1(d_resourceManager, &d_topLevelSubstitutions, d_simplifyAssertionsDepth, &noConflict, d_iteSkolemMap, d_realAssertionsEnd); 
-     pass1.apply(&d_assertions);
-/*    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
+     pass1.apply(&d_assertions);*/
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
     Chat() << "re-simplifying assertions..." << endl;
     ScopeCounter depth(d_simplifyAssertionsDepth);
     noConflict &= simplifyAssertions();
@@ -3761,7 +3769,7 @@ void SmtEnginePrivate::processAssertions() {
       removeITEs();
       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
     }
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;*/
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
   }
   dumpAssertions("post-repeat-simplify", d_assertions);