Merge branch 'master' into rm_svn

13 files changed, 115 insertions, 83 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 10c0c8e26..19d7840a8 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1429,12 +1429,12 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
 /* Solver                                                                     */
 /* -------------------------------------------------------------------------- */
 
-Solver::Solver(Options* opts) : d_opts(new Options())
+Solver::Solver(Options* opts)
 {
-  if (opts) d_opts->copyValues(*opts);
-  d_exprMgr = std::unique_ptr<ExprManager>(new ExprManager(*d_opts));
+  d_exprMgr = std::unique_ptr<ExprManager>(
+      opts == nullptr ? new ExprManager(Options()) : new ExprManager(*opts));
   d_smtEngine = std::unique_ptr<SmtEngine>(new SmtEngine(d_exprMgr.get()));
-  d_rng = std::unique_ptr<Random>(new Random((*d_opts)[options::seed]));
+  d_rng = std::unique_ptr<Random>(new Random((*opts)[options::seed]));
 }
 
 Solver::~Solver() {}
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index b76fbb08f..c3c429009 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2355,8 +2355,6 @@ class CVC4_PUBLIC Solver
   /* Helper to convert a vector of sorts to internal types. */
   std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
 
-  /* The options of this solver. */
-  std::unique_ptr<Options> d_opts;
   /* The expression manager of this solver. */
   std::unique_ptr<ExprManager> d_exprMgr;
   /* The SMT engine of this solver. */
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index bb2832ee3..816b40daa 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -282,7 +282,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
 #endif /* PORTFOLIO_BUILD */
-      InteractiveShell shell(*exprMgr, opts);
+      InteractiveShell shell(*exprMgr);
       if(opts.getInteractivePrompt()) {
         Message() << Configuration::getPackageName()
                   << " " << Configuration::getVersionString();
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 473f7b039..f1220b961 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -88,14 +88,13 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBREADLINE */
 
-InteractiveShell::InteractiveShell(ExprManager& exprManager,
-                                   const Options& options)
-    : d_in(*options.getIn()),
-      d_out(*options.getOutConst()),
-      d_options(options),
+InteractiveShell::InteractiveShell(ExprManager& exprManager)
+    : d_options(exprManager.getOptions()),
+      d_in(*d_options.getIn()),
+      d_out(*d_options.getOutConst()),
       d_quit(false)
 {
-  ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
+  ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
   if(d_options.wasSetByUserForceLogicString()) {
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index b512fe5f0..203dfb766 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -2,7 +2,7 @@
 /*! \file interactive_shell.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Tim King
+ **   Morgan Deters, Christopher L. Conway, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -32,11 +32,12 @@ namespace parser {
   class Parser;
 }/* CVC4::parser namespace */
 
-class CVC4_PUBLIC InteractiveShell {
+class CVC4_PUBLIC InteractiveShell
+{
+  const Options& d_options;
   std::istream& d_in;
   std::ostream& d_out;
   parser::Parser* d_parser;
-  const Options& d_options;
   bool d_quit;
   bool d_usingReadline;
 
@@ -46,25 +47,23 @@ class CVC4_PUBLIC InteractiveShell {
   static const unsigned s_historyLimit = 500;
 
 public:
-  InteractiveShell(ExprManager& exprManager, const Options& options);
-
-  /**
-   * Close out the interactive session.
-   */
-  ~InteractiveShell();
-
-  /**
-   * Read a command from the interactive shell. This will read as
-   * many lines as necessary to parse a well-formed command.
-   */
-  Command* readCommand();
-
-  /**
-   * Return the internal parser being used.
-   */
-  parser::Parser* getParser() {
-    return d_parser;
-  }
+ InteractiveShell(ExprManager& exprManager);
+
+ /**
+  * Close out the interactive session.
+  */
+ ~InteractiveShell();
+
+ /**
+  * Read a command from the interactive shell. This will read as
+  * many lines as necessary to parse a well-formed command.
+  */
+ Command* readCommand();
+
+ /**
+  * Return the internal parser being used.
+  */
+ parser::Parser* getParser() { return d_parser; }
 
 };/* class InteractiveShell */
 
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index b7078225a..4c08d7e47 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -95,7 +95,13 @@ Node BoolToBV::lowerNode(TNode current, bool topLevel)
       Kind new_kind = kind;
       switch (kind)
       {
-        case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break;
+        case kind::EQUAL:
+          if (current[0].getType().isBitVector()
+              || current[0].getType().isBoolean())
+          {
+            new_kind = kind::BITVECTOR_COMP;
+          }
+          break;
         case kind::AND: new_kind = kind::BITVECTOR_AND; break;
         case kind::OR: new_kind = kind::BITVECTOR_OR; break;
         case kind::NOT: new_kind = kind::BITVECTOR_NOT; break;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0e1df15b5..64a52c23f 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -971,6 +971,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::BITVECTOR_SLE: return "bvsle";
   case kind::BITVECTOR_SGT: return "bvsgt";
   case kind::BITVECTOR_SGE: return "bvsge";
+  case kind::BITVECTOR_TO_NAT: return "bv2nat";
   case kind::BITVECTOR_REDOR: return "bvredor";
   case kind::BITVECTOR_REDAND: return "bvredand";
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d19378f72..9ecbbc99c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -477,28 +477,36 @@ bool TheoryBV::doExtfInferences(std::vector<Node>& terms)
         d_extf_collapse_infer.insert(cterm);
 
         Node t = n[0];
-        if (n.getKind() == kind::INT_TO_BITVECTOR)
+        if (t.getType() == parent.getType())
         {
-          Assert(t.getType().isInteger());
-          // congruent modulo 2^( bv width )
-          unsigned bvs = n.getType().getBitVectorSize();
-          Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
-          Node k = nm->mkSkolem(
-              "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
-          t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
-        }
-        Node lem = parent.eqNode(t);
+          if (n.getKind() == kind::INT_TO_BITVECTOR)
+          {
+            Assert(t.getType().isInteger());
+            // congruent modulo 2^( bv width )
+            unsigned bvs = n.getType().getBitVectorSize();
+            Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs)));
+            Node k = nm->mkSkolem(
+                "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence");
+            t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k));
+          }
+          Node lem = parent.eqNode(t);
 
-        if (parent[0] != n)
-        {
-          Assert(ee->areEqual(parent[0], n));
-          lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
+          if (parent[0] != n)
+          {
+            Assert(ee->areEqual(parent[0], n));
+            lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem);
+          }
+          // this handles inferences of the form, e.g.:
+          //   ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
+          //   (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
+          Trace("bv-extf-lemma")
+              << "BV extf lemma (collapse) : " << lem << std::endl;
+          d_out->lemma(lem);
+          sentLemma = true;
         }
-        Trace("bv-extf-lemma")
-            << "BV extf lemma (collapse) : " << lem << std::endl;
-        d_out->lemma(lem);
-        sentLemma = true;
       }
+      Trace("bv-extf-lemma-debug")
+          << "BV extf f collapse based on : " << cterm << std::endl;
     }
   }
   return sentLemma;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c48708126..05bb695e5 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -181,7 +181,28 @@ private:
   bool d_needsLastCallCheck;
   context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer;
   context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer;
+  /** do extended function inferences
+   *
+   * This method adds lemmas on the output channel of TheoryBV based on
+   * reasoning about extended functions, such as bv2nat and int2bv. Examples
+   * of lemmas added by this method include:
+   *   0 <= ((_ int2bv w) x) < 2^w
+   *   ((_ int2bv w) (bv2nat x)) = x
+   *   (bv2nat ((_ int2bv w) x)) == x + k*2^w
+   * The purpose of these lemmas is to recognize easy conflicts before fully
+   * reducing extended functions based on their full semantics.
+   */
   bool doExtfInferences( std::vector< Node >& terms );
+  /** do extended function reductions
+   *
+   * This method adds lemmas on the output channel of TheoryBV based on
+   * reducing all extended function applications that are preregistered to
+   * this theory and have not already been reduced by context-dependent
+   * simplification (see theory/ext_theory.h). Examples of lemmas added by
+   * this method include:
+   *   (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... +
+   *                (ite ((_ extract 1 0) x) 1 0)
+   */
   bool doExtfReductions( std::vector< Node >& terms );
   
   bool wasPropagatedBySubtheory(TNode literal) const {
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 8c6b5afbc..a079017cd 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1065,6 +1065,8 @@ Node ConjectureGenerator::getPredicateForType( TypeNode tn ) {
 
 void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) {
   if( n.getNumChildren()>0 ){
+    Trace("sg-gt-enum-debug") << "Get enumerate uf terms " << n << " (" << num
+                              << ")" << std::endl;
     TermEnumeration* te = d_quantEngine->getTermEnumeration();
     // below, we do a fair enumeration of vectors vec of indices whose sum is
     // 1,2,3, ...
@@ -1090,7 +1092,6 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
     unsigned index = 0;
     unsigned last_size = terms.size();
     while( terms.size()<num ){
-      bool success = true;
       if( vec_sum==-1 ){
         vec_sum = 0;
         // we will construct a new child below
@@ -1114,22 +1115,10 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
           vec_sum -= vec[index];
           vec[index] = 0;
           index++;
-          if (index == vec.size())
-          {
-            // no more indices to iterate, we increment limit and reset below
-            success = false;
-          }
         }
       }
-      else
+      if (index < vec.size())
       {
-        // This should never happen due to invariants of this loop.
-        // However, if it does, we simply abort while not fully enumerating the
-        // full set of terms.
-        Assert(false);
-        return;
-      }
-      if( success ){
         // if we are ready to construct the term
         if( vec.size()==n.getNumChildren() ){
           Node lc =
@@ -1161,6 +1150,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
           index = 0;
         }
       }else{
+        // no more indices to increment, we reset and increment size_limit
         if( terms.size()>last_size ){
           last_size = terms.size();
           size_limit++;
@@ -1169,7 +1159,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
           }
           vec_sum = -1;
         }else{
-          // we've saturated, no more terms can be enumerated
+          // No terms were generated at the previous size.
+          // Thus, we've saturated, no more terms can be enumerated.
           return;
         }
       }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index c15e3d045..0b9e415fa 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1045,6 +1045,7 @@ REG1_TESTS = \
 	regress1/bv/bv-proof00.smt \
 	regress1/bv/bv2nat-ground.smt2 \
 	regress1/bv/bv2nat-simp-range-sat.smt2 \
+	regress1/bv/bv2nat-types.smt2 \
 	regress1/bv/cmu-rdk-3.smt2 \
 	regress1/bv/decision-weight00.smt2 \
 	regress1/bv/divtest.smt2 \
diff --git a/test/regress/regress1/bv/bv2nat-types.smt2 b/test/regress/regress1/bv/bv2nat-types.smt2
new file mode 100644
index 000000000..e75ffb3ca
--- /dev/null
+++ b/test/regress/regress1/bv/bv2nat-types.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_ALL)
+(set-info :status sat)
+(declare-fun x () (_ BitVec 8))
+(assert 
+(= (concat #b000000000000000000000000 x) ((_ int2bv 32) (bv2nat x)))
+)
+(check-sat)
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index e42172251..cf68b5465 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -38,13 +38,14 @@ private:
   stringstream* d_sin;
   stringstream* d_sout;
 
-  /** Read up to maxCommands+1 from the shell and throw an assertion
-      error if it's fewer than minCommands and more than maxCommands.
-      Note that an empty string followed by EOF may be returned as an
-      empty command, and not NULL (subsequent calls to readCommand()
-      should return NULL). E.g., "CHECKSAT;\n" may return two
-      commands: the CHECKSAT, followed by an empty command, followed
-      by NULL. */
+  /**
+   * Read up to maxCommands+1 from the shell and throw an assertion error if
+   * it's fewer than minCommands and more than maxCommands.
+   * Note that an empty string followed by EOF may be returned as an empty
+   * command, and not NULL (subsequent calls to readCommand() should return
+   * NULL). E.g., "CHECKSAT;\n" may return two commands: the CHECKSAT,
+   * followed by an empty command, followed by NULL.
+   */
   void countCommands(InteractiveShell& shell, 
                      int minCommands, 
                      int maxCommands) {
@@ -60,12 +61,12 @@ private:
 
  public:
   void setUp() {
-    d_exprManager = new ExprManager;
     d_sin = new stringstream;
     d_sout = new stringstream;
     d_options.set(options::in, d_sin);
     d_options.set(options::out, d_sout);
     d_options.set(options::inputLanguage, language::input::LANG_CVC4);
+    d_exprManager = new ExprManager(d_options);
   }
 
   void tearDown() {
@@ -76,18 +77,18 @@ private:
 
   void testAssertTrue() {
     *d_sin << "ASSERT TRUE;\n" << flush;
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     countCommands( shell, 1, 1 );
   }
 
   void testQueryFalse() {
     *d_sin << "QUERY FALSE;\n" << flush;
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     countCommands( shell, 1, 1 );
   }
 
   void testDefUse() {
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     *d_sin << "x : REAL; ASSERT x > 0;\n" << flush;
     /* readCommand may return a sequence, so we can't say for sure
        whether it will return 1 or 2... */
@@ -95,7 +96,7 @@ private:
   }
 
   void testDefUse2() {
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     /* readCommand may return a sequence, see above. */
     *d_sin << "x : REAL;\n" << flush;
     Command* tmp = shell.readCommand();
@@ -105,14 +106,14 @@ private:
   }
 
   void testEmptyLine() {
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     *d_sin << flush;
     countCommands(shell,0,0);
   }
 
   void testRepeatedEmptyLines() {
     *d_sin << "\n\n\n";
-    InteractiveShell shell(*d_exprManager, d_options);
+    InteractiveShell shell(*d_exprManager);
     /* Might return up to four empties, might return nothing */
     countCommands( shell, 0, 3 );
   }